Make more updates to assignment and update ctx_pop_frame

3 files changed, 67 insertions, 9 deletions

diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 1f7135a5..e1c80d89 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -642,9 +642,13 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
   let ctx = drop ctx in
   (* Pop the temporary value *)
   let ctx, v = C.ctx_pop_dummy_var ctx in
+  (* Reinsert the value *)
+  let ctx = write_place_unwrap config access p v ctx in
   (* Sanity check *)
-  assert (not (loans_in_value v));
-  assert (not (borrows_in_value v));
+  if end_borrows then (
+    assert (not (loans_in_value v));
+    assert (not (borrows_in_value v)))
+  else assert (not (outer_loans_in_value v));
   (* Return *)
   ctx
 
@@ -718,7 +722,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
 (** Small utility.
     
     Prepare a place which is to be used as the destination of an assignment:
-    update the environment along the paths, end  loans at this place, etc.
+    update the environment along the paths, end the loans at this place, etc.
 
     Return the updated context and the (updated) value at the end of the
     place. This value should not contain any loan or borrow (and we check
@@ -738,8 +742,10 @@ let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
   (* Read the value and check it *)
   let v = read_place_unwrap config access p ctx in
   (* Sanity checks *)
-  assert (not (loans_in_value v));
-  assert (not (borrows_in_value v));
+  if end_borrows then (
+    assert (not (loans_in_value v));
+    assert (not (borrows_in_value v)))
+  else assert (not (outer_loans_in_value v));
   (* Return *)
   (ctx, v)
 
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index de904262..d172d1b7 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -51,8 +51,12 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
   let ctx, v = C.ctx_pop_dummy_var ctx in
   (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
   assert (not (bottom_in_value ctx.ended_regions v));
+  (* Move the value at destination to a dummy variable *)
+  let mv = read_place_unwrap config Write p ctx in
+  let ctx = C.ctx_push_dummy_var ctx mv in
   (* Update the destination *)
   let ctx = write_place_unwrap config Write p v ctx in
+  (* Return *)
   ctx
 
 (** Evaluates an assertion.
@@ -193,11 +197,41 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   in
   (* Sanity check *)
   assert (not (bottom_in_value ctx.ended_regions ret_value));
-  (* We musn't drop the local variables (because otherwise we might end
-   * some borrows in the return value!) but must reintroduce them instead
-   * in the context as dummy variables. *)
+  (* List the local variables, but the return variable *)
+  let rec list_locals env =
+    match env with
+    | [] -> failwith "Inconsistent environment"
+    | C.Abs _ :: env -> list_locals env
+    | C.Var (None, _) :: env -> list_locals env
+    | C.Var (Some var, _) :: env ->
+        let locals = list_locals env in
+        if var.index <> ret_vid then var.index :: locals else locals
+    | C.Frame :: _ -> []
+  in
+  let locals = list_locals ctx.env in
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("ctx_pop_frame: locals in which to drop the outer loans: ["
+      ^ String.concat "," (List.map V.VarId.to_string locals)
+      ^ "]"));
+  (* Drop the outer *loans* in the local variables *)
+  let ctx =
+    let end_borrows = false in
+    List.fold_left
+      (fun ctx lid ->
+        drop_outer_borrows_loans_at_lplace config end_borrows
+          (mk_place_from_var_id lid) ctx)
+      ctx locals
+  in
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("ctx_pop_frame: after dropping outer loans in local variables:\n"
+     ^ eval_ctx_to_string ctx));
   (* Pop the frame - we remove the `Frame` delimiter, and reintroduce all
-   * the local variables as dummy variables in the caller frame *)
+   * the local variables (which may still contain borrow permissions - but
+   * no outer loans - as dummy variables in the caller frame *)
   let rec pop env =
     match env with
     | [] -> failwith "Inconsistent environment"
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 16c94800..f90a98ef 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -60,3 +60,21 @@ let loans_in_value (v : typed_value) : bool =
     obj#visit_typed_value () v;
     false
   with Found -> true
+
+(** Check if a value contains outer loans (i.e., loans which are not in borrwed
+    values. *)
+let outer_loans_in_value (v : typed_value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+
+      method! visit_loan_content _env _ = raise Found
+
+      method! visit_borrow_content _ _ = ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true