summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-17 16:55:55 +0100
committerSon Ho2021-12-17 16:55:55 +0100
commite1c7e68a476f65ec8c0b4d7c02a2dea09b2a4522 (patch)
treeda5bf4925c410d7449fe24e266cc3c2c97d8ce1b
parent644f91b355de4c80b882625e476cc5ee6b86d696 (diff)
Use eval_ctx instead of env in many functions of the interpreter
-rw-r--r--src/Contexts.ml20
-rw-r--r--src/Interpreter.ml316
-rw-r--r--tests/trace_reference.txt1066
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
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
1: i32
[Debug]
@@ -4817,58 +4789,6 @@ move var@6
[Debug] Value to move:
&mut@3 (1: i32)
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug]
# 1 frame(s)
@@ -5076,58 +4996,6 @@ About to evaluate statement: var@9 := copy *(px)
- op:
copy *(px)
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
2: i32
[Debug]
@@ -5994,58 +5862,6 @@ About to evaluate statement: var@15 := copy *(py)
- op:
copy *(py)
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
2: i32
[Debug]
@@ -6455,58 +6271,6 @@ About to evaluate statement: var@18 := copy y
- op:
copy y
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
2: i32
[Debug]
@@ -7485,38 +7249,6 @@ move var@3
});
ty =
(Types.Adt ((Types.Assumed Types.Box), [], [(Types.Integer Types.I32)])) }
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to move:
&mut@0 (@Box(0: i32))
[Debug] ctx_pop_frame:
@@ -7543,50 +7275,6 @@ move var@3
[Debug] ctx_pop_frame: locals to drop: [1]
[Debug] drop_value: place: var@1
-[Debug] 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⌋)) ;
-}
-
-[Debug] 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>) ;
-}
-
[Debug] ctx_pop_frame: after dropping local variables:
# 2 frame(s)
@@ -7746,38 +7434,6 @@ return
About to evaluate statement: var@5 := &b
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug]
# 1 frame(s)
@@ -7872,50 +7528,6 @@ move var@5
[Debug] ctx_pop_frame: locals to drop: [1]
[Debug] drop_value: place: var@1
-[Debug] 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⌋ ;
-}
-
-[Debug] 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>) ;
-}
-
[Debug] ctx_pop_frame: after dropping local variables:
# 2 frame(s)
@@ -8276,38 +7888,6 @@ return
About to evaluate statement: drop(b)
[Debug] drop_value: place: b
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug]
# 1 frame(s)
@@ -9903,50 +9483,6 @@ About to evaluate statement: return
[Debug] ctx_pop_frame: locals to drop: [2,1]
[Debug] drop_value: place: var@2
[Debug] drop_value: place: l
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] ctx_pop_frame: after dropping local variables:
# 2 frame(s)
@@ -10151,36 +9687,6 @@ return
About to evaluate statement: drop(l)
[Debug] drop_value: place: l
-[Debug] 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⌋ ;
-}
-
-[Debug] 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>) ;
-}
-
[Debug]
# 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) }
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to move:
&mut@1 (0: i32)
[Debug] 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) }
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to move:
&mut@3 (0: i32)
[Debug]
@@ -14296,147 +13698,7 @@ About to evaluate statement: return
[Debug] ctx_pop_frame: locals to drop: [4,3,2,1]
[Debug] drop_value: place: var@4
[Debug] drop_value: place: y
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] drop_value: place: x
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] drop_value: place: b
[Debug] 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
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
1: i32
[Debug]
@@ -15788,58 +14946,6 @@ About to evaluate statement: var@18 := copy y
- op:
copy y
-[Debug] 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 ;
-}
-
-[Debug] 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 ;
-}
-
[Debug] Value to copy:
0: i32
[Debug]
@@ -16723,42 +15829,6 @@ move var@7
(Types.Integer Types.U32)]
))
}
-[Debug] 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) ;
-}
-
-[Debug] 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) ;
-}
-
[Debug] Value to move:
&mut@2 ((&mut@0 (0: u32), 1: u32))
[Debug]
@@ -16926,107 +15996,7 @@ About to evaluate statement: return
[Debug] ctx_pop_frame: locals to drop: [2,1]
[Debug] drop_value: place: var@2
-[Debug] 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⌋) ;
-}
-
-[Debug] 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)) ;
-}
-
[Debug] drop_value: place: x
-[Debug] 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)) ;
-}
-
-[Debug] 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)) ;
-}
-
[Debug] ctx_pop_frame: after dropping local variables:
# 2 frame(s)
@@ -17306,42 +16276,6 @@ move var@9
[Debug] Value to move:
&mut@6 (2: u32)
-[Debug] 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⌋) ;
-}
-
-[Debug] 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⌋) ;
-}
-
[Debug]
# 1 frame(s)