diff options
| -rw-r--r-- | src/Interpreter.ml | 15 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 100 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 13 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 22 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 27 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 17 | ||||
| -rw-r--r-- | src/Invariants.ml | 13 | ||||
| -rw-r--r-- | src/Print.ml | 17 | ||||
| -rw-r--r-- | src/Values.ml | 47 |
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 |