diff options
| -rw-r--r-- | lib/prelude.sail | 92 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 152 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 6 |
4 files changed, 163 insertions, 89 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 5f809f72..795fe8fc 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -3,17 +3,19 @@ val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed -val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec +val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec" -val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec +val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec" (* Vector access can't actually be properly polymorphic on vector direction because of the ranges being different for each type, so we overload it instead *) val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access [bitvector_access_inc; bitvector_access_dec; vector_access_inc; vector_access_dec] (* Type safe vector subrange *) (* vector_subrange(v, m, o) returns the subvector of v with elements with @@ -27,15 +29,24 @@ val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n val forall Num 'n, Num 'l, Order 'ord. (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl -overload vector_subrange [vector_subrange_inc; vector_subrange_dec; vector_subrange_bl] +val forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure bitvector_subrange_inc + +val forall Num 'n, Num 'l, Num 'm, Num 'o, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,bit>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,bit> effect pure bitvector_subrange_dec + +overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector_subrange_inc; vector_subrange_dec; vector_subrange_bl] (* Type safe vector append *) -val forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append +val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat" val (list<bit>, list<bit>) -> list<bit> effect pure list_append -overload vector_append [vec_append; list_append] +val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat" + +overload vector_append [bitvec_append; vec_append; list_append] (* Implicit register dereferencing *) val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref @@ -101,12 +112,12 @@ val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect p (* Arithmetic *) -val forall Num 'n, Num 'm, Num 'o, Num 'p. +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add -val (nat, nat) -> nat effect pure add_nat +val extern (nat, nat) -> nat effect pure add_nat = "add" -val (int, int) -> int effect pure add_int +val extern (int, int) -> int effect pure add_int = "add" val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec @@ -117,10 +128,10 @@ val forall Num 'n, Num 'o, Order 'ord. val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec -val forall Num 'n, Num 'm, Num 'o, Num 'p. +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub -val (int, int) -> int effect pure sub_int +val extern (int, int) -> int effect pure sub_int = "sub" val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int @@ -148,7 +159,7 @@ overload (deinfix -) [ sub_int ] -val bool -> bit effect pure bool_to_bit +val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU" val (int, int) -> int effect pure mul_int val forall Num 'n, Num 'o, Order 'ord. @@ -166,10 +177,10 @@ overload (deinfix *_s) [ mul_svec ] -val (bool, bool) -> bool effect pure bool_xor +val extern (bool, bool) -> bool effect pure bool_xor -val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec +val extern forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec = "bitwise_xor" overload (deinfix ^) [ bool_xor; @@ -191,7 +202,7 @@ overload (deinfix >>) [ ] (* Boolean operators *) -val bool -> bool effect pure bool_not +val extern bool -> bool effect pure bool_not = "not" val (bool, bool) -> bool effect pure bool_or val (bool, bool) -> bool effect pure bool_and @@ -228,24 +239,24 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_vec val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_vec -val (int, int) -> bool effect pure gteq_int -val (int, int) -> bool effect pure gt_int -val (int, int) -> bool effect pure lteq_int -val (int, int) -> bool effect pure lt_int - -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range - -val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom -val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom -val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom -val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom +val extern (int, int) -> bool effect pure gteq_int = "gteq" +val extern (int, int) -> bool effect pure gt_int = "gt" +val extern (int, int) -> bool effect pure lteq_int = "lteq" +val extern (int, int) -> bool effect pure lt_int = "lt" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom = "lteq" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom = "gteq" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom = "lt" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt" overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int] overload (deinfix >) [gt_atom_atom; gt_vec; gt_int] @@ -266,11 +277,16 @@ val (int, int) -> int effect pure quotient overload (deinfix quot) [quotient] -val (int, int) -> int effect pure modulus +val (int, int) -> int effect pure modulo + +overload (deinfix mod) [modulo] + +val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length" +val forall Type 'a. list<'a> -> nat effect pure list_length -overload (deinfix mod) [modulus] +val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength" -val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure length +overload length [bitvector_length; vector_length; list_length] val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 70850dc1..0944f42b 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -78,6 +78,8 @@ let read_reg_bitfield reg regfield = read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> return (extract_only_element v) +let reg_deref = read_reg + val write_reg_aux : reg_name -> vector bitU -> M unit let write_reg_aux reg_name v = let regval = external_reg_value reg_name v in diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index f148c1ff..f1541466 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -11,6 +11,12 @@ type nn = natural val pow : integer -> integer -> integer let pow m n = m ** (natFromInteger n) +let bool_or (l, r) = (l || r) +let bool_and (l, r) = (l && r) +let bool_xor (l, r) = xor l r + +let list_append (l, r) = l ++ r + let rec replace bs ((n : integer),b') = match bs with | [] -> [] | b :: bs -> @@ -18,6 +24,7 @@ let rec replace bs ((n : integer),b') = match bs with else b :: replace bs (n - 1,b') end +let upper n = n (*** Bits *) type bitU = B0 | B1 | BU @@ -39,6 +46,8 @@ let bitU_to_bool = function | BU -> failwith "to_bool applied to BU" end +let cast_bit_bool = bitU_to_bool + let bit_lifted_of_bitU = function | B0 -> Bitl_zero | B1 -> Bitl_one @@ -196,6 +205,9 @@ let access (Vector bs start is_inc) n = if is_inc then List_extra.nth bs (natFromInteger (n - start)) else List_extra.nth bs (natFromInteger (start - n)) +let vector_access_inc (v, i) = access v i +let vector_access_dec (v, i) = access v i + val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = update_aux v n n [b] @@ -238,9 +250,12 @@ let reset_bitvector_start v = let set_bitvector_start_to_length v = set_bitvector_start (bvlength v - 1) v -let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) = +let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) = Bitvector (word_concat bs bs') start is_inc +let norm_dec = reset_bitvector_start +let adjust_dec = reset_bitvector_start + let inline (^^^) = bitvector_concat val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b @@ -252,6 +267,13 @@ let bvslice (Bitvector bs start is_inc) i j = let subvector_bits = word_extract lo hi bs in Bitvector subvector_bits i is_inc +let bitvector_subrange_inc (v, i, j) = bvslice v i j +let bitvector_subrange_dec (v, i, j) = bvslice v i j + +let vector_subrange_bl (v, i, j) = + let v' = slice (bvec_to_vec v) i j in + get_elems v' + (* this is for the vector slicing introduced in vector-concat patterns: i and j index into the "raw data", the list of bits. Therefore getting the bit list is easy, but the start index has to be transformed to match the old vector start @@ -277,19 +299,20 @@ val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b let bvupdate v i j (Bitvector bs' _ _) = bvupdate_aux v i j bs' -(* TODO: decide between nat/natural, change either here or in machine_word *) -val getBit' : forall 'a. mword 'a -> nat -> bool -let getBit' w n = getBit w (naturalFromNat n) - val bvaccess : forall 'a. bitvector 'a -> integer -> bitU let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU ( - if is_inc then getBit' bs (natFromInteger (n - start)) - else getBit' bs (natFromInteger (start - n))) + if is_inc then getBit bs (natFromInteger (n - start)) + else getBit bs (natFromInteger (start - n))) val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a let bvupdate_pos v n b = bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1) +let bitvector_access_inc (v, i) = bvaccess v i +let bitvector_access_dec (v, i) = bvaccess v i +let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b +let bitvector_update_dec (v, i, j, v') = bvupdate v i j v' + (*** Bit vector operations *) let extract_only_element (Vector elems _ _) = match elems with @@ -308,6 +331,9 @@ let extract_only_bit (Bitvector elems _ _) = else failwith "extract_single_bit called for vector with more bits"*) +let cast_vec_bool v = bitU_to_bool (extract_only_bit v) +let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false) + let pp_bitu_vector (Vector elems start inc) = let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc @@ -409,19 +435,25 @@ end let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) -let to_vec is_inc ((len : integer),(n : integer)) = - let start = if is_inc then 0 else len - 1 in +let to_vec is_inc ((n : integer)) = + (* Bitvector length is determined by return type *) let bits = wordFromInteger n in - if integerFromNat (word_length bits) = len then + let len = integerFromNat (word_length bits) in + let start = if is_inc then 0 else len - 1 in + (*if integerFromNat (word_length bits) = len then*) Bitvector bits start is_inc - else - failwith "Vector length mismatch in to_vec" + (*else + failwith "Vector length mismatch in to_vec"*) let to_vec_big = to_vec let to_vec_inc = to_vec true let to_vec_dec = to_vec false +let cast_0_vec = to_vec_dec +let cast_1_vec = to_vec_dec +let cast_01_vec = to_vec_dec + (* TODO: Think about undefined bit(vector)s *) let to_vec_undef is_inc (len : integer) = Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc @@ -429,19 +461,25 @@ let to_vec_undef is_inc (len : integer) = let to_vec_inc_undef = to_vec_undef true let to_vec_dec_undef = to_vec_undef false -let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec) -let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec) +let exts (vec) = to_vec (bvget_dir vec) (signed vec) +let extz (vec) = to_vec (bvget_dir vec) (unsigned vec) + +let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec) +let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec) -let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec) -let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec) +let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) -let add = integerAdd -let add_signed = integerAdd -let minus = integerMinus -let multiply = integerMult -let modulo = hardware_mod +let add (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub (l,r) = integerMinus l r +let multiply (l,r) = integerMult l r +let quotient (l,r) = integerDiv l r +let modulo (l,r) = hardware_mod l r let quot = hardware_quot -let power = integerPow +let power (l,r) = integerPow l r + +let sub_int = sub +let mul_int = multiply (* TODO: this, and the definitions that use it, currently require Size for to_vec, which I'd rather avoid in favour of library versions; the @@ -449,7 +487,7 @@ let power = integerPow let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r = let (l',r') = (to_num sign l, to_num sign r) in let n = op l' r' in - to_vec is_inc (size * (bvlength l),n) + to_vec is_inc (n) (* add_vec @@ -464,9 +502,15 @@ let minus_VVV = arith_op_vec integerMinus false 1 let mult_VVV = arith_op_vec integerMult false 2 let multS_VVV = arith_op_vec integerMult true 2 +let mul_vec (l, r) = mult_VVV l r +let mul_svec (l, r) = multS_VVV l r + +let add_vec (l, r) = add_VVV l r +let sub_vec (l, r) = minus_VVV l r + val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r = - arith_op_vec op sign size l ((to_vec is_inc (bvlength l,r)) : bitvector 'a) + arith_op_vec op sign size l ((to_vec is_inc (r)) : bitvector 'a) (* add_vec_range * add_vec_range_signed @@ -480,9 +524,12 @@ let minus_VIV = arith_op_vec_range integerMinus false 1 let mult_VIV = arith_op_vec_range integerMult false 2 let multS_VIV = arith_op_vec_range integerMult true 2 +let add_vec_int (l, r) = add_VIV l r +let sub_vec_int (l, r) = minus_VIV l r + val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) = - arith_op_vec op sign size ((to_vec is_inc (bvlength r, l)) : bitvector 'a) r + arith_op_vec op sign size ((to_vec is_inc (l)) : bitvector 'a) r (* add_range_vec * add_range_vec_signed @@ -528,10 +575,10 @@ let arith_op_vec_vec_range op sign l r = let add_VVI = arith_op_vec_vec_range integerAdd false let addS_VVI = arith_op_vec_vec_range integerAdd true -let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l)r = +let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r = let l' = to_num sign l in let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - to_vec is_inc (bvlength l * size,n) + to_vec is_inc (n) (* add_vec_bit * add_vec_bit_signed @@ -610,17 +657,19 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) = let n = natFromInteger n in match op with | LL_shift (*"<<"*) -> - Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc + Bitvector (shiftLeft bs n) start is_inc | RR_shift (*">>"*) -> - Bitvector (shiftRight bs (naturalFromNat n)) start is_inc + Bitvector (shiftRight bs n) start is_inc | LLL_shift (*"<<<"*) -> - Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc + Bitvector (rotateLeft n bs) start is_inc end let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) +let shiftl = bitwise_leftshift + let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 then Nothing @@ -681,19 +730,19 @@ let rec repeat xs n = if n = 0 then [] else xs ++ repeat xs (n-1) -(* -let duplicate bit length = - Vector (repeat [bit] length) (if dir then 0 else length - 1) dir - *) -let compare_op op (l,r) = bool_to_bitU (op l r) +let duplicate (bit, length) = + vec_to_bvec (Vector (repeat [bit] length) (length - 1) false) + +let duplicate_to_list (bit, length) = repeat [bit] length + +let compare_op op (l,r) = (op l r) let lt = compare_op (<) let gt = compare_op (>) let lteq = compare_op (<=) let gteq = compare_op (>=) - let compare_op_vec op sign (l,r) = let (l',r') = (to_num sign l, to_num sign r) in compare_op op (l',r') @@ -712,6 +761,8 @@ let gt_vec_unsigned = compare_op_vec (>) false let lteq_vec_unsigned = compare_op_vec (<=) false let gteq_vec_unsigned = compare_op_vec (>=) false +let lt_svec = lt_vec_signed + let compare_op_vec_range op sign (l,r) = compare_op op ((to_num sign l),r) @@ -728,20 +779,23 @@ let gt_range_vec = compare_op_range_vec (>) true let lteq_range_vec = compare_op_range_vec (<=) true let gteq_range_vec = compare_op_range_vec (>=) true -let eq (l,r) = bool_to_bitU (l = r) -let eq_range (l,r) = bool_to_bitU (l = r) -let eq_vec (l,r) = bool_to_bitU (l = r) -let eq_bit (l,r) = bool_to_bitU (l = r) +val eq : forall 'a. Eq 'a => 'a * 'a -> bool +let eq (l,r) = (l = r) +let eq_range (l,r) = (l = r) + +val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool +let eq_vec (l,r) = (l = r) +let eq_bit (l,r) = (l = r) let eq_vec_range (l,r) = eq (to_num false l,r) let eq_range_vec (l,r) = eq (l, to_num false r) let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) -let neq (l,r) = bitwise_not_bit (eq (l,r)) -let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r)) -let neq_range (l,r) = bitwise_not_bit (eq_range (l,r)) -let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) -let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) -let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) +let neq (l,r) = not (eq (l,r)) +let neq_bit (l,r) = not (eq_bit (l,r)) +let neq_range (l,r) = not (eq_range (l,r)) +let neq_vec (l,r) = not (eq_vec_vec (l,r)) +let neq_vec_range (l,r) = not (eq_vec_range (l,r)) +let neq_range_vec (l,r) = not (eq_range_vec (l,r)) val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a @@ -757,9 +811,9 @@ let make_bitvector_undef length = (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) -let mask (n,bv) = - let len = bvlength bv in - bvslice_raw bv (len - n) (len - 1) +(* TODO *) +val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b +let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 709052fe..1bc1ad55 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -126,7 +126,7 @@ val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a) let read_reg reg state = let v = get_reg state (name_of_reg reg) in [(Left (vec_to_bvec v),state)] -let read_reg_range reg i j state = +(*let read_reg_range reg i j state = let v = slice (get_reg state (name_of_reg reg)) i j in [(Left (vec_to_bvec v),state)] let read_reg_bit reg i state = @@ -137,7 +137,9 @@ let read_reg_field reg regfield = read_reg_range reg i j let read_reg_bitfield reg regfield = let (i,_) = register_field_indices reg regfield in - read_reg_bit reg i + read_reg_bit reg i *) + +let reg_deref = read_reg val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit let write_reg reg v state = |