diff options
Diffstat (limited to 'src')
| -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 |
9 files changed, 288 insertions, 191 deletions
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; |