diff options
| -rw-r--r-- | src/Interpreter.ml | 322 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
2 files changed, 223 insertions, 101 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 901d12e3..e0ded437 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -76,6 +76,8 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs (** Generic borrow content: concrete or abstract *) +type abs_or_var = Abs of V.AbstractionId.id | Var of V.VarId.id + exception Found (** Utility exception @@ -143,9 +145,16 @@ let loans_in_value (v : V.typed_value) : bool = (** Lookup a loan content. The loan is referred to by a borrow id. + + TODO: group abs_or_var and g_loan_content. *) let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - g_loan_content option = + (abs_or_var * g_loan_content) option = + (* We store here whether we are inside an abstraction or a value - note that we + * could also track that with the environment, it would probably be more idiomatic + * and cleaner *) + let abs_or_var : abs_or_var option ref = ref None in + let obj = object inherit [_] C.iter_env as super @@ -202,15 +211,28 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : allow to dive inside abstractions, we allow to go anywhere (because there are no use cases requiring finer control) *) - method! visit_abs env abs = - if ek.enter_abs then super#visit_Abs env abs else () + method! visit_Var env bv v = + assert (Option.is_none !abs_or_var); + abs_or_var := Some (Var bv.C.index); + super#visit_Var env bv v; + abs_or_var := None + + method! visit_Abs env abs = + assert (Option.is_none !abs_or_var); + if ek.enter_abs then ( + abs_or_var := Some (Abs abs.V.abs_id); + super#visit_Abs env abs) + else () end in (* We use exceptions *) try obj#visit_env () env; None - with FoundGLoanContent lc -> Some lc + with FoundGLoanContent lc -> ( + match !abs_or_var with + | Some abs_or_var -> Some (abs_or_var, lc) + | None -> failwith "Inconsistent state") (** Lookup a loan content. @@ -218,10 +240,10 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : Raises an exception if no loan was found. *) let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - g_loan_content = + abs_or_var * g_loan_content = match lookup_loan_opt ek l env with | None -> failwith "Unreachable" - | Some lc -> lc + | Some res -> res (** Update a loan content. @@ -400,7 +422,7 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : The borrow is referred to by a borrow id. - This is a helper function: it might break invariants. + This is a helper function: it might break invariants. *) let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) (nbc : V.borrow_content) (env : C.env) : C.env = @@ -507,12 +529,16 @@ type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id let update_if_none opt x = match opt with None -> Some x | _ -> opt (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) -let update_outer_borrows (io : inner_outer) opt x = +let update_outer_borrows (io : inner_outer) + (outer : V.AbstractionId.id option * borrow_ids option) (x : borrow_ids) : + V.AbstractionId.id option * borrow_ids option = match io with | Inner -> (* If we can end inner borrows, we don't keep track of the outer borrows *) - None - | Outer -> update_if_none opt x + outer + | Outer -> + let abs, opt = outer in + (abs, update_if_none opt x) (** Return the first loan we find in a value *) let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = @@ -544,7 +570,11 @@ let bottom_in_value (v : V.typed_value) : bool = false with Found -> true -exception FoundOuter of borrow_ids +type outer_borrows_or_abs = + | OuterBorrows of borrow_ids + | OuterAbs of V.AbstractionId.id + +exception FoundOuter of outer_borrows_or_abs (** Utility exception *) (** Auxiliary function to end borrows: lookup a borrow in the environment, @@ -555,22 +585,40 @@ exception FoundOuter of borrow_ids [end_borrow] then simply performs a loop: as long as we need to end (outer) borrows, we end them, before finally ending the borrow we wanted to end in the first place. + + Note that it is possible to end a borrow in an abstraction, without ending + the whole abstraction, if the corresponding loan is inside the abstraction + as well. The [allowed_abs] parameter controls whether we allow to end borrows + in an abstraction or not, and in which abstraction. *) -let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id) - (env : C.env) : (C.env * V.borrow_content option, borrow_ids) result = +let end_borrow_get_borrow_in_env (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env) + : (C.env * g_borrow_content option, outer_borrows_or_abs) result = (* We use a reference to communicate the kind of borrow we found, if we * find one *) - let replaced_bc : V.borrow_content option ref = ref None in - let set_replaced_bc bc = + let replaced_bc : g_borrow_content option ref = ref None in + let set_replaced_bc (bc : g_borrow_content) = assert (Option.is_none !replaced_bc); replaced_bc := Some bc in - (* Raise an exception if there are outer borrows: this exception is caught - * in a wrapper function *) - let raise_if_outer outer_borrows = - match outer_borrows with - | Some borrows -> raise (FoundOuter borrows) - | None -> () + (* Raise an exception if there are outer borrows or if we are inside an + * abstraction: this exception is caught in a wrapper function *) + let raise_if_outer (outer : V.AbstractionId.id option * borrow_ids option) = + let outer_abs, outer_borrows = outer in + match outer_abs with + | Some abs -> ( + if + (* Check if we can end borrows inside this abstraction *) + Some abs <> allowed_abs + then raise (FoundOuter (OuterAbs abs)) + else + match outer_borrows with + | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) + | None -> ()) + | None -> ( + match outer_borrows with + | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) + | None -> ()) in (* The environment is used to keep track of the outer loans *) @@ -578,52 +626,59 @@ let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id) object inherit [_] C.map_env as super - method! visit_Loan outer_borrows lc = + method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option) + lc = match lc with - | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer_borrows bid) + | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid) | V.SharedLoan (bids, v) -> (* Update the outer borrows before diving into the shared value *) - let outer_borrows = - update_outer_borrows io outer_borrows (Borrows bids) - in - V.Loan (super#visit_SharedLoan outer_borrows bids v) + let outer = update_outer_borrows io outer (Borrows bids) in + V.Loan (super#visit_SharedLoan outer bids v) (** We reimplement [visit_Loan] because we may have to update the - outer borrows *) + outer borrows *) - method! visit_Borrow outer_borrows bc = + method! visit_Borrow outer bc = match bc with | SharedBorrow l' | InactivatedMutBorrow l' -> (* Check if this is the borrow we are looking for *) if l = l' then ( - (* Check if there are outer borrows *) - raise_if_outer outer_borrows; + (* Check if there are outer borrows or if we are inside an abstraction *) + raise_if_outer outer; (* Register the update *) - set_replaced_bc bc; + set_replaced_bc (Concrete bc); (* Update the value *) V.Bottom) - else super#visit_Borrow outer_borrows bc + else super#visit_Borrow outer bc | V.MutBorrow (l', bv) -> (* Check if this is the borrow we are looking for *) if l = l' then ( - (* Check if there are outer borrows *) - raise_if_outer outer_borrows; + (* Check if there are outer borrows or if we are inside an abstraction *) + raise_if_outer outer; (* Register the update *) - set_replaced_bc bc; + set_replaced_bc (Concrete bc); (* Update the value *) V.Bottom) else (* Update the outer borrows before diving into the borrowed value *) - let outer_borrows = - update_outer_borrows io outer_borrows (Borrow l') - in - V.Borrow (super#visit_MutBorrow outer_borrows l' bv) + let outer_borrows = update_outer_borrows io outer (Borrow l') in + V.Borrow (super#visit_MutBorrow outer l' bv) - method! visit_Abs _ _ = raise Unimplemented + method! visit_ALoan outer bc = raise Unimplemented + + method! visit_ABorrow outer bc = raise Unimplemented + + method! visit_abs outer abs = + (* Update the outer abs *) + let outer_abs, outer_borrows = outer in + assert (Option.is_none outer_abs); + assert (Option.is_none outer_borrows); + let outer = (Some abs.V.abs_id, None) in + super#visit_abs outer abs end in (* Catch the exceptions - raised if there are outer borrows *) try - let env = obj#visit_env None env in + let env = obj#visit_env (None, None) env in Ok (env, !replaced_bc) with FoundOuter outers -> Error outers @@ -784,81 +839,146 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) assert !r; { ctx with env } +(** Auxiliary function: see [end_borrow_in_env] *) +let give_back_in_env (config : C.config) (l : V.BorrowId.id) + (bc : g_borrow_content) (env : C.env) : C.env = + (* This is used for sanity checks *) + let sanity_ek = + { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } + in + match bc with + | Concrete (V.MutBorrow (_, tv)) -> + (* Check that the corresponding loan is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l env)); + give_back_value config l tv env + | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') -> + assert (l' = l); + (* Sanity check *) + (* Check that the borrow is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l env)); + give_back_shared config l env + | Abstract _ -> raise Unimplemented + (** End a borrow identified by its borrow id in an environment First lookup the borrow in the environment and replace it with [Bottom]. Then, check that there is an associated loan in the environment. When moving - values, before putting putting the value in its destination, we get an + values, before putting the value in its destination, we get an intermediate state where some values are "outside" the environment and thus - inaccessible. As [give_back_value] just performs a map for instance, we - need to check independently that there is indeed a loan ready to receive - the value we give back (note that we also have other invariants like: there - is exacly one mutable loan associated to a mutable borrow, etc. but they - are more easily maintained). Note that in theory, we shouldn't never reach a - problematic state as the one we describe above, because when we move a value - we need to end all the loans inside before moving it. Still, it is a very - useful sanity check. + inaccessible. As [give_back_value] just performs a map for instance (TODO: + not the case anymore), we need to check independently that there is indeed a + loan ready to receive the value we give back (note that we also have other + invariants like: there is exacly one mutable loan associated to a mutable + borrow, etc. but they are more easily maintained). + Note that in theory, we shouldn't never reach a problematic state as the + one we describe above, because when we move a value we need to end all the + loans inside before moving it. Still, it is a very useful sanity check. Finally, give the values back. Of course, we end outer borrows before updating the target borrow if it proves necessary: this is controled by the [io] parameter. If it is [Inner], we allow ending inner borrows (without ending the outer borrows first), otherwise we only allow ending outer borrows. + If a borrow is inside an abstraction, we need to end the whole abstraction, + at the exception of the case where the loan corresponding to the borrow is + inside the same abstraction. We control this with the [allowed_abs] parameter: + if it is not `None`, we allow ending a borrow if it is inside the given + abstraction. In practice, if the value is `Some abs_id`, we should have + checked that the corresponding loan is inside the abstraction given by + `abs_id` before. In practice, only [end_borrow_in_env] should call itself + with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`: + if you look ath the implementation details, `end_borrow_in_env` performs + all tne necessary checks in case a borrow is inside an abstraction. *) let rec end_borrow_in_env (config : C.config) (io : inner_outer) - (l : V.BorrowId.id) (env : C.env) : C.env = - (* This is used for sanity checks *) - let sanity_ek = - { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } - in - match end_borrow_get_borrow_in_env io l env with + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env) + : C.env = + match end_borrow_get_borrow_in_env io allowed_abs l env with (* Two cases: * - error: we found outer borrows (end them first) * - success: we didn't find outer borrows when updating (but maybe we actually didn't find the borrow we were looking for...) *) - | Error outer_borrows -> - (* End the outer borrows *) - let env = - match outer_borrows with - | Borrows bids -> end_borrows_in_env config io bids env - | Borrow bid -> end_borrow_in_env config io bid env - in - (* Retry to end the borrow *) - end_borrow_in_env config io l env + | Error outer -> ( + (* End the outer borrows, abstraction, then try again to end the target + * borrow (if necessary) *) + match outer with + | OuterBorrows (Borrows bids) -> + (* Note that when ending outer borrows, we use io=Outer. However, + * we shouldn't need to end outer borrows if io=Inner, so we just + * add the following assertion *) + assert (io = Outer); + let allowed_abs' = None in + let env = end_borrows_in_env config io allowed_abs' bids env in + (* Retry to end the borrow *) + end_borrow_in_env config io allowed_abs l env + | OuterBorrows (Borrow bid) -> + assert (io = Outer); + let allowed_abs' = None in + let env = end_borrow_in_env config io allowed_abs' bid env in + (* Retry to end the borrow *) + end_borrow_in_env config io allowed_abs l env + | OuterAbs abs_id -> ( + (* The borrow is inside an asbtraction: check if the corresponding + * loan is inside the same abstraction. If this is the case, we end + * the borrow without ending the abstraction. If not, we need to + * end the whole abstraction *) + let ek = + { + enter_shared_loans = true; + enter_mut_borrows = true; + enter_abs = true; + } + in + match lookup_loan ek l env with + | Abs loan_abs_id, _ -> + if loan_abs_id = abs_id then ( + (* Same abstraction! We can end the borrow *) + let env = end_borrow_in_env config io (Some abs_id) l env in + (* Sanity check *) + assert (Option.is_none (lookup_borrow_opt ek l env)); + env) + else + (* Not the same abstraction: we need to end the whole abstraction *) + let env = end_abstraction_in_env config abs_id env in + (* Sanity check *) + assert (Option.is_none (lookup_borrow_opt ek l env)); + env + | Var _, _ -> + (* The loan is not inside the same abstraction (actually inside + * a non-abstraction value): we need to end the whole abstraction *) + let env = end_abstraction_in_env config abs_id env in + (* Sanity check *) + assert (Option.is_none (lookup_borrow_opt ek l env)); + env)) | Ok (env, None) -> (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) assert (config.mode = SymbolicMode); env (* We found a borrow: give the value back (i.e., update the corresponding loan) *) - | Ok (env, Some bc) -> ( - match bc with - | V.MutBorrow (_, tv) -> - (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - give_back_value config l tv env - | V.SharedBorrow l' | V.InactivatedMutBorrow l' -> - assert (l' = l); - (* Sanity check *) - (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - give_back_shared config l env) + | Ok (env, Some bc) -> give_back_in_env config l bc env and end_borrows_in_env (config : C.config) (io : inner_outer) - (lset : V.BorrowId.Set.t) (env : C.env) : C.env = + (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) + (env : C.env) : C.env = V.BorrowId.Set.fold - (fun id env -> end_borrow_in_env config io id env) + (fun id env -> end_borrow_in_env config io allowed_abs id env) lset env +and end_abstraction_in_env (config : C.config) (abs : V.AbstractionId.id) + (env : C.env) : C.env = + raise Unimplemented + (** Same as [end_borrow_in_env], but operating on evaluation contexts *) -let end_borrow (config : C.config) (io : inner_outer) (l : V.BorrowId.id) +let end_borrow (config : C.config) (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_ctx = L.log#ldebug (lazy ("end_borrow " ^ V.BorrowId.to_string l ^ ": context before:\n" ^ eval_ctx_to_string ctx)); - let env = end_borrow_in_env config io l ctx.env in + let env = end_borrow_in_env config io allowed_abs l ctx.env in let ctx = { ctx with env } in L.log#ldebug (lazy @@ -867,14 +987,15 @@ let end_borrow (config : C.config) (io : inner_outer) (l : V.BorrowId.id) ctx (** Same as [end_borrows_in_env], but operating on evaluation contexts *) -let end_borrows (config : C.config) (io : inner_outer) (lset : V.BorrowId.Set.t) +let end_borrows (config : C.config) (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = L.log#ldebug (lazy ("end_borrows " ^ V.BorrowId.set_to_string lset ^ ": context before:\n" ^ eval_ctx_to_string ctx)); - let env = end_borrows_in_env config io lset ctx.env in + let env = end_borrows_in_env config io allowed_abs lset ctx.env in let ctx = { ctx with env } in L.log#ldebug (lazy @@ -883,13 +1004,13 @@ let end_borrows (config : C.config) (io : inner_outer) (lset : V.BorrowId.Set.t) ^ ": context after:\n" ^ eval_ctx_to_string ctx)); ctx -let end_outer_borrow config = end_borrow config Outer +let end_outer_borrow config = end_borrow config Outer None -let end_outer_borrows config = end_borrows config Outer +let end_outer_borrows config = end_borrows config Outer None -let end_inner_borrow config = end_borrow config Inner +let end_inner_borrow config = end_borrow config Inner None -let end_inner_borrows config = end_borrows config Inner +let end_inner_borrows config = end_borrows config Inner None (** Helper function: see [activate_inactivated_mut_borrow]. @@ -912,9 +1033,9 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx.env with - | Concrete (V.MutLoan _) -> + | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan, found a mut loan" - | Concrete (V.SharedLoan (bids, sv)) -> + | _, Concrete (V.SharedLoan (bids, sv)) -> (* Check that there is only one borrow id (l) and update the loan *) assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); (* We need to check that there aren't any loans in the value: @@ -930,7 +1051,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : let ctx = { ctx with env } in (* Return *) (ctx, sv) - | Abstract _ -> raise Unimplemented + | _, Abstract _ -> raise Unimplemented (** Helper function: see [activate_inactivated_mut_borrow]. @@ -964,8 +1085,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in match lookup_loan ek l ctx.env with - | Concrete (V.MutLoan _) -> failwith "Unreachable" - | Concrete (V.SharedLoan (bids, sv)) -> ( + | _, Concrete (V.MutLoan _) -> failwith "Unreachable" + | _, Concrete (V.SharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be inactivated borrows inside the value. If we perform an update, do a recursive call to lookup the updated value *) @@ -992,14 +1113,15 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) (* 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 ctx = end_borrows config io bids ctx in + let allowed_abs = None in + let ctx = end_borrows config io allowed_abs 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 [promote_shared_loan_to_mut_loan] *) promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx) - | Abstract _ -> raise Unimplemented + | _, Abstract _ -> raise Unimplemented (** Paths *) @@ -1148,8 +1270,8 @@ let rec access_projection (access : projection_access) (env : C.env) (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then match lookup_loan ek bid env with - | Concrete (V.MutLoan _) -> failwith "Expected a shared loan" - | Concrete (V.SharedLoan (bids, sv)) -> ( + | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan" + | _, Concrete (V.SharedLoan (bids, sv)) -> ( (* Explore the shared value *) match access_projection access env update p' sv with | Error err -> Error err @@ -1163,7 +1285,7 @@ let rec access_projection (access : projection_access) (env : C.env) in (* Return - note that we don't need to update the borrow itself *) Ok (env, { res with updated = v })) - | Abstract _ -> raise Unimplemented + | _, Abstract _ -> raise Unimplemented else Error (FailBorrow bc) | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) | V.MutBorrow (bid, bv) -> @@ -2021,10 +2143,10 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) let v = read_place_unwrap config access p ctx in match v.V.value with | V.Loan (V.SharedLoan (bids, _)) -> - let ctx = end_borrows config Outer bids ctx in + let ctx = end_outer_borrows config bids ctx in end_loan_exactly_at_place config access p ctx | V.Loan (V.MutLoan bid) -> - let ctx = end_borrow config Outer bid ctx in + let ctx = end_outer_borrow config bid ctx in end_loan_exactly_at_place config access p ctx | _ -> ctx diff --git a/src/Values.ml b/src/Values.ml index bd07ce98..f2f2274d 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -3,7 +3,7 @@ open Types (* TODO: I often write "abstract" (value, borrow content, etc.) while I should * write "abstraction" (because those values are not abstract, they simply are -* inside abstractions) *) + * inside abstractions) *) module VarId = IdGen () |