Introduce wrapper function around MEMw* so that we can clear tags on non-capability writes on cheri.

2 files changed, 28 insertions, 8 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index ee7ae0d4..935f47ca 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -573,10 +573,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
                 success := if (CP0LLBit[0]) then
                     switch(width)
                       {
-                        case B -> MEMw_conditional(pAddr, 1, rs_val[7..0])
-                        case H -> MEMw_conditional(pAddr, 2, rs_val[15..0])
-                        case W -> MEMw_conditional(pAddr, 4, rs_val[31..0])
-                        case D -> MEMw_conditional(pAddr, 8, rs_val)
+                        case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
+                        case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0])
+                        case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0])
+                        case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val)
                       }
                   else
                     false;
@@ -585,10 +585,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
               else
             switch(width)
               {
-                case B -> MEMw(pAddr, 1) := rs_val[7..0]
-                case H -> MEMw(pAddr, 2) := rs_val[15..0]
-                case W -> MEMw(pAddr, 4) := rs_val[31..0]
-                case D -> MEMw(pAddr, 8) := rs_val
+                case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0]
+                case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0]
+                case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0]
+                case D -> MEMw_wrapper(pAddr, 8) := rs_val
               }
           }
       }
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 78bf019f..94e5e759 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -316,6 +316,7 @@ val extern (bit[64]) -> (bit[8]) effect { rmem } TAGr
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
 {
+  (* assumes addr is cap. aligned *)
   let tag = (TAGr (addr)) in
   let mem = (MEMr (addr, cap_size)) in
   (tag[0], mem)
@@ -323,6 +324,7 @@ function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
 {
+  (* assumes addr is cap. aligned *)
   let tag = (TAGr (addr)) in
   let mem = (MEMr_reserve (addr, cap_size)) in
   (tag[0], mem)
@@ -330,14 +332,32 @@ function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
 
 function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
+  (* assumes addr is cap. aligned *)
   MEMw(addr, cap_size, data);
   TAGw(addr, (0b0000000 : [tag]));
 }
 
 function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
+  (* assumes addr is cap. aligned *)
   success := MEMw_conditional(addr, cap_size, data);
   if (success) then
     TAGw(addr, (0b0000000 : [tag]));
   success;
 }
+
+function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+  {
+    (* On cheri non-capability writes must clear the corresponding tag*)
+    TAGw((addr[63..5] : 0b00000), 0x00);
+    MEMw(addr,size,data)
+  }
+
+function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+  {
+    (* On cheri non-capability writes must clear the corresponding tag*)
+    success := MEMw_conditional(addr,size,data);
+    if (success) then
+      TAGw((addr[63..5] : 0b00000), 0x00);
+    success;
+  }