1 files changed, 136 insertions, 0 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
new file mode 100644
index 00000000..58f1b9c7
--- /dev/null
+++ b/aarch64/aarch64_extras.lem
@@ -0,0 +1,136 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_bitlists
+open import Prompt_monad
+open import Prompt
+
+type ty512
+instance (Size ty512) let size = 512 end
+declare isabelle target_rep type ty512 = `512`
+type ty1024
+instance (Size ty1024) let size = 1024 end
+declare isabelle target_rep type ty1024 = `1024`
+type ty2048
+instance (Size ty2048) let size = 2048 end
+declare isabelle target_rep type ty2048 = `2048`
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
+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 : integer -> integer -> integer -> list bitU
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bit_list_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
+  let ext_bs = exts_bits len_n bs in
+  maybe_failwith (signed (update_subrange_list false ext_bs hi lo (bits_of v)))
+
+(*let ext_slice signed v i j =
+  let len = length v in
+  let bits = get_bits false (bits_of v) i j in
+  of_bits (if signed then exts_bits len bits else extz_bits len bits)
+val exts_slice : list bitU -> integer -> integer -> list bitU
+let exts_slice v i j = ext_slice true v i j
+val extz_slice : list bitU -> integer -> integer -> list bitU
+let extz_slice v i j = ext_slice false v i j*)
+
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
+let hexchar_to_bool_list c =
+  if c = #'0' then      Just ([false;false;false;false])
+  else if c = #'1' then Just ([false;false;false;true ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools s =
+  match (toCharList s) with
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
+  end
+
+val hex_slice : forall 'rv 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
+let hex_slice v len lo =
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* 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 'e. integer -> monad 'rv (list bitU) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) '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 write_ram addrsize size hexRAM address value =
+  write_mem_ea Write_plain address size >>
+  write_mem_val value >>= fun _ ->
+  return ()
+
+let read_ram addrsize size hexRAM address =
+  read_mem Read_plain address size