diff options
| -rw-r--r-- | LICENCE | 30 | ||||
| -rw-r--r-- | Makefile | 22 | ||||
| -rw-r--r-- | handwritten_support/0.7.1/riscv_extras.lem | 137 | ||||
| -rw-r--r-- | handwritten_support/0.7.1/riscv_extras_sequential.lem | 137 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 22 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 2 | ||||
| -rw-r--r-- | model/prelude.sail | 8 |
7 files changed, 323 insertions, 35 deletions
@@ -1,28 +1,28 @@ RISCV Sail Model -The Sail architecture models here, comprising all files and -directories are subject to the BSD two-clause licence +This Sail RISC-V architecture model here, comprising all files and +directories, is subject to the BSD two-clause licence below. -Copyright (c) 2013-2018 - Kathyrn Gray - Shaked Flur - Stephen Kell - Gabriel Kerneis +Copyright (c) 2017-2019 + Prashanth Mundkur + Jon French + Brian Campbell Robert Norton-Wright - Christopher Pulte - Peter Sewell Alasdair Armstrong - Brian Campbell Thomas Bauereiss - Anthony Fox - Jon French - Dominic Mulligan - Stephen Kell - Mark Wassell + Shaked Flur + Christopher Pulte + Peter Sewell All rights reserved. +This software was developed by SRI International and the University of +Cambridge Computer Laboratory (Department of Computer Science and +Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and +under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA +SSITH research programme. + This software was developed by the above within the Rigorous Engineering of Mainstream Systems (REMS) project, partly funded by EPSRC grant EP/K008528/1, at the Universities of Cambridge and @@ -106,6 +106,16 @@ else C_FLAGS += -O2 endif +# Feature detect if we are on the latest development version of Sail +# and use an updated lem file if so. This is just until the opam +# version catches up with changes to the monad embedding. +SAIL_LATEST := $(shell $(SAIL) -emacs 1>&2 2> /dev/null; echo $$?) +ifeq ($(SAIL_LATEST),0) +RISCV_EXTRAS_LEM = riscv_extras.lem +else +RISCV_EXTRAS_LEM = 0.7.1/riscv_extras.lem +endif + all: ocaml_emulator/riscv_ocaml_sim c_emulator/riscv_sim riscv_isa riscv_coq riscv_hol riscv_rmem .PHONY: all @@ -185,9 +195,9 @@ generated_definitions/isabelle/ROOT: handwritten_support/ROOT generated_definitions/lem/riscv_duopod.lem: $(PRELUDE_SRCS) model/riscv_duopod.sail mkdir -p generated_definitions/lem $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ -generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv_duopod.lem handwritten_support/riscv_extras.lem +generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv_duopod.lem handwritten_support/$(RISCV_EXTRAS_LEM) lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/riscv_extras.lem \ + handwritten_support/$(RISCV_EXTRAS_LEM) \ generated_definitions/lem/riscv_duopod_types.lem \ generated_definitions/lem/riscv_duopod.lem @@ -213,9 +223,9 @@ generated_definitions/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/lem $(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) -generated_definitions/isabelle/Riscv.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv.lem handwritten_support/riscv_extras.lem Makefile +generated_definitions/isabelle/Riscv.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/riscv_extras.lem \ + handwritten_support/$(RISCV_EXTRAS_LEM) \ generated_definitions/lem/riscv_types.lem \ generated_definitions/lem/riscv.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/Riscv_types.thy @@ -224,10 +234,10 @@ generated_definitions/hol4/Holmakefile: handwritten_support/Holmakefile mkdir -p generated_definitions/hol4 cp handwritten_support/Holmakefile generated_definitions/hol4 -generated_definitions/hol4/riscvScript.sml: generated_definitions/hol4/Holmakefile generated_definitions/lem/riscv.lem handwritten_support/riscv_extras.lem +generated_definitions/hol4/riscvScript.sml: generated_definitions/hol4/Holmakefile generated_definitions/lem/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) lem -hol -outdir generated_definitions/hol4 -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \ - handwritten_support/riscv_extras.lem \ + handwritten_support/$(RISCV_EXTRAS_LEM) \ generated_definitions/lem/riscv_types.lem \ generated_definitions/lem/riscv.lem diff --git a/handwritten_support/0.7.1/riscv_extras.lem b/handwritten_support/0.7.1/riscv_extras.lem new file mode 100644 index 0000000..c1a52c9 --- /dev/null +++ b/handwritten_support/0.7.1/riscv_extras.lem @@ -0,0 +1,137 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +type bitvector 'a = mword 'a + +let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw +let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_r_r () = barrier Barrier_RISCV_r_r +let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w +let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r +let MEM_fence_tso () = barrier Barrier_RISCV_tso +let MEM_fence_i () = barrier Barrier_RISCV_i + +val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e + +let MEMea addr size = write_mem_ea Write_plain addr size +let MEMea_release addr size = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release addr size +let MEMea_conditional addr size = write_mem_ea Write_RISCV_conditional addr size +let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release addr size + = write_mem_ea Write_RISCV_conditional_strong_release addr size + +val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e + +let MEMr addrsize size hexRAM addr = read_mem Read_plain addr size +let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addr size +let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addr size +let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addr size +let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size + +val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +let write_ram addrsize size hexRAM address value = + write_mem_val value + +val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +let read_ram addrsize size hexRAM address = + read_mem Read_plain address size + +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success () = excl_result () + +let match_reservation _ = true +let cancel_reservation () = () + +val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_base () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_base = `Platform.dram_base` + +val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_size () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_size = `Platform.dram_size` + +val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_base () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_base = `Platform.rom_base` + +val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_size () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_size = `Platform.rom_size` + +val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_base () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_base = `Platform.clint_base` + +val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_size () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_size = `Platform.clint_size` + +val plat_enable_dirty_update : unit -> bool +let plat_enable_dirty_update () = false +declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update` + +val plat_enable_misaligned_access : unit -> bool +let plat_enable_misaligned_access () = false +declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` + +val plat_mtval_has_illegal_inst_bits : unit -> bool +let plat_mtval_has_illegal_inst_bits () = false +declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` + +val plat_insns_per_tick : unit -> integer +let plat_insns_per_tick () = 1 +declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick` + +val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a +let plat_htif_tohost () = wordFromInteger 0 +declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost` + +val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit +let plat_term_write _ = () +declare ocaml target_rep function plat_term_write = `Platform.term_write` + +val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a +let plat_term_read () = wordFromInteger 0 +declare ocaml target_rep function plat_term_read = `Platform.term_read` + +val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a +let shift_bits_right v m = shiftr v (uint m) +val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a +let shift_bits_left v m = shiftl v (uint m) + +val print_string : string -> string -> unit +let print_string msg s = () (* print_endline (msg ^ s) *) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) + +val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) diff --git a/handwritten_support/0.7.1/riscv_extras_sequential.lem b/handwritten_support/0.7.1/riscv_extras_sequential.lem new file mode 100644 index 0000000..c1a52c9 --- /dev/null +++ b/handwritten_support/0.7.1/riscv_extras_sequential.lem @@ -0,0 +1,137 @@ +open import Pervasives +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_operators_mwords +open import Sail2_prompt_monad +open import Sail2_prompt + +type bitvector 'a = mword 'a + +let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw +let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_r_r () = barrier Barrier_RISCV_r_r +let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w +let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r +let MEM_fence_tso () = barrier Barrier_RISCV_tso +let MEM_fence_i () = barrier Barrier_RISCV_i + +val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e + +let MEMea addr size = write_mem_ea Write_plain addr size +let MEMea_release addr size = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release addr size +let MEMea_conditional addr size = write_mem_ea Write_RISCV_conditional addr size +let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release addr size + = write_mem_ea Write_RISCV_conditional_strong_release addr size + +val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e + +let MEMr addrsize size hexRAM addr = read_mem Read_plain addr size +let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addr size +let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addr size +let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addr size +let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size + +val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +let write_ram addrsize size hexRAM address value = + write_mem_val value + +val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +let read_ram addrsize size hexRAM address = + read_mem Read_plain address size + +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success () = excl_result () + +let match_reservation _ = true +let cancel_reservation () = () + +val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_base () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_base = `Platform.dram_base` + +val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_ram_size () = wordFromInteger 0 +declare ocaml target_rep function plat_ram_size = `Platform.dram_size` + +val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_base () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_base = `Platform.rom_base` + +val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_rom_size () = wordFromInteger 0 +declare ocaml target_rep function plat_rom_size = `Platform.rom_size` + +val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_base () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_base = `Platform.clint_base` + +val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clint_size () = wordFromInteger 0 +declare ocaml target_rep function plat_clint_size = `Platform.clint_size` + +val plat_enable_dirty_update : unit -> bool +let plat_enable_dirty_update () = false +declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update` + +val plat_enable_misaligned_access : unit -> bool +let plat_enable_misaligned_access () = false +declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` + +val plat_mtval_has_illegal_inst_bits : unit -> bool +let plat_mtval_has_illegal_inst_bits () = false +declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` + +val plat_insns_per_tick : unit -> integer +let plat_insns_per_tick () = 1 +declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick` + +val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a +let plat_htif_tohost () = wordFromInteger 0 +declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost` + +val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit +let plat_term_write _ = () +declare ocaml target_rep function plat_term_write = `Platform.term_write` + +val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a +let plat_term_read () = wordFromInteger 0 +declare ocaml target_rep function plat_term_read = `Platform.term_read` + +val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a +let shift_bits_right v m = shiftr v (uint m) +val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a +let shift_bits_left v m = shiftl v (uint m) + +val print_string : string -> string -> unit +let print_string msg s = () (* print_endline (msg ^ s) *) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) + +val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index ed572be..2919d77 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -49,19 +49,15 @@ let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size -val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e - -let MEMw addrsize size hexRAM addr = write_mem Write_plain addr size -let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addr size -let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addr size -let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addr size -let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addr size -let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addr size +val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +let write_ram addrsize size hexRAM address value = + write_mem Write_plain address size value + +val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +let read_ram addrsize size hexRAM address = + read_mem Read_plain address size val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit let load_reservation addr = () diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index c1a52c9..2919d77 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -52,7 +52,7 @@ let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e let write_ram addrsize size hexRAM address value = - write_mem_val value + write_mem Write_plain address size value val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e diff --git a/model/prelude.sail b/model/prelude.sail index 8c047b9..1f180da 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -113,11 +113,19 @@ val print_reg = {ocaml: "Platform.print_reg", c: "print_reg", _: "print_e val print_mem = {ocaml: "Platform.print_mem_access", c: "print_mem_access", _: "print_endline"} : string -> unit val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", _: "print_endline"} : string -> unit +$ifndef FEATURE_IMPLICITS +val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) + +function EXTS v = sail_sign_extend(v, sizeof('m)) +function EXTZ v = sail_zero_extend(v, sizeof('m)) +$else val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) function EXTS(m, v) = sail_sign_extend(v, m) function EXTZ(m, v) = sail_zero_extend(v, m) +$endif val cast bool_to_bits : bool -> bits(1) function bool_to_bits x = if x then 0b1 else 0b0 |