From c61351e16e803d5ae8c14781d13a4bf214eb51d7 Mon Sep 17 00:00:00 2001
From: PeterRugg <pdr32@cam.ac.uk>
Date: Fri, 13 Sep 2024 19:38:15 +0100
Subject: [PATCH] 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.
---
 model/riscv_sys_control.sail | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index f8ec00ac8..da04278b7 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()
+    }
   }
 }