diff options
| -rw-r--r-- | src/CfimOfJson.ml | 7 | ||||
| -rw-r--r-- | src/Interpreter.ml | 80 |
2 files changed, 11 insertions, 76 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 0b9caebc..39aa88f6 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -191,7 +191,12 @@ let big_int_of_json (js : json) : (big_int, string) result = | `String is -> Ok (Z.of_string is) | _ -> Error "") -(** Deserialize a [scalar_value] from JSON and **check the ranges** *) +(** Deserialize a [scalar_value] from JSON and **check the ranges**. + + Note that in practice we also check that the values are in range + in the interpreter functions. Still, it doesn't cost much to be + a bit conservative. + *) let scalar_value_of_json (js : json) : (scalar_value, string) result = let res = combine_error_msgs js "scalar_value_of_json" diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d4463355..61c1ee0b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,5 +1,6 @@ open Types open Values +open Scalars open Expressions open CfimAst open Print.Values @@ -1126,79 +1127,6 @@ let rec bottom_in_value (v : typed_value) : bool = | SharedLoan (_, sv) -> bottom_in_value sv | MutLoan _ -> false) -(* TODO: move those to Scalar.ml *) - -let integer_type_of_scalar_value (sv : scalar_value) : integer_type = - match sv with - | Isize _ -> Types.Isize - | I8 _ -> Types.I8 - | I16 _ -> Types.I16 - | I32 _ -> Types.I32 - | I64 _ -> Types.I64 - | I128 _ -> Types.I128 - | Usize _ -> Types.Usize - | U8 _ -> Types.U8 - | U16 _ -> Types.U16 - | U32 _ -> Types.U32 - | U64 _ -> Types.U64 - | U128 _ -> Types.U128 - -(** The minimum values an integer type can have *) - -let i8_min = Z.of_string "-128" - -let i8_max = Z.of_string "127" - -let i16_min = Z.of_string "-32768" - -let i16_max = Z.of_string "32767" - -let i32_min = Z.of_string "-2147483648" - -let i32_max = Z.of_string "2147483647" - -let i64_min = Z.of_string "-9223372036854775808" - -let i64_max = Z.of_string "9223372036854775807" - -let i128_min = Z.of_string "-170141183460469231731687303715884105728" - -let i128_max = Z.of_string "170141183460469231731687303715884105727" - -let u8_min = Z.of_string "0" - -let u8_max = Z.of_string "255" - -let u16_min = Z.of_string "0" - -let u16_max = Z.of_string "65535" - -let u32_min = Z.of_string "0" - -let u32_max = Z.of_string "4294967295" - -let u64_min = Z.of_string "0" - -let u64_max = Z.of_string "18446744073709551615" - -let u128_min = Z.of_string "0" - -let u128_max = Z.of_string "340282366920938463463374607431768211455" - -(** Being a bit conservative about isize/usize: depending on the system, - the values are encoded as 32-bit values or 64-bit values - we may - want to take that into account in the future *) - -let isize_min = i32_min - -let isize_max = i32_max - -let usize_min = u32_min - -let usize_max = u32_max - -(*let integer_type_min_value (int_ty : integer_type) : big_int =*) - (** Convert a constant operand value to a typed value *) let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety) (cv : operand_constant_value) : typed_value = @@ -1242,8 +1170,10 @@ let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety) | Types.Char, ConstantValue (Char v) -> { value = Concrete (Char v); ty } | Types.Str, ConstantValue (String v) -> { value = Concrete (String v); ty } | Types.Integer int_ty, ConstantValue (Scalar v) -> - (* TODO *) - raise Unimplemented + (* Check the type and the ranges *) + assert (int_ty == scalar_value_get_integer_type v); + assert (check_scalar_value_in_range v); + { value = Concrete (Scalar v); ty } (* Remaining cases (invalid) - listing as much as we can on purpose (allows to catch errors at compilation if the definitions change) *) | _, Unit | _, ConstantAdt _ | _, ConstantValue _ -> |