diff options
| -rw-r--r-- | src/Identifiers.ml | 2 | ||||
| -rw-r--r-- | src/Interpreter.ml | 82 | ||||
| -rw-r--r-- | src/Substitute.ml | 28 |
3 files changed, 83 insertions, 29 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 68a176bb..04f6c1b8 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -31,7 +31,7 @@ module type Id = sig val to_int : id -> int - val of_int : id -> int + val of_int : int -> id val nth : 'a list -> id -> 'a diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 45b2cce8..bd0ca184 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2666,12 +2666,47 @@ let expand_bottom_value_from_projection (config : C.config) | Ok ctx -> ctx | Error _ -> failwith "Unreachable" -let compute_expanded_symbolic_adt_value (tyctx : T.type_def list) - (expand_enumerations : bool) (def_id : T.TypeDefId.id) +(** Compute the expansion of an adt value. + + The function might return a list of contexts and values if the symbolic + value to expand is an enumeration. + + `expand_enumerations` controls the expansion of enumerations: if false, it + doesn't allow the expansion of enumerations *containing several variants*. + *) +let compute_expanded_symbolic_adt_value (expand_enumerations : bool) + (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.RegionId.id T.region list) (types : T.rty list) : - C.eval_ctx * V.typed_value = - raise Unimplemented + (regions : T.RegionId.id T.region list) (types : T.rty list) + (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list = + (* Lookup the definition and check if it is an enumeration with several + * variants *) + let def = T.TypeDefId.nth ctx.type_context def_id in + assert (List.length regions = List.length def.T.region_params); + (* Retrieve, for every variant, the list of its instantiated field types *) + let variants_fields_types = + Subst.type_def_get_instantiated_variants_fields_rtypes def regions types + in + (* Check if there is strictly more than one variant *) + if List.length variants_fields_types > 1 && not expand_enumerations then + failwith "Not allowed to expand enumerations with several variants"; + (* Initialize the expanded value for a given variant *) + let initialize (ctx : C.eval_ctx) + ((variant_id, field_types) : T.VariantId.id option * T.rty list) : + C.eval_ctx * V.typed_value = + let ctx, field_values = + List.fold_left_map + (fun ctx (ty : T.rty) -> + mk_fresh_symbolic_comp_proj ended_regions ty ctx) + ctx field_types + in + let av = V.Adt { variant_id; field_values } in + let ty = T.Adt (T.AdtId def_id, regions, types) in + let ty = Subst.erase_regions ty in + (ctx, { V.value = av; V.ty }) + in + (* Initialize all the expanded values of all the variants *) + List.map (initialize ctx) variants_fields_types let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) (field_types : T.rty list) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = @@ -2700,20 +2735,12 @@ let compute_expanded_symbolic_ref_value (ended_regions : T.RegionId.set_t) C.eval_ctx * V.typed_value = raise Unimplemented -(** Expand a symbolic value. +(** Expand a symbolic value which is not an enumeration with several variants. - Note that we return a list of contexts because when expanding enumerations - we need one context per variant. - - [expand_enumerations] controls whether we allow to expand enumerations with - strictly more than one variant or not. This only allowed when evaluating a - [Discriminant] rvalue. - If [expand_enumerations] is false, then the function always returns - exactly one evaluation context. + This function is used when exploring a path. *) -let expand_symbolic_value (config : C.config) (expand_enumerations : bool) - (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : - C.eval_ctx list = +let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) + (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : C.eval_ctx = (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let rty = sp.V.svalue.V.sv_ty in @@ -2722,10 +2749,17 @@ let expand_symbolic_value (config : C.config) (expand_enumerations : bool) match (pe, rty) with (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> + T.Adt (T.AdtId def_id', regions, types) ) -> ( assert (def_id = def_id'); - compute_expanded_symbolic_adt_value ctx.type_context expand_enumerations - def_id opt_variant_id regions types + (* Compute the expanded value - there should be exactly one because we + * don't allow to expand enumerations with strictly more than one variant *) + let expand_enumerations = false in + match + compute_expanded_symbolic_adt_value expand_enumerations ended_regions + def_id opt_variant_id regions types ctx + with + | [ (ctx, nv) ] -> (ctx, nv) + | _ -> failwith "Unexpected") (* Tuples *) | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> assert (arity = List.length tys); @@ -2744,14 +2778,6 @@ let expand_symbolic_value (config : C.config) (expand_enumerations : bool) (* Update the context *) raise Unimplemented -(** Expand a symbolic value which is not an enumeration with several variants *) -let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) - (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : C.eval_ctx = - let expand_enumerations = false in - match expand_symbolic_value config expand_enumerations pe sp ctx with - | [ ctx ] -> ctx - | _ -> failwith "Unexpected" - (** Update the environment to be able to read a place. When reading a place, we may be stuck along the way because some value diff --git a/src/Substitute.ml b/src/Substitute.ml index 35304c29..81b0ec7e 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -68,6 +68,34 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) : in fun id -> T.TypeVarId.Map.find id mp +(** Instantiate the type variables in an ADT definition, and return, for + every variant, the list of the types of its fields *) +let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def) + (regions : T.RegionId.id T.region list) (types : T.rty list) : + (T.VariantId.id option * T.rty list) list = + let r_subst = + make_region_subst + (List.map (fun x -> x.T.index) def.T.region_params) + regions + in + let ty_subst = + make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types + in + let (variants_fields : (T.VariantId.id option * T.field list) list) = + match def.T.kind with + | T.Enum variants -> + List.mapi + (fun i v -> (Some (T.VariantId.of_int i), v.T.fields)) + variants + | T.Struct fields -> [ (None, fields) ] + in + List.map + (fun (id, fields) -> + ( id, + List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields + )) + variants_fields + (** Instantiate the type variables in an ADT definition, and return the list of types of the fields for the chosen variant *) let type_def_get_instantiated_field_rtypes (def : T.type_def) |