RISC-V: move the PC and minstret updates into the step function, to better localize them, making loop() purely a platform function.

1 files changed, 48 insertions, 46 deletions

diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 2d074f27..8e5a0090 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -42,52 +42,58 @@ function fetch() -> FetchResult =
     }
   }
 
-/* returns whether an instruction was retired, and whether to increment the step count in the trace */
-val step : int -> (bool, bool) effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-function step(step_no) =
-  match curInterrupt(cur_privilege, mip, mie, mideleg) {
-    Some(intr, priv) => {
-      print_bits("Handling interrupt: ", intr);
-      handle_interrupt(intr, priv);
-      (false, false)
-    },
-    None() => {
-      match fetch() {
-        F_Error(e, addr) => {
-          handle_mem_exception(addr, e);
-          (false, false)
-        },
-        F_RVC(h) => {
-          match decodeCompressed(h) {
-            None() => {
-              print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
-              handle_decode_exception(EXTZ(h));
-              (false, true)
-            },
-            Some(ast) => {
-              print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
-              nextPC = PC + 2;
-              (execute(ast), true)
+/* returns whether to increment the step count in the trace */
+val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function step(step_no) = {
+  minstret_written = false;     /* see note for minstret */
+  let (retired, stepped) : (bool, bool) =
+    match curInterrupt(cur_privilege, mip, mie, mideleg) {
+      Some(intr, priv) => {
+        print_bits("Handling interrupt: ", intr);
+        handle_interrupt(intr, priv);
+        (false, false)
+      },
+      None() => {
+        match fetch() {
+          F_Error(e, addr) => {
+            handle_mem_exception(addr, e);
+            (false, false)
+          },
+          F_RVC(h) => {
+            match decodeCompressed(h) {
+              None() => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
+                handle_decode_exception(EXTZ(h));
+                (false, true)
+              },
+              Some(ast) => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+                nextPC = PC + 2;
+                (execute(ast), true)
+              }
             }
-          }
-        },
-        F_Base(w) => {
-          match decode(w) {
-            None() => {
-              print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
-              handle_decode_exception(EXTZ(w));
-              (false, true)
-            },
-            Some(ast) => {
-              print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
-              nextPC = PC + 4;
-              (execute(ast), true)
+          },
+          F_Base(w) => {
+            match decode(w) {
+              None() => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
+                handle_decode_exception(EXTZ(w));
+                (false, true)
+              },
+              Some(ast) => {
+                print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+                nextPC = PC + 4;
+                (execute(ast), true)
+              }
             }
           }
         }
       }
-    }
-  }
+    };
+  PC = nextPC;
+  if retired then retire_instruction();
+  stepped
+}
 
 val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 function loop () = {
@@ -95,11 +101,7 @@ function loop () = {
   i : int = 0;
   step_no : int = 0;
   while (~ (htif_done)) do {
-    minstret_written = false;     /* see note for minstret */
-    let (retired, stepped) = step(step_no);
-    PC = nextPC;
-    if retired then retire_instruction();
-
+    let stepped = step(step_no);
     if stepped then step_no = step_no + 1;
 
     /* check htif exit */