Move the top-level loop from main to riscv_step, but remove elf bits.

2 files changed, 25 insertions, 27 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index 0a46181b..c923935b 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -1,34 +1,8 @@
-val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
   c: "elf_tohost"
 } :  unit -> int
 
-val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-function loop () = {
-  let tohost = __GetSlice_int(64, elf_tohost(), 0);
-  i : int = 0;
-  while true do {
-    tick_clock();
-    print_int("\nstep: ", i);
-    let retired : bool = step();
-    PC = nextPC;
-    if retired then i = i + 1;
-
-    /* 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
-      if exit_val == 0 then
-        print("SUCCESS")
-      else
-        print_int("FAILURE: ", exit_val);
-      exit(());
-    }
-  }
-}
-
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
   c: "elf_entry"
@@ -40,7 +14,7 @@ function main () = {
   PC = __GetSlice_int(64, elf_entry(), 0);
   try {
     init_sys ();
-    loop ()
+    loop (elf_tohost())
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
     Error_internal_error() => print("Error: internal error")
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 7ddd8a44..d241b84a 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -90,3 +90,27 @@ function step() = {
     }
   }
 }
+
+val loop : int -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function loop (tohost_addr) = {
+  let tohost = __GetSlice_int(64, tohost_addr, 0);
+  i : int = 0;
+  while true do {
+    tick_clock();
+    print_int("\nstep: ", i);
+    let retired : bool = step();
+    PC = nextPC;
+    if retired then i = i + 1;
+
+    /* 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
+      if exit_val == 0 then
+        print("SUCCESS")
+      else
+        print_int("FAILURE: ", exit_val);
+      exit(());
+    }
+  }
+}