Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added support of Smepmp in Sail RISCV #196

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Added support of Smepmp in Sail RISCV #196

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions doc/Status.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).

Expand Down
2 changes: 2 additions & 0 deletions model/riscv_csr_map.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,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"
Expand Down
5 changes: 5 additions & 0 deletions model/riscv_insts_zicsr.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,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
Expand Down Expand Up @@ -195,6 +198,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
Expand Down
63 changes: 52 additions & 11 deletions model/riscv_pmp_control.sail
View file
Open in desktop
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For this file, we needed the following change:

diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 7cca3ba..ce3b1b0 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -139,6 +139,8 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType =
 
 function pmpCheck forall 'n, 'n > 0. (addr: int, width: int('n), acc: AccessType(ext_access_type), priv: Privilege)
                   -> option(ExceptionType) = {
+  if sys_pmp_count() == 0 then return None();
+
   foreach (i from 0 to 3) {
     let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros());
     match pmpMatchEntry(addr, width, acc, priv, pmpcfg_n[i], pmpReadAddrReg(i), prev_pmpaddr) {

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm I think this is handled in phys_access_check() but maybe it makes more sense here.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, then I should probably be using that function in my work as well. Thanks! This can thus be marked as resolved with relation to this PR.

Original file line number Diff line number Diff line change
Expand Up @@ -106,14 +106,42 @@ 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.L(), ent.R(), ent.W(), ent.X()) {
(0b1, 0b0, 0b1, _) =>
match acc {
Execute(_) => true,
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
Read(_) => priv == Machine & ent.X() == 0b1,
_ => false
},
(0b0, 0b0, 0b1, _) =>
match acc {
Read(_) => true,
Write(_) => priv == Machine | ent.X() == 0b1,
_ => false
},
(0b1, 0b1, 0b1, 0b1) =>
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
match acc {
Read(_) => true,
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
_ => false
},
(_, _, _, _) =>
if (priv == Machine) == pmpLockBit(ent)
then pmpCheckRWX(ent, acc)
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
else false
},
0b0 =>
match priv {
Machine =>
if pmpLockBit(ent)
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
then pmpCheckRWX(ent, acc)
else true,
_ => pmpCheckRWX(ent, acc)
}
}
}

Expand Down Expand Up @@ -219,10 +247,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 /* Make Read, Write and execute denied by default, if condition meets for M mode */
then false
else if mseccfg.MML() == 0b1 /* 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
Expand All @@ -236,6 +273,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 = zero_extend(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));
Expand Down
63 changes: 56 additions & 7 deletions model/riscv_pmp_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,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
Expand Down Expand Up @@ -158,15 +167,34 @@ 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
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved

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 = pmpLocked(cfg) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)

function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = {
/* Constructing legal Pmpcfg_ent by making bit 5 and 6 zero */
let legal_v : Pmpcfg_ent = Mk_Pmpcfg_ent(v & 0x9f);
let legal_v : Pmpcfg_ent = match (mseccfg.MML(), legal_v.R(), legal_v.W()) {
(0b0, 0b0, 0b1) => update_W(legal_v, 0b0),
(_, _, _) => legal_v
};
/* If locked then configuration is unchanged */
if pmpLocked(cfg)
then cfg
/* To prevent adding a rule with execution privileges if MML is enabled unless RLB is set */
else if (mseccfg.MML() == 0b1 & mseccfg.RLB() == 0b0 & legal_v.L() == 0b1)
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
then {
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
}
} else legal_v
}

val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
function pmpWriteCfgReg(n, v) = {
Expand Down Expand Up @@ -222,3 +250,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 zero_extend(v[53..0]) }

function mseccfgWrite(reg: Mseccfg_ent, v: xlenbits) -> Mseccfg_ent = {
let legal_v : Mseccfg_ent = Mk_Mseccfg_ent(zero_extend(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)
HamzaKh01 marked this conversation as resolved.
Show resolved Hide resolved
then reg
else update_RLB(reg, legal_v.RLB()),
(_, _) => update_RLB(reg, legal_v.RLB())
};
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
}
3 changes: 3 additions & 0 deletions model/riscv_sys_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,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

Comment on lines +103 to +105
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We recently used this code and needed to make the following change so that mseccfg does not exist when PMP is disabled:

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index c3ac1fe..e5a8cf7 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -50,8 +50,8 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x3D @ idx : bits(4) => p == Machine & sys_pmp_max_count() > unsigned(0b10 @ idx),
     0x3E @ idx : bits(4) => p == Machine & sys_pmp_max_count() > unsigned(0b11 @ idx),
 
-    0x747 => p == Machine, // mseccfg
-    0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh
+    0x747 => p == Machine & sys_pmp_count() > 0, // mseccfg
+    0x757 => p == Machine & (sizeof(xlen) == 32) & sys_pmp_count() > 0, // mseccfgh
 
     0xB00 => p == Machine, // mcycle
     0xB02 => p == Machine, // minstret

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think that is strictly correct. You can have mseccfg without PMPs. Really we need a sys_has_mseccfg() flag or something like that, because it is optional. (As far as I remember anyway.)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you're right. Either way this code needs to be altered before we can merge.

0x3A0 => p == Machine, // pmpcfg0
0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1
0x3A2 => p == Machine, // pmpcfg2
Expand Down