diff options
author | PeterRugg <pdr32@cam.ac.uk> | 2024-09-13 19:38:15 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2024-09-13 19:38:15 +0100 |
commit | c61351e16e803d5ae8c14781d13a4bf214eb51d7 (patch) | |
tree | 396e91a05bff075973c276a0150a90b49391b63f | |
parent | 31f809346e1020d191b46d519ad6435e2428be39 (diff) | |
download | sail-riscv-c61351e16e803d5ae8c14781d13a4bf214eb51d7.zip sail-riscv-c61351e16e803d5ae8c14781d13a4bf214eb51d7.tar.gz sail-riscv-c61351e16e803d5ae8c14781d13a4bf214eb51d7.tar.bz2 |
Remove incorrect privilege assert
The condition checks whether it's possible for a mode other than
machine mode to take interrupts, but just because it can't, that
doesn't mean we can never call this function while in another
mode.
In particular, this causes a crash if you run with S mode disabled
but U mode enabled, then mret to U mode without NExt.
-rw-r--r-- | model/riscv_sys_control.sail | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index f8ec00a..da04278 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -277,14 +277,16 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege /* If we don't have different privilege levels, we don't need to check delegation. * Absence of U-mode implies absence of S-mode. */ - if not(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S)) & not(extensionEnabled(Ext_N))) then { - assert(priv == Machine, "invalid current privilege"); - let enabled_pending = mip.bits & mie.bits; - match findPendingInterrupt(enabled_pending) { - Some(i) => let r = (i, Machine) in Some(r), - None() => None() - } - } else { + let multipleModesSupported = extensionEnabled(Ext_U); + if not(multipleModesSupported) then { + assert(priv == Machine, "invalid current privilege") + }; + /* Even with U-mode, we don't need to check delegation when M-mode is the only + one that can take interrupts, i.e. when we don't have S-mode and don't have + the N extension + */ + let delegationPossible = extensionEnabled(Ext_S) | extensionEnabled(Ext_N); + if multipleModesSupported & delegationPossible then { match getPendingSet(priv) { None() => None(), Some(ip, p) => match findPendingInterrupt(ip) { @@ -292,6 +294,12 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege Some(i) => let r = (i, p) in Some(r) } } + } else { + let enabled_pending = mip.bits & mie.bits; + match findPendingInterrupt(enabled_pending) { + Some(i) => let r = (i, Machine) in Some(r), + None() => None() + } } } |