diff options
author | Son HO | 2022-09-22 18:52:15 +0200 |
---|---|---|
committer | GitHub | 2022-09-22 18:52:15 +0200 |
commit | dd75894c85bbaa5dc6aa54d39980e160e5b7777f (patch) | |
tree | ece56b01bcadea24a3c373236f0254f47e32a98f /src/InterpreterExpressions.ml | |
parent | d8f92140abd7e65b6f1c5dd7e511c0c0aa69e73f (diff) | |
parent | 0d5fb87166cc4eb4ddc783d871ad459479fc9fdc (diff) |
Merge pull request #1 from AeneasVerif/constants-v2
Implement support for globals
Diffstat (limited to 'src/InterpreterExpressions.ml')
-rw-r--r-- | src/InterpreterExpressions.ml | 57 |
1 files changed, 15 insertions, 42 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 6bb2baf0..4a4f3353 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -1,11 +1,13 @@ module T = Types module V = Values +module LA = LlbcAst open Scalars module E = Expressions open Errors module C = Contexts module Subst = Substitute module L = Logging +module PV = Print.Values open TypesUtils open ValuesUtils module Inv = Invariants @@ -108,53 +110,25 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) ctx (** Convert an operand constant operand value to a typed value *) -let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) - (cv : E.operand_constant_value) : V.typed_value = +let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value + = (* Check the type while converting - we actually need some information - * contained in the type *) + * contained in the type *) log#ldebug (lazy - ("operand_constant_value_to_typed_value:" ^ "\n- ty: " - ^ ety_to_string ctx ty ^ "\n- cv: " - ^ operand_constant_value_to_string ctx cv)); + ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv)); match (ty, cv) with - (* Adt *) - | ( T.Adt (adt_id, region_params, type_params), - ConstantAdt (variant_id, field_values) ) -> - assert (region_params = []); - (* Compute the types of the fields *) - let field_tys = - match adt_id with - | T.AdtId def_id -> - let def = C.ctx_lookup_type_decl ctx def_id in - assert (def.region_params = []); - Subst.type_decl_get_instantiated_field_etypes def variant_id - type_params - | T.Tuple -> type_params - | T.Assumed _ -> failwith "Unreachable" - in - (* Compute the field values *) - let field_values = - List.map - (fun (ty, v) -> operand_constant_value_to_typed_value ctx ty v) - (List.combine field_tys field_values) - in - (* Put together *) - let value = V.Adt { variant_id; field_values } in - { value; ty } (* Scalar, boolean... *) - | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty } - | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty } - | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty } - | T.Integer int_ty, ConstantValue (V.Scalar v) -> + | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty } + | T.Char, Char v -> { V.value = V.Concrete (Char v); ty } + | T.Str, String v -> { V.value = V.Concrete (String v); ty } + | T.Integer int_ty, V.Scalar v -> (* Check the type and the ranges *) assert (int_ty = v.int_ty); assert (check_scalar_value_in_range v); { V.value = V.Concrete (V.Scalar v); ty } - (* Remaining cases (invalid) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, ConstantAdt _ | _, ConstantValue _ -> - failwith "Improperly typed constant value" + (* Remaining cases (invalid) *) + | _, _ -> failwith "Improperly typed constant value" (** Reorganize the environment in preparation for the evaluation of an operand. @@ -197,8 +171,9 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : let prepare : cm_fun = fun cf ctx -> match op with - | Expressions.Constant _ -> + | Expressions.Constant (ty, cv) -> (* No need to reorganize the context *) + constant_to_typed_value ty cv |> ignore; cf ctx | Expressions.Copy p -> (* Access the value *) @@ -226,9 +201,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | Expressions.Constant (ty, cv) -> - let v = operand_constant_value_to_typed_value ctx ty cv in - cf v ctx + | Expressions.Constant (ty, cv) -> cf (constant_to_typed_value ty cv) ctx | Expressions.Copy p -> (* Access the value *) let access = Read in |