Introduce mdplace to link meta information about the given back values

to the information about the input arguments

8 files changed, 212 insertions, 114 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index d200276f..065a39b9 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1202,16 +1202,16 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
           ^ aborrow_content_to_string ctx bc));
       let ctx =
         match bc with
-        | V.AMutBorrow (_, bid, av) ->
+        | V.AMutBorrow (mv, bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
-            let v = convert_avalue_to_given_back_value abs.kind av in
+            let sv = convert_avalue_to_given_back_value abs.kind av in
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
-            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in
+            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in
             let ctx = update_aborrow ek_all bid ended_borrow ctx in
             (* Give the value back *)
-            let v = mk_typed_value_from_symbolic_value v in
-            give_back_value config bid v ctx
+            let sv = mk_typed_value_from_symbolic_value sv in
+            give_back_value config bid sv ctx
         | V.ASharedBorrow bid ->
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = V.ABorrow V.AEndedSharedBorrow in
@@ -1256,7 +1256,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       (* Generate a fresh symbolic value *)
       let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
-      let ended_borrow = V.AEndedProjBorrows nsv in
+      let ended_borrow =
+        V.AEndedProjBorrows { original = sv; given_back = nsv }
+      in
       let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
diff --git a/src/Print.ml b/src/Print.ml
index 5ccba517..69379bf9 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -457,7 +457,7 @@ module Values = struct
         ^ ", "
         ^ typed_avalue_to_string fmt av
         ^ ")"
-    | AEndedMutBorrow (_mv, child) ->
+    | AEndedMutBorrow (_mv, _msv, child) ->
         "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")"
     | AEndedIgnoredMutBorrow
         { child; given_back_loans_proj; given_back_meta = _ } ->
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 09194d85..9ca0c064 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -228,16 +228,6 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
   let name = match p.name with None -> "_" | Some name -> name in
   projection_to_string fmt name p.projection
 
-let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string =
-  match v with
-  | Var (v, Some { name = Some name; projection }) ->
-      assert (projection = []);
-      let fmt = value_to_type_formatter fmt in
-      "(" ^ var_to_varname v ^ " @meta[@dest=" ^ name ^ "] : "
-      ^ ty_to_string fmt v.ty ^ ")"
-  | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v
-  | Dummy -> "_"
-
 let place_to_string (fmt : ast_formatter) (p : place) : string =
   (* TODO: improve that *)
   let var = fmt.var_id_to_string p.var in
@@ -315,16 +305,6 @@ let adt_g_value_to_string (fmt : value_formatter)
           ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: "
            ^ Print.option_to_string VariantId.to_string variant_id))
 
-let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) :
-    string =
-  match v.value with
-  | LvConcrete cv -> Print.Values.constant_value_to_string cv
-  | LvVar var -> var_or_dummy_to_string fmt var
-  | LvAdt av ->
-      adt_g_value_to_string fmt
-        (typed_lvalue_to_string fmt)
-        av.variant_id av.field_values v.ty
-
 let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
     =
   match v.value with
@@ -336,6 +316,32 @@ let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
         (typed_rvalue_to_string fmt)
         av.variant_id av.field_values v.ty
 
+let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string =
+  match v with
+  | Var (v, { place = None; from_rvalue = None }) ->
+      var_to_string (ast_to_type_formatter fmt) v
+  | Var (v, { place; from_rvalue }) ->
+      let dest = Print.option_to_string (mplace_to_string fmt) place in
+      let from_rvalue =
+        Print.option_to_string (typed_rvalue_to_string fmt) from_rvalue
+      in
+      "(" ^ var_to_varname v ^ " @meta[@dest=" ^ dest ^ ", from_rvalue="
+      ^ from_rvalue ^ "] : "
+      ^ ty_to_string (ast_to_type_formatter fmt) v.ty
+      ^ ")"
+  | Dummy -> "_"
+
+let rec typed_lvalue_to_string (fmt : ast_formatter) (v : typed_lvalue) : string
+    =
+  match v.value with
+  | LvConcrete cv -> Print.Values.constant_value_to_string cv
+  | LvVar var -> var_or_dummy_to_string fmt var
+  | LvAdt av ->
+      adt_g_value_to_string
+        (ast_to_value_formatter fmt)
+        (typed_lvalue_to_string fmt)
+        av.variant_id av.field_values v.ty
+
 let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string =
   let ty_fmt = ast_to_type_formatter fmt in
   let type_params = List.map type_var_to_string sg.type_params in
@@ -452,7 +458,7 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
   let indent1 = indent ^ indent_incr in
   let re = texpression_to_string fmt indent1 indent_incr re in
   let e = texpression_to_string fmt indent indent_incr e in
-  let lv = typed_lvalue_to_string (ast_to_value_formatter fmt) lv in
+  let lv = typed_lvalue_to_string fmt lv in
   if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
   else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
 
@@ -472,7 +478,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       ^ "else\n" ^ indent ^ e_false
   | Match branches ->
       let branch_to_string (b : match_branch) : string =
-        let pat = typed_lvalue_to_string (ast_to_value_formatter fmt) b.pat in
+        let pat = typed_lvalue_to_string fmt b.pat in
         indent ^ "| " ^ pat ^ " ->\n" ^ indent1
         ^ texpression_to_string fmt indent1 indent_incr b.branch
       in
diff --git a/src/Pure.ml b/src/Pure.ml
index 58ee0b98..dbc6421c 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -182,7 +182,7 @@ class ['self] iter_value_base =
     method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for [map_var_or_dummy] visitor *)
+(** Ancestor for [map_typed_rvalue] visitor *)
 class ['self] map_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
@@ -199,7 +199,7 @@ class ['self] map_value_base =
     method visit_ty : 'env -> ty -> ty = fun _ x -> x
   end
 
-(** Ancestor for [reduce_var_or_dummy] visitor *)
+(** Ancestor for [reduce_typed_rvalue] visitor *)
 class virtual ['self] reduce_value_base =
   object (self : 'self)
     inherit [_] VisitorsRuntime.reduce
@@ -216,7 +216,7 @@ class virtual ['self] reduce_value_base =
     method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
   end
 
-(** Ancestor for [mapreduce_var_or_dummy] visitor *)
+(** Ancestor for [mapreduce_typed_rvalue] visitor *)
 class virtual ['self] mapreduce_value_base =
   object (self : 'self)
     inherit [_] VisitorsRuntime.mapreduce
@@ -235,14 +235,22 @@ class virtual ['self] mapreduce_value_base =
     method visit_ty : 'env -> ty -> ty * 'a = fun _ x -> (x, self#zero)
   end
 
-type var_or_dummy =
-  | Var of var * mplace option (* TODO: the mplace is actually always a variable *)
-  | Dummy  (** Ignored value: `_`. *)
+type rvalue =
+  | RvConcrete of constant_value
+  | RvPlace of place
+  | RvAdt of adt_rvalue
+
+and adt_rvalue = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_rvalue list;
+}
+
+and typed_rvalue = { value : rvalue; ty : ty }
 [@@deriving
   show,
     visitors
       {
-        name = "iter_var_or_dummy";
+        name = "iter_typed_rvalue";
         variety = "iter";
         ancestors = [ "iter_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -251,125 +259,186 @@ type var_or_dummy =
       },
     visitors
       {
-        name = "map_var_or_dummy";
+        name = "map_typed_rvalue";
         variety = "map";
         ancestors = [ "map_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.map] *);
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
       },
     visitors
       {
-        name = "reduce_var_or_dummy";
+        name = "reduce_typed_rvalue";
         variety = "reduce";
         ancestors = [ "reduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       },
     visitors
       {
-        name = "mapreduce_var_or_dummy";
+        name = "mapreduce_typed_rvalue";
         variety = "mapreduce";
         ancestors = [ "mapreduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       }]
 
-(** A left value (which appears on the left of assignments *)
-type lvalue =
-  | LvConcrete of constant_value
-      (** [LvConcrete] is necessary because we merge the switches over integer
-        values and the matches over enumerations *)
-  | LvVar of var_or_dummy
-  | LvAdt of adt_lvalue
+type mdplace = { place : mplace option; from_rvalue : typed_rvalue option }
+[@@deriving show]
+(** "Meta" destination place.
+
+    Meta information for places used as assignment destinations.
+    This is useful for the values given back by the backward functions: in such
+    situations, we link the output variables to the input arguments, to derive
+    names for the output variables from the input variables.
+
+    Ex.:
+    ====
+    ```
+    let y = f<'a>(&mut x);
+    ...
+    // end 'a
+    ...
+    ```
+    gets translated to:
+    ```
+    let y = f_fwd x in
+    ...
+    let s = f_back x y_i in // we want the introduced variable to be name "x1"
+    ...
+    ```
+    In order to compute a proper name for the variable introduced by the backward
+    call, we need to link `s` to `x`. However, because of desugaring, it may happen
+    that the fact `f` takes `x` as argument may have to be computed by propagating
+    naming information. This is why we link the output variables to the input arguments:
+    it allows us to propagate such naming constraints "across" function calls.
+ *)
 
-and adt_lvalue = {
-  variant_id : (VariantId.id option[@opaque]);
-  field_values : typed_lvalue list;
-}
+(** Ancestor for [iter_var_or_dummy] visitor *)
+class ['self] iter_var_or_dummy_base =
+  object (_self : 'self)
+    inherit [_] iter_typed_rvalue
 
-and typed_lvalue = { value : lvalue; ty : ty }
+    method visit_mdplace : 'env -> mdplace -> unit = fun _ _ -> ()
+  end
+
+(** Ancestor for [map_var_or_dummy] visitor *)
+class ['self] map_var_or_dummy_base =
+  object (_self : 'self)
+    inherit [_] map_typed_rvalue
+
+    method visit_mdplace : 'env -> mdplace -> mdplace = fun _ x -> x
+  end
+
+(** Ancestor for [reduce_var_or_dummy] visitor *)
+class virtual ['self] reduce_var_or_dummy_base =
+  object (self : 'self)
+    inherit [_] reduce_typed_rvalue
+
+    method visit_mdplace : 'env -> mdplace -> 'a = fun _ _ -> self#zero
+  end
+
+(** Ancestor for [mapreduce_var_or_dummy] visitor *)
+class virtual ['self] mapreduce_var_or_dummy_base =
+  object (self : 'self)
+    inherit [_] mapreduce_typed_rvalue
+
+    method visit_mdplace : 'env -> mdplace -> mdplace * 'a =
+      fun _ x -> (x, self#zero)
+  end
+
+type var_or_dummy =
+  | Var of var * mdplace
+      (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections).
+
+          We use [mplace] because it leads to a more uniform treatment of the meta
+          information.
+       *)
+  | Dummy  (** Ignored value: `_`. *)
 [@@deriving
   show,
     visitors
       {
-        name = "iter_typed_lvalue";
+        name = "iter_var_or_dummy";
         variety = "iter";
-        ancestors = [ "iter_var_or_dummy" ];
+        ancestors = [ "iter_var_or_dummy_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
       },
     visitors
       {
-        name = "map_typed_lvalue";
+        name = "map_var_or_dummy";
         variety = "map";
-        ancestors = [ "map_var_or_dummy" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        ancestors = [ "map_var_or_dummy_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.map] *);
         concrete = true;
         polymorphic = false;
       },
     visitors
       {
-        name = "reduce_typed_lvalue";
+        name = "reduce_var_or_dummy";
         variety = "reduce";
-        ancestors = [ "reduce_var_or_dummy" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        ancestors = [ "reduce_var_or_dummy_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       },
     visitors
       {
-        name = "mapreduce_typed_lvalue";
+        name = "mapreduce_var_or_dummy";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_var_or_dummy" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        ancestors = [ "mapreduce_var_or_dummy_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       }]
 
-type rvalue =
-  | RvConcrete of constant_value
-  | RvPlace of place
-  | RvAdt of adt_rvalue
+(** A left value (which appears on the left of assignments *)
+type lvalue =
+  | LvConcrete of constant_value
+      (** [LvConcrete] is necessary because we merge the switches over integer
+        values and the matches over enumerations *)
+  | LvVar of var_or_dummy
+  | LvAdt of adt_lvalue
 
-and adt_rvalue = {
+and adt_lvalue = {
   variant_id : (VariantId.id option[@opaque]);
-  field_values : typed_rvalue list;
+  field_values : typed_lvalue list;
 }
 
-and typed_rvalue = { value : rvalue; ty : ty }
+and typed_lvalue = { value : lvalue; ty : ty }
 [@@deriving
   show,
     visitors
       {
-        name = "iter_typed_rvalue";
+        name = "iter_typed_lvalue";
         variety = "iter";
-        ancestors = [ "iter_typed_lvalue" ];
+        ancestors = [ "iter_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
       },
     visitors
       {
-        name = "map_typed_rvalue";
+        name = "map_typed_lvalue";
         variety = "map";
-        ancestors = [ "map_typed_lvalue" ];
+        ancestors = [ "map_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
       },
     visitors
       {
-        name = "reduce_typed_rvalue";
+        name = "reduce_typed_lvalue";
         variety = "reduce";
-        ancestors = [ "reduce_typed_lvalue" ];
+        ancestors = [ "reduce_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       },
     visitors
       {
-        name = "mapreduce_typed_rvalue";
+        name = "mapreduce_typed_lvalue";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_typed_lvalue" ];
+        ancestors = [ "mapreduce_var_or_dummy" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         polymorphic = false;
       }]
@@ -398,7 +467,7 @@ type meta = Assignment of mplace * typed_rvalue [@@deriving show]
 (** Ancestor for [iter_expression] visitor *)
 class ['self] iter_expression_base =
   object (_self : 'self)
-    inherit [_] iter_typed_rvalue
+    inherit [_] iter_typed_lvalue
 
     method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
 
@@ -412,7 +481,7 @@ class ['self] iter_expression_base =
 (** Ancestor for [map_expression] visitor *)
 class ['self] map_expression_base =
   object (_self : 'self)
-    inherit [_] map_typed_rvalue
+    inherit [_] map_typed_lvalue
 
     method visit_meta : 'env -> meta -> meta = fun _ x -> x
 
@@ -428,7 +497,7 @@ class ['self] map_expression_base =
 (** Ancestor for [reduce_expression] visitor *)
 class virtual ['self] reduce_expression_base =
   object (self : 'self)
-    inherit [_] reduce_typed_rvalue
+    inherit [_] reduce_typed_lvalue
 
     method visit_meta : 'env -> meta -> 'a = fun _ _ -> self#zero
 
@@ -444,7 +513,7 @@ class virtual ['self] reduce_expression_base =
 (** Ancestor for [mapreduce_expression] visitor *)
 class virtual ['self] mapreduce_expression_base =
   object (self : 'self)
-    inherit [_] mapreduce_typed_rvalue
+    inherit [_] mapreduce_typed_lvalue
 
     method visit_meta : 'env -> meta -> meta * 'a = fun _ x -> (x, self#zero)
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 06fd3d69..abdeb41e 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -242,11 +242,13 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
         method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ())
 
-        method! visit_Var _ v mp () =
+        method! visit_Var _ v mdp () =
           (* Register the variable *)
           let ctx = add_var (self#zero ()) v in
           (* Register the mplace information if there is such information *)
-          match mp with None -> ctx | Some mp -> add_constraint mp v.id ctx
+          match mdp.place with
+          | None -> ctx
+          | Some mp -> add_constraint mp v.id ctx
       end
     in
     let ctx1 = obj#visit_typed_lvalue () lv () in
@@ -820,7 +822,7 @@ let to_monadic (config : config) (def : fun_decl) : fun_decl =
             let id, _ = VarId.fresh var_cnt in
             let var = { id; basename = None; ty = unit_ty } in
             let inputs = [ var ] in
-            let input_lv = mk_typed_lvalue_from_var var None in
+            let input_lv = mk_typed_lvalue_from_var var None None in
             let inputs_lvs = [ input_lv ] in
             Some { body with inputs; inputs_lvs }
       in
@@ -978,7 +980,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
                    * monadic binding *)
                   let vid = fresh_id () in
                   let tmp : var = { id = vid; basename = None; ty = lv.ty } in
-                  let ltmp = mk_typed_lvalue_from_var tmp None in
+                  let ltmp = mk_typed_lvalue_from_var tmp None None in
                   let rtmp = mk_typed_rvalue_from_var tmp in
                   let rtmp = mk_value_expression rtmp None in
                   (* Visit the next expression *)
@@ -1056,7 +1058,9 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
                 in
                 (* The `Success` branch introduces a fresh state variable *)
                 let state_var = fresh_state_var () in
-                let state_value = mk_typed_lvalue_from_var state_var None in
+                let state_value =
+                  mk_typed_lvalue_from_var state_var None None
+                in
                 let success_pat =
                   mk_result_return_lvalue
                     (mk_simpl_tuple_lvalue [ state_value; lv ])
@@ -1127,7 +1131,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
           let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in
           (* Update the inputs list *)
           let inputs = body.inputs @ [ input_state_var ] in
-          let input_lv = mk_typed_lvalue_from_var input_state_var None in
+          let input_lv = mk_typed_lvalue_from_var input_state_var None None in
           let inputs_lvs = body.inputs_lvs @ [ input_lv ] in
           (* Update the body *)
           let body = { body with inputs; inputs_lvs } in
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 23bffa1d..78ddf8aa 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -64,8 +64,10 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
   let ty = v.ty in
   { value; ty }
 
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
-  let value = LvVar (Var (v, mp)) in
+let mk_typed_lvalue_from_var (v : var) (mp : mplace option)
+    (mfrom_rvalue : typed_rvalue option) : typed_lvalue =
+  let mdplace = { place = mp; from_rvalue = mfrom_rvalue } in
+  let value = LvVar (Var (v, mdplace)) in
   let ty = v.ty in
   { value; ty }
 
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index fe500480..87e86e69 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -647,7 +647,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
         (mk_typed_rvalue_from_var var).value
   in
   let ty = ctx_translate_fwd_ty ctx v.ty in
-  let value = { value; ty } in
+  let value : typed_rvalue = { value; ty } in
   (* Debugging *)
   log#ldebug
     (lazy
@@ -736,7 +736,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       failwith "Unreachable"
-  | AEndedMutBorrow (_, _) ->
+  | AEndedMutBorrow (_, _, _) ->
       (* We collect consumed values: ignore *)
       None
   | AEndedIgnoredMutBorrow _ ->
@@ -804,6 +804,9 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
     
     [mp]: it is possible to provide some meta-place information, to guide
     the heuristics which later find pretty names for the variables.
+
+    TODO:
+    
  *)
 let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
     (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
@@ -875,10 +878,13 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       failwith "Unreachable"
-  | AEndedMutBorrow (mv, _) ->
-      (* Return the meta-value *)
-      let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp))
+  | AEndedMutBorrow (consumed_mv, msv, _) ->
+      (* We use the originally consumed value (which is stored as a meta-value)
+       * to help with propagating naming constraints. *)
+      let consumed = typed_value_to_rvalue ctx consumed_mv in
+      (* Return the meta-symbolic-value *)
+      let ctx, var = fresh_var_for_symbolic_value msv ctx in
+      (ctx, Some (mk_typed_lvalue_from_var var mp (Some consumed)))
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -897,10 +903,15 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
           (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows)
           child_projs);
       (ctx, None)
-  | AEndedProjBorrows mv ->
+  | AEndedProjBorrows { original; given_back = mv } ->
+      (* We use the original symbolic value to help propagate the naming constraints *)
+      let original =
+        InterpreterUtils.mk_typed_value_from_symbolic_value original
+      in
+      let original = typed_value_to_rvalue ctx original in
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp))
+      (ctx, Some (mk_typed_lvalue_from_var var mp (Some original)))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
       failwith "Unreachable"
 
@@ -1039,7 +1050,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
       (fun (arg, mp) -> mk_value_expression arg mp)
       (List.combine args args_mplaces)
   in
-  let dest_v = mk_typed_lvalue_from_var dest dest_mplace in
+  let dest_v = mk_typed_lvalue_from_var dest dest_mplace None in
   let call = { func; type_params; args } in
   let call = Call call in
   let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in
@@ -1104,7 +1115,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       List.fold_right
         (fun (var, value) (e : texpression) ->
           mk_let monadic
-            (mk_typed_lvalue_from_var var None)
+            (mk_typed_lvalue_from_var var None None)
             (mk_value_expression value None)
             e)
         variables_values next_e
@@ -1276,7 +1287,7 @@ and translate_expansion (config : config) (p : S.mplace option)
           let next_e = translate_expression config e ctx in
           let monadic = false in
           mk_let monadic
-            (mk_typed_lvalue_from_var var None)
+            (mk_typed_lvalue_from_var var None None)
             (mk_value_expression scrutinee scrutinee_mplace)
             next_e
       | SeAdt _ ->
@@ -1300,7 +1311,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                 (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
                 let variant_id = Option.get variant_id in
                 let lvars =
-                  List.map (fun v -> mk_typed_lvalue_from_var v None) vars
+                  List.map (fun v -> mk_typed_lvalue_from_var v None None) vars
                 in
                 let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in
                 let monadic = false in
@@ -1329,13 +1340,13 @@ and translate_expansion (config : config) (p : S.mplace option)
                   (fun (fid, var) e ->
                     let field_proj = gen_field_proj fid var in
                     mk_let monadic
-                      (mk_typed_lvalue_from_var var None)
+                      (mk_typed_lvalue_from_var var None None)
                       (mk_value_expression field_proj None)
                       e)
                   id_var_pairs branch
           | T.Tuple ->
               let vars =
-                List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+                List.map (fun x -> mk_typed_lvalue_from_var x None None) vars
               in
               let monadic = false in
               mk_let monadic
@@ -1351,7 +1362,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                * identity when extracted (`box a == a`) *)
               let monadic = false in
               mk_let monadic
-                (mk_typed_lvalue_from_var var None)
+                (mk_typed_lvalue_from_var var None None)
                 (mk_value_expression scrutinee scrutinee_mplace)
                 branch
           | T.Assumed T.Vec ->
@@ -1372,7 +1383,7 @@ and translate_expansion (config : config) (p : S.mplace option)
             let variant_id = Option.get variant_id in
             let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
             let vars =
-              List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+              List.map (fun x -> mk_typed_lvalue_from_var x None None) vars
             in
             let pat_ty = scrutinee.ty in
             let pat = mk_adt_lvalue pat_ty variant_id vars in
@@ -1481,7 +1492,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         in
         let inputs = List.append ctx.forward_inputs backward_inputs in
         let inputs_lvs =
-          List.map (fun v -> mk_typed_lvalue_from_var v None) inputs
+          List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs
         in
         (* Sanity check *)
         assert (
diff --git a/src/Values.ml b/src/Values.ml
index f2807cfa..d415df52 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -329,10 +329,13 @@ type aproj =
           
           Note that we keep the original symbolic value as a meta-value.
        *)
-  | AEndedProjBorrows of msymbolic_value
+  | AEndedProjBorrows of {
+      original : msymbolic_value;
+      given_back : msymbolic_value;
+    }
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
-          purposes, the symbolic value which was generated and given back upon
-          ending the borrow.
+          purposes, the symbolic value which was originally in the borrow projection,
+          and the symbolic value which was generated and given back upon ending the borrow.
        *)
   | AIgnoredProjBorrows
 [@@deriving
@@ -675,9 +678,10 @@ and aborrow_content =
             abstraction so that we can properly call the backward functions
             when generating the pure translation.
        *)
-  | AEndedMutBorrow of msymbolic_value * typed_avalue
+  | AEndedMutBorrow of mvalue * msymbolic_value * typed_avalue
       (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
-          that we gave back as a meta-value, to help with the synthesis.
+          that we gave back as a meta-value, to help with the synthesis, together
+          with the initial consumed value (also as a meta-value).
           We also remember the child [avalue] because this structural information
           is useful for the synthesis (but not for the symbolic execution):
           in practice the child value should only contain ended borrows, ignored