diff options
| -rw-r--r-- | src/Contexts.ml | 20 | ||||
| -rw-r--r-- | src/Interpreter.ml | 316 | ||||
| -rw-r--r-- | tests/trace_reference.txt | 1066 |
3 files changed, 163 insertions, 1239 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 0dc18952..001ebf19 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -244,3 +244,23 @@ class ['self] map_frame_concrete = let env = self#visit_env acc env in em :: env end + +(** Visitor to iterate over the values in a context *) +class ['self] iter_eval_ctx = + object (self : 'self) + inherit [_] iter_env as super + + method visit_eval_ctx : 'acc -> eval_ctx -> unit = + fun acc ctx -> super#visit_env acc ctx.env + end + +(** Visitor to map the values in a context *) +class ['self] map_eval_ctx = + object (self : 'self) + inherit [_] map_env as super + + method visit_eval_ctx : 'acc -> eval_ctx -> eval_ctx = + fun acc ctx -> + let env = super#visit_env acc ctx.env in + { ctx with env } + end diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b3fcc9f5..9634067d 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -176,8 +176,8 @@ let loans_in_value (v : V.typed_value) : bool = TODO: group abs_or_var_id and g_loan_content. *) -let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - (abs_or_var_id * g_loan_content) option = +let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) + (ctx : C.eval_ctx) : (abs_or_var_id * 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 *) @@ -185,7 +185,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : let obj = object - inherit [_] C.iter_env as super + inherit [_] C.iter_eval_ctx as super method! visit_borrow_content env bc = match bc with @@ -258,7 +258,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : in (* We use exceptions *) try - obj#visit_env () env; + obj#visit_eval_ctx () ctx; None with FoundGLoanContent lc -> ( match !abs_or_var with @@ -270,9 +270,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : The loan is referred to by a borrow id. Raises an exception if no loan was found. *) -let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : +let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) : abs_or_var_id * g_loan_content = - match lookup_loan_opt ek l env with + match lookup_loan_opt ek l ctx with | None -> failwith "Unreachable" | Some res -> res @@ -283,7 +283,7 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : This is a helper function: it might break invariants. *) let update_loan (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.loan_content) (env : C.env) : C.env = + (nlc : V.loan_content) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) @@ -296,7 +296,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_borrow_content env bc = match bc with @@ -334,10 +334,10 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) end in - let env = obj#visit_env () env in + let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) assert !r; - env + ctx (** Update a abstraction loan content. @@ -346,7 +346,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) This is a helper function: it might break invariants. *) let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.aloan_content) (env : C.env) : C.env = + (nlc : V.aloan_content) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) @@ -359,7 +359,7 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_aloan_content env lc = match lc with @@ -385,17 +385,17 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) end in - let env = obj#visit_env () env in + let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) assert !r; - env + ctx (** Lookup a borrow content from a borrow id. *) -let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) - : g_borrow_content option = +let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) + (ctx : C.eval_ctx) : g_borrow_content option = let obj = object - inherit [_] C.iter_env as super + inherit [_] C.iter_eval_ctx as super method! visit_borrow_content env bc = match bc with @@ -440,7 +440,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) in (* We use exceptions *) try - obj#visit_env () env; + obj#visit_eval_ctx () ctx; None with FoundGBorrowContent lc -> Some lc @@ -448,9 +448,9 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) Raise an exception if no loan was found *) -let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : - g_borrow_content = - match lookup_borrow_opt ek l env with +let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) + : g_borrow_content = + match lookup_borrow_opt ek l ctx with | None -> failwith "Unreachable" | Some lc -> lc @@ -461,7 +461,7 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : 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 = + (nbc : V.borrow_content) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) @@ -474,7 +474,7 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_borrow_content env bc = match bc with @@ -506,10 +506,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) end in - let env = obj#visit_env () env in + let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) assert !r; - env + ctx (** Update an abstraction borrow content. @@ -518,7 +518,7 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) This is a helper function: it might break invariants. *) let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) - (nbc : V.aborrow_content) (env : C.env) : C.env = + (nbc : V.aborrow_content) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) @@ -531,7 +531,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_aborrow_content env bc = match bc with @@ -549,10 +549,10 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) end in - let env = obj#visit_env () env in + let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) assert !r; - env + ctx (** The following type identifies the relative position of expressions (in particular borrows) in other expressions. @@ -669,6 +669,8 @@ let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) - [ty]: the type with regions which we use for the projection (to map borrows to regions - or to interpret the borrows as belonging to some regions...) + + TODO: we need a context *) let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : V.typed_avalue = @@ -682,6 +684,7 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value) | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv | V.Adt adt, T.Adt (id, regions, tys) -> (* Retrieve the types of the fields *) + (* Explore the field values *) raise Unimplemented | V.Bottom, _ -> failwith "Unreachable" @@ -747,9 +750,10 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value) 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) - (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env) - : (C.env * g_borrow_content option, outer_borrows_or_abs) result = +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 = (* 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 @@ -780,7 +784,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer) (* The environment is used to keep track of the outer loans *) let obj = object - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option) lc = @@ -922,8 +926,8 @@ let end_borrow_get_borrow_in_env (io : inner_outer) in (* Catch the exceptions - raised if there are outer borrows *) try - let env = obj#visit_env (None, None) env in - Ok (env, !replaced_bc) + let ctx = obj#visit_eval_ctx (None, None) ctx in + Ok (ctx, !replaced_bc) with FoundOuter outers -> Error outers (** Auxiliary function to end borrows. See [give_back_in_env]. @@ -936,7 +940,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer) TODO: this was not the case before, so some sanity checks are not useful anymore. *) let give_back_value (config : C.config) (bid : V.BorrowId.id) - (nv : V.typed_value) (env : C.env) : C.env = + (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = @@ -945,7 +949,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) in let obj = object (self) - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_Loan opt_abs lc = match lc with @@ -1034,11 +1038,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) in (* Explore the environment *) - let env = obj#visit_env None env in + let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) assert !replaced; (* Return *) - env + ctx (** Auxiliary function to end borrows. See [give_back_in_env]. @@ -1050,7 +1054,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) abstraction). *) let give_back_avalue (config : C.config) (bid : V.BorrowId.id) - (nv : V.typed_avalue) (env : C.env) : C.env = + (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = @@ -1059,7 +1063,7 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id) in let obj = object (self) - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue = @@ -1123,11 +1127,11 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id) in (* Explore the environment *) - let env = obj#visit_env None env in + let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) assert !replaced; (* Return *) - env + ctx (** Auxiliary function to end borrows. See [give_back_in_env]. @@ -1138,7 +1142,8 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id) we update. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = +let give_back_shared config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : + C.eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = @@ -1147,7 +1152,7 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = in let obj = object (self) - inherit [_] C.map_env as super + inherit [_] C.map_eval_ctx as super method! visit_Loan opt_abs lc = match lc with @@ -1216,11 +1221,11 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = in (* Explore the environment *) - let env = obj#visit_env None env in + let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) assert !replaced; (* Return *) - env + ctx (** When copying values, we duplicate the shared borrows. This is tantamount to reborrowing the shared value. The following function applies this change @@ -1268,8 +1273,8 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) { 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 = +let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) + (ctx : C.eval_ctx) : C.eval_ctx = (* This is used for sanity checks *) let sanity_ek = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -1279,39 +1284,39 @@ let give_back_in_env (config : C.config) (l : V.BorrowId.id) (* Sanity check *) assert (l' = l); (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - (* Update the environment *) - give_back_value config l tv env + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_value config l tv ctx | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - (* Update the environment *) - give_back_shared config l env + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_shared config l ctx | Abstract (V.AMutBorrow (l', av)) -> (* Sanity check *) assert (l' = l); (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - (* Update the environment *) - give_back_avalue config l av env + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_avalue config l av ctx | Abstract (V.ASharedBorrow l') -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l env)); - (* Update the environment *) - give_back_shared config l env + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_shared config l ctx | Abstract (V.AIgnoredSharedBorrow _) -> raise Unimplemented | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable" -(** End a borrow identified by its borrow id in an environment +(** End a borrow identified by its borrow id in a context - 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 + First lookup the borrow in the context and replace it with [Bottom]. + Then, check that there is an associated loan in the context. When moving values, before putting the value in its destination, we get an - intermediate state where some values are "outside" the environment and thus + intermediate state where some values are "outside" the context and thus 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 @@ -1332,15 +1337,15 @@ let give_back_in_env (config : C.config) (l : V.BorrowId.id) 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 + `abs_id` before. In practice, only [end_borrow] 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 + if you look ath the implementation details, `end_borrow` 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) - (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 +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 = + match end_borrow_get_borrow io allowed_abs l ctx with (* Two cases: * - error: we found outer borrows (end them first) * - success: we didn't find outer borrows when updating (but maybe we actually @@ -1359,16 +1364,16 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer) * be trying to end a borrow inside an abstraction, but which is actually * inside another borrow *) let allowed_abs' = None in - let env = end_borrows_in_env config io allowed_abs' bids env in + let ctx = end_borrows config io allowed_abs' bids ctx in (* Retry to end the borrow *) - end_borrow_in_env config io allowed_abs l env + end_borrow config io allowed_abs l ctx | OuterBorrows (Borrow bid) -> (* See the comments for the previous case *) assert (io = Outer); let allowed_abs' = None in - let env = end_borrow_in_env config io allowed_abs' bid env in + let ctx = end_borrow config io allowed_abs' bid ctx in (* Retry to end the borrow *) - end_borrow_in_env config io allowed_abs l env + end_borrow config io allowed_abs l 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 @@ -1382,81 +1387,47 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer) enter_abs = true; } in - match lookup_loan ek l env with + 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 env = end_borrow_in_env config io (Some abs_id) l env in + let ctx = end_borrow config io (Some abs_id) l ctx in (* Sanity check *) - assert (Option.is_none (lookup_borrow_opt ek l env)); - env) + 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 env = end_abstraction_in_env config abs_id env in + 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 env)); - env + 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 env = end_abstraction_in_env config abs_id env in + 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 env)); - env)) - | Ok (env, None) -> + assert (Option.is_none (lookup_borrow_opt ek l ctx)); + ctx)) + | Ok (ctx, 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 + ctx (* We found a borrow: give the value back (i.e., update the corresponding loan) *) - | Ok (env, Some bc) -> give_back_in_env config l bc env + | Ok (ctx, Some bc) -> give_back config l bc ctx -and end_borrows_in_env (config : C.config) (io : inner_outer) +and end_borrows (config : C.config) (io : inner_outer) (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 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) - (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 allowed_abs l ctx.env in - let ctx = { ctx with env } in - L.log#ldebug - (lazy - ("end_borrow " ^ V.BorrowId.to_string l ^ ": context after:\n" - ^ eval_ctx_to_string ctx)); - ctx + V.BorrowId.Set.fold + (fun id ctx -> end_borrow config io allowed_abs id ctx) + lset ctx -(** Same as [end_borrows_in_env], but operating on evaluation contexts *) -let end_borrows (config : C.config) (io : inner_outer) - (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) +and end_abstraction (config : C.config) (abs : V.AbstractionId.id) (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 allowed_abs lset ctx.env in - let ctx = { ctx with env } in - L.log#ldebug - (lazy - ("end_borrows " - ^ V.BorrowId.set_to_string lset - ^ ": context after:\n" ^ eval_ctx_to_string ctx)); - ctx + raise Unimplemented let end_outer_borrow config = end_borrow config Outer None @@ -1486,7 +1457,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx.env with + match lookup_loan ek l ctx with | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan, found a mut loan" | _, Concrete (V.SharedLoan (bids, sv)) -> @@ -1501,8 +1472,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : (* Check there aren't inactivated borrows *) assert (not (inactivated_in_value sv)); (* Update the loan content *) - let env = update_loan ek l (V.MutLoan l) ctx.env in - let ctx = { ctx with env } in + let ctx = update_loan ek l (V.MutLoan l) ctx in (* Return *) (ctx, sv) | _, Abstract _ -> raise Unimplemented @@ -1519,13 +1489,12 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) let ek = { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in - match lookup_borrow ek l ctx.env with + match lookup_borrow ek l ctx with | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> failwith "Expected an inactivated mutable borrow" | Concrete (V.InactivatedMutBorrow _) -> (* Update it *) - let env = update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx.env in - { ctx with env } + update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx | Abstract _ -> raise Unimplemented (** Promote an inactivated mut borrow to a mut borrow. @@ -1538,7 +1507,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx.env with + match lookup_loan ek l ctx with | _, 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 @@ -1626,10 +1595,10 @@ type projection_access = { We return the (eventually) updated value, the value we read at the end of the place and the (eventually) updated environment. *) -let rec access_projection (access : projection_access) (env : C.env) +let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Function to (eventually) update the value we find *) (update : V.typed_value -> V.typed_value) (p : E.projection) - (v : V.typed_value) : (C.env * updated_read_value) path_access_result = + (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result = (* For looking up/updating shared loans *) let ek : exploration_kind = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -1646,7 +1615,7 @@ let rec access_projection (access : projection_access) (env : C.env) failwith "Assertion failed: new value doesn't have the same type as its \ destination"); - Ok (env, { read = v; updated = nv }) + Ok (ctx, { read = v; updated = nv }) | pe :: p' -> ( (* Match on the projection element and the value *) match (pe, v.V.value, v.V.ty) with @@ -1662,31 +1631,31 @@ let rec access_projection (access : projection_access) (env : C.env) | _ -> failwith "Unreachable"); (* Actually project *) let fv = T.FieldId.nth adt.field_values field_id in - match access_projection access env update p' fv with + match access_projection access ctx update p' fv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> (* Update the field value *) let nvalues = T.FieldId.update_nth adt.field_values field_id res.updated in let nadt = V.Adt { adt with V.field_values = nvalues } in let updated = { v with value = nadt } in - Ok (env, { res with updated })) + Ok (ctx, { res with updated })) (* Tuples *) | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( assert (arity = List.length adt.field_values); let fv = T.FieldId.nth adt.field_values field_id in (* Project *) - match access_projection access env update p' fv with + match access_projection access ctx update p' fv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> (* Update the field value *) let nvalues = T.FieldId.update_nth adt.field_values field_id res.updated in let ntuple = V.Adt { adt with field_values = nvalues } in let updated = { v with value = ntuple } in - Ok (env, { res with updated }) + Ok (ctx, { res with updated }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *)) | Field (ProjAdt (_, _), _), V.Bottom, _ -> @@ -1706,9 +1675,9 @@ let rec access_projection (access : projection_access) (env : C.env) * it shouldn't happen due to user code, and we leverage it * when implementing box dereferencement for the concrete * interpreter *) - match access_projection access env update p' bv with + match access_projection access ctx update p' bv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> let nv = { v with @@ -1716,44 +1685,44 @@ let rec access_projection (access : projection_access) (env : C.env) V.Adt { variant_id = None; field_values = [ res.updated ] }; } in - Ok (env, { res with updated = nv })) + Ok (ctx, { res with updated = nv })) (* Borrows *) | Deref, V.Borrow bc, _ -> ( match bc with | V.SharedBorrow bid -> (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then - match lookup_loan ek bid env with + match lookup_loan ek bid ctx with | _, 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 + match access_projection access ctx update p' sv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> (* Update the shared loan with the new value returned by [access_projection] *) - let env = + let ctx = update_loan ek bid (V.SharedLoan (bids, res.updated)) - env + ctx in (* Return - note that we don't need to update the borrow itself *) - Ok (env, { res with updated = v })) + Ok (ctx, { res with updated = v })) | _, Abstract _ -> raise Unimplemented else Error (FailBorrow bc) | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) | V.MutBorrow (bid, bv) -> if access.enter_mut_borrows then - match access_projection access env update p' bv with + match access_projection access ctx update p' bv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> let nv = { v with value = V.Borrow (V.MutBorrow (bid, res.updated)); } in - Ok (env, { res with updated = nv }) + Ok (ctx, { res with updated = nv }) else Error (FailBorrow bc)) | _, V.Loan lc, _ -> ( match lc with @@ -1763,16 +1732,16 @@ let rec access_projection (access : projection_access) (env : C.env) to the fact that we need to reexplore the *whole* place (i.e, we mustn't ignore the current projection element *) if access.enter_shared_loans then - match access_projection access env update (pe :: p') sv with + match access_projection access ctx update (pe :: p') sv with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> let nv = { v with value = V.Loan (V.SharedLoan (bids, res.updated)); } in - Ok (env, { res with updated = nv }) + Ok (ctx, { res with updated = nv }) else Error (FailSharedLoan bids)) | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> let pe, v, ty = r in @@ -1790,18 +1759,18 @@ let rec access_projection (access : projection_access) (env : C.env) *) let access_place (access : projection_access) (* Function to (eventually) update the value we find *) - (update : V.typed_value -> V.typed_value) (p : E.place) (env : C.env) : - (C.env * V.typed_value) path_access_result = + (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx) + : (C.eval_ctx * V.typed_value) path_access_result = (* Lookup the variable's value *) - let value = C.env_lookup_var_value env p.var_id in + let value = C.ctx_lookup_var_value ctx p.var_id in (* Apply the projection *) - match access_projection access env update p.projection value with + match access_projection access ctx update p.projection value with | Error err -> Error err - | Ok (env, res) -> + | Ok (ctx, res) -> (* Update the value *) - let env = C.env_update_var_value env p.var_id res.updated in + let ctx = C.ctx_update_var_value ctx p.var_id res.updated in (* Return *) - Ok (env, res.read) + Ok (ctx, res.read) type access_kind = | Read (** We can go inside borrows and loans *) @@ -1836,17 +1805,18 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) let access = access_kind_to_projection_access access in (* The update function is the identity *) let update v = v in - match access_place access update p ctx.env with + match access_place access update p ctx with | Error err -> Error err - | Ok (env1, read_value) -> + | Ok (ctx1, read_value) -> (* Note that we ignore the new environment: it should be the same as the original one. *) if config.check_invariants then - if env1 <> ctx.env then ( + if ctx1 <> ctx then ( let msg = "Unexpected environment update:\nNew environment:\n" - ^ C.show_env env1 ^ "\n\nOld environment:\n" ^ C.show_env ctx.env + ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" + ^ C.show_env ctx.env in L.log#serror msg; failwith "Unexpected environment update"); @@ -1864,11 +1834,11 @@ let write_place (_config : C.config) (access : access_kind) (p : E.place) let access = access_kind_to_projection_access access in (* The update function substitutes the value with the new value *) let update _ = nv in - match access_place access update p ctx.env with + match access_place access update p ctx with | Error err -> Error err - | Ok (env, _) -> + | Ok (ctx, _) -> (* We ignore the read value *) - Ok { ctx with env } + Ok ctx let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = diff --git a/tests/trace_reference.txt b/tests/trace_reference.txt index f69eff48..4328c2c0 100644 --- a/tests/trace_reference.txt +++ b/tests/trace_reference.txt @@ -3952,34 +3952,6 @@ About to evaluate statement: var@6 := copy x - op: copy x -[[32mDebug[39m] end_borrow 0: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⌊mut@1⌋ ; - ppx -> &mut@1 (&mut@0 (1: i32)) ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 0: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 1: i32 ; - px -> ⌊mut@1⌋ ; - ppx -> &mut@1 (⊥ : &'_ mut (i32)) ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 1: i32 [[32mDebug[39m] @@ -4817,58 +4789,6 @@ move var@6 [[32mDebug[39m] Value to move: &mut@3 (1: i32) -[[32mDebug[39m] end_borrow 0: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@1⌋ ; - px -> ⌊mut@2⌋ ; - py -> &mut@1 (⌊mut@3⌋) ; - ppx -> &mut@2 (&mut@0 (0: i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 0: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> ⌊mut@2⌋ ; - py -> &mut@1 (⌊mut@3⌋) ; - ppx -> &mut@2 (⊥ : &'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] # 1 frame(s) @@ -5076,58 +4996,6 @@ About to evaluate statement: var@9 := copy *(px) - op: copy *(px) -[[32mDebug[39m] end_borrow 2: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> ⌊mut@2⌋ ; - py -> &mut@1 (⌊mut@3⌋) ; - ppx -> &mut@2 (&mut@3 (2: i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 2: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> &mut@3 (2: i32) ; - py -> &mut@1 (⌊mut@3⌋) ; - ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 2: i32 [[32mDebug[39m] @@ -5994,58 +5862,6 @@ About to evaluate statement: var@15 := copy *(py) - op: copy *(py) -[[32mDebug[39m] end_borrow 3: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> &mut@3 (2: i32) ; - py -> &mut@1 (⌊mut@3⌋) ; - ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 3: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> ⊥ : &'_ mut (i32) ; - py -> &mut@1 (2: i32) ; - ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 2: i32 [[32mDebug[39m] @@ -6455,58 +6271,6 @@ About to evaluate statement: var@18 := copy y - op: copy y -[[32mDebug[39m] end_borrow 1: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> ⌊mut@1⌋ ; - px -> ⊥ : &'_ mut (i32) ; - py -> &mut@1 (2: i32) ; - ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 1: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: i32 ; - y -> 2: i32 ; - px -> ⊥ : &'_ mut (i32) ; - py -> ⊥ : &'_ mut (i32) ; - ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : bool ; - var@9 -> ⊥ : i32 ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 2: i32 [[32mDebug[39m] @@ -7485,38 +7249,6 @@ move var@3 }); ty = (Types.Adt ((Types.Assumed Types.Box), [], [(Types.Integer Types.I32)])) } -[[32mDebug[39m] end_borrows {}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @shared_loan({0}, @Box(0: i32)) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⌊inactivated_mut@0⌋ ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrows {}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @shared_loan({0}, @Box(0: i32)) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⌊inactivated_mut@0⌋ ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to move: &mut@0 (@Box(0: i32)) [[32mDebug[39m] ctx_pop_frame: @@ -7543,50 +7275,6 @@ move var@3 [[32mDebug[39m] ctx_pop_frame: locals to drop: [1] [[32mDebug[39m] drop_value: place: var@1 -[[32mDebug[39m] end_borrow 0: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> ⌊mut@0⌋ ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -# Frame 1: -{ - @return -> &mut@1 (0: i32) ; - var@1 -> &mut@0 (@Box(⌊mut@1⌋)) ; -} - -[[32mDebug[39m] end_borrow 0: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(⌊mut@1⌋) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -# Frame 1: -{ - @return -> &mut@1 (0: i32) ; - var@1 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; -} - [[32mDebug[39m] ctx_pop_frame: after dropping local variables: # 2 frame(s) @@ -7746,38 +7434,6 @@ return About to evaluate statement: var@5 := &b -[[32mDebug[39m] end_borrow 1: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(⌊mut@1⌋) ; - x -> &mut@1 (1: i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 1: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(1: i32) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - [[32mDebug[39m] # 1 frame(s) @@ -7872,50 +7528,6 @@ move var@5 [[32mDebug[39m] ctx_pop_frame: locals to drop: [1] [[32mDebug[39m] drop_value: place: var@1 -[[32mDebug[39m] end_borrow 2: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @shared_loan({2}, @Box(@shared_loan({3}, 1: i32))) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -# Frame 1: -{ - @return -> ⌊shared@3⌋ ; - var@1 -> ⌊shared@2⌋ ; -} - -[[32mDebug[39m] end_borrow 2: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(@shared_loan({3}, 1: i32)) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -# Frame 1: -{ - @return -> ⌊shared@3⌋ ; - var@1 -> ⊥ : &'_ (std::boxed::Box<i32>) ; -} - [[32mDebug[39m] ctx_pop_frame: after dropping local variables: # 2 frame(s) @@ -8276,38 +7888,6 @@ return About to evaluate statement: drop(b) [[32mDebug[39m] drop_value: place: b -[[32mDebug[39m] end_borrows {3}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(@shared_loan({3}, 1: i32)) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⌊shared@3⌋ ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrows {3}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - b -> @Box(1: i32) ; - x -> ⊥ : &'_ mut (i32) ; - var@3 -> ⊥ : &'_ mut (std::boxed::Box<i32>) ; - x -> ⊥ : &'_ (i32) ; - var@5 -> ⊥ : &'_ (std::boxed::Box<i32>) ; - var@6 -> ⊥ : bool ; - var@7 -> ⊥ : bool ; - var@8 -> ⊥ : i32 ; -} - [[32mDebug[39m] # 1 frame(s) @@ -9903,50 +9483,6 @@ About to evaluate statement: return [[32mDebug[39m] ctx_pop_frame: locals to drop: [2,1] [[32mDebug[39m] drop_value: place: var@2 [[32mDebug[39m] drop_value: place: l -[[32mDebug[39m] end_borrow 1: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - l -> @shared_loan({0, 1}, test1::List::Cons { 0 = 0: i32; 1 = @Box(test1::List::Nil); }) ; - var@2 -> ⊥ : std::boxed::Box<test1::List<i32>> ; - var@3 -> ⊥ : test1::List<i32> ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : &'_ (test1::List<i32>) ; - var@7 -> ⌊shared@0⌋ ; -} - -# Frame 1: -{ - var@0 -> true ; - l -> ⌊shared@1⌋ ; - var@2 -> ⊥ : isize ; -} - -[[32mDebug[39m] end_borrow 1: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - l -> @shared_loan({0}, test1::List::Cons { 0 = 0: i32; 1 = @Box(test1::List::Nil); }) ; - var@2 -> ⊥ : std::boxed::Box<test1::List<i32>> ; - var@3 -> ⊥ : test1::List<i32> ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : &'_ (test1::List<i32>) ; - var@7 -> ⌊shared@0⌋ ; -} - -# Frame 1: -{ - var@0 -> true ; - l -> ⊥ : &'_ (test1::List<i32>) ; - var@2 -> ⊥ : isize ; -} - [[32mDebug[39m] ctx_pop_frame: after dropping local variables: # 2 frame(s) @@ -10151,36 +9687,6 @@ return About to evaluate statement: drop(l) [[32mDebug[39m] drop_value: place: l -[[32mDebug[39m] end_borrows {0}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - l -> @shared_loan({0}, test1::List::Cons { 0 = 0: i32; 1 = @Box(test1::List::Nil); }) ; - var@2 -> ⊥ : std::boxed::Box<test1::List<i32>> ; - var@3 -> ⊥ : test1::List<i32> ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : &'_ (test1::List<i32>) ; - var@7 -> ⌊shared@0⌋ ; -} - -[[32mDebug[39m] end_borrows {0}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - l -> test1::List::Cons { 0 = 0: i32; 1 = @Box(test1::List::Nil); } ; - var@2 -> ⊥ : std::boxed::Box<test1::List<i32>> ; - var@3 -> ⊥ : test1::List<i32> ; - var@4 -> ⊥ : bool ; - var@5 -> ⊥ : bool ; - var@6 -> ⊥ : &'_ (test1::List<i32>) ; - var@7 -> ⊥ : &'_ (test1::List<i32>) ; -} - [[32mDebug[39m] # 1 frame(s) @@ -13791,58 +13297,6 @@ move var@4 { Values.value = (Values.Concrete (Values.Scalar { Values.value = 0; int_ty = Types.I32 })); ty = (Types.Integer Types.I32) } -[[32mDebug[39m] end_borrows {}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⌊inactivated_mut@1⌋ ; - var@5 -> &mut@0 (@shared_loan({1}, 0: i32)) ; - var@6 -> ⌊inactivated_mut@3⌋ ; - var@7 -> &mut@2 (@shared_loan({3}, 0: i32)) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrows {}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⌊inactivated_mut@1⌋ ; - var@5 -> &mut@0 (@shared_loan({1}, 0: i32)) ; - var@6 -> ⌊inactivated_mut@3⌋ ; - var@7 -> &mut@2 (@shared_loan({3}, 0: i32)) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to move: &mut@1 (0: i32) [[32mDebug[39m] eval_operand: @@ -13880,58 +13334,6 @@ move var@6 { Values.value = (Values.Concrete (Values.Scalar { Values.value = 0; int_ty = Types.I32 })); ty = (Types.Integer Types.I32) } -[[32mDebug[39m] end_borrows {}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@1⌋) ; - var@6 -> ⌊inactivated_mut@3⌋ ; - var@7 -> &mut@2 (@shared_loan({3}, 0: i32)) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrows {}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@1⌋) ; - var@6 -> ⌊inactivated_mut@3⌋ ; - var@7 -> &mut@2 (@shared_loan({3}, 0: i32)) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to move: &mut@3 (0: i32) [[32mDebug[39m] @@ -14296,147 +13698,7 @@ About to evaluate statement: return [[32mDebug[39m] ctx_pop_frame: locals to drop: [4,3,2,1] [[32mDebug[39m] drop_value: place: var@4 [[32mDebug[39m] drop_value: place: y -[[32mDebug[39m] end_borrow 3: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@1⌋) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (⌊mut@3⌋) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -# Frame 1: -{ - var@0 -> &mut@4 (0: i32) ; - b -> true ; - x -> &mut@1 (⌊mut@4⌋) ; - y -> &mut@3 (0: i32) ; - var@4 -> ⊥ : bool ; -} - -[[32mDebug[39m] end_borrow 3: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@1⌋) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -# Frame 1: -{ - var@0 -> &mut@4 (0: i32) ; - b -> true ; - x -> &mut@1 (⌊mut@4⌋) ; - y -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : bool ; -} - [[32mDebug[39m] drop_value: place: x -[[32mDebug[39m] end_borrow 1: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@1⌋) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -# Frame 1: -{ - var@0 -> &mut@4 (0: i32) ; - b -> true ; - x -> &mut@1 (⌊mut@4⌋) ; - y -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : bool ; -} - -[[32mDebug[39m] end_borrow 1: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@4⌋) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> ⊥ : i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -# Frame 1: -{ - var@0 -> &mut@4 (0: i32) ; - b -> true ; - x -> ⊥ : &'_ mut (i32) ; - y -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : bool ; -} - [[32mDebug[39m] drop_value: place: b [[32mDebug[39m] ctx_pop_frame: after dropping local variables: # 2 frame(s) @@ -15275,110 +14537,6 @@ About to evaluate statement: var@15 := copy x - op: copy x -[[32mDebug[39m] end_borrow 0: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - y -> ⌊mut@2⌋ ; - z -> &mut@4 (1: i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> &mut@0 (⌊mut@4⌋) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 0: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@4⌋ ; - y -> ⌊mut@2⌋ ; - z -> &mut@4 (1: i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> ⊥ : &'_ mut (i32) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 4: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@4⌋ ; - y -> ⌊mut@2⌋ ; - z -> &mut@4 (1: i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> ⊥ : &'_ mut (i32) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 4: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 1: i32 ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> ⊥ : &'_ mut (i32) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 1: i32 [[32mDebug[39m] @@ -15788,58 +14946,6 @@ About to evaluate statement: var@18 := copy y - op: copy y -[[32mDebug[39m] end_borrow 2: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 1: i32 ; - y -> ⌊mut@2⌋ ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> ⊥ : &'_ mut (i32) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> &mut@2 (0: i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - -[[32mDebug[39m] end_borrow 2: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 1: i32 ; - y -> 0: i32 ; - z -> ⊥ : &'_ mut (i32) ; - var@4 -> ⊥ : &'_ mut (i32) ; - var@5 -> ⊥ : &'_ mut (i32) ; - var@6 -> ⊥ : &'_ mut (i32) ; - var@7 -> ⊥ : &'_ mut (i32) ; - var@8 -> 0: i32 ; - var@9 -> ⊥ : (i32, bool) ; - var@10 -> ⊥ : bool ; - var@11 -> ⊥ : bool ; - var@12 -> ⊥ : i32 ; - var@13 -> ⊥ : bool ; - var@14 -> ⊥ : bool ; - var@15 -> ⊥ : i32 ; - var@16 -> ⊥ : bool ; - var@17 -> ⊥ : bool ; - var@18 -> ⊥ : i32 ; -} - [[32mDebug[39m] Value to copy: 0: i32 [[32mDebug[39m] @@ -16723,42 +15829,6 @@ move var@7 (Types.Integer Types.U32)] )) } -[[32mDebug[39m] end_borrows {}: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (@shared_loan({2}, (&mut@0 (0: u32), 1: u32))) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⌊inactivated_mut@2⌋ ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - -[[32mDebug[39m] end_borrows {}: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (@shared_loan({2}, (&mut@0 (0: u32), 1: u32))) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⌊inactivated_mut@2⌋ ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - [[32mDebug[39m] Value to move: &mut@2 ((&mut@0 (0: u32), 1: u32)) [[32mDebug[39m] @@ -16926,107 +15996,7 @@ About to evaluate statement: return [[32mDebug[39m] ctx_pop_frame: locals to drop: [2,1] [[32mDebug[39m] drop_value: place: var@2 -[[32mDebug[39m] end_borrow 3: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@2⌋) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - -# Frame 1: -{ - var@0 -> &mut@4 ((&mut@0 (0: u32), 1: u32)) ; - x -> &mut@2 (⌊mut@3⌋) ; - var@2 -> &mut@3 (⌊mut@4⌋) ; -} - -[[32mDebug[39m] end_borrow 3: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@2⌋) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - -# Frame 1: -{ - var@0 -> &mut@4 ((&mut@0 (0: u32), 1: u32)) ; - x -> &mut@2 (⌊mut@4⌋) ; - var@2 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; -} - [[32mDebug[39m] drop_value: place: x -[[32mDebug[39m] end_borrow 2: context before: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@2⌋) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - -# Frame 1: -{ - var@0 -> &mut@4 ((&mut@0 (0: u32), 1: u32)) ; - x -> &mut@2 (⌊mut@4⌋) ; - var@2 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; -} - -[[32mDebug[39m] end_borrow 2: context after: -# 2 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@4⌋) ; - pp1 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⊥ : u32 ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> ⊥ : &'_ mut (u32) ; -} - -# Frame 1: -{ - var@0 -> &mut@4 ((&mut@0 (0: u32), 1: u32)) ; - x -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - var@2 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; -} - [[32mDebug[39m] ctx_pop_frame: after dropping local variables: # 2 frame(s) @@ -17306,42 +16276,6 @@ move var@9 [[32mDebug[39m] Value to move: &mut@6 (2: u32) -[[32mDebug[39m] end_borrow 0: context before: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> ⌊mut@0⌋ ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@4⌋) ; - pp1 -> &mut@4 ((&mut@0 (0: u32), 1: u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⌊mut@5⌋ ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> &mut@5 (⌊mut@6⌋) ; -} - -[[32mDebug[39m] end_borrow 0: context after: -# 1 frame(s) - -# Frame 0: -{ - var@0 -> ⊥ : () ; - x -> 0: u32 ; - px -> ⊥ : &'_ mut (u32) ; - p -> ⌊mut@1⌋ ; - var@4 -> ⊥ : &'_ mut (u32) ; - pp0 -> &mut@1 (⌊mut@4⌋) ; - pp1 -> &mut@4 ((⊥ : &'_ mut (u32), 1: u32)) ; - var@7 -> ⊥ : &'_ mut ((&'_ mut (u32), u32)) ; - y -> ⌊mut@5⌋ ; - var@9 -> ⊥ : &'_ mut (u32) ; - var@10 -> &mut@5 (⌊mut@6⌋) ; -} - [[32mDebug[39m] # 1 frame(s) |