summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml65
-rw-r--r--src/Types.ml24
-rw-r--r--src/Utilities.ml15
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)