diff options
Diffstat (limited to '')
| -rw-r--r-- | TODO.md | 4 | ||||
| -rw-r--r-- | src/Contexts.ml | 14 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 186 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 50 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 196 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 8 | ||||
| -rw-r--r-- | src/Print.ml | 19 | ||||
| -rw-r--r-- | src/ValuesUtils.ml | 2 | ||||
| -rw-r--r-- | src/main.ml | 2 |
10 files changed, 291 insertions, 192 deletions
@@ -8,13 +8,15 @@ * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue * remove the rule which says that we can end a borrow under an abstraction if - the corresponding loan is in the same abstraction + the corresponding loan is in the same abstraction. + Also remove the io parameter from "end_borrow". * add a `allow_borrow_overwrites` in the loan projectors. * add option for: `allow_borrow_overwrites_on_input_values` (but always disallow borrow overwrites on returned values) + * During printing, contexts are often big, with many variables containing "bottom". Some variables also actually never get assigned, especially when they are used for auxiliary assignments which don't exist anymore (because they were merged diff --git a/src/Contexts.ml b/src/Contexts.ml index d8ea9a3f..6eafd9ef 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -2,6 +2,7 @@ open Types open Values open CfimAst module V = Values +open ValuesUtils (** Some global counters. * @@ -223,7 +224,7 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx = { ctx with env = Var (None, v) :: ctx.env } -(** Pop the first dummy variable from the context's environment. *) +(** Pop the first dummy variable from a context's environment. *) let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value = let rec pop_var (env : env) : env * typed_value = match env with @@ -236,8 +237,15 @@ let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value = let env, v = pop_var ctx.env in ({ ctx with env }, v) -(* TODO: move *) -let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty } +(** Read the first dummy variable in a context's environment. *) +let ctx_read_first_dummy_var (ctx : eval_ctx) : typed_value = + let rec read_var (env : env) : typed_value = + match env with + | [] -> failwith "Could not find a dummy variable" + | Var (None, v) :: _env -> v + | _ :: env -> read_var env + in + read_var ctx.env (** Push an uninitialized variable (which thus maps to [Bottom]) *) let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx = diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index c651e2f1..ccaa8bd4 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -26,7 +26,7 @@ open InterpreterProjectors let end_borrow_get_borrow (io : inner_outer) (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (ctx : C.eval_ctx) : - (C.eval_ctx * g_borrow_content option, outer_borrows_or_abs) result = + (C.eval_ctx * g_borrow_content option, priority_borrows_or_abs) result = (* We use a reference to communicate the kind of borrow we found, if we * find one *) let replaced_bc : g_borrow_content option ref = ref None in @@ -34,24 +34,40 @@ let end_borrow_get_borrow (io : inner_outer) assert (Option.is_none !replaced_bc); replaced_bc := Some bc in - (* 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) = + (* Raise an exception if: + * - there are outer borrows + * - if we are inside an abstraction + * - there are inner loans + * this exception is caught in a wrapper function *) + let raise_if_priority (outer : V.AbstractionId.id option * borrow_ids option) + (borrowed_value : V.typed_value option) = + (* First, look for outer borrows or abstraction *) let outer_abs, outer_borrows = outer in - match outer_abs with + (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)) + then raise (FoundPriority (OuterAbs abs)) else match outer_borrows with - | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) + | Some borrows -> raise (FoundPriority (OuterBorrows borrows)) | None -> ()) | None -> ( match outer_borrows with - | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) - | None -> ()) + | Some borrows -> raise (FoundPriority (OuterBorrows borrows)) + | None -> ())); + (* Then check if there are inner loans *) + match borrowed_value with + | None -> () + | Some v -> ( + match get_first_loan_in_value v with + | None -> () + | Some c -> ( + match c with + | V.SharedLoan (bids, _) -> + raise (FoundPriority (InnerLoans (Borrows bids))) + | V.MutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid))))) in (* The environment is used to keep track of the outer loans *) @@ -76,7 +92,7 @@ let end_borrow_get_borrow (io : inner_outer) (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) - raise_if_outer outer; + raise_if_priority outer None; (* Register the update *) set_replaced_bc (Concrete bc); (* Update the value *) @@ -86,7 +102,7 @@ let end_borrow_get_borrow (io : inner_outer) (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) - raise_if_outer outer; + raise_if_priority outer (Some bv); (* Register the update *) set_replaced_bc (Concrete bc); (* Update the value *) @@ -147,7 +163,7 @@ let end_borrow_get_borrow (io : inner_outer) *) (* Check there are outer borrows, or if we need to end the whole * abstraction *) - raise_if_outer outer; + raise_if_priority outer None; (* Register the update *) set_replaced_bc (Abstract bc); (* Update the value - note that we are necessarily in the second @@ -162,7 +178,7 @@ let end_borrow_get_borrow (io : inner_outer) if bid = l then ( (* Check there are outer borrows, or if we need to end the whole * abstraction *) - raise_if_outer outer; + raise_if_priority outer None; (* Register the update *) set_replaced_bc (Abstract bc); (* Update the value - note that we are necessarily in the second @@ -182,7 +198,7 @@ let end_borrow_get_borrow (io : inner_outer) if borrow_in_asb l asb then ( (* Check there are outer borrows, or if we need to end the whole * abstraction *) - raise_if_outer outer; + raise_if_priority outer None; (* Register the update *) set_replaced_bc (Abstract bc); (* Update the value - note that we are necessarily in the second @@ -206,7 +222,7 @@ let end_borrow_get_borrow (io : inner_outer) try let ctx = obj#visit_eval_ctx (None, None) ctx in Ok (ctx, !replaced_bc) - with FoundOuter outers -> Error outers + with FoundPriority outers -> Error outers (** Auxiliary function to end borrows. See [give_back]. @@ -219,6 +235,15 @@ let end_borrow_get_borrow (io : inner_outer) *) let give_back_value (config : C.config) (bid : V.BorrowId.id) (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = + (* Sanity check *) + assert (not (loans_in_value nv)); + assert (not (bottom_in_value ctx.ended_regions nv)); + (* Debug *) + log#ldebug + (lazy + ("give_back_value:\n- bid: " ^ V.BorrowId.to_string bid ^ "\n- value: " + ^ typed_value_to_string ctx nv + ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = @@ -631,6 +656,16 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) (** Auxiliary function: see [end_borrow_in_env] *) let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) (ctx : C.eval_ctx) : C.eval_ctx = + (* Debug *) + log#ldebug + (lazy + (let bc = + match bc with + | Concrete bc -> borrow_content_to_string ctx bc + | Abstract bc -> aborrow_content_to_string ctx bc + in + "give_back:\n- bid: " ^ V.BorrowId.to_string l ^ "\n- content: " ^ bc + ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* This is used for sanity checks *) let sanity_ek = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -639,6 +674,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) | Concrete (V.MutBorrow (l', tv)) -> (* Sanity check *) assert (l' = l); + assert (not (loans_in_value tv)); (* Check that the corresponding loan is somewhere - purely a sanity check *) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) @@ -727,10 +763,46 @@ let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`: if you look ath the implementation details, `end_borrow` performs all tne necessary checks in case a borrow is inside an abstraction. + + TODO: we should split this function in two: one function which doesn't + perform anything smart and is trusted, and another function for the + book-keeping. *) let rec 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 = + log#ldebug + (lazy + ("end borrow: " ^ V.BorrowId.to_string l ^ ":\n- original context:\n" + ^ eval_ctx_to_string ctx)); + (* Utility function for the sanity checks: check that the borrow disappeared + * from the context *) + let ctx0 = ctx in + let check_disappeared (ctx : C.eval_ctx) : unit = + let _ = + match lookup_borrow_opt ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#lerror + (lazy + ("end borrow: " ^ V.BorrowId.to_string l + ^ ": borrow didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ctx)); + failwith "Borrow not eliminated" + in + match lookup_loan_opt ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#lerror + (lazy + ("end borrow: " ^ V.BorrowId.to_string l + ^ ": loan didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ctx)); + failwith "Loan not eliminated" + in + match end_borrow_get_borrow io allowed_abs l ctx with (* Two cases: * - error: we found outer borrows (end them first) @@ -738,10 +810,16 @@ let rec end_borrow (config : C.config) (io : inner_outer) didn't find the borrow we were looking for...) *) | Error outer -> ( - (* End the outer borrows, abstraction, then try again to end the target + (* Debug *) + log#ldebug + (lazy + ("end borrow: " ^ V.BorrowId.to_string l + ^ ": found outer borrows/abs:" + ^ show_priority_borrows_or_abs outer)); + (* End the priority borrows, abstraction, then try again to end the target * borrow (if necessary) *) match outer with - | OuterBorrows (Borrows bids) -> + | OuterBorrows (Borrows bids) | InnerLoans (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 *) @@ -753,14 +831,18 @@ let rec end_borrow (config : C.config) (io : inner_outer) let ctx = end_borrows config io allowed_abs' bids ctx in (* Retry to end the borrow *) end_borrow config io allowed_abs l ctx - | OuterBorrows (Borrow bid) -> + | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> (* See the comments for the previous case *) assert (io = Outer); let allowed_abs' = None in let ctx = end_borrow config io allowed_abs' bid ctx in (* Retry to end the borrow *) - end_borrow config io allowed_abs l ctx - | OuterAbs abs_id -> ( + let ctx = end_borrow config io allowed_abs l ctx in + (* Sanity check *) + check_disappeared ctx; + (* Return *) + ctx + | 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 @@ -773,36 +855,48 @@ let rec end_borrow (config : C.config) (io : inner_outer) enter_abs = true; } in - match lookup_loan ek l ctx with - | AbsId loan_abs_id, _ -> - if loan_abs_id = abs_id then ( - (* Same abstraction! We can end the borrow *) - let ctx = end_borrow config io (Some abs_id) l ctx in - (* Sanity check *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - 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) *) - let ctx = end_abstraction config abs_id ctx in - (* Sanity check: we ended the target borrow *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - ctx - | VarId _, _ -> - (* The loan is not inside the same abstraction (actually inside - * a non-abstraction value): we need to end the whole abstraction *) - let ctx = end_abstraction config abs_id ctx in - (* Sanity check: we ended the target borrow *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - ctx)) + let ctx = + match lookup_loan ek l ctx with + | AbsId loan_abs_id, _ -> + if loan_abs_id = abs_id then + (* Same abstraction! We can end the borrow *) + end_borrow config io (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 + | 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 + in + (* Sanity check *) + check_disappeared ctx; + (* Return *) + ctx) | Ok (ctx, None) -> + log#ldebug (lazy "End borrow: borrow not found"); (* 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); + (* Sanity check *) + check_disappeared ctx; + (* Return *) + ctx + (* We found a borrow: give it back (i.e., update the corresponding loan) *) + | Ok (ctx, Some bc) -> + (* Sanity check: the borrowed value shouldn't contain loans *) + (match bc with + | Concrete (V.MutBorrow (_, bv)) -> + assert (Option.is_none (get_first_loan_in_value bv)) + | _ -> ()); + (* Give back the value *) + let ctx = give_back config l bc ctx in + (* Sanity check *) + check_disappeared ctx; + (* Return *) ctx - (* We found a borrow: give the value back (i.e., update the corresponding loan) *) - | Ok (ctx, Some bc) -> give_back config l bc ctx and end_borrows (config : C.config) (io : inner_outer) (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) @@ -1133,7 +1227,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) log#ldebug (lazy ("activate_inactivated_mut_borrow: resulting value:\n" - ^ V.show_typed_value sv)); + ^ typed_value_to_string ctx sv)); assert (not (loans_in_value sv)); assert (not (bottom_in_value ctx.ended_regions sv)); assert (not (inactivated_in_value sv)); diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 13ad8ee6..3d908e73 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -38,19 +38,27 @@ let ek_all : exploration_kind = *) type inner_outer = Inner | Outer -type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id +type borrow_ids = Borrows of V.BorrowId.set_t | Borrow of V.BorrowId.id +[@@deriving show] exception FoundBorrowIds of borrow_ids -type outer_borrows_or_abs = +type priority_borrows_or_abs = | OuterBorrows of borrow_ids | OuterAbs of V.AbstractionId.id + | InnerLoans of borrow_ids +[@@deriving show] let update_if_none opt x = match opt with None -> Some x | _ -> opt -exception FoundOuter of outer_borrows_or_abs +exception FoundPriority of priority_borrows_or_abs (** Utility exception *) +type loan_or_borrow_content = + | LoanContent of V.loan_content + | BorrowContent of V.borrow_content +[@@deriving show] + (** Lookup a loan content. The loan is referred to by a borrow id. @@ -469,3 +477,39 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = obj#visit_typed_value () v; None with FoundLoanContent lc -> Some lc + +(** Return the first borrow we find in a value *) +let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option = + let obj = + object + inherit [_] V.iter_typed_value + + method! visit_borrow_content _ bc = raise (FoundBorrowContent bc) + end + in + (* We use exceptions *) + try + obj#visit_typed_value () v; + None + with FoundBorrowContent bc -> Some bc + +(** Return the first loan or borrow content we find in a value (starting with + the outer ones) *) +let get_first_loan_or_borrow_in_value (v : V.typed_value) : + loan_or_borrow_content option = + let obj = + object + inherit [_] V.iter_typed_value + + method! visit_borrow_content _ bc = raise (FoundBorrowContent bc) + + method! visit_loan_content _ lc = raise (FoundLoanContent lc) + end + in + (* We use exceptions *) + try + obj#visit_typed_value () v; + None + with + | FoundLoanContent lc -> Some (LoanContent lc) + | FoundBorrowContent bc -> Some (BorrowContent bc) diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index bf039b52..4213f4fa 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -576,149 +576,71 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) seen as an l-value (we will write to it later, but need to drop the borrows before writing). - We start by only dropping the borrows, then we end the loans. The reason - is that some loan we find may be borrowed by another part of the subvalue. - In order to correctly handle the "outer borrow" priority (we should end - the outer borrows first) which is not really applied here (we are preparing - the value for override: we can end the borrows inside, without ending the - borrows we traversed to actually access the value) we first end the borrows - we find in the place, to make sure all the "local" loans are taken care of. - Then, if we find a loan, it means it is "externally" borrowed (the associated - borrow is not in a subvalue of the place under inspection). - Also note that whenever we end a loan, we might propagate back a value inside - the place under inspection: we must re-end all the borrows we find there, - before reconsidering loans. - - Repeat: - - read the value at a given place - - as long as we find a loan or a borrow, end it - This is used to drop values (when we need to write to a place, we first drop the value there to properly propagate back values which are not/can't be borrowed anymore). + + Note that we don't do what is defined in the formalization: we move the + value to a temporary dummy value, then explore this value and end the + loans/borrows inside as long as we find some, starting with the outer + ones. + + TODO: rewrite that. Consider the following example: + Example: + ======= + We want to end the borrows/loans at `*x` in the following environment: + ``` + x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), + mut_loan l2, mut_borrow l2 (mut_loan l3)) + y -> mut_borrow l3 (Bool true) + ``` + We have to consider several things: + - the borrows `mut_borrow l1 (Int 3)` `mut_borrow l2 ...` borrow subvalues of `*x` + - we can't immediately end `mut_borrow l2 ...` because it contains a loan + - the borrow corresponding to the loan `mut_loan l3` is outside of `*x` *) -let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) +let drop_borrows_loans_at_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Iterator to explore a value and update the context whenever we find - borrows/loans. - We use exceptions to make it handy: whenever we update the - context, we raise an exception wrapping the updated context. - - Note that we can end the borrows which are inside the value (while the - value itself might be inside a borrow/loan: we are thus ending inner - borrows). Because a loan inside the value may be linked to a borrow - somewhere else *also inside* the value (it's possible with adts), - we first end all the borrows we find - by using [Inner] to allow - ending inner borrows - then end all the loans we find. - - It is really important to do this in two steps: the borrow linked to a - loan may be inside the value at place p, in which case this borrow may be - an inner borrow that we *can* end, but it may also be outside this - value, in which case we need to end all the outer borrows first... - Also, whenever the context is updated, we need to re-inspect - the value at place p *in two steps* again (end borrows, then end - loans). - - Example: - ======= - We want to end the borrows/loans at `*x` in the following environment: - ``` - x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - We have to consider two things: - - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x` - - the borrow corresponding to the loan `mut_loan l2` is outside of `*x` - - We first end all the *borrows* (not the loans) inside of `*x`, which gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - Note that when ending the borrows, we can (and have to) ignore the outer - borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end - the borrow `l0` which is incorrect (note that we might have to drop the - borrows/loans at `*x` if we evaluate, for instance, `*x = ...`). - It is ok to ignore outer borrows in this case because whenever - we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore - the outer borrows when accessing `*x`, but once examining the value at - `*x` we never dive into borrows: whenever we find one, we end it - it is thus - an outer borrow, in some way). - - Then, we end the loans at `*x`. Note that as at this point `*x` doesn't - contain borrows (only loans), the borrows corresponding to those loans - are thus necessarily outside of `*x`: we mustn't ignore outer borrows this - time. This gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, Bool true) - y -> ⊥ - ``` - *) - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content end_loans bc = - (* Sanity check: we should have ended all the borrows before starting - to end loans *) - assert (not end_loans); - - (* We need to end all borrows. Note that we ignore the outer borrows - when ending the borrows we find here (we call [end_inner_borrow(s)]: - the value at place p might be below a borrow/loan). Note however - that if we restrain ourselves at the value at place p, the borrow we - found here can be considered as an outer borrow. - *) - match bc with - | V.SharedBorrow bid | V.MutBorrow (bid, _) -> - raise (UpdateCtx (end_inner_borrow config bid ctx)) - | V.InactivatedMutBorrow bid -> - (* We need to activate ithe nactivated borrow - later, we will - * actually end it - Rk.: we could actually end it straight away - * (this is not really important) *) - let ctx = activate_inactivated_mut_borrow config Inner bid ctx in - raise (UpdateCtx ctx) - - method! visit_loan_content end_loans lc = - if - (* If we can, end the loans, otherwise ignore: keep for later *) - end_loans - then - (* We need to end all loans. Note that as all the borrows inside - the value at place p should already have ended, the borrows - associated to the loans we find here should be borrows from - outside this value: we need to call [end_outer_borrow(s)] - (we can't ignore outer borrows this time). - *) - match lc with - | V.SharedLoan (bids, _) -> - raise (UpdateCtx (end_outer_borrows config bids ctx)) - | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx)) - else super#visit_loan_content end_loans lc - end - in - - (* We do something similar to [end_loans_at_place]. - First, retrieve the value *) - match read_place config Write p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> ( - (* Inspect the value and update the context while doing so. - If the context gets updated: perform a recursive call (many things - may have been updated in the context: first we need to retrieve the - proper updated value - and this value may actually not be accessible - anymore - *) - try - (* Inspect the value: end the borrows only *) - obj#visit_typed_value false v; - (* Inspect the value: end the loans *) - obj#visit_typed_value true v; - (* No context update required: return the current context *) + (* Move the current value in the place outside of this place and into + * a dummy variable *) + let access = Write in + let v = read_place_unwrap config access p ctx in + let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in + let ctx = C.ctx_push_dummy_var ctx v in + (* Auxiliary function *) + let rec drop (ctx : C.eval_ctx) : C.eval_ctx = + (* Read the value *) + let v = C.ctx_read_first_dummy_var ctx in + (* Check if there are loans or borrows to end *) + match get_first_loan_or_borrow_in_value v with + | None -> + (* We are done *) ctx - with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx) + | Some c -> + (* There are: end them then retry *) + let ctx = + match c with + | LoanContent (V.SharedLoan (bids, _)) -> + end_outer_borrows config bids ctx + | LoanContent (V.MutLoan bid) + | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) -> + end_outer_borrow config bid ctx + | BorrowContent (V.InactivatedMutBorrow bid) -> + (* First activate the borrow *) + activate_inactivated_mut_borrow config Outer bid ctx + in + (* Retry *) + drop ctx + in + (* Apply *) + let ctx = drop ctx in + (* Pop the temporary value *) + let ctx, v = C.ctx_pop_dummy_var ctx in + (* Sanity check *) + assert (not (loans_in_value v)); + assert (not (borrows_in_value v)); + (* Return *) + ctx (** Copy a value, and return the resulting value. diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 23fe8d3b..cda682a3 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -810,7 +810,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) | ret_ty :: locals -> (ret_ty, locals) | _ -> failwith "Unreachable" in - let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in + let ctx = C.ctx_push_var ctx ret_var (mk_bottom ret_var.var_ty) in (* 2. Push the input values *) let input_locals, locals = Utils.list_split_at locals def.A.arg_count in diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index a808e14c..315459fc 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -21,6 +21,14 @@ let rty_to_string = PA.rty_to_string let symbolic_value_to_string = PA.symbolic_value_to_string +let borrow_content_to_string = PA.borrow_content_to_string + +let loan_content_to_string = PA.loan_content_to_string + +let aborrow_content_to_string = PA.aborrow_content_to_string + +let aloan_content_to_string = PA.aloan_content_to_string + let typed_value_to_string = PA.typed_value_to_string let typed_avalue_to_string = PA.typed_avalue_to_string diff --git a/src/Print.ml b/src/Print.ml index 4dbe30f7..bc527acc 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -988,6 +988,25 @@ module EvalCtxCfimAst = struct let fmt = PC.ctx_to_rtype_formatter fmt in PT.rty_to_string fmt t + let borrow_content_to_string (ctx : C.eval_ctx) (bc : V.borrow_content) : + string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.borrow_content_to_string fmt bc + + let loan_content_to_string (ctx : C.eval_ctx) (lc : V.loan_content) : string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.loan_content_to_string fmt lc + + let aborrow_content_to_string (ctx : C.eval_ctx) (bc : V.aborrow_content) : + string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.aborrow_content_to_string fmt bc + + let aloan_content_to_string (ctx : C.eval_ctx) (lc : V.aloan_content) : string + = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.aloan_content_to_string fmt lc + let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) : string = let fmt = PC.eval_ctx_to_ctx_formatter ctx in diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml index f4a10287..16c94800 100644 --- a/src/ValuesUtils.ml +++ b/src/ValuesUtils.ml @@ -8,6 +8,8 @@ let mk_unit_value : typed_value = let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty } +let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty } + (** Box a value *) let mk_box_value (v : typed_value) : typed_value = let box_ty = mk_box_ty v.ty in diff --git a/src/main.ml b/src/main.ml index d8e9aa40..c6545fcb 100644 --- a/src/main.ml +++ b/src/main.ml @@ -47,7 +47,7 @@ let () = main_log#set_level EL.Debug; interpreter_log#set_level EL.Debug; statements_log#set_level EL.Debug; - expressions_log#set_level EL.Warning; + expressions_log#set_level EL.Debug; expansion_log#set_level EL.Debug; borrows_log#set_level EL.Debug; invariants_log#set_level EL.Warning; |