riscv: remove break from main loop and place val spec in prelude.

2 files changed, 18 insertions, 19 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index 994324bd..8c93afdc 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -1,29 +1,26 @@
 val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 
-function break () : unit -> unit = ()
-
 val elf_tohost = "Elf_loader.elf_tohost" :  unit -> int
 
 function fetch_and_execute () =
   let tohost = __GetSlice_int(64, elf_tohost(), 0) in
   while true do {
-  print_bits("PC: ", PC);
-  let instr = __RISCV_read(PC, 4);
-  nextPC = PC + 4;
-  let instr_ast = decode(instr);
-  break ();
-  match instr_ast {
-    Some(ast) => execute(ast),
-    None      => {print("Decode failed"); exit (())}
-  };
-  let tohost_val = __RISCV_read(tohost, 4);
-  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 (());
+    print_bits("PC: ", PC);
+    let instr = __RISCV_read(PC, 4);
+    nextPC = PC + 4;
+    let instr_ast = decode(instr);
+    match instr_ast {
+      Some(ast) => execute(ast),
+      None      => {print("Decode failed"); exit (())}
+    };
+    let tohost_val = __RISCV_read(tohost, 4);
+    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 (());
   };
   PC = nextPC
 }
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 427da759..5d56858c 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -373,3 +373,5 @@ val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits
 val vector64 : int -> bits(64)
 
 function vector64 n = __raw_GetSlice_int(64, n, 0)
+
+function break () : unit -> unit = ()