diff options
| -rw-r--r-- | cheri/Makefile | 2 | ||||
| -rw-r--r-- | mips/Makefile | 2 | ||||
| -rw-r--r-- | mips/prelude.sail | 11 |
3 files changed, 13 insertions, 2 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 44dc3c24..01583280 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -51,7 +51,7 @@ cheri_no_tlb.lem: $(CHERI_NO_TLB_SAILS) cheri_no_tlb_types.lem: cheri_no_tlb.lem cheri.lem: $(CHERI_SAILS) - $(SAIL) -lem -o cheri -lem_lib Mips_extras -undefined_gen -memo_z3 $^ + $(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_types.lem: cheri.lem cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) diff --git a/mips/Makefile b/mips/Makefile index 00703f62..a6a5bbdf 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/prelude.sail b/mips/prelude.sail index aa81175f..281ef5ea 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 @@ -120,6 +123,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) @@ -131,6 +137,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) @@ -292,3 +301,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> |