Start updating the assignment semantics

4 files changed, 63 insertions, 36 deletions

diff --git a/TODO.md b/TODO.md
index c317a8b1..62463d6a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,34 +1,23 @@
+# TODO
+
 * write an interesting example to study with Jonathan
 
 * update the assignment to move the destination value (which will be overriden)
   to a dummy variable, and end all the outer borrows.
-  update pop_frame
+  Also update pop_frame.
 
 * add option for: `allow_borrow_overwrites_on_input_values`
+  (rather: `will_overwrite_input_borrows`)
   (but always disallow borrow overwrites on returned values)
   at the level of abstractions (not at the level of loans!)
 
 * set of types with mutable borrows (what to do when type variables appear under
   shared borrows?)
-
-* split `apply_proj_borrows` into two:
-  * `apply_proj_borrows_on_input_values` : ... -> value -> rty -> avalue
-  * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue
-  TODO: actually not sure
-
-* remove the rule which says that we can end a borrow under an abstraction if
-  the corresponding loan is in the same abstraction.
+  necessary to know what to return.
 
 * Check what happens when symbolic borrows are not expanded (when looking for
   borrows/abstractions to end).
 
-* Reduce projectors to `_` (ignored) when there are no region intersections
-
-* update end_borrow_get_borrow to keep track of the ignored borrows/loans as
-  outer borrows, and track the ids of the ignored shared loans?
-  or: make sure there are no parent abstractions when ending inner loans in
-  abstractions.
-
 * expand symbolic values which are primitively copyable upon using them as
   function arguments or putting them in the return value, in order to deduplicate
   those values.
@@ -45,6 +34,22 @@
   case we will need to split the value given back - for now: disallow this
   behaviour?).
 
+* split `apply_proj_borrows` into two:
+  * `apply_proj_borrows_on_input_values` : ... -> value -> rty -> avalue
+  * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue
+  TODO: actually not sure
+
+* remove the rule which says that we can end a borrow under an abstraction if
+  the corresponding loan is in the same abstraction.
+  Actually: update the rule, rather.
+* Reduce projectors to `_` (ignored) when there are no region intersections
+
+* update end_borrow_get_borrow to keep track of the ignored borrows/loans as
+  outer borrows, and track the ids of the ignored shared loans?
+  or: make sure there are no parent abstractions when ending inner loans in
+  abstractions.
+
+
 * `ended_proj_loans` (with ghost value)
 
 * add a check in function inputs: ok to take as parameters symbolic values with
@@ -65,3 +70,6 @@
 
 * Some variables have the same name. It might be good to also print their id
   to disambiguate?
+
+
+# DONE
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 3e402d88..e34a5383 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -532,14 +532,20 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
   with FoundBorrowContent bc -> Some bc
 
 (** Return the first loan or borrow content we find in a value (starting with
-    the outer ones) *)
-let get_first_loan_or_borrow_in_value (v : V.typed_value) :
-    loan_or_borrow_content option =
+    the outer ones).
+    
+    [with_borrows]:
+    - if true: return the first loan or borrow we find
+    - if false: return the first loan we find, do not dive into borrowed values
+ *)
+let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
+    (v : V.typed_value) : loan_or_borrow_content option =
   let obj =
     object
       inherit [_] V.iter_typed_value
 
-      method! visit_borrow_content _ bc = raise (FoundBorrowContent bc)
+      method! visit_borrow_content _ bc =
+        if with_borrows then raise (FoundBorrowContent bc) else ()
 
       method! visit_loan_content _ lc = raise (FoundLoanContent lc)
     end
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index badee335..1f7135a5 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -572,14 +572,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
         (* The context was updated: do a recursive call to reinspect the value *)
         end_loans_at_place config access p ctx)
 
-(** Drop (end) all the loans and borrows at a given place, which should be
-    seen as an l-value (we will write to it later, but need to drop the borrows
-    before writing).
+(** Drop (end) loans and borrows at a given place, which should be
+    seen as an l-value (we will write to it later, but need to drop
+    the borrows before writing).
 
     This is used to drop values (when we need to write to a place, we first
     drop the value there to properly propagate back values which are not/can't
     be borrowed anymore).
     
+    [end_borrows]:
+    - if true: end all the loans and borrows we find. This is used for instance
+      by [drop_value].
+    - if false: only end the outer loans. This is used by [assign_to_place]
+      or to drop the loans in the local variables when popping a frame.
+
     Note that we don't do what is defined in the formalization: we move the
     value to a temporary dummy value, then explore this value and end the
     loans/borrows inside as long as we find some, starting with the outer
@@ -599,8 +605,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
     - we can't immediately end `mut_borrow l2 ...` because it contains a loan
     - the borrow corresponding to the loan `mut_loan l3` is outside of `*x`
  *)
-let drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
+    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
@@ -612,7 +618,7 @@ let drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
     (* Read the value *)
     let v = C.ctx_read_first_dummy_var ctx in
     (* Check if there are loans or borrows to end *)
-    match get_first_loan_or_borrow_in_value v with
+    match get_first_outer_loan_or_borrow_in_value end_borrows v with
     | None ->
         (* We are done *)
         ctx
@@ -712,20 +718,23 @@ 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 the borrows and loans at
-    this place, etc.
+    update the environment along the paths, end  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
-    it is the case). Note that it is very likely to contain [Bottom] values.
+    it is the case). Note that this value is very likely to contain [Bottom]
+    subvalues.
+    
+    [end_borrows]: if false, we only end the outer loans we find. If true, we
+    end all the loans and the borrows we find.
  *)
-let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
+let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
   (* TODO *)
   let access = Write in
   let ctx = update_ctx_along_write_place config access p ctx in
   (* End the borrows and loans, starting with the borrows *)
-  let ctx = drop_borrows_loans_at_lplace config p ctx in
+  let ctx = drop_outer_borrows_loans_at_lplace config end_borrows p ctx in
   (* Read the value and check it *)
   let v = read_place_unwrap config access p ctx in
   (* Sanity checks *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 3bf9e7a4..de904262 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -25,8 +25,9 @@ type statement_eval_res = Unit | Break of int | Continue of int | Return
 let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
     =
   log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
-  (* Prepare the place (by ending the loans, then the borrows) *)
-  let ctx, v = prepare_lplace config p ctx in
+  (* Prepare the place (by ending the outer loans) *)
+  let end_borrows = true in
+  let ctx, v = prepare_lplace config end_borrows p ctx in
   (* Replace the value with [Bottom] *)
   let nv = { v with value = V.Bottom } in
   let ctx = write_place_unwrap config Write p nv ctx in
@@ -44,10 +45,11 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
   (* Push the rvalue to a dummy variable, for bookkeeping *)
   let ctx = C.ctx_push_dummy_var ctx v in
   (* Prepare the destination *)
-  let ctx, _ = prepare_lplace config p ctx in
+  let end_borrows = false in
+  let ctx, _ = prepare_lplace config end_borrows p ctx in
   (* Retrieve the dummy variable *)
   let ctx, v = C.ctx_pop_dummy_var ctx in
-  (* Checks *)
+  (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
   assert (not (bottom_in_value ctx.ended_regions v));
   (* Update the destination *)
   let ctx = write_place_unwrap config Write p v ctx in
@@ -189,6 +191,8 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   let ctx, ret_value =
     eval_operand config ctx (E.Move (mk_place_from_var_id ret_vid))
   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. *)