diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 84 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 25 |
2 files changed, 70 insertions, 39 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 029a2f1e..d17991ea 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -783,8 +783,11 @@ let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = perform anything smart and is trusted, and another function for the book-keeping. *) -let rec end_borrow (config : C.config) (allowed_abs : V.AbstractionId.id option) - (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_ctx = +let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + let chain0 = chain in + let chain = add_borrow_or_abs_id_to_chain "end_borrow: " (BorrowId l) chain in log#ldebug (lazy ("end borrow: " ^ V.BorrowId.to_string l ^ ":\n- original context:\n" @@ -838,14 +841,14 @@ let rec end_borrow (config : C.config) (allowed_abs : V.AbstractionId.id option) * be trying to end a borrow inside an abstraction, but which is actually * inside another borrow *) let allowed_abs' = None in - let ctx = end_borrows config allowed_abs' bids ctx in + let ctx = end_borrows config chain allowed_abs' bids ctx in (* Retry to end the borrow *) - end_borrow config allowed_abs l ctx + end_borrow config chain0 allowed_abs l ctx | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in - let ctx = end_borrow config allowed_abs' bid ctx in + let ctx = end_borrow config chain allowed_abs' bid ctx in (* Retry to end the borrow *) - let ctx = end_borrow config allowed_abs l ctx in + let ctx = end_borrow config chain0 allowed_abs l ctx in (* Sanity check *) check_disappeared ctx; (* Return *) @@ -868,16 +871,16 @@ let rec end_borrow (config : C.config) (allowed_abs : V.AbstractionId.id option) | AbsId loan_abs_id, _ -> if loan_abs_id = abs_id then (* Same abstraction! We can end the borrow *) - end_borrow config (Some abs_id) l ctx + end_borrow config chain0 (Some abs_id) l ctx else (* Not the same abstraction: we need to end the whole abstraction. * By doing that we should have ended the target borrow (see the * below sanity check) *) - end_abstraction config abs_id ctx + end_abstraction config chain abs_id ctx | VarId _, _ -> (* The loan is not inside the same abstraction (actually inside * a non-abstraction value): we need to end the whole abstraction *) - end_abstraction config abs_id ctx + end_abstraction config chain abs_id ctx in (* Sanity check *) check_disappeared ctx; @@ -906,14 +909,18 @@ let rec end_borrow (config : C.config) (allowed_abs : V.AbstractionId.id option) (* Return *) ctx -and end_borrows (config : C.config) (allowed_abs : V.AbstractionId.id option) - (lset : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = +and end_borrows (config : C.config) (chain : borrow_or_abs_ids) + (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) + (ctx : C.eval_ctx) : C.eval_ctx = V.BorrowId.Set.fold - (fun id ctx -> end_borrow config allowed_abs id ctx) + (fun id ctx -> end_borrow config chain allowed_abs id ctx) lset ctx -and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = +and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) + (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + let chain = + add_borrow_or_abs_id_to_chain "end_abstraction: " (AbsId abs_id) chain + in (* Remember the original context for printing purposes *) let ctx0 = ctx in log#ldebug @@ -924,7 +931,7 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in (* End the parent abstractions first *) - let ctx = end_abstractions config abs.parents ctx in + let ctx = end_abstractions config chain abs.parents ctx in log#ldebug (lazy ("end_abstraction: " @@ -932,14 +939,14 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) ^ "\n- context after parent abstractions ended:\n" ^ eval_ctx_to_string ctx)); (* End the loans inside the abstraction *) - let ctx = end_abstraction_loans config abs_id ctx in + let ctx = end_abstraction_loans config chain abs_id ctx in log#ldebug (lazy ("end_abstraction: " ^ V.AbstractionId.to_string abs_id ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)); (* End the abstraction itself by redistributing the borrows it contains *) - let ctx = end_abstraction_borrows config abs_id ctx in + let ctx = end_abstraction_borrows config chain abs_id ctx in (* End the regions owned by the abstraction - note that we don't need to * relookup the abstraction: the set of regions in an abstraction never * changes... *) @@ -962,14 +969,14 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) (* Return *) ctx -and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t) - (ctx : C.eval_ctx) : C.eval_ctx = +and end_abstractions (config : C.config) (chain : borrow_or_abs_ids) + (abs_ids : V.AbstractionId.set_t) (ctx : C.eval_ctx) : C.eval_ctx = V.AbstractionId.Set.fold - (fun id ctx -> end_abstraction config id ctx) + (fun id ctx -> end_abstraction config chain id ctx) abs_ids ctx -and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = +and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) + (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in (* End the first loan we find *) @@ -1015,14 +1022,14 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) | Borrows bids -> end_outer_borrows config bids ctx in (* Recheck *) - end_abstraction_loans config abs_id ctx + end_abstraction_loans config chain abs_id ctx | FoundSymbolicValue sv -> (* There is a proj_loans over a symbolic value: end the proj_borrows * which intersect this proj_loans *) - end_proj_loans_symbolic config abs_id abs.regions sv ctx + end_proj_loans_symbolic config chain abs_id abs.regions sv ctx -and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = +and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) + (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = (* Note that the abstraction mustn't contain any loans *) (* We end the borrows, starting with the *inner* ones. This is important when considering nested borrows which have the same lifetime. @@ -1131,7 +1138,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) failwith "Unexpected" in (* Reexplore *) - end_abstraction_borrows config abs_id ctx + end_abstraction_borrows config chain abs_id ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> (* Replace the proj_borrows - there should be exactly one *) @@ -1143,7 +1150,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) let nsv = mk_fresh_symbolic_value proj_ty in let ctx = give_back_symbolic_value config sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config abs_id ctx + end_abstraction_borrows config chain abs_id ctx (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : C.config) @@ -1174,9 +1181,9 @@ and end_abstraction_remove_from_context (_config : C.config) intersecting proj_borrows, either in the concrete context or in an abstraction *) -and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id) - (regions : T.RegionId.set_t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : - C.eval_ctx = +and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) + (abs_id : V.AbstractionId.id) (regions : T.RegionId.set_t) + (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with @@ -1205,7 +1212,7 @@ and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id) (fun s id -> V.AbstractionId.Set.add id s) V.AbstractionId.Set.empty abs_ids in - let ctx = end_abstractions config abs_ids ctx in + let ctx = end_abstractions config chain abs_ids ctx in (* We could end the owned projections, but it is simpler to simply return * and let the caller recheck if there are proj_loans to end *) ctx @@ -1234,15 +1241,15 @@ and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id) * or maybe not (if it is a proj over shared values): simply return, * as the caller function will recheck if there are loans to end in the * current abstraction *) - end_abstraction config abs_id' ctx + end_abstraction config chain abs_id' ctx -and end_outer_borrow config = end_borrow config None +and end_outer_borrow config = end_borrow config [] None -and end_outer_borrows config = end_borrows config None +and end_outer_borrows config = end_borrows config [] None -and end_inner_borrow config = end_borrow config None +and end_inner_borrow config = end_borrow config [] None -and end_inner_borrows config = end_borrows config None +and end_inner_borrows config = end_borrows config [] None (** Helper function: see [activate_inactivated_mut_borrow]. @@ -1352,8 +1359,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in - let allowed_abs = None in - let ctx = end_borrows config allowed_abs bids ctx in + let ctx = end_outer_borrows config bids ctx in (* Promote the loan *) let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in (* Promote the borrow - the value should have been checked by diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 00d2cbb3..3c39e76b 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -52,6 +52,31 @@ type loan_or_borrow_content = | BorrowContent of V.borrow_content [@@deriving show] +type borrow_or_abs_id = + | BorrowId of V.BorrowId.id + | AbsId of V.AbstractionId.id + +type borrow_or_abs_ids = borrow_or_abs_id list + +let borrow_or_abs_id_to_string (id : borrow_or_abs_id) : string = + match id with + | AbsId id -> "abs@" ^ V.AbstractionId.to_string id + | BorrowId id -> "l@" ^ V.BorrowId.to_string id + +let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string = + let ids = List.rev ids in + let ids = List.map borrow_or_abs_id_to_string ids in + String.concat " -> " ids + +(** Add a borrow or abs id to a chain of ids, while checking that we don't loop *) +let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id) + (ids : borrow_or_abs_ids) : borrow_or_abs_ids = + if List.mem id ids then + failwith + (msg ^ "detected a loop in the chain of ids: " + ^ borrow_or_abs_ids_chain_to_string (id :: ids)) + else id :: ids + (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that the regions which are already ended inside the abstraction don't |