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

5 files changed, 64 insertions, 41 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;
+  }
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 15aad01d..bb7f991f 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1072,20 +1072,20 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
                   {
                     success := if (CP0LLBit[0]) then switch(width)
                     {
-                      case B -> MEMw_conditional(pAddr, 1, rt_val[7..0])
-                      case H -> MEMw_conditional(pAddr, 2, rt_val[15..0])
-                      case W -> MEMw_conditional(pAddr, 4, rt_val[31..0])
-                      case D -> MEMw_conditional(pAddr, 8, rt_val)
+                      case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0])
+                      case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0])
+                      case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0])
+                      case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val)
                     } else false;
                     wGPR(rt) := EXTZ([success])
                   }
                 else
                   switch(width)
                     {
-                      case B -> MEMw(pAddr, 1) := rt_val[7..0]
-                      case H -> MEMw(pAddr, 2) := rt_val[15..0]
-                      case W -> MEMw(pAddr, 4) := rt_val[31..0]
-                      case D -> MEMw(pAddr, 8) := rt_val
+                      case B -> MEMw_wrapper(pAddr, 1) := rt_val[7..0]
+                      case H -> MEMw_wrapper(pAddr, 2) := rt_val[15..0]
+                      case W -> MEMw_wrapper(pAddr, 4) := rt_val[31..0]
+                      case D -> MEMw_wrapper(pAddr, 8) := rt_val
                     }
           }
       }
@@ -1143,10 +1143,10 @@ function clause execute(SWL(base, rt, offset)) =
             reg_val   := rGPR(rt);
             switch (vAddr[1..0])
             {
-              case 0b00 -> (MEMw(pAddr, 4) := reg_val[31..0])
-              case 0b01 -> (MEMw(pAddr, 3) := reg_val[31..8])
-              case 0b10 -> (MEMw(pAddr, 2) := reg_val[31..16])
-              case 0b11 -> (MEMw(pAddr, 1) := reg_val[31..24])
+              case 0b00 -> (MEMw_wrapper(pAddr, 4) := reg_val[31..0])
+              case 0b01 -> (MEMw_wrapper(pAddr, 3) := reg_val[31..8])
+              case 0b10 -> (MEMw_wrapper(pAddr, 2) := reg_val[31..16])
+              case 0b11 -> (MEMw_wrapper(pAddr, 1) := reg_val[31..24])
             }
           }
       }
@@ -1163,10 +1163,10 @@ function clause execute(SWR(base, rt, offset)) =
             reg_val   := rGPR(rt);
             switch (vAddr[1..0])
               {
-                case 0b00 -> (MEMw(wordAddr, 1) := reg_val[7..0])
-                case 0b01 -> (MEMw(wordAddr, 2) := reg_val[15..0])
-                case 0b10 -> (MEMw(wordAddr, 3) := reg_val[23..0])
-                case 0b11 -> (MEMw(wordAddr, 4) := reg_val[31..0])
+                case 0b00 -> (MEMw_wrapper(wordAddr, 1) := reg_val[7..0])
+                case 0b01 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0])
+                case 0b10 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0])
+                case 0b11 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0])
               }
           }
       }
@@ -1233,14 +1233,14 @@ function clause execute(SDL(base, rt, offset)) =
             reg_val := rGPR(rt);
             switch (vAddr[2..0])
             {
-              case 0b000 -> (MEMw(pAddr, 8) := reg_val[63..00])
-              case 0b001 -> (MEMw(pAddr, 7) := reg_val[63..08])
-              case 0b010 -> (MEMw(pAddr, 6) := reg_val[63..16])
-              case 0b011 -> (MEMw(pAddr, 5) := reg_val[63..24])
-              case 0b100 -> (MEMw(pAddr, 4) := reg_val[63..32])
-              case 0b101 -> (MEMw(pAddr, 3) := reg_val[63..40])
-              case 0b110 -> (MEMw(pAddr, 2) := reg_val[63..48])
-              case 0b111 -> (MEMw(pAddr, 1) := reg_val[63..56])
+              case 0b000 -> (MEMw_wrapper(pAddr, 8) := reg_val[63..00])
+              case 0b001 -> (MEMw_wrapper(pAddr, 7) := reg_val[63..08])
+              case 0b010 -> (MEMw_wrapper(pAddr, 6) := reg_val[63..16])
+              case 0b011 -> (MEMw_wrapper(pAddr, 5) := reg_val[63..24])
+              case 0b100 -> (MEMw_wrapper(pAddr, 4) := reg_val[63..32])
+              case 0b101 -> (MEMw_wrapper(pAddr, 3) := reg_val[63..40])
+              case 0b110 -> (MEMw_wrapper(pAddr, 2) := reg_val[63..48])
+              case 0b111 -> (MEMw_wrapper(pAddr, 1) := reg_val[63..56])
             }
           }
       }
@@ -1259,14 +1259,14 @@ function clause execute(SDR(base, rt, offset)) =
             wordAddr := pAddr[63..3] : 0b000;
             switch (vAddr[2..0])
             {
-              case 0b000 -> (MEMw(wordAddr, 1) := reg_val[07..0])
-              case 0b001 -> (MEMw(wordAddr, 2) := reg_val[15..0])
-              case 0b010 -> (MEMw(wordAddr, 3) := reg_val[23..0])
-              case 0b011 -> (MEMw(wordAddr, 4) := reg_val[31..0])
-              case 0b100 -> (MEMw(wordAddr, 5) := reg_val[39..0])
-              case 0b101 -> (MEMw(wordAddr, 6) := reg_val[47..0])
-              case 0b110 -> (MEMw(wordAddr, 7) := reg_val[55..0])
-              case 0b111 -> (MEMw(wordAddr, 8) := reg_val[63..0])
+              case 0b000 -> (MEMw_wrapper(wordAddr, 1) := reg_val[07..0])
+              case 0b001 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0])
+              case 0b010 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0])
+              case 0b011 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0])
+              case 0b100 -> (MEMw_wrapper(wordAddr, 5) := reg_val[39..0])
+              case 0b101 -> (MEMw_wrapper(wordAddr, 6) := reg_val[47..0])
+              case 0b110 -> (MEMw_wrapper(wordAddr, 7) := reg_val[55..0])
+              case 0b111 -> (MEMw_wrapper(wordAddr, 8) := reg_val[63..0])
             }
           }
       }
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
new file mode 100644
index 00000000..218f985a
--- /dev/null
+++ b/mips/mips_wrappers.sail
@@ -0,0 +1,3 @@
+function unit effect {wmem} MEMw_wrapper(addr, size, data) = MEMw(addr, size, data)
+function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+  MEMw_conditional(addr, size, data)
\ No newline at end of file
diff --git a/src/Makefile b/src/Makefile
index 12535ace..cd21ed1a 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,7 +25,7 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
 ELFDIR= $(BITBUCKET_ROOT)/linksem
 
 MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/l2/mips
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/l2/cheri
 CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail