summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-01 18:04:08 +0100
committerSon Ho2021-12-01 18:04:08 +0100
commit3562ff88d2c65d018b473fc2fb07359f95e6b2f9 (patch)
treed071ffc857fc0c59c7413f6d05850b76bbfa23f2
parentc943e63156ebe2df4f0819ecbb4597966e116868 (diff)
Merge the ADTs, tuples and assumed types in the type and value
definitions
-rw-r--r--src/CfimOfJson.ml24
-rw-r--r--src/Interpreter.ml169
-rw-r--r--src/Print.ml99
-rw-r--r--src/Substitute.ml9
-rw-r--r--src/Types.ml13
-rw-r--r--src/TypesUtils.ml4
-rw-r--r--src/Values.ml26
-rw-r--r--src/ValuesUtils.ml3
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 }