diff options
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/0.11/mem_metadata.lem | 16 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras.lem | 172 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras_fdext.lem | 216 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras_sequential.lem | 160 | ||||
| -rw-r--r-- | handwritten_support/mem_metadata.lem | 8 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 126 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_fdext.lem | 140 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 4 |
8 files changed, 146 insertions, 696 deletions
diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem deleted file mode 100644 index 8a8c070..0000000 --- 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 2509057..0000000 --- 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 e24a63d..0000000 --- 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 0c23651..0000000 --- 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 eadcada..6ea7691 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 5f92ee9..27e8ee5 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 @@ -197,10 +201,6 @@ 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` @@ -209,25 +209,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 +236,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 84e76ee..81c6af5 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 _ _ = () diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 102d082..d113908 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -189,10 +189,6 @@ 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` |