Split handle_load_cap_via_cap into worker/wrapper

CTSRD-CHERI · Sep 29, 2021 · 024900a · 024900a
1 parent 4a63d1a
commit 024900a
Showing 1 changed file with 22 additions and 16 deletions.
diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail
@@ -60,6 +60,8 @@
 /*  SUCH DAMAGE.                                                                         */
 /*=======================================================================================*/
 
+val load_cap_via_cap : (capreg_idx, Capability, xlenbits) -> option(Capability) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+
 /* Capability versions of mode-dependent instructions */
 
 union clause ast = AUIPCC : (bits(20), regidx)
@@ -1469,58 +1471,62 @@ function clause execute (LoadDataCap(rd, cs1, is_unsigned, width)) = {
   handle_load_data_via_cap(rd, 0b0 @ cs1, cs1_val, vaddr, is_unsigned, width)
 }
 
-val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
-function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
+function load_cap_via_cap(auth_idx, auth_val, vaddrBits) = {
   let aq : bool = false;
   let rl : bool = false;
   if not(auth_val.tag) then {
     handle_cheri_cap_exception(CapEx_TagViolation, auth_idx);
-    RETIRE_FAIL
+    None()
   } else if isCapSealed(auth_val) then {
     handle_cheri_cap_exception(CapEx_SealViolation, auth_idx);
-    RETIRE_FAIL
+    None()
   } else if not (auth_val.permit_load) then {
     handle_cheri_cap_exception(CapEx_PermitLoadViolation, auth_idx);
-    RETIRE_FAIL
+    None()
   } else if not(inCapBounds(auth_val, vaddrBits, cap_size)) then {
     handle_cheri_cap_exception(CapEx_LengthViolation, auth_idx);
-    RETIRE_FAIL
+    None()
   } else if not(is_aligned_addr(vaddrBits, cap_size)) then {
     handle_mem_exception(vaddrBits, E_Load_Addr_Align());
-    RETIRE_FAIL
+    None()
   } else match translateAddr(vaddrBits, Read(Cap)) {
     TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap load") },
-    TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
+    TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); None() },
     TR_Address(addr, ptw_info) => {
       let c = mem_read_cap(addr, aq, aq & rl, false);
       match c {
         MemValue(v) => {
           match ptw_info.ptw_lc {
             PTW_LC_OK => {
-              C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
-              RETIRE_SUCCESS
+              Some({ v with tag = v.tag & auth_val.permit_load_cap })
             },
             PTW_LC_CLEAR => {
-              C(cd) = { v with tag = false };
-              RETIRE_SUCCESS
+              Some({ v with tag = false })
             },
             PTW_LC_TRAP  => {
               if v.tag then {
                 handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
-                RETIRE_FAIL
+                None()
               } else {
-                C(cd) = v;
-                RETIRE_SUCCESS
+                Some(v)
               }
             }
           }
         },
-        MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
+        MemException(e) => {handle_mem_exception(vaddrBits, e); None() }
       }
     }
   }
 }
 
+val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
+  match load_cap_via_cap(auth_idx, auth_val, vaddrBits) {
+    None() => RETIRE_FAIL,
+    Some(v) => { C(cd) = v; RETIRE_SUCCESS }
+  }
+}
+
 union clause ast = LoadCapDDC : (regidx, regidx)
 /*!
  * Capability register *cd* is replaced with the capability located in memory