From a3c3cd9b75dc891af9171a0ca4e01b02e53e638a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jan 2022 20:28:28 +0100
Subject: Update ctx_pop_frame to not drop the local variables

---
 src/InterpreterStatements.ml | 40 +++++++---------------------------------
 1 file changed, 7 insertions(+), 33 deletions(-)

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index cda682a3..3bf9e7a4 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -185,47 +185,21 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
   (* Eval *)
   let ret_vid = V.VarId.zero in
-  (* 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 (var, _) :: env ->
-        (* There shouldn't be dummy variables *)
-        let var = Option.get var in
-        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 to drop: ["
-      ^ String.concat "," (List.map V.VarId.to_string locals)
-      ^ "]"));
-  (* Drop the local variables *)
-  let ctx =
-    List.fold_left
-      (fun ctx lid -> drop_value config ctx (mk_place_from_var_id lid))
-      ctx locals
-  in
-  (* Debug *)
-  log#ldebug
-    (lazy
-      ("ctx_pop_frame: after dropping local variables:\n"
-     ^ eval_ctx_to_string ctx));
   (* Move the return value out of the return variable *)
   let ctx, ret_value =
     eval_operand config ctx (E.Move (mk_place_from_var_id ret_vid))
   in
-  (* Pop the frame *)
+  (* 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. *)
+  (* Pop the frame - we remove the `Frame` delimiter, and reintroduce all
+   * the local variables as dummy variables in the caller frame *)
   let rec pop env =
     match env with
     | [] -> failwith "Inconsistent environment"
     | C.Abs abs :: env -> C.Abs abs :: pop env
-    | C.Var (_, _) :: env -> pop env
-    | C.Frame :: env -> env
+    | C.Var (_, v) :: env -> C.Var (None, v) :: pop env
+    | C.Frame :: env -> (* Stop here *) env
   in
   let env = pop ctx.env in
   let ctx = { ctx with env } in
-- 
cgit v1.2.3