diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 2 | ||||
| -rw-r--r-- | mips/mips_extras_sequential.lem | 116 | ||||
| -rw-r--r-- | mips/prelude.sail | 11 |
3 files changed, 128 insertions, 1 deletions
diff --git a/mips/Makefile b/mips/Makefile index 6d605d60..c0670380 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -21,7 +21,7 @@ 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 -memo_z3 $^ + $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -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_sequential.lem b/mips/mips_extras_sequential.lem new file mode 100644 index 00000000..c3651500 --- /dev/null +++ b/mips/mips_extras_sequential.lem @@ -0,0 +1,116 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_instr_kinds +open import Sail_values +open import Sail_operators +open import State_monad +open import State + +val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e +val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e +val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e + +let MEMr addr size = read_memS Read_plain addr size +let MEMr_reserve addr size = read_memS Read_reserve addr size + +val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monadS 'regval bool 'e +let read_tag_bool addr = + read_tagS addr >>$= fun t -> + maybe_failS "read_tag_bool" (bool_of_bitU t) + +val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monadS 'regval unit 'e +let write_tag_bool addr t = write_tagS addr (bitU_of_bool t) >>$= fun _ -> returnS () + +let MEMr_tag addr size = + read_memS Read_plain addr size >>$= fun v -> + read_tag_bool addr >>$= fun t -> + returnS (t, v) + +let MEMr_tag_reserve addr size = + read_memS Read_plain addr size >>$= fun v -> + read_tag_bool addr >>$= fun t -> + returnS (t, v) + + +val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e +val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e +val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e +val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e + +let MEMea addr size = write_mem_eaS Write_plain addr (nat_of_int size) +let MEMea_conditional addr size = write_mem_eaS Write_conditional addr (nat_of_int size) + +let MEMea_tag addr size = write_mem_eaS Write_plain addr (nat_of_int size) +let MEMea_tag_conditional addr size = write_mem_eaS Write_conditional addr (nat_of_int size) + + +val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval unit 'e +val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval bool 'e +val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval unit 'e +val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval bool 'e + +let MEMval _ size v = write_mem_valS v >>$= fun _ -> returnS () +let MEMval_conditional _ size v = write_mem_valS v >>$= fun b -> returnS (if b then true else false) +let MEMval_tag addr size t v = write_mem_valS v >>$= fun _ -> write_tag_bool addr t >>$= fun _ -> returnS () +let MEMval_tag_conditional addr size t v = write_mem_valS v >>$= fun b -> write_tag_bool addr t >>$= fun _ -> returnS (if b then true else false) + +val MEM_sync : forall 'regval 'e. unit -> monadS 'regval unit 'e + +let MEM_sync () = returnS () (*barrier Barrier_MIPS_SYNC*) + +(* Some wrappers copied from aarch64_extras *) +(* TODO: Harmonise into a common library *) + +let get_slice_int_bl len n lo = + (* TODO: Is this the intended behaviour? *) + let hi = lo + len - 1 in + 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_bools (get_slice_int_bl len n lo) + +let write_ram _ size _ addr data = + MEMea addr size >>$ + MEMval addr size data + +let read_ram _ size _ addr = MEMr addr size + +let inline reg_deref = read_regS + +let string_of_bits bs = string_of_bv (bits_of bs) +let string_of_int = show + +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_failS "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_failS "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_failS "shift_bits_right_arith" r + +(* Use constants for undefined values for now *) +let internal_pick vs = returnS (head vs) +let undefined_bool = undefined_boolS +let undefined_string () = returnS "" +let undefined_unit () = returnS () +let undefined_int () = returnS (0:ii) +val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monadS 'rv (list 'a) 'e +let undefined_vector len u = returnS (repeat [u] len) +val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e +let undefined_bitvector len = returnS (of_bools (repeat [false] len)) +val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e +let undefined_bits = undefined_bitvector +let undefined_bit () = returnS B0 +let undefined_real () = returnS (realFromFrac 0 1) +let undefined_range i j = returnS i +let undefined_atom i = returnS i +let undefined_nat () = returnS (0:ii) + +let skip () = returnS () diff --git a/mips/prelude.sail b/mips/prelude.sail index e0bcd8cf..5bb79f97 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -1,8 +1,11 @@ +$include <smt.sail> + default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} + val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool @@ -126,6 +129,9 @@ val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int overload operator ^ = {xor_vec, int_power} +val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('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) @@ -137,6 +143,9 @@ val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) overload operator + = {add_range, add_int, add_vec, add_vec_int} +val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n - 'm) + val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) @@ -301,3 +310,5 @@ val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n) function mask bs = bs['n - 1 .. 0] val "get_time_ns" : unit -> int + +$include <mono_rewrites.sail> |