diff options
| author | Alasdair Armstrong | 2018-01-24 16:25:37 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-24 16:25:37 +0000 |
| commit | cd81acaf58db3edc4187e4cccc35f6aa76d6933d (patch) | |
| tree | 8f1235524095ca0928723ab78e7c6ec8c29dde7c | |
| parent | a55259301692a5c56bb7f389dc8dc59c0e19fe41 (diff) | |
Fixed riscv ocaml compilation
| -rw-r--r-- | riscv/prelude.sail | 5 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 12 | ||||
| -rw-r--r-- | src/sail_lib.ml | 2 |
3 files changed, 12 insertions, 7 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 6f37a6e3..6b58cd2b 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -139,7 +139,10 @@ val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m) -val cast "cast_unit_vec" : bit -> bits(1) +val cast cast_unit_vec : bit -> bits(1) + +function cast_unit_vec bitzero = 0b0 +and cast_unit_vec bitone = 0b1 val print = "prerr_endline" : string -> unit diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index e8f1c5bc..d338bab9 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -103,17 +103,17 @@ function mem_read (addr, width, aq, rl, res) = { } } -val MEMea = {ocaml: "skip", lem: "MEMea"} : forall 'n. +val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} -val MEMea_release = {ocaml: "skip", lem: "MEMea_release"} : forall 'n. +val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} -val MEMea_strong_release = {ocaml: "skip", lem: "MEMea_strong_release"} : forall 'n. +val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} -val MEMea_conditional = {ocaml: "skip", lem: "MEMea_conditional"} : forall 'n. +val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} -val MEMea_conditional_release = {ocaml: "skip", lem: "MEMea_conditional_release"} : forall 'n. +val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} -val MEMea_conditional_strong_release = {ocaml: "skip", lem: "MEMea_conditional_strong_release"} : forall 'n. +val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n. (bits(64), atom('n)) -> unit effect {eamem} val mem_write_ea : forall 'n. (bits(64), atom('n), bool, bool, bool) -> unit effect {eamem, escape} diff --git a/src/sail_lib.ml b/src/sail_lib.ml index c78b81a9..3cd8e18c 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -490,6 +490,8 @@ let rec string_of_list sep string_of = function let skip () = () +let memea (_, _) = () + let zero_extend (vec, n) = let m = Big_int.to_int n in if m <= List.length vec |