diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/aarch64_extras_embed_sequential.lem | 121 | ||||
| -rw-r--r-- | aarch64/prelude.sail | 146 |
2 files changed, 207 insertions, 60 deletions
diff --git a/aarch64/aarch64_extras_embed_sequential.lem b/aarch64/aarch64_extras_embed_sequential.lem new file mode 100644 index 00000000..a9e2e9e3 --- /dev/null +++ b/aarch64/aarch64_extras_embed_sequential.lem @@ -0,0 +1,121 @@ +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import Sail_operators +open import State + + +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))) + +let inline uint = unsigned +let inline sint = signed + +let slice v lo len = + subrange_vec_dec v (lo + len - 1) lo + +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 bits = bits_of_int (hi + 1) n in + get_bits false bits hi lo + +let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo) + +let set_slice_int len n lo v = + let hi = lo + len - 1 in + let bits = bitlist_of_int n in + let len_n = max (hi + 1) (integerFromNat (List.length bits)) in + let ext_bits = exts_bits len_n bits in + signed (set_bits false ext_bits 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) +let exts_slice v i j = ext_slice true v i j +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_bitlist c = + if c = #'0' then [B0;B0;B0;B0] + else if c = #'1' then [B0;B0;B0;B1] + else if c = #'2' then [B0;B0;B1;B0] + else if c = #'3' then [B0;B0;B1;B1] + else if c = #'4' then [B0;B1;B0;B0] + else if c = #'5' then [B0;B1;B0;B1] + else if c = #'6' then [B0;B1;B1;B0] + else if c = #'7' then [B0;B1;B1;B1] + else if c = #'8' then [B1;B0;B0;B0] + else if c = #'9' then [B1;B0;B0;B1] + else if c = #'A' then [B1;B0;B1;B0] + else if c = #'a' then [B1;B0;B1;B0] + else if c = #'B' then [B1;B0;B1;B1] + else if c = #'b' then [B1;B0;B1;B1] + else if c = #'C' then [B1;B1;B0;B0] + else if c = #'c' then [B1;B1;B0;B0] + else if c = #'D' then [B1;B1;B0;B1] + else if c = #'d' then [B1;B1;B0;B1] + else if c = #'E' then [B1;B1;B1;B0] + else if c = #'e' then [B1;B1;B1;B0] + else if c = #'F' then [B1;B1;B1;B1] + else if c = #'f' then [B1;B1;B1;B1] + else failwith "hexchar_to_bitlist given unrecognized character" + +let hexstring_to_bits s = + match (toCharList s) with + | z :: x :: hs -> + let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in + List.concat (List.map hexchar_to_bitlist str) + | _ -> failwith "hexstring_to_bits called with unexpected string" + end + +let hex_slice v len lo = + let hi = len + lo - 1 in + let bits = extz_bits (len + lo) (hexstring_to_bits v) in + of_bits (get_bits false bits hi lo) + +let internal_pick vs = head vs + +let undefined_string () = "" +let undefined_unit () = () +let undefined_int () = (0:ii) +let undefined_bool () = false +let undefined_vector len u = repeat [u] len +let undefined_bitvector len = duplicate B0 len +let undefined_bits len = undefined_bitvector len +let undefined_bit () = B0 +let undefined_real () = realFromFrac 0 1 +let undefined_range i j = i +let undefined_atom i = i +let undefined_nat () = (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 = + (*let _ = prerr_endline ("Reading " ^ (stringFromInteger size) ^ " bytes from address " ^ (stringFromInteger (unsigned address))) in*) + (*read_mem false Read_plain address size*) + undefined_bitvector (8 * size) diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index e763fba3..80751672 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -1,85 +1,106 @@ default Order dec -/* type bits ('n : Int) = vector('n, dec, bit) */ type bits ('n : Int) = vector('n, dec, bit) infix 4 == val div = { - smt : "div" + smt : "div", + lem : "integerDiv" } : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm)) val mod = { - smt : "mod" + smt : "mod", + lem : "integerMod" } : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm)) -val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val eq_int = "eq_int" : (int, int) -> bool +val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool -val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool +val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val eq_string = "eq_string" : (string, string) -> bool +val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool -val eq_real = "eq_real" : (real, real) -> bool +val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool -val eq_anything = { ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything" } : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool -val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) +val bitvector_length = {ocaml: "length", lem: "length"} : forall 'n. bits('n) -> atom('n) +val vector_length = {ocaml: "length", lem: "length_list"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) +val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). list('a) -> int + +overload length = {bitvector_length, vector_length, list_length} overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} -val vector_subrange_A = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. +val vector_subrange_A = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) -val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int). +val vector_subrange_B = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int). (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) overload vector_subrange = {vector_subrange_A, vector_subrange_B} -val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. +val bitvector_access_A = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. + (bits('n), atom('m)) -> bit + +val bitvector_access_B = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int). + (bits('n), int) -> bit + +val vector_access_A = {ocaml: "access", lem: "access_list_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a -val vector_access_B = "access" : forall ('n : Int) ('a : Type). +val vector_access_B = {ocaml: "access", lem: "access_list_dec"} : forall ('n : Int) ('a : Type). (vector('n, dec, 'a), int) -> 'a -overload vector_access = {vector_access_A, vector_access_B} +overload vector_access = {bitvector_access_A, bitvector_access_B, vector_access_A, vector_access_B} -val vector_update = "update" : forall 'n ('a : Type). +val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec"} : forall 'n. + (bits('n), int, bit) -> bits('n) + +val vector_update_B = {ocaml: "update", lem: "update_list_dec"} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) -val vector_update_subrange = "update_subrange" : forall 'n 'm 'o. +overload vector_update = {bitvector_update_B, vector_update_B} + +val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) val vcons : forall ('n : Int) ('a : Type). ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) -val append = "append" : forall ('n : Int) ('m : Int) ('a : Type). +val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('n : Int) ('m : Int). + (bits('n), bits('m)) -> bits('n + 'm) + +val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) +overload append = {bitvector_concat, vector_concat} + val not_bool = "not" : bool -> bool val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) overload ~ = {not_bool, not_vec} -val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool +val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool function neq_atom (x, y) = not_bool(eq_atom(x, y)) -val neq_int : (int, int) -> bool +val neq_int = {lem: "neq"} : (int, int) -> bool function neq_int (x, y) = not_bool(eq_int(x, y)) -val neq_vec : forall 'n. (bits('n), bits('n)) -> bool +val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) -val neq_anything : forall ('a : Type). ('a, 'a) -> bool +val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool function neq_anything (x, y) = not_bool(x == y) @@ -87,7 +108,7 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} val and_bool = "and_bool" : (bool, bool) -> bool -val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) +val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -97,7 +118,7 @@ overload operator & = {and_bool, and_vec} val or_bool = "or_bool" : (bool, bool) -> bool -val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) +val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -130,19 +151,19 @@ val __raw_SetSlice_bits : forall 'n 'w. val __raw_GetSlice_bits : forall 'n 'w. (atom('n), atom('w), bits('n), int) -> bits('w) -val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m) +val __ShiftLeft = "shiftl" : forall 'm. (bits('m), int) -> bits('m) -val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) +val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m) -val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) +val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m) -val cast cast_unit_vec : bit -> bits(1) +val cast "cast_unit_vec" : bit -> bits(1) val print = "prerr_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit -val concat_str = "concat_str" : (string, string) -> string +val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string val DecStr : int -> string @@ -152,84 +173,84 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) -val int_power : (int, int) -> int +val int_power = {lem: "pow"} : (int, int) -> int -val real_power = "real_power" : (real, int) -> real +val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real overload operator ^ = {xor_vec, int_power, real_power} -val add_range = "add_int" : forall 'n 'm 'o 'p. +val add_range = {ocaml: "add", lem: "integerAdd"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = "add_int" : (int, int) -> int +val add_int = {ocaml: "add", lem: "integerAdd"} : (int, int) -> int val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) -val add_real = "add_real" : (real, real) -> real +val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} -val sub_range = "sub_int" : forall 'n 'm 'o 'p. +val sub_range = {ocaml: "sub", lem: "integerMinus"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val sub_int = "sub_int" : (int, int) -> int +val sub_int = {ocaml: "sub", lem: "integerMinus"} : (int, int) -> int val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) -val "sub_real" : (real, real) -> real +val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real -val negate_range = "negate" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) +val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) -val negate_int = "negate" : int -> int +val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int -val "negate_real" : real -> real +val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} overload negate = {negate_range, negate_int, negate_real} -val mult_range = "mult" : forall 'n 'm 'o 'p. +val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) -val mult_int = "mult" : (int, int) -> int +val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int -val mult_real = "mult_real" : (real, real) -> real +val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real overload operator * = {mult_range, mult_int, mult_real} -val Sqrt = "sqrt_real" : real -> real +val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real val gteq_int = "gteq" : (int, int) -> bool -val gteq_real = "gteq_real" : (real, real) -> bool +val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool overload operator >= = {gteq_atom, gteq_int, gteq_real} val lteq_int = "lteq" : (int, int) -> bool -val lteq_real = "lteq_real" : (real, real) -> bool +val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool overload operator <= = {lteq_atom, lteq_int, lteq_real} val gt_int = "gt" : (int, int) -> bool -val gt_real = "gt_real" : (real, real) -> bool +val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool overload operator > = {gt_atom, gt_int, gt_real} val lt_int = "lt" : (int, int) -> bool -val lt_real = "lt_real" : (real, real) -> bool +val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool overload operator < = {lt_atom, lt_int, lt_real} -val RoundDown = "round_down" : real -> int +val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int -val RoundUp = "round_up" : real -> int +val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int val abs_int = "abs_int" : int -> int @@ -237,35 +258,35 @@ val abs_real = "abs_real" : real -> real overload abs = {abs_int, abs_real} -val quotient_nat = "quotient" : (nat, nat) -> nat +val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat -val quotient_real = "quotient_real" : (real, real) -> real +val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> real -val quotient = "quotient" : (int, int) -> int +val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int infixl 7 / overload operator / = {quotient_nat, quotient, quotient_real} -val modulus = "modulus" : (int, int) -> int +val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int infixl 7 % overload operator % = {modulus} -val Real = "to_real" : int -> real +val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real val shl_int = "shl_int" : (int, int) -> int val shr_int = "shr_int" : (int, int) -> int -val min_nat = "min_int" : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat -val min_int = "min_int" : (int, int) -> int +val min_int = {ocaml: "min_int", lem: "min"} : (int, int) -> int -val max_nat = "max_int" : (nat, nat) -> nat +val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat -val max_int = "max_int" : (int, int) -> int +val max_int = {ocaml: "max_int", lem: "max"} : (int, int) -> int overload min = {min_nat, min_int} @@ -318,4 +339,9 @@ union exception = { Error_See : string, Error_Implementation_Defined : string, Error_ReservedEncoding -}
\ No newline at end of file +} + +union option ('a : Type) = { + None, + Some : 'a +} |