Simplify the top-level execute loop using the step function.

2 files changed, 15 insertions, 50 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index 6337826e..684aeff0 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -5,51 +5,15 @@ val elf_tohost = {
   c: "elf_tohost"
 } :  unit -> int
 
-function fetch_and_execute () =
-  let tohost = __GetSlice_int(64, elf_tohost(), 0) in
+val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function loop () = {
+  let tohost = __GetSlice_int(64, elf_tohost(), 0);
   while true do {
     tick_clock();
-    print_bits("\nPC: ", PC);
+    step();
+    PC = nextPC;
 
-    /* for now, always fetch a 32-bit value.  this would need to
-       change with privileged mode, since we could cross a page
-       boundary with PC only 16-bit aligned in C mode.  */
-    let irdval = checked_mem_read(Instruction, PC, 4);
-    match (irdval) {
-      MemValue(instr) => {
-        let (instr_ast, instr_sz) : (option(ast), int) =
-          match (instr[1 .. 0]) {
-             0b11 => { cur_inst = EXTZ(instr);
-                       (decode(instr), 4)
-                     },
-             _    => { cur_inst = EXTZ(instr[15 .. 0]);
-                       (decodeCompressed(instr[15 .. 0]), 2)
-                     }
-          };
-        match (instr_ast, instr_sz) {
-          (Some(ast), 4) => print(BitStr(instr)          ^ ":  " ^ ast),
-          (Some(ast), 2) => print(BitStr(instr[15 .. 0]) ^ ":  " ^ ast),
-          (_,         _) => print(BitStr(instr)          ^ ":  no-decode")
-        };
-        /* check whether a compressed instruction is legal. */
-        if (misa.C() == 0b0 & (instr_sz == 2)) then {
-          let t : sync_exception = struct { trap = E_Illegal_Instr,
-                                            excinfo = Some(cur_inst) } in
-          nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-        } else {
-          nextPC = PC + instr_sz;
-          match instr_ast {
-            Some(ast) => execute(ast),
-            None()    => {print("Decode failed"); exit()}
-          }
-        }
-      },
-      MemException(e) => {
-        let t : sync_exception = struct { trap = e,
-                                          excinfo = Some(PC) } in
-        nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-      }
-    };
+    /* check htif exit */
     let tohost_val = __ReadRAM(64, 4, 0x0000_0000_0000_0000, tohost);
     if unsigned(tohost_val) != 0 then {
       let exit_val = unsigned(tohost_val >> 0b1) in
@@ -57,9 +21,9 @@ function fetch_and_execute () =
         print("SUCCESS")
       else
         print_int("FAILURE: ", exit_val);
-      exit (());
-  };
-  PC = nextPC
+      exit(());
+    }
+  }
 }
 
 val elf_entry = {
@@ -73,7 +37,7 @@ function main () = {
   PC = __GetSlice_int(64, elf_entry(), 0);
   try {
     init_sys ();
-    fetch_and_execute()
+    loop ()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
     Error_misaligned_access() => print("Error: misaligned_access"),
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index e670e2b8..b5d8e897 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -43,12 +43,13 @@ function fetch() -> FetchResult = {
 
 val step : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 function step() = {
-  tick_clock();
-
   match curInterrupt(mip, mie, mideleg) {
-    Some(intr, priv) =>
-      handle_interrupt(intr, priv),
+    Some(intr, priv) => {
+      print_bits("\nHandling interrupt: ", intr);
+      handle_interrupt(intr, priv)
+    },
     None() => {
+      print_bits("\nPC: ", PC);
       match fetch() {
         F_Error(e, addr) => handle_mem_exception(addr, e),
         F_RVC(h) => {