diff options
| -rw-r--r-- | src/Identifiers.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 65 | ||||
| -rw-r--r-- | src/Types.ml | 24 | ||||
| -rw-r--r-- | src/Utilities.ml | 15 |
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) |