diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 19 | ||||
| -rw-r--r-- | lib/elf.sail | 2 | ||||
| -rw-r--r-- | lib/flow.sail | 4 | ||||
| -rw-r--r-- | lib/instr_kinds.sail | 28 | ||||
| -rw-r--r-- | lib/regfp.sail | 28 | ||||
| -rw-r--r-- | lib/sail.h | 1 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 13 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 14 |
8 files changed, 96 insertions, 13 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 798bde12..6ddc58aa 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,19 +5,19 @@ $include <flow.sail> // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int +val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int overload operator + = {add_atom, add_int} // ***** Subtraction ***** -val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. +val sub_atom = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int overload operator - = {sub_atom, sub_int} @@ -29,18 +29,18 @@ val sub_nat = { // ***** Negation ***** -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) +val negate_atom = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int +val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int overload negate = {negate_atom, negate_int} // ***** Multiplication ***** -val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. +val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. (int('n), int('m)) -> int('n * 'm) -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int +val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int overload operator * = {mult_atom, mult_int} @@ -81,6 +81,7 @@ overload shr_int = {_shr32, _shr_int} /*! Truncating division (rounds towards zero) */ val tdiv_int = { ocaml: "tdiv_int", + interpreter: "tdiv_int", lem: "integerDiv_t", c: "tdiv_int" } : (int, int) -> int @@ -88,6 +89,7 @@ val tdiv_int = { /*! Remainder for truncating division (has sign of dividend) */ val tmod_int = { ocaml: "tmod_int", + interpreter: "tmod_int", lem: "integerMod_t", c: "tmod_int" } : (int, int) -> nat @@ -95,6 +97,7 @@ val tmod_int = { val abs_int = { smt : "abs", ocaml: "abs_int", + interpreter: "abs_int", lem: "abs_int", c: "abs_int", coq: "Z.abs" diff --git a/lib/elf.sail b/lib/elf.sail index 2d799d4d..6ea5de19 100644 --- a/lib/elf.sail +++ b/lib/elf.sail @@ -3,12 +3,14 @@ $define _ELF val elf_entry = { ocaml: "Elf_loader.elf_entry", + interpreter: "Elf_loader.elf_entry", lem: "elf_entry", c: "elf_entry" } : unit -> int val elf_tohost = { ocaml: "Elf_loader.elf_tohost", + interpreter: "Elf_loader.elf_tohost", lem: "elf_tohost", c: "elf_tohost" } : unit -> int diff --git a/lib/flow.sail b/lib/flow.sail index e6fe7fc0..5c69a128 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -25,9 +25,9 @@ val and_bool_no_flow = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool val or_bool = {coq: "orb", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q) -val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm) +val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm) -val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool +val eq_bool = {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool val neq_int = {lem: "neq"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm) function neq_int (x, y) = not_bool(eq_int(x, y)) diff --git a/lib/instr_kinds.sail b/lib/instr_kinds.sail new file mode 100644 index 00000000..66ef90c6 --- /dev/null +++ b/lib/instr_kinds.sail @@ -0,0 +1,28 @@ +union read_kind = { + Read_plain : unit, + Read_reserve : unit, + Read_acquire : unit, + Read_exclusive : unit, + Read_exclusive_acquire : unit, + Read_stream : unit, + Read_RISCV_acquire : unit, + Read_RISCV_strong_acquire : unit, + Read_RISCV_reserved : unit, + Read_RISCV_reserved_acquire : unit, + Read_RISCV_reserved_strong_acquire : unit, + Read_X86_locked : unit +} + +union write_kind = { + Write_plain : unit + Write_conditional : unit + Write_release : unit + Write_exclusive : unit + Write_exclusive_release : unit + Write_RISCV_release : unit + Write_RISCV_strong_release : unit + Write_RISCV_conditional : unit + Write_RISCV_conditional_release : unit + Write_RISCV_conditional_strong_release : unit + Write_X86_locked : unit +}
\ No newline at end of file diff --git a/lib/regfp.sail b/lib/regfp.sail index 6044e1cc..90af9b44 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -1,3 +1,6 @@ +$ifndef _REGFP +$define _REGFP + /* iR : input registers, * oR : output registers, * aR : registers feeding into the memory address */ @@ -110,3 +113,28 @@ union instruction_kind = { IK_simple : unit, IK_cache_op : cache_op_kind } + +val __read_mem + = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" } + : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem} +val __write_mem_ea + = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" } + : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem} +val __write_mem + = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" } + : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {wmv} +val __excl_res + = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_res" } + : unit -> bool effect {exmem} +val __barrier + = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" } + : barrier_kind -> unit effect {barr} + + +val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv} +function __write (wk, addr, len, value) = { + __write_mem_ea(wk, addr, len); + __write_mem(wk, addr, len, value) +} + +$endif @@ -376,6 +376,7 @@ void string_length(sail_int *len, sail_string s); void string_drop(sail_string *dst, sail_string s, sail_int len); void string_take(sail_string *dst, sail_string s, sail_int len); + /* ***** Printing ***** */ void string_of_int(sail_string *str, const sail_int i); diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 746d29c6..b4014aa6 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -7,6 +7,7 @@ type bits ('n : Int) = vector('n, dec, bit) val eq_bits = { ocaml: "eq_list", + interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec" @@ -28,6 +29,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", + interpreter: "length", lem: "length_list", c: "length", coq: "vec_length" @@ -48,6 +50,7 @@ THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits. */ val truncate = { ocaml: "vector_truncate", + interpreter: "vector_truncate", lem: "vector_truncate", coq: "vector_truncate", c: "sail_truncate" @@ -69,7 +72,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail overload operator ^ = {sail_mask} -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -79,6 +82,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) val bitvector_access = { ocaml: "access", + interpreter: "access", lem: "access_vec_dec", coq: "access_vec_dec", c: "vector_access" @@ -86,6 +90,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", + interpreter: "access", lem: "access_list_dec", coq: "vec_access_dec", c: "vector_access" @@ -95,6 +100,7 @@ overload vector_access = {bitvector_access, plain_vector_access} val bitvector_update = { ocaml: "update", + interpreter: "update", lem: "update_vec_dec", coq: "update_vec_dec", c: "vector_update" @@ -102,6 +108,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", + interpreter: "update", lem: "update_list_dec", coq: "vec_update_dec", c: "vector_update" @@ -111,6 +118,7 @@ overload vector_update = {bitvector_update, plain_vector_update} val add_bits = { ocaml: "add_vec", + interpreter: "add_vec", lem: "add_vec", c: "add_bits", coq: "add_vec" @@ -118,6 +126,7 @@ val add_bits = { val add_bits_int = { ocaml: "add_vec_int", + interpreter: "add_vec_int", lem: "add_vec_int", c: "add_bits_int", coq: "add_vec_int" @@ -144,6 +153,7 @@ overload operator | = {or_vec} val vector_subrange = { ocaml: "subrange", + interpreter: "subrange", lem: "subrange_vec_dec", c: "vector_subrange", coq: "subrange_vec_dec" @@ -152,6 +162,7 @@ val vector_subrange = { val vector_update_subrange = { ocaml: "update_subrange", + interpreter: "update_subrange", lem: "update_subrange_vec_dec", c: "vector_update_subrange", coq: "update_subrange_vec_dec" diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index 581dded7..daba99be 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -9,6 +9,7 @@ val "eq_bit" : (bit, bit) -> bool val eq_bits = { ocaml: "eq_list", + interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec" @@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", + interpreter: "length", lem: "length_list", c: "length", coq: "length_list" @@ -37,6 +39,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val truncate = { ocaml: "vector_truncate", + interpreter: "vector_truncate", lem: "vector_truncate", coq: "vector_truncate", c: "truncate" @@ -48,7 +51,7 @@ function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_exte overload operator ^ = {mask} -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -58,6 +61,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) val bitvector_access = { ocaml: "access", + interpreter: "access", lem: "access_vec_inc", coq: "access_vec_inc", c: "vector_access" @@ -65,6 +69,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", + interpreter: "access", lem: "access_list_inc", coq: "access_list_inc", c: "vector_access" @@ -74,6 +79,7 @@ overload vector_access = {bitvector_access, plain_vector_access} val bitvector_update = { ocaml: "update", + interpreter: "update", lem: "update_vec_inc", coq: "update_vec_inc", c: "vector_update" @@ -81,6 +87,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", + interpreter: "update", lem: "update_list_inc", coq: "update_list_inc", c: "vector_update" @@ -90,11 +97,12 @@ overload vector_update = {bitvector_update, plain_vector_update} val add_bits = { ocaml: "add_vec", + interpreter: "add_vec", c: "add_bits" } : forall 'n. (bits('n), bits('n)) -> bits('n) val add_bits_int = { - ocaml: "add_vec_int", + ocaml: "add_vec_int", interpreter: "add_vec_int", c: "add_bits_int" } : forall 'n. (bits('n), int) -> bits('n) @@ -102,6 +110,7 @@ overload operator + = {add_bits, add_bits_int} val vector_subrange = { ocaml: "subrange", + interpreter: "subrange", lem: "subrange_vec_inc", c: "vector_subrange", coq: "subrange_vec_inc" @@ -110,6 +119,7 @@ val vector_subrange = { val vector_update_subrange = { ocaml: "update_subrange", + interpreter: "update_subrange", lem: "update_subrange_vec_inc", c: "vector_update_subrange", coq: "update_subrange_vec_inc" |