changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ocaml main so that we can have simboot + kernel. Support UART output only.

6 files changed, 37 insertions, 21 deletions

diff --git a/lib/main.ml b/lib/main.ml
index 5733425f..1e9943a7 100644
--- a/lib/main.ml
+++ b/lib/main.ml
@@ -52,8 +52,19 @@
 open Elf_loader;;
 
 let opt_file_arguments = ref ([] : string list)
-
-let options = Arg.align []
+let opt_raw_fname = ref ""
+let opt_raw_addr = ref Nat_big_num.zero
+let options = Arg.align [
+    ( "-raw",
+      Arg.String (fun s ->
+      let l = String.split_on_char '@' s in
+      match l with
+      | [fname;addr] -> begin
+          opt_raw_fname := fname;
+          opt_raw_addr := Nat_big_num.of_string addr;
+        end
+      | _ -> raise (Arg.Bad (s ^ " not of form <filename>@:<addr>"))),
+    "<file@0xADDR> load a raw binary in memory at given address.")]
 
 let usage_msg = "Sail OCaml RTS options:"
 
@@ -67,4 +78,15 @@ let () =
     | f :: _ -> load_elf f
     | _ -> ()
   end;
+  if !opt_raw_fname != "" then
+    begin
+      let ic = open_in_bin !opt_raw_fname in
+      try
+        while true do
+          let b = input_byte ic in
+          Sail_lib.wram !opt_raw_addr b;
+          opt_raw_addr := Nat_big_num.succ !opt_raw_addr;
+        done
+      with End_of_file -> ();
+    end;
   (* ocaml_backend.ml will append from here *)
diff --git a/mips/main.sail b/mips/main.sail
index 54fb34ee..45ced6d7 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -30,6 +30,10 @@ function fetch_and_execute () = {
        just continue from nextPC, which should have been set to the appropriate
        exception vector (along with clearing branchPending etc.) . */
   };
+  if UART_WRITTEN then {
+    putchar(unsigned(UART_WDATA));
+    UART_WRITTEN = 0b0;
+  }
 }
 
 val elf_entry = {
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index f9049b5d..c151f38b 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -614,22 +614,20 @@ function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 *
     reverse_endianness'(sizeof 'W, value)
 }*/
 
-val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem}
-function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size))
-/* TODO
+val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg}
+function MEMr_wrapper (addr, size) = 
     if (addr == 0x000000007f000000) then
       {
         let rvalid = UART_RVALID in
-	let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in
         {
           UART_RVALID = [bitzero];
-          rdata
+          mask(0x00000000 @ UART_RDATA @ rvalid @ 0b0000000 @ 0x0000)
         }
       }
     else if (addr == 0x000000007f000004) then
       mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */
     else
-      reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */
+      reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */
 
 val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
 function MEMr_reserve_wrapper (addr , size) =
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 70e6fa83..0cc098a5 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -42,7 +42,7 @@ function MEMw_wrapper(addr, size, data) =
     if (addr == 0x000000007f000000) then
       {
         UART_WDATA   = ledata[7..0];
-	UART_WRITTEN = bitone;
+        UART_WRITTEN = bitone;
       } else {
         MEMea(addr, size);
         MEMval(addr, size, ledata);
diff --git a/mips/prelude.sail b/mips/prelude.sail
index f805876a..477d0967 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -27,6 +27,7 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 overload operator == = {eq_bit}
 
 $include <flow.sail>
+$include <arith.sail>
 
 overload operator == = {eq_vec, eq_string, eq_anything}
 
@@ -135,8 +136,6 @@ val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm.
 val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
-
 val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
@@ -149,16 +148,12 @@ val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n
 val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int
-
 val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
 
 val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
 
-val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int
-
 overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int}
 
 overload negate = {negate_range, negate_int}
@@ -166,8 +161,6 @@ overload negate = {negate_range, negate_int}
 val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
 
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-
 overload operator * = {mult_range, mult_int}
 
 val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
@@ -219,7 +212,6 @@ function operator ^^ (bs, n) = replicate_bits (bs, n)
 
 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
 val print_string = "print_string" : (string, string) -> unit
 
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 47acae88..21a84af8 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -523,13 +523,13 @@ let real_of_string str =
 let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
 
 let print_int (str, x) =
-  print_endline (str ^ Big_int.to_string x)
+  prerr_endline (str ^ Big_int.to_string x)
 
 let print_bits (str, xs) =
-  print_endline (str ^ string_of_bits xs)
+  prerr_endline (str ^ string_of_bits xs)
 
 let print_string(str, msg) =
-  print_endline (str ^ msg)
+  prerr_endline (str ^ msg)
 
 let reg_deref r = !r