diff options
Diffstat (limited to 'handwritten_support/riscv_extras.lem')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 107 |
1 files changed, 57 insertions, 50 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index ed572be..993ab4b 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -6,8 +6,6 @@ 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 @@ -20,12 +18,12 @@ 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 +val MEMea : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e +val MEMea_release : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e +val MEMea_strong_release : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e +val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => mword '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 @@ -35,35 +33,44 @@ let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_ 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 MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e - -let MEMw addrsize size hexRAM addr = write_mem Write_plain addr size -let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addr size -let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addr size -let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addr size -let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addr size -let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addr size - -val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +val read_memt_bool : forall 'rv 'a 'b 'e. Size 'a, Size 'b => read_kind -> mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +let read_memt_bool rk addr size = + read_memt rk addr size >>= fun (data, tag) -> + maybe_fail "read_memt" (bool_of_bitU tag) >>= fun tag -> + return (tag, data) + +val ReadMemT : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +val ReadMemT_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +val ReadMemT_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +val ReadMemT_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +val ReadMemT_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e +val ReadMemT_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e + +let ReadMemT addr size = read_memt_bool Read_plain addr size +let ReadMemT_acquire addr size = read_memt_bool Read_RISCV_acquire addr size +let ReadMemT_strong_acquire addr size = read_memt_bool Read_RISCV_strong_acquire addr size +let ReadMemT_reserved addr size = read_memt_bool Read_RISCV_reserved addr size +let ReadMemT_reserved_acquire addr size = read_memt_bool Read_RISCV_reserved_acquire addr size +let ReadMemT_reserved_strong_acquire addr size = read_memt_bool Read_RISCV_reserved_strong_acquire addr size + +val write_memt_bool : forall 'rv 'a 'b 'e. Size 'a, Size 'b => write_kind -> mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +let write_memt_bool wk addr size tag data = write_memt wk addr size data (bitU_of_bool tag) + +val WriteMemT : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +val WriteMemT_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +val WriteMemT_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +val WriteMemT_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +val WriteMemT_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e +val WriteMemT_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e + +let WriteMemT addr size tag data = write_memt_bool Write_plain addr size tag data +let WriteMemT_release addr size tag data = write_memt_bool Write_RISCV_release addr size tag data +let WriteMemT_strong_release addr size tag data = write_memt_bool Write_RISCV_strong_release addr size tag data +let WriteMemT_conditional addr size tag data = write_memt_bool Write_RISCV_conditional addr size tag data +let WriteMemT_conditional_release addr size tag data = write_memt_bool Write_RISCV_conditional_release addr size tag data +let WriteMemT_conditional_strong_release addr size tag data = write_memt_bool Write_RISCV_conditional_strong_release addr size tag data + +val load_reservation : forall 'a. Size 'a => mword 'a -> unit let load_reservation addr = () let speculate_conditional_success () = excl_result () @@ -71,27 +78,27 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () -val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a +val plat_ram_base : forall 'a. Size 'a => unit -> mword '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 +val plat_ram_size : forall 'a. Size 'a => unit -> mword '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 +val plat_rom_base : forall 'a. Size 'a => unit -> mword '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 +val plat_rom_size : forall 'a. Size 'a => unit -> mword '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 +val plat_clint_base : forall 'a. Size 'a => unit -> mword '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 +val plat_clint_size : forall 'a. Size 'a => unit -> mword 'a let plat_clint_size () = wordFromInteger 0 declare ocaml target_rep function plat_clint_size = `Platform.clint_size` @@ -111,21 +118,21 @@ 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 +val plat_htif_tohost : forall 'a. Size 'a => unit -> mword '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 +val plat_term_write : forall 'a. Size 'a => mword '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 +val plat_term_read : forall 'a. Size 'a => unit -> mword '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 +val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'b -> mword '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 +val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'b -> mword 'a let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit @@ -134,8 +141,8 @@ let print_string msg s = () (* print_endline (msg ^ s) *) val prerr_string : string -> string -> unit let prerr_string msg s = prerr_endline (msg ^ s) -val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +val prerr_bits : forall 'a. Size 'a => string -> mword '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 +val print_bits : forall 'a. Size 'a => string -> mword 'a -> unit let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) |