WIP: points-to-PCC indirect sentries

src/cheri_cap_common.sail

@@ -416,6 +416,10 @@ function isCapSealed(cap) = signed(cap.otype) != otype_unsealed
 val hasReservedOType : Capability -> bool
 function hasReservedOType(cap) = unsigned(cap.otype) > cap_max_otype
 
+function isCapSentryOrIsentry(cap) : Capability -> bool =
+  let sotype = signed(cap.otype) in
+  (sotype == otype_sentry) | (sotype == otype_isentry_ptp)
+
 function sealCap(cap, otyp) : (Capability, bits(cap_otype_width)) -> Capability =
     {cap with otype=otyp}
 

src/cheri_insts.sail

@@ -110,6 +110,48 @@ function clause execute(CJAL(imm, cd)) = {
   }
 }
 
+val handle_cjalr_isentry_ptp : (regidx, regidx) -> Retired effect { escape, rmem, rmemt, rreg, wmv, wmvt, wreg }
+function handle_cjalr_isentry_ptp(cd, cs) = {
+  let cs_val = C(cs);
+  let idc = unsealCap(cs_val);
+  let idcaddr = cs_val.address;
+
+  // tag and otype has already been checked by caller
+  if not (idc.permit_load) | not (idc.permit_load_cap) then {
+    handle_cheri_reg_exception(CapEx_PermitLoadViolation, cs);
+    RETIRE_FAIL
+  } else if not(inCapBounds(idc, idcaddr, cap_size)) then {
+    handle_cheri_reg_exception(CapEx_LengthViolation, cs);
+    RETIRE_FAIL
+  } else if not(is_aligned_addr(idcaddr, cap_size)) then {
+    handle_mem_exception(idcaddr, E_Load_Addr_Align());
+    RETIRE_FAIL
+  } else {
+    match load_cap_via_cap(0b0 @ cs, cs_val, idcaddr) {
+      None() => RETIRE_FAIL,
+      Some(v) => {
+        if not (v.tag) then {
+          handle_cheri_reg_exception(CapEx_TagViolation, cs);
+          RETIRE_FAIL
+        } else if not (v.permit_execute) then {
+          handle_cheri_reg_exception(CapEx_PermitExecuteViolation, cs);
+          RETIRE_FAIL
+        } else {
+          /* Note that nextPC accounts for compressed instrucitons */
+          let (success, linkCap) = setCapAddr(PCC, nextPC);
+          assert(success, "Link cap should always be representable.");
+
+          C(cd) = sealCap(linkCap, to_bits(cap_otype_width, otype_sentry));
+          C(31) = idc;
+          nextPCC = v;
+          nextPC = [nextPCC.address with 0 = bitzero];
+          RETIRE_SUCCESS
+        }
+      }
+    }
+  }
+}
+
 union clause ast = CJALR : (bits(12), regidx, regidx)
 /*!
  * Capability register *cd* is replaced with the next instruction's **PCC** and
@@ -137,6 +179,9 @@ function clause execute(CJALR(imm, cs1, cd)) = {
   if not (cs1_val.tag) then {
     handle_cheri_reg_exception(CapEx_TagViolation, cs1);
     RETIRE_FAIL
+  } else if signed(cs1_val.otype) == otype_isentry_ptp then {
+    /* Indirect points-to-PCC sentries have their own requirements; jump out */
+    handle_cjalr_isentry_ptp(cd, cs1)
   } else if isCapSealed(cs1_val) &
             ((signed(cs1_val.otype) != otype_sentry) | imm != zeros()) then {
     handle_cheri_reg_exception(CapEx_SealViolation, cs1);
@@ -918,7 +963,7 @@ function clause execute (CBuildCap(cd, cs1, cs2)) = {
       RETIRE_FAIL
     } else {
       assert(exact, "CBuildCap: setCapBounds was not exact"); /* base and top came from cs2 originally so will be exact */
-      let cd5 = if signed(cs2_val.otype) == otype_sentry then sealCap(cd4, to_bits(cap_otype_width, otype_sentry)) else cd4;
+      let cd5 = if isCapSentryOrIsentry(cs2_val) then sealCap(cd4, cs2_val.otype) else cd4;
       C(cd) = cd5;
       RETIRE_SUCCESS
     }
@@ -1272,6 +1317,39 @@ function clause execute (CSealEntry(cd, cs1)) = {
   }
 }
 
+union clause ast = CSealPTPEntry : (regidx, regidx)
+/*!
+ * Capability register *cd* is replaced with capability register *cs1* and
+ * sealed as an indirect, points-to-PCC sentry
+ *
+ * ## Exceptions
+ *
+ * An exception is raised if:
+ *   - *cs1*.**tag** is not set.
+ *   - *cs1* is sealed.
+ *   - *cs1*.**perms** does not grant both **Permit_Load** and
+ *     **Permit_Load_Capability**.
+ */
+function clause execute (CSealPTPEntry(cd, cs1)) = {
+  let cs1_val = C(cs1);
+  if not (cs1_val.tag) then {
+    handle_cheri_reg_exception(CapEx_TagViolation, cs1);
+    RETIRE_FAIL
+  } else if (isCapSealed(cs1_val)) then {
+    handle_cheri_reg_exception(CapEx_SealViolation, cs1);
+    RETIRE_FAIL
+  } else if not (cs1_val.permit_load) then {
+    handle_cheri_reg_exception(CapEx_PermitLoadViolation, cs1);
+    RETIRE_FAIL
+  } else if not (cs1_val.permit_load_cap) then {
+    handle_cheri_reg_exception(CapEx_PermitLoadCapViolation, cs1);
+    RETIRE_FAIL
+  } else {
+    C(cd) = sealCap(cs1_val, to_bits(cap_otype_width, otype_isentry_ptp));
+    RETIRE_SUCCESS
+  }
+}
+
 union clause ast = CInvoke : (regidx, regidx)
 /*!
  * **PCC** is set equal to capability register *cs1* and unsealed with the 0th

src/cheri_types.sail

@@ -60,9 +60,10 @@
 /*  SUCH DAMAGE.                                                                         */
 /*=======================================================================================*/
 
-let reserved_otypes = 4
+let reserved_otypes = 8
 let otype_unsealed = -1
 let otype_sentry   = -2 /* Sealed erstwhile or prospective PCC */
+let otype_isentry_ptp = -3 /* Sealed erstwhile IDC pointing at PCC */
 
 enum CPtrCmpOp = {
   CEQ,