summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml15
-rw-r--r--src/InterpreterBorrows.ml100
-rw-r--r--src/InterpreterBorrowsCore.ml13
-rw-r--r--src/InterpreterExpansion.ml22
-rw-r--r--src/InterpreterProjectors.ml27
-rw-r--r--src/InterpreterStatements.ml17
-rw-r--r--src/Invariants.ml13
-rw-r--r--src/Print.ml17
-rw-r--r--src/Values.ml47
9 files changed, 220 insertions, 51 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2789517e..9ac8149b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -67,6 +67,9 @@ module Test = struct
List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
in
(* Create the abstractions and insert them in the context *)
+ let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+ ref V.AbstractionId.Map.empty
+ in
let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
let abs_id = rg.A.id in
let parents =
@@ -79,10 +82,20 @@ module Test = struct
(fun s rid -> T.RegionId.Set.add rid s)
T.RegionId.Set.empty rg.A.regions
in
+ let ancestors_regions =
+ List.fold_left
+ (fun acc parent_id ->
+ T.RegionId.Set.union acc
+ (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+ regions rg.A.parents
+ in
+ abs_to_ancestors_regions :=
+ V.AbstractionId.Map.add abs_id ancestors_regions
+ !abs_to_ancestors_regions;
(* Project over the values - we use *loan* projectors, as explained above *)
let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
(* Create the abstraction *)
- let abs = { V.abs_id; parents; regions; avalues } in
+ let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
(* Insert the abstraction in the context *)
let ctx = { ctx with env = Abs abs :: ctx.env } in
(* Return *)
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c9637f46..b52454b1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -169,9 +169,14 @@ let end_borrow_get_borrow (io : inner_outer)
* of the two cases described above *)
V.ABottom)
else V.ABorrow (super#visit_ASharedBorrow outer bid)
- | V.AIgnoredMutBorrow av ->
+ | V.AIgnoredMutBorrow (opt_bid, av) ->
(* Nothing special to do *)
- V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
+ V.ABorrow (super#visit_AIgnoredMutBorrow outer opt_bid av)
+ | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+ (* Nothing special to do *)
+ V.ABorrow
+ (super#visit_AEndedIgnoredMutBorrow outer given_back_loans_proj
+ child)
| V.AProjSharedBorrow asb ->
(* Check if the borrow we are looking for is in the asb *)
if borrow_in_asb l asb then (
@@ -232,7 +237,18 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
object (self)
inherit [_] C.map_eval_ctx as super
- method! visit_Loan opt_abs lc =
+ method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value =
+ match v.V.value with
+ | V.Loan lc ->
+ let value = self#visit_typed_Loan opt_abs v.V.ty lc in
+ ({ v with V.value } : V.typed_value)
+ | _ -> super#visit_typed_value opt_abs v
+ (** This is a bit annoying, but as we need the type of the value we
+ are exploring, for sanity checks, we need to implement
+ [visit_typed_avalue] instead of
+ overriding [visit_ALoan] *)
+
+ method visit_typed_Loan opt_abs ty lc =
match lc with
| V.SharedLoan (bids, v) ->
(* We are giving back a value (i.e., the content of a *mutable*
@@ -241,6 +257,15 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
| V.MutLoan bid' ->
(* Check if this is the loan we are looking for *)
if bid' = bid then (
+ (* Sanity check *)
+ let expected_ty = ty in
+ if nv.V.ty <> expected_ty then (
+ log#serror
+ ("give_back_value: improper type:\n- expected: "
+ ^ ety_to_string ctx ty ^ "\n- received: "
+ ^ ety_to_string ctx nv.V.ty);
+ failwith "Value given back doesn't have the proper type");
+ (* Replace *)
set_replaced ();
nv.V.value)
else V.Loan (super#visit_MutLoan opt_abs bid')
@@ -257,15 +282,46 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
back, we need to reimplement [visit_typed_avalue] instead of
[visit_ALoan] *)
+ method! visit_ABorrow (opt_abs : V.abs option) (bc : V.aborrow_content)
+ : V.avalue =
+ match bc with
+ | V.AIgnoredMutBorrow (bid', child) ->
+ if bid' = Some bid then
+ (* Insert a loans projector - note that if this case happens,
+ * it is necessarily because we ended a parent abstraction,
+ * and the given back value is thus a symbolic value *)
+ match nv.V.value with
+ | V.Symbolic sv ->
+ (* The loan projector *)
+ let given_back_loans_proj =
+ mk_aproj_loans_from_symbolic_value sv
+ in
+ (* Continue giving back in the child value *)
+ let child = super#visit_typed_avalue opt_abs child in
+ (* Return *)
+ V.ABorrow
+ (V.AEndedIgnoredMutBorrow { given_back_loans_proj; child })
+ | _ -> failwith "Unreachable"
+ else
+ (* Continue exploring *)
+ V.ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
+ | _ ->
+ (* Continue exploring *)
+ super#visit_ABorrow opt_abs bc
+ (** We need to inspect ignored mutable borrows, to insert loan projectors
+ if necessary.
+ *)
+
method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
(lc : V.aloan_content) : V.avalue =
(* Preparing a bit *)
- let regions =
+ let regions, ancestors_regions =
match opt_abs with
| None -> failwith "Unreachable"
- | Some abs -> abs.V.regions
+ | Some abs -> (abs.V.regions, abs.V.ancestors_regions)
in
- (* Rk.: there is a small issue with the types of the aloan values *)
+ (* Rk.: there is a small issue with the types of the aloan values.
+ * See the comment at the level of definition of [typed_avalue] *)
let borrowed_value_aty =
let _, ty, _ = ty_get_ref ty in
ty
@@ -281,8 +337,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
(* Apply the projection *)
let given_back =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- regions nv borrowed_value_aty
+ regions ancestors_regions nv borrowed_value_aty
in
+ (* Continue giving back in the child value *)
+ let child = super#visit_typed_avalue opt_abs child in
(* Return the new value *)
V.ALoan (V.AEndedMutLoan { given_back; child }))
else
@@ -307,8 +365,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
* (i.e., we don't call [set_replaced]) *)
let given_back =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- regions nv borrowed_value_aty
+ regions ancestors_regions nv borrowed_value_aty
in
+ (* Continue giving back in the child value *)
+ let child = super#visit_typed_avalue opt_abs child in
V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
| V.AEndedIgnoredMutLoan { given_back; child } ->
@@ -378,13 +438,22 @@ let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
match lc with
| V.AMutLoan (bid', child) ->
if bid' = bid then (
+ (* Sanity check - about why we need to call [ty_get_ref]
+ * (and don't do the same thing as in [give_back_value])
+ * see the comment at the level of the definition of
+ * [typed_avalue] *)
+ let _, expected_ty, _ = ty_get_ref ty in
+ if nv.V.ty <> expected_ty then (
+ log#serror
+ ("give_back_avalue: improper type:\n- expected: "
+ ^ rty_to_string ctx ty ^ "\n- received: "
+ ^ rty_to_string ctx nv.V.ty);
+ failwith "Value given back doesn't have the proper type");
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
* an ended loan *)
(* Register the insertion *)
set_replaced ();
- (* Sanity check *)
- assert (nv.V.ty = ty);
(* Return the new value *)
V.ALoan (V.AEndedMutLoan { given_back = nv; child }))
else
@@ -600,7 +669,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
assert (borrow_in_asb l asb);
(* Update the context *)
give_back_shared config l ctx
- | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
+ | Abstract (V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _) ->
+ failwith "Unreachable"
(** Convert an [avalue] to a [value].
@@ -889,7 +959,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
asb
then raise (FoundABorrowContent bc)
else ()
- | V.AIgnoredMutBorrow _ ->
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
(* Nothing to do for ignored borrows *)
()
end
@@ -918,7 +988,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
with
| V.AsbBorrow bid -> bid
| _ -> failwith "Unexpected")
- | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+ failwith "Unexpected"
in
let ctx = update_aborrow ek_all bid V.ABottom ctx in
(* Then give back the value *)
@@ -932,7 +1003,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
| V.AProjSharedBorrow _ ->
(* Nothing to do *)
ctx
- | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+ failwith "Unexpected"
in
(* Reexplore *)
end_abstraction_borrows config abs_id ctx
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index aaab18cb..b590eff6 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -305,7 +305,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
| V.ASharedBorrow bid ->
if bid = l then raise (FoundGBorrowContent (Abstract bc))
else super#visit_ASharedBorrow env bid
- | V.AIgnoredMutBorrow av -> super#visit_AIgnoredMutBorrow env av
+ | V.AIgnoredMutBorrow (opt_bid, av) ->
+ super#visit_AIgnoredMutBorrow env opt_bid av
+ | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+ super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj child
| V.AProjSharedBorrow asb ->
if borrow_in_asb l asb then
raise (FoundGBorrowContent (Abstract bc))
@@ -418,8 +421,12 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
| V.ASharedBorrow bid ->
if bid = l then update ()
else V.ABorrow (super#visit_ASharedBorrow env bid)
- | V.AIgnoredMutBorrow av ->
- V.ABorrow (super#visit_AIgnoredMutBorrow env av)
+ | V.AIgnoredMutBorrow (opt_bid, av) ->
+ V.ABorrow (super#visit_AIgnoredMutBorrow env opt_bid av)
+ | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+ V.ABorrow
+ (super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj
+ child)
| V.AProjSharedBorrow asb ->
if borrow_in_asb l asb then update ()
else V.ABorrow (super#visit_AProjSharedBorrow env asb)
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index aebcda3c..e19f8bb4 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -63,15 +63,17 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
object
inherit [_] C.map_eval_ctx as super
- method! visit_abs proj_regions abs =
- assert (Option.is_none proj_regions);
- let proj_regions = Some abs.V.regions in
- super#visit_abs proj_regions abs
+ method! visit_abs current_abs abs =
+ assert (Option.is_none current_abs);
+ let current_abs = Some abs in
+ super#visit_abs current_abs abs
(** When visiting an abstraction, we remember the regions it owns to be
able to properly reduce projectors when expanding symbolic values *)
- method! visit_ASymbolic proj_regions aproj =
- let proj_regions = Option.get proj_regions in
+ method! visit_ASymbolic current_abs aproj =
+ let current_abs = Option.get current_abs in
+ let proj_regions = current_abs.regions in
+ let ancestors_regions = current_abs.ancestors_regions in
match (aproj, proj_kind) with
| V.AProjLoans sv, LoanProj ->
(* Check if this is the symbolic value we are looking for *)
@@ -85,7 +87,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
projected_value.V.value
else
(* Not the searched symbolic value: nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
+ super#visit_ASymbolic (Some current_abs) aproj
| V.AProjBorrows (sv, proj_ty), BorrowProj ->
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then
@@ -101,16 +103,16 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
(* Apply the projector *)
let projected_value =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- proj_regions expansion proj_ty
+ proj_regions ancestors_regions expansion proj_ty
in
(* Replace *)
projected_value.V.value
else
(* Not the searched symbolic value: nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
+ super#visit_ASymbolic (Some current_abs) aproj
| V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
(* Nothing to do *)
- super#visit_ASymbolic (Some proj_regions) aproj
+ super#visit_ASymbolic (Some current_abs) aproj
end
in
(* Apply the expansion *)
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 036082eb..cbd07f3e 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -129,8 +129,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
*)
let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
- (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
- V.typed_avalue =
+ (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t)
+ (v : V.typed_value) (ty : T.rty) : V.typed_avalue =
(* Sanity check - TODO: move this elsewhere (here we perform the check at every
* recursive call which is a bit overkill...) *)
let ety = Substitute.erase_regions ty in
@@ -151,7 +151,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
List.map
(fun (fv, fty) ->
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- regions fv fty)
+ regions ancestors_regions fv fty)
fields_types
in
V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
@@ -169,7 +169,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(* Apply the projection on the borrowed value *)
let bv =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- regions bv ref_ty
+ regions ancestors_regions bv ref_ty
in
V.AMutBorrow (bid, bv)
| V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
@@ -183,13 +183,19 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(* Not in the set: ignore *)
let bc =
match (bc, kind) with
- | V.MutBorrow (_bid, bv), T.Mut ->
+ | V.MutBorrow (bid, bv), T.Mut ->
(* Apply the projection on the borrowed value *)
let bv =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
- regions bv ref_ty
+ regions ancestors_regions bv ref_ty
in
- V.AIgnoredMutBorrow bv
+ (* If the borrow id is in the ancestor's regions, we still need
+ * to remember it *)
+ let opt_bid =
+ if region_in_set r ancestors_regions then Some bid else None
+ in
+ (* Return *)
+ V.AIgnoredMutBorrow (opt_bid, bv)
| V.SharedBorrow bid, T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
@@ -493,8 +499,8 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
(fresh_reborrow, apply_registered_reborrows)
let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
- (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
- C.eval_ctx * V.typed_avalue =
+ (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t)
+ (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue =
let check_symbolic_no_ended = true in
let allow_reborrows = true in
(* Prepare the reborrows *)
@@ -503,7 +509,8 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
in
(* Apply the projector *)
let av =
- apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty
+ apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions
+ ancestors_regions v ty
in
(* Apply the reborrows *)
let ctx = apply_registered_reborrows ctx in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 36d11a9e..82f95556 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -815,6 +815,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
arg.V.ty = Subst.erase_regions rty)
args_with_rtypes);
(* Create the abstractions from the region groups and add them to the context *)
+ let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+ ref V.AbstractionId.Map.empty
+ in
let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
let abs_id = rg.A.id in
let parents =
@@ -827,17 +830,27 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(fun s rid -> T.RegionId.Set.add rid s)
T.RegionId.Set.empty rg.A.regions
in
+ let ancestors_regions =
+ List.fold_left
+ (fun acc parent_id ->
+ T.RegionId.Set.union acc
+ (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+ regions rg.A.parents
+ in
+ abs_to_ancestors_regions :=
+ V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions;
(* Project over the input values *)
let ctx, args_projs =
List.fold_left_map
(fun ctx (arg, arg_rty) ->
- apply_proj_borrows_on_input_value config ctx regions arg arg_rty)
+ apply_proj_borrows_on_input_value config ctx regions ancestors_regions
+ arg arg_rty)
ctx args_with_rtypes
in
(* Group the input and output values *)
let avalues = List.append args_projs [ ret_av ] in
(* Create the abstraction *)
- let abs = { V.abs_id; parents; regions; avalues } in
+ let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
(* Insert the abstraction in the context *)
let ctx = { ctx with env = Abs abs :: ctx.env } in
(* Return *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 3c5d24e3..be5f3ed3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -253,7 +253,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
match bc with
| V.AMutBorrow (bid, _) -> register_borrow Mut bid
| V.ASharedBorrow bid -> register_borrow Shared bid
- | V.AIgnoredMutBorrow _ | V.AProjSharedBorrow _ ->
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
+ | V.AProjSharedBorrow _ ->
(* Do nothing *)
()
in
@@ -347,7 +348,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
match bc with
| V.AMutBorrow (_, _) -> set_outer_mut info
| V.ASharedBorrow _ -> set_outer_shared info
- | V.AIgnoredMutBorrow _ -> set_outer_mut info
+ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+ set_outer_mut info
| V.AProjSharedBorrow _ -> set_outer_shared info
in
(* Continue exploring *)
@@ -526,7 +528,12 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Abstract (V.ASharedLoan (_, sv, _)) ->
assert (sv.V.ty = Subst.erase_regions ref_ty)
| _ -> failwith "Inconsistent context")
- | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty)
+ | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
+ assert (av.V.ty = ref_ty)
+ | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child }, T.Mut
+ ->
+ assert (given_back_loans_proj.V.ty = ref_ty);
+ assert (child.V.ty = ref_ty)
| V.AProjSharedBorrow _, T.Shared -> ()
| _ -> failwith "Inconsistent context")
| V.ALoan lc, aty -> (
diff --git a/src/Print.ml b/src/Print.ml
index ce31338d..5ae722b9 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -7,6 +7,9 @@ module A = CfimAst
module C = Contexts
module M = Modules
+let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
+ match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
+
(** Pretty-printing for types *)
module Types = struct
let type_var_to_string (tv : T.type_var) : string = tv.name
@@ -406,8 +409,18 @@ module Values = struct
^ typed_avalue_to_string fmt av
^ ")"
| ASharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
- | AIgnoredMutBorrow av ->
- "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")"
+ | AIgnoredMutBorrow (opt_bid, av) ->
+ "@ignored_mut_borrow("
+ ^ option_to_string V.BorrowId.to_string opt_bid
+ ^ ", "
+ ^ typed_avalue_to_string fmt av
+ ^ ")"
+ | AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+ "@ended_ignored_mut_borrow{ given_back_loans_proj="
+ ^ typed_avalue_to_string fmt given_back_loans_proj
+ ^ "; child="
+ ^ typed_avalue_to_string fmt child
+ ^ ")"
| AProjSharedBorrow sb ->
"@ignored_shared_borrow("
^ abstract_shared_borrows_to_string fmt sb
diff --git a/src/Values.ml b/src/Values.ml
index b6bb414b..c9dff56a 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -195,6 +195,8 @@ class ['self] iter_typed_avalue_base =
object (_self : 'self)
inherit [_] iter_typed_value
+ method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
+
method visit_region : 'env -> region -> unit = fun _ _ -> ()
method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
@@ -211,6 +213,8 @@ class ['self] map_typed_avalue_base =
object (_self : 'self)
inherit [_] map_typed_value
+ method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
+
method visit_region : 'env -> region -> region = fun _ r -> r
method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
@@ -421,11 +425,15 @@ and aborrow_content =
> abs0 { a_shared_bororw l0 }
```
*)
- | AIgnoredMutBorrow of typed_avalue
+ | AIgnoredMutBorrow of BorrowId.id option * typed_avalue
(** An ignored mutable borrow.
-
- This is mostly useful for typing concerns: when a borrow doesn't
- belong to an abstraction, it would be weird to ignore it altogether.
+
+ We need to keep track of ignored mut borrows because when ending such
+ borrows, we need to project the loans of the given back value to
+ insert them in the proper abstractions.
+
+ Note that we need to do so only for borrows consumed by parent
+ abstractions (hence the optional borrow id).
Example:
========
@@ -441,8 +449,29 @@ and aborrow_content =
> x -> mut_loan l0
> px -> mut_loan l1
> ppx -> ⊥
- > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow (U32 0)) } // TODO: duplication
- > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) }
+ > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
+ > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }
+
+ ... // abs'a ends
+
+ > x -> mut_loan l0
+ > px -> @s0
+ > ppx -> ⊥
+ > abs'b {
+ > a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
+ > (a_mut_borrow l0 (U32 0))
+ > }
+
+ ... // `@s0` gets expanded to `&mut l2 @s1`
+
+ > x -> mut_loan l0
+ > px -> &mut l2 @s1
+ > ppx -> ⊥
+ > abs'b {
+ > a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
+ > (a_mut_borrow l0 (U32 0))
+ > }
+
```
TODO: this is annoying, we are duplicating information. Maybe we
could introduce an "Ignored" value? We have to pay attention to
@@ -460,6 +489,10 @@ and aborrow_content =
abstraction so that we can properly call the backward functions
when generating the pure translation.
*)
+ | AEndedIgnoredMutBorrow of {
+ given_back_loans_proj : typed_avalue;
+ child : typed_avalue;
+ } (** See the explanations for [AIgnoredMutBorrow] *)
| AProjSharedBorrow of abstract_shared_borrows
(** A projected shared borrow.
@@ -522,6 +555,8 @@ type abs = {
abs_id : (AbstractionId.id[@opaque]);
parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *)
regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *)
+ ancestors_regions : (RegionId.set_t[@opaque]);
+ (** Union of the regions owned by this abstraction and its ancestors *)
avalues : typed_avalue list; (** The values in this abstraction *)
}
[@@deriving