Added support of Smepmp in sail Riscv

doc/Status.md

@@ -19,6 +19,8 @@ The Sail specification currently captures the following ISA features:
 
 - Physical Memory Protection (PMP)
 
+- PMP Enhancements for memory accesses and execution prevention on Machine mode (Smepmp)
+
 For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the 
 RMEM tool](https://github.com/rems-project/rmem).
 

model/riscv_csr_map.sail

@@ -132,6 +132,8 @@ mapping clause csr_name_map = 0x342  <-> "mcause"
 mapping clause csr_name_map = 0x343  <-> "mtval"
 mapping clause csr_name_map = 0x344  <-> "mip"
 /* machine protection and translation */
+mapping clause csr_name_map = 0x747  <-> "mseccfg"
+mapping clause csr_name_map = 0x757  <-> "mseccfgh"
 mapping clause csr_name_map = 0x3A0  <-> "pmpcfg0"
 mapping clause csr_name_map = 0x3A1  <-> "pmpcfg1"
 mapping clause csr_name_map = 0x3A2  <-> "pmpcfg2"

model/riscv_insts_zicsr.sail

@@ -105,6 +105,9 @@ function readCSR csr : csreg -> xlenbits = {
     (0x343,  _) => mtval,
     (0x344,  _) => mip.bits(),
 
+    (0x747,  _) => mseccfg.bits(),             // mseccfg
+    (0x757, 32) => mseccfgh,                   // mseccfgh
+
     (0x3A0,  _) => pmpReadCfgReg(0),           // pmpcfg0
     (0x3A1, 32) => pmpReadCfgReg(1),           // pmpcfg1
     (0x3A2,  _) => pmpReadCfgReg(2),           // pmpcfg2
@@ -193,6 +196,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x344,  _) => { mip = legalize_mip(mip, value); Some(mip.bits()) },
 
     // Note: Some(value) returned below is not the legalized value due to locked entries
+    (0x747,  _) => { mseccfg = mseccfgWrite(mseccfg, value); Some(mseccfg.bits()) },
+    (0x757, 32) => { Some(mseccfgh) }, // ignore writes for now
     (0x3A0,  _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) },  // pmpcfg0
     (0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) },  // pmpcfg1
     (0x3A2,  _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) },  // pmpcfg2

model/riscv_mem.sail

@@ -142,7 +142,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
 
 /* PMP checks if enabled */
 function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
-  if   (~ (plat_enable_pmp ()))
+  if   (~ ((plat_enable_pmp ()) | (haveSmepmp())))
   then checked_mem_read(t, paddr, width, aq, rl, res, meta)
   else {
     match pmpCheck(paddr, width, t, p) {
@@ -267,7 +267,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
 
 /* PMP checks if enabled */
 function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) =
-  if   (~ (plat_enable_pmp ()))
+  if   (~ ((plat_enable_pmp ()) | (haveSmepmp())))
   then checked_mem_write(wk, paddr, width, data, meta)
   else {
     match pmpCheck(paddr, width, typ, priv) {

model/riscv_pmp_control.sail

@@ -104,14 +104,41 @@ function pmpCheckRWX(ent, acc) = {
   }
 }
 
-// this needs to be called with the effective current privilege.
-val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
+/* this needs to be called with the effective current privilege */
+val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool effect {rreg}
 function pmpCheckPerms(ent, acc, priv) = {
-  match priv {
-    Machine => if   pmpLocked(ent)
-               then pmpCheckRWX(ent, acc)
-               else true,
-    _       => pmpCheckRWX(ent, acc)
+  match mseccfg.MML() {
+    0b1 =>
+      match (ent.R(), ent.W(), ent.L(), ent.X()) {
+        (0b0, 0b1, 0b1, _) =>
+          match acc {
+            Execute(_) => true,
+            Read(_)    => priv == Machine & ent.X() == 0b1,
+            _          => false
+          },
+        (0b0, 0b1, 0b0, _) =>
+          match acc {
+            Read(_)  => true,
+            Write(_) => priv == Machine | ent.X() == 0b1,
+            _        => false
+          },
+        (0b1, 0b1, 0b1, 0b1) =>
+          match acc {
+            Read(_) => true,
+            _       => false
+          },
+        (_, _, _, _) =>
+          if (priv == Machine) == pmpLockBit(ent)
+          then pmpCheckRWX(ent, acc)
+          else false
+      },
+    0b0 =>
+      match priv {
+        Machine => if pmpLockBit(ent)
+        then pmpCheckRWX(ent, acc)
+        else true,
+        _       => pmpCheckRWX(ent, acc)
+      }
   }
 }
 
@@ -217,10 +244,19 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
   match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
     PMP_Success  => true,
     PMP_Fail     => false,
-    PMP_Continue => match priv {
-                      Machine => true,
-                      _       => false
-                    }
+    PMP_Continue =>
+      match priv {
+        Machine =>
+          if mseccfg.MMWP() == 0b1 & haveSmepmp()                /* Make Read, Write and execute denied by default, if condition meets for M mode */
+          then false
+          else if mseccfg.MML() == 0b1 & haveSmepmp()            /* Make execute denied, if condition meets for M mode */
+          then match acc {
+                 Execute(_) => false,
+                 _          => true
+               }
+          else true,
+        _       => false                                         /* Make Read, Write and execute denied by default for S/U mode */
+      }
   }}}}}}}}}}}}}}}};
 
   if   check
@@ -234,6 +270,10 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
 }
 
 function init_pmp() -> unit = {
+  mseccfg->RLB() = 0b0;
+  mseccfg->MML() = 0b0;
+  mseccfg->MMWP() = 0b0;
+  mseccfgh = EXTZ(0b0);
   pmp0cfg  = update_A(pmp0cfg,  pmpAddrMatchType_to_bits(OFF));
   pmp1cfg  = update_A(pmp1cfg,  pmpAddrMatchType_to_bits(OFF));
   pmp2cfg  = update_A(pmp2cfg,  pmpAddrMatchType_to_bits(OFF));

model/riscv_pmp_regs.sail

@@ -66,6 +66,9 @@
 /*  SUCH DAMAGE.                                                                         */
 /*=======================================================================================*/
 
+function haveSmepmp() -> bool =
+  return false
+
 /* PMP configuration entries */
 
 enum PmpAddrMatchType = {OFF, TOR, NA4, NAPOT}
@@ -100,6 +103,15 @@ bitfield Pmpcfg_ent : bits(8) = {
   R : 0         /* read */
 }
 
+bitfield Mseccfg_ent : xlenbits = {
+  RLB : 2,        /* Rule Locking Bypass */
+  MMWP : 1,       /* Machine Mode Whitelist Policy */
+  MML : 0         /* Machine Mode Lockdown */
+}
+
+register mseccfg  : Mseccfg_ent
+register mseccfgh : bits(32)
+
 register pmp0cfg  : Pmpcfg_ent
 register pmp1cfg  : Pmpcfg_ent
 register pmp2cfg  : Pmpcfg_ent
@@ -154,15 +166,42 @@ function pmpReadCfgReg(n) = {
 }
 
 /* Helpers to handle locked entries */
-function pmpLocked(cfg: Pmpcfg_ent) -> bool =
-   cfg.L() == 0b1
+function pmpLockBit(cfg: Pmpcfg_ent) -> bool = cfg.L() == 0b1
 
-function pmpTORLocked(cfg: Pmpcfg_ent) -> bool =
-   (cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)
+function pmpLocked(cfg: Pmpcfg_ent) -> bool = (cfg.L() == 0b1) & (mseccfg.RLB() == 0b0)
 
-function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
-  if pmpLocked(cfg) then cfg
-  else Mk_Pmpcfg_ent(v & 0x9f)  // Bits 5 and 6 are zero.
+function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = (cfg.L() == 0b1) & (mseccfg.RLB() == 0b0) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)
+
+function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = {
+  let legal_v : Pmpcfg_ent = Mk_Pmpcfg_ent(v & 0x9f);                    /* Constructing legal Pmpcfg_ent by making bit 5 and 6 zero */
+  let legal_v : Pmpcfg_ent = match haveSmepmp() {
+    true  =>
+      match (mseccfg.MML(), legal_v.R(), legal_v.W()) {
+        (0b0, 0b0, 0b1) => update_W(legal_v, 0b0),
+        (_, _, _)       => legal_v
+      },
+    false =>
+      match (legal_v.R(), legal_v.W()) {
+        (0b0, 0b1) => update_W(legal_v, 0b0),
+        (_, _)     => legal_v
+      }
+  };
+  if ((pmpLockBit(cfg) & ~(haveSmepmp())) | (pmpLocked(cfg) & haveSmepmp()))
+  then cfg                                                               /* If locked then configuration is unchanged */
+  else if (mseccfg.MML() == 0b1 & mseccfg.RLB() == 0b0 & legal_v.L() == 0b1)
+  then {
+    match haveSmepmp() {
+      true  => match (legal_v.R(), legal_v.W(), legal_v.X()) {
+                 (0b0, 0b0, 0b1) => cfg,
+                 (0b0, 0b1, 0b0) => cfg,
+                 (0b0, 0b1, 0b1) => cfg,
+                 (0b1, 0b0, 0b1) => cfg,
+                 (_, _, _)       => legal_v
+               },
+      false => legal_v
+    };
+  } else legal_v
+}
 
 val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
 function pmpWriteCfgReg(n, v) = {
@@ -216,3 +255,24 @@ function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits
   if   sizeof(xlen) == 32
   then { if (locked | tor_locked) then reg else v }
   else { if (locked | tor_locked) then reg else EXTZ(v[53..0]) }
+
+function mseccfgWrite(reg: Mseccfg_ent, v: xlenbits) -> Mseccfg_ent = {
+  let legal_v : Mseccfg_ent = Mk_Mseccfg_ent(EXTZ(v[2 .. 0]));
+  let reg : Mseccfg_ent = match (reg.RLB(), legal_v.RLB()) {                   /* to set RLB, need to check PMPCFG_L */
+    (0b0, 0b1) =>
+      if (pmp0cfg.L() == 0b1 | pmp1cfg.L() == 0b1 | pmp2cfg.L() == 0b1 | pmp3cfg.L() == 0b1
+         | pmp4cfg.L() == 0b1 | pmp5cfg.L() == 0b1 | pmp6cfg.L() == 0b1 | pmp7cfg.L() == 0b1
+         | pmp8cfg.L() == 0b1 | pmp9cfg.L() == 0b1 | pmp10cfg.L() == 0b1 | pmp11cfg.L() == 0b1
+         | pmp12cfg.L() == 0b1 | pmp13cfg.L() == 0b1 | pmp14cfg.L() == 0b1 | pmp15cfg.L() == 0b1)
+      then reg
+      else update_RLB(reg, legal_v.RLB()),
+    (_, _) => reg
+  };
+  let reg : Mseccfg_ent = match (reg.MML(), reg.MMWP()) {                      /* Implements stickiness of MML bit, if once set remains set */
+    (0b0, 0b0) => update_MML(update_MMWP(reg, legal_v.MMWP()), legal_v.MML()),
+    (0b0, 0b1) => update_MML(reg, legal_v.MML()),
+    (0b1, 0b0) => update_MMWP(reg, legal_v.MMWP()),
+    (0b1, 0b1) => reg
+  };
+  reg
+}

model/riscv_sys_control.sail

@@ -98,6 +98,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x343 => p == Machine, // mtval
     0x344 => p == Machine, // mip
 
+    0x747 => p == Machine, // mseccfg
+    0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh
+
     0x3A0 => p == Machine,                        // pmpcfg0
     0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1
     0x3A2 => p == Machine,                        // pmpcfg2