Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2

2 files changed, 19 insertions, 2 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index f7099398..994324bd 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -2,14 +2,28 @@ val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, r
 
 function break () : unit -> unit = ()
 
-function fetch_and_execute () = while true do {
+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      => exit (())
+    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 6b58cd2b..427da759 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -27,6 +27,8 @@ val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). li
 overload length = {bitvector_length, vector_length, list_length}
 
 val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
 
@@ -323,6 +325,7 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
 val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 
 val print_int = "print_int" : (string, int) -> unit
+val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 union exception = {
   Error_not_implemented : string,