Reduce code nesting in `run_hart_active` for simplicity. (#1570)HEAD2026-03-02-efdfe9bmaster

When triggers need to be handled for Sdtrig, they need to be considered
in conjunction with pending interrupts. This minor refactor reduces the
code churn to handle that case.

1 files changed, 56 insertions, 55 deletions

diff --git a/model/postlude/step.sail b/model/postlude/step.sail
index f78acfd..33d04d5 100644
--- a/model/postlude/step.sail
+++ b/model/postlude/step.sail
@@ -88,63 +88,64 @@ private function run_hart_waiting(_step_no : int, wr: WaitReason, instbits : ins
 
 private function run_hart_active(step_no: nat) -> Step = {
   match dispatchInterrupt(cur_privilege) {
-    Some(intr, priv) => Step_Pending_Interrupt(intr, priv),
-    None() => match ext_fetch_hook(fetch()) {
-      // extension error
-      F_Ext_Error(e)   => Step_Ext_Fetch_Failure(e),
-      // standard error
-      F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e),
-      // non-error cases:
-      F_RVC(h) => {
-        sail_instr_announce(h);
-        fetch_callback(h);
-        let instbits : instbits = zero_extend(h);
-        let instruction = ext_decode_compressed(h);
-        if   get_config_print_instr()
-        then {
-          print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(h) ^ ") " ^ to_str(instruction), zero_extend(PC));
+    Some(intr, priv) => return Step_Pending_Interrupt(intr, priv),
+    None() => (),
+  };
+  match ext_fetch_hook(fetch()) {
+    // extension error
+    F_Ext_Error(e)   => Step_Ext_Fetch_Failure(e),
+    // standard error
+    F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e),
+    // non-error cases:
+    F_RVC(h) => {
+      sail_instr_announce(h);
+      fetch_callback(h);
+      let instbits : instbits = zero_extend(h);
+      let instruction = ext_decode_compressed(h);
+      if   get_config_print_instr()
+      then {
+        print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(h) ^ ") " ^ to_str(instruction), zero_extend(PC));
+      };
+      // When ELP is set to LP_EXPECTED, the next instruction needs to be
+      // the non-RVC `LPAD` instruction.
+      if is_landing_pad_expected() then {
+        let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC);
+        Step_Execute(r, instbits)
+      }
+      // check for RVC once here instead of every RVC execute clause.
+      else if currentlyEnabled(Ext_Zca) then {
+        nextPC = PC + 2;
+        let result : ExecutionResult = match execute(instruction) {
+          ExecuteAs(other_inst) => execute(other_inst),
+          result => result,
         };
-        // When ELP is set to LP_EXPECTED, the next instruction needs to be
-        // the non-RVC `LPAD` instruction.
-        if is_landing_pad_expected() then {
-          let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC);
-          Step_Execute(r, instbits)
-        }
-        // check for RVC once here instead of every RVC execute clause.
-        else if currentlyEnabled(Ext_Zca) then {
-          nextPC = PC + 2;
-          let result : ExecutionResult = match execute(instruction) {
-            ExecuteAs(other_inst) => execute(other_inst),
-            result => result,
-          };
-          Step_Execute(result, instbits)
-        } else {
-          Step_Execute(Illegal_Instruction(), instbits)
-        }
-      },
-      F_Base(w) => {
-        sail_instr_announce(w);
-        fetch_callback(w);
-        let instbits : instbits = zero_extend(w);
-        let instruction = ext_decode(w);
-        if   get_config_print_instr()
-        then {
-          print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(w) ^ ") " ^ to_str(instruction), zero_extend(PC));
+        Step_Execute(result, instbits)
+      } else {
+        Step_Execute(Illegal_Instruction(), instbits)
+      }
+    },
+    F_Base(w) => {
+      sail_instr_announce(w);
+      fetch_callback(w);
+      let instbits : instbits = zero_extend(w);
+      let instruction = ext_decode(w);
+      if   get_config_print_instr()
+      then {
+        print_log_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ bits_str(PC) ^ " (" ^ bits_str(w) ^ ") " ^ to_str(instruction), zero_extend(PC));
+      };
+      // When ELP is set to LP_EXPECTED, if the next instruction in
+      // the instruction stream is not LPAD, then a software check
+      // exception with a landing pad fault code is thrown.
+      if is_landing_pad_expected() & not(is_lpad_instruction(instruction)) then {
+        let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC);
+        Step_Execute(r, instbits)
+      } else {
+        nextPC = PC + 4;
+        let result : ExecutionResult = match execute(instruction) {
+          ExecuteAs(other_inst) => execute(other_inst),
+          result => result,
         };
-        // When ELP is set to LP_EXPECTED, if the next instruction in
-        // the instruction stream is not LPAD, then a software check
-        // exception with a landing pad fault code is thrown.
-        if is_landing_pad_expected() & not(is_lpad_instruction(instruction)) then {
-          let r = Trap(cur_privilege, CTL_TRAP(make_landing_pad_exception()), PC);
-          Step_Execute(r, instbits)
-        } else {
-          nextPC = PC + 4;
-          let result : ExecutionResult = match execute(instruction) {
-            ExecuteAs(other_inst) => execute(other_inst),
-            result => result,
-          };
-          Step_Execute(result, instbits)
-        }
+        Step_Execute(result, instbits)
       }
     }
   }