Skip to content

Commit

Permalink
Add missing mstatus.MPP legalization
Browse files Browse the repository at this point in the history
`mstatus.MPP` legal values are User (`0b00`) (if U-mode implemented), Supervisor (`0b01`) (if S-mode implemented) and Machine (`0b11`). Encoding `0b10` is illegal.
  • Loading branch information
ved-rivos authored Jun 18, 2024
1 parent 0e9850f commit 157d4d1
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 0 deletions.
1 change: 1 addition & 0 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -501,6 +501,7 @@ function init_sys() -> unit = {
mstatus = set_mstatus_SXL(mstatus, misa[MXL]);
mstatus = set_mstatus_UXL(mstatus, misa[MXL]);
mstatus[SD] = 0b0;
mstatus[MPP] = privLevel_to_bits(lowest_supported_privLevel());

/* set to little-endian mode */
if sizeof(xlen) == 64 then {
Expand Down
19 changes: 19 additions & 0 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,21 @@ function haveZalrsc() -> bool = haveAtomics()
/* Zicond extension support */
function haveZicond() -> bool = true

/*
* Illegal values legalized to least privileged mode supported.
* Note: the only valid combinations of supported modes are M, M+U, M+S+U.
*/
function lowest_supported_privLevel() -> Privilege =
if haveUsrMode() then User else Machine

function have_privLevel(priv : priv_level) -> bool =
match priv {
0b00 => haveUsrMode(),
0b01 => haveSupMode(),
0b10 => false,
0b11 => true,
}

bitfield Mstatush : bits(32) = {
MBE : 5,
SBE : 4
Expand Down Expand Up @@ -255,6 +270,10 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
*/
let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0]));

/* Legalize MPP */
let m = [m with MPP = if have_privLevel(m[MPP]) then m[MPP]
else privLevel_to_bits(lowest_supported_privLevel())];

/* We don't have any extension context yet. */
let m = [m with XS = extStatus_to_bits(Off)];

Expand Down

0 comments on commit 157d4d1

Please sign in to comment.