Revocation 3.0 PTE bits

Makefile

@@ -12,15 +12,13 @@ SAIL_RISCV_MODEL_DIR=$(SAIL_RISCV_DIR)/model
 SAIL_CHERI_MODEL_DIR=src
 
 SAIL_RV32_XLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_xlen32.sail
-SAIL_RV32_FLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_flen_F.sail
 CHERI_CAP_RV32_IMPL := cheri_prelude_64.sail
 
 SAIL_RV64_XLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_xlen64.sail
-SAIL_RV64_FLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail
 CHERI_CAP_RV64_IMPL := cheri_prelude_128.sail
 
 SAIL_XLEN = $(SAIL_$(ARCH)_XLEN)
-SAIL_FLEN = $(SAIL_$(ARCH)_FLEN)
+SAIL_FLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail
 CHERI_CAP_IMPL = $(CHERI_CAP_$(ARCH)_IMPL)
 
 
@@ -191,7 +189,7 @@ GMP_LIBS := $(shell pkg-config --libs gmp || echo -lgmp)
 ZLIB_FLAGS = $(shell pkg-config --cflags zlib)
 ZLIB_LIBS = $(shell pkg-config --libs zlib)
 
-C_FLAGS = -I $(SAIL_LIB_DIR) -I $(SAIL_RISCV_DIR)/c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS)
+C_FLAGS = -I $(SAIL_LIB_DIR) -I $(SAIL_RISCV_DIR)/c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS) -fcommon
 C_LIBS  = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS)
 
 ifneq (,$(SAILCOV))

src/cheri_addr_checks.sail

@@ -212,6 +212,12 @@ function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = {
   handle_cheri_cap_exception(capEx, regnum)
 }
 
+/* Default implementations of these hooks permit all accesses.  */
+function ext_check_phys_mem_read (access_type, paddr, size, aquire, release, reserved, read_meta) =
+  Ext_PhysAddr_OK()
+
+function ext_check_phys_mem_write(write_kind, paddr, size, data, metadata) =
+  Ext_PhysAddr_OK()
 
 /* Is XRET from given mode permitted by extension? */
 function ext_check_xret_priv (p : Privilege) : Privilege -> bool =

src/cheri_insts.sail

@@ -1498,11 +1498,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
       let c = mem_read_cap(addr, aq, 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 }
       }
@@ -1727,15 +1741,28 @@ if not(auth_val.tag) then {
       let c = mem_read_cap(addr, aq, 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

@@ -78,23 +78,57 @@ bitfield PTE_Bits : pteAttribs = {
 /*
  * Reserved PTE bits used by extensions on RV64.
  *
- * There are no such bits on RV32/SV32, so we hard-code both CapWrite=1
- * and CapRead=1 (i.e., there is no ability to disable capability loads
- * from or stores to pages in the SV32 MMU).
+ * For capability store the behaviors are as follows.
+ *
+ *   CW  CD  Action
+ *
+ *    0   X    Trap on tagged capability store
+ *    1   0    CAS the PTE to CW=1, CD=1 (i.e., set both bits) or trap
+ *    1   1    Permit tagged capability store
+ *
+ * The CW/CD pair is akin to Sv{32,48,...}'s W/D bits.
+ *
+ * The CW=1 CD=0 behavior is described as a CAS (and not an AMO OR) of the PTE
+ * to close race conditions, much as with W and D.  Should the TLB have this
+ * 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  CRT CRG 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 [ms]ccsr.[su]gclg, where
+ *                   the compared bit is keyed off of this PTE's U.  sccsr is
+ *                   used if the machine has Supervisor mode, otherwise mccsr.
+ *
+ * Sv32: There are no extension bits available, so we hard-code the result to
+ * CW=1 CR=1 CD=1 CRT=0 CRG=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 */
+  CapReadTrap : 6, /* Trap on capability loads; see above table */
+  CapReadGen  : 5, /* When load-cap gens. are in use, the "local" gen. bit */
 }
 
 /*
- * CapWrite     = 1,
- * CapRead      = 1,
- * bits 0 .. 7  = 0
+ * CapWrite    = 1,
+ * CapRead     = 1,
+ * CapDirty    = 1,
+ * CapReadTrap = 0,
+ * CapReadGen  = 0,
+ * bits 0 .. 4 = 0
  */
-let default_sv32_ext_pte : extPte = 0b1100000000
+let default_sv32_ext_pte : extPte = 0b1110000000
 
 function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
   let a = Mk_PTE_Bits(p);
@@ -103,14 +137,45 @@ 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.CapReadGen() == 0b1) |
+  (e.CapRead() == 0b1 & e.CapReadGen() == 0b1 & e.CapReadTrap() == 0b0)
 }
 
 union PTE_Check = {
   PTE_Check_Success : ext_ptw,
   PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
 }
 
+/* Gate Cap-transporting stores on the CapWrite PTE bit */
+val checkPTEPermission_SC : (Ext_PTE_Bits, ext_ptw) -> PTE_Check
+function checkPTEPermission_SC(e, ext_ptw) = {
+  if   e.CapWrite() == 0b1
+  then PTE_Check_Success(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.CapReadTrap(), e.CapReadGen()) {
+    (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 ccsr = if haveSupMode() then sccsr else mccsr;
+      let gclg : bits(1) = if p.U() == 0b1 then ccsr.ugclg() else ccsr.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
@@ -124,7 +189,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,
@@ -139,29 +204,42 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (_,            Machine)    => internal_error("m-mode mem perm check")
   };
 
+  let res =
+    if   succ
+    then PTE_Check_Success(ext_ptw)
+    else PTE_Check_Failure(ext_ptw, EPTWF_NO_PERM);
+
   let e = Mk_Ext_PTE_Bits(ext);
-  let ptw_lc = if e.CapRead()  == 0b1 then PTW_LC_OK else PTW_LC_CLEAR;
-  let ptw_sc = if e.CapWrite() == 0b1 then PTW_SC_OK else PTW_SC_TRAP;
-  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_lc_join(ext_ptw, ptw_lc)),
-    (true,  Write(Cap))            => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)),
-    (true,  ReadWrite(Data, Cap))  => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)),
-    (true,  ReadWrite(Cap, Data))  => (true, ext_ptw_lc_join(ext_ptw, ptw_lc)),
-    (true,  ReadWrite(Cap, Cap))   => (true, ext_ptw_sc_join(ext_ptw_lc_join(ext_ptw, ptw_lc), ptw_sc)),
-
-    (true,  Read(Data))            => (true, ext_ptw),
-    (true,  Write(Data))           => (true, ext_ptw),
-    (true,  ReadWrite(Data, Data)) => (true, ext_ptw),
-    (true,  Execute())             => (true, ext_ptw)
+
+  /* Store side */
+  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,
+
+      Write(Cap)         => checkPTEPermission_SC(e, ext_ptw),
+      ReadWrite(_, Cap)  => checkPTEPermission_SC(e, ext_ptw)
+    }
   };
 
-  if succ
-  then PTE_Check_Success(ext_ptw')
-  else PTE_Check_Failure(ext_ptw', if ext_ptw'.ptw_sc == PTW_SC_TRAP then EPTWF_CAP_ERR else EPTWF_NO_PERM)
+  /* Load side */
+  let res : PTE_Check = match res {
+    PTE_Check_Failure(_, _) => res,
+    PTE_Check_Success(ext_ptw) => match ac {
+      Execute()          => res,
+      Read(Data)         => res,
+      Write(_)           => res,
+      ReadWrite(Data, _) => res,
+
+      Read(Cap)          => checkPTEPermission_LC(p, e, ext_ptw),
+      ReadWrite(Cap, _)  => checkPTEPermission_LC(p, e, ext_ptw)
+    }
+  };
+
+  res
 }
 
 function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {
@@ -176,9 +254,24 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex
   // accessed bit
   let update_a = p.A() == 0b0;
 
-  if update_d | update_a then {
+  let pte_ext = Mk_Ext_PTE_Bits(ext);
+
+  // store cap bits
+  let update_cd = pte_ext.CapWrite() == 0b1 &
+                  pte_ext.CapDirty() == 0b0 &
+                  (match a {
+                    Execute()          => false,
+                    Read(_)            => false,
+                    Write(Cap)         => true,
+                    Write(Data)        => false,
+                    ReadWrite(_, Cap)  => true,
+                    ReadWrite(_, Data) => false
+                  });
+
+  if update_d | update_a | update_cd then {
     let np = update_A(p, 0b1);
     let np = if update_d then update_D(np, 0b1) else np;
-    Some(np, ext)
+    let npte_ext = if update_cd then update_CapDirty(pte_ext, 0b1) else pte_ext;
+    Some(np, npte_ext.bits())
   } else None()
 }

src/cheri_riscv_types.sail

@@ -72,42 +72,32 @@ enum ext_ptw_lc = {
   PTW_LC_OK,
 
   /* PTE settings require clearing tags */
-  PTW_LC_CLEAR
-}
-
-enum ext_ptw_sc = {
-  /* Tag stores are permitted */
-  PTW_SC_OK,
+  PTW_LC_CLEAR,
 
-  /* Tag-asserting stores trap */
-  PTW_SC_TRAP
+  /* PTE settings require us to trap */
+  PTW_LC_TRAP
 }
 
 struct ext_ptw = {
-  ptw_lc : ext_ptw_lc,
-  ptw_sc : ext_ptw_sc
+  ptw_lc : ext_ptw_lc
 }
 
 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
-      }
-  }
-
-function ext_ptw_sc_join(e : ext_ptw, s : ext_ptw_sc) -> ext_ptw =
-  { e with ptw_sc =
-      match s {
-        PTW_SC_OK => e.ptw_sc,
-        PTW_SC_TRAP => s
+        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
       }
   }
 
 /* initial value of the PTW accumulator */
 let init_ext_ptw : ext_ptw = struct {
-  ptw_lc = PTW_LC_OK,
-  ptw_sc = PTW_SC_OK
+  ptw_lc = PTW_LC_OK
 }
 
 /* Address translation failures */