Fix the semantics of drop

4 files changed, 32 insertions, 5 deletions

diff --git a/TODO.md b/TODO.md
index 37d35138..39a16cdd 100644
--- a/TODO.md
+++ b/TODO.md
@@ -78,7 +78,7 @@
 
 6. add `mvalue` (meta values) stored in abstractions when ending loans
 
-8. The following doesn't work:
+8. The following doesn't work (if we don't expand the symbolic values):
   ```
   fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T)
 
diff --git a/src/Collections.ml b/src/Collections.ml
index 2cb298a7..351b6523 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -184,6 +184,7 @@ module type Set = sig
 
   val pp : Format.formatter -> t -> unit
   val show : t -> string
+  val pairwise_distinct : elt list -> bool
 end
 
 module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
@@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
     pp_string "}"
 
   let show s = to_string None s
+
+  let pairwise_distinct ls =
+    let s = ref empty in
+    let rec check ls =
+      match ls with
+      | [] -> true
+      | x :: ls' ->
+          if mem x !s then false
+          else (
+            s := add x !s;
+            check ls')
+    in
+    check ls
 end
 
 (** A map where the bindings are injective (i.e., if two keys are distinct,
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index edd27138..16ab9aad 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
     
     [end_borrows]: if false, we only end the outer loans we find. If true, we
     end all the loans and the borrows we find.
+    TODO: end_borrows is not necessary anymore.
  *)
 let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 34310ea1..ae9e59fe 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -20,20 +20,32 @@ open InterpreterExpressions
 (** The local logger *)
 let log = L.statements_log
 
-(** Drop a value at a given place *)
+(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
 let drop_value (config : C.config) (p : E.place) : cm_fun =
  fun cf ctx ->
-  log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
-  (* Prepare the place (by ending the outer loans and the borrows).
+  log#ldebug
+    (lazy
+      ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
+     ^ eval_ctx_to_string ctx));
+  (* Prepare the place (by ending the outer loans).
    * Note that [prepare_lplace] will use the `Write` access kind:
    * it is ok, because when updating the value with [Bottom] below,
    * we will use the `Move` access *)
-  let end_borrows = true in
+  let end_borrows = false in
   let prepare = prepare_lplace config end_borrows p in
   (* Replace the value with [Bottom] *)
   let replace cf (v : V.typed_value) ctx =
+    (* Move the value at destination (that we will overwrite) to a dummy variable
+     * to preserve the borrows *)
+    let mv = read_place_unwrap config Write p ctx in
+    let ctx = C.ctx_push_dummy_var ctx mv in
+    (* Update the destination to ⊥ *)
     let nv = { v with value = V.Bottom } in
     let ctx = write_place_unwrap config Move p nv ctx in
+    log#ldebug
+      (lazy
+        ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
+       ^ eval_ctx_to_string ctx));
     cf ctx
   in
   (* Compose and apply *)