diff options
| -rw-r--r-- | src/CfimOfJson.ml | 24 | ||||
| -rw-r--r-- | src/Interpreter.ml | 169 | ||||
| -rw-r--r-- | src/Print.ml | 99 | ||||
| -rw-r--r-- | src/Substitute.ml | 9 | ||||
| -rw-r--r-- | src/Types.ml | 13 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 4 | ||||
| -rw-r--r-- | src/Values.ml | 26 | ||||
| -rw-r--r-- | src/ValuesUtils.ml | 3 |
8 files changed, 149 insertions, 198 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 265a4c7b..0a7eeb78 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -78,14 +78,28 @@ let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result = combine_error_msgs js "assumed_ty_of_json" (match js with `String "Box" -> Ok T.Box | _ -> Error "") +let type_id_of_json (js : json) : (T.type_id, string) result = + combine_error_msgs js "type_id_of_json" + (match js with + | `Assoc [ ("Adt", id) ] -> + let* id = T.TypeDefId.id_of_json id in + Ok (T.AdtId id) + | `String "Tuple" -> Ok T.Tuple + | `Assoc [ ("Assumed", aty) ] -> + let* aty = assumed_ty_of_json aty in + Ok (T.Assumed aty) + | _ -> Error "") + let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) : ('r T.ty, string) result = combine_error_msgs js "ty_of_json" (match js with | `Assoc [ ("Adt", `List [ id; regions; types ]) ] -> - let* id = T.TypeDefId.id_of_json id in + let* id = type_id_of_json id in let* regions = list_of_json r_of_json regions in let* types = list_of_json (ty_of_json r_of_json) types in + (* Sanity check *) + (match id with T.Tuple -> assert (List.length regions = 0) | _ -> ()); Ok (T.Adt (id, regions, types)) | `Assoc [ ("TypeVar", `List [ id ]) ] -> let* id = T.TypeVarId.id_of_json id in @@ -108,14 +122,6 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) : let* ty = ty_of_json r_of_json ty in let* ref_kind = ref_kind_of_json ref_kind in Ok (T.Ref (region, ty, ref_kind)) - | `Assoc [ ("Tuple", `List [ types ]) ] -> - let* types = list_of_json (ty_of_json r_of_json) types in - Ok (T.Tuple types) - | `Assoc [ ("Assumed", `List [ assumed_ty; regions; types ]) ] -> - let* assumed_ty = assumed_ty_of_json assumed_ty in - let* regions = list_of_json r_of_json regions in - let* types = list_of_json (ty_of_json r_of_json) types in - Ok (T.Assumed (assumed_ty, regions, types)) | _ -> Error "") let rty_of_json (js : json) : (T.rty, string) result = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 90f5a30e..032d7844 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -68,8 +68,6 @@ let rec check_borrows_in_value (check : V.borrow_content -> bool) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> true | V.Adt av -> List.for_all (check_borrows_in_value check) av.field_values - | V.Tuple values -> List.for_all (check_borrows_in_value check) values - | V.Assumed (Box bv) -> check_borrows_in_value check bv | V.Borrow bc -> ( check bc && @@ -87,8 +85,6 @@ let rec check_loans_in_value (check : V.loan_content -> bool) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> true | V.Adt av -> List.for_all (check_loans_in_value check) av.field_values - | V.Tuple values -> List.for_all (check_loans_in_value check) values - | V.Assumed (Box bv) -> check_loans_in_value check bv | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> true @@ -106,8 +102,6 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> None | V.Adt av -> List.find_map (lookup_loan_in_value ek l) av.field_values - | V.Tuple values -> List.find_map (lookup_loan_in_value ek l) values - | V.Assumed (Box bv) -> lookup_loan_in_value ek l bv | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None @@ -160,11 +154,6 @@ let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id) let values = List.map (update_loan_in_value ek l nlc) av.field_values in let av = { av with field_values = values } in { v with value = Adt av } - | V.Tuple values -> - let values = List.map (update_loan_in_value ek l nlc) values in - { v with value = Tuple values } - | V.Assumed (Box bv) -> - { v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) } | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> v @@ -209,8 +198,6 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id) match v.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> None | V.Adt av -> List.find_map (lookup_borrow_in_value ek l) av.field_values - | V.Tuple values -> List.find_map (lookup_borrow_in_value ek l) values - | V.Assumed (Box bv) -> lookup_borrow_in_value ek l bv | V.Borrow bc -> ( match bc with | V.SharedBorrow bid -> if l = bid then Some bc else None @@ -260,11 +247,6 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id) let values = List.map (update_borrow_in_value ek l nbc) av.field_values in let av = { av with field_values = values } in { v with value = Adt av } - | V.Tuple values -> - let values = List.map (update_borrow_in_value ek l nbc) values in - { v with value = Tuple values } - | V.Assumed (Box bv) -> - { v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) } | V.Borrow bc -> ( match bc with | V.SharedBorrow bid | V.InactivatedMutBorrow bid -> @@ -344,8 +326,6 @@ let rec loans_in_value (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ -> false | V.Adt av -> List.exists loans_in_value av.field_values - | V.Tuple fields -> List.exists loans_in_value fields - | V.Assumed (Box bv) -> loans_in_value bv | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> false @@ -358,8 +338,6 @@ let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option = match v.V.value with | V.Concrete _ -> None | V.Adt av -> get_first_loan_in_values av.field_values - | V.Tuple fields -> get_first_loan_in_values fields - | V.Assumed (Box bv) -> get_first_loan_in_value bv | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None @@ -380,8 +358,6 @@ let rec bottom_in_value (v : V.typed_value) : bool = match v.V.value with | V.Concrete _ -> false | V.Adt av -> List.exists bottom_in_value av.field_values - | V.Tuple fields -> List.exists bottom_in_value fields - | V.Assumed (Box bv) -> bottom_in_value bv | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> false @@ -401,27 +377,17 @@ let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer) : V.typed_value * borrow_lres = match v0.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> (v0, NotFound) - | V.Assumed (Box bv) -> - let bv', res = - end_borrow_get_borrow_in_value config io l outer_borrows bv - in - (* Note that we allow boxes to outlive the inner borrows. - * Also note that when using the symbolic mode, boxes will never - * be "opened" and will be manipulated solely through functions - * like new, deref, etc. which will enforce that we destroy - * boxes upon ending inner borrows *) - ({ v0 with value = Assumed (Box bv') }, res) | V.Adt adt -> + (* Note that we allow assumed types (like boxes) to outlive their + * inner borrows. Also note that when using the symbolic mode, + * boxes will never be "opened" and will be manipulated solely + * through functions like new, deref, etc. which will enforce that + * we destroy boxes upon ending inner borrows *) let values, res = end_borrow_get_borrow_in_values config io l outer_borrows adt.field_values in ({ v0 with value = Adt { adt with field_values = values } }, res) - | V.Tuple values -> - let values, res = - end_borrow_get_borrow_in_values config io l outer_borrows values - in - ({ v0 with value = Tuple values }, res) | V.Loan (V.MutLoan _) -> (v0, NotFound) | V.Loan (V.SharedLoan (borrows, v)) -> (* Update the outer borrows, if necessary *) @@ -505,14 +471,6 @@ let rec give_back_value_to_value config bid (v : V.typed_value) List.map (give_back_value_to_value config bid v) av.field_values in { destv with value = Adt { av with field_values } } - | V.Tuple values -> - let values = List.map (give_back_value_to_value config bid v) values in - { destv with value = Tuple values } - | V.Assumed (Box destv') -> - { - destv with - value = Assumed (Box (give_back_value_to_value config bid v destv')); - } | V.Borrow bc -> (* We may need to insert the value inside a borrowed value *) let bc' = @@ -544,14 +502,6 @@ let rec give_back_shared_to_value (config : C.config) bid List.map (give_back_shared_to_value config bid) av.field_values in { destv with value = Adt { av with field_values } } - | V.Tuple values -> - let values = List.map (give_back_shared_to_value config bid) values in - { destv with value = Tuple values } - | V.Assumed (Box destv') -> - { - destv with - value = Assumed (Box (give_back_shared_to_value config bid destv')); - } | V.Borrow bc -> (* We may need to insert the value inside a borrowed value *) let bc' = @@ -644,11 +594,6 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id) | V.Adt av -> let fields = List.map reborrow_in_value av.field_values in { v with value = Adt { av with field_values = fields } } - | V.Tuple fields -> - let fields = List.map reborrow_in_value fields in - { v with value = Tuple fields } - | V.Assumed (Box bv) -> - { v with value = Assumed (Box (reborrow_in_value bv)) } | V.Borrow bc -> ( match bc with | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> v @@ -961,9 +906,12 @@ let rec access_projection (access : projection_access) (env : C.env) Ok (env, { read = v; updated = nv }) | pe :: p' -> ( (* Match on the projection element and the value *) - match (pe, v.V.value) with - (* Field projection *) - | Field (ProjAdt (_def_id, opt_variant_id), field_id), V.Adt adt -> ( + match (pe, v.V.value, v.V.ty) with + (* Field projection - ADTs *) + | ( Field (ProjAdt (def_id, opt_variant_id), field_id), + V.Adt adt, + T.Adt (T.AdtId def_id', _, _) ) -> ( + assert (def_id = def_id'); (* Check that the projection is consistent with the current value *) (match (opt_variant_id, adt.variant_id) with | None, None -> () @@ -982,30 +930,34 @@ let rec access_projection (access : projection_access) (env : C.env) let updated = { v with value = nadt } in Ok (env, { res with updated })) (* Tuples *) - | Field (ProjTuple arity, field_id), V.Tuple values -> ( - assert (arity = List.length values); - let fv = T.FieldId.nth values field_id in + | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( + assert (arity = List.length adt.field_values); + let fv = T.FieldId.nth adt.field_values field_id in (* Project *) match access_projection access env update p' fv with | Error err -> Error err | Ok (env, res) -> (* Update the field value *) - let nvalues = T.FieldId.update_nth values field_id res.updated in - let ntuple = V.Tuple nvalues in + let nvalues = + T.FieldId.update_nth adt.field_values field_id res.updated + in + let ntuple = V.Adt { adt with field_values = nvalues } in let updated = { v with value = ntuple } in Ok (env, { res with updated }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *)) - | Field (ProjAdt (_, _), _), V.Bottom -> + | Field (ProjAdt (_, _), _), V.Bottom, _ -> Error (FailBottom (1 + List.length p', pe, v.ty)) - | Field (ProjTuple _, _), V.Bottom -> + | Field (ProjTuple _, _), V.Bottom, _ -> Error (FailBottom (1 + List.length p', pe, v.ty)) (* Symbolic value: needs to be expanded *) - | _, Symbolic sp -> + | _, Symbolic sp, _ -> (* Expand the symbolic value *) Error (FailSymbolic (pe, sp)) (* Box dereferencement *) - | DerefBox, Assumed (Box bv) -> ( + | ( DerefBox, + Adt { variant_id = None; field_values = [ bv ] }, + T.Adt (T.Assumed T.Box, _, _) ) -> ( (* We allow moving inside of boxes. In practice, this kind of * manipulations should happen only inside unsage code, so * it shouldn't happen due to user code, and we leverage it @@ -1014,10 +966,16 @@ let rec access_projection (access : projection_access) (env : C.env) match access_projection access env update p' bv with | Error err -> Error err | Ok (env, res) -> - let nv = { v with value = V.Assumed (V.Box res.updated) } in + let nv = + { + v with + value = + V.Adt { variant_id = None; field_values = [ res.updated ] }; + } + in Ok (env, { res with updated = nv })) (* Borrows *) - | Deref, V.Borrow bc -> ( + | Deref, V.Borrow bc, _ -> ( match bc with | V.SharedBorrow bid -> (* Lookup the loan content, and explore from there *) @@ -1053,7 +1011,7 @@ let rec access_projection (access : projection_access) (env : C.env) in Ok (env, { res with updated = nv }) else Error (FailBorrow bc)) - | _, V.Loan lc -> ( + | _, V.Loan lc, _ -> ( match lc with | V.MutLoan bid -> Error (FailMutLoan bid) | V.SharedLoan (bids, sv) -> @@ -1072,13 +1030,12 @@ let rec access_projection (access : projection_access) (env : C.env) in Ok (env, { res with updated = nv }) else Error (FailSharedLoan bids)) - | ( _, - ( V.Concrete _ | V.Adt _ | V.Tuple _ | V.Bottom | V.Assumed _ - | V.Borrow _ ) ) as r -> - let pe, v = r in + | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> + let pe, v, ty = r in let pe = "- pe: " ^ E.show_projection_elem pe in let v = "- v:\n" ^ V.show_value v in - L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v); + let ty = "- ty:\n" ^ T.show_ety ty in + L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); failwith "Inconsistent projection") (** Generic function to access (read/write) the value at a given place. @@ -1192,7 +1149,7 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list) (* Initialize the expanded value *) let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in - let ty = T.Adt (def_id, regions, types) in + let ty = T.Adt (T.AdtId def_id, regions, types) in { V.value = av; V.ty } (** Compute an expanded tuple bottom value *) @@ -1200,8 +1157,8 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : V.typed_value = (* Generate the field values *) let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in - let v = V.Tuple fields in - let ty = T.Tuple field_types in + let v = V.Adt { variant_id = None; field_values = fields } in + let ty = T.Adt (T.Tuple, [], field_types) in { V.value = v; V.ty } (** Auxiliary helper to expand [Bottom] values. @@ -1251,12 +1208,14 @@ let expand_bottom_value_from_projection (config : C.config) *) let nv = match (pe, ty) with + (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (def_id', regions, types) ) -> + T.Adt (T.AdtId def_id', regions, types) ) -> assert (def_id = def_id'); compute_expanded_bottom_adt_value ctx.type_context def_id opt_variant_id regions types - | Field (ProjTuple arity, _), T.Tuple tys -> + (* Tuples *) + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> assert (arity = List.length tys); (* Generate the field values *) compute_expanded_bottom_tuple_value tys @@ -1361,8 +1320,6 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) to be copied, etc. we perform additional checks later *) () | V.Adt adt -> List.iter inspect_update adt.field_values - | V.Tuple values -> List.iter inspect_update values - | V.Assumed (Box v) -> inspect_update v | V.Borrow bc -> ( match bc with | V.SharedBorrow _ -> () @@ -1463,8 +1420,6 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) (* Nothing to do for symbolic values - TODO: not sure *) raise Unimplemented | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values - | V.Tuple values -> List.iter (inspect_update end_loans) values - | V.Assumed (Box v) -> inspect_update end_loans v | V.Borrow bc -> ( assert (not end_loans); @@ -1536,15 +1491,16 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) : match v.V.value with | V.Concrete _ -> (ctx, v) | V.Adt av -> + (* Sanity check *) + (match v.V.ty with + | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value" + | T.Adt ((T.AdtId _ | T.Tuple), _, _) -> () (* Ok *) + | _ -> failwith "Unreachable"); let ctx, fields = List.fold_left_map (copy_value config) ctx av.field_values in (ctx, { v with V.value = V.Adt { av with field_values = fields } }) - | V.Tuple fields -> - let ctx, fields = List.fold_left_map (copy_value config) ctx fields in - (ctx, { v with V.value = V.Tuple fields }) | V.Bottom -> failwith "Can't copy ⊥" - | V.Assumed _ -> failwith "Can't copy an assumed value" | V.Borrow bc -> ( (* We can only copy shared borrows *) match bc with @@ -1570,9 +1526,9 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (* Check the type while converting *) match (ty, cv) with (* Unit *) - | T.Tuple [], Unit -> { V.value = V.Tuple []; ty } + | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value (* Adt with one variant and no fields *) - | T.Adt (def_id, [], []), ConstantAdt def_id' -> + | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' -> assert (def_id = def_id'); (* Check that the adt definition only has one variant with no fields, compute the variant id at the same time. *) @@ -1837,7 +1793,9 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : match aggregate_kind with | E.AggregatedTuple -> let tys = List.map (fun v -> v.V.ty) values in - Ok (ctx, { V.value = Tuple values; ty = T.Tuple tys }) + let v = V.Adt { variant_id = None; field_values = values } in + let ty = T.Adt (T.Tuple, [], tys) in + Ok (ctx, { V.value = v; ty }) | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) let type_def = C.ctx_lookup_type_def ctx def_id in @@ -1849,7 +1807,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : assert (expected_field_types = List.map (fun v -> v.V.ty) values); (* Construct the value *) let av = { V.variant_id = opt_variant_id; V.field_values = values } in - let aty = T.Adt (def_id, regions, types) in + let aty = T.Adt (T.AdtId def_id, regions, types) in Ok (ctx, { V.value = Adt av; ty = aty })) (** Result of evaluating a statement - TODO: add prefix *) @@ -1920,7 +1878,7 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) let v = read_place_unwrap config access p ctx in (* Update the value *) match (v.V.ty, v.V.value) with - | T.Adt (def_id, regions, types), V.Adt av -> ( + | T.Adt (T.AdtId def_id, regions, types), V.Adt av -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -1940,7 +1898,7 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) in let ctx = write_place_unwrap config access p bottom_v ctx in Ok (ctx, Unit)) - | T.Adt (def_id, regions, types), V.Bottom -> + | T.Adt (T.AdtId def_id, regions, types), V.Bottom -> let bottom_v = compute_expanded_bottom_adt_value ctx.type_context def_id (Some variant_id) regions types @@ -1951,8 +1909,7 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) assert (config.mode = SymbolicMode); (* TODO *) raise Unimplemented | _, (V.Adt _ | V.Bottom) -> failwith "Inconsistent state" - | _, (V.Concrete _ | V.Tuple _ | V.Borrow _ | V.Loan _ | V.Assumed _) -> - failwith "Unexpected value" + | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> failwith "Unexpected value" (** Push a frame delimiter in the context's environment *) let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = @@ -1975,7 +1932,7 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx let get_non_local_function_return_type (fid : A.assumed_fun_id) (region_params : T.erased_region list) (type_params : T.ety list) : T.ety = match (fid, region_params, type_params) with - | A.BoxNew, [], [ bty ] -> T.Assumed (T.Box, [], [ bty ]) + | A.BoxNew, [], [ bty ] -> T.Adt (T.Assumed T.Box, [], [ bty ]) | A.BoxDeref, [], [ bty ] -> T.Ref (T.Erased, bty, T.Shared) | A.BoxDerefMut, [], [ bty ] -> T.Ref (T.Erased, bty, T.Mut) | A.BoxFree, [], [ _ ] -> mk_unit_ty @@ -2065,8 +2022,10 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list) in (* Create the box value *) - let box_ty = T.Assumed (T.Box, [], [ boxed_ty ]) in - let box_v = V.Assumed (V.Box moved_input_value) in + let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) in + let box_v = + V.Adt { variant_id = None; field_values = [ moved_input_value ] } + in let box_v = mk_typed_value box_ty box_v in (* Move this value to the return variable *) @@ -2080,7 +2039,7 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list) (** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *) let ty_get_box (box_ty : T.ety) : T.ety = match box_ty with - | T.Assumed (T.Box, [], [ boxed_ty ]) -> boxed_ty + | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> boxed_ty | _ -> failwith "Not a boxed type" (** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and diff --git a/src/Print.ml b/src/Print.ml index be6f4186..9863507e 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -51,11 +51,18 @@ module Types = struct | T.U64 -> "u64" | T.U128 -> "u128" + let type_id_to_string (fmt : 'r type_formatter) (id : T.type_id) : string = + match id with + | T.AdtId id -> fmt.type_def_id_to_string id + | T.Tuple -> "" + | T.Assumed aty -> ( match aty with Box -> "std::boxed::Box") + let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r T.ty) : string = match ty with | T.Adt (id, regions, tys) -> - let params = params_to_string fmt regions tys in - fmt.type_def_id_to_string id ^ params + let is_tuple = match id with T.Tuple -> true | _ -> false in + let params = params_to_string fmt is_tuple regions tys in + type_id_to_string fmt id ^ params | T.TypeVar tv -> fmt.type_var_id_to_string tv | T.Bool -> "bool" | T.Char -> "char" @@ -70,19 +77,14 @@ module Types = struct "&" ^ fmt.r_to_string r ^ " mut (" ^ ty_to_string fmt rty ^ ")" | T.Shared -> "&" ^ fmt.r_to_string r ^ " (" ^ ty_to_string fmt rty ^ ")") - | T.Tuple tys -> - "(" ^ String.concat ", " (List.map (ty_to_string fmt) tys) ^ ")" - | T.Assumed (aty, regions, tys) -> ( - let params = params_to_string fmt regions tys in - match aty with Box -> "std::boxed::Box" ^ params) - - and params_to_string (fmt : 'r type_formatter) (regions : 'r list) - (types : 'r T.ty list) : string = - if List.length regions + List.length types > 0 then - let regions = List.map fmt.r_to_string regions in - let types = List.map (ty_to_string fmt) types in - let params = String.concat ", " (List.append regions types) in - "<" ^ params ^ ">" + + and params_to_string (fmt : 'r type_formatter) (is_tuple : bool) + (regions : 'r list) (types : 'r T.ty list) : string = + let regions = List.map fmt.r_to_string regions in + let types = List.map (ty_to_string fmt) types in + let params = String.concat ", " (List.append regions types) in + if is_tuple then "(" ^ params ^ ")" + else if List.length regions + List.length types > 0 then "<" ^ params ^ ">" else "" let rty_to_string fmt (ty : T.rty) : string = ty_to_string fmt ty @@ -219,45 +221,44 @@ module Values = struct in match v.value with | Concrete cv -> constant_value_to_string cv - | Adt av -> - let def_id = - match v.ty with - | Adt (def_id, _, _) -> def_id - | _ -> failwith "Inconsistent value" - in - let adt_ident = - match av.variant_id with - | Some vid -> fmt.adt_variant_to_string def_id vid - | None -> fmt.type_def_id_to_string def_id + | Adt av -> ( + let is_tuple = + match v.ty with T.Adt (T.Tuple, _, _) -> true | _ -> false in let field_values = List.map (g_typed_value_to_string fmt gfmt) av.field_values in - if List.length field_values > 0 then - match fmt.adt_field_names def_id av.V.variant_id with - | None -> - let field_values = String.concat ", " field_values in - adt_ident ^ " (" ^ field_values ^ ")" - | Some field_names -> - let field_values = List.combine field_names field_values in - let field_values = - List.map - (fun (field, value) -> field ^ " = " ^ value ^ ";") - field_values - in - let field_values = String.concat " " field_values in - adt_ident ^ " { " ^ field_values ^ " }" - else adt_ident - | Tuple values -> - let values = - String.concat ", " - (List.map (g_typed_value_to_string fmt gfmt) values) - in - "(" ^ values ^ ")" + match v.ty with + | T.Adt (T.Tuple, _, _) -> + (* Tuple *) + "(" ^ String.concat ", " field_values ^ ")" + | T.Adt (T.AdtId def_id, _, _) -> + let adt_ident = + match av.variant_id with + | Some vid -> fmt.adt_variant_to_string def_id vid + | None -> fmt.type_def_id_to_string def_id + in + if List.length field_values > 0 then + match fmt.adt_field_names def_id av.V.variant_id with + | None -> + let field_values = String.concat ", " field_values in + adt_ident ^ " (" ^ field_values ^ ")" + | Some field_names -> + let field_values = List.combine field_names field_values in + let field_values = + List.map + (fun (field, value) -> field ^ " = " ^ value ^ ";") + field_values + in + let field_values = String.concat " " field_values in + adt_ident ^ " { " ^ field_values ^ " }" + else adt_ident + | T.Adt (T.Assumed aty, _, _) -> ( + match (aty, field_values) with + | Box, [ bv ] -> "@Box(" ^ bv ^ ")" + | _ -> failwith "Inconsistent value") + | _ -> failwith "Inconsistent typed value") | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty - | Assumed av -> ( - match av with - | Box bv -> "@Box(" ^ g_typed_value_to_string fmt gfmt bv ^ ")") | Borrow bc -> gfmt.bc_to_string bc | Loan lc -> gfmt.lc_to_string lc | Symbolic s -> gfmt.sv_to_string s diff --git a/src/Substitute.ml b/src/Substitute.ml index 635795ac..78109913 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -18,15 +18,12 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2) match ty with | Adt (def_id, regions, tys) -> Adt (def_id, List.map rsubst regions, List.map subst tys) - | Tuple tys -> Tuple (List.map subst tys) | Array aty -> Array (subst aty) | Slice sty -> Slice (subst sty) | Ref (r, ref_ty, ref_kind) -> Ref (rsubst r, subst ref_ty, ref_kind) - | Assumed (aty, regions, tys) -> - Assumed (aty, List.map rsubst regions, List.map subst tys) - (* Below variants: we technically return the same value, but because - one has type ['r1 ty] and the other has type ['r2 ty] we need to - deconstruct then reconstruct *) + (* Below variants: we technically return the same value, but because + one has type ['r1 ty] and the other has type ['r2 ty], we need to + deconstruct then reconstruct *) | Bool -> Bool | Char -> Char | Never -> Never diff --git a/src/Types.ml b/src/Types.ml index 8af62388..59a512eb 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -56,9 +56,17 @@ type ref_kind = Mut | Shared [@@deriving show] type assumed_ty = Box [@@deriving show] +(** Type identifier for ADTs. + + ADTs are very general in our encoding: they account for "regular" ADTs, + tuples and also assumed types. +*) +type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty +[@@deriving show] + type 'r ty = - | Adt of TypeDefId.id * 'r list * 'r ty list - | Tuple of 'r ty list + | Adt of type_id * 'r list * 'r ty list + (** [Adt] encodes ADTs, tuples and assumed types *) | TypeVar of TypeVarId.id | Bool | Char @@ -68,7 +76,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 - | Assumed of assumed_ty * 'r list * 'r ty list [@@deriving show] (* TODO: group Bool, Char, etc. in Constant *) diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index 0b8364a8..9741004c 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -17,7 +17,7 @@ let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) (** Return [true] if a [ty] is actually `unit` *) let ty_is_unit (ty : 'r ty) : bool = - match ty with Tuple tys -> List.length tys = 0 | _ -> false + match ty with Adt (Tuple, [], []) -> true | _ -> false (** The unit type *) -let mk_unit_ty : ety = Tuple [] +let mk_unit_ty : ety = Adt (Tuple, [], []) diff --git a/src/Values.ml b/src/Values.ml index 2ee2bdf5..f95cbc07 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -76,14 +76,10 @@ type symbolic_proj_comp = { Can be specialized for "regular" values or values in abstractions *) type ('r, 'sv, 'bc, 'lc) g_value = | Concrete of constant_value (** Concrete (non-symbolic) value *) - | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value (** Enumerations and structures *) - | Tuple of ('r, 'sv, 'bc, 'lc) g_typed_value list - (** Tuple - note that units are encoded as 0-tuples - TODO: merge with Adt? - *) + | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value + (** Enumerations, structures, tuples, assumed types. Note that units + are encoded as 0-tuples *) | Bottom (** No value (uninitialized or moved value) *) - | Assumed of ('r, 'sv, 'bc, 'lc) g_assumed_value - (** Value of an abstract type (Box, Vec, Cell...) *) | Borrow of 'bc (** A borrowed value *) | Loan of 'lc (** A loaned value *) | Symbolic of 'sv (** Unknown value *) @@ -96,10 +92,6 @@ and ('r, 'sv, 'bc, 'lc) g_adt_value = { [@@deriving show] (** "Generic" ADT value (not "GADT" value) *) -and ('r, 'sv, 'bc, 'lc) g_assumed_value = - | Box of ('r, 'sv, 'bc, 'lc) g_typed_value -[@@deriving show] - and ('r, 'sv, 'bc, 'lc) g_typed_value = { value : ('r, 'sv, 'bc, 'lc) g_value; ty : 'r ty; @@ -115,14 +107,6 @@ and adt_value = (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value [@@deriving show] -and assumed_value = - ( erased_region, - symbolic_proj_comp, - borrow_content, - loan_content ) - g_assumed_value -[@@deriving show] - and typed_value = ( erased_region, symbolic_proj_comp, @@ -177,10 +161,6 @@ type avalue = and aadt_value = (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_adt_value -and aassumed_value = - (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_assumed_value -[@@deriving show] - and typed_avalue = (RegionVarId.id region, aproj, aborrow_content, aloan_content) g_typed_value [@@deriving show] diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml index 3fd04b56..488de15d 100644 --- a/src/ValuesUtils.ml +++ b/src/ValuesUtils.ml @@ -2,6 +2,7 @@ module T = Types open TypesUtils open Values -let mk_unit_value : typed_value = { value = Tuple []; ty = mk_unit_ty } +let mk_unit_value : typed_value = + { value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty } let mk_typed_value (ty : T.ety) (value : value) : typed_value = { value; ty } |