revised ccopytype with check for offset being in bounds and clearing tag instead of using magic value if unsealed. Also corresponding CCSeal instruction which degrades to a cmove if ct.tag is unset.

1 files changed, 54 insertions, 10 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index ad933dea..2a5ae43f 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -586,6 +586,8 @@ function clause execute (CCopyType(cd, cb, ct)) =
   cb_val := readCapReg(cb);
   ct_val := readCapReg(ct);
   cb_base := getCapBase(cb_val);
+  cb_top  := getCapTop(cb_val);
+  ct_otype := unsigned(ct_val.otype);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -596,18 +598,18 @@ function clause execute (CCopyType(cd, cb, ct)) =
     raise_c2_exception(CapEx_TagViolation, cb)
   else if (cb_val.sealed) then
     raise_c2_exception(CapEx_SealViolation, cb)
-  else
-    {
-      let newOffset = if (ct_val.sealed) 
-        then 
-          unsigned(ct_val.otype) - cb_base
-        else
-          -1 in
-      let (success, cap) = setCapOffset(cb_val, (bit[64]) newOffset) in {
+  else if (ct_val.sealed) then {
+    if ct_otype < cb_base then
+      raise_c2_exception(CapEx_LengthViolation, cb)
+    else if ct_otype >= cb_top then
+      raise_c2_exception(CapEx_LengthViolation, cb)
+    else
+      let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in {
+        assert(success, None); (* offset is in bounds so must succeed *)
         writeCapReg(cd, cap);
-        assert(success, None); (*XXX TODO can this fail*)
       }
-    }
+  } else
+    writeCapReg(cd, {cb_val with tag=false})
   (* END_CCopyType *)
 }
 
@@ -700,6 +702,48 @@ function clause execute (CSeal(cd, cs, ct)) =
   (* END_CSeal *)
 }
 
+union ast member regregreg CCSeal
+(*function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CCSeal(cd, cs, ct)) XXX no encoding yet *)
+function clause execute (CCSeal(cd, cs, ct)) =
+{
+  (* START_CCSeal *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  ct_val := readCapReg(ct);
+  ct_cursor := getCapCursor(ct_val);
+  ct_top    := getCapTop(ct_val);
+  ct_base   := getCapBase(ct_val);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (ct_val.tag) then
+    writeCapReg(cd, cs_val)
+  else if (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if (ct_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, ct)
+  else if not (ct_val.permit_seal) then
+    raise_c2_exception(CapEx_PermitSealViolation, ct)
+  else if (ct_cursor < ct_base) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else if (ct_cursor >= ct_top) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else if (ct_cursor > max_otype) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else
+    let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in
+    if not (success) then
+        raise_c2_exception(CapEx_InexactBounds, cs)
+    else
+        writeCapReg(cd, newCap)
+  (* END_CCSeal *)
+}
+
 union ast member regregreg CUnseal
 function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct))
 function clause execute (CUnseal(cd, cs, ct)) =