Finish implementing constant_value_to_typed_value

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 _ ->