Refactor try_step() some more

* Simplify the `stepped` code. It is equivalent to whether or not the model ends in an active state, so we can just return that.
* Simplify handling of `minstret_increment`.
* Change `step_no` to `nat`.
* Remove unused `exit_wait` parameter from `run_hart_active()`.
* Change `instbits` to 32-bit instead of xlenbits.

Author: Timmmm

model/riscv_platform.sail

@@ -446,9 +446,9 @@ function tick_platform() -> unit = {
 
 /* Platform-specific handling of instruction faults */
 
-function handle_illegal(instbits: xlenbits) -> unit = {
-  let info = if plat_mtval_has_illegal_inst_bits ()
-             then Some(instbits)
+function handle_illegal(instbits : instbits) -> unit = {
+  let info = if plat_mtval_has_illegal_inst_bits()
+             then Some(zero_extend(xlen, instbits))
              else None();
   let t : sync_exception = struct { trap    = E_Illegal_Instr(),
                                     excinfo = info,

model/riscv_step.sail

@@ -10,28 +10,6 @@
 
 register hart_state : HartState = HART_ACTIVE()
 
-// Returns whether the retire result returned by the execution of an
-// instruction counts as a step, where a step is said to occur when an
-// instruction retires successfully or it raises an exception.
-// Crucially, if an instruction returns a Wait retire result, it does
-// not step.
-function retires_or_traps(r : ExecutionResult(Retire_Failure)) -> bool =
-  match r {
-    RETIRE_OK()                        => true,
-    RETIRE_FAIL(Illegal_Instruction()) => true,
-    RETIRE_FAIL(Memory_Exception(_))   => true,
-    RETIRE_FAIL(Trap(_))               => true,
-
-    // do not step if a wait instruction executed.
-    RETIRE_FAIL(Wait_For_Interrupt())  => false,
-
-    // errors from extensions
-    RETIRE_FAIL(Ext_ControlAddr_Check_Failure(_)) => true,
-    RETIRE_FAIL(Ext_DataAddr_Check_Failure(_))    => true,
-    RETIRE_FAIL(Ext_CSR_Check_Failure())          => true,
-    RETIRE_FAIL(Ext_XRET_Priv_Failure(_))         => true,
-}
-
 union Step = {
   Step_Pending_Interrupt  : (InterruptType, Privilege),
   Step_Ext_Fetch_Failure  : ext_fetch_addr_error,
@@ -40,15 +18,15 @@ union Step = {
   Step_Waiting            : unit,
 }
 
-function run_hart_waiting(step_no : int, exit_wait : bool, instbits : instbits) -> (Step, bool) = {
+function run_hart_waiting(step_no : nat, exit_wait : bool, instbits : instbits) -> Step = {
   if shouldWakeForInterrupt() then {
     if   get_config_print_instr()
     then print_instr("interrupt exit from WAIT state at PC " ^ BitStr(PC));
 
     hart_state = HART_ACTIVE();
     // The waiting instruction retires successfully.  The
     // pending interrupts will be handled in the next step.
-    (Step_Execute(RETIRE_OK(), instbits), true)
+    Step_Execute(RETIRE_OK(), instbits)
   } else if exit_wait then {
     // There are no pending interrupts; transition out of the Wait
     // as instructed.
@@ -61,27 +39,27 @@ function run_hart_waiting(step_no : int, exit_wait : bool, instbits : instbits)
     // implementation-specific, bounded time limit, the WFI
     // instruction causes an illegal-instruction exception."
     if   (cur_privilege == Machine | mstatus[TW] == 0b0)
-    then (Step_Execute(RETIRE_OK(), instbits), true)
-    else (Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits), true)
+    then Step_Execute(RETIRE_OK(), instbits)
+    else Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits)
   } else {
     if   get_config_print_instr()
     then print_instr("remaining in WAIT state at PC " ^ BitStr(PC));
-    (Step_Waiting(), false)
+    Step_Waiting()
   }
 }
 
-function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
+function run_hart_active(step_no: nat) -> Step = {
   match dispatchInterrupt(cur_privilege) {
-    Some(intr, priv) => (Step_Pending_Interrupt(intr, priv), false),
+    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), false),
+      F_Ext_Error(e)   => Step_Ext_Fetch_Failure(e),
       /* standard error */
-      F_Error(e, addr) => (Step_Fetch_Failure(Virtaddr(addr), e), false),
+      F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e),
       /* non-error cases: */
       F_RVC(h) => {
         sail_instr_announce(h);
-        let instbits : xlenbits = zero_extend(h);
+        let instbits : instbits = zero_extend(h);
         let ast = ext_decode_compressed(h);
         if   get_config_print_instr()
         then {
@@ -91,9 +69,9 @@ function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
         if currentlyEnabled(Ext_Zca) then {
           nextPC = PC + 2;
           let r = execute(ast);
-          (Step_Execute(r, instbits), retires_or_traps(r))
+          Step_Execute(r, instbits)
         } else {
-          (Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits), true)
+          Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits)
         }
       },
       F_Base(w) => {
@@ -106,7 +84,7 @@ function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
         };
         nextPC = PC + 4;
         let r = execute(ast);
-        (Step_Execute(r, instbits), retires_or_traps(r))
+        Step_Execute(r, instbits)
       }
     }
   }
@@ -117,12 +95,28 @@ function wfi_is_nop() -> bool = config platform.wfi_is_nop
 // The `try_step` function is the main internal driver of the Sail
 // model. It performs the fetch-decode-execute for an instruction. It
 // is also the primary interface to the non-Sail execution harness.
-// The harness calls this function with the current step number (which
-// numbers the active or wait step), and whether it should exit a wait
-// state. The `try_step` function returns whether the Sail emulator
-// executed a step, and the stepper state at the end of the step.
-
-function try_step(step_no : int, exit_wait : bool) -> bool = {
+//
+// A "step" is a full execution of an instruction, resulting either
+// in its retirement or a trap. WFI and WRS instructions can cause
+// the model to wait (hart_state is HART_WAITING), in which case
+// a step has not happened and `try_step()` returns false. Otherwise
+// it returns true. Equivalently, it returns whether the model is now
+// in an active state (HART_ACTIVE).
+//
+// * step_no: the current step number; this is maintained by by the
+//            non-Sail harness and is incremented when `try_step()`
+//            returns true.
+// * exit_wait: if true, and the model is waiting (HART_WAITING)
+//              then it will wake up (switch to HART_ACTIVE) and
+//              complete the WFI/WRS instruction, either successfully
+//              retiring it or causing an illegal instruction
+//              exception depending on mstatus[TW]. `exit_wait`
+//              only affects the behaviour if the model is already
+//              waiting from a previous WFI/WRS. It doesn't affect
+//              WFI/WRS instructions executed in the same call of
+//              `try_step()` (but see `wfi_is_nop()`).
+//
+function try_step(step_no : nat, exit_wait : bool) -> bool = {
   /* for step extensions */
   ext_pre_step_hook();
 
@@ -136,95 +130,72 @@ function try_step(step_no : int, exit_wait : bool) -> bool = {
    */
   minstret_increment = should_inc_minstret(cur_privilege);
 
-  let (step_val, did_step) : (Step, bool) = match hart_state {
+  let step_val : Step = match hart_state {
       HART_WAITING(instbits) => run_hart_waiting(step_no, exit_wait, instbits),
-      HART_ACTIVE()          => run_hart_active(step_no, exit_wait),
+      HART_ACTIVE()          => run_hart_active(step_no),
     };
 
-  var stepped : bool = did_step;
-
   match step_val {
     Step_Pending_Interrupt(intr, priv) => {
       if   get_config_print_instr()
       then print_bits("Handling interrupt: ", interruptType_to_bits(intr));
-      minstret_increment = false;
       handle_interrupt(intr, priv)
     },
-    Step_Ext_Fetch_Failure(e) => {
-      minstret_increment = false;
-      ext_handle_fetch_check_error(e)
-    },
-    Step_Fetch_Failure(vaddr, e) => {
-      minstret_increment = false;
-      handle_mem_exception(vaddr, e)
-    },
-    Step_Waiting() => {
-      assert(hart_is_waiting(hart_state), "cannot be Waiting in a non-Wait state")
-    },
-    Step_Execute(RETIRE_OK(), _) => {
-      assert(hart_is_active(hart_state))
-    },
+    Step_Ext_Fetch_Failure(e) => ext_handle_fetch_check_error(e),
+    Step_Fetch_Failure(vaddr, e) => handle_mem_exception(vaddr, e),
+    Step_Waiting() => assert(hart_is_waiting(hart_state), "cannot be Waiting in a non-Wait state"),
+    Step_Execute(RETIRE_OK(), _) => assert(hart_is_active(hart_state)),
     // standard errors
-    Step_Execute(RETIRE_FAIL(Trap(priv, ctl, pc)), _) => {
-      minstret_increment = false;
-      set_next_pc(exception_handler(priv, ctl, pc))
-    },
-    Step_Execute(RETIRE_FAIL(Memory_Exception(vaddr, e)), _) => {
-      minstret_increment = false;
-      handle_mem_exception(vaddr, e)
-    },
-    Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits) => {
-      minstret_increment = false;
-      handle_illegal(instbits)
-    },
+    Step_Execute(RETIRE_FAIL(Trap(priv, ctl, pc)), _) => set_next_pc(exception_handler(priv, ctl, pc)),
+    Step_Execute(RETIRE_FAIL(Memory_Exception(vaddr, e)), _) => handle_mem_exception(vaddr, e),
+    Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits) => handle_illegal(instbits),
     Step_Execute(RETIRE_FAIL(Wait_For_Interrupt()), instbits) =>
       if wfi_is_nop() then {
         // This is the same as the RETIRE_OK case.
         assert(hart_is_active(hart_state));
-        // Override the default step for WFI.
-        stepped = true;
       } else {
         // Transition into the wait state.
         if   get_config_print_instr()
         then print_instr("entering WAIT state at PC " ^ BitStr(PC));
         hart_state = HART_WAITING(instbits);
       },
     // errors from extensions
-    Step_Execute(RETIRE_FAIL(Ext_CSR_Check_Failure()), _) => {
-      minstret_increment = false;
-      ext_check_CSR_fail()
-    },
-    Step_Execute(RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), _) => {
-      minstret_increment = false;
-      ext_handle_control_check_error(e)
-    },
-    Step_Execute(RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), _) => {
-      minstret_increment = false;
-      ext_handle_data_check_error(e)
-    },
-    Step_Execute(RETIRE_FAIL(Ext_XRET_Priv_Failure()), _) => {
-      minstret_increment = false;
-      ext_fail_xret_priv ()
-    },
+    Step_Execute(RETIRE_FAIL(Ext_CSR_Check_Failure()), _) => ext_check_CSR_fail(),
+    Step_Execute(RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), _) => ext_handle_control_check_error(e),
+    Step_Execute(RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), _) => ext_handle_data_check_error(e),
+    Step_Execute(RETIRE_FAIL(Ext_XRET_Priv_Failure()), _) => ext_fail_xret_priv(),
   };
 
   match hart_state {
-    HART_WAITING(_) => (),
+    HART_WAITING(_) => false,
     HART_ACTIVE() => {
       tick_pc();
-      update_minstret();
+
+      let retired : bool = match step_val {
+        Step_Execute(RETIRE_OK(), _) => true,
+        // WFI retires immediately if the model is configured to treat it as a nop.
+        // Otherwise it always waits for at least one call of `try_step()`.
+        Step_Execute(RETIRE_FAIL(Wait_For_Interrupt()), _) if wfi_is_nop() => true,
+        _ => false,
+      };
+
+      // Increment minstret if we retired an instruction and the
+      // update wasn't suppressed by writing to it explicitly or
+      // mcountinhibit[IR] or minstretcfg.
+      if retired & minstret_increment then minstret = minstret + 1;
+
       /* for step extensions */
       ext_post_step_hook();
+      // Return that we have stepped and are active.
+      true
     }
-  };
-
-  stepped
+  }
 }
 
 function loop () : unit -> unit = {
   let insns_per_tick = plat_insns_per_tick();
-  var i : int = 0;
-  var step_no : int = 0;
+  var i : nat = 0;
+  var step_no : nat = 0;
   while not(htif_done) do {
     // This standalone loop always exits immediately out of waiting
     // states.

model/riscv_step_common.sail

@@ -18,23 +18,13 @@
 // instruction should finish execution.  Note that in the latter
 // case, the platform can decide to end the stall for any reason,
 // even if there are no interrupts or invalidated reservation set.
-
-type instbits = xlenbits
-
 union HartState = {
   HART_ACTIVE  : unit,
-  HART_WAITING : instbits, // the instruction that caused the wait
-}
-
-/* The result of a fetch, which includes any possible error
- * from an extension that interposes on the fetch operation.
- */
-
-union FetchResult = {
-  F_Ext_Error : ext_fetch_addr_error,      /* For extensions */
-  F_Base      : word,                      /* Base ISA */
-  F_RVC       : half,                      /* Compressed ISA */
-  F_Error     : (ExceptionType, xlenbits)  /* standard exception and PC */
+  // The instruction that caused the wait. This is needed
+  // because WFI and WRS can time out and cause an illegal
+  // instruction exception so we need to know what to write
+  // to mtval.
+  HART_WAITING : instbits,
 }
 
 // utility predicates
@@ -50,3 +40,14 @@ function hart_is_waiting(s : HartState) -> bool =
     HART_ACTIVE()   => false,
     HART_WAITING(_) => true,
   }
+
+/* The result of a fetch, which includes any possible error
+ * from an extension that interposes on the fetch operation.
+ */
+
+union FetchResult = {
+  F_Ext_Error : ext_fetch_addr_error,      /* For extensions */
+  F_Base      : word,                      /* Base ISA */
+  F_RVC       : half,                      /* Compressed ISA */
+  F_Error     : (ExceptionType, xlenbits)  /* standard exception and PC */
+}

model/riscv_sys_regs.sail

@@ -638,10 +638,6 @@ register minstret : bits(64)
 /* Should minstret be incremented when the instruction is retired. */
 register minstret_increment : bool
 
-function update_minstret() -> unit = {
-  if minstret_increment then minstret = minstret + 1;
-}
-
 /* machine information registers */
 register mvendorid : bits(32) = zeros()
 register mimpid : xlenbits = zeros()

model/riscv_types.sail

@@ -20,6 +20,9 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1)
 type half = bits(16)
 type word = bits(32)
 
+// Bit-vector of an uncompressed instruction.
+type instbits = bits(32)
+
 type pagesize_bits : Int = 12
 let  pagesize_bits = sizeof(pagesize_bits)