Introduce load-capability generation traps

Co-authored-by: Jessica Clarke <[email protected]>

Author: nwf-msr

src/cheri_insts.sail

@@ -1376,11 +1376,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
       let c = mem_read_cap(addr, aq, rl, false);
       match c {
         MemValue(v) => {
-          let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
-                   then {v with tag = false} /* strip the tag */
-                   else {v with tag = v.tag & auth_val.permit_load_cap};
-          C(cd) = cr;
-          RETIRE_SUCCESS
+          match ptw_info.ptw_lc {
+            PTW_LC_OK => {
+              C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
+              RETIRE_SUCCESS
+            },
+            PTW_LC_CLEAR => {
+              C(cd) = { v with tag = false };
+              RETIRE_SUCCESS
+            },
+            PTW_LC_TRAP  => {
+              if v.tag then {
+                handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
+                RETIRE_FAIL
+              } else {
+                C(cd) = v;
+                RETIRE_SUCCESS
+              }
+            }
+          }
         },
         MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
       }
@@ -1607,15 +1621,28 @@ if not(auth_val.tag) then {
       let c = mem_read_cap(addr, aq, rl, false);
       match c {
         MemValue(v) => {
-          let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
-                   then {v with tag = false} /* strip the tag */
-                   else {
-                     /* the Sail model currently reserves virtual addresses */
-                     load_reservation(addr);
-                     {v with tag = v.tag & auth_val.permit_load_cap}
-                   };
-          C(cd) = cr;
-          RETIRE_SUCCESS
+          match ptw_info.ptw_lc {
+            PTW_LC_OK => {
+              load_reservation(addr);
+              C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
+              RETIRE_SUCCESS
+            },
+            PTW_LC_CLEAR => {
+              load_reservation(addr);
+              C(cd) = { v with tag = false };
+              RETIRE_SUCCESS
+            },
+            PTW_LC_TRAP  => {
+              if v.tag then {
+                handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
+                RETIRE_FAIL
+              } else {
+                load_reservation(addr);
+                C(cd) = v;
+                RETIRE_SUCCESS
+              }
+            }
+          }
         },
         MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
       }

src/cheri_pte.sail

@@ -31,22 +31,39 @@ bitfield PTE_Bits : pteAttribs = {
  * state cached and then observe a CW=1 CD=1 PTE, no PTE write is necessary.
  * On the other hand, if CW=0 is observed, the store operation must trap.
  *
+ * The intended semantics for capability loads are as follows.
+ *
+ *   CR  CR_Mod CR_Gen  Action
+ *
+ *    0     0      0    Capability loads strip tags
+ *    0     1      0    Capability loads trap (on set tag)
+ *    0     X      1    [Reserved]
+ *
+ *    1     0      0    Capability loads succeed: no traps or tag clearing
+ *    1     0      1    [Reserved]
+ *    1     1      G    Capability loads trap if G mismatches sccsr.[su]gclg,
+ *                      where the compared bit is keyed off of this PTE's U.
+ *
  * SV32: There are no extension bits available, so we hard-code the result to
- * CW=1 CR=1 CD=1.
+ * CW=1 CR=1 CD=1 CR_Mod=0 CR_Gen=0
  */
 type extPte = bits(10)
 
 bitfield Ext_PTE_Bits : extPte = {
   CapWrite     : 9, /* Permit capability stores */
   CapRead      : 8, /* Permit capability loads */
   CapDirty     : 7, /* Capability Dirty flag */
+  CapRead_Mod  : 6, /* Modify capability load prohibition; see above table */
+  CapRead_Gen  : 5, /* When load-cap gens. are in use, the "local" gen. bit */
 }
 
 /*
  * CapWrite     = 1,
  * CapRead      = 1,
  * CapDirty     = 1,
- * bits 0 .. 6  = 0
+ * CapRead_Mod  = 0,
+ * CapRead_Gen  = 0,
+ * bits 0 .. 4  = 0
  */
 let default_sv32_ext_pte : extPte = 0b1110000000
 
@@ -57,7 +74,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
 
 function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
   let a = Mk_PTE_Bits(p);
-  a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
+  let e = Mk_Ext_PTE_Bits(ext);
+  a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) |
+  (e.CapRead() == 0b0 & e.CapRead_Gen() == 0b1) |
+  (e.CapRead() == 0b1 & e.CapRead_Gen() == 0b1 & e.CapRead_Mod() == 0b0)
 }
 
 union PTE_Check = {
@@ -73,6 +93,25 @@ function checkPTEPermission_SC(e, ext_ptw) = {
   else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR)
 }
 
+/*
+ * Assuming we're allowed to load from this page, modulate our cap response
+ */
+val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits, ext_ptw) -> PTE_Check effect { escape, rreg }
+function checkPTEPermission_LC(p, e, ext_ptw) =
+  match (e.CapRead(), e.CapRead_Mod(), e.CapRead_Gen()) {
+    (0b0, 0b0, 0b0)  => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_CLEAR)), /* Clear tag for "unmodified" no-LC case */
+    (0b0, 0b1, 0b0)  => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_TRAP)),  /* Trap on tag load for "modified" no-LC case */
+    (0b0, _  , 0b1)  => internal_error("Bad PTE not caught by isInvalidPTE"),
+    (0b1, 0b0, 0b0)  => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_OK)), /* Unmodified LC case: go ahead */
+    (0b1, 0b0, 0b1)  => internal_error("Bad PTE not caught by isInvalidPTE"),
+    (0b1, 0b1, lclg) => {
+      /* Compare local CLG against the pte.U-selected, not mode-selected, global CLG bit */
+      let gclg : bits(1) = if p.U() == 0b1 then sccsr.ugclg() else sccsr.sgclg();
+      let ptwl = if lclg == gclg then PTW_LC_OK else PTW_LC_TRAP;
+      PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptwl))
+    }
+  }
+
 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
@@ -123,7 +162,6 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
   };
 
   /* Load side */
-  let ptw_lc = if e.CapRead()  == 0b1 then PTW_LC_OK else PTW_LC_CLEAR;
   let res : PTE_Check = match res {
     PTE_Check_Failure(_, _) => res,
     PTE_Check_Success(ext_ptw) => match ac {
@@ -132,8 +170,8 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
       Write(_)           => res,
       ReadWrite(Data, _) => res,
 
-      Read(Cap)          => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc)),
-      ReadWrite(Cap, _)  => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc))
+      Read(Cap)          => checkPTEPermission_LC(p, e, ext_ptw),
+      ReadWrite(Cap, _)  => checkPTEPermission_LC(p, e, ext_ptw)
     }
   };
 

src/cheri_riscv_types.sail

@@ -10,7 +10,10 @@ enum ext_ptw_lc = {
   PTW_LC_OK,
 
   /* PTE settings require clearing tags */
-  PTW_LC_CLEAR
+  PTW_LC_CLEAR,
+
+  /* PTE settings require us to trap */
+  PTW_LC_TRAP
 }
 
 struct ext_ptw = {
@@ -21,7 +24,12 @@ function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw =
   { e with ptw_lc =
       match l {
         PTW_LC_OK => e.ptw_lc,
-        PTW_LC_CLEAR => l
+        PTW_LC_CLEAR => match e.ptw_lc {
+                          PTW_LC_OK    => PTW_LC_CLEAR,
+                          PTW_LC_CLEAR => PTW_LC_CLEAR,
+                          PTW_LC_TRAP  => PTW_LC_TRAP
+                        },
+        PTW_LC_TRAP => PTW_LC_TRAP
       }
   }
 

src/cheri_sys_regs.sail

@@ -3,6 +3,8 @@
 /* Capability control csr */
 
 bitfield ccsr : xlenbits = {
+  ugclg   :  3,      /* Global Cap Load Gen bit for User pages */
+  sgclg   :  2,      /* Global Cap Load Gen bit for System (not User) pages */
   d       :  1,      /* dirty  */
   e       :  0       /* enable */
 }
@@ -16,6 +18,18 @@ function legalize_ccsr(csrp : Privilege, c : ccsr, v : xlenbits) -> ccsr = {
   // write only the defined bits, leaving the other bits untouched
   let v = Mk_ccsr(v);
 
+  let c : ccsr = match csrp {
+    User => {
+      // No bits defined for uccsr
+      c
+    },
+    _    => {
+      let c = update_ugclg(c, v.ugclg());
+      let c = update_sgclg(c, v.sgclg());
+      c
+    }
+  };
+
   /* For now these bits are not really supported so hardwired to true */
   let c = update_d(c, 0b1);
   let c = update_e(c, 0b1);