Introduce dummy variables and update assign_to_place

6 files changed, 61 insertions, 14 deletions

diff --git a/TODO.md b/TODO.md
index 52085328..0070000f 100644
--- a/TODO.md
+++ b/TODO.md
@@ -16,6 +16,11 @@
 * remove the rule which says that we can end a borrow under an abstraction if
   the corresponding loan is in the same abstraction
 
+* add a `allow_borrow_overwrites` in the loan projectors.
+
+* add option for: `allow_borrow_overwrites_on_input_values`
+  (but always disallow borrow overwrites on returned values)
+
 * During printing, contexts are often big, with many variables containing "bottom".
   Some variables also actually never get assigned, especially when they are used
   for auxiliary assignments which don't exist anymore (because they were merged
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 0fe3a09a..d8ea9a3f 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -55,7 +55,13 @@ type binder = {
     
     TODO: rename Var (-> Binding?)
  *)
-type env_elem = Var of (binder[@opaque]) * typed_value | Abs of abs | Frame
+type env_elem =
+  | Var of (binder option[@opaque]) * typed_value
+      (** Variable binding - the binder is None if the variable is a dummy variable
+          (we use dummy variables to store temporaries while doing bookkeeping such
+           as ending borrows for instance). *)
+  | Abs of abs
+  | Frame
 [@@deriving
   show,
     visitors
@@ -115,13 +121,17 @@ type eval_ctx = {
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
+let opt_binder_has_vid (bv : binder option) (vid : VarId.id) : bool =
+  match bv with Some bv -> bv.index = vid | None -> false
+
 let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   (* TOOD: we might want to stop at the end of the frame *)
   let rec lookup env =
     match env with
     | [] ->
         raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
-    | Var (var, _) :: env' -> if var.index = vid then var else lookup env'
+    | Var (var, _) :: env' ->
+        if opt_binder_has_vid var vid then Option.get var else lookup env'
     | (Abs _ | Frame) :: env' -> lookup env'
   in
   lookup ctx.env
@@ -140,7 +150,8 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
   let rec lookup env =
     match env with
     | [] -> failwith "Unexpected"
-    | Var (var, v) :: env' -> if var.index = vid then v else lookup env'
+    | Var (var, v) :: env' ->
+        if opt_binder_has_vid var vid then v else lookup env'
     | Abs _ :: env' -> lookup env'
     | Frame :: _ -> failwith "End of frame"
   in
@@ -163,7 +174,7 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
     match env with
     | [] -> failwith "Unexpected"
     | Var (var, v) :: env' ->
-        if var.index = vid then Var (var, nv) :: env'
+        if opt_binder_has_vid var vid then Var (var, nv) :: env'
         else Var (var, v) :: update env'
     | Abs abs :: env' -> Abs abs :: update env'
     | Frame :: _ -> failwith "End of frame"
@@ -189,7 +200,7 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
 let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
   assert (var.var_ty = v.ty);
   let bv = var_to_binder var in
-  { ctx with env = Var (bv, v) :: ctx.env }
+  { ctx with env = Var (Some bv, v) :: ctx.env }
 
 (** Push a list of variables.
 
@@ -203,11 +214,29 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
       (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
       vars);
   let vars =
-    List.map (fun (var, value) -> Var (var_to_binder var, value)) vars
+    List.map (fun (var, value) -> Var (Some (var_to_binder var), value)) vars
   in
   let vars = List.rev vars in
   { ctx with env = List.append vars ctx.env }
 
+(** Push a dummy variable in the context's environment. *)
+let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
+  { ctx with env = Var (None, v) :: ctx.env }
+
+(** Pop the first dummy variable from the context's environment. *)
+let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value =
+  let rec pop_var (env : env) : env * typed_value =
+    match env with
+    | [] -> failwith "Could not find a dummy variable"
+    | Var (None, v) :: env -> (env, v)
+    | ee :: env ->
+        let env, v = pop_var env in
+        (ee :: env, v)
+  in
+  let env, v = pop_var ctx.env in
+  ({ ctx with env }, v)
+
+(* TODO: move *)
 let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
 
 (** Push an uninitialized variable (which thus maps to [Bottom]) *)
@@ -237,7 +266,7 @@ class ['self] iter_frame =
   object (self : 'self)
     inherit [_] V.iter_abs
 
-    method visit_Var : 'acc -> binder -> typed_value -> unit =
+    method visit_Var : 'acc -> binder option -> typed_value -> unit =
       fun acc _vid v -> self#visit_typed_value acc v
 
     method visit_Abs : 'acc -> abs -> unit =
@@ -265,7 +294,7 @@ class ['self] map_frame_concrete =
   object (self : 'self)
     inherit [_] V.map_abs
 
-    method visit_Var : 'acc -> binder -> typed_value -> env_elem =
+    method visit_Var : 'acc -> binder option -> typed_value -> env_elem =
       fun acc vid v ->
         let v = self#visit_typed_value acc v in
         Var (vid, v)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index b590eff6..13ad8ee6 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -122,7 +122,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_Var env bv v =
         assert (Option.is_none !abs_or_var);
-        abs_or_var := Some (VarId bv.C.index);
+        abs_or_var :=
+          Some
+            (VarId (match bv with Some bv -> Some bv.C.index | None -> None));
         super#visit_Var env bv v;
         abs_or_var := None
 
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 38813894..0100a9c6 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -35,9 +35,14 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
 (** Assign a value to a given place *)
 let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
     (p : E.place) : C.eval_ctx =
+  (* Push the rvalue to a dummy variable, for bookkeeping *)
+  let ctx = C.ctx_push_dummy_var ctx v in
   (* Prepare the destination *)
-  (* TODO: there might be a problem because the value to assign is hanging in the air ! *)
   let ctx, _ = prepare_lplace config p ctx in
+  (* Retrieve the dummy variable *)
+  let ctx, v = C.ctx_pop_dummy_var ctx in
+  (* Checks *)
+  assert (not (bottom_in_value ctx.ended_regions v));
   (* Update the destination *)
   let ctx = write_place_unwrap config Write p v ctx in
   ctx
@@ -180,6 +185,8 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
     | [] -> 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 :: _ -> []
@@ -226,7 +233,8 @@ let eval_box_new_concrete (config : C.config)
   match (region_params, type_params, ctx.env) with
   | ( [],
       [ boxed_ty ],
-      Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) ->
+      Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ )
+    ->
       (* Required type checking *)
       assert (input_value.V.ty = boxed_ty);
 
@@ -260,7 +268,8 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
   match (region_params, type_params, ctx.env) with
   | ( [],
       [ boxed_ty ],
-      Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> (
+      Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ )
+    -> (
       (* Required type checking. We must have:
          - input_value.ty == & (mut) Box<ty>
          - boxed_ty == ty
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fd596fd3..a808e14c 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -105,7 +105,7 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
 type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 (** Generic borrow content: concrete or abstract *)
 
-type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id
+type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id option
 
 exception FoundBorrowContent of V.borrow_content
 (** Utility exception *)
diff --git a/src/Print.ml b/src/Print.ml
index 5ae722b9..4dbe30f7 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -455,7 +455,9 @@ module Contexts = struct
       (indent_incr : string) (ev : C.env_elem) : string =
     match ev with
     | Var (var, tv) ->
-        indent ^ binder_to_string var ^ " -> "
+        indent
+        ^ option_to_string binder_to_string var
+        ^ " -> "
         ^ PV.typed_value_to_string fmt tv
         ^ " ;"
     | Abs abs -> PV.abs_to_string fmt indent indent_incr abs