Improve the generation of names for given back values

15 files changed, 236 insertions, 72 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 89dfb274..1905cf79 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -92,7 +92,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
 
       method! visit_Borrow outer bc =
         match bc with
-        | SharedBorrow (_, l') | InactivatedMutBorrow l' ->
+        | SharedBorrow (_, l') | InactivatedMutBorrow (_, l') ->
             (* Check if this is the borrow we are looking for *)
             if l = l' then (
               (* Check if there are outer borrows or if we are inside an abstraction *)
@@ -730,7 +730,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
       give_back_value config l tv ctx
-  | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') ->
+  | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow (_, l')) ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the borrow is somewhere - purely a sanity check *)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 30314307..d1c60941 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -197,9 +197,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (mv, bid) ->
             (* Nothing specific to do *)
             super#visit_SharedBorrow env mv bid
-        | V.InactivatedMutBorrow bid ->
+        | V.InactivatedMutBorrow (mv, bid) ->
             (* Nothing specific to do *)
-            super#visit_InactivatedMutBorrow env bid
+            super#visit_InactivatedMutBorrow env mv bid
         | V.MutBorrow (bid, mv) ->
             (* Control the dive *)
             if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
@@ -410,7 +410,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
-        | V.InactivatedMutBorrow bid ->
+        | V.InactivatedMutBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
 
@@ -494,10 +494,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
         | V.SharedBorrow (mv, bid) ->
             (* Check the id *)
             if bid = l then update () else super#visit_SharedBorrow env mv bid
-        | V.InactivatedMutBorrow bid ->
+        | V.InactivatedMutBorrow (mv, bid) ->
             (* Check the id *)
             if bid = l then update ()
-            else super#visit_InactivatedMutBorrow env bid
+            else super#visit_InactivatedMutBorrow env mv bid
 
       method! visit_loan_content env lc =
         match lc with
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index bd89649b..c967688f 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -558,7 +558,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         in
         let bc =
           if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid)
-          else V.InactivatedMutBorrow bid
+          else V.InactivatedMutBorrow (shared_mvalue, bid)
         in
         let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
         (* Continue *)
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 826e8563..1fd504d2 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -214,7 +214,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                         (* Return - note that we don't need to update the borrow itself *)
                         Ok (ctx, { res with updated = v }))
               else Error (FailBorrow bc)
-          | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
+          | V.InactivatedMutBorrow (_, bid) ->
+              Error (FailInactivatedMutBorrow bid)
           | V.MutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
                 match access_projection access ctx update p' bv with
@@ -565,7 +566,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
         match bc with
         | V.SharedBorrow _ | V.MutBorrow (_, _) ->
             (* Nothing special to do *) super#visit_borrow_content env bc
-        | V.InactivatedMutBorrow bid ->
+        | V.InactivatedMutBorrow (_, bid) ->
             (* We need to activate inactivated borrows *)
             let cc = activate_inactivated_mut_borrow config bid in
             raise (UpdateCtx cc)
@@ -654,7 +655,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
           | LoanContent (V.MutLoan bid)
           | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) ->
               end_outer_borrow config bid
-          | BorrowContent (V.InactivatedMutBorrow bid) ->
+          | BorrowContent (V.InactivatedMutBorrow (_, bid)) ->
               (* First activate the borrow *)
               activate_inactivated_mut_borrow config bid
         in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 5a700f1a..c3331de5 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -808,12 +808,15 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
                * inactivated borrow, we later can't translate it to pure values...) *)
               match rvalue with
               | E.Use _
-              | E.Ref (_, (E.Shared | E.Mut))
+              | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut))
               | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ ->
-                  S.synthesize_assignment (S.mk_mplace p ctx) rv expr
-              | E.Ref (_, E.TwoPhaseMut) ->
-                  (* Two-phase borrow: don't synthesize meta-information *)
-                  expr)
+                  let rp = rvalue_get_place rvalue in
+                  let rp =
+                    match rp with
+                    | Some rp -> Some (S.mk_mplace rp ctx)
+                    | None -> None
+                  in
+                  S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr)
         in
 
         (* Compose and apply *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 27d65a62..7a2e22f7 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -249,3 +249,13 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
     obj#visit_typed_value () v;
     false
   with Found -> true
+
+(** Return the place used in an rvalue, if that makes sense.
+    This is used to compute meta-data, to find pretty names.
+ *)
+let rvalue_get_place (rv : E.rvalue) : E.place option =
+  match rv with
+  | Use (Copy p | Move p) -> Some p
+  | Use (Constant _) -> None
+  | Ref (p, _) -> Some p
+  | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> None
diff --git a/src/Invariants.ml b/src/Invariants.ml
index f12911d4..81e35de3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -244,7 +244,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           match bc with
           | V.SharedBorrow (_, bid) -> register_borrow Shared bid
           | V.MutBorrow (bid, _) -> register_borrow Mut bid
-          | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid
+          | V.InactivatedMutBorrow (_, bid) -> register_borrow Inactivated bid
         in
         (* Continue exploring *)
         super#visit_borrow_content env bc
@@ -461,7 +461,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | V.SharedBorrow (_, bid), T.Shared
-            | V.InactivatedMutBorrow bid, T.Mut -> (
+            | V.InactivatedMutBorrow (_, bid), T.Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
diff --git a/src/Print.ml b/src/Print.ml
index 5ccba517..98876acb 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -309,7 +309,7 @@ module Values = struct
         "&mut@" ^ V.BorrowId.to_string bid ^ " ("
         ^ typed_value_to_string fmt tv
         ^ ")"
-    | InactivatedMutBorrow bid ->
+    | InactivatedMutBorrow (_, bid) ->
         "⌊inactivated_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
   and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) :
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index e962c27c..1c3d396d 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -225,7 +225,8 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
               "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
 
 let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
-  let name = match p.name with None -> "_" | Some name -> name in
+  let name = match p.name with None -> "" | Some name -> name in
+  let name = name ^ "^" ^ V.VarId.to_string p.var_id in
   projection_to_string fmt name p.projection
 
 let place_to_string (fmt : ast_formatter) (p : place) : string =
@@ -408,17 +409,28 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
 let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
   let meta =
     match meta with
-    | Assignment (p, rv) ->
-        "@assign(" ^ mplace_to_string fmt p ^ " := "
+    | Assignment (lp, rv, rp) ->
+        let rp =
+          match rp with
+          | None -> ""
+          | Some rp -> " [@src=" ^ mplace_to_string fmt rp ^ "]"
+        in
+        "@assign(" ^ mplace_to_string fmt lp ^ " := "
         ^ typed_rvalue_to_string fmt rv
-        ^ ")"
+        ^ rp ^ ")"
   in
   "@meta[" ^ meta ^ "]"
 
 let rec expression_to_string (fmt : ast_formatter) (indent : string)
     (indent_incr : string) (e : expression) : string =
   match e with
-  | Value (v, _) -> "(" ^ typed_rvalue_to_string fmt v ^ ")"
+  | Value (v, mp) ->
+      let mp =
+        match mp with
+        | None -> ""
+        | Some mp -> " [@mplace=" ^ mplace_to_string fmt mp ^ "]"
+      in
+      "(" ^ typed_rvalue_to_string fmt v ^ mp ^ ")"
   | Call call -> call_to_string fmt indent indent_incr call
   | Let (monadic, lv, re, e) ->
       let_to_string fmt indent indent_incr monadic lv re e
@@ -469,8 +481,8 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
   | If (e_true, e_false) ->
       let e_true = texpression_to_string fmt indent1 indent_incr e_true in
       let e_false = texpression_to_string fmt indent1 indent_incr e_false in
-      "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent
-      ^ "else\n" ^ indent ^ e_false
+      "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent1 ^ e_true ^ "\n"
+      ^ indent ^ "else\n" ^ indent1 ^ e_false
   | Match branches ->
       let branch_to_string (b : match_branch) : string =
         let pat = typed_lvalue_to_string fmt b.pat in
diff --git a/src/Pure.ml b/src/Pure.ml
index f0e43115..02b821ef 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -165,7 +165,11 @@ type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 
 type projection = projection_elem list [@@deriving show]
 
-type mplace = { name : string option; projection : projection }
+type mplace = {
+  var_id : V.VarId.id;
+  name : string option;
+  projection : projection;
+}
 [@@deriving show]
 (** "Meta" place.
 
@@ -476,7 +480,8 @@ type fun_id =
 [@@deriving show, ord]
 
 (** Meta-information stored in the AST *)
-type meta = Assignment of mplace * typed_rvalue [@@deriving show]
+type meta = Assignment of mplace * typed_rvalue * mplace option
+[@@deriving show]
 
 (** Ancestor for [iter_expression] visitor *)
 class ['self] iter_expression_base =
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index ceaaa129..a963e628 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -3,6 +3,7 @@
 open Pure
 open PureUtils
 open TranslateCore
+module V = Values
 
 (** The local logger *)
 let log = L.pure_micro_passes_log
@@ -109,7 +110,10 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
   let id = obj#visit_expression () body.body.e () in
   VarId.generator_from_incr_id id
 
-type pn_ctx = string VarId.Map.t
+type pn_ctx = {
+  pure_vars : string VarId.Map.t;
+  llbc_vars : string V.VarId.Map.t;
+}
 (** "pretty-name context": see [compute_pretty_names] *)
 
 (** This function computes pretty names for the variables in the pure AST. It
@@ -229,50 +233,101 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
    *   also.
    *)
   let merge_ctxs (ctx0 : pn_ctx) (ctx1 : pn_ctx) : pn_ctx =
-    VarId.Map.fold (fun id name ctx -> VarId.Map.add id name ctx) ctx0 ctx1
+    let pure_vars =
+      VarId.Map.fold
+        (fun id name ctx -> VarId.Map.add id name ctx)
+        ctx0.pure_vars ctx1.pure_vars
+    in
+    let llbc_vars =
+      V.VarId.Map.fold
+        (fun id name ctx -> V.VarId.Map.add id name ctx)
+        ctx0.llbc_vars ctx1.llbc_vars
+    in
+    { pure_vars; llbc_vars }
+  in
+  let empty_ctx =
+    { pure_vars = VarId.Map.empty; llbc_vars = V.VarId.Map.empty }
   in
   let merge_ctxs_ls (ctxs : pn_ctx list) : pn_ctx =
-    List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) VarId.Map.empty ctxs
+    List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs
   in
 
   let add_var (ctx : pn_ctx) (v : var) : pn_ctx =
-    assert (not (VarId.Map.mem v.id ctx));
+    assert (not (VarId.Map.mem v.id ctx.pure_vars));
     match v.basename with
     | None -> ctx
-    | Some name -> VarId.Map.add v.id name ctx
+    | Some name ->
+        let pure_vars = VarId.Map.add v.id name ctx.pure_vars in
+        { ctx with pure_vars }
   in
-  let update_var (ctx : pn_ctx) (v : var) : var =
+  let update_var (ctx : pn_ctx) (v : var) (mp : mplace option) : var =
     match v.basename with
     | Some _ -> v
     | None -> (
-        match VarId.Map.find_opt v.id ctx with
-        | None -> v
-        | Some basename -> { v with basename = Some basename })
+        match VarId.Map.find_opt v.id ctx.pure_vars with
+        | Some basename -> { v with basename = Some basename }
+        | None ->
+            if Option.is_some mp then
+              match
+                V.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
+              with
+              | None -> v
+              | Some basename -> { v with basename = Some basename }
+            else v)
   in
   let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue =
     let obj =
       object
         inherit [_] map_typed_lvalue
 
-        method! visit_var _ v = update_var ctx v
+        method! visit_Var _ v mp = Var (update_var ctx v mp, mp)
       end
     in
     obj#visit_typed_lvalue () lv
   in
 
+  let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx =
+    match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
+    | None, Some name ->
+        let llbc_vars = V.VarId.Map.add mp.var_id name ctx.llbc_vars in
+        { ctx with llbc_vars }
+    | _ -> ctx
+  in
+
+  let add_pure_var_constraint (var_id : VarId.id) (name : string) (ctx : pn_ctx)
+      : pn_ctx =
+    let pure_vars =
+      if VarId.Map.mem var_id ctx.pure_vars then ctx.pure_vars
+      else VarId.Map.add var_id name ctx.pure_vars
+    in
+    { ctx with pure_vars }
+  in
+  let add_llbc_var_constraint (var_id : V.VarId.id) (name : string)
+      (ctx : pn_ctx) : pn_ctx =
+    let llbc_vars =
+      if V.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars
+      else V.VarId.Map.add var_id name ctx.llbc_vars
+    in
+    { ctx with llbc_vars }
+  in
   let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx =
+    (* Register the place *)
+    let ctx = register_mplace mp ctx in
     (* Update the variable name *)
     match (mp.name, mp.projection) with
     | Some name, [] ->
         (* Check if the variable already has a name - if not: insert the new name *)
-        if VarId.Map.mem var_id ctx then ctx else VarId.Map.add var_id name ctx
+        let ctx = add_pure_var_constraint var_id name ctx in
+        let ctx = add_llbc_var_constraint mp.var_id name ctx in
+        ctx
     | _ -> ctx
   in
   let add_right_constraint (mp : mplace) (rv : typed_rvalue) (ctx : pn_ctx) :
       pn_ctx =
-    match rv.value with
-    | RvPlace { var = var_id; projection = [] } -> add_constraint mp var_id ctx
-    | _ -> ctx
+    (* Register the place *)
+    let ctx = register_mplace mp ctx in
+    (* Add the constraint *)
+    match rv.value with RvPlace p -> add_constraint mp p.var ctx | _ -> ctx
   in
   let add_opt_right_constraint (mp : mplace option) (rv : typed_rvalue)
       (ctx : pn_ctx) : pn_ctx =
@@ -283,7 +338,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       object (self)
         inherit [_] reduce_typed_lvalue
 
-        method zero _ = VarId.Map.empty
+        method zero _ = empty_ctx
 
         method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ())
 
@@ -302,22 +357,69 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
    * assignments *)
   let add_left_right_constraint (lv : typed_lvalue) (re : texpression)
       (ctx : pn_ctx) : pn_ctx =
-    (* We propagate constraints across variable reassignments: `^0 = x` *)
-    match (lv.value, re.e) with
-    | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
-        Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) ->
-        (* Use the meta-information on the right *)
-        add_constraint rmp lvar.id ctx
-    | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
-        Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _)
-      ) -> (
-        (* Use the variable name *)
-        match
-          (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx)
-        with
-        | None, Some name -> VarId.Map.add lvar.id name ctx
-        | _ -> ctx)
-    | _ -> (* Nothing to propagate *) ctx
+    (* We propagate constraints across variable reassignments: `^0 = x`,
+     * if the destination doesn't have naming information *)
+    match lv.value with
+    | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) -> (
+        if
+          (* Check that there is not already a name for teh variable *)
+          VarId.Map.mem lvar.id ctx.pure_vars
+        then ctx
+        else
+          (* We ignore the left meta-place information: it should have been taken
+           * care of by [add_left_constraint]. We try to use the right meta-place
+           * information *)
+          let add (name : string) (ctx : pn_ctx) : pn_ctx =
+            (* Add the constraint for the pure variable *)
+            let ctx = add_pure_var_constraint lvar.id name ctx in
+            (* Add the constraint for the LLBC variable *)
+            match lmp with
+            | None -> ctx
+            | Some lmp -> add_llbc_var_constraint lmp.var_id name ctx
+          in
+          match re.e with
+          | Value (rv, rmp) ->
+              (* We try to use the right-place information *)
+              let ctx =
+                match rmp with
+                | Some { var_id; name; projection = [] } -> (
+                    if Option.is_some name then add (Option.get name) ctx
+                    else
+                      match V.VarId.Map.find_opt var_id ctx.llbc_vars with
+                      | None -> ctx
+                      | Some name -> add name ctx)
+                | _ -> ctx
+              in
+              (* We try to use the rvalue information *)
+              let ctx =
+                match rv with
+                | { value = RvPlace { var = rvar_id; projection = [] }; ty = _ }
+                  -> (
+                    match VarId.Map.find_opt rvar_id ctx.pure_vars with
+                    | None -> ctx
+                    | Some name -> add name ctx)
+                | _ -> ctx
+              in
+              ctx
+          | _ -> ctx)
+    | _ -> ctx
+    (* match (lv.value, re.e) with
+       (* Case 1: *)
+       | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
+           Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) ->
+           (* Use the meta-information on the right *)
+           add_constraint rmp lvar.id ctx
+       (* Case 2: *)
+       | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
+           Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _)
+         ) -> (
+           (* Use the variable name *)
+           match
+             (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx)
+           with
+           | None, Some name -> VarId.Map.add lvar.id name ctx
+           | _ -> ctx)
+         | _ -> (* Nothing to propagate *) ctx *)
   in
 
   (* *)
@@ -350,7 +452,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   (* *)
   and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
       (e : texpression) (ctx : pn_ctx) : pn_ctx * expression =
+    (* We first add the left-constraint *)
     let ctx = add_left_constraint lv ctx in
+    (* Then we try to propagate the right-constraints to the left, in case
+     * the left constraints didn't give naming information *)
     let ctx = add_left_right_constraint lv re ctx in
     let ctx, re = update_texpression re ctx in
     let ctx, e = update_texpression e ctx in
@@ -387,8 +492,21 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) :
       pn_ctx * expression =
     match meta with
-    | Assignment (mp, rvalue) ->
+    | Assignment (mp, rvalue, rmp) ->
         let ctx = add_right_constraint mp rvalue ctx in
+        let ctx =
+          match (mp.projection, rmp) with
+          | [], Some { var_id; name; projection = [] } -> (
+              let name =
+                match name with
+                | Some name -> Some name
+                | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars
+              in
+              match name with
+              | None -> ctx
+              | Some name -> add_llbc_var_constraint mp.var_id name ctx)
+          | _ -> ctx
+        in
         let ctx, e = update_texpression e ctx in
         (ctx, e.e)
   in
@@ -405,7 +523,12 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
               | Some name -> Some (v.id, name))
             body.inputs
         in
-        let ctx = VarId.Map.of_list input_names in
+        let ctx =
+          {
+            pure_vars = VarId.Map.of_list input_names;
+            llbc_vars = V.VarId.Map.empty;
+          }
+        in
         let _, body_exp = update_texpression body.body ctx in
         Some { body with body = body_exp }
   in
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 3df91d23..5fa7d754 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -49,8 +49,8 @@ type call = {
  *)
 
 type meta =
-  | Assignment of mplace * V.typed_value
-      (** We generated an assignment (destination, assigned value) *)
+  | Assignment of mplace * V.typed_value * mplace option
+      (** We generated an assignment (destination, assigned value, src) *)
 
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
     used in CFIM: they are a first step towards lambda-calculus expressions.
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 163ddde8..65bdcf9c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -638,7 +638,11 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
             (* The meta-value stored in the shared borrow was added especially
              * for this case (because we can't use the borrow id for lookups) *)
             (translate mv).value
-        | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+        | V.InactivatedMutBorrow (mv, _) ->
+            (* Same as for shared borrows. However, note that we use inactivated borrows
+             * only in meta-data: a value actually used in the translation can't come
+             * from an unpromoted inactivated borrow *)
+            (translate mv).value
         | V.MutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
             (translate v).value)
@@ -784,9 +788,10 @@ let translate_mprojection (p : E.projection) : projection =
 
 (** Translate a "meta"-place *)
 let translate_mplace (p : S.mplace) : mplace =
+  let var_id = p.bv.index in
   let name = p.bv.name in
   let projection = translate_mprojection p.projection in
-  { name; projection }
+  { var_id; name; projection }
 
 let translate_opt_mplace (p : S.mplace option) : mplace option =
   match p with None -> None | Some p -> Some (translate_mplace p)
@@ -1434,10 +1439,11 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression)
   let next_e = translate_expression config e ctx in
   let meta =
     match meta with
-    | S.Assignment (p, rv) ->
-        let p = translate_mplace p in
+    | S.Assignment (lp, rv, rp) ->
+        let lp = translate_mplace lp in
         let rv = typed_value_to_rvalue ctx rv in
-        Assignment (p, rv)
+        let rp = translate_opt_mplace rp in
+        Assignment (lp, rv, rp)
   in
   let e = Meta (meta, next_e) in
   let ty = next_e.ty in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 785f034b..95da38e6 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -145,8 +145,8 @@ let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
   | None -> None
   | Some expr -> Some (EndAbstraction (abs, expr))
 
-let synthesize_assignment (place : mplace) (rvalue : V.typed_value)
-    (expr : expression option) : expression option =
+let synthesize_assignment (lplace : mplace) (rvalue : V.typed_value)
+    (rplace : mplace option) (expr : expression option) : expression option =
   match expr with
   | None -> None
-  | Some expr -> Some (Meta (Assignment (place, rvalue), expr))
+  | Some expr -> Some (Meta (Assignment (lplace, rvalue, rplace), expr))
diff --git a/src/Values.ml b/src/Values.ml
index 3314defb..3f1fc0bd 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -144,7 +144,7 @@ and borrow_content =
        *)
   | MutBorrow of (BorrowId.id[@opaque]) * typed_value
       (** A mutably borrowed value. *)
-  | InactivatedMutBorrow of (BorrowId.id[@opaque])
+  | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque])
       (** An inactivated mut borrow.
 
           This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html).
@@ -169,6 +169,10 @@ and borrow_content =
           l = Vec::len(move v2);
           Vec::push(move v1, move l); // In practice, v1 gets activated only here
           ```
+          
+          The meta-value is used for the same purposes as with shared borrows,
+          at the exception that in case of inactivated borrows it is not
+          *necessary* for the synthesis: we keep it only as meta-information.
        *)
 
 and loan_content =