diff --git a/doc/Status.md b/doc/Status.md index 539020a0a..a4d0db0ea 100644 --- a/doc/Status.md +++ b/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). diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 31872d3f1..d47ce8d12 100644 --- a/model/riscv_csr_map.sail +++ b/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" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 518396f91..fe88eec70 100644 --- a/model/riscv_insts_zicsr.sail +++ b/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 diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0ec855522..1236075bb 100644 --- a/model/riscv_mem.sail +++ b/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) { diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 669725b5b..9fdeecc41 100644 --- a/model/riscv_pmp_control.sail +++ b/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)); diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index a5e21edf5..3e734a8ed 100644 --- a/model/riscv_pmp_regs.sail +++ b/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 +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6204ae59e..5e118ef4b 100644 --- a/model/riscv_sys_control.sail +++ b/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