diff options
Diffstat (limited to 'mips/mips_extras.lem')
| -rw-r--r-- | mips/mips_extras.lem | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem deleted file mode 100644 index 4edb0066..00000000 --- a/mips/mips_extras.lem +++ /dev/null @@ -1,128 +0,0 @@ -open import Pervasives -open import Pervasives_extra -open import Sail2_instr_kinds -open import Sail2_values -open import Sail2_operators -open import Sail2_prompt_monad -open import Sail2_prompt - -val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e -val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e -val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e -val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e - -let MEMr addr size = read_mem Read_plain addr size -let MEMr_reserve addr size = read_mem Read_reserve addr size - -val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e -let read_tag_bool addr = - read_tag addr >>= fun t -> - maybe_fail "read_tag_bool" (bool_of_bitU t) - -val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e -let write_tag_bool addr t = write_tag addr (bitU_of_bool t) >>= fun _ -> return () - -let MEMr_tag addr size = - read_mem Read_plain addr size >>= fun v -> - read_tag_bool addr >>= fun t -> - return (t, v) - -let MEMr_tag_reserve addr size = - read_mem Read_plain addr size >>= fun v -> - read_tag_bool addr >>= fun t -> - return (t, v) - - -val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e -val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e -val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e -val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e - -let MEMea addr size = write_mem_ea Write_plain addr size -let MEMea_conditional addr size = write_mem_ea Write_conditional addr size - -let MEMea_tag addr size = write_mem_ea Write_plain addr size -let MEMea_tag_conditional addr size = write_mem_ea Write_conditional addr size - - -val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e -val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e -val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e -val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e - -let MEMval _ size v = write_mem_val v >>= fun _ -> return () -let MEMval_conditional _ size v = write_mem_val v >>= fun b -> return (if b then true else false) -let MEMval_tag addr size t v = write_mem_val v >>= fun _ -> write_tag_bool addr t >>= fun _ -> return () -let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag_bool addr t >>= fun _ -> return (if b then true else false) - -val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e - -let MEM_sync () = barrier Barrier_MIPS_SYNC - -(* Some wrappers copied from aarch64_extras *) -(* TODO: Harmonise into a common library *) - -let get_slice_int_bl len n lo = - (* TODO: Is this the intended behaviour? *) - let hi = lo + len - 1 in - let bs = bools_of_int (hi + 1) n in - subrange_list false bs hi lo - -val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo) - -let write_ram _ size _ addr data = - MEMea addr size >> - MEMval addr size data - -let read_ram _ size _ addr = MEMr addr size - -let string_of_int = show - -let shift_bits_left v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in - maybe_fail "shift_bits_left" r -let shift_bits_right v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in - maybe_fail "shift_bits_right" r -let shift_bits_right_arith v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in - maybe_fail "shift_bits_right_arith" r - -(* Use constants for undefined values for now *) -let undefined_string () = return "" -let undefined_unit () = return () -let undefined_int () = return (0:ii) -val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e -let undefined_vector len u = return (repeat [u] len) -val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e -let undefined_bitvector len = return (of_bools (repeat [false] len)) -val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e -let undefined_bits = undefined_bitvector -let undefined_bit () = return B0 -let undefined_real () = return (realFromFrac 0 1) -let undefined_range i j = return i -let undefined_atom i = return i -let undefined_nat () = return (0:ii) - -let skip () = return () - -val elf_entry : unit -> integer -let elf_entry () = 0 -declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` - -let print_bits msg bs = print_endline (msg ^ (string_of_bv bs)) -let prerr_bits msg bs = prerr_endline (msg ^ (string_of_bv bs)) - -val prerr_string : string -> unit -let prerr_string _ = () -declare ocaml target_rep function prerr_string = `Pervasives.prerr_string` - -val get_time_ns : unit -> integer -let get_time_ns () = 0 -declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))` - -val cycle_count : unit -> unit -let cycle_count _ = () - -let inline eq_bit = eq |