Skip to content

Commit

Permalink
Remove incorrect privilege assert
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
PeterRugg authored Sep 13, 2024
1 parent 31f8093 commit c61351e
Showing 1 changed file with 16 additions and 8 deletions.
24 changes: 16 additions & 8 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -277,21 +277,29 @@ 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) {
None() => None(),
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()
}
}
}

Expand Down

0 comments on commit c61351e

Please sign in to comment.