diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 76 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 10 |
2 files changed, 61 insertions, 25 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index ca9fa48a..ec67edb8 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -18,9 +18,6 @@ let rec replace bs ((n : integer),b') = match bs with end - - - (*** Bits *) type bitU = O | I | Undef @@ -229,7 +226,7 @@ let bitwise_and = bitwise_binop (&&) let bitwise_or = bitwise_binop (||) let bitwise_xor = bitwise_binop xor -let unsigned (Vector bs _ _ as v) : integer = +let unsigned (Vector bs _ _) : integer = let (sum,_) = List.foldr (fun b (acc,exp) -> @@ -250,6 +247,21 @@ let signed v : integer = | Undef -> failwith "signed applied to vector with undefined bits" end +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 + +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 signed_big = signed let to_num sign = if sign then signed else unsigned @@ -337,8 +349,8 @@ let add = integerAdd let add_signed = integerAdd let minus = integerMinus let multiply = integerMult -let modulo = integerMod -let quot = integerDiv +let modulo = hardware_mod +let quot = hardware_quot let power = integerPow let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = @@ -482,7 +494,7 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz then if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size then O else I - else I in + else O in (correct_size_num,overflow,most_significant one_larger) (* add_overflow_vec_bit_signed @@ -495,7 +507,7 @@ let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 type shift = LL_shift | RR_shift | LLL_shift -let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) = +let shift_op_vec op (Vector bs start is_inc,(n : integer)) = let n = natFromInteger n in match op with | LL_shift (*"<<"*) -> @@ -530,9 +542,9 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector then to_vec is_inc (act_size,n') else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc -let mod_VVV = arith_op_vec_no0 integerMod false 1 -let quot_VVV = arith_op_vec_no0 integerDiv false 1 -let quotS_VVV = arith_op_vec_no0 integerDiv true 1 +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 @@ -557,13 +569,13 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = let overflow = if representable then O else I in (correct_size_num,overflow,most_significant one_more) -let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1 -let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1 +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 integerMod false 1 +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 = @@ -582,7 +594,7 @@ 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 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 @@ -704,11 +716,35 @@ type register = | UndefinedRegister of integer (* length *) | RegisterPair of register * register -let name_of_reg (Register name _ _ _ _) = name -let size_of_reg (Register _ size _ _ _) = size -let start_of_reg (Register _ _ start _ _) = start -let is_inc_of_reg (Register _ _ _ is_inc _) = is_inc -let dir_of_reg (Register _ _ _ is_inc _) = dir is_inc +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) diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 7ce7f2fd..ee67c2c7 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -109,11 +109,11 @@ let bytes_lifted_homogenous_to_string = function | Bitslh_undef -> "uu" | Bitslh_unknown -> "??" -let simple_bit_lifteds_to_string bls (show_length_and_start:bool) (starto: int option) = +let simple_bit_lifteds_to_string ?(collapse=true) bls (show_length_and_start:bool) (starto: int option) = let s = String.concat "" (List.map bit_lifted_to_string bls) in let s = - collapse_leading s in + if collapse then collapse_leading s else s in let len = string_of_int (List.length bls) in if show_length_and_start then match starto with @@ -124,14 +124,14 @@ let simple_bit_lifteds_to_string bls (show_length_and_start:bool) (starto: int o (* if a multiple of 8 lifted bits and each chunk of 8 is homogenous, print as lifted hex, otherwise print as lifted bits *) -let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (starto: int option) (abbreviate_zero_to_nine: bool) = +let bit_lifteds_to_string ?(collapse=true) (bls: bit_lifted list) (show_length_and_start:bool) (starto: int option) (abbreviate_zero_to_nine: bool) = let l = List.length bls in if l mod 8 = 0 then (* if List.mem l [8;16;32;64;128] then *) let bytesl = List.map (fun (Byte_lifted bs) -> bs) (Sail_impl_base.byte_lifteds_of_bit_lifteds bls) in let byteslhos = List.map bits_lifted_homogenous_of_bit_lifteds bytesl in match maybe_all byteslhos with | None -> (* print as bitvector after all *) - simple_bit_lifteds_to_string bls show_length_and_start starto + simple_bit_lifteds_to_string ~collapse:collapse bls show_length_and_start starto | Some (byteslhs: bits_lifted_homogenous list) -> (* if abbreviate_zero_to_nine, all bytes are concrete, and the number is <=9, just print that *) (* (note that that doesn't print the length or start - it's appropriate only for memory values, where we typically have an explicit footprint also printed *) @@ -161,7 +161,7 @@ let memory_value_to_string endian mv = bit_lifteds_to_string bls true None true let logfile_register_value_to_string rv = - bit_lifteds_to_string rv.rv_bits false (Some rv.rv_start) false + bit_lifteds_to_string ~collapse:false rv.rv_bits false (Some rv.rv_start) false let logfile_memory_value_to_string endian mv = let bls = List.concat(List.map (fun (Byte_lifted bs) -> bs) (if endian = E_big_endian then mv else (List.rev mv))) in |