4 files changed, 70 insertions, 43 deletions
diff --git a/mips/Makefile b/mips/Makefile
index 55d8e986..87fc96b6 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -13,15 +13,15 @@ MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.s
 MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail
 
 mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
-	$(SAIL) -ocaml -o mips $^
+	$(SAIL) -ocaml -o mips -memo_z3 $^
 
 mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
-	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen $^
+	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_no_tlb_types.lem: mips_no_tlb.lem
 
 # TODO: Use monomorphisation so that we can switch to machine words
 mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
-	$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen $^
+	$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_types.lem: mips.lem
 
 M%.thy: m%.lem m%_types.lem mips_extras.lem
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 12915271..bed8cd39 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -14,15 +14,23 @@ val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a
 let MEMr addr size             = read_mem Read_plain addr size
 let MEMr_reserve addr size     = read_mem Read_reserve addr size
 
+val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e
+let read_tag_bool addr =
+  read_tag addr >>= fun t ->
+  maybe_fail "read_tag_bool" (bool_of_bitU t)
+
+val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e
+let write_tag_bool addr t = write_tag addr (bitU_of_bool t) >>= fun _ -> return ()
+
 let MEMr_tag addr size =
   read_mem Read_plain addr size >>= fun v ->
-  read_tag addr >>= fun t ->
-  return (bool_of_bitU t, v)
+  read_tag_bool addr >>= fun t ->
+  return (t, v)
 
 let MEMr_tag_reserve addr size =
   read_mem Read_plain addr size >>= fun v ->
-  read_tag addr >>= fun t ->
-  return (bool_of_bitU t, v)
+  read_tag_bool addr >>= fun t ->
+  return (t, v)
 
 
 val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
@@ -44,8 +52,8 @@ val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b
 
 let MEMval _ size v                      = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional _ size v          = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag addr size t v             = write_mem_val v >>= fun _ -> write_tag addr (bitU_of_bool t) >>= fun _ -> return ()
-let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag addr (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
+let MEMval_tag addr size t v             = write_mem_val v >>= fun _ -> write_tag_bool addr t >>= fun _ -> return ()
+let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag_bool addr t >>= fun _ -> return (if b then true else false)
 
 val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e
 
@@ -57,11 +65,11 @@ let MEM_sync () = barrier Barrier_MIPS_SYNC
 let get_slice_int_bl len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  get_bits false bits hi lo
+  let bs = bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
 
 val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
 
 let write_ram _ size _ addr data =
   MEMea addr size >>
@@ -69,29 +77,48 @@ let write_ram _ size _ addr data =
 
 let read_ram _ size _ addr = MEMr addr size
 
-let sign_extend bits len = exts_bv len bits
-let zero_extend bits len = extz_bv len bits
-
-let shift_bits_left v n = shiftl_bv v (unsigned n)
-let shift_bits_right v n = shiftr_bv v (unsigned n)
-let shift_bits_right_arith v n = arith_shiftr_bv v (unsigned n)
-
-(* TODO: These could be monadic instead of hardcoded *)
-let internal_pick vs = head vs
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a
-let undefined_bitvector len = of_bits (repeat [B0] len)
-val undefined_bits : forall 'a. Bitvector 'a => integer -> 'a
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
+let string_of_bits bs = string_of_bv (bits_of bs)
+let string_of_int = show
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+let sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
+let zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
+
+let shift_bits_left v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in
+  maybe_fail "shift_bits_left" r
+let shift_bits_right v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in
+  maybe_fail "shift_bits_right" r
+let shift_bits_right_arith v n =
+  let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in
+  maybe_fail "shift_bits_right_arith" r
+
+(* Use constants for undefined values for now *)
+let internal_pick vs = return (head vs)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
 
 let skip () = return ()
diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail
index f0ffb9dd..c42e4764 100644
--- a/mips/mips_tlb_stub.sail
+++ b/mips/mips_tlb_stub.sail
@@ -36,7 +36,7 @@ $ifndef _MIPS_TLB_STUB
 $define _MIPS_TLB_STUB
 
 val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
-function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None
+function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None()
 
 val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
 function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) = 
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 5b89521f..272b6e04 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -86,9 +86,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
 overload operator | = {or_bool, or_vec}
 
-val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
-val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
 val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
 
@@ -355,18 +355,18 @@ infix 1 >>
 infix 1 <<
 infix 1 >>_s
 
-val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
 
 val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
 val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
 
 overload operator >> = {shift_bits_right, shiftr}
 overload operator << = {shift_bits_left, shiftl}
-val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
 
 infix 7 *_s
-val operator *_s = "smult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
+val operator *_s = "mults_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
 infix 7 *_u
 val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)