From d7a3d8012fd579f40e53a29569141d72dd5e0c32 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 18 Nov 2023 00:16:49 +0000 Subject: [PATCH] lem: Fix issues created by vector extension Switch to bitlist representation because the machine words can't handle the vector code currently Remove RMEM target from default set of targets in Makefile. This is only interesting for RMEM maintainers. There's no reason for it to be generated by default, and it's also broken. While we are hacking on these files purge the duplicate versions for Sail 0.11+ --- Makefile | 14 +- handwritten_support/0.11/mem_metadata.lem | 16 -- handwritten_support/0.11/riscv_extras.lem | 172 -------------- .../0.11/riscv_extras_fdext.lem | 216 ------------------ .../0.11/riscv_extras_sequential.lem | 160 ------------- handwritten_support/mem_metadata.lem | 8 +- handwritten_support/riscv_extras.lem | 122 +++++----- handwritten_support/riscv_extras_fdext.lem | 140 +++++++----- 8 files changed, 149 insertions(+), 699 deletions(-) delete mode 100644 handwritten_support/0.11/mem_metadata.lem delete mode 100644 handwritten_support/0.11/riscv_extras.lem delete mode 100644 handwritten_support/0.11/riscv_extras_fdext.lem delete mode 100644 handwritten_support/0.11/riscv_extras_sequential.lem diff --git a/Makefile b/Makefile index 9f284ca24..923c6a3d0 100644 --- a/Makefile +++ b/Makefile @@ -187,15 +187,7 @@ C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl endif RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem -# 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 barrier type. -SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?) -ifeq ($(SAIL_LATEST),0) -RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES)) -else RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) -endif .PHONY: @@ -325,12 +317,12 @@ endif generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS) echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem # sed -i isn't posix compliant, unfortunately generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile - lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ + lem -wl ign -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem @@ -451,7 +443,7 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS) FORCE: -SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(sort $(wildcard handwritten_support/0.11/*.lem)) $(RMEM_FILES) +SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(RMEM_FILES) sail-riscv.install: FORCE echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem deleted file mode 100644 index 8a8c07014..000000000 --- a/handwritten_support/0.11/mem_metadata.lem +++ /dev/null @@ -1,16 +0,0 @@ -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 - -val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e -let write_ram wk addr width data meta = - write_mem wk () addr width data - -val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e -let read_ram rk addr width read_tag = - read_mem rk () addr width >>= (fun (data : mword 'n) -> - return (data, ())) diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem deleted file mode 100644 index 2509057e6..000000000 --- a/handwritten_support/0.11/riscv_extras.lem +++ /dev/null @@ -1,172 +0,0 @@ -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 addrsize addr size -let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addrsize addr size -let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addrsize addr size -let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addrsize addr size -let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addrsize addr size -let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize 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 addrsize addr size -let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addrsize addr size -let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addrsize addr size -let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addrsize addr size -let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addrsize addr size -let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr 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 sys_enable_writable_misa : unit -> bool -let sys_enable_writable_misa () = true -declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` - -val sys_enable_rvc : unit -> bool -let sys_enable_rvc () = true -declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` - -val sys_enable_next : unit -> bool -let sys_enable_next () = true -declare ocaml target_rep function sys_enable_next = `Platform.enable_next` - -val sys_enable_fdext : unit -> bool -let sys_enable_fdext () = true -declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext` - -val sys_enable_zfinx : unit -> bool -let sys_enable_zfinx () = false -declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx` - -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_enable_pmp : unit -> bool -let plat_enable_pmp () = false -declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` - -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 plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a -let plat_get_16_random_bits () = wordFromInteger 0 -declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits` - -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))) *) - -val print_dbg : string -> unit -let print_dbg msg = () diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem deleted file mode 100644 index e24a63d6a..000000000 --- a/handwritten_support/0.11/riscv_extras_fdext.lem +++ /dev/null @@ -1,216 +0,0 @@ -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 - -(* stub functions emulating the C softfloat interface *) - -val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f16_add _ _ _ = () - -val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f16_sub _ _ _ = () - -val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f16_mul _ _ _ = () - -val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f16_div _ _ _ = () - -val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f32_add _ _ _ = () - -val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f32_sub _ _ _ = () - -val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f32_mul _ _ _ = () - -val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f32_div _ _ _ = () - -val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f64_add _ _ _ = () - -val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f64_sub _ _ _ = () - -val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f64_mul _ _ _ = () - -val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit -let softfloat_f64_div _ _ _ = () - - -val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit -let softfloat_f16_muladd _ _ _ _ = () - -val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit -let softfloat_f32_muladd _ _ _ _ = () - -val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit -let softfloat_f64_muladd _ _ _ _ = () - - -val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_sqrt _ _ = () - -val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_sqrt _ _ = () - -val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_sqrt _ _ = () - - -val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_i32 _ _ = () - -val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_ui32 _ _ = () - -val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i32_to_f16 _ _ = () - -val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui32_to_f16 _ _ = () - -val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_i64 _ _ = () - -val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_ui64 _ _ = () - -val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i64_to_f16 _ _ = () - -val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui64_to_f16 _ _ = () - - -val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_i32 _ _ = () - -val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_ui32 _ _ = () - -val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i32_to_f32 _ _ = () - -val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui32_to_f32 _ _ = () - -val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_i64 _ _ = () - -val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_ui64 _ _ = () - -val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i64_to_f32 _ _ = () - -val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui64_to_f32 _ _ = () - - -val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_i32 _ _ = () - -val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_ui32 _ _ = () - -val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i32_to_f64 _ _ = () - -val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui32_to_f64 _ _ = () - -val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_i64 _ _ = () - -val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_ui64 _ _ = () - -val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_i64_to_f64 _ _ = () - -val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_ui64_to_f64 _ _ = () - - -val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_f32 _ _ = () - -val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f16_to_f64 _ _ = () - -val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_f64 _ _ = () - -val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f32_to_f16 _ _ = () - -val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_f16 _ _ = () - -val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit -let softfloat_f64_to_f32 _ _ = () - - -val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f16_lt _ _ = () - -val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f16_lt_quiet _ _ = () - -val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f16_le _ _ = () - -val softfloat_f16_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f16_le_quiet _ _ = () - -val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f16_eq _ _ = () - -val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f32_lt _ _ = () - -val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f32_lt_quiet _ _ = () - -val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f32_le _ _ = () - -val softfloat_f32_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f32_le_quiet _ _ = () - -val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f32_eq _ _ = () - -val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f64_lt _ _ = () - -val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f64_lt_quiet _ _ = () - -val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f64_le _ _ = () - -val softfloat_f64_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f64_le_quiet _ _ = () - -val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit -let softfloat_f64_eq _ _ = () - -val softfloat_f16_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit -let softfloat_f16_round_to_int _ _ _ = () - -val softfloat_f32_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit -let softfloat_f32_round_to_int _ _ _ = () - -val softfloat_f64_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit -let softfloat_f64_round_to_int _ _ _ = () diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem deleted file mode 100644 index 0c236515f..000000000 --- a/handwritten_support/0.11/riscv_extras_sequential.lem +++ /dev/null @@ -1,160 +0,0 @@ -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 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 = () - -let speculate_conditional_success () = excl_result () - -let match_reservation _ = true -let cancel_reservation () = () - -val sys_enable_writable_misa : unit -> bool -let sys_enable_writable_misa () = true -declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` - -val sys_enable_rvc : unit -> bool -let sys_enable_rvc () = true -declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` - -val sys_enable_zfinx : unit -> bool -let sys_enable_zfinx () = false -declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx` - -val sys_enable_next : unit -> bool -let sys_enable_next () = true -declare ocaml target_rep function sys_enable_next = `Platform.enable_next` - -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_enable_pmp : unit -> bool -let plat_enable_pmp () = false -declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` - -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))) *) - -val print_dbg : string -> unit -let print_dbg msg = () diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem index eadcadad6..6ea76911a 100644 --- a/handwritten_support/mem_metadata.lem +++ b/handwritten_support/mem_metadata.lem @@ -72,15 +72,15 @@ open import Pervasives open import Pervasives_extra open import Sail2_instr_kinds open import Sail2_values -open import Sail2_operators_mwords +open import Sail2_operators_bitlists open import Sail2_prompt_monad open import Sail2_prompt -val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e +val write_ram : forall 'rv 'e. write_kind -> list bitU -> integer -> list bitU -> unit -> monad 'rv bool 'e let write_ram wk addr width data meta = write_mem wk () addr width data -val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +val read_ram : forall 'rv 'e. read_kind -> list bitU -> integer -> bool -> monad 'rv (list bitU * unit) 'e let read_ram rk addr width read_tag = - read_mem rk () addr width >>= (fun (data : mword 'n) -> + read_mem rk () addr width >>= (fun data -> return (data, ())) diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 5f92ee904..bc04c2df5 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -72,30 +72,30 @@ open import Pervasives open import Pervasives_extra open import Sail2_instr_kinds open import Sail2_values -open import Sail2_operators_mwords +open import Sail2_operators_bitlists 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 +type bitvector = list Sail2_values.bitU + +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 'e. bitvector -> integer -> monad 'rv unit 'e +val MEMea_release : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e +val MEMea_strong_release : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e +val MEMea_conditional : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e +val MEMea_conditional_release : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e +val MEMea_conditional_strong_release : forall 'rv 'e. bitvector -> 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 @@ -103,14 +103,14 @@ let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_relea 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 + = 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 +val MEMr : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e let MEMr addrsize size hexRAM addr = read_mem Read_plain addrsize addr size let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addrsize addr size @@ -119,12 +119,12 @@ 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 addrsize addr size let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize 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 +val MEMw : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e +val MEMw_release : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e +val MEMw_strong_release : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e +val MEMw_conditional : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e +val MEMw_conditional_release : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e +val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e let MEMw addrsize size hexRAM addr = write_mem Write_plain addrsize addr size let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addrsize addr size @@ -133,7 +133,7 @@ let MEMw_conditional addrsize size hexRAM addr = write_mem Write_ let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addrsize addr size let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr size -val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +val load_reservation : bitvector -> unit let load_reservation addr = () let speculate_conditional_success () = excl_result () @@ -161,32 +161,36 @@ val sys_enable_zfinx : unit -> bool let sys_enable_zfinx () = false declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx` +val sys_enable_vext : unit -> bool +let sys_enable_vext () = true +declare ocaml target_rep function sys_enable_vext = `Platform.enable_vext` + val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` -val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a -let plat_ram_base () = wordFromInteger 0 +val plat_ram_base : unit -> bitvector +let plat_ram_base () = [] 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 +val plat_ram_size : unit -> bitvector +let plat_ram_size () = [] 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 +val plat_rom_base : unit -> bitvector +let plat_rom_base () = [] 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 +val plat_rom_size : unit -> bitvector +let plat_rom_size () = [] 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 +val plat_clint_base : unit -> bitvector +let plat_clint_base () = [] 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 +val plat_clint_size : unit -> bitvector +let plat_clint_size () = [] declare ocaml target_rep function plat_clint_size = `Platform.clint_size` val plat_enable_dirty_update : unit -> bool @@ -209,25 +213,25 @@ 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 +val plat_htif_tohost : unit -> bitvector +let plat_htif_tohost () = [] declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost` -val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit +val plat_term_write : bitvector -> 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 +val plat_term_read : unit -> bitvector +let plat_term_read () = [] declare ocaml target_rep function plat_term_read = `Platform.term_read` -val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a -let plat_get_16_random_bits () = wordFromInteger 0 +val plat_get_16_random_bits : unit -> bitvector +let plat_get_16_random_bits () = [] declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits` -val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a +val shift_bits_right : bitvector -> bitvector -> bitvector 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 +val shift_bits_left : bitvector -> bitvector -> bitvector let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit @@ -236,11 +240,11 @@ 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 +val prerr_bits : string -> bitvector -> 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))) *) +val print_bits : string -> bitvector -> unit +let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) val print_dbg : string -> unit let print_dbg msg = () diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem index 84e76ee47..81c6af504 100644 --- a/handwritten_support/riscv_extras_fdext.lem +++ b/handwritten_support/riscv_extras_fdext.lem @@ -76,193 +76,211 @@ open import Sail2_operators_mwords open import Sail2_prompt_monad open import Sail2_prompt -type bitvector 'a = mword 'a +type bitvector = list Sail2_values.bitU (* stub functions emulating the C softfloat interface *) -val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f16_round_to_int : bitvector -> bitvector -> bool -> unit +let softfloat_f16_round_to_int _ _ _ = () + +val softfloat_f32_round_to_int : bitvector -> bitvector -> bool -> unit +let softfloat_f32_round_to_int _ _ _ = () + +val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit +let softfloat_f64_round_to_int _ _ _ = () + +val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_add _ _ _ = () -val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f16_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_sub _ _ _ = () -val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f16_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_mul _ _ _ = () -val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f16_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_div _ _ _ = () -val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f32_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_add _ _ _ = () -val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f32_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_sub _ _ _ = () -val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f32_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_mul _ _ _ = () -val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f32_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_div _ _ _ = () -val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f64_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_add _ _ _ = () -val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f64_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_sub _ _ _ = () -val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f64_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_mul _ _ _ = () -val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit +val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_div _ _ _ = () -val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f16_muladd _ _ _ _ = () -val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +val softfloat_f32_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f32_muladd _ _ _ _ = () -val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit +val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f64_muladd _ _ _ _ = () -val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_sqrt : bitvector -> bitvector -> unit let softfloat_f16_sqrt _ _ = () -val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_sqrt : bitvector -> bitvector -> unit let softfloat_f32_sqrt _ _ = () -val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_sqrt : bitvector -> bitvector -> unit let softfloat_f64_sqrt _ _ = () -val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_i32: bitvector -> bitvector -> unit let softfloat_f16_to_i32 _ _ = () -val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_ui32: bitvector -> bitvector -> unit let softfloat_f16_to_ui32 _ _ = () -val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i32_to_f16: bitvector -> bitvector -> unit let softfloat_i32_to_f16 _ _ = () -val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui32_to_f16: bitvector -> bitvector -> unit let softfloat_ui32_to_f16 _ _ = () -val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_i64: bitvector -> bitvector -> unit let softfloat_f16_to_i64 _ _ = () -val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_ui64: bitvector -> bitvector -> unit let softfloat_f16_to_ui64 _ _ = () -val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i64_to_f16: bitvector -> bitvector -> unit let softfloat_i64_to_f16 _ _ = () -val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui64_to_f16: bitvector -> bitvector -> unit let softfloat_ui64_to_f16 _ _ = () -val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_i32: bitvector -> bitvector -> unit let softfloat_f32_to_i32 _ _ = () -val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_ui32: bitvector -> bitvector -> unit let softfloat_f32_to_ui32 _ _ = () -val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i32_to_f32: bitvector -> bitvector -> unit let softfloat_i32_to_f32 _ _ = () -val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui32_to_f32: bitvector -> bitvector -> unit let softfloat_ui32_to_f32 _ _ = () -val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_i64: bitvector -> bitvector -> unit let softfloat_f32_to_i64 _ _ = () -val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_ui64: bitvector -> bitvector -> unit let softfloat_f32_to_ui64 _ _ = () -val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i64_to_f32: bitvector -> bitvector -> unit let softfloat_i64_to_f32 _ _ = () -val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui64_to_f32: bitvector -> bitvector -> unit let softfloat_ui64_to_f32 _ _ = () -val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_i32: bitvector -> bitvector -> unit let softfloat_f64_to_i32 _ _ = () -val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_ui32: bitvector -> bitvector -> unit let softfloat_f64_to_ui32 _ _ = () -val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i32_to_f64: bitvector -> bitvector -> unit let softfloat_i32_to_f64 _ _ = () -val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui32_to_f64: bitvector -> bitvector -> unit let softfloat_ui32_to_f64 _ _ = () -val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_i64: bitvector -> bitvector -> unit let softfloat_f64_to_i64 _ _ = () -val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_ui64: bitvector -> bitvector -> unit let softfloat_f64_to_ui64 _ _ = () -val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_i64_to_f64: bitvector -> bitvector -> unit let softfloat_i64_to_f64 _ _ = () -val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_ui64_to_f64: bitvector -> bitvector -> unit let softfloat_ui64_to_f64 _ _ = () -val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_f32: bitvector -> bitvector -> unit let softfloat_f16_to_f32 _ _ = () -val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f16_to_f64: bitvector -> bitvector -> unit let softfloat_f16_to_f64 _ _ = () -val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_f64: bitvector -> bitvector -> unit let softfloat_f32_to_f64 _ _ = () -val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f32_to_f16: bitvector -> bitvector -> unit let softfloat_f32_to_f16 _ _ = () -val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_f16: bitvector -> bitvector -> unit let softfloat_f64_to_f16 _ _ = () -val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +val softfloat_f64_to_f32: bitvector -> bitvector -> unit let softfloat_f64_to_f32 _ _ = () -val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f16_lt : bitvector -> bitvector -> unit let softfloat_f16_lt _ _ = () -val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f16_lt_quiet : bitvector -> bitvector -> unit let softfloat_f16_lt_quiet _ _ = () -val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f16_le : bitvector -> bitvector -> unit let softfloat_f16_le _ _ = () -val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f16_le_quiet : bitvector -> bitvector -> unit +let softfloat_f16_le_quiet _ _ = () + +val softfloat_f16_eq : bitvector -> bitvector -> unit let softfloat_f16_eq _ _ = () -val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f32_lt : bitvector -> bitvector -> unit let softfloat_f32_lt _ _ = () -val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f32_lt_quiet : bitvector -> bitvector -> unit let softfloat_f32_lt_quiet _ _ = () -val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f32_le : bitvector -> bitvector -> unit let softfloat_f32_le _ _ = () -val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f32_le_quiet : bitvector -> bitvector -> unit +let softfloat_f32_le_quiet _ _ = () + +val softfloat_f32_eq : bitvector -> bitvector -> unit let softfloat_f32_eq _ _ = () -val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f64_lt : bitvector -> bitvector -> unit let softfloat_f64_lt _ _ = () -val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f64_lt_quiet : bitvector -> bitvector -> unit let softfloat_f64_lt_quiet _ _ = () -val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f64_le : bitvector -> bitvector -> unit let softfloat_f64_le _ _ = () -val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +val softfloat_f64_le_quiet : bitvector -> bitvector -> unit +let softfloat_f64_le_quiet _ _ = () + +val softfloat_f64_eq : bitvector -> bitvector -> unit let softfloat_f64_eq _ _ = ()