Implement expand_bottom_value

4 files changed, 105 insertions, 3 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 9b125161..adcb9124 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -29,6 +29,8 @@ module type Id = sig
 
   val update_nth : 'a vector -> id -> 'a -> 'a vector
 
+  val map : ('a -> 'b) -> 'a vector -> 'b vector
+
   module Set : Set.S with type elt = id
 
   val set_to_string : Set.t -> string
@@ -77,6 +79,8 @@ module IdGen () : Id = struct
     | _ :: vec', 0 -> v :: vec'
     | x :: vec', _ -> x :: update_nth vec' (id - 1) v
 
+  let map = List.map
+
   module Set = Set.Make (struct
     type t = id
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 21f347a6..f43848e6 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -710,10 +710,71 @@ let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) :
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
 *)
-(*let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
+let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
     (p : place) (env : env) (remaining_pes : int) (pe : projection_elem)
     (ty : ety) : env =
-  let *)
+  (* Prepare the update: we need to take the proper prefix of the place
+     during whose evaluation we got stuck *)
+  let projection' =
+    fst
+      (Utilities.list_split_at p.projection
+         (List.length p.projection - remaining_pes))
+  in
+  let p' = { p with projection = projection' } in
+  (* The type of the [Bottom] value should be a tuple or an ADT: use it
+     to generate the expanded value. Note that the projection element we
+     got stuck at should be a field projection, and gives the variant id
+     if the [Bottom] value is an enumeration value.
+     Also, the expanded value should be the proper ADT variant or a tuple
+     with the proper arity, with all the fields initialized to [Bottom]
+  *)
+  let nv =
+    match (pe, ty) with
+    | ( Field (ProjAdt (def_id, opt_variant_id), _),
+        Types.Adt (def_id', regions, types) ) ->
+        (* Lookup the definition and check if it is an enumeration - it
+           should be an enumeration if and only if the projection element
+           is a field projection with *some* variant id. Retrieve the list
+           of fields at the same time. *)
+        assert (def_id = def_id');
+        let def = TypeDefId.nth tyctx def_id in
+        let fields =
+          match (def.kind, opt_variant_id) with
+          | Struct fields, None -> fields
+          | Enum variants, Some variant_id ->
+              (* Retrieve the proper variant *)
+              let variant = VariantId.nth variants variant_id in
+              variant.fields
+        in
+        (* Initialize the expanded value *)
+        let fields = FieldId.vector_to_list fields in
+        let fields =
+          List.map
+            (fun f -> { value = Bottom; ty = erase_regions f.field_ty })
+            fields
+        in
+        let fields = FieldId.vector_of_list fields in
+        Values.Adt
+          {
+            def_id;
+            variant_id = opt_variant_id;
+            regions;
+            types;
+            field_values = fields;
+          }
+    | Field (ProjTuple arity, _), Types.Tuple tys ->
+        assert (arity = List.length tys);
+        (* Generate the field values *)
+        let fields = List.map (fun ty -> { value = Bottom; ty }) tys in
+        let fields = FieldId.vector_of_list fields in
+        Values.Tuple fields
+    | _ -> failwith "Unreachable"
+  in
+  let nv = { value = nv; ty } in
+  (* Update the environment by inserting the expanded value at the proper place *)
+  match write_place config nv p' env with
+  | Ok env -> env
+  | Error _ -> failwith "Unreachable"
 
 (** Update the environment to be able to read a place.
 
diff --git a/src/Types.ml b/src/Types.ml
index da01d73f..6f979718 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -59,6 +59,7 @@ type assumed_ty = Box
 
 type 'r ty =
   | Adt of TypeDefId.id * 'r list * 'r ty list
+  | Tuple of 'r ty list
   | TypeVar of TypeVarId.id
   | Bool
   | Char
@@ -68,7 +69,6 @@ type 'r ty =
   | Array of 'r ty (* TODO: there should be a constant with the array *)
   | Slice of 'r ty
   | Ref of 'r * 'r ty * ref_kind
-  | Tuple of 'r ty list
   | Assumed of assumed_ty * 'r list * 'r ty list
 
 type rty = RegionVarId.id region ty
@@ -98,3 +98,25 @@ type type_def = {
   type_params : type_var TypeVarId.vector;
   kind : type_def_kind;
 }
+
+(** Convert an [rty] to an [ety] by erasing the region variables *)
+let rec erase_regions (ty : rty) : ety =
+  match ty with
+  | Adt (def_id, regions, tys) ->
+      let regions = List.map (fun _ -> Erased) regions in
+      let tys = List.map erase_regions tys in
+      Adt (def_id, regions, tys)
+  | Tuple tys -> Tuple (List.map erase_regions tys)
+  | TypeVar vid -> TypeVar vid
+  | Bool -> Bool
+  | Char -> Char
+  | Never -> Never
+  | Integer int_ty -> Integer int_ty
+  | Str -> Str
+  | Array ty -> Array (erase_regions ty)
+  | Slice ty -> Slice (erase_regions ty)
+  | Ref (r, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
+  | Assumed (aty, regions, tys) ->
+      let regions = List.map (fun _ -> Erased) regions in
+      let tys = List.map erase_regions tys in
+      Assumed (aty, regions, tys)
diff --git a/src/Utilities.ml b/src/Utilities.ml
new file mode 100644
index 00000000..84cbd6e9
--- /dev/null
+++ b/src/Utilities.ml
@@ -0,0 +1,15 @@
+(* Split a list at a given index i (the first list contains all the elements
+   up to element of index i, not included, the second one contains the remaining
+   elements *)
+let rec list_split_at (ls : 'a list) (i : int) =
+  if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
+  else if i = 0 then ([], ls)
+  else
+    match ls with
+    | [] ->
+        raise
+          (Failure
+             "The int given to list_split_at should be <= the list's length")
+    | x :: ls' ->
+        let ls1, ls2 = list_split_at ls' (i - 1) in
+        (x :: ls1, ls2)