diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | prelude.sail | 69 | ||||
| -rw-r--r-- | riscv_mem.sail | 32 | ||||
| -rw-r--r-- | riscv_platform.c | 5 | ||||
| -rw-r--r-- | riscv_platform.h | 3 | ||||
| -rw-r--r-- | riscv_sys.sail | 2 |
6 files changed, 57 insertions, 57 deletions
@@ -2,7 +2,8 @@ SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail ris PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml SAIL_DIR ?= $(realpath ..) SAIL ?= $(SAIL_DIR)/sail -C_WARNINGS ?= -Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function +C_WARNINGS ?= +#-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function C_SRCS = riscv_prelude.c riscv_platform.c export SAIL_DIR diff --git a/prelude.sail b/prelude.sail index 6b2e13f..5d418aa 100644 --- a/prelude.sail +++ b/prelude.sail @@ -1,5 +1,7 @@ default Order dec +$include <flow.sail> + type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} @@ -144,8 +146,17 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything} +val vector_subrange = { + ocaml: "subrange", + lem: "subrange_vec_dec", + c: "vector_subrange", + coq: "subrange_vec_dec" +} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. + (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) +/* val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) +*/ val bitvector_access = {c: "bitvector_access", ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. (bits('n), atom('m)) -> bit @@ -183,14 +194,6 @@ val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n) overload ~ = {not_bool, not_vec} -val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool - -function neq_atom (x, y) = not_bool(eq_atom(x, y)) - -val neq_int = {lem: "neq"} : (int, int) -> bool - -function neq_int (x, y) = not_bool(eq_int(x, y)) - val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) @@ -199,27 +202,15 @@ val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, ' function neq_anything (x, y) = not_bool(x == y) -overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} - -val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool - -val builtin_and_vec = {c: "and_bits", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val and_vec = {lem: "and_vec", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -function and_vec (xs, ys) = builtin_and_vec(xs, ys) - -overload operator & = {and_bool, and_vec} - -val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool +overload operator != = {neq_vec, neq_anything} -val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val or_vec = {lem: "or_vec", coq: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +overload operator & = {and_vec} -function or_vec (xs, ys) = builtin_or_vec(xs, ys) +val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -overload operator | = {or_bool, or_vec} +overload operator | = {or_vec} val unsigned = {ocaml: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) @@ -276,16 +267,16 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val int_power = {ocaml: "int_power", lem: "pow", coq: "pow"} : (int, int) -> int +val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real overload operator ^ = {xor_vec, int_power, real_power, concat_str} -val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. +val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int +val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -295,12 +286,12 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} -val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. +val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", - lem: "integerMinus", coq: "sub_nat"} + lem: "integerMinus", coq: "sub_nat", c: "sub_nat"} : (nat, nat) -> nat val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -372,10 +363,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int overload operator / = {quotient_nat, quotient, quotient_real} -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int +val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int +val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int overload operator % = {modulus} @@ -385,13 +376,13 @@ val shl_int = "shl_int" : (int, int) -> int val shr_int = "shr_int" : (int, int) -> int -val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat -val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min"} : (int, int) -> int +val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int -val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat +val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat -val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max"} : (int, int) -> int +val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int overload min = {min_nat, min_int} @@ -522,7 +513,7 @@ function vector64 n = __raw_GetSlice_int(64, n, 0) val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) -val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. +val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. diff --git a/riscv_mem.sail b/riscv_mem.sail index 7268e9c..6c34134 100644 --- a/riscv_mem.sail +++ b/riscv_mem.sail @@ -58,17 +58,17 @@ function mem_read (addr, width, aq, rl, res) = { } } -val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n. +val MEMea = {lem: "MEMea", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n. +val MEMea_release = {lem: "MEMea_release", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n. +val MEMea_strong_release = {lem: "MEMea_strong_release", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n. +val MEMea_conditional = {lem: "MEMea_conditional", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n. +val MEMea_conditional_release = {lem: "MEMea_conditional_release", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n. +val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", _: "memea"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} @@ -136,13 +136,13 @@ function mem_write_value (addr, width, value, aq, rl, con) = { } } -val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr} -val MEM_fence_r_rw = {ocaml: "skip", lem: "MEM_fence_r_rw"} : unit -> unit effect {barr} -val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit effect {barr} -val MEM_fence_rw_w = {ocaml: "skip", lem: "MEM_fence_rw_w"} : unit -> unit effect {barr} -val MEM_fence_w_w = {ocaml: "skip", lem: "MEM_fence_w_w"} : unit -> unit effect {barr} -val MEM_fence_w_rw = {ocaml: "skip", lem: "MEM_fence_w_rw"} : unit -> unit effect {barr} -val MEM_fence_rw_r = {ocaml: "skip", lem: "MEM_fence_rw_r"} : unit -> unit effect {barr} -val MEM_fence_r_w = {ocaml: "skip", lem: "MEM_fence_r_w"} : unit -> unit effect {barr} -val MEM_fence_w_r = {ocaml: "skip", lem: "MEM_fence_w_r"} : unit -> unit effect {barr} -val MEM_fence_i = {ocaml: "skip", lem: "MEM_fence_i"} : unit -> unit effect {barr} +val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_r_rw = {lem: "MEM_fence_r_rw", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_r_r = {lem: "MEM_fence_r_r", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_rw_w = {lem: "MEM_fence_rw_w", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_w_w = {lem: "MEM_fence_w_w", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_w_rw = {lem: "MEM_fence_w_rw", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_rw_r = {lem: "MEM_fence_rw_r", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_r_w = {lem: "MEM_fence_r_w", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_w_r = {lem: "MEM_fence_w_r", _: "skip"} : unit -> unit effect {barr} +val MEM_fence_i = {lem: "MEM_fence_i", _: "skip"} : unit -> unit effect {barr} diff --git a/riscv_platform.c b/riscv_platform.c index 2ad3d3c..d21824a 100644 --- a/riscv_platform.c +++ b/riscv_platform.c @@ -46,3 +46,8 @@ void plat_insns_per_tick(sail_int *rop, unit u) mach_bits plat_htif_tohost(unit u) { return 0; } + +unit memea(mach_bits len, sail_int n) +{ + return UNIT; +} diff --git a/riscv_platform.h b/riscv_platform.h index 2d63dca..4401ad4 100644 --- a/riscv_platform.h +++ b/riscv_platform.h @@ -22,3 +22,6 @@ void plat_insns_per_tick(sail_int *rop, unit); unit plat_term_write(mach_bits); mach_bits plat_htif_tohost(unit); + +unit memea(mach_bits, sail_int); + diff --git a/riscv_sys.sail b/riscv_sys.sail index 94643ec..59bff60 100644 --- a/riscv_sys.sail +++ b/riscv_sys.sail @@ -765,7 +765,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit -val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem} +val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem} val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit |