Plumb feature flags into PTW for data dependence control

Author: nwf

src/cheri_insts.sail

@@ -902,6 +902,9 @@ val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Reti
 function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
   let aq : bool = false;
   let rl : bool = false;
+
+  let vialc : bool = cap_val.permit_load_cap;
+
   if not(cap_val.tag) then {
     handle_cheri_cap_exception(CapEx_TagViolation, cs);
     RETIRE_FAIL
@@ -917,11 +920,9 @@ function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
   } else if not(is_aligned_addr(vaddrBits, cap_size)) then {
     handle_mem_exception(vaddrBits, E_Load_Addr_Align());
     RETIRE_FAIL
-  } else match translateAddr(vaddrBits, Read(Cap)) {
-    TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap load") },
+  } else match translateAddr(vaddrBits, Read(if vialc then Cap else Data)) {
     TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
     TR_Address(addr, ptw_info) => {
-      let vialc : bool = cap_val.permit_load_cap;
       let lcav : ext_ptw_lcm = ptw_info.ptw_lc_mod;
 
       let c = mem_read_cap(addr, aq, rl, false);

src/cheri_pte.sail

@@ -87,7 +87,7 @@ function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
 
 union PTE_Check = {
   PTE_Check_Success : ext_ptw,
-  PTE_Check_Failure : ext_ptw
+  PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
 }
 
 val checkPTEPermission_SC_caveat : Ext_PTE_Bits -> ext_ptw_scm
@@ -117,6 +117,51 @@ function checkPTEPermission_LC_caveat(p, e) =
               else PTW_LCM_TRAP
        }
 
+val checkPTEPermission_LC_caveat_datadep : (ext_ptw_lcm, ext_ptw) -> PTE_Check effect { rreg }
+function checkPTEPermission_LC_caveat_datadep(lcav, ext_ptw) = {
+  let ext_ptw' = ext_ptw_join_lcm(ext_ptw, lcav);
+  match (lcav) {
+    PTW_LCM_OK   => PTE_Check_Success(ext_ptw),
+    PTW_LCM_CLR  => PTE_Check_Success(ext_ptw'),
+    PTW_LCM_TRAP => {
+      if scisa.pte_cap_lc_datadep() == 0b1 then {
+        /*
+         * Continue translating, but add caveat
+         */
+        PTE_Check_Success(ext_ptw')
+      } else {
+        /*
+         * Stop translating and raise a trap now
+         */
+        PTE_Check_Failure(ext_ptw', EPTWF_CAP_ERR)
+      }
+    }
+  }
+}
+
+val checkPTEPermission_SC_caveat : Ext_PTE_Bits -> ext_ptw_scm
+function checkPTEPermission_SC_caveat(e) =
+  match (e.StoreCap(), e.StoreCap_Mod()) {
+    (0b1, _)   => PTW_SCM_OK,   /* Permitted */
+    (0b0, 0b0) => PTW_SCM_TRAP, /* Forbidden, unmodified */
+    (0b0, 0b1) => PTW_SCM_OK    /* Forbidden, modified; see update_PTE_bits */
+  }
+
+val checkPTEPermission_SC_caveat_datadep : (ext_ptw_scm, ext_ptw) -> PTE_Check effect { rreg }
+function checkPTEPermission_SC_caveat_datadep(scav, ext_ptw) = {
+  match (scav) {
+    PTW_SCM_OK => PTE_Check_Success(ext_ptw),
+    PTW_SCM_TRAP => {
+      let ext_ptw' = ext_ptw_join_scm(ext_ptw, scav);
+      if scisa.pte_cap_sc_datadep() == 0b1 then {
+        PTE_Check_Success(ext_ptw')
+      } else {
+        PTE_Check_Failure(ext_ptw', EPTWF_CAP_ERR)
+      }
+    }
+  }
+}
+
 function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
   /*
    * Although in many cases MXR doesn't make sense for capabilities, we honour
@@ -130,7 +175,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
    *
    * 3. It's simpler to implement yet still safe (LC is unaffected by MXR).
    */
-  let base_succ : bool =
+  let succ : bool =
   match (ac, priv) {
     (Read(_),      User)       => p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
     (Write(_),     User)       => p.U() == 0b1 & p.W() == 0b1,
@@ -145,27 +190,67 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (_,            Machine)    => internal_error("m-mode mem perm check")
   };
 
+  let res : PTE_Check =
+    if   succ
+    then PTE_Check_Success(ext_ptw)
+    else PTE_Check_Failure(ext_ptw, EPTWF_NO_PERM);
+
   let e = Mk_Ext_PTE_Bits(ext);
+
+  /* And now it's time for a little (manual, expanded) Either-monadic logic. */
+
+  /*
+   * Check for invalid modifiers
+   */
+  let res : PTE_Check =
+    match res {
+      PTE_Check_Failure(_, _) => res,
+      PTE_Check_Success(_) =>
+       if scisa.pte_cap_lsmod() == 0b0 &
+          ~(e.StoreCap_Mod() == 0b0 &
+            e.LoadCap_Mod() == 0b0 &
+            e.LoadCap_Gen() == 0b0)
+       then PTE_Check_Failure(ext_ptw, EPTWF_INVALID)
+       else res
+    };
+
+  /*
+   * Check for store-side caveats, which may force a fault if data-independent
+   */
   let scav = checkPTEPermission_SC_caveat(e);
+  let res : PTE_Check =
+    match res {
+      PTE_Check_Failure(_, _) => res,
+      PTE_Check_Success(ext_ptw) => match ac {
+        Execute()          => res,
+        Read(_)            => res,
+        Write(Data)        => res,
+        ReadWrite(_, Data) => res,
+
+        ReadWrite(_, Cap ) => checkPTEPermission_SC_caveat_datadep(scav, ext_ptw),
+        Write(Cap)         => checkPTEPermission_SC_caveat_datadep(scav, ext_ptw)
+      }
+    };
+
+  /*
+   * Now do load-side caveats, which may also force a fault if data-dependent
+   */
   let lcav = checkPTEPermission_LC_caveat(p, e);
-  let (succ, ext_ptw') : (bool, ext_ptw) =
-  match (base_succ, ac) {
-    /* Base translation exceptions take priority over CHERI exceptions */
-    (false, _)                    => (false, init_ext_ptw),
-
-    (true,  Read(Cap))            => (true, ext_ptw_join_lcm(ext_ptw, lcav)),
-    (true,  Write(Cap))           => (true, ext_ptw_join_scm(ext_ptw, scav)),
-    (true,  ReadWrite(Data,Cap))  => (true, ext_ptw_join_scm(ext_ptw, scav)),
-    (true,  ReadWrite(Cap,Data))  => (true, ext_ptw_join_lcm(ext_ptw, lcav)),
-    (true,  ReadWrite(Cap,Cap))   => (true, ext_ptw_join_scm(ext_ptw_join_lcm(ext_ptw, lcav), scav)),
-
-    (true,  Read(Data))           => (true, ext_ptw),
-    (true,  Write(Data))          => (true, ext_ptw),
-    (true,  ReadWrite(Data,Data)) => (true, ext_ptw),
-    (true,  Execute())            => (true, ext_ptw)
-  };
+  let res : PTE_Check =
+    match res {
+      PTE_Check_Failure(_, _) => res,
+      PTE_Check_Success(ext_ptw) => match ac {
+        Execute()          => res,
+        Write(_)           => res,
+        Read(Data)         => res,
+        ReadWrite(Data, _) => res,
+
+        Read(Cap)          => checkPTEPermission_LC_caveat_datadep(lcav, ext_ptw),
+        ReadWrite(Cap, _)  => checkPTEPermission_LC_caveat_datadep(lcav, ext_ptw)
+      }
+    };
 
-  if succ then PTE_Check_Success(ext_ptw') else PTE_Check_Failure(ext_ptw')
+  res
 }
 
 function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {

src/cheri_ptw.sail

@@ -25,29 +25,15 @@ function ptw_error_to_str(e) =
 overload to_str = {ptw_error_to_str}
 
 /*
- * I apologize for the confusion you have experienced if you have skipped over
- * this comment and read the body of this function first.  Hopefully these two
- * points resolve most of it:
- *
- * 1) While it may look like we're signaling that we must *always* raise
- * faults, translationException below can see whether the instruction
- * triggering the PTW is claiming to store an asserted tag, and will ignore our
- * result if that isn't so.
- *
- * 2) We analyse only the store-side component of ext_ptw here.  The PTW logic
- * cannot see into the data path, and so load-side responses, including traps,
- * must be handled by the instruction that initiated the translation.
+ * checkPTEPermission has returned a failure; here, ext_ptw is no longer
+ * caveats for data dependence, but rather certainly identifies the cause of a
+ * trap.
  */
-function ext_get_ptw_error(ext_ptw : ext_ptw) -> PTW_Error =
-  match (ext_ptw.ptw_sc_mod) {
-
-    /*
-     * This is confusing: PTW_No_Permission() is never used as such, but just
-     * dodges the pattern matches in translationException, below.
-     */
-    PTW_SCM_OK   => PTW_No_Permission(),
-
-    PTW_SCM_TRAP => PTW_Ext_Error(AT_CAP_ERR)
+function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error =
+  match (eptwf) {
+    EPTWF_NO_PERM  => PTW_No_Permission(),
+    EPTWF_INVALID  => PTW_Invalid_PTE(),
+    EPTWF_CAP_ERR  => PTW_Ext_Error(AT_CAP_ERR)
   }
 
 /* conversion of these translation/PTW failures into architectural exceptions */

src/cheri_riscv_types.sail

@@ -63,6 +63,13 @@ let init_ext_ptw : ext_ptw = struct {
   ptw_sc_mod = PTW_SCM_OK
 }
 
+/* Address translation failures */
+enum ext_ptw_fail = {
+  EPTWF_NO_PERM,
+  EPTWF_INVALID,
+  EPTWF_CAP_ERR
+}
+
 /* Address translation errors */
 enum ext_ptw_error = {AT_CAP_ERR}