Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.

1 files changed, 17 insertions, 38 deletions

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 63af1021..b839b282 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -214,52 +214,38 @@ function bool register_inaccessible((regno) r) =
   else
     false
 
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag_reserve
 
-val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> unit effect { wmvt } MEMval_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> bool effect { wmvt } MEMval_tag_conditional
 
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
-{
   (* assumes addr is cap. aligned *)
-  let tagmem = reverse_endianness(MEMr_tag (addr, cap_size)) in
-  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
-  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
-  (tag[0], mem)
-}
+  let (tag, data) = MEMr_tag (addr, cap_size) in
+  (tag, reverse_endianness(data))
+
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
-{
   (* assumes addr is cap. aligned *)
-  let tagmem = reverse_endianness(MEMr_tag_reserve (addr, cap_size)) in
-  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
-  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
-  (tag[0], mem)
-}
+  let (tag, data) = MEMr_tag_reserve(addr, cap_size) in
+  (tag, reverse_endianness(data))
 
 function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  MEMea_tag(addr, cap_size);
-  MEMval_tag(addr, cap_size,  reverse_endianness(0b0000000 : [tag] : data));
+  MEMea(addr, cap_size);
+  MEMval_tag(addr, cap_size,  tag, reverse_endianness(data));
 }
 
 function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  MEMea_tag_conditional(addr, cap_size);
-  MEMval_tag_conditional(addr, cap_size, reverse_endianness(0b0000000 : [tag] : data));
+  MEMea_conditional(addr, cap_size);
+  MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
 }
 
-function (bit[64]) align((bit[64]) addr, (nat) alignment) =
-    let remainder = unsigned(addr) mod alignment in
-    addr - remainder
-
 function unit effect {wmem} MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
@@ -269,23 +255,16 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
   }
   else
   {
-    (* On cheri non-capability writes must clear the corresponding tag
-       XXX this is vestigal and only works on sequential modle -- tag clearing
-       should probably be done in memory model. *)
-    TAGw(align(addr, cap_size), 0x00);
-    MEMea(addr,size);
-    MEMval(addr, size, ledata);
+    (* On cheri non-capability writes must clear the corresponding tag *)
+    MEMea(addr, size);
+    MEMval_tag(addr, size, false, ledata);
   }
 
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
     MEMea_conditional(addr, size);
-    success := MEMval_conditional(addr,size,reverse_endianness(data));
-    if (success) then
-      (* XXX as above TAGw is vestigal and must die *)
-      TAGw(align(addr, cap_size), 0x00);
-    success;
+    MEMval_tag_conditional(addr,size,false,reverse_endianness(data));
   }
 
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =