diff options
Diffstat (limited to 'src')
45 files changed, 3219 insertions, 1158 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index d7318567..5dbdb157 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -343,12 +343,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let quot_signed = hardware_quot diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index e2ddd3e9..d160e84a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -24,6 +24,8 @@ type value = exception Sail_exit exception Sail_return +let _print s = print_string s + let string_of_bit = function | Vone -> "1" | Vzero -> "0" @@ -331,6 +333,8 @@ let most_significant = function | Vregister(array,_,_,_,_) -> !array.(0) | _ -> assert false +let _most_significant = most_significant + let bitwise_not_bit = function | Vone -> Vzero | Vzero -> Vone @@ -466,22 +470,25 @@ let min_32 = big_int_of_int (-2147483648) let max_8 = big_int_of_int 127 let min_8 = big_int_of_int (-128) let max_5 = big_int_of_int 31 -let min_5 = big_int_of_int (-32) let get_max_representable_in sign n = - if (n = 64) then match sign with | true -> max_64 | false -> max_64u - else if (n=32) then match sign with | true -> max_32 | false -> max_32u - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | true -> power_big two_big_int (pred_big_int (big_int_of_int n)) - | false -> power_big two_big_int (big_int_of_int n) - -let get_min_representable_in _ n = - if (n = 64) then min_64 - else if (n=32) then min_32 - else if (n=8) then min_8 - else if (n=5) then min_5 - else minus_big_int (power_big two_big_int (big_int_of_int n)) + match (sign, n) with + | (true, 64) -> max_64 + | (false, 64) -> max_64u + | (true, 32) -> max_32 + | (false, 32) -> max_32u + | (true, 8) -> max_8 + | (false, 5) -> max_5 + | (true, _) -> pred_big_int (power_big two_big_int (big_int_of_int (n-1))) + | (false, _) -> pred_big_int (power_big two_big_int (big_int_of_int n)) + +let get_min_representable_in sign n = + match (sign, n) with + | (false, _) -> zero_big_int + | (true, 64) -> min_64 + | (true, 32) -> min_32 + | (true, 8) -> min_8 + | (true, _) -> minus_big_int (power_big two_big_int (big_int_of_int (n-1))) let to_vec_int ord len n = let array = Array.make len Vzero in @@ -603,6 +610,9 @@ let min_int = min (* the built-in version *) let min = min_big (* is overwritten here *) let max_int = max (* likewise *) let max = max_big +let abs_int = abs +let abs_big = abs_big_int +let abs = abs_big let arith_op_vec_big op sign size (l,r) = let ord = get_ord l in @@ -910,8 +920,8 @@ let rec arith_op_no0_big op (l,r) = then None else Some (op l r) -let modulo_no0_big = arith_op_no0_big mod_big_int -let quot_no0_big = arith_op_no0_big div_big_int +let modulo_no0_big = arith_op_no0_big (Z.rem) +let quot_no0_big = arith_op_no0_big (Z.div) let rec arith_op_no0_int op (l,r) = if r = 0 @@ -960,9 +970,9 @@ let rec arith_op_vec_no0_big op sign size (l,r) = Vvector((Array.make act_size Vundef), start, ord) | _ -> assert false -let mod_vec_big = arith_op_vec_no0_big mod_big_int false unit_big_int -let quot_vec_big = arith_op_vec_no0_big div_big_int false unit_big_int -let quot_vec_signed_big = arith_op_vec_no0_big div_big_int true unit_big_int +let mod_vec_big = arith_op_vec_no0_big (Z.rem) false unit_big_int +let quot_vec_big = arith_op_vec_no0_big (Z.div) false unit_big_int +let quot_vec_signed_big = arith_op_vec_no0_big (Z.div) true unit_big_int let mod_vec = mod_vec_big let quot_vec = quot_vec_big @@ -1021,8 +1031,8 @@ let arith_op_overflow_no0_vec_big op sign size (l,r) = let overflow = if representable then Vzero else Vone in (correct_size_num,overflow,most_significant one_more) -let quot_overflow_vec_big = arith_op_overflow_no0_vec_big div_big_int false unit_big_int -let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big div_big_int true unit_big_int +let quot_overflow_vec_big = arith_op_overflow_no0_vec_big (Z.div) false unit_big_int +let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big (Z.div) true unit_big_int let quot_overflow_vec = quot_overflow_vec_big let quot_overflow_vec_signed = quot_overflow_vec_signed_big @@ -1038,7 +1048,7 @@ let arith_op_vec_range_no0_big op sign size (l,r) = let ord = get_ord l in arith_op_vec_no0_big op sign size (l,(to_vec_big ord (length_big l) r)) -let mod_vec_range_big = arith_op_vec_range_no0_big mod_big_int false unit_big_int +let mod_vec_range_big = arith_op_vec_range_no0_big (Z.rem) false unit_big_int let mod_vec_range = mod_vec_range_big @@ -1051,6 +1061,15 @@ let duplicate_big (bit,length) = let duplicate = duplicate_big +let duplicate_bits_big (bits, x) = + let len = (length_int bits) * (int_of_big_int x) in + let is_inc = get_ord bits in + let bits_arr = get_barray bits in + let arr = Array.concat (Array.to_list(Array.make (int_of_big_int x) bits_arr)) in + Vvector(arr, (if is_inc then 0 else (len - 1)), is_inc) + +let duplicate_bits = duplicate_bits_big + let compare_op op (l,r) = if (op l r) then Vone diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem new file mode 100644 index 00000000..048bf30a --- /dev/null +++ b/src/gen_lib/sail_values_word.lem @@ -0,0 +1,1030 @@ +(* Version of sail_values.lem that uses Lem's machine words library *) + +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base + + +type ii = integer +type nn = natural + +val pow : integer -> integer -> integer +let pow m n = m ** (natFromInteger n) + +let rec replace bs ((n : integer),b') = match bs with + | [] -> [] + | b :: bs -> + if n = 0 then b' :: bs + else b :: replace bs (n - 1,b') + end + + +(*** Bits *) +type bitU = B0 | B1 | BU + +let showBitU = function + | B0 -> "O" + | B1 -> "I" + | BU -> "U" +end + +instance (Show bitU) + let show = showBitU +end + + +let bitU_to_bool = function + | B0 -> false + | B1 -> true + | BU -> failwith "to_bool applied to BU" + end + +let bit_lifted_of_bitU = function + | B0 -> Bitl_zero + | B1 -> Bitl_one + | BU -> Bitl_undef + end + +let bitU_of_bit = function + | Bitc_zero -> B0 + | Bitc_one -> B1 + end + +let bit_of_bitU = function + | B0 -> Bitc_zero + | B1 -> Bitc_one + | BU -> failwith "bit_of_bitU: BU" + end + +let bitU_of_bit_lifted = function + | Bitl_zero -> B0 + | Bitl_one -> B1 + | Bitl_undef -> BU + | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" + end + +let bitwise_not_bit = function + | B1 -> B0 + | B0 -> B1 + | BU -> BU + end + +let inline (~) = bitwise_not_bit + +val is_one : integer -> bitU +let is_one i = + if i = 1 then B1 else B0 + +let bool_to_bitU b = if b then B1 else B0 + +let bitwise_binop_bit op = function + | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) + | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) + | (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y)) + end + +val bitwise_and_bit : bitU * bitU -> bitU +let bitwise_and_bit = bitwise_binop_bit (&&) + +val bitwise_or_bit : bitU * bitU -> bitU +let bitwise_or_bit = bitwise_binop_bit (||) + +val bitwise_xor_bit : bitU * bitU -> bitU +let bitwise_xor_bit = bitwise_binop_bit xor + +val (&.) : bitU -> bitU -> bitU +let inline (&.) x y = bitwise_and_bit (x,y) + +val (|.) : bitU -> bitU -> bitU +let inline (|.) x y = bitwise_or_bit (x,y) + +val (+.) : bitU -> bitU -> bitU +let inline (+.) x y = bitwise_xor_bit (x,y) + + + +(*** Vectors *) + +(* element list * start * has increasing direction *) +type vector 'a = Vector of list 'a * integer * bool + +let showVector (Vector elems start inc) = + "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc + +let get_dir (Vector _ _ ord) = ord +let get_start (Vector _ s _) = s +let get_elems (Vector elems _ _) = elems +let length (Vector bs _ _) = integerFromNat (length bs) + +instance forall 'a. Show 'a => (Show (vector 'a)) + let show = showVector +end + +let dir is_inc = if is_inc then D_increasing else D_decreasing +let bool_of_dir = function + | D_increasing -> true + | D_decreasing -> false + end + +(*** Vector operations *) + +val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a +let set_vector_start new_start (Vector bs _ is_inc) = + Vector bs new_start is_inc + +let reset_vector_start v = + set_vector_start (if (get_dir v) then 0 else (length v - 1)) v + +let set_vector_start_to_length v = + set_vector_start (length v - 1) v + +let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = + Vector (bs ++ bs') start is_inc + +let inline (^^) = vector_concat + +val sublist : forall 'a. list 'a -> (nat * nat) -> list 'a +let sublist xs (i,j) = + let (toJ,_suffix) = List.splitAt (j+1) xs in + let (_prefix,fromItoJ) = List.splitAt i toJ in + fromItoJ + +val update_sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -> list 'a +let update_sublist xs (i,j) xs' = + let (toJ,suffix) = List.splitAt (j+1) xs in + let (prefix,_fromItoJ) = List.splitAt i toJ in + prefix ++ xs' ++ suffix + +val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a +let slice (Vector bs start is_inc) i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let subvector_bits = + sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in + Vector subvector_bits i is_inc + +(* 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 +and the direction. *) +val slice_raw : forall 'a. vector 'a -> integer -> integer -> vector 'a +let slice_raw (Vector bs start is_inc) i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + let bits = sublist bs (iN,jN) in + let len = integerFromNat (List.length bits) in + Vector bits (if is_inc then 0 else len - 1) is_inc + + +val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a +let update_aux (Vector bs start is_inc) i j bs' = + let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let bits = + (update_sublist bs) + (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in + Vector bits start is_inc + +val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a +let update v i j (Vector bs' _ _) = + update_aux v i j bs' + +val access : forall 'a. vector 'a -> integer -> 'a +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)) + +val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a +let update_pos v n b = + update_aux v n n [b] + +(*** Bitvectors *) + +(* element list * start * has increasing direction *) +type bitvector 'a = Bitvector of mword 'a * integer * bool + +let showBitvector (Bitvector elems start inc) = + "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc + +let bvget_dir (Bitvector _ _ ord) = ord +let bvget_start (Bitvector _ s _) = s +let bvget_elems (Bitvector elems _ _) = elems +let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs) + +instance forall 'a. Show 'a => (Show (bitvector 'a)) + let show = showBitvector +end + +(*** Vector operations *) + +val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a +let set_bitvector_start new_start (Bitvector bs _ is_inc) = + Bitvector bs new_start is_inc + +let reset_bitvector_start v = + set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) 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' _ _) = + Bitvector (word_concat bs bs') start is_inc + +let inline (^^^) = bitvector_concat + +val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b +let bvslice (Bitvector bs start is_inc) i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in + let subvector_bits = word_extract lo hi bs in + Bitvector subvector_bits i is_inc + +(* 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 +and the direction. *) +val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b +let bvslice_raw (Bitvector bs start is_inc) i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + let bits = word_extract iN jN bs in + let len = integerFromNat (word_length bits) in + Bitvector bits (if is_inc then 0 else len - 1) is_inc + +val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a +let bvupdate_aux (Bitvector bs start is_inc) i j bs' = + let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in + let bits = word_update bs lo hi bs' in + Bitvector bits start is_inc + +val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a +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 -> bool +let bvaccess (Bitvector bs start is_inc) 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 -> bool -> bitvector 'a +let bvupdate_pos v n b = + bvupdate_aux v n n (wordFromNatural (if b then 1 else 0)) + +(*** Bit vector operations *) + +let extract_only_bit (Bitvector elems _ _) = + let l = word_length elems in + if l = 1 then + msb elems + else if l = 0 then + failwith "extract_single_bit called for empty vector" + else + failwith "extract_single_bit called for vector with more bits" + +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 + + +let most_significant (Bitvector v _ _) = + if word_length v = 0 then + failwith "most_significant applied to empty vector" + else + msb v + +let bitwise_not_bitlist = List.map bitwise_not_bit + +let bitwise_not (Bitvector bs start is_inc) = + Bitvector (lNot bs) start is_inc + +let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) = + Bitvector (op bsl bsr) start is_inc + +let bitwise_and = bitwise_binop lAnd +let bitwise_or = bitwise_binop lOr +let bitwise_xor = bitwise_binop lXor + +let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs +let unsigned_big = unsigned + +let signed (Bitvector v _ _) : integer = signedIntegerFromWord v + +let hardware_mod (a: integer) (b:integer) : integer = + if a < 0 && b < 0 + then (abs a) mod (abs b) + else if (a < 0 && b >= 0) + then (a mod b) - b + else a mod b + +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) +let hardware_quot (a:integer) (b:integer) : integer = + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) + +let quot_signed = hardware_quot + + +let signed_big = signed + +let to_num sign = if sign then signed else unsigned + +let max_64u = (integerPow 2 64) - 1 +let max_64 = (integerPow 2 63) - 1 +let min_64 = 0 - (integerPow 2 63) +let max_32u = (4294967295 : integer) +let max_32 = (2147483647 : integer) +let min_32 = (0 - 2147483648 : integer) +let max_8 = (127 : integer) +let min_8 = (0 - 128 : integer) +let max_5 = (31 : integer) +let min_5 = (0 - 32 : integer) + +let get_max_representable_in sign (n : integer) : integer = + if (n = 64) then match sign with | true -> max_64 | false -> max_64u end + else if (n=32) then match sign with | true -> max_32 | false -> max_32u end + else if (n=8) then max_8 + else if (n=5) then max_5 + else match sign with | true -> integerPow 2 ((natFromInteger n) -1) + | false -> integerPow 2 (natFromInteger n) + end + +let get_min_representable_in _ (n : integer) : integer = + if n = 64 then min_64 + else if n = 32 then min_32 + else if n = 8 then min_8 + else if n = 5 then min_5 + else 0 - (integerPow 2 (natFromInteger n)) + +val to_bin_aux : natural -> list bitU +let rec to_bin_aux x = + if x = 0 then [] + else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) +let to_bin n = List.reverse (to_bin_aux n) + +val pad_zero : list bitU -> integer -> list bitU +let rec pad_zero bits n = + if n = 0 then bits else pad_zero (B0 :: bits) (n -1) + + +let rec add_one_bit_ignore_overflow_aux bits = match bits with + | [] -> [] + | B0 :: bits -> B1 :: bits + | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits + | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +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 bits = wordFromInteger n in + if integerFromNat (word_length bits) = len then + Bitvector bits start is_inc + 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 +(* TODO?? +let to_vec_undef is_inc (len : integer) = + Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc + +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_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 add = integerAdd +let add_signed = integerAdd +let minus = integerMinus +let multiply = integerMult +let modulo = hardware_mod +let quot = hardware_quot +let power = integerPow + +(* TODO: this, and the definitions that use it, currently requires Size for + to_vec, which I'd rather avoid *) +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) + + +(* add_vec + * add_vec_signed + * minus_vec + * multiply_vec + * multiply_vec_signed + *) +let add_VVV = arith_op_vec integerAdd false 1 +let addS_VVV = arith_op_vec integerAdd true 1 +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 + +val arith_op_vec_range : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'a +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)) + +(* add_vec_range + * add_vec_range_signed + * minus_vec_range + * mult_vec_range + * mult_vec_range_signed + *) +let add_VIV = arith_op_vec_range integerAdd false 1 +let addS_VIV = arith_op_vec_range integerAdd true 1 +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 + +val arith_op_range_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'a +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)) r + +(* add_range_vec + * add_range_vec_signed + * minus_range_vec + * mult_range_vec + * mult_range_vec_signed + *) +let add_IVV = arith_op_range_vec integerAdd false 1 +let addS_IVV = arith_op_range_vec integerAdd true 1 +let minus_IVV = arith_op_range_vec integerMinus false 1 +let mult_IVV = arith_op_range_vec integerMult false 2 +let multS_IVV = arith_op_range_vec integerMult true 2 + +let arith_op_range_vec_range op sign l r = op l (to_num sign r) + +(* add_range_vec_range + * add_range_vec_range_signed + * minus_range_vec_range + *) +let add_IVI = arith_op_range_vec_range integerAdd false +let addS_IVI = arith_op_range_vec_range integerAdd true +let minus_IVI = arith_op_range_vec_range integerMinus false + +let arith_op_vec_range_range op sign l r = op (to_num sign l) r + +(* add_vec_range_range + * add_vec_range_range_signed + * minus_vec_range_range + *) +let add_VII = arith_op_vec_range_range integerAdd false +let addS_VII = arith_op_vec_range_range integerAdd true +let minus_VII = arith_op_vec_range_range integerMinus false + + + +let arith_op_vec_vec_range op sign l r = + let (l',r') = (to_num sign l,to_num sign r) in + op l' r' + +(* add_vec_vec_range + * add_vec_vec_range_signed + *) +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 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) + +(* add_vec_bit + * add_vec_bit_signed + * minus_vec_bit_signed + *) +let add_VBV = arith_op_vec_bit integerAdd false 1 +let addS_VBV = arith_op_vec_bit integerAdd true 1 +let minus_VBV = arith_op_vec_bit integerMinus true 1 + +val arith_op_overflow_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'a * bitU * bool +let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r = + let len = bvlength l in + let act_size = len * size in + let (l_sign,r_sign) = (to_num sign l,to_num sign r) in + let (l_unsign,r_unsign) = (to_num false l,to_num false r) in + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size_num = to_vec is_inc (act_size,n) in + let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size_num,overflow,c_out) + +(* add_overflow_vec + * add_overflow_vec_signed + * minus_overflow_vec + * minus_overflow_vec_signed + * mult_overflow_vec + * mult_overflow_vec_signed + *) +let addO_VVV = arith_op_overflow_vec integerAdd false 1 +let addSO_VVV = arith_op_overflow_vec integerAdd true 1 +let minusO_VVV = arith_op_overflow_vec integerMinus false 1 +let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 +let multO_VVV = arith_op_overflow_vec integerMult false 2 +let multSO_VVV = arith_op_overflow_vec integerMult true 2 + +val arith_op_overflow_vec_bit : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> + bitvector 'a -> bitU -> bitvector 'a * bitU * bool +let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) + (Bitvector _ _ is_inc as l) r_bit = + let act_size = bvlength l * size in + let l' = to_num sign l in + let l_u = to_num false l in + let (n,nu,changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l',l_u,false) + | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" + end in +(* | _ -> assert false *) + let correct_size_num = to_vec is_inc (act_size,n) in + let one_larger = to_vec is_inc (act_size + 1,nu) in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size_num,overflow,most_significant one_larger) + +(* add_overflow_vec_bit_signed + * minus_overflow_vec_bit + * minus_overflow_vec_bit_signed + *) +let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 +let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 +let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 + +type shift = LL_shift | RR_shift | LLL_shift + +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 + | RR_shift (*">>"*) -> + Bitvector (shiftRight bs (naturalFromNat n)) start is_inc + | LLL_shift (*"<<<"*) -> + Bitvector (rotateLeft (naturalFromNat 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 rec arith_op_no0 (op : integer -> integer -> integer) l r = + if r = 0 + then Nothing + else Just (op l r) +(* TODO +let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r = + let act_size = bvlength l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let n = arith_op_no0 op l' r' in + let (representable,n') = + match n with + | Just n' -> + (n' <= get_max_representable_in sign act_size && + n' >= get_min_representable_in sign act_size, n') + | _ -> (false,0) + end in + if representable + then to_vec is_inc (act_size,n') + else Vector (List.replicate (natFromInteger act_size) BU) start is_inc + +let mod_VVV = arith_op_vec_no0 hardware_mod false 1 +let quot_VVV = arith_op_vec_no0 hardware_quot false 1 +let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 + +let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = + let rep_size = length r * size in + let act_size = length l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let (l_u,r_u) = (to_num false l,to_num false r) in + let n = arith_op_no0 op l' r' in + let n_u = arith_op_no0 op l_u r_u in + let (representable,n',n_u') = + match (n, n_u) with + | (Just n',Just n_u') -> + ((n' <= get_max_representable_in sign rep_size && + n' >= (get_min_representable_in sign rep_size)), n', n_u') + | _ -> (true,0,0) + end in + let (correct_size_num,one_more) = + if representable then + (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) + else + (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, + Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in + let overflow = if representable then B0 else B1 in + (correct_size_num,overflow,most_significant one_more) + +let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 +let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 + +let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = + arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) + +let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 +*) +val repeat : forall 'a. list 'a -> integer -> list 'a +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 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') + +let lt_vec = compare_op_vec (<) true +let gt_vec = compare_op_vec (>) true +let lteq_vec = compare_op_vec (<=) true +let gteq_vec = compare_op_vec (>=) true + +let lt_vec_signed = compare_op_vec (<) true +let gt_vec_signed = compare_op_vec (>) true +let lteq_vec_signed = compare_op_vec (<=) true +let gteq_vec_signed = compare_op_vec (>=) true +let lt_vec_unsigned = compare_op_vec (<) false +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 compare_op_vec_range op sign (l,r) = + compare_op op ((to_num sign l),r) + +let lt_vec_range = compare_op_vec_range (<) true +let gt_vec_range = compare_op_vec_range (>) true +let lteq_vec_range = compare_op_vec_range (<=) true +let gteq_vec_range = compare_op_vec_range (>=) true + +let compare_op_range_vec op sign (l,r) = + compare_op op (l, (to_num sign r)) + +let lt_range_vec = compare_op_range_vec (<) true +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) +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)) + + +val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a +let make_indexed_vector entries default start length dir = + let length = natFromInteger length in + Vector (List.foldl replace (replicate length default) entries) start dir + +(* +val make_bit_vector_undef : integer -> vector bitU +let make_bitvector_undef length = + Vector (replicate (natFromInteger length) BU) 0 true + *) + +(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) + +let mask (n,Vector bits start dir) = + let current_size = List.length bits in + Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir + + +val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) +let rec byte_chunks n list = match (n,list) with + | (0,_) -> [] + | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest + | _ -> failwith "byte_chunks not given enough bits" +end + +val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU +let bitv_of_byte_lifteds dir v = + let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in + let len = integerFromNat (List.length bits) in + Vector bits (if dir then 0 else len - 1) dir + +val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU +let bitv_of_bytes dir v = + let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in + let len = integerFromNat (List.length bits) in + Vector bits (if dir then 0 else len - 1) dir + + +val byte_lifteds_of_bitv : vector bitU -> list byte_lifted +let byte_lifteds_of_bitv (Vector bits length is_inc) = + let bits = List.map bit_lifted_of_bitU bits in + byte_lifteds_of_bit_lifteds bits + +val bytes_of_bitv : vector bitU -> list byte +let bytes_of_bitv (Vector bits length is_inc) = + let bits = List.map bit_of_bitU bits in + bytes_of_bits bits + +val bit_lifteds_of_bitUs : list bitU -> list bit_lifted +let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits + +val bit_lifteds_of_bitv : vector bitU -> list bit_lifted +let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v) + + +val address_lifted_of_bitv : vector bitU -> address_lifted +let address_lifted_of_bitv v = + let byte_lifteds = byte_lifteds_of_bitv v in + let maybe_address_integer = + match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing + end in + Address_lifted byte_lifteds maybe_address_integer + +val address_of_bitv : vector bitU -> address +let address_of_bitv v = + let bytes = bytes_of_bitv v in + address_of_byte_list bytes + + + +(*** Registers *) + +type register_field = string +type register_field_index = string * (integer * integer) (* name, start and end *) + +type register = + | Register of string * (* name *) + integer * (* length *) + integer * (* start index *) + bool * (* is increasing *) + list register_field_index + | UndefinedRegister of integer (* length *) + | RegisterPair of register * register + +let name_of_reg = function + | Register name _ _ _ _ -> name + | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "name_of_reg RegisterPair" +end + +let size_of_reg = function + | Register _ size _ _ _ -> size + | UndefinedRegister size -> size + | RegisterPair _ _ -> failwith "size_of_reg RegisterPair" +end + +let start_of_reg = function + | Register _ _ start _ _ -> start + | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "start_of_reg RegisterPair" +end + +let is_inc_of_reg = function + | Register _ _ _ is_inc _ -> is_inc + | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair" +end + +let dir_of_reg = function + | Register _ _ _ is_inc _ -> dir is_inc + | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister" + | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair" +end + +let size_of_reg_nat reg = natFromInteger (size_of_reg reg) +let start_of_reg_nat reg = natFromInteger (start_of_reg reg) + +val register_field_indices_aux : register -> register_field -> maybe (integer * integer) +let rec register_field_indices_aux register rfield = + match register with + | Register _ _ _ _ rfields -> List.lookup rfield rfields + | RegisterPair r1 r2 -> + let m_indices = register_field_indices_aux r1 rfield in + if isJust m_indices then m_indices else register_field_indices_aux r2 rfield + | UndefinedRegister _ -> Nothing + end + +val register_field_indices : register -> register_field -> integer * integer +let register_field_indices register rfield = + match register_field_indices_aux register rfield with + | Just indices -> indices + | Nothing -> failwith "Invalid register/register-field combination" + end + +let register_field_indices_nat reg regfield= + let (i,j) = register_field_indices reg regfield in + (natFromInteger i,natFromInteger j) + +let rec external_reg_value reg_name v = + let (internal_start, external_start, direction) = + match reg_name with + | Reg _ start size dir -> + (start, (if dir = D_increasing then start else (start - (size +1))), dir) + | Reg_slice _ reg_start dir (slice_start, slice_end) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + | Reg_field _ reg_start dir _ (slice_start, slice_end) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) -> + ((if dir = D_increasing then slice_start else (reg_start - slice_start)), + slice_start, dir) + end in + let bits = bit_lifteds_of_bitv v in + <| rv_bits = bits; + rv_dir = direction; + rv_start = external_start; + rv_start_internal = internal_start |> + +val internal_reg_value : register_value -> vector bitU +let internal_reg_value v = + Vector (List.map bitU_of_bit_lifted v.rv_bits) + (integerFromNat v.rv_start_internal) + (v.rv_dir = D_increasing) + + +let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = + match d with + (*This is the case the thread/concurrecny model expects, so no change needed*) + | D_increasing -> (i,j) + | D_decreasing -> let slice_i = start - i in + let slice_j = (i - j) + slice_i in + (slice_i,slice_j) + end + +let external_reg_whole reg = + Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg) + +let external_reg_slice reg (i,j) = + let start = start_of_reg_nat reg in + let dir = dir_of_reg reg in + Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j)) + +let external_reg_field_whole reg rfield = + let (m,n) = register_field_indices_nat reg rfield in + let start = start_of_reg_nat reg in + let dir = dir_of_reg reg in + Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n)) + +let external_reg_field_slice reg rfield (i,j) = + let (m,n) = register_field_indices_nat reg rfield in + let start = start_of_reg_nat reg in + let dir = dir_of_reg reg in + Reg_f_slice (name_of_reg reg) start dir rfield + (external_slice dir start (m,n)) + (external_slice dir start (i,j)) + +let external_mem_value v = + byte_lifteds_of_bitv v $> List.reverse + +let internal_mem_value direction bytes = + List.reverse bytes $> bitv_of_byte_lifteds direction + + + + + +val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> 'vars) -> 'vars +let rec foreach_inc (i,stop,by) vars body = + if i <= stop + then let vars = body i vars in + foreach_inc (i + by,stop,by) vars body + else vars + +val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> 'vars) -> 'vars +let rec foreach_dec (i,stop,by) vars body = + if i >= stop + then let vars = body i vars in + foreach_dec (i - by,stop,by) vars body + else vars + +let assert' b msg_opt = + let msg = match msg_opt with + | Just msg -> msg + | Nothing -> "unspecified error" + end in + if bitU_to_bool b then () else failwith msg + +(* convert numbers unsafely to naturals *) + +class (ToNatural 'a) val toNatural : 'a -> natural end +(* eta-expanded for Isabelle output, otherwise it breaks *) +instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end +instance (ToNatural int) let toNatural = (fun n -> naturalFromInt n) end +instance (ToNatural nat) let toNatural = (fun n -> naturalFromNat n) end +instance (ToNatural natural) let toNatural = (fun n -> n) end + +let toNaturalFiveTup (n1,n2,n3,n4,n5) = + (toNatural n1, + toNatural n2, + toNatural n3, + toNatural n4, + toNatural n5) + + +type regfp = + | RFull of (string) + | RSlice of (string * integer * integer) + | RSliceBit of (string * integer) + | RField of (string * string) + +type niafp = + | NIAFP_successor + | NIAFP_concrete_address of vector bitU + | NIAFP_LR + | NIAFP_CTR + | NIAFP_register of regfp + +(* only for MIPS *) +type diafp = + | DIAFP_none + | DIAFP_concrete of vector bitU + | DIAFP_reg of regfp + +let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function + | RFull name -> + let (start,length,direction,_) = reg_info name Nothing in + Reg name start length direction + | RSlice (name,i,j) -> + let i = natFromInteger i in + let j = natFromInteger j in + let (start,length,direction,_) = reg_info name Nothing in + let slice = external_slice direction start (i,j) in + Reg_slice name start direction slice + | RSliceBit (name,i) -> + let i = natFromInteger i in + let (start,length,direction,_) = reg_info name Nothing in + let slice = external_slice direction start (i,i) in + Reg_slice name start direction slice + | RField (name,field_name) -> + let (start,length,direction,span) = reg_info name (Just field_name) in + let slice = external_slice direction start span in + Reg_field name start direction field_name slice +end + +let niafp_to_nia reginfo = function + | NIAFP_successor -> NIA_successor + | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) + | NIAFP_LR -> NIA_LR + | NIAFP_CTR -> NIA_CTR + | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) +end + +let diafp_to_dia reginfo = function + | DIAFP_none -> DIA_none + | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) + | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) +end + diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 9c88eec7..58874fa6 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -45,6 +45,7 @@ import Map import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *) import Set_extra (* For 'to_list' because map only goes to set *) import List_extra (* For 'nth' and 'head' where we know that they cannot fail *) +open import Show open import Show_extra (* for 'show' to convert nat to string) *) open import String_extra (* for chr *) import Assert_extra (*For failwith when partiality is known to be unreachable*) @@ -54,7 +55,14 @@ open import Interp_ast open import Interp_utilities open import Instruction_extractor -type tannot = Interp_utilities.tannot +(* TODO: upstream into Lem *) +val stringFromTriple : forall 'a 'b 'c. ('a -> string) -> ('b -> string) -> ('c -> string) -> ('a * 'b * 'c) -> string +let stringFromTriple showX showY showZ (x,y,z) = + "(" ^ showX x ^ ", " ^ showY y ^ ", " ^ showZ z ^ ")" + +instance forall 'a 'b 'c. Show 'a, Show 'b, Show 'c => (Show ('a * 'b * 'c)) + let show = stringFromTriple show show show +end val debug_print : string -> unit declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s @@ -78,36 +86,14 @@ let non_det_annot annot maybe_id = match annot with | _ -> Nothing end -type i_direction = IInc | IDec let is_inc = function | IInc -> true | _ -> false end let id_of_string s = (Id_aux (Id s) Unknown) -type reg_form = - | Reg of id * tannot * i_direction - | SubReg of id * reg_form * index_range - -type ctor_kind = C_Enum of nat | C_Union - -type value = - | V_boxref of nat * t - | V_lit of lit - | V_tuple of list value - | V_list of list value - (* A full vector: int is the first index, bool says if that's most or least significant *) - | V_vector of nat * i_direction * list value - (* A vector with default values, second int stores length; as above otherwise *) - | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value - | V_record of t * list (id * value) - | V_ctor of id * t * ctor_kind * value - | V_unknown (* Distinct from undefined, used by memory system *) - | V_register of reg_form (* Value to store register access, when not actively reading or writing *) - | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *) - | V_track of value * (set reg_form) (* Used when memory system wants to track what register(s) a value came from *) let rec {ocaml} string_of_reg_form r = match r with - | Reg id _ _ -> get_id id - | SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id) + | Form_Reg id _ _ -> get_id id + | Form_SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id) end let rec {ocaml} string_of_value v = match v with @@ -196,18 +182,21 @@ let rec debug_print_value v = match v with | V_record t vals -> let ppidval (id,v) = "(" ^ (get_id id) ^ "," ^ debug_print_value v ^ ")" in "V_record t [" ^ debug_print_value_list (List.map ppidval vals) ^ "]" - | V_ctor id t k vals -> + | V_ctor id t k v' -> "V_ctor " ^ (get_id id) ^ " t " ^ (match k with | C_Enum n -> "(C_Enum " ^ show n ^ ")" | C_Union -> "C_Union" end) ^ - "(" ^ debug_print_value v ^ ")" + "(" ^ debug_print_value v' ^ ")" | V_unknown -> "V_unknown" | V_register r -> "V_register (" ^ string_of_reg_form r ^ ")" | V_register_alias _ _ -> "V_register_alias _ _" | V_track v rs -> "V_track (" ^ debug_print_value v ^ ") _" end - - + +instance (Show value) + let show v = debug_print_value v +end + let rec {coq;ocaml} id_value_eq strict (i, v) (i', v') = i = i' && value_eq strict v v' and value_eq strict left right = match (left, right) with @@ -249,7 +238,7 @@ end let reg_start_pos reg = match reg with - | Reg _ (Just(typ,_,_,_,_)) _ -> + | Form_Reg _ (Just(typ,_,_,_,_)) _ -> let start_from_vec targs = match targs with | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s | T_args [T_arg_nexp _; T_arg_nexp (Ne_const s); T_arg_order Odec; _] -> (natFromInteger s) - 1 @@ -277,7 +266,7 @@ end let reg_size reg = match reg with - | Reg _ (Just(typ,_,_,_,_)) _ -> + | Form_Reg _ (Just(typ,_,_,_,_)) _ -> let end_from_vec targs = match targs with | T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s | _ -> Assert_extra.failwith "register vector type not well formed" @@ -326,12 +315,20 @@ end let env_to_string (LEnv c env) = "(LEnv " ^ show c ^ " [" ^ (list_to_string ", " (fun (k,v) -> k ^ " -> " ^ (string_of_value v)) (Map_extra.toList env)) ^ - "])" + "])" + +instance (Show lenv) + let show env = env_to_string env +end let mem_to_string (LMem f c mem _) = "(LMem " ^ f ^ " " ^ show c ^ " [" ^ (list_to_string ", " (fun (k,v) -> show k ^ " -> " ^ (string_of_value v)) (Map_extra.toList mem)) ^ "])" +instance (Show lmem) + let show mem = mem_to_string mem +end + type sub_reg_map = map string index_range (*top_level is a tuple of @@ -351,6 +348,7 @@ type top_level = * map string typ (*typedef union constructors *) * map string sub_reg_map (*sub register mappings*) * map string (alias_spec tannot) (*register aliases*) + * bool (* debug? *) type action = | Read_reg of reg_form * maybe (nat * nat) @@ -387,10 +385,246 @@ type outcome = | Action of action * stack | Error of l * string -type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool|> +let string_of_id id' = + (match id' with + | Id_aux id _ -> + (match id with + | Id s -> s + | DeIid s -> s + end) + end) + +instance (Show id) + let show = string_of_id +end + +let string_of_kid kid' = + (match kid' with + | Kid_aux kid _ -> + (match kid with + | Var s -> s + end) + end) + +instance (Show kid) + let show = string_of_kid +end + +let string_of_reg_id (RI_aux (RI_id id ) _) = string_of_id id + +instance forall 'a. (Show reg_id 'a) + let show = string_of_reg_id +end + +let rec string_of_typ typ' = + (match typ' with + | Typ_aux typ _ -> + (match typ with + | Typ_wild -> "(Typ_wild)" + | Typ_id id -> "(Typ_id " ^ (string_of_id id) ^ ")" + | Typ_var kid -> "(Typ_var " ^ (string_of_kid kid) ^ ")" + | Typ_fn typ1 typ2 eff -> "(Typ_fn _ _ _)" + | Typ_tup typs -> "(Typ_tup [" ^ String.concat "; " (List.map string_of_typ typs) ^ "])" + | Typ_app id args -> "(Typ_app " ^ string_of_id id ^ " _)" + end) + end) + +instance (Show typ) + let show = string_of_typ +end + +let rec string_of_lexp l' = + (match l' with + | LEXP_aux l _ -> + (match l with + | LEXP_id id -> "(LEXP_id " ^ string_of_id id ^ ")" + | LEXP_memory id exps -> "(LEXP_memory " ^ string_of_id id ^ " _)" + | LEXP_cast typ id -> "(LEXP_cast " ^ string_of_typ typ ^ " " ^ string_of_id id ^ ")" + | LEXP_tup lexps -> "(LEXP_tup [" ^ String.concat "; " (List.map string_of_lexp lexps) ^ "])" + | LEXP_vector lexps exps -> "(LEXP_vector _ _)" + | LEXP_vector_range lexp exp1 exp2 -> "(LEXP_vector_range _ _ _)" + | LEXP_field lexp id -> "(LEXP_field " ^ string_of_lexp lexp ^ "." ^ string_of_id id ^ ")" + end) + end) + +instance forall 'a. (Show lexp 'a) + let show = string_of_lexp +end + +let string_of_lit l' = + (match l' with + | L_aux l _ -> + (match l with + | L_unit -> "()" + | L_zero -> "0" + | L_one -> "1" + | L_true -> "true" + | L_false -> "false" + | L_num n -> "0d" ^ (show n) + | L_hex s -> "0x" ^ s + | L_bin s -> "0b" ^ s + | L_undef -> "undef" + | L_string s -> "\"" ^ s ^ "\"" + end) + end) + +instance (Show lit) + let show = string_of_lit +end + +let string_of_order o' = + (match o' with + | Ord_aux o _ -> + (match o with + | Ord_var kid -> string_of_kid kid + | Ord_inc -> "inc" + | Ord_dec -> "dec" + end) + end) + +instance (Show order) + let show = string_of_order +end + +let rec string_of_exp e' = + (match e' with + | E_aux e _ -> + (match e with + | E_block exps -> "(E_block [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_nondet exps -> "(E_nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_id id -> "(E_id \"" ^ string_of_id id ^ "\")" + | E_lit lit -> "(E_lit " ^ string_of_lit lit ^ ")" + | E_cast typ exp -> "(E_cast " ^ string_of_typ typ ^ " " ^ string_of_exp exp ^ ")" + | E_app id exps -> "(E_app " ^ string_of_id id ^ " [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_app_infix exp1 id exp2 -> "(E_app_infix " ^ string_of_exp exp1 ^ " " ^ string_of_id id ^ " " ^ string_of_exp exp2 ^ ")" + | E_tuple exps -> "(E_tuple [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_if cond thn els -> "(E_if " ^ (string_of_exp cond) ^ " ? " ^ (string_of_exp thn) ^ " : " ^ (string_of_exp els) ^ ")" + | E_for id from to_ by order exp -> "(E_for " ^ string_of_id id ^ " " ^ string_of_exp from ^ " " ^ string_of_exp to_ ^ " " ^ string_of_exp by ^ " " ^ string_of_order order ^ " " ^ string_of_exp exp ^ ")" + | E_vector exps -> "(E_vector [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_vector_indexed _ _ -> "(E_vector_indexed)" + | E_vector_access exp1 exp2 -> "(E_vector_access " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")" + | E_vector_subrange exp1 exp2 exp3 -> "(E_vector_subrange " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ " " ^ string_of_exp exp3 ^ ")" + | E_vector_update _ _ _ -> "(E_vector_update)" + | E_vector_update_subrange _ _ _ _ -> "(E_vector_update_subrange)" + | E_vector_append exp1 exp2 -> "(E_vector_append " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")" + | E_list exps -> "(E_list [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])" + | E_cons exp1 exp2 -> "(E_cons " ^ string_of_exp exp1 ^ " :: " ^ string_of_exp exp2 ^ ")" + | E_record _ -> "(E_record)" + | E_record_update _ _ -> "(E_record_update)" + | E_field _ _ -> "(E_field)" + | E_case _ _ -> "(E_case)" + | E_let _ _ -> "(E_let)" + | E_assign lexp exp -> "(E_assign " ^ string_of_lexp lexp ^ " := " ^ string_of_exp exp ^ ")" + | E_sizeof _ -> "(E_sizeof _)" + | E_exit exp -> "(E_exit " ^ string_of_exp exp ^ ")" + | E_return exp -> "(E_return " ^ string_of_exp exp ^ ")" + | E_assert cond msg -> "(E_assert " ^ string_of_exp cond ^ " " ^ string_of_exp msg ^ ")" + | E_internal_cast _ _ -> "(E_internal_cast _ _)" + | E_internal_exp _ -> "(E_internal_exp _)" + | E_sizeof_internal _ -> "(E_size _)" + | E_internal_exp_user _ _ -> "(E_internal_exp_user _ _)" + | E_comment _ -> "(E_comment _)" + | E_comment_struc _ -> "(E_comment_struc _)" + | E_internal_let _ _ _ -> "(E_internal_let _ _ _)" + | E_internal_plet _ _ _ -> "(E_internal_plet _ _ _)" + | E_internal_return _ -> "(E_internal_return _)" + | E_internal_value value -> "(E_internal_value " ^ debug_print_value value ^ ")" + end) + end) + +instance forall 'a. (Show (exp 'a)) + let show = string_of_exp +end + +let string_of_alias_spec (AL_aux _as _) = + (match _as with + | AL_subreg reg_id id -> "(AL_subreg " ^ (show reg_id) ^ " " ^ (show id) ^ ")" + | AL_bit reg_id exp -> "(AL_bit " ^ (show reg_id) ^ " " ^ (show exp) ^ ")" + | AL_slice reg_id exp1 exp2 -> "(AL_slice " ^ (show reg_id) ^ " " ^ (show exp1) ^ " " ^ (show exp2) ^ ")" + | AL_concat reg_id1 reg_id2 -> "(AL_concat " ^ (show reg_id1) ^ " " ^ (show reg_id2) ^ ")" + end) + +instance forall 'a. (Show alias_spec 'a) + let show = string_of_alias_spec +end + +let string_of_quant_item (QI_aux qi _) = + (match qi with + | QI_id kinded_id -> "(QI_id _)" + | QI_const nc -> "(QI_const _)" + end) + +instance (Show quant_item) + let show = string_of_quant_item +end + +let string_of_typquant (TypQ_aux tq _) = + (match tq with + | TypQ_tq qis -> "(TypQ_tq [" ^ (String.concat "; " (List.map show qis)) ^ "]" + | TypQ_no_forall -> "TypQ_no_forall" + end) + +instance (Show typquant) + let show = string_of_typquant +end + +let string_of_typschm (TypSchm_aux (TypSchm_ts typquant typ) _) = + "(TypSchm " ^ (show typquant) ^ " " ^ (show typ) ^ ")" + +instance (Show typschm) + let show = string_of_typschm +end + +let rec string_of_pat (P_aux pat _) = + (match pat with + | P_lit lit -> "(P_lit " ^ show lit ^ ")" + | P_wild -> "P_wild" + | P_as pat' id -> "(P_as " ^ string_of_pat pat' ^ " " ^ show id ^ ")" + | P_typ typ pat' -> "(P_typ" ^ show typ ^ " " ^ string_of_pat pat' ^ ")" + | P_id id -> "(P_id " ^ show id ^ ")" + | P_app id pats -> "(P_app " ^ show id ^ " [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])" + | P_record _ _ -> "(P_record _ _)" + | P_vector pats -> "(P_vector [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])" + | P_vector_indexed _ -> "(P_vector_indexed _)" + | P_vector_concat pats -> "(P_vector_concat [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])" + | P_tup pats -> "(P_tup [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])" + | P_list pats -> "(P_list [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])" + end) + +instance forall 'a. (Show pat 'a) + let show = string_of_pat +end + +let string_of_letbind (LB_aux lb _) = + (match lb with + | LB_val_explicit ts pat exp -> "(LB_val_explicit " ^ (show ts) ^ " " ^ (show pat) ^ " " ^ (show exp) ^ ")" + | LB_val_implicit pat exp -> "(LB_val_implicit " ^ (show pat) ^ " " ^ (show exp) ^ ")" + end) + +instance forall 'a. (Show letbind 'a) + let show = string_of_letbind +end + +type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool; debug : bool; debug_indent : string |> + +let indent_mode mode = if mode.debug then <| mode with debug_indent = " " ^ mode.debug_indent |> else mode + +val debug_fun_enter : interp_mode -> string -> list string -> unit +let debug_fun_enter mode name args = + if mode.debug then + debug_print (mode.debug_indent ^ ":: " ^ name ^ " args: [" ^ (String.concat "; " args) ^ "]\n") + else + () + +val debug_fun_exit : forall 'a. Show 'a => interp_mode -> string -> 'a -> unit +let debug_fun_exit mode name retval = + if mode.debug then + debug_print (mode.debug_indent ^ "=> " ^ name ^ " returns: " ^ (show retval) ^ "\n") + else + () (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *) -val to_top_env : (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level) +val to_top_env : bool -> (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level) val get_default_direction : top_level -> i_direction (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *) @@ -439,7 +673,7 @@ let rec to_registers dd (Defs defs) = | Nothing -> dd | Just(t, _, _, _,_) -> dd (*TODO, lets pull the direction out properly*) end in - Map.insert (get_id id) (V_register(Reg id tannot dir)) (to_registers dd (Defs defs)) + Map.insert (get_id id) (V_register(Form_Reg id tannot dir)) (to_registers dd (Defs defs)) | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> Map.insert (get_id id) (V_register_alias aspec tannot) (to_registers dd (Defs defs)) | _ -> to_registers dd (Defs defs) @@ -1039,7 +1273,7 @@ let rec combine_typs ts = let reg_to_t r = match r with - | Reg _ (Just (t,_,_,_,_)) _ -> t + | Form_Reg _ (Just (t,_,_,_,_)) _ -> t | _ -> T_var "fresh" end @@ -1084,89 +1318,8 @@ let rec val_typ v = | V_register_alias _ _ -> T_var "fresh_alias" end -(* When mode.track_values keeps tracking on registers by extending environment *) let rec to_exp mode env v : (exp tannot * lenv) = - let mk_annot is_ctor ctor_kind = - (Interp_ast.Unknown, - if is_ctor - then match ctor_kind with - | Just(C_Enum i) -> (enum_annot (val_typ v) (integerFromNat i)) - | _ -> (ctor_annot (val_typ v)) end - else (val_annot (val_typ v))) in - let annot = mk_annot false Nothing in - let mapf vs ((LEnv l env) as lenv) : (list (exp tannot) * lenv) = - let (es, env) = - List.foldr (fun v (es,env) -> let (e,ev) = (to_exp mode env v) in - if mode.track_values - then ((e::es), union_env ev env) - else ((e::es), env)) - ([],(LEnv l Map.empty)) vs in - (es, union_env env lenv) - in - match v with - | V_boxref n t -> (E_aux (E_id (Id_aux (Id (show n)) Unknown)) annot, env) - | V_lit lit -> (E_aux (E_lit lit) annot, env) - | V_tuple(vals) -> - let (es,env') = mapf vals env in (E_aux (E_tuple es) annot, env') - | V_vector n dir vals -> - let (es,env') = mapf vals env in - if (is_inc(dir) && n=0) - then (E_aux (E_vector es) annot, env') - else if is_inc(dir) - then (E_aux (E_vector_indexed - (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es))) - (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') - else if (n+1)= List.length vals - then (E_aux (E_vector es) annot, env') - else - (E_aux (E_vector_indexed - (snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es)) - (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') - | V_vector_sparse n m dir vals d -> - let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in - let ((d : (exp tannot)),env') = to_exp mode env' d in - (E_aux (E_vector_indexed - ((if is_inc(dir) then List.reverse else (fun i -> i)) - (List.map (fun ((i,v), e) -> ((integerFromNat i), e)) (List.zip vals es))) - (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env') - | V_record t ivals -> - let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in - (E_aux (E_record(FES_aux (FES_Fexps - (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing))) - (List.zip ivals es)) false) - (Unknown,Nothing))) annot, env') - | V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env') - | V_ctor id t ckind vals -> - let annotation = mk_annot true (Just ckind) in - (match (vals,ckind) with - | (V_lit (L_aux L_unit _), C_Union) -> (E_aux (E_app id []) annotation, env) - | (V_lit (L_aux L_unit _), C_Enum _) -> (E_aux (E_id id) annotation, env) - | (V_track (V_lit (L_aux L_unit _)) _, C_Union) -> (E_aux (E_app id []) annotation, env) - | (V_track (V_lit (L_aux L_unit _)) _, C_Enum _) -> (E_aux (E_id id) annotation, env) - | (V_tuple vals,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env') - | (V_track (V_tuple vals) _,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env') - | (V_track _ _,_) -> - if mode.track_values - then begin let (fid,env') = fresh_var env in - let env' = add_to_env (fid,vals) env' in - (E_aux - (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))]) - annotation, env') - end - else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation, env') - | _ -> - let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation,env') end) - | V_register (Reg id tan dir) -> (E_aux (E_id id) annot, env) - | V_register _ -> Assert_extra.failwith "V_register contains subreg" - | V_register_alias _ _ -> (E_aux (E_id (id_of_string "dummy_register")) annot, env) (*If this persists, then alias spec must change*) - | V_track v' _ -> - if mode.track_values - then begin let (fid,env') = fresh_var env in - let env' = add_to_env (fid,v) env' in - (E_aux (E_id fid) annot, env') end - else to_exp mode env v' - | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env) -end + ((E_aux (E_internal_value v) (Interp_ast.Unknown, (val_annot (val_typ v)))), env) val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv) let rec env_to_let_help mode env taint_env = match env with @@ -1208,7 +1361,7 @@ end (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv let rec match_pattern t_level (P_aux p (_, annot)) value_whole = - let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in + let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in let (t,tag,cs) = match annot with | Just(t,tag,cs,e,_) -> (t,tag,cs) | Nothing -> (T_var "fresh",Tag_empty,[]) end in @@ -1535,7 +1688,43 @@ let resolve_outcome to_match value_thunk action_thunk = | (Value v,lm,le) -> value_thunk v lm le | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le) | (Error l s,lm,le) -> (Error l s,lm,le) - end +end + +let string_of_action a = + (match a with + | Read_reg r _ -> "(Read_reg " ^ string_of_reg_form r ^ " _)" + | Write_reg r _ _ -> "(Write_reg " ^ string_of_reg_form r ^ " _ _)" + | Read_mem id v _ -> "(Read_mem " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)" + | Read_mem_tagged id v _ -> "(Read_mem_tagged " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)" + | Write_mem _ _ _ _ -> "(Write_mem _ _ _ _)" + | Write_ea id v -> "(Write_ea " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)" + | Write_memv _ _ _ -> "(Write_memv _ _ _)" + | Excl_res id -> "(Excl_res " ^ string_of_id id ^ ")" + | Write_memv_tagged _ _ _ _ -> "(Write_memv_tagged _ _ _ _)" + | Barrier id v -> "(Barrier " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")" + | Footprint id v -> "(Footprint " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")" + | Nondet exps _ -> "(Nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "] _)" + | Call_extern s v -> "(Call_extern \"" ^ s ^ "\" " ^ debug_print_value v ^ ")" + | Return v -> "(Return " ^ debug_print_value v ^ ")" + | Exit exp -> "(Exit " ^ string_of_exp exp ^ ")" + | Fail v -> "(Fail " ^ debug_print_value v ^ ")" + | Step _ _ _ -> "(Step _ _ _)" + end) + +instance (Show action) + let show action = string_of_action action +end + +let string_of_outcome outcome = + (match outcome with + | Value v -> "(Value " ^ debug_print_value v ^ ")" + | Action a _ -> "(Action " ^ string_of_action a ^ " _)" + | Error _ s -> "(Error _ \"" ^ s ^ "\")" + end) + +instance (Show outcome) + let show outcome = string_of_outcome outcome +end let update_stack o fn = match o with | Action act stack -> Action act (fn stack) @@ -1553,7 +1742,7 @@ let get_num v = match v with | _ -> 0 end (*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *) -let rec exp_list mode t_level build_e build_v l_env l_mem vals exps = +let rec __exp_list mode t_level build_e build_v l_env l_mem vals exps = match exps with | [ ] -> (Value (build_v vals), l_mem, l_env) | e::exps -> @@ -1566,13 +1755,20 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps = (e,env'')))) end -and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = - let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in +and exp_list mode t_level build_e build_v l_env l_mem vals exps = + let _ = debug_fun_enter mode "exp_list" [show vals; show exps] in + let retval = __exp_list (indent_mode mode) t_level build_e build_v l_env l_mem vals exps in + let _ = debug_fun_exit mode "exp_list" retval in + retval + +and __interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = + let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in let (typ,tag,ncs,effect,reffect) = match annot with | Nothing -> (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown)) | Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in match exp with + | E_internal_value v -> (Value v, l_mem, l_env) | E_lit lit -> if is_lit_vector lit then let is_inc = (match typ with @@ -1637,7 +1833,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | _ -> match in_env regs name with (* Register isn't a local value, so pull from global environment *) | Just(V_register regform) -> regform - | _ -> Reg id annot default_dir end end in + | _ -> Form_Reg id annot default_dir end end in (Action (Read_reg regf Nothing) (mk_hole l annot t_level l_env l_mem), l_mem, l_env) | Tag_alias -> match in_env aliases name with @@ -1823,7 +2019,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (match in_env (env_from_list fexps) (get_id id) with | Just v -> (Value (retaint value_whole v),lm,l_env) | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end) - | V_register ((Reg _ annot _) as reg_form) -> + | V_register ((Form_Reg _ annot _) as reg_form) -> let id' = match annot with | Just((T_id id'),_,_,_,_) -> id' | Just((T_abbrev (T_id id') _),_,_,_,_) -> id' @@ -1833,7 +2029,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | Just(indexes) -> (match in_env indexes (get_id id) with | Just ir -> - let sub_reg = SubReg id reg_form ir in + let sub_reg = Form_SubReg id reg_form ir in (Action (Read_reg sub_reg Nothing) (mk_hole l (val_annot (reg_to_t sub_reg)) t_level le lm),lm,le) | _ -> (Error l "Internal error: unrecognized read, no id",lm,le) end) @@ -1845,254 +2041,226 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun a -> match (exp,a) with | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)), - (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) -> + (Action (Read_reg ((Form_Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) -> match in_env subregs id' with | Just(indexes) -> (match in_env indexes (get_id id) with | Just ir -> - (Action (Read_reg (SubReg id regf ir) Nothing) s) + (Action (Read_reg (Form_SubReg id regf ir) Nothing) s) | _ -> Error l "Internal error, unrecognized read, no id" end) | Nothing -> Error l "Internal error, unrecognized read, no reg" end | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)), - (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))-> + (Action (Read_reg ((Form_Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))-> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> - (Action (Read_reg (SubReg id regf ir) Nothing) s) + (Action (Read_reg (Form_SubReg id regf ir) Nothing) s) | _ -> Error l "Internal error, unrecognized read, no id" end | Nothing -> Error l "Internal error, unrecognized read, no reg" end | _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end) | E_vector_access vec i -> - resolve_outcome - (interp_main mode t_level l_env l_mem i) - (fun iv lm le -> - match detaint iv with - | V_unknown -> (Value iv,lm,le) - | V_lit (L_aux (L_num n) ln) -> - let n = natFromInteger n in - resolve_outcome - (interp_main mode t_level l_env lm vec) - (fun vvec lm le -> - let v_access vvec num = (match (detaint vvec, detaint num) with - | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n) - | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n) - | (V_register reg, V_lit _) -> - Action (Read_reg reg (Just (n,n))) (mk_hole l annot t_level l_env lm) - | (V_unknown,_) -> Value V_unknown - | _ -> Assert_extra.failwith - ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") end) in - (v_access (retaint iv vvec) iv,lm,le)) - (fun a -> - (*TODO I think this pattern match is no longer necessary *) - match a with - | Action (Read_reg reg Nothing) stack -> - (match vec with - | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack - | _ -> Action (Read_reg reg Nothing) - (add_to_top_frame - (fun v env -> - let (iv_e, env) = to_exp mode env iv in - (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end) - | Action (Read_reg reg (Just (o,p))) stack -> - (match vec with - | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack - | _ -> Action (Read_reg reg (Just (o,p))) - (add_to_top_frame - (fun v env -> - let (iv_e, env) = to_exp mode env iv in - (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end) - | _ -> - update_stack a - (add_to_top_frame - (fun v env -> - let (iv_e, env) = to_exp mode env iv in - (E_aux (E_vector_access v iv_e) (l,annot), env))) end) - | _ -> (Error l "Vector access not given a number for index",lm,l_env) end) - (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_access vec i) (l,annot), env)))) - | E_vector_subrange vec i1 i2 -> - resolve_outcome - (interp_main mode t_level l_env l_mem i1) - (fun i1v lm le -> - match detaint i1v with - | V_unknown -> (Value i1v,lm,le) - | V_lit (L_aux (L_num n1) nl1) -> - resolve_outcome - (interp_main mode t_level l_env lm i2) - (fun i2v lm le -> - match detaint i2v with - | V_unknown -> (Value i2v,lm,le) - | V_lit (L_aux (L_num n2) nl2) -> - resolve_outcome - (interp_main mode t_level l_env lm vec) - (fun vvec lm le -> - let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in - let take_slice vvec = - let (n1,n2) = (natFromInteger n1,natFromInteger n2) in - (match detaint vvec with - | V_vector _ _ _ -> Value (slice_vector vvec n1 n2) - | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2) - | V_unknown -> - let inc = n1 < n2 in - Value (retaint vvec (V_vector n1 (if inc then IInc else IDec) - (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown))) - | V_register reg -> - Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm) - | _ -> (Error l ("Vector slice of non-vector " ^ (string_of_value vvec))) end) in - ((take_slice (retaint slice vvec)), lm,le)) - (fun a -> - let rebuild v env = let (ie1,env) = to_exp mode env i1v in - let (ie2,env) = to_exp mode env i2v in - (E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in - (*TODO this pattern match should no longer be needed*) - match a with - | Action (Read_reg reg Nothing) stack -> - match vec with - | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> - Action (Read_reg reg (Just((natFromInteger (get_num i1v)), - (natFromInteger (get_num i2v))))) stack - | _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end - | Action (Read_reg reg (Just (o,p))) stack -> - match vec with - | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> - Action (Read_reg reg (Just((natFromInteger (get_num i1v)), - (natFromInteger (get_num i2v))))) stack - | _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end - | _ -> update_stack a (add_to_top_frame rebuild) end) - | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) - end) - (fun a -> update_stack a - (add_to_top_frame - (fun i2 env -> - let (ie1,env) = to_exp mode env i1v in - (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env)))) - | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) end) - (fun a -> - update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env)))) - | E_vector_update vec i exp -> - resolve_outcome - (interp_main mode t_level l_env l_mem i) - (fun vi lm le -> - (match (detaint vi) with - | V_lit (L_aux (L_num n1) ln1) -> - (resolve_outcome - (interp_main mode t_level le lm exp) - (fun vup lm le -> - resolve_outcome - (interp_main mode t_level le lm vec) - (fun vec lm le -> - let fvup vi vec = (match vec with - | V_vector _ _ _ -> fupdate_vec vec (natFromInteger n1) vup - | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec (natFromInteger n1) vup - | V_unknown -> V_unknown - | _ -> Assert_extra.failwith "Update of vector given non-vector" end) in - (Value (binary_taint fvup vi vec),lm,le)) - (fun a -> update_stack a - (add_to_top_frame - (fun v env -> - let (eup,env') = (to_exp mode env vup) in - let (ei, env') = (to_exp mode env' vi) in - (E_aux (E_vector_update v ei eup) (l,annot), env'))))) - (fun a -> update_stack a - (add_to_top_frame - (fun e env -> - let (ei, env) = to_exp mode env vi in - (E_aux (E_vector_update vec ei e) (l,annot), env))))) - | V_unknown -> (Value vi,lm,l_env) - | _ -> Assert_extra.failwith "Update of vector requires number for access" end)) - (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_update vec i exp) (l,annot), env)))) - | E_vector_update_subrange vec i1 i2 exp -> - resolve_outcome - (interp_main mode t_level l_env l_mem i1) - (fun vi1 lm le -> - match detaint vi1 with - | V_unknown -> (Value vi1,lm,le) - | V_lit (L_aux (L_num n1) ln1) -> - resolve_outcome - (interp_main mode t_level l_env lm i2) - (fun vi2 lm le -> - match detaint vi2 with - | V_unknown -> (Value vi2,lm,le) - | V_lit (L_aux (L_num n2) ln2) -> - resolve_outcome - (interp_main mode t_level l_env lm exp) - (fun v_rep lm le -> - (resolve_outcome - (interp_main mode t_level l_env lm vec) - (fun vvec lm le -> - let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in - let fup_v_slice v1 vvec = (match vvec with - | V_vector _ _ _ -> - fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2) - | V_vector_sparse _ _ _ _ _ -> - fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2) - | V_unknown -> V_unknown - | _ -> Assert_extra.failwith "Vector update requires vector" end) in - (Value (binary_taint fup_v_slice slice vvec),lm,le)) - (fun a -> update_stack a - (add_to_top_frame - (fun v env -> - let (e_rep,env') = to_exp mode env v_rep in - let (ei1, env') = to_exp mode env' vi1 in - let (ei2, env') = to_exp mode env' vi2 in - (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env')))))) - (fun a -> update_stack a - (add_to_top_frame - (fun e env -> - let (ei1,env') = to_exp mode env vi1 in - let (ei2,env') = to_exp mode env' vi2 in - (E_aux (E_vector_update_subrange vec ei1 ei2 e) (l,annot),env')))) - | _ -> Assert_extra.failwith "vector update requires number" end) - (fun a -> - update_stack a (add_to_top_frame - (fun i2 env -> - let (ei1, env') = to_exp mode env vi1 in - (E_aux (E_vector_update_subrange vec ei1 i2 exp) (l,annot), env')))) - | _ -> Assert_extra.failwith "vector update requires number" end) - (fun a -> - update_stack a - (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env)))) - | E_vector_append e1 e2 -> - resolve_outcome - (interp_main mode t_level l_env l_mem e1) - (fun v1 lm le -> - match detaint v1 with - | V_unknown -> (Value v1,lm,l_env) - | _ -> - (resolve_outcome - (interp_main mode t_level l_env lm e2) - (fun v2 lm le -> - let append v1 v2 = (match (v1,v2) with - | (V_vector _ dir vals1, V_vector _ _ vals2) -> - let vals = vals1++vals2 in - let len = List.length vals in - if is_inc(dir) - then V_vector 0 dir vals - else V_vector (len-1) dir vals - | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) -> - let original_len = List.length vals1 in - let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in - let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in - V_vector_sparse m (len+original_len) dir (sparse_vals ++ sparse_update) d - | (V_vector_sparse m len dir vals1 d, V_vector _ _ vals2) -> - let new_len = List.length vals2 in - let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in - V_vector_sparse m (len+new_len) dir (vals1++sparse_vals) d - | (V_vector_sparse m len dir vals1 d, V_vector_sparse _ new_len _ vals2 _) -> - let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in - V_vector_sparse m (len+new_len) dir (vals1 ++ sparse_update) d - | (V_unknown,_) -> V_unknown (*update to get length from type*) - | (_,V_unknown) -> V_unknown (*see above*) - | _ -> Assert_extra.failwith ("vector concat requires two vectors but given " - ^ (string_of_value v1) ^ " " ^ (string_of_value v2)) end) in - (Value (binary_taint append v1 v2),lm,le)) - (fun a -> update_stack a (add_to_top_frame - (fun e env -> - let (e1,env') = to_exp mode env v1 in - (E_aux (E_vector_append e1 e) (l,annot),env'))))) end) - (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_append e e2) (l,annot),env)))) + resolve_outcome + (interp_main mode t_level l_env l_mem vec) + (fun vvec lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i) + (fun iv lm le -> + (match detaint iv with + | V_unknown -> (Value iv,lm,le) + | V_lit (L_aux (L_num n) ln) -> + let n = natFromInteger n in + let v_access vvec num = + (match (detaint vvec, detaint num) with + | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n) + | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n) + | (V_register reg, V_lit _) -> + Action (Read_reg reg (Just (n,n))) (mk_hole l annot t_level l_env lm) + | (V_unknown,_) -> Value V_unknown + | _ -> Assert_extra.failwith + ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") + end) + in + (v_access (retaint iv vvec) iv,lm,le) + | _ -> (Error l "Vector access not given a number for index",lm,l_env) + end)) + (fun a -> update_stack a (add_to_top_frame(fun i' env -> + let (vec_e, env') = to_exp mode env vvec in + (E_aux (E_vector_access vec_e i') (l,annot), env'))))) + (fun a -> + update_stack a (add_to_top_frame (fun vec' env -> + (E_aux (E_vector_access vec' i) (l,annot), env)))) + | E_vector_subrange vec i1 i2 -> + resolve_outcome + (interp_main mode t_level l_env l_mem vec) + (fun vvec lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i1) + (fun i1v lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i2) + (fun i2v lm le -> + match detaint i1v with + | V_unknown -> (Value i1v,lm,le) + | V_lit (L_aux (L_num n1) nl1) -> + match detaint i2v with + | V_unknown -> (Value i2v,lm,le) + | V_lit (L_aux (L_num n2) nl2) -> + let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in + let take_slice vvec = + let (n1,n2) = (natFromInteger n1,natFromInteger n2) in + (match detaint vvec with + | V_vector _ _ _ -> Value (slice_vector vvec n1 n2) + | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2) + | V_unknown -> + let inc = n1 < n2 in + Value (retaint vvec (V_vector n1 (if inc then IInc else IDec) + (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown))) + | V_register reg -> + Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm) + | _ -> (Error l ("Vector slice of non-vector " ^ (string_of_value vvec))) end) in + ((take_slice (retaint slice vvec)), lm,le) + | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) + end + | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) + end) + (fun a -> update_stack a (add_to_top_frame (fun i2' env -> + let (vec_e, env') = to_exp mode env vvec in + let (i1_e, env'') = to_exp mode env' i1v in + (E_aux (E_vector_subrange vec_e i1_e i2') (l,annot), env''))))) + (fun a -> + update_stack a (add_to_top_frame (fun i1' env -> + let (vec_e, env') = to_exp mode env vvec in + (E_aux (E_vector_subrange vec_e i1' i2) (l,annot), env'))))) + (fun a -> + update_stack a (add_to_top_frame (fun vec' env -> + (E_aux (E_vector_subrange vec' i1 i2) (l,annot), env)))) + | E_vector_update vec i exp -> + resolve_outcome + (interp_main mode t_level l_env l_mem vec) + (fun vvec lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i) + (fun vi lm le -> + resolve_outcome + (interp_main mode t_level l_env lm exp) + (fun vup lm le -> + (match (detaint vi) with + | V_lit (L_aux (L_num n1) ln1) -> + let fvup vi vvec = + (match vvec with + | V_vector _ _ _ -> fupdate_vec vvec (natFromInteger n1) vup + | V_vector_sparse _ _ _ _ _ -> fupdate_vec vvec (natFromInteger n1) vup + | V_unknown -> V_unknown + | _ -> Assert_extra.failwith "Update of vector given non-vector" + end) + in + (Value (binary_taint fvup vi vvec),lm,le) + | V_unknown -> (Value vi,lm,le) + | _ -> Assert_extra.failwith "Update of vector requires number for access" + end)) + (fun a -> update_stack a (add_to_top_frame (fun exp' env -> + let (vec_e, env') = to_exp mode env vvec in + let (i_e, env'') = to_exp mode env' vi in + (E_aux (E_vector_update vec_e i_e exp') (l,annot), env''))))) + (fun a -> update_stack a (add_to_top_frame (fun i' env -> + let (vec_e, env') = to_exp mode env vvec in + (E_aux (E_vector_update vec_e i' exp) (l,annot), env'))))) + (fun a -> update_stack a (add_to_top_frame (fun vec' env -> + (E_aux (E_vector_update vec' i exp) (l,annot), env)))) + | E_vector_update_subrange vec i1 i2 exp -> + resolve_outcome + (interp_main mode t_level l_env l_mem vec) + (fun vvec lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i1) + (fun vi1 lm le -> + resolve_outcome + (interp_main mode t_level l_env lm i2) + (fun vi2 lm le -> + resolve_outcome + (interp_main mode t_level l_env lm exp) + (fun v_rep lm le -> + (match detaint vi1 with + | V_unknown -> (Value vi1,lm,le) + | V_lit (L_aux (L_num n1) ln1) -> + (match detaint vi2 with + | V_unknown -> (Value vi2,lm,le) + | V_lit (L_aux (L_num n2) ln2) -> + let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in + let fup_v_slice v1 vvec = + (match vvec with + | V_vector _ _ _ -> + fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2) + | V_vector_sparse _ _ _ _ _ -> + fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2) + | V_unknown -> V_unknown + | _ -> Assert_extra.failwith "Vector update requires vector" + end) in + (Value (binary_taint fup_v_slice slice vvec),lm,le) + | _ -> Assert_extra.failwith "vector update requires number" + end) + | _ -> Assert_extra.failwith "vector update requires number" + end)) + (fun a -> update_stack a (add_to_top_frame (fun exp' env -> + let (vec_e, env') = to_exp mode env vvec in + let (i1_e, env'') = to_exp mode env' vi1 in + let (i2_e, env''') = to_exp mode env'' vi1 in + (E_aux (E_vector_update_subrange vec_e i1_e i2_e exp') (l,annot), env'''))))) + (fun a -> update_stack a (add_to_top_frame (fun i2' env -> + let (vec_e, env') = to_exp mode env vvec in + let (i1_e, env'') = to_exp mode env' vi1 in + (E_aux (E_vector_update_subrange vec_e i1_e i2' exp) (l,annot), env''))))) + (fun a -> update_stack a (add_to_top_frame (fun i1' env -> + let (vec_e, env') = to_exp mode env vvec in + (E_aux (E_vector_update_subrange vec_e i1' i2 exp) (l,annot), env'))))) + (fun a -> update_stack a (add_to_top_frame (fun vec' env -> + (E_aux (E_vector_update_subrange vec' i1 i2 exp) (l,annot), env)))) + | E_vector_append e1 e2 -> + resolve_outcome + (interp_main mode t_level l_env l_mem e1) + (fun v1 lm le -> + resolve_outcome + (interp_main mode t_level l_env lm e2) + (fun v2 lm le -> + (match detaint v1 with + | V_unknown -> (Value v1,lm,le) + | _ -> + let append v1 v2 = + (match (v1,v2) with + | (V_vector _ dir vals1, V_vector _ _ vals2) -> + let vals = vals1++vals2 in + let len = List.length vals in + if is_inc(dir) + then V_vector 0 dir vals + else V_vector (len-1) dir vals + | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) -> + let original_len = List.length vals1 in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in + let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in + V_vector_sparse m (len+original_len) dir (sparse_vals ++ sparse_update) d + | (V_vector_sparse m len dir vals1 d, V_vector _ _ vals2) -> + let new_len = List.length vals2 in + let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in + V_vector_sparse m (len+new_len) dir (vals1++sparse_vals) d + | (V_vector_sparse m len dir vals1 d, V_vector_sparse _ new_len _ vals2 _) -> + let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in + V_vector_sparse m (len+new_len) dir (vals1 ++ sparse_update) d + | (V_unknown,_) -> V_unknown (*update to get length from type*) + | (_,V_unknown) -> V_unknown (*see above*) + | _ -> Assert_extra.failwith ("vector concat requires two vectors but given " + ^ (string_of_value v1) ^ " " ^ (string_of_value v2)) + end) + in + (Value (binary_taint append v1 v2),lm,le) + end)) + (fun a -> update_stack a (add_to_top_frame (fun e2' env -> + let (e1_e, env') = to_exp mode env v1 in + (E_aux (E_vector_append e1_e e2') (l,annot), env'))))) + (fun a -> update_stack a (add_to_top_frame (fun e1' env -> + (E_aux (E_vector_append e1' e2) (l,annot), env)))) | E_tuple(exps) -> exp_list mode t_level (fun exps env' -> (E_aux (E_tuple exps) (l,annot), env')) V_tuple l_env l_mem [] exps | E_vector(exps) -> @@ -2415,8 +2583,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | _ -> (Error l "Internal expression escaped to interpreter", l_mem, l_env) end +and interp_main mode t_level l_env l_mem exp = + let _ = debug_fun_enter mode "interp_main" [show exp] in + let retval = __interp_main (indent_mode mode) t_level l_env l_mem exp in + let _ = debug_fun_exit mode "interp_main" retval in + retval + (*TODO shrink location information on recursive calls *) - and interp_block mode t_level init_env local_env local_mem l tannot exps = +and __interp_block mode t_level init_env local_env local_mem l tannot exps = match exps with | [] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env) | [exp] -> @@ -2431,12 +2605,18 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le) (fun a -> update_stack a (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env)))) - end + end + +and interp_block mode t_level init_env local_env local_mem l tannot exps = + let _ = debug_fun_enter mode "interp_block" [show exps] in + let retval = __interp_block (indent_mode mode) t_level init_env local_env local_mem l tannot exps in + let _ = debug_fun_exit mode "interp_block" retval in + retval -and create_write_message_or_update mode t_level value l_env l_mem is_top_level +and __create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv)) * maybe value) = - let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in + let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in let (typ,tag,ncs,ef,efr) = match annot with | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown)) @@ -2575,7 +2755,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (match in_env indexes (get_id subreg) with | Just ir -> (Action - (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing + (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) @@ -2589,7 +2769,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (match in_env indexes (get_id subreg) with | Just ir -> (Action - (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing + (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) @@ -2602,7 +2782,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (fun v le lm -> match v with | V_lit (L_aux (L_num i) _) -> let i = natFromInteger i in - (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i)) + (Action (Write_reg (Form_Reg reg annot' default_dir) (Just (i,i)) (update_vector_start default_dir i 1 value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) t_level l_env l_mem Top), l_mem, l_env) @@ -2619,7 +2799,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | V_lit (L_aux (L_num stop) _) -> let (start,stop) = (natFromInteger start,natFromInteger stop) in let size = if start < stop then stop - start +1 else start -stop +1 in - (Action (Write_reg (Reg reg annot' default_dir) (Just (start,stop)) + (Action (Write_reg (Form_Reg reg annot' default_dir) (Just (start,stop)) (update_vector_start default_dir start size value)) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) t_level l_env l_mem Top), @@ -2640,7 +2820,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]), T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) -> (Action - (Write_reg (Reg reg1 annot1 default_dir) Nothing + (Write_reg (Form_Reg reg1 annot1 default_dir) Nothing (slice_vector value (natFromInteger b1) (natFromInteger r1))) (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2) @@ -3062,13 +3242,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Read_mem_tagged _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Call_extern _ _ -> ((Action a s,lm,le), next_builder, Nothing) - | Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> + | Write_reg ((Form_Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> ((Action - (Write_reg (SubReg id regf ir) Nothing + (Write_reg (Form_SubReg id regf ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), @@ -3076,13 +3256,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing,Nothing) end | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing,Nothing) end - | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> + | Write_reg ((Form_Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> match in_env subregs id' with | Just(indexes) -> match in_env indexes (get_id id) with | Just ir -> ((Action - (Write_reg (SubReg id regf ir) Nothing + (Write_reg (Form_SubReg id regf ir) Nothing (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s, lm,le), @@ -3095,7 +3275,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level | e -> e end) end -and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) = +and create_write_message_or_update mode t_level value l_env l_mem is_top_level le = + let _ = debug_fun_enter mode "create_write_message_or_update" [show le] in + let retval = __create_write_message_or_update (indent_mode mode) t_level value l_env l_mem is_top_level le in + let _ = debug_fun_exit mode "create_write_message_or_update" "_" in + retval + +and __interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) = match lbind with | LB_val_explicit t pat exp -> match (interp_main mode t_level l_env l_mem exp) with @@ -3113,10 +3299,16 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) = | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end) | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot))))) | e -> (e,Nothing) end -end +end + +and interp_letbind mode t_level l_env l_mem lb = + let _ = debug_fun_enter mode "interp_letbind" [show lb] in + let retval = __interp_letbind (indent_mode mode) t_level l_env l_mem lb in + let _ = debug_fun_exit mode "interp_letbind" "_" in + retval -and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = - let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in +and __interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = + let (Env defs instrs default_dir lets regs ctors subregs aliases debug) = t_level in let stack = Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top in let get_reg_typ_name typ = match typ with @@ -3130,7 +3322,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (match in_env subregs reg_ti with | Just indexes -> (match in_env indexes (get_id subreg) with - | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack, + | Just ir -> (Action (Read_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing) stack, l_mem, l_env) | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end) | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), @@ -3140,7 +3332,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (fun v le lm -> match v with | V_lit (L_aux (L_num i) _) -> let i = natFromInteger i in - (Action (Read_reg (Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env) + (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env) | _ -> Assert_extra.failwith "alias bit did not reduce to number" end) (fun a -> a) (*Should not currently happen as type system enforces constants*) | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> @@ -3154,7 +3346,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = (match v with | V_lit (L_aux (L_num stop) _) -> let (start,stop) = (natFromInteger start,natFromInteger stop) in - (Action (Read_reg (Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env) + (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env) | _ -> Assert_extra.failwith ("Alias slice evaluted non-lit " ^ (string_of_value v)) end)) (fun a -> a)) @@ -3162,7 +3354,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = end) (fun a -> a) (*Neither action function should occur, due to above*) | AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> - (Action (Read_reg (Reg reg1 annot1 default_dir) Nothing) + (Action (Read_reg (Form_Reg reg1 annot1 default_dir) Nothing) (Hole_frame redex_id (E_aux (E_vector_append (E_aux (E_id redex_id) (l1, (intern_annot annot1))) (E_aux (E_id reg2) annot2)) @@ -3170,8 +3362,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = | _ -> Assert_extra.failwith "alias spec not well formed" end +and interp_alias_read mode t_level l_env l_mem al = + let _ = debug_fun_enter mode "interp_alias_read" [show al] in + let retval = __interp_alias_read (indent_mode mode) t_level l_env l_mem al in + let _ = debug_fun_exit mode "interp_alias_read" retval in + retval + let rec eval_toplevel_let handle_action tlevel env mem lbind = - match interp_letbind <|eager_eval=true; track_values=false; track_lmem=false|> tlevel env mem lbind with + match interp_letbind <| eager_eval=true; track_values=false; track_lmem=false; debug=false; debug_indent="" |> tlevel env mem lbind with | ((Value v, lm, (LEnv _ le)),_) -> Just le | ((Action a s,lm,le), Just le_builder) -> (match handle_action (Action a s) with @@ -3184,7 +3382,7 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind = | _ -> Nothing end let rec to_global_letbinds handle_action (Defs defs) t_level = - let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in + let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in match defs with | [] -> ((Value (V_lit (L_aux L_unit Unknown)), (emem "global_letbinds"), eenv),t_level) | def::defs -> @@ -3194,10 +3392,10 @@ let rec to_global_letbinds handle_action (Defs defs) t_level = | Just le -> to_global_letbinds handle_action (Defs defs) - (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases) + (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases debug) | Nothing -> to_global_letbinds handle_action (Defs defs) - (Env fdefs instrs default_dir lets regs ctors subregs aliases) end + (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) end | DEF_type (TD_aux tdef _) -> match tdef with | TD_enum id ns ids _ -> @@ -3208,7 +3406,7 @@ let rec to_global_letbinds handle_action (Defs defs) t_level = (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in to_global_letbinds handle_action (Defs defs) - (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases) + (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases debug) | _ -> to_global_letbinds handle_action (Defs defs) t_level end | _ -> to_global_letbinds handle_action (Defs defs) t_level end @@ -3223,28 +3421,34 @@ let rec extract_default_direction (Defs defs) = match defs with | _ -> extract_default_direction (Defs defs) end end (*TODO Contemplate making execute environment variable instead of constant*) -let to_top_env external_functions defs = +let to_top_env debug external_functions defs = let direction = (extract_default_direction defs) in let t_level = Env (to_fdefs defs) (extract_instructions "execute" defs) direction Map.empty (* empty letbind and enum values, call below will fill in any *) (to_registers direction defs) - (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in + (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) debug in let (o,t_level) = to_global_letbinds (external_functions direction) defs t_level in match o with | (Value _,_,_) -> (Nothing,t_level) | (o,_,_) -> (Just o,t_level) end -let interp mode external_functions defs exp = - match (to_top_env external_functions defs) with +let __interp mode external_functions defs exp = + match (to_top_env mode.debug external_functions defs) with | (Nothing,t_level) -> interp_main mode t_level eenv (emem "top level") exp | (Just o,_) -> (o,(emem "top level error"),eenv) end -let rec resume_with_env mode stack value = +let interp mode external_functions defs exp = + let _ = debug_fun_enter mode "interp" [show exp] in + let retval = __interp (indent_mode mode) external_functions defs exp in + let _ = debug_fun_exit mode "interp" retval in + retval + +let rec __resume_with_env mode stack value = match (stack,value) with | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv) | (Hole_frame id exp t_level env mem Top,Just value) -> @@ -3271,10 +3475,17 @@ let rec resume_with_env mode stack value = match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end | (Action action stack,e) -> (Action action (Thunk_frame exp t_level env mem stack),e) | (Error l s,e) -> (Error l s,e) - end + end end -let rec resume mode stack value = +and resume_with_env mode stack value = + let _ = debug_fun_enter mode "resume_with_env" [show value] in + let retval = __resume_with_env (indent_mode mode) stack value in + let _ = debug_fun_exit mode "interp" retval in + retval + + +let rec __resume mode stack value = match (stack,value) with | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",(emem "top level error"),eenv) | (Hole_frame id exp t_level env mem Top,Just value) -> @@ -3305,3 +3516,8 @@ let rec resume mode stack value = end end +and resume mode stack value = + let _ = debug_fun_enter mode "resume" [show value] in + let retval = __resume (indent_mode mode) stack value in + let _ = debug_fun_exit mode "resume" retval in + retval diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem index b706d3aa..733d1a36 100644 --- a/src/lem_interp/interp_ast.lem +++ b/src/lem_interp/interp_ast.lem @@ -40,9 +40,11 @@ (* SUCH DAMAGE. *) (*========================================================================*) -(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +(* generated by Ott 0.25 from: l2.ott *) open import Pervasives +open import Pervasives +open import Pervasives_extra open import Map open import Maybe open import Set_extra @@ -72,21 +74,17 @@ type base_kind_aux = (* base kind *) | BK_effect (* kind of effect sets *) -type base_kind = - | BK_aux of base_kind_aux * l - - -type kid_aux = (* variables with kind, ticked to differntiate from program variables *) +type kid_aux = (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *) | Var of x -type id_aux = (* Identifier *) +type id_aux = (* identifier *) | Id of x | DeIid of x (* remove infix status *) -type kind_aux = (* kinds *) - | K_kind of list base_kind +type base_kind = + | BK_aux of base_kind_aux * l type kid = @@ -97,24 +95,28 @@ type id = | Id_aux of id_aux * l -type kind = - | K_aux of kind_aux * l +type kind_aux = (* kinds *) + | K_kind of list base_kind -type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) - | Nexp_id of id (* identifier, bound by def Nat x = nexp *) +type nexp_aux = (* numeric expression, of kind $Nat$ *) + | Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_minus of nexp * nexp (* subtraction *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use *) + | Nexp_neg of nexp (* for internal use only *) and nexp = | Nexp_aux of nexp_aux * l +type kind = + | K_aux of kind_aux * l + + type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) @@ -129,23 +131,23 @@ type base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism from intra-instruction parallelism *) - | BE_escape (* Tracking of expressions and functions that might call exit *) - | BE_lset (* Local mutation happend; not user-writable *) - | BE_lret (* Local return happened; not user-writable *) + | BE_nondet (* nondeterminism, from $nondet$ *) + | BE_escape (* potential call of $exit$ *) + | BE_lset (* local mutation; not user-writable *) + | BE_lret (* local return; not user-writable *) type base_effect = | BE_aux of base_effect_aux * l -type order_aux = (* vector order specifications, of kind Order *) +type order_aux = (* vector order specifications, of kind $Order$ *) | Ord_var of kid (* variable *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) + | Ord_inc (* increasing *) + | Ord_dec (* decreasing *) -type effect_aux = (* effect set, of kind Effects *) +type effect_aux = (* effect set, of kind $Effect$ *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -163,11 +165,6 @@ let effect_union e1 e2 = end -type kinded_id_aux = (* optionally kind-annotated identifier *) - | KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) - - type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -175,17 +172,22 @@ type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of kid * list integer -type kinded_id = - | KOpt_aux of kinded_id_aux * l +type kinded_id_aux = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type n_constraint = | NC_aux of n_constraint_aux * l -type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of n_constraint (* A constraint for this type *) +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + +type quant_item_aux = (* kinded identifier or $Nat$ constraint *) + | QI_id of kinded_id (* optionally kinded identifier *) + | QI_const of n_constraint (* $Nat$ constraint *) type quant_item = @@ -194,38 +196,25 @@ type quant_item = type typquant_aux = (* type quantifiers and constraints *) | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type lit_aux = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) + | TypQ_no_forall (* empty *) type typquant = | TypQ_aux of typquant_aux * l -type typ_aux = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_id of id (* Defined type *) - | Typ_var of kid (* Type variable *) - | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) +type typ_aux = (* type expressions, of kind $Type$ *) + | Typ_wild (* unspecified type *) + | Typ_id of id (* defined type *) + | Typ_var of kid (* type variable *) + | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) + | Typ_tup of list typ (* Tuple *) | Typ_app of id * list typ_arg (* type constructor application *) and typ = | Typ_aux of typ_aux * l -and typ_arg_aux = (* Type constructor arguments of all kinds *) +and typ_arg_aux = (* type constructor arguments of all kinds *) | Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order @@ -235,15 +224,41 @@ and typ_arg = | Typ_arg_aux of typ_arg_aux * l -type lit = - | L_aux of lit_aux * l +type lit_aux = (* literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) + + +type index_range_aux = (* index specification, for bitfields in register types *) + | BF_single of integer (* single index *) + | BF_range of integer * integer (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + | BF_aux of index_range_aux * l type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ -type pat_aux 'a = (* Pattern *) +type lit = + | L_aux of lit_aux * l + + +type typschm = + | TypSchm_aux of typschm_aux * l + + +type pat_aux 'a = (* pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of (pat 'a) * id (* named pattern *) @@ -260,207 +275,33 @@ type pat_aux 'a = (* Pattern *) and pat 'a = | P_aux of (pat_aux 'a) * annot 'a -and fpat_aux 'a = (* Field pattern *) +and fpat_aux 'a = (* field pattern *) | FP_Fpat of id * (pat 'a) and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a -type typschm = - | TypSchm_aux of typschm_aux * l - - -type reg_id_aux 'a = - | RI_id of id - - -type exp_aux 'a = (* Expression *) - | E_block of list (exp 'a) (* block *) - | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * (exp 'a) (* cast *) - | E_app of id * list (exp 'a) (* function application *) - | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) - | E_tuple of list (exp 'a) (* tuple *) - | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) - | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) - | E_vector of list (exp 'a) (* vector (indexed from 0) *) - | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) - | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) - | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) - | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) - | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) - | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) - | E_list of list (exp 'a) (* list *) - | E_cons of (exp 'a) * (exp 'a) (* cons *) - | E_record of (fexps 'a) (* struct *) - | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) - | E_field of (exp 'a) * id (* field projection from struct *) - | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) - | E_let of (letbind 'a) * (exp 'a) (* let expression *) - | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) - | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) - | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) - | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) - | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) - | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) - | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) - | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) - | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) - | E_comment of string (* For generated unstructured comments *) - | E_comment_struc of (exp 'a) (* For generated structured comments *) - | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) - | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) - | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) - -and exp 'a = - | E_aux of (exp_aux 'a) * annot 'a - -and lexp_aux 'a = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_memory of id * list (exp 'a) (* memory write via function call *) - | LEXP_cast of typ * id - | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *) - | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) - | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) - | LEXP_field of (lexp 'a) * id (* struct field *) - -and lexp 'a = - | LEXP_aux of (lexp_aux 'a) * annot 'a - -and fexp_aux 'a = (* Field-expression *) - | FE_Fexp of id * (exp 'a) - -and fexp 'a = - | FE_aux of (fexp_aux 'a) * annot 'a - -and fexps_aux 'a = (* Field-expression list *) - | FES_Fexps of list (fexp 'a) * bool - -and fexps 'a = - | FES_aux of (fexps_aux 'a) * annot 'a - -and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) - | Def_val_empty - | Def_val_dec of (exp 'a) - -and opt_default 'a = - | Def_val_aux of (opt_default_aux 'a) * annot 'a - -and pexp_aux 'a = (* Pattern match *) - | Pat_exp of (pat 'a) * (exp 'a) - -and pexp 'a = - | Pat_aux of (pexp_aux 'a) * annot 'a - -and letbind_aux 'a = (* Let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) - -and letbind 'a = - | LB_aux of (letbind_aux 'a) * annot 'a - - -type reg_id 'a = - | RI_aux of (reg_id_aux 'a) * annot 'a - - -type type_union_aux = (* Type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id - - -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) +type name_scm_opt_aux = (* optional variable naming-scheme constraint *) | Name_sect_none | Name_sect_some of string -type effect_opt_aux = (* Optional effect annotation for functions *) - | Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect - - -type funcl_aux 'a = (* Function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) - - -type rec_opt_aux = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) - - -type tannot_opt_aux = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ - - -type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) - | AL_subreg of (reg_id 'a) * id - | AL_bit of (reg_id 'a) * (exp 'a) - | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) - | AL_concat of (reg_id 'a) * (reg_id 'a) - - -type type_union = - | Tu_aux of type_union_aux * l - - -type index_range_aux = (* index specification, for bitfields in register types *) - | BF_single of integer (* single index *) - | BF_range of integer * integer (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - | BF_aux of index_range_aux * l +type type_union_aux = (* type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id type name_scm_opt = | Name_sect_aux of name_scm_opt_aux * l -type effect_opt = - | Effect_opt_aux of effect_opt_aux * l - - -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * annot 'a - - -type rec_opt = - | Rec_aux of rec_opt_aux * l - - -type tannot_opt = - | Typ_annot_opt_aux of tannot_opt_aux * l - - -type alias_spec 'a = - | AL_aux of (alias_spec_aux 'a) * annot 'a - - -type default_spec_aux 'a = (* Default kinding or typing assumption *) - | DT_kind of base_kind * kid - | DT_order of order - | DT_typ of typschm * id - - -type type_def_aux 'a = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type val_spec_aux 'a = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +type type_union = + | Tu_aux of type_union_aux * l -type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *) - | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) +type kind_def_aux 'a = (* Definition body for elements of kind *) + | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) @@ -468,71 +309,20 @@ type kind_def_aux 'a = (* Definition body for elements of kind; many are shorth | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -type scattered_def_aux 'a = (* Function and type union definitions that can be spread across - a file. Each one must end in $id$ *) - | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) - - -type fundef_aux 'a = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) - - -type dec_spec_aux 'a = (* Register declarations *) - | DEC_reg of typ * id - | DEC_alias of id * (alias_spec 'a) - | DEC_typ_alias of typ * id * (alias_spec 'a) - - -type default_spec 'a = - | DT_aux of (default_spec_aux 'a) * l - - -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a - - -type val_spec 'a = - | VS_aux of (val_spec_aux 'a) * annot 'a +type type_def_aux 'a = (* type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* tagged union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) type kind_def 'a = | KD_aux of (kind_def_aux 'a) * annot 'a -type scattered_def 'a = - | SD_aux of (scattered_def_aux 'a) * annot 'a - - -type fundef 'a = - | FD_aux of (fundef_aux 'a) * annot 'a - - -type dec_spec 'a = - | DEC_aux of (dec_spec_aux 'a) * annot 'a - - -type dec_comm 'a = (* Top-level generated comments *) - | DC_comm of string (* generated unstructured comment *) - | DC_comm_struct of (def 'a) (* generated structured comment *) - -and def 'a = (* Top-level definition *) - | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) - | DEF_type of (type_def 'a) (* type definition *) - | DEF_fundef of (fundef 'a) (* function definition *) - | DEF_val of (letbind 'a) (* value definition *) - | DEF_spec of (val_spec 'a) (* top-level type constraint *) - | DEF_default of (default_spec 'a) (* default kind and type assumptions *) - | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) - | DEF_reg_dec of (dec_spec 'a) (* register declaration *) - | DEF_comm of (dec_comm 'a) (* generated comments *) - - -type defs 'a = (* Definition sequence *) - | Defs of list (def 'a) +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a let rec remove_one i l = @@ -569,6 +359,24 @@ type ne = (* internal numeric expressions *) | Ne_unary of ne +type t = (* Internal types *) + | T_id of x + | T_var of x + | T_fn of t * t * effect + | T_tup of list t + | T_app of x * t_args + | T_abbrev of t * t + +and t_arg = (* Argument to type constructors *) + | T_arg_typ of t + | T_arg_nexp of ne + | T_arg_effect of effect + | T_arg_order of order + +and t_args = (* Arguments to type constructors *) + | T_args of list t_arg + + type k = (* Internal kinds *) | Ki_typ | Ki_nat @@ -578,15 +386,6 @@ type k = (* Internal kinds *) | Ki_infer (* Representing an unknown kind, inferred by context *) -type nec = (* Numeric expression constraints *) - | Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * list integer - | Nec_cond of list nec * list nec - | Nec_branch of list nec - - type tid = (* A type identifier or type variable *) | Tid_id of id | Tid_var of kid @@ -597,22 +396,13 @@ type kinf = (* Whether a kind is default or from a local binding *) | Kinf_def of k -type t = (* Internal types *) - | T_id of x - | T_var of x - | T_fn of t * t * effect - | T_tup of list t - | T_app of x * t_args - | T_abbrev of t * t - -and t_arg = (* Argument to type constructors *) - | T_arg_typ of t - | T_arg_nexp of ne - | T_arg_effect of effect - | T_arg_order of order - -and t_args = (* Arguments to type constructors *) - | T_args of list t_arg +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of x * list integer + | Nec_cond of list nec * list nec + | Nec_branch of list nec type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) @@ -640,26 +430,26 @@ type conformsto = (* how much conformance does overloading need *) | Conformsto_parm +type widennum = + | Widennum_widen + | Widennum_dont + | Widennum_dontcare + + type widenvec = | Widenvec_widen | Widenvec_dont | Widenvec_dontcare -type widennum = - | Widennum_widen - | Widennum_dont - | Widennum_dontcare +type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) + | Widening_w of widennum * widenvec type tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) | Tinfs_empty | Tinfs_ls of list tinf - -type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) - | Widening_w of widennum * widenvec - type definition_env = | DenvEmp | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) @@ -705,10 +495,253 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should +type I = inf + + type E = env -type I = inf +type tannot = maybe (t * tag * list nec * effect * effect) + + + +type i_direction = + | IInc + | IDec + + +type reg_id_aux 'a = + | RI_id of id + + +type reg_form = + | Form_Reg of id * tannot * i_direction + | Form_SubReg of id * reg_form * index_range + + +type ctor_kind = + | C_Enum of nat + | C_Union + + +type reg_id 'a = + | RI_aux of (reg_id_aux 'a) * annot 'a + + +type exp_aux 'a = (* expression *) + | E_block of list (exp 'a) (* sequential block *) + | E_nondet of list (exp 'a) (* nondeterministic block *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of typ * (exp 'a) (* cast *) + | E_app of id * list (exp 'a) (* function application *) + | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) + | E_tuple of list (exp 'a) (* tuple *) + | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) + | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) + | E_vector of list (exp 'a) (* vector (indexed from 0) *) + | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) + | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) + | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) + | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) + | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *) + | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) + | E_list of list (exp 'a) (* list *) + | E_cons of (exp 'a) * (exp 'a) (* cons *) + | E_record of (fexps 'a) (* struct *) + | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) + | E_field of (exp 'a) * id (* field projection from struct *) + | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) + | E_let of (letbind 'a) * (exp 'a) (* let expression *) + | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) + | E_sizeof of nexp (* the value of nexp at run time *) + | E_return of (exp 'a) (* return (exp 'a) from current function *) + | E_exit of (exp 'a) (* halt all current execution *) + | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *) + | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) + | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) + | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of (exp 'a) (* For generated structured comments *) + | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) + | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) + | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *) + +and exp 'a = + | E_aux of (exp_aux 'a) * annot 'a + +and value = (* interpreter evaluated value *) + | V_boxref of nat * t + | V_lit of lit + | V_tuple of list value + | V_list of list value + | V_vector of nat * i_direction * list value + | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value + | V_record of t * list (id * value) + | V_ctor of id * t * ctor_kind * value + | V_unknown + | V_register of reg_form + | V_register_alias of alias_spec tannot * tannot + | V_track of value * set reg_form + +and lexp_aux 'a = (* lvalue expression *) + | LEXP_id of id (* identifier *) + | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *) + | LEXP_cast of typ * id (* cast *) + | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *) + | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) + | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) + | LEXP_field of (lexp 'a) * id (* struct field *) + +and lexp 'a = + | LEXP_aux of (lexp_aux 'a) * annot 'a + +and fexp_aux 'a = (* field expression *) + | FE_Fexp of id * (exp 'a) + +and fexp 'a = + | FE_aux of (fexp_aux 'a) * annot 'a + +and fexps_aux 'a = (* field expression list *) + | FES_Fexps of list (fexp 'a) * bool + +and fexps 'a = + | FES_aux of (fexps_aux 'a) * annot 'a + +and opt_default_aux 'a = (* optional default value for indexed vector expressions *) + | Def_val_empty + | Def_val_dec of (exp 'a) + +and opt_default 'a = + | Def_val_aux of (opt_default_aux 'a) * annot 'a + +and pexp_aux 'a = (* pattern match *) + | Pat_exp of (pat 'a) * (exp 'a) + +and pexp 'a = + | Pat_aux of (pexp_aux 'a) * annot 'a + +and letbind_aux 'a = (* let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *) + +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a + +and alias_spec_aux 'a = (* register alias expression forms *) + | AL_subreg of (reg_id 'a) * id + | AL_bit of (reg_id 'a) * (exp 'a) + | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) + | AL_concat of (reg_id 'a) * (reg_id 'a) + +and alias_spec 'a = + | AL_aux of (alias_spec_aux 'a) * annot 'a + + +type funcl_aux 'a = (* function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + +type rec_opt_aux = (* optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type tannot_opt_aux = (* optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ + + +type effect_opt_aux = (* optional effect annotation for functions *) + | Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * annot 'a + + +type rec_opt = + | Rec_aux of rec_opt_aux * l + + +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * l + + +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l + + +type val_spec_aux 'a = (* value type specification *) + | VS_val_spec of typschm * id (* specify the type of an upcoming definition *) + | VS_extern_no_rename of typschm * id (* specify the type of an external function *) + | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) + + +type fundef_aux 'a = (* function definition *) + | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) + + +type scattered_def_aux 'a = (* scattered function and union type definitions *) + | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type default_spec_aux 'a = (* default kinding or typing assumption *) + | DT_order of order + | DT_kind of base_kind * kid + | DT_typ of typschm * id + + +type dec_spec_aux 'a = (* register declarations *) + | DEC_reg of typ * id + | DEC_alias of id * (alias_spec 'a) + | DEC_typ_alias of typ * id * (alias_spec 'a) + + +type val_spec 'a = + | VS_aux of (val_spec_aux 'a) * annot 'a + + +type fundef 'a = + | FD_aux of (fundef_aux 'a) * annot 'a + + +type scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a + + +type default_spec 'a = + | DT_aux of (default_spec_aux 'a) * l + + +type dec_spec 'a = + | DEC_aux of (dec_spec_aux 'a) * annot 'a + + +type dec_comm 'a = (* top-level generated comments *) + | DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of (def 'a) (* generated structured comment *) + +and def 'a = (* top-level definition *) + | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) + | DEF_type of (type_def 'a) (* type definition *) + | DEF_fundef of (fundef 'a) (* function definition *) + | DEF_val of (letbind 'a) (* value definition *) + | DEF_spec of (val_spec 'a) (* top-level type constraint *) + | DEF_default of (default_spec 'a) (* default kind and type assumptions *) + | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) + | DEF_reg_dec of (dec_spec 'a) (* register declaration *) + | DEF_comm of (dec_comm 'a) (* generated comments *) + + +type defs 'a = (* definition sequence *) + | Defs of list (def 'a) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index f0d7dec4..fda9d5dd 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -51,35 +51,35 @@ open import Interp_ast open import Sail_impl_base open import Interp_interface -val intern_reg_value : register_value -> Interp.value -val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value -val extern_reg_value : reg_name -> Interp.value -> register_value -val extern_with_track: forall 'a. interp_mode -> (Interp.value -> 'a) -> Interp.value -> ('a * maybe (list reg_name)) -val extern_vector_value: Interp.value -> list byte_lifted -val extern_mem_value : Interp.value -> memory_value -val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name - -let make_interpreter_mode eager_eval tracking_values = - <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;; - -let make_mode eager_eval tracking_values = - <|internal_mode = make_interpreter_mode eager_eval tracking_values|>;; -let make_mode_exhaustive = - <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|> |>;; +val intern_reg_value : register_value -> Interp_ast.value +val intern_mem_value : interp_mode -> direction -> memory_value -> Interp_ast.value +val extern_reg_value : reg_name -> Interp_ast.value -> register_value +val extern_with_track: forall 'a. interp_mode -> (Interp_ast.value -> 'a) -> Interp_ast.value -> ('a * maybe (list reg_name)) +val extern_vector_value: Interp_ast.value -> list byte_lifted +val extern_mem_value : Interp_ast.value -> memory_value +val extern_reg : Interp_ast.reg_form -> maybe (nat * nat) -> reg_name + +let make_interpreter_mode eager_eval tracking_values debug = + <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false; Interp.debug = debug; Interp.debug_indent = "" |>;; + +let make_mode eager_eval tracking_values debug = + <| internal_mode = make_interpreter_mode eager_eval tracking_values debug |>;; +let make_mode_exhaustive debug = + <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true; Interp.debug = debug; Interp.debug_indent = "" |> |>;; let tracking_dependencies mode = mode.internal_mode.Interp.track_values -let make_eager_mode mode = <| internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;; -let make_default_mode = fun () -> <|internal_mode = make_interpreter_mode false false|>;; +let make_eager_mode mode = <| internal_mode = <| mode.internal_mode with Interp.eager_eval = true |> |>;; +let make_default_mode = fun () -> <| internal_mode = make_interpreter_mode false false false |>;; let bitl_to_ibit = function - | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) - | Bitl_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) - | Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown)) - | Bitl_unknown -> Interp.V_unknown + | Bitl_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) + | Bitl_one -> (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown)) + | Bitl_undef -> (Interp_ast.V_lit (L_aux L_undef Interp_ast.Unknown)) + | Bitl_unknown -> Interp_ast.V_unknown end let bit_to_ibit = function - | Bitc_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) - | Bitc_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) + | Bitc_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) + | Bitc_one -> (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown)) end let to_bool = function @@ -99,13 +99,13 @@ end let bitl_from_ibit b = let b = Interp.detaint b in match b with - | Interp.V_lit (L_aux L_zero _) -> Bitl_zero - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitl_zero - | Interp.V_lit (L_aux L_one _) -> Bitl_one - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitl_one - | Interp.V_lit (L_aux L_undef _) -> Bitl_undef - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef - | Interp.V_unknown -> Bitl_unknown + | Interp_ast.V_lit (L_aux L_zero _) -> Bitl_zero + | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitl_zero + | Interp_ast.V_lit (L_aux L_one _) -> Bitl_one + | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitl_one + | Interp_ast.V_lit (L_aux L_undef _) -> Bitl_undef + | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_undef _)] -> Bitl_undef + | Interp_ast.V_unknown -> Bitl_unknown | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) end let bits_to_ibits l = List.map bit_to_ibit l @@ -116,10 +116,10 @@ let bits_from_ibits l = List.map (fun b -> let b = Interp.detaint b in match b with - | Interp.V_lit (L_aux L_zero _) -> Bitc_zero - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitc_zero - | Interp.V_lit (L_aux L_one _) -> Bitc_one - | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitc_one + | Interp_ast.V_lit (L_aux L_zero _) -> Bitc_zero + | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitc_zero + | Interp_ast.V_lit (L_aux L_one _) -> Bitc_one + | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitc_one | _ -> Assert_extra.failwith ("bits_from_ibits given unexpected " ^ (Interp.string_of_value b)) end) l @@ -138,23 +138,23 @@ let bits_to_word8 b = else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u" let intern_direction = function - | D_increasing -> Interp.IInc - | D_decreasing -> Interp.IDec + | D_increasing -> Interp_ast.IInc + | D_decreasing -> Interp_ast.IDec end let extern_direction = function - | Interp.IInc -> D_increasing - | Interp.IDec -> D_decreasing + | Interp_ast.IInc -> D_increasing + | Interp_ast.IDec -> D_decreasing end let intern_opcode direction (Opcode v) = let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in let direction = intern_direction direction in - Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits + Interp_ast.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits let intern_reg_value v = match v with | <| rv_bits=[b] |> -> bitl_to_ibit b - | _ -> Interp.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits) + | _ -> Interp_ast.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits) end let intern_mem_value mode direction v = @@ -162,12 +162,12 @@ let intern_mem_value mode direction v = $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) $> fun bits -> let direction = intern_direction direction in - Interp.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits + Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits let intern_ifield_value direction v = let bits = bits_to_ibits v in let direction = intern_direction direction in - Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits + Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = match d with @@ -179,25 +179,25 @@ let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = end let extern_reg r slice = match (r,slice) with - | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> + | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir) - | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> + | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> let start = Interp.reg_start_pos r in let edir = extern_direction dir in Reg_slice x start edir (extern_slice edir start (i1, i2)) - | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _), + | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _), Nothing) -> let i = natFromInteger i in let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_field y start edir x (extern_slice edir start (i,i)) - | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), + | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Nothing) -> let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_field y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) - | (Interp.SubReg (Id_aux (Id x) _) - ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) -> + | (Interp_ast.Form_SubReg (Id_aux (Id x) _) + ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) -> let start = Interp.reg_start_pos main_r in let edir = extern_direction dir in Reg_f_slice y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) @@ -207,8 +207,8 @@ end let rec extern_reg_value reg_name v = match v with - | Interp.V_track v regs -> extern_reg_value reg_name v - | Interp.V_vector_sparse fst stop inc bits default -> + | Interp_ast.V_track v regs -> extern_reg_value reg_name v + | Interp_ast.V_vector_sparse fst stop inc bits default -> extern_reg_value reg_name (Interp_lib.fill_in_sparse v) | _ -> let (internal_start, external_start, direction) = @@ -226,13 +226,13 @@ let rec extern_reg_value reg_name v = slice_start, dir) end) in let bit_list = (match v with - | Interp.V_vector fst dir bits -> bitls_from_ibits bits - | Interp.V_lit (L_aux L_zero _) -> [Bitl_zero] - | Interp.V_lit (L_aux L_false _) -> [Bitl_zero] - | Interp.V_lit (L_aux L_one _) -> [Bitl_one] - | Interp.V_lit (L_aux L_true _) -> [Bitl_one] - | Interp.V_lit (L_aux L_undef _) -> [Bitl_undef] - | Interp.V_unknown -> [Bitl_unknown] + | Interp_ast.V_vector fst dir bits -> bitls_from_ibits bits + | Interp_ast.V_lit (L_aux L_zero _) -> [Bitl_zero] + | Interp_ast.V_lit (L_aux L_false _) -> [Bitl_zero] + | Interp_ast.V_lit (L_aux L_one _) -> [Bitl_one] + | Interp_ast.V_lit (L_aux L_true _) -> [Bitl_one] + | Interp_ast.V_lit (L_aux L_undef _) -> [Bitl_undef] + | Interp_ast.V_unknown -> [Bitl_unknown] | _ -> Assert_extra.failwith ("extern_reg_val given non externable value " ^ (Interp.string_of_value v)) end) in <| rv_bits=bit_list; @@ -242,7 +242,7 @@ let rec extern_reg_value reg_name v = end let extern_with_track mode f = function - | Interp.V_track v regs -> + | Interp_ast.V_track v regs -> (f v, if mode.internal_mode.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs))) @@ -251,13 +251,13 @@ let extern_with_track mode f = function end let rec extern_vector_value v = match v with - | Interp.V_vector _fst _inc bits -> + | Interp_ast.V_vector _fst _inc bits -> bitls_from_ibits bits $> to_bytes - | Interp.V_vector_sparse _fst _stop _inc _bits _default -> + | Interp_ast.V_vector_sparse _fst _stop _inc _bits _default -> Interp_lib.fill_in_sparse v $> extern_vector_value - | Interp.V_track v _ -> extern_vector_value v + | Interp_ast.V_track v _ -> extern_vector_value v | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v)) end @@ -265,19 +265,19 @@ let rec extern_mem_value v = List.reverse (extern_vector_value v) let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with - | (Interp.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp - | (Interp.V_vector fst inc bits,_) -> bits_from_ibits bits - | (Interp.V_vector_sparse fst stop inc bits default,_) -> + | (Interp_ast.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp + | (Interp_ast.V_vector fst inc bits,_) -> bits_from_ibits bits + | (Interp_ast.V_vector_sparse fst stop inc bits default,_) -> extern_ifield_value i_name field_name (Interp_lib.fill_in_sparse v) ftyp - | (Interp.V_lit (L_aux L_zero _),_) -> [Bitc_zero] - | (Interp.V_lit (L_aux L_false _),_) -> [Bitc_zero] - | (Interp.V_lit (L_aux L_one _),_) -> [Bitc_one] - | (Interp.V_lit (L_aux L_true _),_) -> [Bitc_one] - | (Interp.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i - | (Interp.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i - | (Interp.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i - | (Interp.V_ctor _ _ (Interp.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i) - | (Interp.V_ctor _ _ (Interp.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i) + | (Interp_ast.V_lit (L_aux L_zero _),_) -> [Bitc_zero] + | (Interp_ast.V_lit (L_aux L_false _),_) -> [Bitc_zero] + | (Interp_ast.V_lit (L_aux L_one _),_) -> [Bitc_one] + | (Interp_ast.V_lit (L_aux L_true _),_) -> [Bitc_one] + | (Interp_ast.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i + | (Interp_ast.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i + | (Interp_ast.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i + | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i) + | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i) | _ -> Assert_extra.failwith ("extern_ifield_value of " ^ i_name ^ " for field " ^ field_name ^ " given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp) @@ -351,11 +351,11 @@ let initial_instruction_state top_level main args = type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis type interp_value_return = - | Ivh_value of Interp.value - | Ivh_value_after_exn of Interp.value + | Ivh_value of Interp_ast.value + | Ivh_value_after_exn of Interp_ast.value | Ivh_error of decode_error -let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk = +let rec interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen thunk = let errk_str = match ivh_mode with | Ivh_translate -> "translate" | Ivh_analysis -> "analysis" @@ -363,7 +363,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Ivh_unsupported -> "supported_instructions" | Ivh_illegal -> "illegal instruction" end in let events_out = match events with [] -> Nothing | _ -> Just events end in - let mode = (make_interpreter_mode true false) in + let mode = (make_interpreter_mode true false debug) in match thunk() with | (Interp.Value value,_,_) -> if exn_seen @@ -374,8 +374,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Ivh_analysis -> (Ivh_value value, events_out) | _ -> (match value with - | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) - | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ -> + | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out) + | Interp_ast.V_ctor (Id_aux (Id "None") _) _ _ _ -> (match (ivh_mode,arg) with | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out) | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out) @@ -384,27 +384,27 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | _ -> (Ivh_error (Interp_interface.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end) | (Interp.Error l msg,_,_) -> (Ivh_error (Interp_interface.Internal_error msg), events_out) | (Interp.Action (Interp.Return value) stack,_,_) -> - interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen + interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just value)) | (Interp.Action (Interp.Call_extern i value) stack,_,_) -> match List.lookup i (Interp_lib.library_functions direction) with | Nothing -> (Ivh_error (Interp_interface.Internal_error ("External function not available " ^ i)), events_out) | Just f -> - interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen + interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just (f value))) end | (Interp.Action (Interp.Fail v) stack, _, _) -> match (Interp.detaint v) with - | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> + | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) -> (Ivh_error (Interp_interface.Internal_error ("Assert failed: " ^ s)), events_out) | _ -> (Ivh_error (Interp_interface.Internal_error "Assert failed"), events_out) end | (Interp.Action (Interp.Exit exp) stack,_,_) -> - interp_to_value_helper arg ivh_mode err_str instr direction registers events true + interp_to_value_helper debug arg ivh_mode err_str instr direction registers events true (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing) | (Interp.Action (Interp.Read_reg r slice) stack,_,_) -> let rname = match r with - | Interp.Reg (Id_aux (Id i) _) _ _ -> i - | Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i + | Interp_ast.Form_Reg (Id_aux (Id i) _) _ _ -> i + | Interp_ast.Form_SubReg (Id_aux (Id i) _) (Interp_ast.Form_Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i | _ -> Assert_extra.failwith "Reg not following expected structure" end in let err_value = (Ivh_error (Interp_interface.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)), @@ -418,12 +418,12 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev | Just v -> let value = intern_reg_value v in (* let _ = Interp.debug_print ("Register read of " ^ rname ^ " returning value " ^ (Interp.string_of_value value) ^ "\n") in *) - interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen + interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen (fun _ -> Interp.resume mode stack (Just value)) end end) | (Interp.Action (Interp.Write_reg r slice value) stack,_,_) -> let ext_reg = extern_reg r slice in let reg_value = extern_reg_value ext_reg value in - interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events) + interp_to_value_helper debug arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events) exn_seen (fun _ -> Interp.resume mode stack Nothing) | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out) @@ -450,25 +450,26 @@ let call_external_functions direction outcome = | Just f -> Just (f value) end | _ -> Nothing end -let build_context defs reads writes write_eas write_vals barriers excl_res externs = +let build_context debug defs reads writes write_eas write_vals barriers excl_res externs = (*TODO add externs to to_top_env*) - match Interp.to_top_env call_external_functions defs with - | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> + match Interp.to_top_env debug call_external_functions defs with + | (_,((Interp.Env _ _ dir _ _ _ _ _ debug) as context)) -> Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers excl_res externs end let translate_address top_level end_flag thunk_name registers address = let (Address bytes i) = address in - let mode = make_mode true false in - let int_mode = mode.internal_mode in let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in + let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in + let mode = make_mode true false debug in + let int_mode = mode.internal_mode in let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in - let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (address_error,events) = - interp_to_value_helper (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction + interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction registers [] false (fun _ -> Interp.resume int_mode @@ -489,7 +490,7 @@ end let value_of_instruction_param direction (name,typ,v) = let vec = intern_ifield_value direction v in let v = match vec with - | Interp.V_vector start dir bits -> + | Interp_ast.V_vector start dir bits -> match typ with | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec @@ -500,19 +501,20 @@ let value_of_instruction_param direction (name,typ,v) = end in v let intern_instruction direction (name,parms) = - Interp.V_ctor (Interp.id_of_string name) (T_id "ast") Interp.C_Union - (Interp.V_tuple (List.map (value_of_instruction_param direction) parms)) + Interp_ast.V_ctor (Interp.id_of_string name) (T_id "ast") Interp_ast.C_Union + (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms)) let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction = - let mode = make_mode true false in - let int_mode = mode.internal_mode in let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in + let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in + let mode = make_mode true false debug in + let int_mode = mode.internal_mode in let intern_val = intern_instruction direction instruction in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in - let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (analysis_or_error,events) = - interp_to_value_helper Nothing Ivh_analysis val_str ("",[]) internal_direction + interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction registers [] false (fun _ -> Interp.resume int_mode @@ -523,31 +525,31 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis match (analysis_or_error) with | Ivh_value analysis -> (match analysis with - | Interp.V_tuple [Interp.V_list regs1; - Interp.V_list regs2; - Interp.V_list regs3; - Interp.V_list nias; + | Interp_ast.V_tuple [Interp_ast.V_list regs1; + Interp_ast.V_list regs2; + Interp_ast.V_list regs3; + Interp_ast.V_list nias; dia; ik] -> let reg_to_reg_name v = match v with - | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) -> + | Interp_ast.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp_ast.V_lit (L_aux (L_string n) _)) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg n start length direction - | Interp.V_ctor (Id_aux (Id "RSlice") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_num s1) _); - Interp.V_lit (L_aux (L_num s2) _);]) -> + | Interp_ast.V_ctor (Id_aux (Id "RSlice") _) _ _ + (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); + Interp_ast.V_lit (L_aux (L_num s1) _); + Interp_ast.V_lit (L_aux (L_num s2) _);]) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg_slice n start direction (extern_slice direction start (natFromInteger s1, natFromInteger s2)) (*Note, this may need to change order depending on the direction*) - | Interp.V_ctor (Id_aux (Id "RSliceBit") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_num s) _);]) -> + | Interp_ast.V_ctor (Id_aux (Id "RSliceBit") _) _ _ + (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); + Interp_ast.V_lit (L_aux (L_num s) _);]) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in Reg_slice n start direction (extern_slice direction start (natFromInteger s,natFromInteger s)) - | Interp.V_ctor (Id_aux (Id "RField") _) _ _ - (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _); - Interp.V_lit (L_aux (L_string f) _);]) -> + | Interp_ast.V_ctor (Id_aux (Id "RField") _) _ _ + (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _); + Interp_ast.V_lit (L_aux (L_string f) _);]) -> let (start,length,direction,span) = regn_to_reg_details n (Just f) in Reg_field n start direction f (extern_slice direction start span) | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end @@ -556,23 +558,23 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Just addr -> addr | Nothing -> failwith "get_nia encountered invalid address" end in let dia_to_dia = function - | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none - | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address -> + | Interp_ast.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none + | Interp_ast.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address -> DIA_concrete_address (get_addr address) - | Interp.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) + | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return dia of expected type" end in let nia_to_nia = function - | Interp.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor - | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> NIA_concrete_address (get_addr address) - | Interp.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR - | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR - | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> NIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let ik_to_ik = function - | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ - (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> + | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> IK_barrier (match b with | "Barrier_Sync" -> Barrier_Sync | "Barrier_LwSync" -> Barrier_LwSync @@ -587,8 +589,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_ISB" -> Barrier_ISB | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC end) - | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ - (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> IK_mem_read (match r with | "Read_plain" -> Read_plain | "Read_reserve" -> Read_reserve @@ -597,8 +599,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Read_exclusive_acquire" -> Read_exclusive_acquire | "Read_stream" -> Read_stream end) - | Interp.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ - (Interp.V_ctor (Id_aux (Id w) _) _ _ _) -> + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> IK_mem_write (match w with | "Write_plain" -> Write_plain | "Write_conditional" -> Write_conditional @@ -606,9 +608,9 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Write_exclusive" -> Write_exclusive | "Write_exclusive_release" -> Write_exclusive_release end) - | Interp.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> + | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> IK_cond_branch - | Interp.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> + | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" end in @@ -646,17 +648,17 @@ end let interp_value_to_instr_external top_level instr = - let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _) = top_level in + let (Context (Interp.Env _ instructions _ _ _ _ _ _ debug) _ _ _ _ _ _ _ _ _ _) = top_level in match instr with - | Interp.V_ctor (Id_aux (Id i) _) _ _ parm -> + | Interp_ast.V_ctor (Id_aux (Id i) _) _ _ parm -> match (find_instruction i instructions) with | Just(Instruction_extractor.Instr_form name parms effects) -> match (parm,parms) with - | (Interp.V_lit (L_aux L_unit _),[]) -> (name, []) + | (Interp_ast.V_lit (L_aux L_unit _),[]) -> (name, []) | (value,[(p_name,ie_typ)]) -> let t = migrate_typ ie_typ in (name, [(p_name,t, (extern_ifield_value name p_name value t))]) - | (Interp.V_tuple vals,parms) -> + | (Interp_ast.V_tuple vals,parms) -> (name, (Interp_utilities.map2 (fun value (p_name,ie_typ) -> let t = migrate_typ ie_typ in @@ -670,14 +672,14 @@ let interp_value_to_instr_external top_level instr = let decode_to_instruction top_level registers value : instruction_or_decode_error = - let mode = make_interpreter_mode true false in - let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in + let (Context ((Interp.Env _ instructions _ _ _ _ _ _ debug) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in + let mode = make_interpreter_mode true false debug in let intern_val = intern_opcode direction value in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in - let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (instr_decoded_error,events) = - interp_to_value_helper (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false + interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false (fun _ -> Interp.resume mode (Interp.Thunk_frame @@ -687,7 +689,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro | Ivh_value instr -> let instr_external = interp_value_to_instr_external top_level instr in let (instr_decoded_error,events) = - interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction + interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction registers [] false (fun _ -> Interp.resume mode @@ -729,7 +731,7 @@ let instr_external_to_interp_value top_level instr = let get_value (_,typ,v) = let vec = intern_ifield_value direction v in match vec with - | Interp.V_vector start dir bits -> + | Interp_ast.V_vector start dir bits -> match typ with | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec @@ -740,12 +742,12 @@ let instr_external_to_interp_value top_level instr = end in let parmsV = match parms with - | [] -> Interp.V_lit (L_aux L_unit Unknown) - | _ -> Interp.V_tuple (List.map get_value parms) + | [] -> Interp_ast.V_lit (L_aux L_unit Unknown) + | _ -> Interp_ast.V_tuple (List.map get_value parms) end in (*This type shouldn't be hard-coded*) - Interp.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) - (T_id "ast") Interp.C_Union parmsV + Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) + (T_id "ast") Interp_ast.C_Union parmsV val instruction_to_istate : context -> instruction -> instruction_state let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state = @@ -761,7 +763,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct let rec interp_to_outcome mode context thunk = let (Context _ direction mem_reads mem_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers excl_res spec_externs) = context in - let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in + let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in match thunk () with | (Interp.Value _,lm,le) -> (Done,lm) | (Interp.Error l msg,lm,le) -> (Error msg,lm) @@ -771,7 +773,7 @@ let rec interp_to_outcome mode context thunk = (Read_reg (extern_reg reg_form slice) (fun v -> let v = (intern_reg_value v) in - let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in + let v = if mode.internal_mode.Interp.track_values then (Interp_ast.V_track v (Set.fromList [reg_form])) else v in IState (Interp.add_answer_to_stack next_state v) context), lm) | Interp.Write_reg reg_form slice value -> let reg_name = extern_reg reg_form slice in @@ -798,7 +800,7 @@ let rec interp_to_outcome mode context thunk = | Just bs -> Just (integer_of_byte_list bs) | _ -> Nothing end in Read_mem_tagged read_k (Address_lifted location address_int) length tracking - (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context) + (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp_ast.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context) else Error ("Memory address on read is not 64 bits") | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) @@ -844,7 +846,7 @@ let rec interp_to_outcome mode context thunk = | (Just (MV parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with - | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) + | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) | _ -> extern_with_track mode extern_mem_value write_val end in let location_opt = match parmf mode address_val with | Nothing -> Nothing @@ -863,7 +865,7 @@ let rec interp_to_outcome mode context thunk = | (Just (MVT parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with - | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) + | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) | _ -> extern_with_track mode extern_mem_value write_val end in let location_opt = match parmf mode address_val with | Nothing -> Nothing @@ -913,7 +915,7 @@ let rec interp_to_outcome mode context thunk = (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm) | Interp.Fail value -> (match value with - | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm) + | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm) | _ -> (Fail Nothing,lm) end) | Interp.Exit e -> (Escape (match e with @@ -1028,9 +1030,9 @@ let rec ie_loop mode register_values (IState interp_state context) = | _ -> Assert_extra.failwith "interp_to_outcome may have produced a nondet action" end ;; -val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event -let interp_exhaustive register_values i_state = - let mode = make_mode_exhaustive in +val interp_exhaustive : bool -> maybe (list (reg_name * register_value)) -> instruction_state -> list event +let interp_exhaustive debug register_values i_state = + let mode = make_mode_exhaustive debug in match ie_loop mode register_values i_state with | (events,_) -> events end @@ -1086,7 +1088,7 @@ and state_to_outcome_s pp_instruction_state mode state = let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in (next_outcome, Just ((pp_instruction_state state), - (fun env -> interp_exhaustive (Just env) state)) + (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state)) ) val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 0ce7b43a..937db466 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -162,7 +162,7 @@ end type interpreter_state = Interp.stack (*Deem abstract*) (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *) -type specification = Interp_ast.defs Interp.tannot (*Deem abstract*) +type specification = Interp_ast.defs Interp_ast.tannot (*Deem abstract*) type interpreter_mode = Interp.interp_mode (*Deem abstract*) type interp_mode = <| internal_mode: interpreter_mode |> val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode @@ -171,12 +171,12 @@ val tracking_dependencies : interp_mode -> bool (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) -type external_functions = list (string * (Interp.value -> Interp.value)) +type external_functions = list (string * (Interp_ast.value -> Interp_ast.value)) (*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*) type barriers = list (string * barrier_kind) -type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name)) -type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value +type memory_parameter_transformer = interp_mode -> Interp_ast.value -> (memory_value * nat * maybe (list reg_name)) +type optional_memory_transformer = interp_mode -> Interp_ast.value -> maybe memory_value type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) type memory_read_tagged = MRT of read_kind * memory_parameter_transformer @@ -264,7 +264,7 @@ val initial_instruction_state : context -> string -> list register_value -> inst (* string is a function name, list of value are the parameters to that function *) type instruction_or_decode_error = - | IDE_instr of instruction * Interp.value + | IDE_instr of instruction * Interp_ast.value | IDE_decode_error of decode_error (** propose to remove the following type and use the above instead *) diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 36a31f3f..40dbab88 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -54,6 +54,11 @@ open import Bool type signed = Unsigned | Signed +val debug_print : string -> unit +declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s + +let print s = let _ = debug_print (string_of_value s) in V_lit(L_aux L_unit Unknown) + let hardware_mod (a: integer) (b:integer) : integer = if a < 0 && b < 0 then (abs a) mod (abs b) @@ -61,13 +66,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b - + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1) let (max_64 : integer) = integerFromNat ((natPow 2 63) - 1) @@ -78,23 +86,29 @@ let (min_32 : integer) = integerNegate (integerFromNat (natPow 2 31)) (*2147483 let (max_8 : integer) = (integerFromNat 127) let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128) let (max_5 : integer) = (integerFromNat 31) -let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32) val get_max_representable_in : signed -> nat -> integer let get_max_representable_in sign n = - if (n = 64) then match sign with | Signed -> max_64 | Unsigned -> max_64u end - else if (n=32) then match sign with | Signed -> max_32 | Unsigned -> max_32u end - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | Signed -> 2**n - 1 | Unsigned -> 2**n end + match (sign, n) with + | (Signed, 64) -> max_64 + | (Unsigned, 64) -> max_64u + | (Signed, 32) -> max_32 + | (Unsigned, 32) -> max_32u + | (Signed, 8) -> max_8 + | (Unsigned, 5) -> max_5 + | (Signed, _) -> 2**(n -1) - 1 + | (Unsigned, _) -> 2**n - 1 + end val get_min_representable_in : signed -> nat -> integer -let get_min_representable_in _ n = - if (n = 64) then min_64 - else if (n=32) then min_32 - else if (n=8) then min_8 - else if (n=5) then min_5 - else 0-(2**n) +let get_min_representable_in sign n = + match (sign, n) with + | (Unsigned, _) -> 0 + | (Signed, 64) -> min_64 + | (Signed, 32) -> min_32 + | (Signed, 8) -> min_8 + | (Signed, _) -> 0-(2**(n-1)) + end let ignore_sail x = V_lit (L_aux L_unit Unknown) ;; @@ -428,6 +442,8 @@ end) let neq = compose neg eq ;; let neq_vec = compose neg eq_vec +let neq_vec_range = compose neg eq_vec_range +let neq_range_vec = compose neg eq_range_vec let rec v_abs v = retaint v (match detaint v with | V_lit (L_aux arg la) -> @@ -1012,6 +1028,7 @@ let library_functions direction = [ ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1); ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1); ("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1); + ("print", print); ("power", arith_op power); ("eq", eq); ("eq_vec", eq_vec); @@ -1021,8 +1038,8 @@ let library_functions direction = [ ("eq_range", eq); ("neq", neq); ("neq_vec", neq_vec); - ("neq_vec_range", neq); - ("neq_range_vec", neq); + ("neq_vec_range", neq_vec_range); + ("neq_range_vec", neq_range_vec); ("neq_bit", neq); ("neq_range", neq); ("vec_concat", vec_concat); @@ -1055,8 +1072,8 @@ let library_functions direction = [ ("gt_range_vec", compare_op_range_vec (>) Signed); ("lteq_vec_range", compare_op_vec_range (<=) Signed); ("gteq_vec_range", compare_op_vec_range (>=) Signed); - ("lteq_range_vec", compare_op_vec_range (<=) Signed); - ("gteq_range_vec", compare_op_vec_range (>=) Signed); + ("lteq_range_vec", compare_op_range_vec (<=) Signed); + ("gteq_range_vec", compare_op_range_vec (>=) Signed); ("lteq_vec", compare_op_vec (<=) Signed); ("gteq_vec", compare_op_vec (>=) Signed); ("lt_vec_signed", compare_op_vec (<) Signed); diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index b019fb53..a51598b3 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -71,6 +71,92 @@ let pp_format_id (Id_aux(i,_)) = | Id(i) -> i | DeIid(x) -> "(deinfix " ^ x ^ ")" +let lit_to_string = function + | L_unit -> "unit" + | L_zero -> "0b0" + | L_one -> "0b1" + | L_true -> "true" + | L_false -> "false" + | L_num n -> Nat_big_num.to_string n + | L_hex s -> "0x"^s + | L_bin s -> "0b"^s + | L_undef -> "undefined" + | L_string s -> "\"" ^ s ^ "\"" +;; + +let id_to_string = function + | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s +;; + +let rec loc_to_string = function + | Unknown -> "location unknown" + | Int(s,_) -> s + | Generated l -> "Generated near " ^ loc_to_string l + | Range(s,fline,fchar,tline,tchar) -> + if fline = tline + then sprintf "%s:%d:%d" s fline fchar + else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar +;; + +let collapse_leading s = + if String.length s <= 8 then s else + let first_bit = s.[0] in + let templ = sprintf "%c...%c" first_bit first_bit in + + let rec find_first_diff str cha pos = + if pos >= String.length str then None + else if str.[pos] != cha then Some pos + else find_first_diff str cha (pos+1) + in + + match find_first_diff s first_bit 0 with + | None -> templ + | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos)) + | _ -> s +;; + +(* pp the bytes of a Bytevector as a hex value *) + +let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function + | Interp_ast.V_lit(L_aux(L_zero, _)) -> "0" + | Interp_ast.V_lit(L_aux(L_one, _)) -> "1" + | Interp_ast.V_lit(L_aux(L_undef, _)) -> "u" + | Interp_ast.V_unknown -> "?" + | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) + (List.map Interp.detaint l))) + ;; + + +let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function + | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory) + | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) + | Interp_ast.V_tuple l -> + let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in + sprintf "(%s)" repr + | Interp_ast.V_list l -> + let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in + sprintf "[||%s||]" repr + | Interp_ast.V_vector (first_index, inc, l) -> + let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in + let repr = + try bitvec_to_string l + with Failure _ -> + sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in + sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index) + | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> + val_to_string_internal mem (Interp_lib.fill_in_sparse v) + | Interp_ast.V_record(_, l) -> + let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in + let repr = String.concat "; " (List.map pp l) in + sprintf "{%s}" repr + | Interp_ast.V_ctor (id,_,_, value) -> + sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value) + | Interp_ast.V_register _ | Interp_ast.V_register_alias _ -> + sprintf "reg-as-value" + | Interp_ast.V_unknown -> "unknown" + | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v) +;; + (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) @@ -293,108 +379,108 @@ let doc_pat, doc_atomic_pat = in pat, atomic_pat let doc_exp, doc_let = - let rec exp env add_red show_hole_contents e = group (or_exp env add_red show_hole_contents e) - and or_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + let rec exp env mem add_red show_hole_contents e = group (or_exp env mem add_red show_hole_contents e) + and or_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) -> - doc_op (doc_id op) (and_exp env add_red show_hole_contents l) (or_exp env add_red show_hole_contents r) - | _ -> and_exp env add_red show_hole_contents expr - and and_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (and_exp env mem add_red show_hole_contents l) (or_exp env mem add_red show_hole_contents r) + | _ -> and_exp env mem add_red show_hole_contents expr + and and_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) -> - doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (and_exp env add_red show_hole_contents r) - | _ -> eq_exp env add_red show_hole_contents expr - and eq_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (and_exp env mem add_red show_hole_contents r) + | _ -> eq_exp env mem add_red show_hole_contents expr + and eq_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( (* XXX this is not very consistent - is the parser bogus here? *) "=" | "==" | "!=" | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" ),_) as op),r) -> - doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r) + doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r) (* XXX assignment should not have the same precedence as equal etc. *) | E_assign(le,exp) -> - doc_op coloneq (doc_lexp env add_red show_hole_contents le) (at_exp env add_red show_hole_contents exp) - | _ -> at_exp env add_red show_hole_contents expr - and at_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op coloneq (doc_lexp env mem add_red show_hole_contents le) (at_exp env mem add_red show_hole_contents exp) + | _ -> at_exp env mem add_red show_hole_contents expr + and at_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) -> - doc_op (doc_id op) (cons_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r) - | _ -> cons_exp env add_red show_hole_contents expr - and cons_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (cons_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r) + | _ -> cons_exp env mem add_red show_hole_contents expr + and cons_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_vector_append(l,r) -> - doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r) + doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r) | E_cons(l,r) -> - doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r) - | _ -> shift_exp env add_red show_hole_contents expr - and shift_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r) + | _ -> shift_exp env mem add_red show_hole_contents expr + and shift_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) -> - doc_op (doc_id op) (shift_exp env add_red show_hole_contents l) (plus_exp env add_red show_hole_contents r) - | _ -> plus_exp env add_red show_hole_contents expr - and plus_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (shift_exp env mem add_red show_hole_contents l) (plus_exp env mem add_red show_hole_contents r) + | _ -> plus_exp env mem add_red show_hole_contents expr + and plus_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("+" | "-"| "+_s" | "-_s" ),_) as op),r) -> - doc_op (doc_id op) (plus_exp env add_red show_hole_contents l) (star_exp env add_red show_hole_contents r) - | _ -> star_exp env add_red show_hole_contents expr - and star_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (plus_exp env mem add_red show_hole_contents l) (star_exp env mem add_red show_hole_contents r) + | _ -> star_exp env mem add_red show_hole_contents expr + and star_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( "*" | "/" | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) -> - doc_op (doc_id op) (star_exp env add_red show_hole_contents l) (starstar_exp env add_red show_hole_contents r) - | _ -> starstar_exp env add_red show_hole_contents expr - and starstar_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (star_exp env mem add_red show_hole_contents l) (starstar_exp env mem add_red show_hole_contents r) + | _ -> starstar_exp env mem add_red show_hole_contents expr + and starstar_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> - doc_op (doc_id op) (starstar_exp env add_red show_hole_contents l) (app_exp env add_red show_hole_contents r) - | E_if _ | E_for _ | E_let _ -> right_atomic_exp env add_red show_hole_contents expr - | _ -> app_exp env add_red show_hole_contents expr - and right_atomic_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_op (doc_id op) (starstar_exp env mem add_red show_hole_contents l) (app_exp env mem add_red show_hole_contents r) + | E_if _ | E_for _ | E_let _ -> right_atomic_exp env mem add_red show_hole_contents expr + | _ -> app_exp env mem add_red show_hole_contents expr + and right_atomic_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with (* Special case: omit "else ()" when the else branch is empty. *) | E_if(c,t,E_aux(E_block [], _)) -> - string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^ - string "then" ^^ space ^^ group (exp env add_red show_hole_contents t) + string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^ + string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t) | E_if(c,t,e) -> - string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^ - string "then" ^^ space ^^ group (exp env add_red show_hole_contents t) ^/^ - string "else" ^^ space ^^ group (exp env add_red show_hole_contents e) + string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^ + string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t) ^/^ + string "else" ^^ space ^^ group (exp env mem add_red show_hole_contents e) | E_for(id,exp1,exp2,exp3,order,exp4) -> string "foreach" ^^ space ^^ group (parens ( separate (break 1) [ doc_id id; - string "from " ^^ (atomic_exp env add_red show_hole_contents exp1); - string "to " ^^ (atomic_exp env add_red show_hole_contents exp2); - string "by " ^^ (atomic_exp env add_red show_hole_contents exp3); + string "from " ^^ (atomic_exp env mem add_red show_hole_contents exp1); + string "to " ^^ (atomic_exp env mem add_red show_hole_contents exp2); + string "by " ^^ (atomic_exp env mem add_red show_hole_contents exp3); string "in " ^^ doc_ord order ] )) ^/^ - (exp env add_red show_hole_contents exp4) - | E_let(leb,e) -> doc_op (string "in") (let_exp env add_red show_hole_contents leb) (exp env add_red show_hole_contents e) - | _ -> group (parens (exp env add_red show_hole_contents expr)) - and app_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + (exp env mem add_red show_hole_contents exp4) + | E_let(leb,e) -> doc_op (string "in") (let_exp env mem add_red show_hole_contents leb) (exp env mem add_red show_hole_contents e) + | _ -> group (parens (exp env mem add_red show_hole_contents expr)) + and app_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_app(f,args) -> - doc_unop (doc_id f) (parens (separate_map comma (exp env add_red show_hole_contents) args)) - | _ -> vaccess_exp env add_red show_hole_contents expr - and vaccess_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + doc_unop (doc_id f) (parens (separate_map comma (exp env mem add_red show_hole_contents) args)) + | _ -> vaccess_exp env mem add_red show_hole_contents expr + and vaccess_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with | E_vector_access(v,e) -> - (atomic_exp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e) + (atomic_exp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e) | E_vector_subrange(v,e1,e2) -> - (atomic_exp env add_red show_hole_contents v) ^^ - brackets (doc_op dotdot (exp env add_red show_hole_contents e1) (exp env add_red show_hole_contents e2)) - | _ -> field_exp env add_red show_hole_contents expr - and field_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with - | E_field(fexp,id) -> (atomic_exp env add_red show_hole_contents fexp) ^^ dot ^^ doc_id id - | _ -> atomic_exp env add_red show_hole_contents expr - and atomic_exp env add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with + (atomic_exp env mem add_red show_hole_contents v) ^^ + brackets (doc_op dotdot (exp env mem add_red show_hole_contents e1) (exp env mem add_red show_hole_contents e2)) + | _ -> field_exp env mem add_red show_hole_contents expr + and field_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with + | E_field(fexp,id) -> (atomic_exp env mem add_red show_hole_contents fexp) ^^ dot ^^ doc_id id + | _ -> atomic_exp env mem add_red show_hole_contents expr + and atomic_exp env mem add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with (* Special case: an empty block is equivalent to unit, but { } is a syntactic struct *) | E_block [] -> string "()" | E_block exps -> - let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in + let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in surround 2 1 lbrace exps_doc rbrace | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in + let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace) | E_id id -> (match id with | Id_aux(Id("0"), _) -> (match Interp.in_lenv env id with - | Interp.V_unknown -> string (add_red "[_]") + | Interp_ast.V_unknown -> string (add_red "[_]") | v -> if show_hole_contents then string (add_red (Interp.string_of_value v)) @@ -403,22 +489,22 @@ let doc_exp, doc_let = | E_lit lit -> doc_lit lit | E_cast(typ,e) -> if !ignore_casts then - atomic_exp env add_red show_hole_contents e + atomic_exp env mem add_red show_hole_contents e else - prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env add_red show_hole_contents e)) + prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env mem add_red show_hole_contents e)) | E_internal_cast(_,e) -> (* XXX ignore internal casts in the interpreter *) - atomic_exp env add_red show_hole_contents e + atomic_exp env mem add_red show_hole_contents e | E_tuple exps -> - parens (separate_map comma (exp env add_red show_hole_contents) exps) + parens (separate_map comma (exp env mem add_red show_hole_contents) exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - braces (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps) + braces (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps) | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> braces (doc_op (string "with") - (exp env add_red show_hole_contents e) - (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps)) + (exp env mem add_red show_hole_contents e) + (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps)) | E_vector exps -> - let default_print _ = brackets (separate_map comma (exp env add_red show_hole_contents) exps) in + let default_print _ = brackets (separate_map comma (exp env mem add_red show_hole_contents) exps) in (match exps with | [] -> default_print () | es -> @@ -441,28 +527,28 @@ let doc_exp, doc_let = let default_string = (match default with | Def_val_empty -> string "" - | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env add_red show_hole_contents e)]) in - let iexp (i,e) = doc_op equals (doc_int i) (exp env add_red show_hole_contents e) in + | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env mem add_red show_hole_contents e)]) in + let iexp (i,e) = doc_op equals (doc_int i) (exp env mem add_red show_hole_contents e) in brackets (concat [(separate_map comma iexp iexps);default_string]) | E_vector_update(v,e1,e2) -> brackets (doc_op (string "with") - (exp env add_red show_hole_contents v) - (doc_op equals (atomic_exp env add_red show_hole_contents e1) - (exp env add_red show_hole_contents e2))) + (exp env mem add_red show_hole_contents v) + (doc_op equals (atomic_exp env mem add_red show_hole_contents e1) + (exp env mem add_red show_hole_contents e2))) | E_vector_update_subrange(v,e1,e2,e3) -> brackets ( - doc_op (string "with") (exp env add_red show_hole_contents v) - (doc_op equals ((atomic_exp env add_red show_hole_contents e1) ^^ colon - ^^ (atomic_exp env add_red show_hole_contents e2)) (exp env add_red show_hole_contents e3))) + doc_op (string "with") (exp env mem add_red show_hole_contents v) + (doc_op equals ((atomic_exp env mem add_red show_hole_contents e1) ^^ colon + ^^ (atomic_exp env mem add_red show_hole_contents e2)) (exp env mem add_red show_hole_contents e3))) | E_list exps -> - squarebarbars (separate_map comma (exp env add_red show_hole_contents) exps) + squarebarbars (separate_map comma (exp env mem add_red show_hole_contents) exps) | E_case(e,pexps) -> - let opening = separate space [string "switch"; exp env add_red show_hole_contents e; lbrace] in - let cases = separate_map (break 1) (doc_case env add_red show_hole_contents) pexps in + let opening = separate space [string "switch"; exp env mem add_red show_hole_contents e; lbrace] in + let cases = separate_map (break 1) (doc_case env mem add_red show_hole_contents) pexps in surround 2 1 opening cases rbrace - | E_exit e -> separate space [string "exit"; exp env add_red show_hole_contents e;] - | E_return e -> separate space [string "return"; exp env add_red show_hole_contents e;] - | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env add_red show_hole_contents) [e; msg]) + | E_exit e -> separate space [string "exit"; exp env mem add_red show_hole_contents e;] + | E_return e -> separate space [string "return"; exp env mem add_red show_hole_contents e;] + | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) [e; msg]) (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) @@ -484,57 +570,59 @@ let doc_exp, doc_let = | "*_s" | "*_si" | "*_u" | "*_ui" | "**"), _)) , _) -> - group (parens (exp env add_red show_hole_contents expr)) + group (parens (exp env mem add_red show_hole_contents expr)) (* XXX fixup deinfix into infix ones *) | E_app_infix(l, (Id_aux((DeIid op), annot')), r) -> group (parens - (exp env add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot)))) + (exp env mem add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot)))) (* XXX default precedence for app_infix? *) | E_app_infix(l,op,r) -> failwith ("unexpected app_infix operator " ^ (pp_format_id op)) (* doc_op (doc_id op) (exp l) (exp r) *) (* XXX missing case *) - | E_comment _ | E_comment_struc _ -> string "" + | E_comment _ | E_comment_struc _ -> string "" + | E_internal_value v -> + string (val_to_string_internal mem v) | _-> failwith "internal expression escaped" - and let_exp env add_red show_hole_contents (LB_aux(lb,_)) = match lb with + and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> prefix 2 1 (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals]) - (exp env add_red show_hole_contents e) + (exp env mem add_red show_hole_contents e) | LB_val_implicit(pat,e) -> prefix 2 1 (separate space [string "let"; doc_atomic_pat pat; equals]) - (exp env add_red show_hole_contents e) + (exp env mem add_red show_hole_contents e) - and doc_fexp env add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) = - doc_op equals (doc_id id) (exp env add_red show_hole_contents e) + and doc_fexp env mem add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) = + doc_op equals (doc_id id) (exp env mem add_red show_hole_contents e) - and doc_case env add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env add_red show_hole_contents e)) + and doc_case env mem add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) = + doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env mem add_red show_hole_contents e)) (* lexps are parsed as eq_exp - we need to duplicate the precedence * structure for them *) - and doc_lexp env add_red show_hole_contents le = app_lexp env add_red show_hole_contents le - and app_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env add_red show_hole_contents) args) - | _ -> vaccess_lexp env add_red show_hole_contents le - and vaccess_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + and doc_lexp env mem add_red show_hole_contents le = app_lexp env mem add_red show_hole_contents le + and app_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) args) + | _ -> vaccess_lexp env mem add_red show_hole_contents le + and vaccess_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_vector(v,e) -> - (atomic_lexp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e) + (atomic_lexp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e) | LEXP_vector_range(v,e1,e2) -> - (atomic_lexp env add_red show_hole_contents v) ^^ - brackets ((exp env add_red show_hole_contents e1) ^^ dotdot ^^ (exp env add_red show_hole_contents e2)) - | _ -> field_lexp env add_red show_hole_contents le - and field_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_field(v,id) -> (atomic_lexp env add_red show_hole_contents v) ^^ dot ^^ doc_id id - | _ -> atomic_lexp env add_red show_hole_contents le - and atomic_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + (atomic_lexp env mem add_red show_hole_contents v) ^^ + brackets ((exp env mem add_red show_hole_contents e1) ^^ dotdot ^^ (exp env mem add_red show_hole_contents e2)) + | _ -> field_lexp env mem add_red show_hole_contents le + and field_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_field(v,id) -> (atomic_lexp env mem add_red show_hole_contents v) ^^ dot ^^ doc_id id + | _ -> atomic_lexp env mem add_red show_hole_contents le + and atomic_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_id id -> doc_id id | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) - | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env add_red show_hole_contents) lexps)) + | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env mem add_red show_hole_contents) lexps)) | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ - | LEXP_field _ -> group (parens (doc_lexp env add_red show_hole_contents le)) + | LEXP_field _ -> group (parens (doc_lexp env mem add_red show_hole_contents le)) (* expose doc_exp and doc_let *) in exp, let_exp @@ -611,15 +699,15 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with | Effect_opt_pure -> string "pure" | Effect_opt_effect e -> doc_effects e -let doc_funcl env add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env add_red false exp)) +let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env mem add_red false exp)) -let doc_fundef env add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) = +let doc_fundef env mem add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) = match fcls with | [] -> failwith "FD_function with empty function list" | _ -> let sep = hardline ^^ string "and" ^^ space in - let clauses = separate_map sep (doc_funcl env add_red) fcls in + let clauses = separate_map sep (doc_funcl env mem add_red) fcls in separate space [string "function"; doc_rec r ^^ doc_tannot_opt typa; string "effect"; doc_effects_opt efa; @@ -629,7 +717,7 @@ let doc_dec (DEC_aux(d,_)) = match d with | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id] | _ -> failwith "interpreter printing out declarations unexpectedly" -let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with +let doc_scattered env mem add_red (SD_aux (sdef, _)) = match sdef with | SD_scattered_function (r, typa, efa, id) -> separate space [ string "scattered function"; @@ -641,35 +729,35 @@ let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns) (doc_typquant tq empty) | SD_scattered_funcl funcl -> - string "function clause" ^^ space ^^ doc_funcl env add_red funcl + string "function clause" ^^ space ^^ doc_funcl env mem add_red funcl | SD_scattered_unioncl (id, tu) -> separate space [string "union"; doc_id id; string "member"; doc_type_union tu] | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id -let rec doc_def env add_red def = group (match def with +let rec doc_def env mem add_red def = group (match def with | DEF_default df -> doc_default df | DEF_spec v_spec -> doc_spec v_spec | DEF_type t_def -> doc_typdef t_def | DEF_kind k_def -> failwith "interpreter unexpectedly printing kind def" - | DEF_fundef f_def -> doc_fundef env add_red f_def - | DEF_val lbind -> doc_let env add_red false lbind + | DEF_fundef f_def -> doc_fundef env mem add_red f_def + | DEF_val lbind -> doc_let env mem add_red false lbind | DEF_reg_dec dec -> doc_dec dec - | DEF_scattered sdef -> doc_scattered env add_red sdef - | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env add_red comm_dec ^^ string "*)" + | DEF_scattered sdef -> doc_scattered env mem add_red sdef + | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env mem add_red comm_dec ^^ string "*)" ) ^^ hardline -and doc_comm_dec env add_red dec = match dec with +and doc_comm_dec env mem add_red dec = match dec with | DC_comm s -> string s - | DC_comm_struct d -> doc_def env add_red d + | DC_comm_struct d -> doc_def env mem add_red d -let doc_defs env add_red (Defs(defs)) = - separate_map hardline (doc_def env add_red) defs +let doc_defs env mem add_red (Defs(defs)) = + separate_map hardline (doc_def env mem add_red) defs let print ?(len=80) channel doc = ToChannel.pretty 1. len channel doc let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc -let pp_exp env add_red show_hole_contents e = +let pp_exp env mem add_red show_hole_contents e = let b = Buffer.create 20 in - to_buf b (doc_exp env add_red show_hole_contents e); + to_buf b (doc_exp env mem add_red show_hole_contents e); Buffer.contents b diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index f0c0d392..79a86113 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -49,60 +49,13 @@ open Interp_interface ;; open Nat_big_num ;; -let lit_to_string = function - | L_unit -> "unit" - | L_zero -> "0b0" - | L_one -> "0b1" - | L_true -> "true" - | L_false -> "false" - | L_num n -> to_string n - | L_hex s -> "0x"^s - | L_bin s -> "0b"^s - | L_undef -> "undefined" - | L_string s -> "\"" ^ s ^ "\"" -;; - -let id_to_string = function - | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s -;; - -let rec loc_to_string = function - | Unknown -> "location unknown" - | Int(s,_) -> s - | Generated l -> "Generated near " ^ loc_to_string l - | Range(s,fline,fchar,tline,tchar) -> - if fline = tline - then sprintf "%s:%d:%d" s fline fchar - else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar -;; - -let collapse_leading s = - if String.length s <= 8 then s else - let first_bit = s.[0] in - let templ = sprintf "%c...%c" first_bit first_bit in - - let rec find_first_diff str cha pos = - if pos >= String.length str then None - else if str.[pos] != cha then Some pos - else find_first_diff str cha (pos+1) - in - - match find_first_diff s first_bit 0 with - | None -> templ - | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos)) - | _ -> s -;; +let val_to_string_internal = Pretty_interp.val_to_string_internal ;; +let lit_to_string = Pretty_interp.lit_to_string ;; +let id_to_string = Pretty_interp.id_to_string ;; +let loc_to_string = Pretty_interp.loc_to_string ;; +let bitvec_to_string = Pretty_interp.bitvec_to_string ;; +let collapse_leading = Pretty_interp.collapse_leading ;; -let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function - | Interp.V_lit(L_aux(L_zero, _)) -> "0" - | Interp.V_lit(L_aux(L_one, _)) -> "1" - | Interp.V_lit(L_aux(L_undef, _)) -> "u" - | Interp.V_unknown -> "?" - | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) - (List.map Interp.detaint l))) -;; - -(* pp the bytes of a Bytevector as a hex value *) type bits_lifted_homogenous = | Bitslh_concrete of bit list @@ -322,36 +275,6 @@ let reg_name_to_string = function let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies) -let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function - | Interp.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory) - | Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) - | Interp.V_tuple l -> - let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in - sprintf "(%s)" repr - | Interp.V_list l -> - let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in - sprintf "[||%s||]" repr - | Interp.V_vector (first_index, inc, l) -> - let last_index = (if (Interp.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in - let repr = - try bitvec_to_string l - with Failure _ -> - sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in - sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index) - | (Interp.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> - val_to_string_internal mem (Interp_lib.fill_in_sparse v) - | Interp.V_record(_, l) -> - let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in - let repr = String.concat "; " (List.map pp l) in - sprintf "{%s}" repr - | Interp.V_ctor (id,_,_, value) -> - sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value) - | Interp.V_register _ | Interp.V_register_alias _ -> - sprintf "reg-as-value" - | Interp.V_unknown -> "unknown" - | Interp.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v) -;; - let rec top_frame_exp_state = function | Interp.Top -> raise (Invalid_argument "top_frame_exp") | Interp.Hole_frame(_, e, _, env, mem, Interp.Top) @@ -485,27 +408,27 @@ let yellow = color true 3 let blue = color true 4 let grey = color false 7 -let exp_to_string env show_hole_value e = Pretty_interp.pp_exp env red show_hole_value e +let exp_to_string env mem show_hole_value e = Pretty_interp.pp_exp env mem red show_hole_value e let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l -let print_exp printer env show_hole_value e = - printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env red show_hole_value e) ^ "\n") +let print_exp printer env mem show_hole_value e = + printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env mem red show_hole_value e) ^ "\n") let instruction_state_to_string (IState(stack, _)) = - List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env true e) ^ "\n" ^ es) (compact_stack stack) "" + List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env mem true e) ^ "\n" ^ es) (compact_stack stack) "" let top_instruction_state_to_string (IState(stack,_)) = - let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env true exp + let (exp,(env,mem)) = top_frame_exp_state stack in exp_to_string env mem true exp let instruction_stack_to_string (IState(stack,_)) = let rec stack_to_string = function Interp.Top -> "" | Interp.Hole_frame(_,e,_,env,mem,Interp.Top) | Interp.Thunk_frame(e,_,env,mem,Interp.Top) -> - exp_to_string env true e + exp_to_string env mem true e | Interp.Hole_frame(_,e,_,env,mem,s) | Interp.Thunk_frame(e,_,env,mem,s) -> - (exp_to_string env false e) ^ "\n----------------------------------------------------------\n" ^ + (exp_to_string env mem false e) ^ "\n----------------------------------------------------------\n" ^ (stack_to_string s) in match stack with @@ -536,7 +459,7 @@ let instr_parm_to_string (name, typ, value) = | Other -> "Unrepresentable external value" | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value D_increasing value) in match Interp_lib.to_num Interp_lib.Unsigned intern_v with - | Interp.V_lit (L_aux(L_num n, _)) -> to_string n + | Interp_ast.V_lit (L_aux(L_num n, _)) -> to_string n | _ -> ifield_to_string value let rec instr_parms_to_string ps = @@ -551,12 +474,12 @@ let instruction_to_string (name, parms) = ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms let print_backtrace_compact printer (IState(stack,_)) = - List.iter (fun (e,(env,mem)) -> print_exp printer env true e) (compact_stack stack) + List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack) let print_stack printer is = printer (instruction_stack_to_string is) let print_continuation printer (IState(stack,_)) = - let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env true e + let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env mem true e let print_instruction printer instr = printer (instruction_to_string instr) let pp_instruction_state state () = diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli index f629a307..85744d61 100644 --- a/src/lem_interp/printing_functions.mli +++ b/src/lem_interp/printing_functions.mli @@ -10,7 +10,7 @@ val loc_to_string : l -> string val get_loc : tannot exp -> string (*interp_interface.value to string*) val reg_value_to_string : register_value -> string -val val_to_string_internal : Interp.lmem -> Interp.value -> string +val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*) val val_to_hex_string : value0 -> string*) @@ -19,7 +19,7 @@ val reg_name_to_string : reg_name -> string (* format the register dependencies *) val dependencies_to_string : reg_name list -> string (* formats an expression, using interp_pretty *) -val exp_to_string : Interp.lenv -> bool -> tannot exp -> string +val exp_to_string : Interp.lenv -> Interp.lmem -> bool -> tannot exp -> string (* Functions to set the color of parts of the output *) type ppmode = @@ -55,7 +55,7 @@ val local_variables_to_string : instruction_state -> string val instruction_to_string : instruction -> string (*Functions to take a print function and cause a print event for the above functions *) -val print_exp : (string-> unit) -> Interp.lenv -> bool -> tannot exp -> unit +val print_exp : (string-> unit) -> Interp.lenv -> Interp.lmem -> bool -> tannot exp -> unit val print_backtrace_compact : (string -> unit) -> instruction_state -> unit val print_continuation : (string -> unit) -> instruction_state -> unit val print_instruction : (string -> unit) -> instruction -> unit diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index d6f6e30c..6978aeb9 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -292,7 +292,7 @@ let run interact mode env stack | "e" | "exh" | "exhaust" -> interactf "interpreting exhaustively from current state\n"; - let events = interp_exhaustive None stack in + let events = interp_exhaustive false None stack in interactf "%s" (format_events events); interact mode env stack | "c" | "cont" | "continuation" -> @@ -339,7 +339,7 @@ let run let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in let loc = get_loc (compact_exp top_exp) in if mode = Step || force then begin - interactf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp); + interactf "%s\n" (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp); interact mode env' state end else mode in @@ -433,7 +433,7 @@ let run (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in show "nondeterministic evaluation begun" "" "" ""; let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> - loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) + loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next)) choose_order (false,mode,!track_dependencies,env'); in show "nondeterministic evaluation ended" "" "" ""; (step next,env',next) @@ -445,7 +445,7 @@ let run else begin show "undefined triggered a non_det" "" "" ""; let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> - loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) + loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next)) choose_order (false,mode,!track_dependencies,env'); in (step i_state,env',i_state) end | Escape0(Some e,_) -> @@ -462,15 +462,15 @@ let run | Write_memv1 _ -> assert false) (*| _ -> assert false*) in - loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies) next) in + loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) next) in let mode = match mode with | None -> if eager_eval then Run else Step | Some m -> m in - let imode = make_mode eager_eval !track_dependencies in + let imode = make_mode eager_eval !track_dependencies false in let (IState(instr_state,context)) = istate in let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in interactf "%s: %s %s\n" (grey name) (blue "evaluate") - (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp); + (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp); try Printexc.record_backtrace true; loop mode (reg, mem,tagmem) (Interp_inter_imp.interp0 imode istate) diff --git a/src/lem_interp/type_check.lem b/src/lem_interp/type_check.lem index 179e53d3..6c6cda1a 100644 --- a/src/lem_interp/type_check.lem +++ b/src/lem_interp/type_check.lem @@ -54,7 +54,7 @@ open import Interp_ast open import Interp_utilities open import Instruction_extractor -type tannot = Interp_utilities.tannot +type tannot = Interp_ast.tannot (*Env of t counter, nexp counter, order counter, type env, order env, nexp env, nec env*) type envs = | Env of nat * nat * nat * map string (t * nec) * map string order * map string ne * map string nec diff --git a/src/test/lib/Makefile b/src/test/lib/Makefile new file mode 100644 index 00000000..d2185866 --- /dev/null +++ b/src/test/lib/Makefile @@ -0,0 +1,55 @@ + +# Disable built-in make madness +MAKEFLAGS=-r +.SUFFIXES: + +TESTS=div.sail + +BITBUCKET_DIR:=$(realpath ../../../../) +LEM_DIR:=$(BITBUCKET_DIR)/lem +LEM:=$(LEM_DIR)/lem +LEMLIB = $(LEM_DIR)/ocaml-lib +SAIL_DIR:=$(BITBUCKET_DIR)/sail/src +SAIL:=$(SAIL_DIR)/sail.native +ZARITH_DIR:=$(LEM_DIR)/ocaml-lib/dependencies/zarith +ZARITH_LIB:=$(ZARITH_DIR)/zarith.cmxa +SAIL_VALUES:=$(SAIL_DIR)/gen_lib/sail_values.ml + +BUILD_DIR:=_build + +TESTS:=$(wildcard tests/*.sail) +OCAML_RESULTS:=$(addsuffix _embed.out,$(addprefix $(BUILD_DIR)/,$(notdir $(basename $(TESTS))))) +INTERP_RESULTS:=$(addsuffix _interp.out,$(addprefix $(BUILD_DIR)/,$(notdir $(basename $(TESTS))))) + +all: tests.xml + +clean: + rm -rf $(BUILD_DIR) tests.xml + +$(BUILD_DIR): + mkdir -p $@ + +$(BUILD_DIR)/run_test_embed.ml: | $(BUILD_DIR) + cp run_test_embed.ml $(BUILD_DIR) + +$(BUILD_DIR)/run_test_interp.ml: | $(BUILD_DIR) + cp run_test_interp.ml $(BUILD_DIR) + +$(BUILD_DIR)/sail_values.ml: | $(BUILD_DIR) + cp $(SAIL_VALUES) $(BUILD_DIR) + +$(BUILD_DIR)/%_embed.out : tests/%.sail $(BUILD_DIR)/run_test_embed.ml $(BUILD_DIR)/sail_values.ml + cd $(BUILD_DIR) && \ + $(SAIL) -ocaml ../test_prelude.sail ../$< ../test_epilogue.sail -o test && \ + ocamlopt -I $(ZARITH_DIR) $(ZARITH_LIB) sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \ + ./test_embed.native > $(notdir $@) + +$(BUILD_DIR)/%_interp.out : tests/%.sail $(BUILD_DIR)/run_test_interp.ml + cd $(BUILD_DIR) && \ + $(SAIL) -lem_ast ../test_prelude.sail ../$< ../test_epilogue.sail -o test_lem_ast && \ + $(LEM) -ocaml test_lem_ast.lem -lib $(SAIL_DIR)/lem_interp && \ + ocamlfind ocamlopt -g -package num -I $(ZARITH_DIR) -I $(SAIL_DIR)/_build/lem_interp -I $(LEMLIB) -linkpkg $(ZARITH_LIB) $(LEMLIB)/extract.cmxa $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \ + ./test_interp.native >$(notdir $@) 2>&1 + +tests.xml: $(OCAML_RESULTS) $(INTERP_RESULTS) + ./test_to_junit.sh $^ diff --git a/src/test/lib/run_test_embed.ml b/src/test/lib/run_test_embed.ml new file mode 100644 index 00000000..f7b45316 --- /dev/null +++ b/src/test/lib/run_test_embed.ml @@ -0,0 +1,2 @@ +Test._run() + diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml new file mode 100644 index 00000000..3446ef9f --- /dev/null +++ b/src/test/lib/run_test_interp.ml @@ -0,0 +1,51 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Interp_interface ;; +open Interp_inter_imp ;; +open Sail_impl_base ;; + +let doit () = + let context = build_context Test_lem_ast.defs [] [] [] [] [] [] [] None [] in + translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));; + +doit () ;; diff --git a/src/test/lib/test_epilogue.sail b/src/test/lib/test_epilogue.sail new file mode 100644 index 00000000..434b8a95 --- /dev/null +++ b/src/test/lib/test_epilogue.sail @@ -0,0 +1,5 @@ +(* TranslateAddress compatible "main" function *) +function (bit[64]) run ((bit[64]) x) = { + test(); + return 0; +} diff --git a/src/test/lib/test_prelude.sail b/src/test/lib/test_prelude.sail new file mode 100644 index 00000000..3525af8e --- /dev/null +++ b/src/test/lib/test_prelude.sail @@ -0,0 +1,19 @@ +default Order inc + +scattered typedef ast = const union +val ast -> unit effect pure execute +scattered function unit execute + +union ast member (unit) DUMMY +function clause execute (DUMMY) = () + +end ast +end execute + +function unit test_assert (name, pred) = { + print (name); + if pred then + print (": pass\n") + else + print(": fail\n") +} diff --git a/src/test/lib/test_to_junit.sh b/src/test/lib/test_to_junit.sh new file mode 100755 index 00000000..71e908bd --- /dev/null +++ b/src/test/lib/test_to_junit.sh @@ -0,0 +1,62 @@ +#!/usr/bin/env bash +set -e + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + + +pass=0 +fail=0 + +XML="" + +XML_FILE=tests.xml + +function green { + (( pass += 1 )) + printf "$1: ${GREEN}$2${NC}\n" + XML+=" <testcase name=\"$1\"/>\n" +} + +function yellow { + (( fail += 1 )) + printf "$1: ${YELLOW}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function red { + (( fail += 1 )) + printf "$1: ${RED}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function finish_suite { + printf "$1: Passed ${pass} out of $(( pass + fail ))\n" + XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n" + printf "$XML" >> $XML_FILE + XML="" + pass=0 + fail=0 +} + +test_regex="^\"*([^\"]*)\"*: (pass|fail)$" +echo "<testsuites>" > $XML_FILE +for result_file in $@; do + while read line; do + if [[ $line =~ $test_regex ]] ; then + test_name=${BASH_REMATCH[1]} + test_status=${BASH_REMATCH[2]} + if [[ $test_status == pass ]] ; then + green $test_name $test_status + else + red $test_name $test_status + fi + else + echo $line + fi + done < "$result_file" + finish_suite $result_file +done +echo "</testsuites>" >> $XML_FILE diff --git a/src/test/lib/tests/test_add.sail b/src/test/lib/tests/test_add.sail new file mode 100644 index 00000000..ce0a19f0 --- /dev/null +++ b/src/test/lib/tests/test_add.sail @@ -0,0 +1,19 @@ +function unit test () = { + test_assert ("add", 1 + 1 == 2); + test_assert ("add_vec", ((bit[4])(0x1 + 0x1)) == 0x2); + test_assert ("add_vec_ov", ((bit[4])(0xf + 0x1)) == 0x0); + test_assert ("add_vec_vec_range", ((range<0,30>)(0x1 + 0x1)) == 2); + test_assert ("add_vec_vec_range_ov", ((range<0,15>)(0xf + 0x1)) == 0); (* XXX broken... *) + test_assert ("add_vec_range", ((bit[4])(0x1 + 1)) == 0x2); + test_assert ("add_vec_range_range", ((range<0,15>)(0xe + 1)) == 15); + test_assert ("add_overflow_vec", (((bit[4], bit, bit))(0x1 + 0x1)) == (0x2, false, false)); + test_assert ("add_overflow_vec_ov", (((bit[4], bit, bit))(0xf + 0x1)) == (0x0, true, true)); (* XXX overflow flag makes no sense for unsigned... *) + test_assert ("add_overflow_vec_ovs", (((bit[4], bit, bit))(0x4 + 0x4)) == (0x8, false, false)); + test_assert ("add_vec_range_range", ((range<0,16>)(0xe + 1)) == 15); + test_assert ("add_range_vec", ((bit[4])(1 + 0xe)) == 0xf); + test_assert ("add_range_vec_range", ((range<0,3>)(1 + 0xe)) == 15); + test_assert ("add_vec_bit", ((bit[4])(0xe + bitone)) == 0xf); + (* not defined on either model... + test_assert ("add_bit_vec", ((bit[4])(bitone + 0x1)) == 0x2); *) +} + diff --git a/src/test/lib/tests/test_add_signed.sail b/src/test/lib/tests/test_add_signed.sail new file mode 100644 index 00000000..a723389e --- /dev/null +++ b/src/test/lib/tests/test_add_signed.sail @@ -0,0 +1,27 @@ +function unit test() = { + test_assert ("adds", 1 +_s 1 == 2); (* same as unsigned *) + test_assert ("adds_vec", ((bit[4])(0x1 +_s 0x1)) == 0x2); (* same as unsigned *) + test_assert ("adds_vec_ov", ((bit[4])(0xf +_s 0x1)) == 0x0); (* same as unsigned *) + + (* XXX would be good to restrict range type *) + test_assert ("adds_vec_vec_range_pp", ((int)(0x1 +_s 0x1)) == 2); + test_assert ("adds_vec_vec_range_np", ((int)(0xa +_s 0x1)) == (-5)); + test_assert ("adds_vec_vec_range_pn", ((int)(0x3 +_s 0xe)) == 1); + test_assert ("adds_vec_vec_range_nn", ((int)(0x8 +_s 0x8)) == (-16)); + + test_assert ("adds_vec_range", ((bit[4])(0xe +_s 1)) == 0xf); + test_assert ("adds_vec_range_range", ((int)(0xe +_s 1)) == (-1)); + (* returns (result, signed overflow, carry out)*) + test_assert ("adds_overflow_vec0", (((bit[4], bit, bit))(0x1 +_s 0x1)) == (0x2, false, false)); + test_assert ("adds_overflow_vec1", (((bit[4], bit, bit))(0xf +_s 0x1)) == (0x0, false, true)); + test_assert ("adds_overflow_vec2", (((bit[4], bit, bit))(0x7 +_s 0x1)) == (0x8, true, false)); + test_assert ("adds_overflow_vec3", (((bit[4], bit, bit))(0x8 +_s 0x8)) == (0x0, true, true)); + + test_assert ("adds_vec_range_range", ((int)(0xe +_s 1)) == (-1)); + test_assert ("adds_range_vec", ((bit[4])(1 +_s 0xe)) == 0xf); + test_assert ("adds_range_vec_range", ((int)(1 +_s 0xe)) == -1); + test_assert ("adds_vec_bit", ((bit[4])(0xe +_s bitone)) == 0xf); + (* not defined on either model... + test_assert ("adds_bit_vec", ((bit[4])(bitone +_s 0xe)) == 0xf);*) +} + diff --git a/src/test/lib/tests/test_and.sail b/src/test/lib/tests/test_and.sail new file mode 100644 index 00000000..7c9cd800 --- /dev/null +++ b/src/test/lib/tests/test_and.sail @@ -0,0 +1,7 @@ +function unit test () = { + test_assert ("bitwise_and", (0b0101 & 0b0011) == 0b0001); + test_assert ("bitwise_and_00", (bitzero & bitzero) == bitzero); + test_assert ("bitwise_and_01", (bitzero & bitone) == bitzero); + test_assert ("bitwise_and_10", (bitone & bitzero) == bitzero); + test_assert ("bitwise_and_11", (bitone & bitone) == bitone); +} diff --git a/src/test/lib/tests/test_div.sail b/src/test/lib/tests/test_div.sail new file mode 100644 index 00000000..1af58d20 --- /dev/null +++ b/src/test/lib/tests/test_div.sail @@ -0,0 +1,39 @@ +function unit test () = { + test_assert ("divpospos_exact", (21 div 7) == 3); + test_assert ("divposneg_exact", (21 div -7) == -3); + test_assert ("divnegpos_exact", (-21 div 7) == -3); + test_assert ("divnegneg_exact", (-21 div -7) == 3); + + test_assert ("divpospos_approx", (21 div 8) == 2); + test_assert ("divposneg_approx", (21 div -8) == -2); + test_assert ("divnegpos_approx", (-21 div 8) == -2); + test_assert ("divnegneg_approx", (-21 div -8) == 2); + + (* quot and div are synonyms but let's check... *) + test_assert ("quotpospos_exact", (21 quot 7) == 3); + test_assert ("quotposneg_exact", (21 quot -7) == -3); + test_assert ("quotnegpos_exact", (-21 quot 7) == -3); + test_assert ("quotnegneg_exact", (-21 quot -7) == 3); + + test_assert ("quotpospos_approx", (21 quot 8) == 2); + test_assert ("quotposneg_approx", (21 quot -8) == -2); + test_assert ("quotnegpos_approx", (-21 quot 8) == -2); + test_assert ("quotnegneg_approx", (-21 quot -8) == 2); + + (* XXX currently crashes on shallow embedding + test_assert ("div_overflow", ((bit[8])(0x80 quot_s 0xff)) == 0x80); + *) + test_assert ("quot_vec_pospos_exact", ((bit[8])(0x15 quot 0x07)) == 0x03); + test_assert ("quot_vec_posneg_exact", ((bit[8])(0x15 quot 0xf9)) == 0x00); + test_assert ("quot_vec_negpos_exact", ((bit[8])(0xeb quot 0x07)) == 0x21); + test_assert ("quot_vec_negneg_exact", ((bit[8])(0xeb quot 0xf9)) == 0x00); + + test_assert ("quot_vec_pospos_approx", ((bit[8])(0x15 quot 0x08)) == 0x02); + test_assert ("quot_vec_posneg_approx", ((bit[8])(0x15 quot 0xf8)) == 0x00); + test_assert ("quot_vec_negpos_approx", ((bit[8])(0xeb quot 0x08)) == 0x1d); + test_assert ("quot_vec_negneg_approx", ((bit[8])(0xeb quot 0xf8)) == 0x00); + + test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x15 quot 0x08)) == (0x02, false, false)); + test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x80 quot 0xff)) == (0x00, false, false)); +} + diff --git a/src/test/lib/tests/test_duplicate.sail b/src/test/lib/tests/test_duplicate.sail new file mode 100644 index 00000000..99ffbe6c --- /dev/null +++ b/src/test/lib/tests/test_duplicate.sail @@ -0,0 +1,14 @@ +function unit test () = { + (* XXX crashes on shallow embedding + should type have a constraint n>0? + test_assert ("duplicate_empty", (bitzero ^^ 0) == []); *) + test_assert ("duplicate0", (bitzero ^^ 8) == 0x00); + test_assert ("duplicate1", (bitone ^^ 8) == 0xff); + + (* XXX crashes on shallow embedding + test_assert ("duplicate_bits0", (0x21 ^^ 0) == []);*) + test_assert ("duplicate_bits1", (0xce ^^ 1) == 0xce); + test_assert ("duplicate_bits9", (0xce ^^ 9) == 0xcecececececececece); + test_assert ("duplicate_covfefe", (0xc0 : (0xfe ^^ 2)) == 0xc0fefe); +} + diff --git a/src/test/lib/tests/test_eq.sail b/src/test/lib/tests/test_eq.sail new file mode 100644 index 00000000..3000b7c5 --- /dev/null +++ b/src/test/lib/tests/test_eq.sail @@ -0,0 +1,18 @@ +function unit test () = { + test_assert("eq_bit00", false == bitzero); + test_assert("eq_bit01", not(false == bitone)); + test_assert("eq_bit10", not(true == bitzero)); + test_assert("eq_bit11", true == bitone); + + test_assert("eq_vec0", not (0x1 == 0x2)); + test_assert("eq_vec1", 0x2 == 0x2); + test_assert("eq_vec_range0", not (0xf == 16)); + test_assert("eq_vec_range1", 0xf == 15); + test_assert("eq_range_vec0", not (16 == 0xf)); + test_assert("eq_range_vec1", 15 == 0xf); + test_assert("eq_range0", not(12 == 13)); + test_assert("eq_range1", 13 == 13); + test_assert("eq_tup0", not ((true, false) == (bitzero, bitzero))); + test_assert("eq_tup1", (true, false) == (bitone, bitzero)); +} + diff --git a/src/test/lib/tests/test_ext.sail b/src/test/lib/tests/test_ext.sail new file mode 100644 index 00000000..1cbc2855 --- /dev/null +++ b/src/test/lib/tests/test_ext.sail @@ -0,0 +1,15 @@ +function unit test () = { + test_assert ("extz0", EXTZ(0b00) == 0x00); + test_assert ("extz1", EXTZ(0b10) == 0x02); + test_assert ("extz2", EXTZ(0b10) == 0b10); + test_assert ("extz3", EXTZ(0b10) == 0b0); + + test_assert ("exts0", EXTS(0b00) == 0x00); + test_assert ("exts1", EXTS(0b10) == 0xfe); + test_assert ("exts2", EXTS(0b10) == 0b10); + test_assert ("exts3", EXTS(0b10) == 0b0); + + test_assert ("most_significant0", most_significant(0b011) == bitzero); + test_assert ("most_significant1", most_significant(0b100) == bitone); + } + diff --git a/src/test/lib/tests/test_gt.sail b/src/test/lib/tests/test_gt.sail new file mode 100644 index 00000000..8576a8cd --- /dev/null +++ b/src/test/lib/tests/test_gt.sail @@ -0,0 +1,36 @@ +function unit test() = { + test_assert("gt0", ( 1 > -1)); + test_assert("gt1", not(-1 > -1)); + test_assert("gt2", not(-1 > 1)); + + (* XXX default is signed -- document this! *) + test_assert("gt_vec0", (0x1 > 0xf)); + test_assert("gt_vec1", not(0xf > 0xf)); + test_assert("gt_vec2", not(0xf > 0x1)); + + test_assert("gt_vec_range0", (0x1 > -1)); + test_assert("gt_vec_range1", not(0xf > -1)); + test_assert("gt_vec_range2", not(0xf > 1)); + (* NB missing range_vec version *) + + (* XXX missing implementations + test_assert("gt_unsigned0", ( 1 >_u -1)); + test_assert("gt_unsigned1", not(-1 >_u -1)); + test_assert("gt_unsigned2", not(-1 >_u 1)); *) + + test_assert("gt_vec_unsigned0", not(0x1 >_u 0xf)); + test_assert("gt_vec_unsigned1", not(0xf >_u 0xf)); + test_assert("gt_vec_unsigned2", (0xf >_u 0x1)); + + (* NB there is no gt_vec_range unsigned or signed *) + + (* XXX missing implementations + test_assert("gt_signed0", ( 1 >_s -1)); + test_assert("gt_signed1", not(-1 >_s -1)); + test_assert("gt_signed2", not(-1 >_s 1)); *) + + test_assert("gt_vec_signed0", (0x1 >_s 0xf)); + test_assert("gt_vec_signed1", not(0xf >_s 0xf)); + test_assert("gt_vec_signed2", not(0xf >_s 0x1)); +} + diff --git a/src/test/lib/tests/test_gteq.sail b/src/test/lib/tests/test_gteq.sail new file mode 100644 index 00000000..79d4d378 --- /dev/null +++ b/src/test/lib/tests/test_gteq.sail @@ -0,0 +1,41 @@ +function unit test() = { + test_assert("gteq0", ( 1 >= -1)); + test_assert("gteq1", (-1 >= -1)); + test_assert("gteq2", not(-1 >= 1)); + + (* XXX default is signed -- document this! *) + test_assert("gteq_vec0", (0x1 >= 0xf)); + test_assert("gteq_vec1", (0xf >= 0xf)); + test_assert("gteq_vec2", not(0xf >= 0x1)); + + (* XXX odd type error here -- sail seems to prefer gteq_vec... + test_assert("gteq_vec_range0", (0x1 >= -1)); + test_assert("gteq_vec_range1", (0xf >= -1)); + test_assert("gteq_vec_range2", not(0xf >= 1)); + + test_assert("gteq_range_vec0", ( 1 >= 0xf)); + test_assert("gteq_range_vec1", (-1 >= 0xf)); + test_assert("gteq_range_vec2", not(-1 >= 0x1));*) + + (* XXX missing implementations + test_assert("gteq_unsigned0", ( 1 >=_u -1)); + test_assert("gteq_unsigned1", not(-1 >=_u -1)); + test_assert("gteq_unsigned2", not(-1 >=_u 1)); *) + + (* XXX missing + test_assert("gteq_unsigned_vec0", not(0x1 >=_u 0xf)); + test_assert("gteq_unsigned_vec1", not(0xf >=_u 0xf)); + test_assert("gteq_unsigned_vec2", (0xf >=_u 0x1)); *) + + (* NB there is no gteq_vec_range unsigned or signed *) + + (* XXX missing implementations + test_assert("gteq_signed0", ( 1 >=_s -1)); + test_assert("gteq_signed1", not(-1 >=_s -1)); + test_assert("gteq_signed2", not(-1 >=_s 1)); *) + + test_assert("gteq_vec_signed0", (0x1 >=_s 0xf)); + test_assert("gteq_vec_signed1", (0xf >=_s 0xf)); + test_assert("gteq_vec_signed2", not(0xf >=_s 0x1)); +} + diff --git a/src/test/lib/tests/test_leftshift.sail b/src/test/lib/tests/test_leftshift.sail new file mode 100644 index 00000000..15c308bc --- /dev/null +++ b/src/test/lib/tests/test_leftshift.sail @@ -0,0 +1,11 @@ +function unit test () = { + test_assert ("leftshift_small0", (0x99 << 0) == 0x99); + test_assert ("leftshift_small3", (0x99 << 3) == 0xc8); + test_assert ("leftshift_small7", (0x99 << 7) == 0x80); + test_assert ("leftshift_small8", (0x99 << 8) == 0x00); + test_assert ("leftshift_big0", (0x99999999999999999 << 0) == 0x99999999999999999); + test_assert ("leftshift_big3", (0x99999999999999999 << 3) == 0xcccccccccccccccc8); + test_assert ("leftshift_big7", (0x99999999999999999 << 7) == 0xccccccccccccccc80); + test_assert ("leftshift_big68", (0x99999999999999999 << 68) == 0x00000000000000000); +} + diff --git a/src/test/lib/tests/test_lt.sail b/src/test/lib/tests/test_lt.sail new file mode 100644 index 00000000..6ae7a3c3 --- /dev/null +++ b/src/test/lib/tests/test_lt.sail @@ -0,0 +1,36 @@ +function unit test() = { + test_assert("lt0", not( 1 < -1)); + test_assert("lt1", not(-1 < -1)); + test_assert("lt2", (-1 < 1)); + + (* XXX default is signed -- document this! *) + test_assert("lt_vec0", not(0x1 < 0xf)); + test_assert("lt_vec1", not(0xf < 0xf)); + test_assert("lt_vec2", (0xf < 0x1)); + + test_assert("lt_vec_range0", not(0x1 < -1)); + test_assert("lt_vec_range1", not(0xf < -1)); + test_assert("lt_vec_range2", (0xf < 1)); + (* NB missing range_vec version *) + + (* XXX missing implementations + test_assert("lt_unsigned0", not( 1 <_u -1)); + test_assert("lt_unsigned1", not(-1 <_u -1)); + test_assert("lt_unsigned2", (-1 <_u 1)); *) + + test_assert("lt_vec_unsigned0", (0x1 <_u 0xf)); + test_assert("lt_vec_unsigned1", not(0xf <_u 0xf)); + test_assert("lt_vec_unsigned2", not(0xf <_u 0x1)); + + (* NB there is no lt_vec_range unsigned or signed *) + + (* XXX missing implementations + test_assert("lt_signed0", not( 1 <_s -1)); + test_assert("lt_signed1", not(-1 <_s -1)); + test_assert("lt_signed2", (-1 <_s 1)); *) + + test_assert("lt_vec_signed0", not(0x1 <_s 0xf)); + test_assert("lt_vec_signed1", not(0xf <_s 0xf)); + test_assert("lt_vec_signed2", (0xf <_s 0x1)); +} + diff --git a/src/test/lib/tests/test_lteq.sail b/src/test/lib/tests/test_lteq.sail new file mode 100644 index 00000000..612023e9 --- /dev/null +++ b/src/test/lib/tests/test_lteq.sail @@ -0,0 +1,40 @@ +function unit test() = { + test_assert("lteq0", not( 1 <= -1)); + test_assert("lteq1", (-1 <= -1)); + test_assert("lteq2", (-1 <= 1)); + + (* XXX default is signed -- document this! *) + test_assert("lteq_vec0", not(0x1 <= 0xf)); + test_assert("lteq_vec1", (0xf <= 0xf)); + test_assert("lteq_vec2", (0xf <= 0x1)); + + test_assert("lteq_vec_range0", not(0x1 <= -1)); + test_assert("lteq_vec_range1", (0xf <= -1)); + test_assert("lteq_vec_range2", (0xf <= 1)); + + test_assert("lteq_range_vec0", not( 1 <= 0xf)); + test_assert("lteq_range_vec1", (-1 <= 0xf)); + test_assert("lteq_range_vec2", (-1 <= 0x1)); + + (* XXX missing implementations + test_assert("lteq_unsigned0", not( 1 <=_u -1)); + test_assert("lteq_unsigned1", (-1 <=_u -1)); + test_assert("lteq_unsigned2", (-1 <=_u 1)); *) + + (* XXX missing type / parser + test_assert("lteq_unsigned_vec0", (0x1 <=_u 0xf)); + test_assert("lteq_unsigned_vec1", (0xf <=_u 0xf)); + test_assert("lteq_unsigned_vec2", not(0xf <=_u 0x1));*) + + (* NB there is no lteq_vec_range unsigned or signed *) + + (* XXX missing implementations + test_assert("lteq_signed0", not( 1 <=_s -1)); + test_assert("lteq_signed1", (-1 <=_s -1)); + test_assert("lteq_signed2", (-1 <=_s 1)); *) + + test_assert("lteq_vec_signed0", not(0x1 <=_s 0xf)); + test_assert("lteq_vec_signed1", (0xf <=_s 0xf)); + test_assert("lteq_vec_signed2", (0xf <=_s 0x1)); +} + diff --git a/src/test/lib/tests/test_minus.sail b/src/test/lib/tests/test_minus.sail new file mode 100644 index 00000000..455f3954 --- /dev/null +++ b/src/test/lib/tests/test_minus.sail @@ -0,0 +1,25 @@ +function unit test() = { + test_assert("minus", 1 - 1 == 0); + test_assert("minus_vec", ((bit[4])(0x2 - 0x1)) == 0x1); + test_assert("minus_vec_ov", ((bit[4])(0x1 - 0xf)) == 0x2); + (* XXX minus_vec_vec_range not implemented + test_assert("minus_vec_vec_range_pp", ((int)(0x1 - 0x1)) == 0); + test_assert("minus_vec_vec_range_np", ((int)(0xa - 0x1)) == 9); + test_assert("minus_vec_vec_range_pn", ((int)(0x3 - 0xe)) == 5); + test_assert("minus_vec_vec_range_nn", ((int)(0x8 - 0x8)) == 0);*) + test_assert("minus_vec_range", ((bit[4])(0xe - 1)) == 0xd); + test_assert("minus_vec_range_range", ((int)(0xe - 1)) == 13); + test_assert("minus_range_vec", ((bit[4])(1 - 0xe)) == 0x3); + test_assert("minus_range_vec_range", ((int)(1 - 0xe)) == -13); + (* returns (result, signed overflow, borrow in)*) + test_assert ("minus_overflow_vec0", (((bit[4], bit, bit))(0x1 - 0x1)) == (0x0, false, false)); + test_assert ("minus_overflow_vec1", (((bit[4], bit, bit))(0x0 - 0x1)) == (0xf, true, true)); + test_assert ("minus_overflow_vec2", (((bit[4], bit, bit))(0x8 - 0x1)) == (0x7, false, false)); + test_assert ("minus_overflow_vec3", (((bit[4], bit, bit))(0x0 - 0x8)) == (0x8, true, true)); + + test_assert ("minus_overflow_vec_bit0", (((bit[4], bit, bit))(0x1 - bitone)) == (0x0, false, false)); + test_assert ("minus_overflow_vec_bit1", (((bit[4], bit, bit))(0x0 - bitone)) == (0xf, true, true)); + test_assert ("minus_overflow_vec_bit2", (((bit[4], bit, bit))(0x8 - bitone)) == (0x7, false, false)); + test_assert ("minus_overflow_vec_bit3", (((bit[4], bit, bit))(0x8 - bitzero)) == (0x8, false, false)); (* XXX shallow embedding returns true, false... *) +} + diff --git a/src/test/lib/tests/test_minus_signed.sail b/src/test/lib/tests/test_minus_signed.sail new file mode 100644 index 00000000..7268f340 --- /dev/null +++ b/src/test/lib/tests/test_minus_signed.sail @@ -0,0 +1,27 @@ +function unit test() = { + test_assert("minus_signed", 1 -_s 1 == 0); + (* XXX minus_vec_signed not implemented + test_assert("minus_vec_signed", ((bit[4])(0x2 -_s 0x1)) == 0x1); + test_assert("minus_vec_ov_signed", ((bit[4])(0x1 -_s 0xf)) == 0x2); *) + (* XXX minus_vec_vec_range_signed not implemented + test_assert("minus_vec_vec_range_signed_pp", ((int)(0x1 -_s 0x1)) == 0); + test_assert("minus_vec_vec_range_signed_np", ((int)(0xa -_s 0x1)) == 9); + test_assert("minus_vec_vec_range_signed_pn", ((int)(0x3 -_s 0xe)) == 5); + test_assert("minus_vec_vec_range_signed_nn", ((int)(0x8 -_s 0x8)) == 0);*) + (* XXX not implemented + test_assert("minus_vec_range_signed", ((bit[4])(0xe -_s 1)) == 0xd); + test_assert("minus_vec_range_range_signed", ((int)(0xe -_s 1)) == -3); + test_assert("minus_range_vec_signed", ((bit[4])(1 -_s 0xe)) == 0x3); + test_assert("minus_range_vec_range_signed", ((int)(1 -_s 0xe)) == 3);*) + (* returns (result, signed overflow, borrow in)*) + test_assert ("minus_overflow_vec_signed0", (((bit[4], bit, bit))(0x1 -_s 0x1)) == (0x0, false, false)); + test_assert ("minus_overflow_vec_signed1", (((bit[4], bit, bit))(0x0 -_s 0x1)) == (0xf, true, true)); + test_assert ("minus_overflow_vec_signed2", (((bit[4], bit, bit))(0x8 -_s 0x1)) == (0x7, false, false)); + test_assert ("minus_overflow_vec_signed3", (((bit[4], bit, bit))(0x0 -_s 0x8)) == (0x8, true, true)); + + test_assert ("minus_overflow_vec_bit_signed0", (((bit[4], bit, bit))(0x1 -_s bitone)) == (0x0, false, false)); + test_assert ("minus_overflow_vec_bit_signed1", (((bit[4], bit, bit))(0x0 -_s bitone)) == (0xf, true, true)); + test_assert ("minus_overflow_vec_bit_signed2", (((bit[4], bit, bit))(0x8 -_s bitone)) == (0x7, false, false)); + test_assert ("minus_overflow_vec_bit_signed3", (((bit[4], bit, bit))(0x8 -_s bitzero)) == (0x8, false, false)); +} + diff --git a/src/test/lib/tests/test_misc.sail b/src/test/lib/tests/test_misc.sail new file mode 100644 index 00000000..5b4b6fd4 --- /dev/null +++ b/src/test/lib/tests/test_misc.sail @@ -0,0 +1,19 @@ +function unit test () = { + test_assert ("power0", (0 ** 3) == 0); + test_assert ("power1", (3 ** 0) == 1); + test_assert ("power2", (11 ** 17) == 505447028499293771); + (* XXX should be type error but isn't + test_assert ("power-1", (1 ** -1) == 0); *) + + test_assert ("abs_neg", (abs (-42)) == 42); + test_assert ("abs_zero", (abs (0)) == 0); + test_assert ("abs_pos", (abs (143)) == 143); + + test_assert ("max", max(-1, 1) == 1); + test_assert ("min", min(-1, 1) == -1); + + test_assert ("length0", length([]) == 0); + test_assert ("length1", length([bitzero]) == 1); + test_assert ("length2", length(0x1234) == 16); +} + diff --git a/src/test/lib/tests/test_mod.sail b/src/test/lib/tests/test_mod.sail new file mode 100644 index 00000000..7f078bae --- /dev/null +++ b/src/test/lib/tests/test_mod.sail @@ -0,0 +1,23 @@ +function unit test () = { + test_assert ("modpospos_exact", (21 mod 7) == 0); + test_assert ("modposneg_exact", (21 mod -7) == 0); + test_assert ("modnegpos_exact", (-21 mod 7) == 0); + test_assert ("modnegneg_exact", (-21 mod -7) == 0); + + test_assert ("modpospos_approx", (21 mod 8) == 5); + test_assert ("modposneg_approx", (21 mod -8) == 5); + test_assert ("modnegpos_approx", (-21 mod 8) == -5); + test_assert ("modnegneg_approx", (-21 mod -8) == -5); + + (* XXX how to test this? Type checker should catch? + test_assert ("mod_zero", (21 mod 0) == undefined); *) + + test_assert("mod_vec_range_pos", (0x7 mod 5) == 2); + test_assert("mod_vec_range_neg", (0xf mod 5) == 0); + + test_assert("mod_vec_pos", (0x7 mod 0x5) == 0x2); + test_assert("mod_vec_neg", (0xf mod 0x5) == 0x0); + test_assert("mod_vec_pos_neg", (0x7 mod 0x8) == 0x7); + test_assert("mod_vec_neg_neg", (0xf mod 0x8) == 0x7); +} + diff --git a/src/test/lib/tests/test_mod_signed.sail b/src/test/lib/tests/test_mod_signed.sail new file mode 100644 index 00000000..61acec17 --- /dev/null +++ b/src/test/lib/tests/test_mod_signed.sail @@ -0,0 +1,26 @@ +function unit test () = { + (); + (* XXX mod_signed does exist on ocaml shallow embedding... + test_assert ("mod_signed_pospos_exact", (21 mod_s 7) == 0); + test_assert ("mod_signed_posneg_exact", (21 mod_s -7) == 0); + test_assert ("mod_signed_negpos_exact", (-21 mod_s 7) == 0); + test_assert ("mod_signed_negneg_exact", (-21 mod_s -7) == 0); + + test_assert ("mod_signed_pospos_approx", (21 mod_s 8) == 5); + test_assert ("mod_signed_posneg_approx", (21 mod_s -8) == 5); + test_assert ("mod_signed_negpos_approx", (-21 mod_s 8) == -5); + test_assert ("mod_signed_negneg_approx", (-21 mod_s -8) == -5); + + (* XXX how to test this? Type checker should catch? + test_assert ("mod_signed_zero", (21 mod_s 0) == undefined); *) + + test_assert("mod_vec_range_signed_pos", (0x7 mod_s 5) == 2); + test_assert("mod_vec_range_signed_neg", (0xf mod_s 5) == -1); + + test_assert("mod_vec_signed_pos", (0x7 mod_s 0x5) == 0x2); + test_assert("mod_vec_signed_neg", (0xf mod_s 0x5) == 0xf); + test_assert("mod_vec_signed_pos_neg", (0x7 mod_s 0x8) == 0x7); + test_assert("mod_vec_signed_neg_neg", (0xf mod_s 0x8) == 0x7); + *) +} + diff --git a/src/test/lib/tests/test_multiply.sail b/src/test/lib/tests/test_multiply.sail new file mode 100644 index 00000000..03adfa27 --- /dev/null +++ b/src/test/lib/tests/test_multiply.sail @@ -0,0 +1,21 @@ +function unit test () = { + test_assert ("multiply", 6 * 9 == 54); + test_assert ("multiply_vec", ((bit[8])(0x6 * 0xb)) == 0x42); + test_assert ("mult_range_vec", ((bit[8])(6 * 0xb)) == 0x42); + test_assert ("mult_vec_range", ((bit[8])(0x6 * 11)) == 0x42); + (* XXX mult_oveflow_vec missing *) + + (* XXX not implmented + test_assert ("multiply_signed", 6 *_s 9 == 54); *) + test_assert ("multiply_vec_signed", ((bit[8])(0x6 *_s 0xb)) == 0xe2); + test_assert ("mult_range_vec_signed", ((bit[8])(6 *_s 0xb)) == 0xe2); + test_assert ("mult_vec_range_signed", ((bit[8])(0x6 *_s 11)) == 0xe2); + + (* XXX don't think it's possible to set carryout out bit *) + test_assert ("mult_overflow_vec_signed0", (((bit[8], bit, bit)) (0xf *_s 0x2)) == (0xfe, false, false)); + test_assert ("mult_overflow_vec_signed1", (((bit[8], bit, bit)) (0xf *_s 0xf)) == (0x01, false, false)); + test_assert ("mult_overflow_vec_signed2", (((bit[8], bit, bit)) (0x8 *_s 0x8)) == (0x40, true, false)); + test_assert ("mult_overflow_vec_signed3", (((bit[8], bit, bit)) (0x7 *_s 0x7)) == (0x31, true, false)); + test_assert ("mult_overflow_vec_signed4", (((bit[8], bit, bit)) (0x8 *_s 0x7)) == (0xc8, true, false)); +} + diff --git a/src/test/lib/tests/test_neq.sail b/src/test/lib/tests/test_neq.sail new file mode 100644 index 00000000..e3ad50cf --- /dev/null +++ b/src/test/lib/tests/test_neq.sail @@ -0,0 +1,20 @@ +function unit test () = { + test_assert("neq_bit00", not(false != bitzero)); + test_assert("neq_bit01", false != bitone); + test_assert("neq_bit10", true != bitzero); + test_assert("neq_bit11", not(true != bitone)); + + test_assert("neq_vec0", 0x1 != 0x2); + test_assert("neq_vec1", not(0x2 != 0x2)); + test_assert("neq_vec_range0", 0xf != 16); + test_assert("neq_vec_range0", 0x7 != 8); + test_assert("neq_vec_range1", not(0xf != 15)); + (* XXX not implemented for ocaml + test_assert("neq_range_vec0", 16 != 0xf); + test_assert("neq_range_vec1", not(15 != 0xf)); *) + test_assert("neq_range0", 12 != 13); + test_assert("neq_range1", not(13 != 13)); + test_assert("neq_tup0", (true, false) != (bitzero, bitzero)); + test_assert("neq_tup1", not((true, false) != (bitone, bitzero))); +} + diff --git a/src/test/lib/tests/test_not.sail b/src/test/lib/tests/test_not.sail new file mode 100644 index 00000000..8ae2514f --- /dev/null +++ b/src/test/lib/tests/test_not.sail @@ -0,0 +1,8 @@ +function unit test () = { + test_assert ("not_bit0", (not (bitzero)) == bitone); + test_assert ("not_bit1", (not (bitone)) == bitzero); + + test_assert ("bitwise_not", (~ (0b01) == 0b10)); + test_assert ("bitwise_not_bit0", ((~ (bitzero)) == bitone)); + test_assert ("bitwise_not_bit1", ((~ (bitone)) == bitzero)); +} diff --git a/src/test/lib/tests/test_oddments.sail b/src/test/lib/tests/test_oddments.sail new file mode 100644 index 00000000..4c8fd086 --- /dev/null +++ b/src/test/lib/tests/test_oddments.sail @@ -0,0 +1,14 @@ +function unit test () = { + (* XXX this is weird, wrong type? + test_assert("is_one0", not(is_one(bitzero))); + test_assert("is_one1", is_one(bitone)); *) + + test_assert("signed-1", signed(0xf) == -1); + test_assert("signed0", signed(0x0) == 0); + test_assert("signed1", signed(0x1) == 1); + + test_assert("unsigned-1", unsigned(0xf) == 15); + test_assert("unsigned0", unsigned(0x0) == 0); + test_assert("unsigned1", unsigned(0x1) == 1); +} + diff --git a/src/test/lib/tests/test_or.sail b/src/test/lib/tests/test_or.sail new file mode 100644 index 00000000..c48caedc --- /dev/null +++ b/src/test/lib/tests/test_or.sail @@ -0,0 +1,7 @@ +function unit test () = { + test_assert ("bitwise_or", (0b0101 | 0b0011) == 0b0111); + test_assert ("bitwise_or_00", (bitzero | bitzero) == bitzero); + test_assert ("bitwise_or_01", (bitzero | bitone) == bitone); + test_assert ("bitwise_or_10", (bitone | bitzero) == bitone); + test_assert ("bitwise_or_11", (bitone | bitone) == bitone); +} diff --git a/src/test/lib/tests/test_quot_signed.sail b/src/test/lib/tests/test_quot_signed.sail new file mode 100644 index 00000000..39259204 --- /dev/null +++ b/src/test/lib/tests/test_quot_signed.sail @@ -0,0 +1,18 @@ +function unit test () = { + test_assert ("quot_vec_signed_pospos_exact", ((bit[8])(0x15 quot_s 0x07)) == 0x03); + test_assert ("quot_vec_signed_posneg_exact", ((bit[8])(0x15 quot_s 0xf9)) == 0xfd); + test_assert ("quot_vec_signed_negpos_exact", ((bit[8])(0xeb quot_s 0x07)) == 0xfd); + test_assert ("quot_vec_signed_negneg_exact", ((bit[8])(0xeb quot_s 0xf9)) == 0x03); + + test_assert ("quot_vec_signed_pospos_approx", ((bit[8])(0x15 quot_s 0x08)) == 0x02); + test_assert ("quot_vec_signed_posneg_approx", ((bit[8])(0x15 quot_s 0xf8)) == 0xfe); + test_assert ("quot_vec_signed_negpos_approx", ((bit[8])(0xeb quot_s 0x08)) == 0xfe); + test_assert ("quot_vec_signed_negneg_approx", ((bit[8])(0xeb quot_s 0xf8)) == 0x02); + + test_assert ("quot_signed_overflow_vec", (((bit[8], bit, bit))(0x15 quot_s 0x08)) == (0x02, false, false)); + (* XXX crashes shallow embedding due to undefined result + let (result, overflow, carry) = ((bit[8], bit, bit))(0x80 quot_s 0xff) in { + test_assert ("quot_signed_overflow_vec_ov", overflow); + test_assert ("quot_signed_overflow_vec_ca", carry); + };*) +} diff --git a/src/test/lib/tests/test_rightshift.sail b/src/test/lib/tests/test_rightshift.sail new file mode 100644 index 00000000..7879a33e --- /dev/null +++ b/src/test/lib/tests/test_rightshift.sail @@ -0,0 +1,10 @@ +function unit test () = { + test_assert ("rightshift_small0", (0x99 >> 0) == 0x99); + test_assert ("rightshift_small3", (0x99 >> 3) == 0x13); + test_assert ("rightshift_small7", (0x99 >> 7) == 0x01); + test_assert ("rightshift_small8", (0x99 >> 8) == 0x00); (* XXX fails on interp *) + test_assert ("rightshift_big0", (0x99999999999999999 >> 0) == 0x99999999999999999); + test_assert ("rightshift_big3", (0x99999999999999999 >> 3) == 0x13333333333333333); + test_assert ("rightshift_big7", (0x99999999999999999 >> 7) == 0x01333333333333333); + test_assert ("rightshift_big68", (0x99999999999999999 >> 68) == 0x00000000000000000); (* XXX fails on interp *) +} diff --git a/src/test/lib/tests/test_rotate.sail b/src/test/lib/tests/test_rotate.sail new file mode 100644 index 00000000..f0f8e45c --- /dev/null +++ b/src/test/lib/tests/test_rotate.sail @@ -0,0 +1,7 @@ +function unit test () = { + test_assert ("rotate0", (0x99 <<< 0) == 0x99); (* XXX fails on interp *) + test_assert ("rotate3", (0x99 <<< 3) == 0xcc); + test_assert ("rotate7", (0x99 <<< 7) == 0xcc); + test_assert ("rotate8", (0x99 <<< 8) == 0x99); +} + diff --git a/src/test/lib/tests/test_xor.sail b/src/test/lib/tests/test_xor.sail new file mode 100644 index 00000000..125b2f10 --- /dev/null +++ b/src/test/lib/tests/test_xor.sail @@ -0,0 +1,7 @@ +function unit test () = { + test_assert ("bitwise_xor", (0b0101 ^ 0b0011) == 0b0110); + test_assert ("bitwise_xor_00", (bitzero ^ bitzero) == bitzero); + test_assert ("bitwise_xor_01", (bitzero ^ bitone) == bitone); + test_assert ("bitwise_xor_10", (bitone ^ bitzero) == bitone); + test_assert ("bitwise_xor_11", (bitone ^ bitone) == bitzero); +} |