From 663e24a3d8f45b4b184b3a4bc3a57bc0f3d6cd78 Mon Sep 17 00:00:00 2001 From: Aditya Naik Date: Fri, 27 Aug 2021 13:07:37 -0400 Subject: Initial; working SAIL RISC-V regs The register definition along with read/write functions for registers are lowered to Coq. The FIRRTL annotation does not work as expected. --- handwritten_support/.mem_metadata.aux | 3 + handwritten_support/.riscv_extras.aux | 23 + handwritten_support/0.11/mem_metadata.lem | 16 + handwritten_support/0.11/riscv_extras.lem | 164 ++++ handwritten_support/0.11/riscv_extras_fdext.lem | 125 +++ .../0.11/riscv_extras_sequential.lem | 156 ++++ handwritten_support/Holmakefile | 13 + handwritten_support/ROOT | 9 + handwritten_support/hgen/ast.hgen | 22 + handwritten_support/hgen/fold.hgen | 21 + .../hgen/herdtools_ast_to_shallow_ast.hgen | 91 +++ .../hgen/herdtools_types_to_shallow_types.hgen | 90 +++ handwritten_support/hgen/lexer.hgen | 63 ++ handwritten_support/hgen/lexer_regexps.hgen | 131 +++ handwritten_support/hgen/map.hgen | 21 + handwritten_support/hgen/parser.hgen | 76 ++ handwritten_support/hgen/pretty.hgen | 36 + handwritten_support/hgen/pretty_xml.hgen | 143 ++++ handwritten_support/hgen/sail_trans_out.hgen | 27 + .../hgen/shallow_ast_to_herdtools_ast.hgen | 26 + .../hgen/shallow_types_to_herdtools_types.hgen | 87 ++ handwritten_support/hgen/token_types.hgen | 24 + handwritten_support/hgen/tokens.hgen | 20 + handwritten_support/hgen/trans_sail.hgen | 162 ++++ handwritten_support/hgen/types.hgen | 172 ++++ handwritten_support/hgen/types_sail_trans_out.hgen | 98 +++ handwritten_support/hgen/types_trans_sail.hgen | 57 ++ handwritten_support/mem_metadata.glob | 64 ++ handwritten_support/mem_metadata.lem | 16 + handwritten_support/mem_metadata.v | 8 + handwritten_support/mem_metadata.vo | Bin 0 -> 25483 bytes handwritten_support/mem_metadata.vok | 0 handwritten_support/mem_metadata.vos | 0 handwritten_support/riscv_extras.glob | 875 +++++++++++++++++++++ handwritten_support/riscv_extras.lem | 164 ++++ handwritten_support/riscv_extras.v | 154 ++++ handwritten_support/riscv_extras.vo | Bin 0 -> 67854 bytes handwritten_support/riscv_extras.vok | 0 handwritten_support/riscv_extras.vos | 0 handwritten_support/riscv_extras_fdext.lem | 125 +++ handwritten_support/riscv_extras_sequential.lem | 156 ++++ 41 files changed, 3438 insertions(+) create mode 100644 handwritten_support/.mem_metadata.aux create mode 100644 handwritten_support/.riscv_extras.aux create mode 100644 handwritten_support/0.11/mem_metadata.lem create mode 100644 handwritten_support/0.11/riscv_extras.lem create mode 100644 handwritten_support/0.11/riscv_extras_fdext.lem create mode 100644 handwritten_support/0.11/riscv_extras_sequential.lem create mode 100644 handwritten_support/Holmakefile create mode 100644 handwritten_support/ROOT create mode 100644 handwritten_support/hgen/ast.hgen create mode 100644 handwritten_support/hgen/fold.hgen create mode 100644 handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen create mode 100644 handwritten_support/hgen/herdtools_types_to_shallow_types.hgen create mode 100644 handwritten_support/hgen/lexer.hgen create mode 100644 handwritten_support/hgen/lexer_regexps.hgen create mode 100644 handwritten_support/hgen/map.hgen create mode 100644 handwritten_support/hgen/parser.hgen create mode 100644 handwritten_support/hgen/pretty.hgen create mode 100644 handwritten_support/hgen/pretty_xml.hgen create mode 100644 handwritten_support/hgen/sail_trans_out.hgen create mode 100644 handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen create mode 100644 handwritten_support/hgen/shallow_types_to_herdtools_types.hgen create mode 100644 handwritten_support/hgen/token_types.hgen create mode 100644 handwritten_support/hgen/tokens.hgen create mode 100644 handwritten_support/hgen/trans_sail.hgen create mode 100644 handwritten_support/hgen/types.hgen create mode 100644 handwritten_support/hgen/types_sail_trans_out.hgen create mode 100644 handwritten_support/hgen/types_trans_sail.hgen create mode 100644 handwritten_support/mem_metadata.glob create mode 100644 handwritten_support/mem_metadata.lem create mode 100644 handwritten_support/mem_metadata.v create mode 100644 handwritten_support/mem_metadata.vo create mode 100644 handwritten_support/mem_metadata.vok create mode 100644 handwritten_support/mem_metadata.vos create mode 100644 handwritten_support/riscv_extras.glob create mode 100644 handwritten_support/riscv_extras.lem create mode 100644 handwritten_support/riscv_extras.v create mode 100644 handwritten_support/riscv_extras.vo create mode 100644 handwritten_support/riscv_extras.vok create mode 100644 handwritten_support/riscv_extras.vos create mode 100644 handwritten_support/riscv_extras_fdext.lem create mode 100644 handwritten_support/riscv_extras_sequential.lem (limited to 'handwritten_support') diff --git a/handwritten_support/.mem_metadata.aux b/handwritten_support/.mem_metadata.aux new file mode 100644 index 0000000..cfce1c3 --- /dev/null +++ b/handwritten_support/.mem_metadata.aux @@ -0,0 +1,3 @@ +COQAUX1 693b57d74f776ae8bd215fbfc8b03df3 /home/aditya/dev/firrtl-proof/sail-riscv/handwritten_support/mem_metadata.v +183 386 context_used "" +0 0 vo_compile_time "0.304" diff --git a/handwritten_support/.riscv_extras.aux b/handwritten_support/.riscv_extras.aux new file mode 100644 index 0000000..d53d7e5 --- /dev/null +++ b/handwritten_support/.riscv_extras.aux @@ -0,0 +1,23 @@ +COQAUX1 9f6e940694efb436e57a7a26d0b1b3b3 /home/aditya/dev/firrtl-proof/sail-riscv/handwritten_support/riscv_extras.v +3801 3993 context_used "" +3994 4194 context_used "" +4195 4402 context_used "" +4403 4604 context_used "" +4605 4814 context_used "" +4815 5031 context_used "" +7223 7331 context_used "" +7333 7442 context_used "" +7444 7565 context_used "" +8744 8878 context_used "" +9948 9983 context_used "" +10049 10053 proof_build_time "0.017" +0 0 euclid_modulo "0.017" +10005 10048 context_used "" +10049 10053 proof_check_time "0.004" +10096 10182 context_used "" +10183 10267 context_used "" +11004 11008 proof_build_time "0.001" +0 0 n_leading_spaces_fact "0.001" +10997 11003 context_used "" +11004 11008 proof_check_time "0.001" +0 0 vo_compile_time "0.514" diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem new file mode 100644 index 0000000..8a8c070 --- /dev/null +++ b/handwritten_support/0.11/mem_metadata.lem @@ -0,0 +1,16 @@ +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 new file mode 100644 index 0000000..db93001 --- /dev/null +++ b/handwritten_support/0.11/riscv_extras.lem @@ -0,0 +1,164 @@ +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 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/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem new file mode 100644 index 0000000..12cfe00 --- /dev/null +++ b/handwritten_support/0.11/riscv_extras_fdext.lem @@ -0,0 +1,125 @@ +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_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_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_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_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_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_f64 _ _ = () + +val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_f32 _ _ = () + + +val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_lt _ _ = () + +val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_le _ _ = () + +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_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_le _ _ = () + +val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_eq _ _ = () diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem new file mode 100644 index 0000000..827f601 --- /dev/null +++ b/handwritten_support/0.11/riscv_extras_sequential.lem @@ -0,0 +1,156 @@ +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_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/Holmakefile b/handwritten_support/Holmakefile new file mode 100644 index 0000000..dd483e9 --- /dev/null +++ b/handwritten_support/Holmakefile @@ -0,0 +1,13 @@ +INCLUDES = $(LEM_DIR)/hol-lib $(SAIL_LIB_DIR)/hol + +SCRIPTS = riscv_extrasScript.sml riscv_typesScript.sml riscvScript.sml + +THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) + +all: $(THYS) +.PHONY: all + +ifdef POLY +BASE_HEAP = $(SAIL_LIB_DIR)/hol/sail-heap + +endif diff --git a/handwritten_support/ROOT b/handwritten_support/ROOT new file mode 100644 index 0000000..281bd26 --- /dev/null +++ b/handwritten_support/ROOT @@ -0,0 +1,9 @@ +session "Sail-RISC-V" = "Sail" + + options [document = false] + theories + "Riscv_lemmas" + +session "Sail-RISC-V-Duopod" = "Sail" + + options [document = false] + theories + "Riscv_duopod_lemmas" diff --git a/handwritten_support/hgen/ast.hgen b/handwritten_support/hgen/ast.hgen new file mode 100644 index 0000000..25d19a4 --- /dev/null +++ b/handwritten_support/hgen/ast.hgen @@ -0,0 +1,22 @@ +| `RISCVStopFetching (* this is a special instruction used by rmem to + indicate the end of a litmus thread *) +| `RISCVThreadStart (* this instruction indicates a thread creation in ELF files *) + +| `RISCVUTYPE of bit20 * reg * riscvUop +| `RISCVJAL of bit20 * reg +| `RISCVJALR of bit12 * reg * reg +| `RISCVBType of bit12 * reg * reg * riscvBop +| `RISCVIType of bit12 * reg * reg * riscvIop +| `RISCVShiftIop of bit6 * reg * reg * riscvSop +| `RISCVRType of reg * reg * reg * riscvRop +| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool +| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool +| `RISCVADDIW of bit12 * reg * reg +| `RISCVSHIFTW of bit5 * reg * reg * riscvSop +| `RISCVRTYPEW of reg * reg * reg * riscvRopw +| `RISCVFENCE of bit4 * bit4 +| `RISCVFENCE_TSO of bit4 * bit4 +| `RISCVFENCEI +| `RISCVLoadRes of bool * bool * reg * wordWidth * reg +| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg +| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg diff --git a/handwritten_support/hgen/fold.hgen b/handwritten_support/hgen/fold.hgen new file mode 100644 index 0000000..7f9d05c --- /dev/null +++ b/handwritten_support/hgen/fold.hgen @@ -0,0 +1,21 @@ +| `RISCVThreadStart -> (y_reg, y_sreg) +| `RISCVStopFetching -> (y_reg, y_sreg) + +| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVLoad (_, r0, r1, _, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVStore (_, r0, r1, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVFENCE (_, _) -> (y_reg, y_sreg) +| `RISCVFENCE_TSO (_, _) -> (y_reg, y_sreg) +| `RISCVFENCEI -> (y_reg, y_sreg) +| `RISCVLoadRes (_, _, rs1, _, rd) -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg)) +| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) +| `RISCVAMO (_, _, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) diff --git a/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen b/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen new file mode 100644 index 0000000..2ebef02 --- /dev/null +++ b/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen @@ -0,0 +1,91 @@ +| `RISCVThreadStart -> THREAD_START() +| `RISCVStopFetching -> STOP_FETCHING() + +| `RISCVUTYPE(imm, rd, op) -> UTYPE( + translate_imm20 "imm" imm, + translate_reg "rd" rd, + translate_uop op) +| `RISCVJAL(imm, rd) -> RISCV_JAL( + translate_imm21 "imm" imm, + translate_reg "rd" rd) +| `RISCVJALR(imm, rs, rd) -> RISCV_JALR( + translate_imm12 "imm" imm, + translate_reg "rs" rd, + translate_reg "rd" rd) +| `RISCVBType(imm, rs2, rs1, op) -> BTYPE( + translate_imm13 "imm" imm, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_bop op) +| `RISCVIType(imm, rs1, rd, op) -> ITYPE( + translate_imm12 "imm" imm, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_iop op) +| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP( + translate_imm6 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd, + translate_sop op) +| `RISCVRType (rs2, rs1, rd, op) -> RTYPE ( + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_rop op) +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD( + translate_imm12 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd, + translate_bool "unsigned" unsigned, + translate_wordWidth width, + translate_bool "aq" aq, + translate_bool "rl" rl) +| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE ( + translate_imm12 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd, + translate_wordWidth width, + translate_bool "aq" aq, + translate_bool "rl" rl) +| `RISCVADDIW(imm, rs, rd) -> ADDIW( + translate_imm12 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd) +| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW( + translate_imm5 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd, + translate_sop op) +| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW( + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_ropw op) +| `RISCVFENCE(pred, succ) -> FENCE( + translate_imm4 "pred" pred, + translate_imm4 "succ" succ) +| `RISCVFENCE_TSO(pred, succ) -> FENCE_TSO( + translate_imm4 "pred" pred, + translate_imm4 "succ" succ) +| `RISCVFENCEI -> FENCEI () +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES( + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON( + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) +| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO( + translate_amoop op, + translate_bool "aq" aq, + translate_bool "rl" rl, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_wordWidth width, + translate_reg "rd" rd) diff --git a/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen b/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen new file mode 100644 index 0000000..8bd311b --- /dev/null +++ b/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen @@ -0,0 +1,90 @@ +let is_inc = false + +let translate_reg name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int (reg_to_int value)) + +let translate_uop op = match op with + | RISCVLUI -> RISCV_LUI + | RISCVAUIPC -> RISCV_AUIPC + +let translate_bop op = match op with + | RISCVBEQ -> RISCV_BEQ + | RISCVBNE -> RISCV_BNE + | RISCVBLT -> RISCV_BLT + | RISCVBGE -> RISCV_BGE + | RISCVBLTU -> RISCV_BLTU + | RISCVBGEU -> RISCV_BGEU + +let translate_iop op = match op with + | RISCVADDI -> RISCV_ADDI + | RISCVSLTI -> RISCV_SLTI + | RISCVSLTIU -> RISCV_SLTIU + | RISCVXORI -> RISCV_XORI + | RISCVORI -> RISCV_ORI + | RISCVANDI -> RISCV_ANDI + +let translate_sop op = match op with + | RISCVSLLI -> RISCV_SLLI + | RISCVSRLI -> RISCV_SRLI + | RISCVSRAI -> RISCV_SRAI + +let translate_rop op = match op with + | RISCVADD -> RISCV_ADD + | RISCVSUB -> RISCV_SUB + | RISCVSLL -> RISCV_SLL + | RISCVSLT -> RISCV_SLT + | RISCVSLTU -> RISCV_SLTU + | RISCVXOR -> RISCV_XOR + | RISCVSRL -> RISCV_SRL + | RISCVSRA -> RISCV_SRA + | RISCVOR -> RISCV_OR + | RISCVAND -> RISCV_AND + +let translate_ropw op = match op with + | RISCVADDW -> RISCV_ADDW + | RISCVSUBW -> RISCV_SUBW + | RISCVSLLW -> RISCV_SLLW + | RISCVSRLW -> RISCV_SRLW + | RISCVSRAW -> RISCV_SRAW + +let translate_amoop op = match op with + | RISCVAMOSWAP -> AMOSWAP + | RISCVAMOADD -> AMOADD + | RISCVAMOXOR -> AMOXOR + | RISCVAMOAND -> AMOAND + | RISCVAMOOR -> AMOOR + | RISCVAMOMIN -> AMOMIN + | RISCVAMOMAX -> AMOMAX + | RISCVAMOMINU -> AMOMINU + | RISCVAMOMAXU -> AMOMAXU + +let translate_wordWidth op = match op with + | RISCVBYTE -> BYTE + | RISCVHALF -> HALF + | RISCVWORD -> WORD + | RISCVDOUBLE -> DOUBLE + +let translate_bool name b = b (* function + * | true -> trueSail2_values.B10 + * | false -> false Sail2_values.B00 *) + +let translate_imm21 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty21_dict (Nat_big_num.of_int value) + +let translate_imm20 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty20_dict (Nat_big_num.of_int value) + +let translate_imm13 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty13_dict (Nat_big_num.of_int value) + +let translate_imm12 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty12_dict (Nat_big_num.of_int value) + +let translate_imm6 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty6_dict (Nat_big_num.of_int value) + +let translate_imm5 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int value) + +let translate_imm4 name value = + Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty4_dict (Nat_big_num.of_int value) diff --git a/handwritten_support/hgen/lexer.hgen b/handwritten_support/hgen/lexer.hgen new file mode 100644 index 0000000..9009f33 --- /dev/null +++ b/handwritten_support/hgen/lexer.hgen @@ -0,0 +1,63 @@ +(** RV32I (and RV64I) ***********************************************) +"lui" , UTYPE { op=RISCVLUI }; +"auipc" , UTYPE { op=RISCVAUIPC }; + +"jal", JAL (); +"jalr", JALR (); + +"beq", BTYPE {op=RISCVBEQ}; +"bne", BTYPE {op=RISCVBNE}; +"blt", BTYPE {op=RISCVBLT}; +"bge", BTYPE {op=RISCVBGE}; +"bltu", BTYPE {op=RISCVBLTU}; +"bgeu", BTYPE {op=RISCVBGEU}; + +"addi", ITYPE {op=RISCVADDI}; +"stli", ITYPE {op=RISCVSLTI}; +"sltiu", ITYPE {op=RISCVSLTIU}; +"xori", ITYPE {op=RISCVXORI}; +"ori", ITYPE {op=RISCVORI}; +"andi", ITYPE {op=RISCVANDI}; + +"add", RTYPE {op=RISCVADD}; +"sub", RTYPE {op=RISCVSUB}; +"sll", RTYPE {op=RISCVSLL}; +"slt", RTYPE {op=RISCVSLT}; +"sltu", RTYPE {op=RISCVSLT}; +"xor", RTYPE {op=RISCVXOR}; +"srl", RTYPE {op=RISCVSRL}; +"sra", RTYPE {op=RISCVSRA}; +"or", RTYPE {op=RISCVOR}; +"and", RTYPE {op=RISCVAND}; + +"fence", FENCE (); +"fence.tso", FENCETSO (); +"fence.i", FENCEI (); + +(** RV64I (in addition to RV32I) ************************************) + +"addiw", ADDIW (); + +"addw", RTYPEW {op=RISCVADDW}; +"subw", RTYPEW {op=RISCVSUBW}; +"sllw", RTYPEW {op=RISCVSLLW}; +"srlw", RTYPEW {op=RISCVSRLW}; +"sraw", RTYPEW {op=RISCVSRAW}; + +"slli", SHIFTIOP {op=RISCVSLLI}; +"srli", SHIFTIOP {op=RISCVSRLI}; +"srai", SHIFTIOP {op=RISCVSRAI}; + +"slliw", SHIFTW {op=RISCVSLLI}; +"srliw", SHIFTW {op=RISCVSRLI}; +"sraiw", SHIFTW {op=RISCVSRAI}; + +(** RV32A (and RV64A) ***********************************************) + +"r", FENCEOPTION Fence_R; +"w", FENCEOPTION Fence_W; +"rw", FENCEOPTION Fence_RW; + +(** pseudo instructions *********************************************) + +"li", LI () diff --git a/handwritten_support/hgen/lexer_regexps.hgen b/handwritten_support/hgen/lexer_regexps.hgen new file mode 100644 index 0000000..b8f3ca6 --- /dev/null +++ b/handwritten_support/hgen/lexer_regexps.hgen @@ -0,0 +1,131 @@ +(** RV32I (and RV64I) ***********************************************) + +| 'l' (('b'|'h') as width) ("u"? as u) (".aq"? as aq) (".rl"? as rl) as load + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else + LOAD { width = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | _ -> failwith "bad width"); + unsigned = (u = "u"); + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "lw" (".aq"? as aq) (".rl"? as rl) as load + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else + LOAD { width = RISCVWORD; + unsigned = false; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| 's' (('b'|'h'|'w') as width) (".aq"? as aq) (".rl"? as rl) as store + { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else + STORE { width = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | 'w' -> RISCVWORD | _ -> failwith "bad width"); + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +(** RV64I (in addition to RV32I) ************************************) + +| "lwu" (".aq"? as aq) (".rl"? as rl) as load + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else + LOAD { width = RISCVWORD; + unsigned = true; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "ld" (".aq"? as aq) (".rl"? as rl) as load + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else + LOAD { width = RISCVDOUBLE; + unsigned = false; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "sd" (".aq"? as aq) (".rl"? as rl) as store + { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else + STORE { width = RISCVDOUBLE; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +(** RV32A (and RV64A) ***********************************************) + +| "lr.w" (".aq"? as aq) (".rl"? as rl) as lr + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else + LOADRES { width = RISCVWORD; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "sc.w" (".aq"? as aq) (".rl"? as rl) as sc + { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else + STORECON { width = RISCVWORD; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".w" (".aq"? as aq) (".rl"? as rl) + { AMO { op = + begin match op with + | "swap" -> RISCVAMOSWAP; + | "add" -> RISCVAMOADD; + | "and" -> RISCVAMOAND; + | "or" -> RISCVAMOOR; + | "xor" -> RISCVAMOXOR; + | "max" -> RISCVAMOMAX; + | "min" -> RISCVAMOMIN; + | "maxu" -> RISCVAMOMAXU; + | "minu" -> RISCVAMOMINU; + | _ -> failwith "bad amo" + end; + width = RISCVWORD; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +(** RV64A (in addition to RV32A) ************************************) + +| "lr.d" (".aq"? as aq) (".rl"? as rl) as lr + { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else + LOADRES { width = RISCVDOUBLE; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "sc.d" (".aq"? as aq) (".rl"? as rl) as sc + { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else + STORECON { width = RISCVDOUBLE; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } + +| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".d" (".aq"? as aq) (".rl"? as rl) + { AMO { op = + begin match op with + | "swap" -> RISCVAMOSWAP; + | "add" -> RISCVAMOADD; + | "and" -> RISCVAMOAND; + | "or" -> RISCVAMOOR; + | "xor" -> RISCVAMOXOR; + | "max" -> RISCVAMOMAX; + | "min" -> RISCVAMOMIN; + | "maxu" -> RISCVAMOMAXU; + | "minu" -> RISCVAMOMINU; + | _ -> failwith "bad amo" + end; + width = RISCVDOUBLE; + aq = (aq = ".aq"); + rl = (rl = ".rl"); + } + } diff --git a/handwritten_support/hgen/map.hgen b/handwritten_support/hgen/map.hgen new file mode 100644 index 0000000..aa3882e --- /dev/null +++ b/handwritten_support/hgen/map.hgen @@ -0,0 +1,21 @@ +| `RISCVThreadStart -> `RISCVThreadStart +| `RISCVStopFetching -> `RISCVStopFetching + +| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) +| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) +| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) +| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) +| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y) +| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y) +| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y) +| `RISCVLoad (x, r0, r1, y, z, a, b) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b) +| `RISCVStore (x, r0, r1, y, z, a) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a) +| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1) +| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y) +| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) +| `RISCVFENCE (p, s) -> `RISCVFENCE (p, s) +| `RISCVFENCE_TSO (p, s) -> `RISCVFENCE_TSO (p, s) +| `RISCVFENCEI -> `RISCVFENCEI +| `RISCVLoadRes (aq, rl, rs1, w, rd) -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd) +| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) +| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd) -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) diff --git a/handwritten_support/hgen/parser.hgen b/handwritten_support/hgen/parser.hgen new file mode 100644 index 0000000..a4d5c07 --- /dev/null +++ b/handwritten_support/hgen/parser.hgen @@ -0,0 +1,76 @@ +| UTYPE reg COMMA NUM + { (* it's not clear if NUM here should be before or after filling the + lowest 12 bits with zeros, or if it should be signed or unsigned; + currently assuming: NUM does not include the 12 zeros, and is unsigned *) + if not (iskbituimm 20 $4) then failwith "immediate is not 20bit" + else `RISCVUTYPE ($4, $2, $1.op) } +| JAL reg COMMA NUM + { if not ($4 mod 2 = 0) then failwith "odd offset" + else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit" + else `RISCVJAL ($4, $2) } +| JALR reg COMMA reg COMMA NUM + { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit" + else `RISCVJALR ($6, $4, $2) } +| BTYPE reg COMMA reg COMMA NUM + { if not ($6 mod 2 = 0) then failwith "odd offset" + else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit" + else `RISCVBType ($6, $4, $2, $1.op) } +| ITYPE reg COMMA reg COMMA NUM + { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" + else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit" + else `RISCVIType ($6, $4, $2, $1.op) } +| ADDIW reg COMMA reg COMMA NUM + { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" + else `RISCVADDIW ($6, $4, $2) } +| SHIFTIOP reg COMMA reg COMMA NUM + { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit" + else `RISCVShiftIop ($6, $4, $2, $1.op) } +| SHIFTW reg COMMA reg COMMA NUM + { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit" + else `RISCVSHIFTW ($6, $4, $2, $1.op) } +| RTYPE reg COMMA reg COMMA reg + { `RISCVRType ($6, $4, $2, $1.op) } +| LOAD reg COMMA NUM LPAR reg RPAR + { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" + else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) } +| STORE reg COMMA NUM LPAR reg RPAR + { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" + else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) } +| RTYPEW reg COMMA reg COMMA reg + { `RISCVRTYPEW ($6, $4, $2, $1.op) } +| FENCE FENCEOPTION COMMA FENCEOPTION + { match ($2, $4) with + | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011) + | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011) + | (Fence_W, Fence_RW) -> `RISCVFENCE (0b0001, 0b0011) + | (Fence_RW, Fence_R) -> `RISCVFENCE (0b0011, 0b0010) + | (Fence_R, Fence_R) -> `RISCVFENCE (0b0010, 0b0010) + | (Fence_W, Fence_R) -> `RISCVFENCE (0b0001, 0b0010) + | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001) + | (Fence_R, Fence_W) -> `RISCVFENCE (0b0010, 0b0001) + | (Fence_W, Fence_W) -> `RISCVFENCE (0b0001, 0b0001) + } +| FENCETSO + { `RISCVFENCE_TSO (0b0011, 0b0011) } +| FENCEI + { `RISCVFENCEI } +| LOADRES reg COMMA LPAR reg RPAR + { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) } +| LOADRES reg COMMA NUM LPAR reg RPAR + { if $4 <> 0 then failwith "'lr' offset must be 0" else + `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) } +| STORECON reg COMMA reg COMMA LPAR reg RPAR + { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) } +| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR + { if $6 <> 0 then failwith "'sc' offset must be 0" else + `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) } +| AMO reg COMMA reg COMMA LPAR reg RPAR + { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) } +| AMO reg COMMA reg COMMA NUM LPAR reg RPAR + { if $6 <> 0 then failwith "'amo' offset must be 0" else + `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) } + +/* pseudo-ops */ +| LI reg COMMA NUM + { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)" + else `RISCVIType ($4, IReg R0, $2, RISCVORI) } diff --git a/handwritten_support/hgen/pretty.hgen b/handwritten_support/hgen/pretty.hgen new file mode 100644 index 0000000..3e6e6d1 --- /dev/null +++ b/handwritten_support/hgen/pretty.hgen @@ -0,0 +1,36 @@ +| `RISCVThreadStart -> "start" +| `RISCVStopFetching -> "stop" + +| `RISCVUTYPE(imm, rd, op) -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm +| `RISCVJAL(imm, rd) -> sprintf "jal %s, %d" (pp_reg rd) imm +| `RISCVJALR(imm, rs, rd) -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm +| `RISCVBType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm +| `RISCVIType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm +| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm +| `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) + +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs) + +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (pp_reg rs2) imm (pp_reg rs1) + +| `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm +| `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm +| `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) + +| `RISCVFENCE(pred, succ) -> sprintf "fence %s,%s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ) + +| `RISCVFENCE_TSO(0b0011, 0b0011) -> sprintf "fence.tso" +| `RISCVFENCE_TSO(_, _) -> failwith "bad fence.tso" + +| `RISCVFENCEI -> sprintf "fence.i" + +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1) + +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) + +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) diff --git a/handwritten_support/hgen/pretty_xml.hgen b/handwritten_support/hgen/pretty_xml.hgen new file mode 100644 index 0000000..be080cd --- /dev/null +++ b/handwritten_support/hgen/pretty_xml.hgen @@ -0,0 +1,143 @@ +| `RISCVThreadStart -> ("op_thread_start", []) + +| `RISCVStopFetching -> ("op_stop_fetching", []) + +| `RISCVUTYPE(imm, rd, op) -> + ("op_U_type", + [ ("op", pp_riscv_uop op); + ("uimm", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVJAL(imm, rd) -> + ("op_jal", + [ ("offset", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVJALR(imm, rs1, rd) -> + ("op_jalr", + [ ("offset", sprintf "%d" imm); + ("base", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVBType(imm, rs2, rs1, op) -> + ("op_branch", + [ ("op", pp_riscv_bop op); + ("offset", sprintf "%d" imm); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ]) + +| `RISCVIType(imm, rs1, rd, op) -> + ("op_I_type", + [ ("op", pp_riscv_iop op); + ("iimm", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVShiftIop(imm, rs1, rd, op) -> + ("op_IS_type", + [ ("op", pp_riscv_sop op); + ("shamt", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVSHIFTW(imm, rs1, rd, op) -> + ("op_ISW_type", + [ ("op", pp_riscv_sop op); + ("shamt", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVRType (rs2, rs1, rd, op) -> + ("op_R_type", + [ ("op", pp_riscv_rop op); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) -> + ("op_load", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("unsigned", if unsigned then "true" else "false"); + ("base", pp_reg rs1); + ("offset", sprintf "%d" imm); + ("dest", pp_reg rd); + ]) + +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + ("op_store", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("src", pp_reg rs2); + ("base", pp_reg rs1); + ("offset", sprintf "%d" imm); + ]) + +| `RISCVADDIW(imm, rs1, rd) -> + ("op_addiw", + [ ("iimm", sprintf "%d" imm); + ("src", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVRTYPEW(rs2, rs1, rd, op) -> + ("op_RW_type", + [ ("op", pp_riscv_ropw op); + ("src2", pp_reg rs2); + ("src1", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVFENCE(pred, succ) -> + ("op_fence", + [ ("pred", pp_riscv_fence_option pred); + ("succ", pp_riscv_fence_option succ); + ]) + +| `RISCVFENCE_TSO(pred, succ) -> + ("op_fence_tso", + [ ("pred", pp_riscv_fence_option pred); + ("succ", pp_riscv_fence_option succ); + ]) + +| `RISCVFENCEI -> ("op_fence_i", []) + +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + ("op_lr", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("addr", pp_reg rs1); + ("dest", pp_reg rd); + ]) + +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + ("op_sc", + [ ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("addr", pp_reg rs1); + ("src", pp_reg rs2); + ("dest", pp_reg rd); + ]) + +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + ("op_amo", + [ ("op", pp_riscv_amo_op_part op); + ("aq", if aq then "true" else "false"); + ("rl", if rl then "true" else "false"); + ("width", pp_word_width width); + ("src", pp_reg rs2); + ("addr", pp_reg rs1); + ("dest", pp_reg rd); + ]) diff --git a/handwritten_support/hgen/sail_trans_out.hgen b/handwritten_support/hgen/sail_trans_out.hgen new file mode 100644 index 0000000..0ddc508 --- /dev/null +++ b/handwritten_support/hgen/sail_trans_out.hgen @@ -0,0 +1,27 @@ +| ("StopFetching", []) -> `RISCVStopFetching +| ("ThreadStart", []) -> `RISCVThreadStart + +| ("UTYPE", [imm; rd; op]) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) +| ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) +| ("JALR", [imm; rs; rd]) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| ("BTYPE", [imm; rs2; rs1; op]) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| ("ITYPE", [imm; rs1; rd; op]) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) +| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| ("RTYPE", [rs2; rs1; rd; op]) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) +| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl]) + -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| ("STORE", [imm; rs; rd; width; aq; rl]) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) +| ("FENCE", [0; pred; succ]) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) +| ("FENCE", [1; pred; succ]) -> `RISCVFENCE_TSO(translate_out_imm4 pred, translate_out_imm4 succ) +| ("FENCE", [_; pred; succ]) -> failwith "Unknown fm_mode in sail translate out" +| ("FENCEI", []) -> `RISCVFENCEI +| ("LOADRES", [aq; rl; rs1; width; rd]) + -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| ("STORECON", [aq; rl; rs2; rs1; width; rd]) + -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| ("AMO", [op; aq; rl; rs2; rs1; width; rd]) + -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen b/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen new file mode 100644 index 0000000..bea72ac --- /dev/null +++ b/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen @@ -0,0 +1,26 @@ +| STOP_FETCHING () -> `RISCVStopFetching +| THREAD_START () -> `RISCVThreadStart + +| UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) +| RISCV_JAL( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) +| RISCV_JALR( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) +| SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| RTYPE( rs2, rs1, rd, op) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) +| LOAD( imm, rs, rd, unsigned, width, aq, rl) + -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| STORE( imm, rs, rd, width, aq, rl) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) +| ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) +| FENCE( pred, succ) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) +| FENCE_TSO( pred, succ) -> `RISCVFENCE_TSO(translate_out_imm4 pred, translate_out_imm4 succ) +| FENCEI () -> `RISCVFENCEI +| LOADRES( aq, rl, rs1, width, rd) + -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| STORECON( aq, rl, rs2, rs1, width, rd) + -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) +| AMO( op, aq, rl, rs2, rs1, width, rd) + -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen b/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen new file mode 100644 index 0000000..f3e3856 --- /dev/null +++ b/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen @@ -0,0 +1,87 @@ +(* let translate_out_big_bit = Sail_values.unsigned + * + * let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) + * let translate_out_signed_int inst bits = + * let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in + * if (i >= (1 lsl (bits - 1))) then + * (i - (1 lsl bits)) else + * i *) + +let translate_out_int i = Nat_big_num.to_int (Lem.naturalFromWord i) +let translate_out_signed_int i = Nat_big_num.to_int (Lem.signedIntegerFromWord i) + +let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) + +let translate_out_uop op = match op with + | RISCV_LUI -> RISCVLUI + | RISCV_AUIPC -> RISCVAUIPC + +let translate_out_bop op = match op with + | RISCV_BEQ -> RISCVBEQ + | RISCV_BNE -> RISCVBNE + | RISCV_BLT -> RISCVBLT + | RISCV_BGE -> RISCVBGE + | RISCV_BLTU -> RISCVBLTU + | RISCV_BGEU -> RISCVBGEU + +let translate_out_iop op = match op with + | RISCV_ADDI -> RISCVADDI + | RISCV_SLTI -> RISCVSLTI + | RISCV_SLTIU -> RISCVSLTIU + | RISCV_XORI -> RISCVXORI + | RISCV_ORI -> RISCVORI + | RISCV_ANDI -> RISCVANDI + +let translate_out_sop op = match op with + | RISCV_SLLI -> RISCVSLLI + | RISCV_SRLI -> RISCVSRLI + | RISCV_SRAI -> RISCVSRAI + +let translate_out_rop op = match op with + | RISCV_ADD -> RISCVADD + | RISCV_SUB -> RISCVSUB + | RISCV_SLL -> RISCVSLL + | RISCV_SLT -> RISCVSLT + | RISCV_SLTU -> RISCVSLTU + | RISCV_XOR -> RISCVXOR + | RISCV_SRL -> RISCVSRL + | RISCV_SRA -> RISCVSRA + | RISCV_OR -> RISCVOR + | RISCV_AND -> RISCVAND + +let translate_out_ropw op = match op with + | RISCV_ADDW -> RISCVADDW + | RISCV_SUBW -> RISCVSUBW + | RISCV_SLLW -> RISCVSLLW + | RISCV_SRLW -> RISCVSRLW + | RISCV_SRAW -> RISCVSRAW + +let translate_out_amoop op = match op with + | AMOSWAP -> RISCVAMOSWAP + | AMOADD -> RISCVAMOADD + | AMOXOR -> RISCVAMOXOR + | AMOAND -> RISCVAMOAND + | AMOOR -> RISCVAMOOR + | AMOMIN -> RISCVAMOMIN + | AMOMAX -> RISCVAMOMAX + | AMOMINU -> RISCVAMOMINU + | AMOMAXU -> RISCVAMOMAXU + +let translate_out_wordWidth op = match op with + | BYTE -> RISCVBYTE + | HALF -> RISCVHALF + | WORD -> RISCVWORD + | DOUBLE -> RISCVDOUBLE + +let translate_out_bool b = b (* function + * | Sail_values.B1 -> true + * | Sail_values.B0 -> false + * | _ -> failwith "translate_out_bool Undef" *) + +let translate_out_simm21 imm = translate_out_signed_int imm (* 21 *) +let translate_out_simm20 imm = translate_out_signed_int imm (* 20 *) +let translate_out_simm13 imm = translate_out_signed_int imm (* 13 *) +let translate_out_simm12 imm = translate_out_signed_int imm (* 12 *) +let translate_out_imm6 imm = translate_out_int imm +let translate_out_imm5 imm = translate_out_int imm +let translate_out_imm4 imm = translate_out_int imm diff --git a/handwritten_support/hgen/token_types.hgen b/handwritten_support/hgen/token_types.hgen new file mode 100644 index 0000000..1a2895a --- /dev/null +++ b/handwritten_support/hgen/token_types.hgen @@ -0,0 +1,24 @@ +type token_UTYPE = {op : riscvUop } +type token_JAL = unit +type token_JALR = unit +type token_BType = {op : riscvBop } +type token_IType = {op : riscvIop } +type token_ShiftIop = {op : riscvSop } +type token_RTYPE = {op : riscvRop } +type token_Load = {unsigned: bool; width : wordWidth; aq: bool; rl: bool } +type token_Store = {width : wordWidth; aq: bool; rl: bool } +type token_ADDIW = unit +type token_SHIFTW = {op : riscvSop } +type token_RTYPEW = {op : riscvRopw } +type token_FENCE = unit +type token_FENCETSO = unit +type token_FENCEI = unit +type token_LoadRes = {width : wordWidth; aq: bool; rl: bool } +type token_StoreCon = {width : wordWidth; aq: bool; rl: bool } +type token_AMO = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop } + +type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW + +(* pseudo-ops *) + +type token_LI = unit diff --git a/handwritten_support/hgen/tokens.hgen b/handwritten_support/hgen/tokens.hgen new file mode 100644 index 0000000..37c76a2 --- /dev/null +++ b/handwritten_support/hgen/tokens.hgen @@ -0,0 +1,20 @@ +%token UTYPE +%token JAL +%token JALR +%token BTYPE +%token ITYPE +%token SHIFTIOP +%token RTYPE +%token LOAD +%token STORE +%token ADDIW +%token SHIFTW +%token RTYPEW +%token FENCE +%token FENCEOPTION +%token FENCETSO +%token FENCEI +%token LOADRES +%token STORECON +%token AMO +%token LI diff --git a/handwritten_support/hgen/trans_sail.hgen b/handwritten_support/hgen/trans_sail.hgen new file mode 100644 index 0000000..aceaee7 --- /dev/null +++ b/handwritten_support/hgen/trans_sail.hgen @@ -0,0 +1,162 @@ +| `RISCVStopFetching -> ("StopFetching", [], []) +| `RISCVThreadStart -> ("ThreadStart", [], []) + +| `RISCVUTYPE(imm, rd, op) -> + ("UTYPE", + [ + translate_imm20 "imm" imm; + translate_reg "rd" rd; + translate_uop "op" op; + ], + []) +| `RISCVJAL(imm, rd) -> + ("JAL", + [ + translate_imm21 "imm" imm; + translate_reg "rd" rd; + ], + []) +| `RISCVJALR(imm, rs, rd) -> + ("JALR", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rd; + translate_reg "rd" rd; + ], + []) +| `RISCVBType(imm, rs2, rs1, op) -> + ("BTYPE", + [ + translate_imm13 "imm" imm; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_bop "op" op; + ], + []) +| `RISCVIType(imm, rs1, rd, op) -> + ("ITYPE", + [ + translate_imm12 "imm" imm; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_iop "op" op; + ], + []) +| `RISCVShiftIop(imm, rs, rd, op) -> + ("SHIFTIOP", + [ + translate_imm6 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRType (rs2, rs1, rd, op) -> + ("RTYPE", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_rop "op" op; + ], + []) +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> + ("LOAD", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_bool "unsigned" unsigned; + translate_width "width" width; + translate_bool "aq" aq; + translate_bool "rl" rl; + ], + []) +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + ("STORE", + [ + translate_imm12 "imm" imm; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_bool "aq" aq; + translate_bool "rl" rl; + ], + []) +| `RISCVADDIW(imm, rs, rd) -> + ("ADDIW", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + ], + []) +| `RISCVSHIFTW(imm, rs, rd, op) -> + ("SHIFTW", + [ + translate_imm5 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRTYPEW(rs2, rs1, rd, op) -> + ("RTYPEW", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_ropw "op" op; + ], + []) +| `RISCVFENCE(pred, succ) -> + ("FENCE", + [ + translate_imm4 "pred" pred; + translate_imm4 "succ" succ; + ], + []) +| `RISCVFENCE_TSO(pred, succ) -> + ("FENCE_TSO", + [ + translate_imm4 "pred" pred; + translate_imm4 "succ" succ; + ], + []) +| `RISCVFENCEI -> + ("FENCEI", + [], + []) +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + ("LOADRES", + [ + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + ("STORECON", + [ + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + ("AMO", + [ + translate_amoop "op" op; + translate_bool "aq" aq; + translate_bool "rl" rl; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_width "width" width; + translate_reg "rd" rd; + ], + []) diff --git a/handwritten_support/hgen/types.hgen b/handwritten_support/hgen/types.hgen new file mode 100644 index 0000000..a0b7560 --- /dev/null +++ b/handwritten_support/hgen/types.hgen @@ -0,0 +1,172 @@ +type bit20 = int +type bit12 = int +type bit6 = int +type bit5 = int +type bit4 = int + +type riscvUop = (* upper immediate ops *) +| RISCVLUI +| RISCVAUIPC + +let pp_riscv_uop = function +| RISCVLUI -> "lui" +| RISCVAUIPC -> "auipc" + + +type riscvBop = (* branch ops *) +| RISCVBEQ +| RISCVBNE +| RISCVBLT +| RISCVBGE +| RISCVBLTU +| RISCVBGEU + +let pp_riscv_bop = function +| RISCVBEQ -> "beq" +| RISCVBNE -> "bne" +| RISCVBLT -> "blt" +| RISCVBGE -> "bge" +| RISCVBLTU -> "bltu" +| RISCVBGEU -> "bgeu" + +type riscvIop = (* immediate ops *) +| RISCVADDI +| RISCVSLTI +| RISCVSLTIU +| RISCVXORI +| RISCVORI +| RISCVANDI + +let pp_riscv_iop = function +| RISCVADDI -> "addi" +| RISCVSLTI -> "slti" +| RISCVSLTIU -> "sltiu" +| RISCVXORI -> "xori" +| RISCVORI -> "ori" +| RISCVANDI -> "andi" + +type riscvSop = (* shift ops *) +| RISCVSLLI +| RISCVSRLI +| RISCVSRAI + +let pp_riscv_sop = function +| RISCVSLLI -> "slli" +| RISCVSRLI -> "srli" +| RISCVSRAI -> "srai" + +type riscvRop = (* reg-reg ops *) +| RISCVADD +| RISCVSUB +| RISCVSLL +| RISCVSLT +| RISCVSLTU +| RISCVXOR +| RISCVSRL +| RISCVSRA +| RISCVOR +| RISCVAND + +let pp_riscv_rop = function +| RISCVADD -> "add" +| RISCVSUB -> "sub" +| RISCVSLL -> "sll" +| RISCVSLT -> "slt" +| RISCVSLTU -> "sltu" +| RISCVXOR -> "xor" +| RISCVSRL -> "srl" +| RISCVSRA -> "sra" +| RISCVOR -> "or" +| RISCVAND -> "and" + +type riscvRopw = (* reg-reg 32-bit ops *) +| RISCVADDW +| RISCVSUBW +| RISCVSLLW +| RISCVSRLW +| RISCVSRAW + +let pp_riscv_ropw = function +| RISCVADDW -> "addw" +| RISCVSUBW -> "subw" +| RISCVSLLW -> "sllw" +| RISCVSRLW -> "srlw" +| RISCVSRAW -> "sraw" + +type wordWidth = + | RISCVBYTE + | RISCVHALF + | RISCVWORD + | RISCVDOUBLE + +let pp_word_width width : string = + begin match width with + | RISCVBYTE -> "b" + | RISCVHALF -> "h" + | RISCVWORD -> "w" + | RISCVDOUBLE -> "d" + end + +let pp_riscv_load_op (unsigned, width, aq, rl) = + "l" ^ + (pp_word_width width) ^ + (if unsigned then "u" else "") ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_store_op (width, aq, rl) = + "s" ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_load_reserved_op (aq, rl, width) = + "lr." ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_store_conditional_op (aq, rl, width) = + "sc." ^ + (pp_word_width width) ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +type riscvAmoop = + | RISCVAMOSWAP + | RISCVAMOADD + | RISCVAMOXOR + | RISCVAMOAND + | RISCVAMOOR + | RISCVAMOMIN + | RISCVAMOMAX + | RISCVAMOMINU + | RISCVAMOMAXU + +let pp_riscv_amo_op_part = function + | RISCVAMOSWAP -> "swap" + | RISCVAMOADD -> "add" + | RISCVAMOXOR -> "xor" + | RISCVAMOAND -> "and" + | RISCVAMOOR -> "or" + | RISCVAMOMIN -> "min" + | RISCVAMOMAX -> "max" + | RISCVAMOMINU -> "minu" + | RISCVAMOMAXU -> "maxu" + +let pp_riscv_amo_op (op, aq, rl, width) = + "amo" ^ + pp_riscv_amo_op_part op ^ + begin match width with + | RISCVWORD -> ".w" + | RISCVDOUBLE -> ".d" + | _ -> assert false + end ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") + +let pp_riscv_fence_option = function + | 0b0011 -> "rw" + | 0b0010 -> "r" + | 0b0001 -> "w" + | _ -> failwith "unexpected fence option" diff --git a/handwritten_support/hgen/types_sail_trans_out.hgen b/handwritten_support/hgen/types_sail_trans_out.hgen new file mode 100644 index 0000000..66a2020 --- /dev/null +++ b/handwritten_support/hgen/types_sail_trans_out.hgen @@ -0,0 +1,98 @@ +let translate_out_big_bit = function + | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits + | _ -> assert false + +let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) +let translate_out_signed_int inst bits = + let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in + if (i >= (1 lsl (bits - 1))) then + (i - (1 lsl bits)) else + i + +let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) + +let translate_out_simm21 imm = translate_out_signed_int imm 21 +let translate_out_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm13 imm = translate_out_signed_int imm 13 +let translate_out_simm12 imm = translate_out_signed_int imm 12 +let translate_out_imm6 imm = translate_out_int imm +let translate_out_imm5 imm = translate_out_int imm +let translate_out_imm4 imm = translate_out_int imm + +let translate_out_bool = function + | (name, Bit, [Bitc_one]) -> true + | (name, Bit, [Bitc_zero]) -> false + | _ -> assert false + +let translate_out_enum (name,_,bits) = + Nat_big_num.to_int (IInt.integer_of_bit_list bits) + +let translate_out_wordWidth w = + match translate_out_enum w with + | 0 -> RISCVBYTE + | 1 -> RISCVHALF + | 2 -> RISCVWORD + | 3 -> RISCVDOUBLE + | _ -> failwith "Unknown wordWidth in sail translate out" + +let translate_out_uop op = match translate_out_enum op with + | 0 -> RISCVLUI + | 1 -> RISCVAUIPC + | _ -> failwith "Unknown uop in sail translate out" + +let translate_out_bop op = match translate_out_enum op with +| 0 -> RISCVBEQ +| 1 -> RISCVBNE +| 2 -> RISCVBLT +| 3 -> RISCVBGE +| 4 -> RISCVBLTU +| 5 -> RISCVBGEU +| _ -> failwith "Unknown bop in sail translate out" + +let translate_out_iop op = match translate_out_enum op with +| 0 -> RISCVADDI +| 1 -> RISCVSLTI +| 2 -> RISCVSLTIU +| 3 -> RISCVXORI +| 4 -> RISCVORI +| 5 -> RISCVANDI +| _ -> failwith "Unknown iop in sail translate out" + +let translate_out_sop op = match translate_out_enum op with +| 0 -> RISCVSLLI +| 1 -> RISCVSRLI +| 2 -> RISCVSRAI +| _ -> failwith "Unknown sop in sail translate out" + +let translate_out_rop op = match translate_out_enum op with +| 0 -> RISCVADD +| 1 -> RISCVSUB +| 2 -> RISCVSLL +| 3 -> RISCVSLT +| 4 -> RISCVSLTU +| 5 -> RISCVXOR +| 6 -> RISCVSRL +| 7 -> RISCVSRA +| 8 -> RISCVOR +| 9 -> RISCVAND +| _ -> failwith "Unknown rop in sail translate out" + +let translate_out_ropw op = match translate_out_enum op with +| 0 -> RISCVADDW +| 1 -> RISCVSUBW +| 2 -> RISCVSLLW +| 3 -> RISCVSRLW +| 4 -> RISCVSRAW +| _ -> failwith "Unknown ropw in sail translate out" + +let translate_out_amoop op = match translate_out_enum op with +| 0 -> RISCVAMOSWAP +| 1 -> RISCVAMOADD +| 2 -> RISCVAMOXOR +| 3 -> RISCVAMOAND +| 4 -> RISCVAMOOR +| 5 -> RISCVAMOMIN +| 6 -> RISCVAMOMAX +| 7 -> RISCVAMOMINU +| 8 -> RISCVAMOMAXU +| _ -> failwith "Unknown amoop in sail translate out" diff --git a/handwritten_support/hgen/types_trans_sail.hgen b/handwritten_support/hgen/types_trans_sail.hgen new file mode 100644 index 0000000..238c7e5 --- /dev/null +++ b/handwritten_support/hgen/types_trans_sail.hgen @@ -0,0 +1,57 @@ +let translate_enum enum_values name value = + let rec bit_count n = + if n = 0 then 0 + else 1 + (bit_count (n lsr 1)) in + let rec find_index element = function + | h::tail -> if h = element then 0 else 1 + (find_index element tail) + | _ -> failwith "translate_enum could not find value" + in + let size = bit_count (List.length enum_values) in + let index = find_index value enum_values in + (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index)) + +let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC] + +let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *) + +let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *) + +let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *) + +let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *) + +let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *) + +let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU] + +let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] + +let translate_reg name value = + (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value))) + +let translate_imm21 name value = + (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value)) + +let translate_imm20 name value = + (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value)) + +let translate_imm16 name value = + (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value)) + +let translate_imm13 name value = + (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value)) + +let translate_imm12 name value = + (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value)) + +let translate_imm6 name value = + (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value)) + +let translate_imm5 name value = + (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value)) + +let translate_imm4 name value = + (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value)) + +let translate_bool name value = + (name, Bit, [if value then Bitc_one else Bitc_zero]) diff --git a/handwritten_support/mem_metadata.glob b/handwritten_support/mem_metadata.glob new file mode 100644 index 0000000..c2d0ccd --- /dev/null +++ b/handwritten_support/mem_metadata.glob @@ -0,0 +1,64 @@ +DIGEST 693b57d74f776ae8bd215fbfc8b03df3 +Fmem_metadata +R15:23 Sail.Base <> <> lib +def 52:60 <> write_ram +binder 63:64 <> rv:1 +binder 66:66 <> e:2 +binder 68:68 <> a:3 +binder 71:72 <> wk:4 +R82:86 Sail.Values <> mword def +R88:88 mem_metadata <> a:3 var +binder 75:78 <> addr:5 +binder 91:94 <> size:6 +R101:105 Sail.Values <> mword def +R109:111 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R112:115 mem_metadata <> size:6 var +binder 97:97 <> v:7 +R127:130 Coq.Init.Datatypes <> unit ind +binder 120:123 <> meta:8 +R135:139 Sail.Prompt_monad <> monad ind +R141:142 mem_metadata <> rv:1 var +R144:147 Coq.Init.Datatypes <> bool ind +R149:149 mem_metadata <> e:2 var +R154:162 Sail.Prompt_monad <> write_mem def +R179:179 mem_metadata <> v:7 var +R174:177 mem_metadata <> size:6 var +R169:172 mem_metadata <> addr:5 var +R167:167 mem_metadata <> a:3 var +R164:165 mem_metadata <> wk:4 var +def 194:201 <> read_ram +binder 204:205 <> rv:9 +binder 207:207 <> e:10 +binder 209:209 <> a:11 +binder 212:213 <> rk:12 +R223:227 Sail.Values <> mword def +R229:229 mem_metadata <> a:11 var +binder 216:219 <> addr:13 +binder 232:235 <> size:14 +R249:252 Coq.Init.Datatypes <> bool ind +binder 238:245 <> read_tag:15 +R257:265 Sail.Values <> ArithFact class +R272:276 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R268:271 mem_metadata <> size:14 var +binder 257:278 <> H:16 +R283:287 Sail.Prompt_monad <> monad ind +R289:290 mem_metadata <> rv:9 var +R309:311 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not +R293:297 Sail.Values <> mword def +R301:303 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R304:307 mem_metadata <> size:14 var +R312:315 Coq.Init.Datatypes <> unit ind +R318:318 mem_metadata <> e:10 var +R348:352 Sail.Prompt_monad <> :::x_'>>='_x not +R325:332 Sail.Prompt_monad <> read_mem def +R344:347 mem_metadata <> size:14 var +R339:342 mem_metadata <> addr:13 var +R337:337 mem_metadata <> a:11 var +R334:335 mem_metadata <> rk:12 var +binder 357:360 <> data:17 +R367:373 Sail.Prompt_monad <> returnm def +R375:375 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not +R380:381 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not +R384:384 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not +R376:379 mem_metadata <> data:17 var +R382:383 Coq.Init.Datatypes <> tt constr diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem new file mode 100644 index 0000000..8a8c070 --- /dev/null +++ b/handwritten_support/mem_metadata.lem @@ -0,0 +1,16 @@ +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/mem_metadata.v b/handwritten_support/mem_metadata.v new file mode 100644 index 0000000..bbfc856 --- /dev/null +++ b/handwritten_support/mem_metadata.v @@ -0,0 +1,8 @@ +Require Import Sail.Base. +Open Scope Z. + +Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v. + +Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e := + read_mem rk a addr size >>= fun data => + returnm (data, tt). diff --git a/handwritten_support/mem_metadata.vo b/handwritten_support/mem_metadata.vo new file mode 100644 index 0000000..76f5087 Binary files /dev/null and b/handwritten_support/mem_metadata.vo differ diff --git a/handwritten_support/mem_metadata.vok b/handwritten_support/mem_metadata.vok new file mode 100644 index 0000000..e69de29 diff --git a/handwritten_support/mem_metadata.vos b/handwritten_support/mem_metadata.vos new file mode 100644 index 0000000..e69de29 diff --git a/handwritten_support/riscv_extras.glob b/handwritten_support/riscv_extras.glob new file mode 100644 index 0000000..980acb4 --- /dev/null +++ b/handwritten_support/riscv_extras.glob @@ -0,0 +1,875 @@ +DIGEST 9f6e940694efb436e57a7a26d0b1b3b3 +Friscv_extras +R15:23 Sail.Base <> <> lib +R41:46 Coq.Strings.String <> <> lib +R64:67 Coq.Lists.List <> <> lib +def 123:137 <> MEM_fence_rw_rw +binder 140:141 <> rv:1 +binder 143:143 <> e:2 +R149:152 Coq.Init.Datatypes <> unit ind +R157:161 Sail.Prompt_monad <> monad ind +R163:164 riscv_extras <> rv:1 var +R166:169 Coq.Init.Datatypes <> unit ind +R171:171 riscv_extras <> e:2 var +R176:182 Sail.Prompt_monad <> barrier def +R185:203 Sail.Instr_kinds <> Barrier_RISCV_rw_rw constr +R205:206 Coq.Init.Datatypes <> tt constr +def 221:234 <> MEM_fence_r_rw +binder 238:239 <> rv:3 +binder 241:241 <> e:4 +R247:250 Coq.Init.Datatypes <> unit ind +R255:259 Sail.Prompt_monad <> monad ind +R261:262 riscv_extras <> rv:3 var +R264:267 Coq.Init.Datatypes <> unit ind +R269:269 riscv_extras <> e:4 var +R274:280 Sail.Prompt_monad <> barrier def +R283:300 Sail.Instr_kinds <> Barrier_RISCV_r_rw constr +R302:303 Coq.Init.Datatypes <> tt constr +def 318:330 <> MEM_fence_r_r +binder 335:336 <> rv:5 +binder 338:338 <> e:6 +R344:347 Coq.Init.Datatypes <> unit ind +R352:356 Sail.Prompt_monad <> monad ind +R358:359 riscv_extras <> rv:5 var +R361:364 Coq.Init.Datatypes <> unit ind +R366:366 riscv_extras <> e:6 var +R371:377 Sail.Prompt_monad <> barrier def +R380:396 Sail.Instr_kinds <> Barrier_RISCV_r_r constr +R398:399 Coq.Init.Datatypes <> tt constr +def 414:427 <> MEM_fence_rw_w +binder 431:432 <> rv:7 +binder 434:434 <> e:8 +R440:443 Coq.Init.Datatypes <> unit ind +R448:452 Sail.Prompt_monad <> monad ind +R454:455 riscv_extras <> rv:7 var +R457:460 Coq.Init.Datatypes <> unit ind +R462:462 riscv_extras <> e:8 var +R467:473 Sail.Prompt_monad <> barrier def +R476:493 Sail.Instr_kinds <> Barrier_RISCV_rw_w constr +R495:496 Coq.Init.Datatypes <> tt constr +def 511:523 <> MEM_fence_w_w +binder 528:529 <> rv:9 +binder 531:531 <> e:10 +R537:540 Coq.Init.Datatypes <> unit ind +R545:549 Sail.Prompt_monad <> monad ind +R551:552 riscv_extras <> rv:9 var +R554:557 Coq.Init.Datatypes <> unit ind +R559:559 riscv_extras <> e:10 var +R564:570 Sail.Prompt_monad <> barrier def +R573:589 Sail.Instr_kinds <> Barrier_RISCV_w_w constr +R591:592 Coq.Init.Datatypes <> tt constr +def 607:620 <> MEM_fence_w_rw +binder 624:625 <> rv:11 +binder 627:627 <> e:12 +R633:636 Coq.Init.Datatypes <> unit ind +R641:645 Sail.Prompt_monad <> monad ind +R647:648 riscv_extras <> rv:11 var +R650:653 Coq.Init.Datatypes <> unit ind +R655:655 riscv_extras <> e:12 var +R660:666 Sail.Prompt_monad <> barrier def +R669:686 Sail.Instr_kinds <> Barrier_RISCV_w_rw constr +R688:689 Coq.Init.Datatypes <> tt constr +def 704:717 <> MEM_fence_rw_r +binder 721:722 <> rv:13 +binder 724:724 <> e:14 +R730:733 Coq.Init.Datatypes <> unit ind +R738:742 Sail.Prompt_monad <> monad ind +R744:745 riscv_extras <> rv:13 var +R747:750 Coq.Init.Datatypes <> unit ind +R752:752 riscv_extras <> e:14 var +R757:763 Sail.Prompt_monad <> barrier def +R766:783 Sail.Instr_kinds <> Barrier_RISCV_rw_r constr +R785:786 Coq.Init.Datatypes <> tt constr +def 801:813 <> MEM_fence_r_w +binder 818:819 <> rv:15 +binder 821:821 <> e:16 +R827:830 Coq.Init.Datatypes <> unit ind +R835:839 Sail.Prompt_monad <> monad ind +R841:842 riscv_extras <> rv:15 var +R844:847 Coq.Init.Datatypes <> unit ind +R849:849 riscv_extras <> e:16 var +R854:860 Sail.Prompt_monad <> barrier def +R863:879 Sail.Instr_kinds <> Barrier_RISCV_r_w constr +R881:882 Coq.Init.Datatypes <> tt constr +def 897:909 <> MEM_fence_w_r +binder 914:915 <> rv:17 +binder 917:917 <> e:18 +R923:926 Coq.Init.Datatypes <> unit ind +R931:935 Sail.Prompt_monad <> monad ind +R937:938 riscv_extras <> rv:17 var +R940:943 Coq.Init.Datatypes <> unit ind +R945:945 riscv_extras <> e:18 var +R950:956 Sail.Prompt_monad <> barrier def +R959:975 Sail.Instr_kinds <> Barrier_RISCV_w_r constr +R977:978 Coq.Init.Datatypes <> tt constr +def 993:1005 <> MEM_fence_tso +binder 1010:1011 <> rv:19 +binder 1013:1013 <> e:20 +R1019:1022 Coq.Init.Datatypes <> unit ind +R1027:1031 Sail.Prompt_monad <> monad ind +R1033:1034 riscv_extras <> rv:19 var +R1036:1039 Coq.Init.Datatypes <> unit ind +R1041:1041 riscv_extras <> e:20 var +R1046:1052 Sail.Prompt_monad <> barrier def +R1055:1071 Sail.Instr_kinds <> Barrier_RISCV_tso constr +R1073:1074 Coq.Init.Datatypes <> tt constr +def 1089:1099 <> MEM_fence_i +binder 1106:1107 <> rv:21 +binder 1109:1109 <> e:22 +R1115:1118 Coq.Init.Datatypes <> unit ind +R1123:1127 Sail.Prompt_monad <> monad ind +R1129:1130 riscv_extras <> rv:21 var +R1132:1135 Coq.Init.Datatypes <> unit ind +R1137:1137 riscv_extras <> e:22 var +R1142:1148 Sail.Prompt_monad <> barrier def +R1151:1165 Sail.Instr_kinds <> Barrier_RISCV_i constr +R1167:1168 Coq.Init.Datatypes <> tt constr +def 1867:1871 <> MEMea +binder 1874:1875 <> rv:23 +binder 1877:1877 <> a:24 +binder 1879:1879 <> e:25 +binder 1882:1889 <> addrsize:26 +R1899:1903 Sail.Values <> mword def +R1905:1905 riscv_extras <> a:24 var +binder 1892:1895 <> addr:27 +binder 1908:1911 <> size:28 +R1935:1939 Sail.Prompt_monad <> monad ind +R1941:1942 riscv_extras <> rv:23 var +R1944:1947 Coq.Init.Datatypes <> unit ind +R1949:1949 riscv_extras <> e:25 var +R1954:1965 Sail.Prompt_monad <> write_mem_ea def +R1993:1996 riscv_extras <> size:28 var +R1988:1991 riscv_extras <> addr:27 var +R1979:1986 riscv_extras <> addrsize:26 var +R1967:1977 Sail.Instr_kinds <> Write_plain constr +def 2010:2022 <> MEMea_release +binder 2025:2026 <> rv:29 +binder 2028:2028 <> a:30 +binder 2030:2030 <> e:31 +binder 2033:2040 <> addrsize:32 +R2050:2054 Sail.Values <> mword def +R2056:2056 riscv_extras <> a:30 var +binder 2043:2046 <> addr:33 +binder 2059:2062 <> size:34 +R2078:2082 Sail.Prompt_monad <> monad ind +R2084:2085 riscv_extras <> rv:29 var +R2087:2090 Coq.Init.Datatypes <> unit ind +R2092:2092 riscv_extras <> e:31 var +R2097:2108 Sail.Prompt_monad <> write_mem_ea def +R2144:2147 riscv_extras <> size:34 var +R2139:2142 riscv_extras <> addr:33 var +R2130:2137 riscv_extras <> addrsize:32 var +R2110:2128 Sail.Instr_kinds <> Write_RISCV_release constr +def 2161:2180 <> MEMea_strong_release +binder 2183:2184 <> rv:35 +binder 2186:2186 <> a:36 +binder 2188:2188 <> e:37 +binder 2191:2198 <> addrsize:38 +R2208:2212 Sail.Values <> mword def +R2214:2214 riscv_extras <> a:36 var +binder 2201:2204 <> addr:39 +binder 2217:2220 <> size:40 +R2229:2233 Sail.Prompt_monad <> monad ind +R2235:2236 riscv_extras <> rv:35 var +R2238:2241 Coq.Init.Datatypes <> unit ind +R2243:2243 riscv_extras <> e:37 var +R2248:2259 Sail.Prompt_monad <> write_mem_ea def +R2302:2305 riscv_extras <> size:40 var +R2297:2300 riscv_extras <> addr:39 var +R2288:2295 riscv_extras <> addrsize:38 var +R2261:2286 Sail.Instr_kinds <> Write_RISCV_strong_release constr +def 2319:2335 <> MEMea_conditional +binder 2338:2339 <> rv:41 +binder 2341:2341 <> a:42 +binder 2343:2343 <> e:43 +binder 2346:2353 <> addrsize:44 +R2363:2367 Sail.Values <> mword def +R2369:2369 riscv_extras <> a:42 var +binder 2356:2359 <> addr:45 +binder 2372:2375 <> size:46 +R2387:2391 Sail.Prompt_monad <> monad ind +R2393:2394 riscv_extras <> rv:41 var +R2396:2399 Coq.Init.Datatypes <> unit ind +R2401:2401 riscv_extras <> e:43 var +R2406:2417 Sail.Prompt_monad <> write_mem_ea def +R2457:2460 riscv_extras <> size:46 var +R2452:2455 riscv_extras <> addr:45 var +R2443:2450 riscv_extras <> addrsize:44 var +R2419:2441 Sail.Instr_kinds <> Write_RISCV_conditional constr +def 2474:2498 <> MEMea_conditional_release +binder 2501:2502 <> rv:47 +binder 2504:2504 <> a:48 +binder 2506:2506 <> e:49 +binder 2509:2516 <> addrsize:50 +R2526:2530 Sail.Values <> mword def +R2532:2532 riscv_extras <> a:48 var +binder 2519:2522 <> addr:51 +binder 2535:2538 <> size:52 +R2542:2546 Sail.Prompt_monad <> monad ind +R2548:2549 riscv_extras <> rv:47 var +R2551:2554 Coq.Init.Datatypes <> unit ind +R2556:2556 riscv_extras <> e:49 var +R2561:2572 Sail.Prompt_monad <> write_mem_ea def +R2620:2623 riscv_extras <> size:52 var +R2615:2618 riscv_extras <> addr:51 var +R2606:2613 riscv_extras <> addrsize:50 var +R2574:2604 Sail.Instr_kinds <> Write_RISCV_conditional_release constr +def 2637:2668 <> MEMea_conditional_strong_release +binder 2671:2672 <> rv:53 +binder 2674:2674 <> a:54 +binder 2676:2676 <> e:55 +binder 2679:2686 <> addrsize:56 +R2696:2700 Sail.Values <> mword def +R2702:2702 riscv_extras <> a:54 var +binder 2689:2692 <> addr:57 +binder 2705:2708 <> size:58 +R2712:2716 Sail.Prompt_monad <> monad ind +R2718:2719 riscv_extras <> rv:53 var +R2721:2724 Coq.Init.Datatypes <> unit ind +R2726:2726 riscv_extras <> e:55 var +R2773:2784 Sail.Prompt_monad <> write_mem_ea def +R2839:2842 riscv_extras <> size:58 var +R2834:2837 riscv_extras <> addr:57 var +R2825:2832 riscv_extras <> addrsize:56 var +R2786:2823 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr +def 3812:3815 <> MEMr +binder 3818:3819 <> rv:59 +binder 3821:3821 <> e:60 +binder 3824:3831 <> addrsize:61 +binder 3833:3836 <> size:62 +R3853:3857 Sail.Values <> mword def +R3859:3866 riscv_extras <> addrsize:61 var +binder 3839:3844 <> hexRAM:63 +binder 3846:3849 <> addr:64 +R3895:3903 Sail.Values <> ArithFact class +R3910:3914 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R3906:3909 riscv_extras <> size:62 var +binder 3895:3916 <> H:65 +R3921:3925 Sail.Prompt_monad <> monad ind +R3927:3928 riscv_extras <> rv:59 var +R3931:3935 Sail.Values <> mword def +R3939:3941 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R3942:3945 riscv_extras <> size:62 var +R3949:3949 riscv_extras <> e:60 var +R3954:3961 Sail.Prompt_monad <> read_mem def +R3988:3991 riscv_extras <> size:62 var +R3983:3986 riscv_extras <> addr:64 var +R3974:3981 riscv_extras <> addrsize:61 var +R3963:3972 Sail.Instr_kinds <> Read_plain constr +def 4005:4016 <> MEMr_acquire +binder 4019:4020 <> rv:66 +binder 4022:4022 <> e:67 +binder 4025:4032 <> addrsize:68 +binder 4034:4037 <> size:69 +R4054:4058 Sail.Values <> mword def +R4060:4067 riscv_extras <> addrsize:68 var +binder 4040:4045 <> hexRAM:70 +binder 4047:4050 <> addr:71 +R4088:4096 Sail.Values <> ArithFact class +R4103:4107 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R4099:4102 riscv_extras <> size:69 var +binder 4088:4109 <> H:72 +R4114:4118 Sail.Prompt_monad <> monad ind +R4120:4121 riscv_extras <> rv:66 var +R4124:4128 Sail.Values <> mword def +R4132:4134 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R4135:4138 riscv_extras <> size:69 var +R4142:4142 riscv_extras <> e:67 var +R4147:4154 Sail.Prompt_monad <> read_mem def +R4189:4192 riscv_extras <> size:69 var +R4184:4187 riscv_extras <> addr:71 var +R4175:4182 riscv_extras <> addrsize:68 var +R4156:4173 Sail.Instr_kinds <> Read_RISCV_acquire constr +def 4206:4224 <> MEMr_strong_acquire +binder 4227:4228 <> rv:73 +binder 4230:4230 <> e:74 +binder 4233:4240 <> addrsize:75 +binder 4242:4245 <> size:76 +R4262:4266 Sail.Values <> mword def +R4268:4275 riscv_extras <> addrsize:75 var +binder 4248:4253 <> hexRAM:77 +binder 4255:4258 <> addr:78 +R4289:4297 Sail.Values <> ArithFact class +R4304:4308 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R4300:4303 riscv_extras <> size:76 var +binder 4289:4310 <> H:79 +R4315:4319 Sail.Prompt_monad <> monad ind +R4321:4322 riscv_extras <> rv:73 var +R4325:4329 Sail.Values <> mword def +R4333:4335 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R4336:4339 riscv_extras <> size:76 var +R4343:4343 riscv_extras <> e:74 var +R4348:4355 Sail.Prompt_monad <> read_mem def +R4397:4400 riscv_extras <> size:76 var +R4392:4395 riscv_extras <> addr:78 var +R4383:4390 riscv_extras <> addrsize:75 var +R4357:4381 Sail.Instr_kinds <> Read_RISCV_strong_acquire constr +def 4414:4426 <> MEMr_reserved +binder 4429:4430 <> rv:80 +binder 4432:4432 <> e:81 +binder 4435:4442 <> addrsize:82 +binder 4444:4447 <> size:83 +R4464:4468 Sail.Values <> mword def +R4470:4477 riscv_extras <> addrsize:82 var +binder 4450:4455 <> hexRAM:84 +binder 4457:4460 <> addr:85 +R4497:4505 Sail.Values <> ArithFact class +R4512:4516 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R4508:4511 riscv_extras <> size:83 var +binder 4497:4518 <> H:86 +R4523:4527 Sail.Prompt_monad <> monad ind +R4529:4530 riscv_extras <> rv:80 var +R4533:4537 Sail.Values <> mword def +R4541:4543 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R4544:4547 riscv_extras <> size:83 var +R4551:4551 riscv_extras <> e:81 var +R4556:4563 Sail.Prompt_monad <> read_mem def +R4599:4602 riscv_extras <> size:83 var +R4594:4597 riscv_extras <> addr:85 var +R4585:4592 riscv_extras <> addrsize:82 var +R4565:4583 Sail.Instr_kinds <> Read_RISCV_reserved constr +def 4616:4636 <> MEMr_reserved_acquire +binder 4639:4640 <> rv:87 +binder 4642:4642 <> e:88 +binder 4645:4652 <> addrsize:89 +binder 4654:4657 <> size:90 +R4674:4678 Sail.Values <> mword def +R4680:4687 riscv_extras <> addrsize:89 var +binder 4660:4665 <> hexRAM:91 +binder 4667:4670 <> addr:92 +R4699:4707 Sail.Values <> ArithFact class +R4714:4718 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R4710:4713 riscv_extras <> size:90 var +binder 4699:4720 <> H:93 +R4725:4729 Sail.Prompt_monad <> monad ind +R4731:4732 riscv_extras <> rv:87 var +R4735:4739 Sail.Values <> mword def +R4743:4745 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R4746:4749 riscv_extras <> size:90 var +R4753:4753 riscv_extras <> e:88 var +R4758:4765 Sail.Prompt_monad <> read_mem def +R4809:4812 riscv_extras <> size:90 var +R4804:4807 riscv_extras <> addr:92 var +R4795:4802 riscv_extras <> addrsize:89 var +R4767:4793 Sail.Instr_kinds <> Read_RISCV_reserved_acquire constr +def 4826:4853 <> MEMr_reserved_strong_acquire +binder 4856:4857 <> rv:94 +binder 4859:4859 <> e:95 +binder 4862:4869 <> addrsize:96 +binder 4871:4874 <> size:97 +R4891:4895 Sail.Values <> mword def +R4897:4904 riscv_extras <> addrsize:96 var +binder 4877:4882 <> hexRAM:98 +binder 4884:4887 <> addr:99 +R4909:4917 Sail.Values <> ArithFact class +R4924:4928 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R4920:4923 riscv_extras <> size:97 var +binder 4909:4930 <> H:100 +R4935:4939 Sail.Prompt_monad <> monad ind +R4941:4942 riscv_extras <> rv:94 var +R4945:4949 Sail.Values <> mword def +R4953:4955 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R4956:4959 riscv_extras <> size:97 var +R4963:4963 riscv_extras <> e:95 var +R4968:4975 Sail.Prompt_monad <> read_mem def +R5026:5029 riscv_extras <> size:97 var +R5021:5024 riscv_extras <> addr:99 var +R5012:5019 riscv_extras <> addrsize:96 var +R4977:5010 Sail.Instr_kinds <> Read_RISCV_reserved_strong_acquire constr +def 6053:6056 <> MEMw +binder 6059:6060 <> rv:101 +binder 6062:6062 <> e:102 +binder 6065:6072 <> addrsize:103 +binder 6074:6077 <> size:104 +R6094:6098 Sail.Values <> mword def +R6100:6107 riscv_extras <> addrsize:103 var +binder 6080:6085 <> hexRAM:105 +binder 6087:6090 <> addr:106 +R6115:6119 Sail.Values <> mword def +R6123:6125 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R6126:6129 riscv_extras <> size:104 var +binder 6111:6111 <> v:107 +R6162:6166 Sail.Prompt_monad <> monad ind +R6168:6169 riscv_extras <> rv:101 var +R6171:6174 Coq.Init.Datatypes <> bool ind +R6176:6176 riscv_extras <> e:102 var +R6181:6189 Sail.Prompt_monad <> write_mem def +R6222:6222 riscv_extras <> v:107 var +R6217:6220 riscv_extras <> size:104 var +R6212:6215 riscv_extras <> addr:106 var +R6203:6210 riscv_extras <> addrsize:103 var +R6191:6201 Sail.Instr_kinds <> Write_plain constr +def 6236:6247 <> MEMw_release +binder 6250:6251 <> rv:108 +binder 6253:6253 <> e:109 +binder 6256:6263 <> addrsize:110 +binder 6265:6268 <> size:111 +R6285:6289 Sail.Values <> mword def +R6291:6298 riscv_extras <> addrsize:110 var +binder 6271:6276 <> hexRAM:112 +binder 6278:6281 <> addr:113 +R6306:6310 Sail.Values <> mword def +R6314:6316 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R6317:6320 riscv_extras <> size:111 var +binder 6302:6302 <> v:114 +R6345:6349 Sail.Prompt_monad <> monad ind +R6351:6352 riscv_extras <> rv:108 var +R6354:6357 Coq.Init.Datatypes <> bool ind +R6359:6359 riscv_extras <> e:109 var +R6364:6372 Sail.Prompt_monad <> write_mem def +R6413:6413 riscv_extras <> v:114 var +R6408:6411 riscv_extras <> size:111 var +R6403:6406 riscv_extras <> addr:113 var +R6394:6401 riscv_extras <> addrsize:110 var +R6374:6392 Sail.Instr_kinds <> Write_RISCV_release constr +def 6427:6445 <> MEMw_strong_release +binder 6448:6449 <> rv:115 +binder 6451:6451 <> e:116 +binder 6454:6461 <> addrsize:117 +binder 6463:6466 <> size:118 +R6483:6487 Sail.Values <> mword def +R6489:6496 riscv_extras <> addrsize:117 var +binder 6469:6474 <> hexRAM:119 +binder 6476:6479 <> addr:120 +R6504:6508 Sail.Values <> mword def +R6512:6514 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R6515:6518 riscv_extras <> size:118 var +binder 6500:6500 <> v:121 +R6536:6540 Sail.Prompt_monad <> monad ind +R6542:6543 riscv_extras <> rv:115 var +R6545:6548 Coq.Init.Datatypes <> bool ind +R6550:6550 riscv_extras <> e:116 var +R6555:6563 Sail.Prompt_monad <> write_mem def +R6611:6611 riscv_extras <> v:121 var +R6606:6609 riscv_extras <> size:118 var +R6601:6604 riscv_extras <> addr:120 var +R6592:6599 riscv_extras <> addrsize:117 var +R6565:6590 Sail.Instr_kinds <> Write_RISCV_strong_release constr +def 6625:6640 <> MEMw_conditional +binder 6643:6644 <> rv:122 +binder 6646:6646 <> e:123 +binder 6649:6656 <> addrsize:124 +binder 6658:6661 <> size:125 +R6678:6682 Sail.Values <> mword def +R6684:6691 riscv_extras <> addrsize:124 var +binder 6664:6669 <> hexRAM:126 +binder 6671:6674 <> addr:127 +R6699:6703 Sail.Values <> mword def +R6707:6709 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R6710:6713 riscv_extras <> size:125 var +binder 6695:6695 <> v:128 +R6734:6738 Sail.Prompt_monad <> monad ind +R6740:6741 riscv_extras <> rv:122 var +R6743:6746 Coq.Init.Datatypes <> bool ind +R6748:6748 riscv_extras <> e:123 var +R6753:6761 Sail.Prompt_monad <> write_mem def +R6806:6806 riscv_extras <> v:128 var +R6801:6804 riscv_extras <> size:125 var +R6796:6799 riscv_extras <> addr:127 var +R6787:6794 riscv_extras <> addrsize:124 var +R6763:6785 Sail.Instr_kinds <> Write_RISCV_conditional constr +def 6820:6843 <> MEMw_conditional_release +binder 6846:6847 <> rv:129 +binder 6849:6849 <> e:130 +binder 6852:6859 <> addrsize:131 +binder 6861:6864 <> size:132 +R6881:6885 Sail.Values <> mword def +R6887:6894 riscv_extras <> addrsize:131 var +binder 6867:6872 <> hexRAM:133 +binder 6874:6877 <> addr:134 +R6902:6906 Sail.Values <> mword def +R6910:6912 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R6913:6916 riscv_extras <> size:132 var +binder 6898:6898 <> v:135 +R6929:6933 Sail.Prompt_monad <> monad ind +R6935:6936 riscv_extras <> rv:129 var +R6938:6941 Coq.Init.Datatypes <> bool ind +R6943:6943 riscv_extras <> e:130 var +R6948:6956 Sail.Prompt_monad <> write_mem def +R7009:7009 riscv_extras <> v:135 var +R7004:7007 riscv_extras <> size:132 var +R6999:7002 riscv_extras <> addr:134 var +R6990:6997 riscv_extras <> addrsize:131 var +R6958:6988 Sail.Instr_kinds <> Write_RISCV_conditional_release constr +def 7023:7053 <> MEMw_conditional_strong_release +binder 7056:7057 <> rv:136 +binder 7059:7059 <> e:137 +binder 7062:7069 <> addrsize:138 +binder 7071:7074 <> size:139 +R7091:7095 Sail.Values <> mword def +R7097:7104 riscv_extras <> addrsize:138 var +binder 7077:7082 <> hexRAM:140 +binder 7084:7087 <> addr:141 +R7112:7116 Sail.Values <> mword def +R7120:7122 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R7123:7126 riscv_extras <> size:139 var +binder 7108:7108 <> v:142 +R7132:7136 Sail.Prompt_monad <> monad ind +R7138:7139 riscv_extras <> rv:136 var +R7141:7144 Coq.Init.Datatypes <> bool ind +R7146:7146 riscv_extras <> e:137 var +R7151:7159 Sail.Prompt_monad <> write_mem def +R7219:7219 riscv_extras <> v:142 var +R7214:7217 riscv_extras <> size:139 var +R7209:7212 riscv_extras <> addr:141 var +R7200:7207 riscv_extras <> addrsize:138 var +R7161:7198 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr +def 7234:7248 <> shift_bits_left +binder 7251:7251 <> a:143 +binder 7253:7253 <> b:144 +R7261:7265 Sail.Values <> mword def +R7267:7267 riscv_extras <> a:143 var +binder 7257:7257 <> v:145 +R7275:7279 Sail.Values <> mword def +R7281:7281 riscv_extras <> b:144 var +binder 7271:7271 <> n:146 +R7286:7290 Sail.Values <> mword def +R7292:7292 riscv_extras <> a:143 var +R7299:7304 Sail.Operators_mwords <> shiftl def +R7309:7320 Sail.Values <> int_of_mword def +R7328:7328 riscv_extras <> n:146 var +R7322:7326 Coq.Init.Datatypes <> false constr +R7306:7306 riscv_extras <> v:145 var +def 7344:7359 <> shift_bits_right +binder 7362:7362 <> a:147 +binder 7364:7364 <> b:148 +R7372:7376 Sail.Values <> mword def +R7378:7378 riscv_extras <> a:147 var +binder 7368:7368 <> v:149 +R7386:7390 Sail.Values <> mword def +R7392:7392 riscv_extras <> b:148 var +binder 7382:7382 <> n:150 +R7397:7401 Sail.Values <> mword def +R7403:7403 riscv_extras <> a:147 var +R7410:7415 Sail.Operators_mwords <> shiftr def +R7420:7431 Sail.Values <> int_of_mword def +R7439:7439 riscv_extras <> n:150 var +R7433:7437 Coq.Init.Datatypes <> false constr +R7417:7417 riscv_extras <> v:149 var +def 7455:7476 <> shift_bits_right_arith +binder 7479:7479 <> a:151 +binder 7481:7481 <> b:152 +R7489:7493 Sail.Values <> mword def +R7495:7495 riscv_extras <> a:151 var +binder 7485:7485 <> v:153 +R7503:7507 Sail.Values <> mword def +R7509:7509 riscv_extras <> b:152 var +binder 7499:7499 <> n:154 +R7514:7518 Sail.Values <> mword def +R7520:7520 riscv_extras <> a:151 var +R7527:7538 Sail.Operators_mwords <> arith_shiftr def +R7543:7554 Sail.Values <> int_of_mword def +R7562:7562 riscv_extras <> n:154 var +R7556:7560 Coq.Init.Datatypes <> false constr +R7540:7540 riscv_extras <> v:153 var +def 7627:7639 <> internal_pick +binder 7642:7643 <> rv:155 +binder 7645:7645 <> a:156 +binder 7647:7647 <> e:157 +R7656:7659 Coq.Init.Datatypes <> list ind +R7661:7661 riscv_extras <> a:156 var +binder 7651:7652 <> vs:158 +R7666:7670 Sail.Prompt_monad <> monad ind +R7672:7673 riscv_extras <> rv:155 var +R7675:7675 riscv_extras <> a:156 var +R7677:7677 riscv_extras <> e:157 var +R7688:7689 riscv_extras <> vs:158 var +R7700:7701 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not +R7708:7714 Sail.Prompt_monad <> returnm def +R7725:7728 Sail.Prompt_monad <> Fail constr +def 7776:7791 <> undefined_string +binder 7794:7795 <> rv:160 +binder 7797:7797 <> e:161 +R7803:7806 Coq.Init.Datatypes <> unit ind +R7811:7815 Sail.Prompt_monad <> monad ind +R7817:7818 riscv_extras <> rv:160 var +R7820:7825 Coq.Strings.String <> string ind +R7827:7827 riscv_extras <> e:161 var +R7832:7838 Sail.Prompt_monad <> returnm def +def 7862:7875 <> undefined_unit +binder 7878:7879 <> rv:162 +binder 7881:7881 <> e:163 +R7887:7890 Coq.Init.Datatypes <> unit ind +R7895:7899 Sail.Prompt_monad <> monad ind +R7901:7902 riscv_extras <> rv:162 var +R7904:7907 Coq.Init.Datatypes <> unit ind +R7909:7909 riscv_extras <> e:163 var +R7914:7920 Sail.Prompt_monad <> returnm def +R7922:7923 Coq.Init.Datatypes <> tt constr +def 7937:7949 <> undefined_int +binder 7952:7953 <> rv:164 +binder 7955:7955 <> e:165 +R7961:7964 Coq.Init.Datatypes <> unit ind +R7969:7973 Sail.Prompt_monad <> monad ind +R7975:7976 riscv_extras <> rv:164 var +R7978:7978 Coq.Numbers.BinNums <> Z ind +R7980:7980 riscv_extras <> e:165 var +R7985:7991 Sail.Prompt_monad <> returnm def +R7996:7997 Sail.Values <> ii def +def 8097:8112 <> undefined_vector +binder 8115:8116 <> rv:166 +binder 8118:8118 <> a:167 +binder 8120:8120 <> e:168 +binder 8123:8125 <> len:169 +R8132:8132 riscv_extras <> a:167 var +binder 8128:8128 <> u:170 +R8137:8145 Sail.Values <> ArithFact class +R8151:8155 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R8148:8150 riscv_extras <> len:169 var +binder 8137:8157 <> H:171 +R8162:8166 Sail.Prompt_monad <> monad ind +R8168:8169 riscv_extras <> rv:166 var +R8172:8174 Sail.Values <> vec def +R8176:8176 riscv_extras <> a:167 var +R8178:8180 riscv_extras <> len:169 var +R8183:8183 riscv_extras <> e:168 var +R8188:8194 Sail.Prompt_monad <> returnm def +R8197:8204 Sail.Values <> vec_init def +R8208:8210 riscv_extras <> len:169 var +R8206:8206 riscv_extras <> u:170 var +def 8316:8334 <> undefined_bitvector +binder 8337:8338 <> rv:172 +binder 8340:8340 <> e:173 +binder 8343:8345 <> len:174 +R8349:8357 Sail.Values <> ArithFact class +R8363:8367 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not +R8360:8362 riscv_extras <> len:174 var +binder 8349:8369 <> H:175 +R8374:8378 Sail.Prompt_monad <> monad ind +R8380:8381 riscv_extras <> rv:172 var +R8384:8388 Sail.Values <> mword def +R8390:8392 riscv_extras <> len:174 var +R8395:8395 riscv_extras <> e:173 var +R8400:8406 Sail.Prompt_monad <> returnm def +R8409:8420 Sail.Values <> mword_of_int def +def 8523:8536 <> undefined_bits +binder 8539:8540 <> rv:176 +binder 8542:8542 <> e:177 +R8549:8567 riscv_extras <> undefined_bitvector def +R8569:8570 riscv_extras <> rv:176 var +R8572:8572 riscv_extras <> e:177 var +def 8586:8598 <> undefined_bit +binder 8601:8602 <> rv:178 +binder 8604:8604 <> e:179 +R8610:8613 Coq.Init.Datatypes <> unit ind +R8618:8622 Sail.Prompt_monad <> monad ind +R8624:8625 riscv_extras <> rv:178 var +R8627:8630 Sail.Values <> bitU ind +R8632:8632 riscv_extras <> e:179 var +R8637:8643 Sail.Prompt_monad <> returnm def +R8645:8646 Sail.Values <> BU constr +def 8755:8769 <> undefined_range +binder 8772:8773 <> rv:180 +binder 8775:8775 <> e:181 +binder 8778:8778 <> i:182 +binder 8780:8780 <> j:183 +R8784:8792 Sail.Values <> ArithFact class +R8796:8800 Coq.ZArith.BinInt <> ::Z_scope:x_'<=?'_x not +R8795:8795 riscv_extras <> i:182 var +R8801:8801 riscv_extras <> j:183 var +binder 8784:8802 <> H:184 +R8807:8811 Sail.Prompt_monad <> monad ind +R8813:8814 riscv_extras <> rv:180 var +R8816:8816 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R8818:8820 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R8822:8824 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R8850:8850 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R8821:8821 Coq.Numbers.BinNums <> Z ind +binder 8817:8817 <> z:185 +R8825:8833 Sail.Values <> ArithFact class +R8837:8841 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not +R8843:8847 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not +R8836:8836 riscv_extras <> i:182 var +R8842:8842 riscv_extras <> z:185 var +R8842:8842 riscv_extras <> z:185 var +R8848:8848 riscv_extras <> j:183 var +R8852:8852 riscv_extras <> e:181 var +R8857:8863 Sail.Prompt_monad <> returnm def +R8866:8873 Sail.Values <> build_ex def +R8875:8875 riscv_extras <> i:182 var +def 8890:8903 <> undefined_atom +binder 8906:8907 <> rv:186 +binder 8909:8909 <> e:187 +binder 8912:8912 <> i:188 +R8916:8920 Sail.Prompt_monad <> monad ind +R8922:8923 riscv_extras <> rv:186 var +R8925:8925 Coq.Numbers.BinNums <> Z ind +R8927:8927 riscv_extras <> e:187 var +R8932:8938 Sail.Prompt_monad <> returnm def +R8940:8940 riscv_extras <> i:188 var +def 8954:8966 <> undefined_nat +binder 8969:8970 <> rv:189 +binder 8972:8972 <> e:190 +R8978:8981 Coq.Init.Datatypes <> unit ind +R8986:8990 Sail.Prompt_monad <> monad ind +R8992:8993 riscv_extras <> rv:189 var +R8995:8995 Coq.Numbers.BinNums <> Z ind +R8997:8997 riscv_extras <> e:190 var +R9002:9008 Sail.Prompt_monad <> returnm def +R9013:9014 Sail.Values <> ii def +def 9030:9033 <> skip +binder 9036:9037 <> rv:191 +binder 9039:9039 <> e:192 +R9045:9048 Coq.Init.Datatypes <> unit ind +R9053:9057 Sail.Prompt_monad <> monad ind +R9059:9060 riscv_extras <> rv:191 var +R9062:9065 Coq.Init.Datatypes <> unit ind +R9067:9067 riscv_extras <> e:192 var +R9072:9078 Sail.Prompt_monad <> returnm def +R9080:9081 Coq.Init.Datatypes <> tt constr +def 9132:9140 <> elf_entry +R9145:9148 Coq.Init.Datatypes <> unit ind +R9153:9153 Coq.Numbers.BinNums <> Z ind +def 9247:9256 <> print_bits +binder 9259:9259 <> n:193 +binder 9262:9264 <> msg:194 +R9272:9276 Sail.Values <> mword def +R9278:9278 riscv_extras <> n:193 var +binder 9267:9268 <> bs:195 +R9284:9296 Sail.Values <> prerr_endline def +R9302:9306 Coq.Strings.String <> ::string_scope:x_'++'_x not +R9324:9324 Coq.Strings.String <> ::string_scope:x_'++'_x not +R9299:9301 riscv_extras <> msg:194 var +R9307:9320 Sail.Operators_mwords <> string_of_bits def +R9322:9323 riscv_extras <> bs:195 var +def 9378:9388 <> get_time_ns +R9393:9396 Coq.Init.Datatypes <> unit ind +R9401:9401 Coq.Numbers.BinNums <> Z ind +def 9548:9553 <> eq_bit +R9560:9563 Sail.Values <> bitU ind +binder 9556:9556 <> x:196 +R9571:9574 Sail.Values <> bitU ind +binder 9567:9567 <> y:197 +R9579:9582 Coq.Init.Datatypes <> bool ind +R9598:9598 riscv_extras <> y:197 var +R9595:9595 riscv_extras <> x:196 var +R9609:9610 Sail.Values <> B0 constr +R9613:9614 Sail.Values <> B0 constr +R9619:9622 Coq.Init.Datatypes <> true constr +R9628:9629 Sail.Values <> B1 constr +R9632:9633 Sail.Values <> B1 constr +R9638:9641 Coq.Init.Datatypes <> true constr +R9647:9648 Sail.Values <> BU constr +R9651:9652 Sail.Values <> BU constr +R9657:9660 Coq.Init.Datatypes <> true constr +R9673:9677 Coq.Init.Datatypes <> false constr +R9702:9708 Coq.ZArith.Zeuclid <> <> lib +def 9722:9734 <> euclid_modulo +R9743:9743 Coq.Numbers.BinNums <> Z ind +binder 9737:9737 <> m:200 +binder 9739:9739 <> n:201 +R9748:9756 Sail.Values <> ArithFact class +R9760:9763 Coq.ZArith.BinInt <> ::Z_scope:x_'>?'_x not +R9759:9759 riscv_extras <> n:201 var +binder 9748:9765 <> H:202 +R9770:9770 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R9772:9774 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R9776:9778 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R9806:9806 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not +R9775:9775 Coq.Numbers.BinNums <> Z ind +binder 9771:9771 <> z:203 +R9779:9787 Sail.Values <> ArithFact class +R9791:9795 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not +R9797:9801 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not +R9796:9796 riscv_extras <> z:203 var +R9796:9796 riscv_extras <> z:203 var +R9803:9803 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not +R9802:9802 riscv_extras <> n:201 var +R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def +R9815:9820 Coq.Init.Specif <> existT constr +R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def +R9815:9820 Coq.Init.Specif <> existT constr +R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not +R9932:9936 Coq.ZArith.BinInt Z abs def +R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not +R9932:9936 Coq.ZArith.BinInt Z abs def +R9956:9963 Coq.ZArith.BinInt Z abs_eq thm +R9956:9963 Coq.ZArith.BinInt Z abs_eq thm +R9956:9963 Coq.ZArith.BinInt Z abs_eq thm +R9956:9963 Coq.ZArith.BinInt Z abs_eq thm +R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm +R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm +def 10107:10115 <> mults_vec +binder 10118:10118 <> n:204 +R10126:10130 Sail.Values <> mword def +R10132:10132 riscv_extras <> n:204 var +binder 10122:10122 <> l:205 +R10140:10144 Sail.Values <> mword def +R10146:10146 riscv_extras <> n:204 var +binder 10136:10136 <> r:206 +R10151:10155 Sail.Values <> mword def +R10159:10161 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R10162:10162 riscv_extras <> n:204 var +R10168:10176 Sail.Operators_mwords <> mults_vec def +R10180:10180 riscv_extras <> r:206 var +R10178:10178 riscv_extras <> l:205 var +def 10194:10201 <> mult_vec +binder 10204:10204 <> n:207 +R10212:10216 Sail.Values <> mword def +R10218:10218 riscv_extras <> n:207 var +binder 10208:10208 <> l:208 +R10226:10230 Sail.Values <> mword def +R10232:10232 riscv_extras <> n:207 var +binder 10222:10222 <> r:209 +R10237:10241 Sail.Values <> mword def +R10245:10247 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R10248:10248 riscv_extras <> n:207 var +R10254:10261 Sail.Operators_mwords <> mult_vec def +R10265:10265 riscv_extras <> r:209 var +R10263:10263 riscv_extras <> l:208 var +def 10281:10293 <> print_endline +R10298:10303 Coq.Strings.String <> string ind +R10308:10311 Coq.Init.Datatypes <> unit ind +R10316:10317 Coq.Init.Datatypes <> tt constr +def 10331:10343 <> prerr_endline +R10348:10353 Coq.Strings.String <> string ind +R10358:10361 Coq.Init.Datatypes <> unit ind +R10366:10367 Coq.Init.Datatypes <> tt constr +def 10381:10392 <> prerr_string +R10397:10402 Coq.Strings.String <> string ind +R10407:10410 Coq.Init.Datatypes <> unit ind +R10415:10416 Coq.Init.Datatypes <> tt constr +def 10430:10436 <> putchar +binder 10439:10439 <> T:210 +R10445:10445 riscv_extras <> T:210 var +R10450:10453 Coq.Init.Datatypes <> unit ind +R10458:10459 Coq.Init.Datatypes <> tt constr +R10470:10482 Coq.Numbers.DecimalString <> <> lib +def 10496:10508 <> string_of_int +binder 10510:10510 <> z:211 +R10515:10549 Coq.Numbers.DecimalString NilZero string_of_int def +R10552:10559 Coq.ZArith.BinInt Z to_int def +R10561:10561 riscv_extras <> z:211 var +ax 10572:10595 <> sys_enable_writable_misa +R10603:10606 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R10599:10602 Coq.Init.Datatypes <> unit ind +R10607:10610 Coq.Init.Datatypes <> bool ind +ax 10619:10632 <> sys_enable_rvc +R10640:10643 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R10636:10639 Coq.Init.Datatypes <> unit ind +R10644:10647 Coq.Init.Datatypes <> bool ind +ax 10656:10671 <> sys_enable_fdext +R10679:10682 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R10675:10678 Coq.Init.Datatypes <> unit ind +R10683:10686 Coq.Init.Datatypes <> bool ind +ax 10695:10709 <> sys_enable_next +R10717:10720 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R10713:10716 Coq.Init.Datatypes <> unit ind +R10721:10724 Coq.Init.Datatypes <> bool ind +prf 10868:10888 <> n_leading_spaces_fact +binder 10891:10894 <> w__0:216 +R10910:10913 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R10905:10908 Coq.ZArith.BinInt <> ::Z_scope:x_'>='_x not +R10901:10904 riscv_extras <> w__0:216 var +R10914:10920 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not +R10933:10934 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not +R10932:10932 Coq.Numbers.BinNums <> Z ind +binder 10921:10928 <> ex17629_:217 +R10958:10961 Coq.Init.Logic <> ::type_scope:x_'/\'_x not +R10943:10945 Coq.Init.Logic <> ::type_scope:x_'='_x not +R10936:10938 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R10939:10942 riscv_extras <> w__0:216 var +R10947:10949 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R10950:10957 riscv_extras <> ex17629_:217 var +R10963:10966 Coq.ZArith.BinInt <> ::Z_scope:x_'<='_x not +R10967:10974 riscv_extras <> ex17629_:217 var diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem new file mode 100644 index 0000000..15ac8c7 --- /dev/null +++ b/handwritten_support/riscv_extras.lem @@ -0,0 +1,164 @@ +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 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/riscv_extras.v b/handwritten_support/riscv_extras.v new file mode 100644 index 0000000..4b069ec --- /dev/null +++ b/handwritten_support/riscv_extras.v @@ -0,0 +1,154 @@ +Require Import Sail.Base. +Require Import String. +Require Import List. +Import List.ListNotations. +Open Scope Z. + +Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_rw tt). +Definition MEM_fence_r_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_rw tt). +Definition MEM_fence_r_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_r tt). +Definition MEM_fence_rw_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_w tt). +Definition MEM_fence_w_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_w tt). +Definition MEM_fence_w_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_rw tt). +Definition MEM_fence_rw_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_r tt). +Definition MEM_fence_r_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_w tt). +Definition MEM_fence_w_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_r tt). +Definition MEM_fence_tso {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_tso tt). +Definition MEM_fence_i {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_i tt). +(* +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 +*) +Definition MEMea {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_plain addrsize addr size. +Definition MEMea_release {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_release addrsize addr size. +Definition MEMea_strong_release {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_strong_release addrsize addr size. +Definition MEMea_conditional {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_conditional addrsize addr size. +Definition MEMea_conditional_release {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_conditional_release addrsize addr size. +Definition MEMea_conditional_strong_release {rv a e} addrsize (addr : mword a) size : monad rv unit e + := write_mem_ea Write_RISCV_conditional_strong_release addrsize 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 +*) + +Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size. +Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size. +Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size. +Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size. +Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size. +Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := 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 +*) + +Definition MEMw {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_plain addrsize addr size v. +Definition MEMw_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_release addrsize addr size v. +Definition MEMw_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_strong_release addrsize addr size v. +Definition MEMw_conditional {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional addrsize addr size v. +Definition MEMw_conditional_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_release addrsize addr size v. +Definition MEMw_conditional_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_strong_release addrsize addr size v. + +Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a := + shiftl v (int_of_mword false n). + +Definition shift_bits_right {a b} (v : mword a) (n : mword b) : mword a := + shiftr v (int_of_mword false n). + +Definition shift_bits_right_arith {a b} (v : mword a) (n : mword b) : mword a := + arith_shiftr v (int_of_mword false n). + +(* Use constants for undefined values for now *) +Definition internal_pick {rv a e} (vs : list a) : monad rv a e := +match vs with +| (h::_) => returnm h +| _ => Fail "empty list in internal_pick" +end. +Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string. +Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. +Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). +(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) +Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >=? 0)} : monad rv (vec a len) e := returnm (vec_init u len). +(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bitvector {rv e} len `{ArithFact (len >=? 0)} : monad rv (mword len) e := returnm (mword_of_int 0). +(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bits {rv e} := @undefined_bitvector rv e. +Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. +(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) +Definition undefined_range {rv e} i j `{ArithFact (i <=? j)} : monad rv {z : Z & ArithFact (i <=? z <=? j)} e := returnm (build_ex i). +Definition undefined_atom {rv e} i : monad rv Z e := returnm i. +Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). + +Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. + +(*val elf_entry : unit -> integer*) +Definition elf_entry (_:unit) : Z := 0. +(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*) + +Definition print_bits {n} msg (bs : mword n) := prerr_endline (msg ++ (string_of_bits bs)). + +(*val get_time_ns : unit -> integer*) +Definition get_time_ns (_:unit) : Z := 0. +(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*) + +Definition eq_bit (x : bitU) (y : bitU) : bool := + match x, y with + | B0, B0 => true + | B1, B1 => true + | BU, BU => true + | _,_ => false + end. + +Require Import Zeuclid. +Definition euclid_modulo (m n : Z) `{ArithFact (n >? 0)} : {z : Z & ArithFact (0 <=? z <=? n-1)}. +apply existT with (x := ZEuclid.modulo m n). +constructor. +destruct H. +unbool_comparisons. +unbool_comparisons_goal. +assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } +rewrite <- H at 3. +lapply (ZEuclid.mod_always_pos m n); omega. +Qed. + +(* Override the more general version *) + +Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. +Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). + +Axiom sys_enable_writable_misa : unit -> bool. +Axiom sys_enable_rvc : unit -> bool. +Axiom sys_enable_fdext : unit -> bool. +Axiom sys_enable_next : unit -> bool. + +(* The constraint solver can do this itself, but a Coq bug puts + anonymous_subproof into the term instead of an actual subproof. *) +Lemma n_leading_spaces_fact {w__0} : + w__0 >= 0 -> exists ex17629_ : Z, 1 + w__0 = 1 + ex17629_ /\ 0 <= ex17629_. +intro. +exists w__0. +omega. +Qed. +Hint Resolve n_leading_spaces_fact : sail. diff --git a/handwritten_support/riscv_extras.vo b/handwritten_support/riscv_extras.vo new file mode 100644 index 0000000..995df56 Binary files /dev/null and b/handwritten_support/riscv_extras.vo differ diff --git a/handwritten_support/riscv_extras.vok b/handwritten_support/riscv_extras.vok new file mode 100644 index 0000000..e69de29 diff --git a/handwritten_support/riscv_extras.vos b/handwritten_support/riscv_extras.vos new file mode 100644 index 0000000..e69de29 diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem new file mode 100644 index 0000000..12cfe00 --- /dev/null +++ b/handwritten_support/riscv_extras_fdext.lem @@ -0,0 +1,125 @@ +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_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_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_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_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_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f32_to_f64 _ _ = () + +val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit +let softfloat_f64_to_f32 _ _ = () + + +val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_lt _ _ = () + +val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_le _ _ = () + +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_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_le _ _ = () + +val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_eq _ _ = () diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem new file mode 100644 index 0000000..c1c99ed --- /dev/null +++ b/handwritten_support/riscv_extras_sequential.lem @@ -0,0 +1,156 @@ +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_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 = () -- cgit v1.2.3