Introduce capability load generation traps

nwf · nwf · commit d14889fcef2c · 2020-05-15T15:30:04.000+01:00
diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail
@@ -882,6 +882,17 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =
   handle_load_data_via_cap(rd, 0b0 @ cs, cap_val, vaddr, is_unsigned, width)
 }
 
+val handle_load_cap_ptw_ext : (Capability, bool, ext_ptw) -> option(Capability)
+function handle_load_cap_ptw_ext (v, vialc, ptw_info) =
+  if v.tag == false
+  then Some(v)
+  else match ptw_info {
+         PTW_CAP_OK => Some({v with tag = v.tag & vialc}),
+         PTW_LOAD_CAP_CLR => Some({v with tag = false}),
+         PTW_LOAD_CAP_TRAP => None(),
+         PTW_STORE_CAP_ERR => internal_error("PTW store fault on load path")
+       }
+
 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(rd, cs, cap_val, vaddrBits) = {
   let aq : bool = false;
@@ -908,11 +919,10 @@ function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
       let c = mem_read_cap(addr, aq, rl, false);
       match c {
         MemValue(v) => {
-          let cr = if ptw_info == PTW_LOAD_CAP_ERR
-                   then {v with tag = false} /* strip the tag */
-                   else {v with tag = v.tag & cap_val.permit_load_cap};
-          writeCapReg(rd, cr);
-          RETIRE_SUCCESS
+          match handle_load_cap_ptw_ext(v, cap_val.permit_load_cap, ptw_info) {
+            Some(v') => { writeCapReg(rd, v'); RETIRE_SUCCESS },
+            None() => { handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL }
+          }
         },
         MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
       }
@@ -1006,15 +1016,10 @@ if not(cap_val.tag) then {
       let c = mem_read_cap(addr, aq, rl, false);
       match c {
         MemValue(v) => {
-          let cr = if   ptw_info == PTW_LOAD_CAP_ERR
-                   then {v with tag = false} /* strip the tag */
-                   else {
-                     /* the Sail model currently reserves virtual addresses */
-                     load_reservation(addr);
-                     {v with tag = v.tag & cap_val.permit_load_cap}
-                   };
-          writeCapReg(cd, cr);
-          RETIRE_SUCCESS
+          match handle_load_cap_ptw_ext(v, cap_val.permit_load_cap, ptw_info) {
+            Some(v') => { load_reservation(addr); writeCapReg(cd, v'); RETIRE_SUCCESS },
+            None() => { handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL }
+          }
         },
         MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
       }
diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail
@@ -15,12 +15,29 @@ bitfield PTE_Bits : pteAttribs = {
 
 /* Reserved PTE bits could be used by extensions on RV64.  There are
  * no such available bits on RV32, so these bits will be zeros on RV32.
+ *
+ * XXX Because these bits are 0 on RV32, do we want to use inverted polarity,
+ * so that 0 is the *enabled* form?
+ *
+ * The intended semantics for LoadCap* are:
+ *
+ *   LC  LC_Mod  LC_CLG  Action
+ *    0     0       0    Capability loads always strip tags
+ *    0   [other values] [Reserved]
+ *
+ *    1     0       0    Capability loads always succeed without tag stripping
+ *    1     0       1    Capability loads always trap
+ *    1     1       G    Capability loads trap if G mismatches sccsr.gclg[su],
+ *                         where the compared bit is keyed off of this PTE's U.
+ *
  */
 type extPte = bits(10)
 
 bitfield Ext_PTE_Bits : extPte = {
   LoadCap  : 9,
   StoreCap : 8,
+  LoadCap_Mod : 7,
+  LoadCap_CLG : 6,
 }
 
 function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
@@ -41,6 +58,26 @@ union PTE_Check = {
 function to_pte_check(b : bool) -> (bool, pte_check) =
   (b, PTE_CAP_OK)
 
+/*
+ * Assuming we're allowed to load from this page, modulate our cap response
+ */
+val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits) -> pte_check effect {rreg}
+function checkPTEPermission_LC(p, e) =
+  if e.LoadCap() == 0b0
+  then PTE_LOAD_CAP_CLR
+  else if e.LoadCap_Mod() == 0b0
+       then { /* With LoadCap_Mod off, CLG modulates the behavior directly */
+              if e.LoadCap_CLG() == 0b0
+              then PTE_CAP_OK
+              else PTE_LOAD_CAP_TRAP
+            }
+       else { /* With LoadCap_Mod on, use CLG as such */
+              let gclg : bits(1) = if p.U() == 0b1 then sccsr.gclgu() else sccsr.gclgs();
+              if e.LoadCap_CLG() == gclg
+              then PTE_CAP_OK
+              else PTE_LOAD_CAP_TRAP
+            }
+
 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 = {
   let (succ, pte_chk) : (bool, pte_check) =
   match (ac, priv) {
@@ -58,12 +95,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
                                        if   p.U() == 0b1 & p.R() == 0b1
                                        then {
                                          let  e = Mk_Ext_PTE_Bits(ext);
-                                         if   e.LoadCap() == 0b1
-                                         then (true, PTE_CAP_OK)
-                                         else {
-                                           /* Allow the address translation to proceed, but mark for tag stripping */
-                                           (true, PTE_LOAD_CAP_ERR)
-                                         }
+                                         (true, checkPTEPermission_LC(p, e))
                                        }
                                        else (false, PTE_CAP_OK)
                                      },
@@ -84,23 +116,22 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (ReadWrite(Cap),  User)       => { if   p.U() == 0b1 & p.R() == 0b1 & p.W() == 0b1
                                        then {
                                          let  e = Mk_Ext_PTE_Bits(ext);
-                                         if   e.StoreCap() == 0b1 & e.LoadCap() == 0b1
+                                         let  lcm = checkPTEPermission_LC(p, e);
+                                         if   e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
                                          then (true, PTE_CAP_OK)
                                          else if e.StoreCap() == 0b0
                                          /* return a failure since we should cause an exception */
                                          then (false, PTE_STORE_CAP_ERR)
                                          /* return a success since the translation should proceed */
-                                         else (true, PTE_LOAD_CAP_ERR)
+                                         else (true, lcm)
                                        }
                                        else (false, PTE_CAP_OK)
                                      },
 
     (Read(Cap),       Supervisor) => { if   (p.U() == 0b0 | do_sum) & p.R() == 0b1
                                        then {
                                          let  e = Mk_Ext_PTE_Bits(ext);
-                                         if   e.LoadCap() == 0b1
-                                         then (true, PTE_CAP_OK)
-                                         else (true, PTE_LOAD_CAP_ERR)
+                                         (true, checkPTEPermission_LC(p, e))
                                        }
                                        else (false, PTE_CAP_OK)
                                      },
@@ -118,13 +149,14 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (ReadWrite(Cap),  Supervisor) => { let e = Mk_Ext_PTE_Bits(ext);
                                        if   (p.U() == 0b0 | do_sum) & p.R() == 0b1 & p.W() == 0b1
                                        then {
-                                         if   e.StoreCap() == 0b1 & e.LoadCap() == 0b1
+                                         let  lcm = checkPTEPermission_LC(p, e);
+                                         if   e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
                                          then (true, PTE_CAP_OK)
                                          else if e.StoreCap() == 0b0
                                          /* return a failure since we should cause an exception */
                                          then (false, PTE_STORE_CAP_ERR)
                                          /* return a success since the translation should proceed */
-                                         else (true, PTE_LOAD_CAP_ERR)
+                                         else (true, lcm)
                                        }
                                        else (false, PTE_CAP_OK)
                                      },
diff --git a/src/cheri_riscv_types.sail b/src/cheri_riscv_types.sail
@@ -1,26 +1,44 @@
 /* Extension for CHERI PTE checks */
-enum pte_check = {PTE_CAP_OK, PTE_LOAD_CAP_ERR, PTE_STORE_CAP_ERR}
+enum pte_check = {
+  PTE_CAP_OK,
+  PTE_LOAD_CAP_TRAP,
+  PTE_LOAD_CAP_CLR,
+  PTE_STORE_CAP_ERR
+}
 
 /* Extension for CHERI page-table-walks */
 
-enum ext_ptw = {PTW_CAP_OK, PTW_LOAD_CAP_ERR, PTW_STORE_CAP_ERR}
+enum ext_ptw = {
+  PTW_CAP_OK,
+  PTW_LOAD_CAP_TRAP,
+  PTW_LOAD_CAP_CLR,
+  PTW_STORE_CAP_ERR
+}
 
 let init_ext_ptw : ext_ptw = PTW_CAP_OK /* initial value of the PTW accumulator */
 
 /* Default accumulation of PTE check extensions into PTW accumulator */
 function ext_accum_ptw_result(ptw : ext_ptw, pte : pte_check) -> ext_ptw =
   match (ptw, pte) {
-    (PTW_CAP_OK, PTE_CAP_OK)        => PTW_CAP_OK,
-    (PTW_CAP_OK, PTE_LOAD_CAP_ERR)  => PTW_LOAD_CAP_ERR,
-    (PTW_CAP_OK, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
+    (PTW_CAP_OK, PTE_CAP_OK)               => PTW_CAP_OK,
+    (PTW_CAP_OK, PTE_LOAD_CAP_TRAP)        => PTW_LOAD_CAP_TRAP,
+    (PTW_CAP_OK, PTE_LOAD_CAP_CLR)         => PTW_LOAD_CAP_CLR,
+    (PTW_CAP_OK, PTE_STORE_CAP_ERR)        => PTW_STORE_CAP_ERR,
+
+    /*
+     * CHECK ME: The below prioritizes store exceptions over load modifiers,
+     * and prefers load traps from permission to load traps from CLG to load
+     * clearing.
+     */
 
-    /* CHECK ME: The below prioritizes store exceptions over load tag stripping. */
+    (PTW_LOAD_CAP_CLR, PTE_STORE_CAP_ERR)  => PTW_STORE_CAP_ERR,
+    (PTW_LOAD_CAP_CLR, PTE_STORE_CAP_TRAP) => PTW_LOAD_CAP_TRAP,
+    (PTW_LOAD_CAP_CLR, _)                  => PTW_LOAD_CAP_CLR,
 
-    (PTW_LOAD_CAP_ERR, PTE_CAP_OK)        => PTW_LOAD_CAP_ERR,
-    (PTW_LOAD_CAP_ERR, PTE_LOAD_CAP_ERR)  => PTW_LOAD_CAP_ERR,
-    (PTW_LOAD_CAP_ERR, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
+    (PTW_LOAD_CAP_TRAP, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
+    (PTW_LOAD_CAP_TRAP, _)                 => PTW_LOAD_CAP_TRAP,
 
-    (PTW_STORE_CAP_ERR, _ )               => PTW_STORE_CAP_ERR
+    (PTW_STORE_CAP_ERR, _ )                => PTW_STORE_CAP_ERR
   }
 
 /* Address translation errors */
diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail
@@ -5,6 +5,8 @@
 bitfield ccsr : xlenbits = {
   cap_idx : 15 .. 10,
   cause   :  9 .. 5, /* cap cause */
+  gclgu   :  3,
+  gclgs   :  2,
   d       :  1,      /* dirty  */
   e       :  0       /* enable */
 }
diff --git a/src/cheri_types.sail b/src/cheri_types.sail
@@ -79,7 +79,8 @@ enum CapEx = {
   CapEx_PermitCCallViolation,
   CapEx_AccessCCallIDCViolation,
   CapEx_PermitUnsealViolation,
-  CapEx_PermitSetCIDViolation
+  CapEx_PermitSetCIDViolation,
+  CapEx_CapLoadGen
 }
 
 function CapExCode(ex) : CapEx -> bits(5) =
@@ -108,7 +109,8 @@ function CapExCode(ex) : CapEx -> bits(5) =
     CapEx_PermitCCallViolation          => 0b11001,
     CapEx_AccessCCallIDCViolation       => 0b11010,
     CapEx_PermitUnsealViolation         => 0b11011,
-    CapEx_PermitSetCIDViolation         => 0b11100
+    CapEx_PermitSetCIDViolation         => 0b11100,
+    CapEx_CapLoadGen                    => 0b11101
   }
 
 function string_of_capex (ex) : CapEx -> string =
@@ -137,7 +139,8 @@ function string_of_capex (ex) : CapEx -> string =
     CapEx_PermitCCallViolation          => "PermitCCallViolation"        ,
     CapEx_AccessCCallIDCViolation       => "AccessCCallIDCViolation"     ,
     CapEx_PermitUnsealViolation         => "PermitUnsealViolation"       ,
-    CapEx_PermitSetCIDViolation         => "PermitSetCIDViolation"
+    CapEx_PermitSetCIDViolation         => "PermitSetCIDViolation"       ,
+    CapEx_CapLoadGen                    => "CapLoadGen"
   }
 
 type capreg_idx = bits(6)

Original file line number	Diff line number	Diff line change
`@@ -5,6 +5,8 @@`
`5`	`5`	`bitfield ccsr : xlenbits = {`
`6`	`6`	`cap_idx : 15 .. 10,`
`7`	`7`	`cause : 9 .. 5, /* cap cause */`
	`8`	`+ gclgu : 3,`
	`9`	`+ gclgs : 2,`
`8`	`10`	`d : 1, /* dirty */`
`9`	`11`	`e : 0 /* enable */`
`10`	`12`	`}`