add support for the new ccall selector 1 implementation that directly unseals capabilities.

4 files changed, 65 insertions, 13 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index b11dadfa..fe55d7aa 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -637,9 +637,9 @@ function clause execute (CUnseal(cd, cs, ct)) =
   (* END_CUnseal *)
 }
 
-union ast member (regno, regno) CCall
-function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb))
-function clause execute (CCall(cs, cb)) =
+union ast member (regno, regno, bit[11]) CCall
+function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb, selector))
+function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *)
 {
   (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *)
   (* START_CCall *)
@@ -674,6 +674,56 @@ function clause execute (CCall(cs, cb)) =
   (* END_CCall *)
 }
 
+function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
+{
+  (* Jump-like implementation of CCall that unseals arguments *)
+  (* START_CCall2 *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  cs_cursor := getCapCursor(cs_val);
+  if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if not (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if not (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if ((cs_val.otype) != (cb_val.otype)) then
+    raise_c2_exception(CapEx_TypeViolation, cs)
+  else if not (cs_val.permit_ccall) then
+    raise_c2_exception(CapEx_PermitCCallViolation, cs)
+  else if not (cb_val.permit_ccall) then
+    raise_c2_exception(CapEx_PermitCCallViolation, cb)
+  else if not (cs_val.permit_execute) then
+    raise_c2_exception(CapEx_PermitExecuteViolation, cs)
+  else if (cb_val.permit_execute) then
+    raise_c2_exception(CapEx_PermitExecuteViolation, cb)
+  else if (cs_cursor < getCapBase(cs_val)) then
+    raise_c2_exception(CapEx_LengthViolation, cs)
+  else if (cs_cursor >= getCapTop(cs_val)) then
+    raise_c2_exception(CapEx_LengthViolation, cs)
+  else
+    let csUnsealed = capStructToCapReg({cs_val with
+        sealed=false;
+        otype=0;
+    }) in {
+      nextPC := (bit[64]) (getCapOffset(cs_val));
+      nextPCC := csUnsealed;
+      delayedPCC := csUnsealed;
+      C26 := capStructToCapReg({cb_val with
+        sealed=false;
+        otype=0;
+      });
+    }
+  (* END_CCall2 *)
+}
+
 union ast member unit CReturn
 function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
 function clause execute (CReturn) =
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 2bdbbe77..98b0a40c 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -40,7 +40,7 @@ typedef CapStruct = const struct {
   bit[4]  uperms;
   bool    access_system_regs;
   bool    perm_reserved9;
-  bool    perm_reserved8;
+  bool    permit_ccall;
   bool    permit_seal;
   bool    permit_store_local_cap;
   bool    permit_store_cap;
@@ -63,7 +63,7 @@ let (CapStruct) null_cap = {
   uperms                 = 0;
   access_system_regs     = false;
   perm_reserved9         = false;
-  perm_reserved8         = false;
+  permit_ccall           = false;
   permit_seal            = false;
   permit_store_local_cap = false;
   permit_store_cap       = false;
@@ -94,7 +94,7 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     uperms                 = c[127..124];
     access_system_regs     = c[123];
     perm_reserved9         = c[122];
-    perm_reserved8         = c[121];
+    permit_ccall           = c[121];
     permit_seal            = c[120];
     permit_store_local_cap = c[119];
     permit_store_cap       = c[118];
@@ -115,7 +115,7 @@ function CapStruct capRegToCapStruct((CapReg) c) =
 function (bit[11]) getCapHardPerms((CapStruct) cap) =
    ([cap.access_system_regs]
   : [cap.perm_reserved9]
-  : [cap.perm_reserved8]
+  : [cap.permit_ccall]
   : [cap.permit_seal]
   : [cap.permit_store_local_cap]
   : [cap.permit_store_cap]
@@ -157,7 +157,7 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
       (* 14..11 reserved -- ignore *)
       access_system_regs     = perms[10];
       perm_reserved9         = perms[9];
-      perm_reserved8         = perms[8];
+      permit_ccall           = perms[8];
       permit_seal            = perms[7];
       permit_store_local_cap = perms[6];
       permit_store_cap       = perms[5];
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 388d9ed7..f41d9c14 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -43,7 +43,7 @@ typedef CapStruct = const struct {
   bit[4]  perm_reserved11_14;
   bool    access_system_regs;
   bool    perm_reserved9;
-  bool    perm_reserved8;
+  bool    permit_ccall;
   bool    permit_seal;
   bool    permit_store_local_cap;
   bool    permit_store_cap;
@@ -66,7 +66,7 @@ let (CapStruct) null_cap = {
   perm_reserved11_14 = 0;
   access_system_regs = false;
   perm_reserved9 = false;
-  perm_reserved8 = false;
+  permit_ccall = false;
   permit_seal = false;
   permit_store_local_cap = false;
   permit_store_cap = false;
@@ -93,7 +93,7 @@ function CapStruct capRegToCapStruct((CapReg) capReg) =
     perm_reserved11_14         = capReg[207..204];
     access_system_regs         = capReg[203];
     perm_reserved9             = capReg[202];
-    perm_reserved8             = capReg[201];
+    permit_ccall               = capReg[201];
     permit_seal                = capReg[200];
     permit_store_local_cap     = capReg[199];
     permit_store_cap           = capReg[198];
@@ -114,7 +114,7 @@ function (bit[31]) getCapPerms((CapStruct) cap) =
       : cap.perm_reserved11_14
       : [cap.access_system_regs]
       : [cap.perm_reserved9]
-      : [cap.perm_reserved8]
+      : [cap.permit_ccall]
       : [cap.permit_seal]
       : [cap.permit_store_local_cap]
       : [cap.permit_store_cap]
@@ -169,7 +169,7 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
       perm_reserved11_14     = perms[14..11];
       access_system_regs     = perms[10];
       perm_reserved9         = perms[9];
-      perm_reserved8         = perms[8];
+      permit_ccall           = perms[8];
       permit_seal            = perms[7];
       permit_store_local_cap = perms[6];
       permit_store_cap       = perms[5];
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index b839b282..13b18ac1 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -104,6 +104,7 @@ typedef CapEx = enumerate {
   CapEx_PermitStoreLocalCapViolation;
   CapEx_PermitSealViolation;
   CapEx_AccessSystemRegsViolation;
+  CapEx_PermitCCallViolation;
 }
 
 typedef CPtrCmpOp = enumerate {
@@ -145,6 +146,7 @@ function (bit[8]) CapExCode((CapEx) ex) =
     case CapEx_PermitStoreLocalCapViolation -> 0x16
     case CapEx_PermitSealViolation          -> 0x17
     case CapEx_AccessSystemRegsViolation    -> 0x18
+    case CapEx_PermitCCallViolation         -> 0x19
   }
 
 typedef CapCauseReg = register bits [15:0] {