Make in-memory format of capabilities conform with that of CHERI which stores an absolute cursor instead of offset relative to base as a uarch optimisation. This is now part of the ISA and there is a test for it.

2 files changed, 28 insertions, 3 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index d3d84a53..132d7da3 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -727,13 +727,13 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
             else if (conditional) then
               {
                 success := if (CP0LLBit[0]) then
-                    MEMw_tagged_conditional(pAddr, cs_val.tag, (capStructToBit257(cs_val))[255..0])
+                    MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
                   else
                     false;
                 wGPR(rd) := EXTZ([success]);
               }
             else
-              MEMw_tagged(pAddr, cs_val.tag, (capStructToBit257(cs_val))[255..0]);
+              MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
           }
       }
   }
@@ -779,7 +779,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
               else 
                 (MEMr_tagged(pAddr)))
             in
-            (CapRegs[cd]) := ([tag & (~(suppressTag))] : mem);
+            (CapRegs[cd]) := memBitsToCapBits(tag & (~(suppressTag)), mem);
           }
       }
   }
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index ec0ba6e8..c8483548 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -208,6 +208,31 @@ function (bit[31]) capPermsToVec((CapStruct) cap) =
       : [cap.global]
   )
 
+(* Function used to convert capabilities to in-memory format 
+   - this is the same as register format except for the offset,
+     field which is stored as an absolute cursor on CHERI
+     due to uarch optimisation *)
+function (bit[256]) capStructToMemBits((CapStruct) cap) =
+  (
+        cap.padding
+      : cap.otype
+      : capPermsToVec(cap)
+      : [cap.sealed]
+        (* NB in memory format stores cursor, not offset *)
+      : (cap.base + cap.offset) 
+      : cap.base
+      : cap.length
+  )
+
+
+(* Reverse of above used when reading from memory *)
+function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) =
+  ([tag]
+   : b[255..192]
+   : ((bit[64])(b[191..128] - b[127..64]))
+   : b[127..0]
+  )
+
 function (bit[257]) capStructToBit257((CapStruct) cap) =
     (
       [cap.tag]