Implement compute_expanded_symbolic_adt_value

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)