Add meta information for the variable names in SymbolicAst

7 files changed, 150 insertions, 58 deletions

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 2dd36535..77bf0bd8 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -12,6 +12,7 @@ module L = Logging
 open TypesUtils
 module Inv = Invariants
 module S = SynthesizeSymbolic
+module SA = SymbolicAst
 open Cps
 open ValuesUtils
 open InterpreterUtils
@@ -264,7 +265,8 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
   see
 
 let expand_symbolic_value_shared_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (ref_ty : T.rty) : cm_fun =
+    (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+    (ref_ty : T.rty) : cm_fun =
  fun cf ctx ->
   (* First, replace the projectors on borrows.
    * The important point is that the symbolic value to expand may appear
@@ -374,12 +376,14 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   (* Call the continuation *)
   let expr = cf ctx in
   (* Update the synthesized program *)
-  S.synthesize_symbolic_expansion_no_branching original_sv see expr
+  S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
+    expr
 
 (** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (region : T.RegionId.id T.region)
-    (ref_ty : T.rty) (rkind : T.ref_kind) : cm_fun =
+    (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+    (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
+    cm_fun =
  fun cf ctx ->
   (* Check that we are allowed to expand the reference *)
   assert (not (region_in_set region ctx.ended_regions));
@@ -407,9 +411,11 @@ let expand_symbolic_value_borrow (config : C.config)
       (* Apply the continuation *)
       let expr = cf ctx in
       (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_no_branching original_sv see expr
+      S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
+        see expr
   | T.Shared ->
-      expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx
+      expand_symbolic_value_shared_borrow config original_sv original_sv_place
+        ref_ty cf ctx
 
 (** A small helper.
 
@@ -420,7 +426,7 @@ let expand_symbolic_value_borrow (config : C.config)
     [see_cf_l]: list of pairs (optional symbolic expansion, continuation)
 *)
 let apply_branching_symbolic_expansions_non_borrow (config : C.config)
-    (sv : V.symbolic_value)
+    (sv : V.symbolic_value) (sv_place : SA.place option)
     (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun =
  fun ctx ->
   assert (see_cf_l <> []);
@@ -450,7 +456,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
   in
   (* Synthesize and return *)
   let seel = List.map fst see_cf_l in
-  S.synthesize_symbolic_expansion sv seel subterms
+  S.synthesize_symbolic_expansion sv sv_place seel subterms
 
 (** Expand a symbolic value which is not an enumeration with several variants
     (i.e., in a situation where it doesn't lead to branching).
@@ -461,7 +467,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
     TODO: rename [sp] to [sv]
  *)
 let expand_symbolic_value (config : C.config) (allow_branching : bool)
-    (sp : V.symbolic_value) : cm_fun =
+    (sp : V.symbolic_value) (sp_place : SA.place option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
@@ -470,6 +476,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sp in
+  let original_sv_place = sp_place in
   let rty = original_sv.V.sv_ty in
   let cc : cm_fun =
    fun cf ctx ->
@@ -485,8 +492,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         assert (List.length seel <= 1 || allow_branching);
         (* Apply *)
         let seel = List.map (fun see -> (Some see, cf)) seel in
-        apply_branching_symbolic_expansions_non_borrow config original_sv seel
-          ctx
+        apply_branching_symbolic_expansions_non_borrow config original_sv
+          original_sv_place seel ctx
     (* Tuples *)
     | T.Adt (T.Tuple, [], tys) ->
         (* Generate the field values *)
@@ -498,7 +505,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         (* Call the continuation *)
         let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv see expr
+        S.synthesize_symbolic_expansion_no_branching original_sv
+          original_sv_place see expr
     (* Boxes *)
     | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
         let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
@@ -509,11 +517,12 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         (* Call the continuation *)
         let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv see expr
+        S.synthesize_symbolic_expansion_no_branching original_sv
+          original_sv_place see expr
     (* Borrows *)
     | T.Ref (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv region ref_ty rkind cf
-          ctx
+        expand_symbolic_value_borrow config original_sv original_sv_place region
+          ref_ty rkind cf ctx
     (* Booleans *)
     | T.Bool ->
         assert allow_branching;
@@ -523,8 +532,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         let seel = [ see_true; see_false ] in
         let seel = List.map (fun see -> (Some see, cf)) seel in
         (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-        apply_branching_symbolic_expansions_non_borrow config original_sv seel
-          ctx
+        apply_branching_symbolic_expansions_non_borrow config original_sv
+          original_sv_place seel ctx
     | _ -> failwith ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)
   in
   (* Debug *)
@@ -569,8 +578,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     switch. The continuation is thus for the execution *after* the switch.
 *)
 let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
-    (int_type : T.integer_type) (tgts : (V.scalar_value * m_fun) list)
-    (otherwise : m_fun) : m_fun =
+    (sv_place : SA.place option) (int_type : T.integer_type)
+    (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun =
   (* Sanity check *)
   assert (sv.V.sv_ty = T.Integer int_type);
   (* For all the branches of the switch, we expand the symbolic value
@@ -587,13 +596,13 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
   in
   let tgts = List.append tgts [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
-  apply_branching_symbolic_expansions_non_borrow config sv tgts
+  apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts
 
 (** See [expand_symbolic_value] *)
 let expand_symbolic_value_no_branching (config : C.config)
-    (sp : V.symbolic_value) : cm_fun =
+    (sv : V.symbolic_value) (sv_place : SA.place option) : cm_fun =
   let allow_branching = false in
-  expand_symbolic_value config allow_branching sp
+  expand_symbolic_value config allow_branching sv sv_place
 
 (** Expand all the symbolic values which contain borrows.
     Allows us to restrict ourselves to a simpler model for the projectors over
@@ -649,10 +658,10 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
                 ("Attempted to greedily expand a recursive definition (option \
                   [greedy_expand_symbolics_with_borrows] of [config]): "
                 ^ Print.name_to_string def.name)
-            else expand_symbolic_value_no_branching config sv
+            else expand_symbolic_value_no_branching config sv None
         | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching config sv
+            expand_symbolic_value_no_branching config sv None
         | T.Array _ -> raise Errors.Unimplemented
         | T.Slice _ -> failwith "Can't expand symbolic slices"
         | T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 84f51c94..356bae2d 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -39,7 +39,9 @@ let expand_primitively_copyable_at_place (config : C.config)
     with
     | None -> cf ctx
     | Some sv ->
-        let cc = expand_symbolic_value_no_branching config sv in
+        let cc =
+          expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx))
+        in
         comp cc expand cf ctx
   in
   (* Apply *)
@@ -290,7 +292,9 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
     (* Call the continuation *)
     let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
     (* Synthesize the symbolic AST *)
-    S.synthesize_unary_op unop v res_sv expr
+    S.synthesize_unary_op unop v
+      (S.mk_opt_place_from_op op ctx)
+      res_sv None expr
   in
   (* Compose and apply *)
   comp eval_op apply cf ctx
@@ -427,7 +431,9 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
     let v = mk_typed_value_from_symbolic_value res_sv in
     let expr = cf (Ok v) ctx in
     (* Synthesize the symbolic AST *)
-    S.synthesize_binary_op binop v1 v2 res_sv expr
+    let p1 = S.mk_opt_place_from_op op1 ctx in
+    let p2 = S.mk_opt_place_from_op op2 ctx in
+    S.synthesize_binary_op binop v1 p1 v2 p2 res_sv None expr
   in
   (* Compose and apply *)
   comp eval_ops compute cf ctx
@@ -488,7 +494,10 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
     | Symbolic sv ->
         (* Expand the symbolic value - may lead to branching *)
         let allow_branching = true in
-        let cc = expand_symbolic_value config allow_branching sv in
+        let cc =
+          expand_symbolic_value config allow_branching sv
+            (Some (S.mk_place p ctx))
+        in
         (* This time the value is concrete: reevaluate *)
         comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
     | _ -> failwith "Invalid input for `discriminant`"
@@ -584,7 +593,7 @@ let eval_rvalue_aggregate (config : C.config)
         (* Call the continuation *)
         let expr = cf aggregated ctx in
         (* Synthesize the symbolic AST *)
-        S.synthesize_aggregated_value aggregated expr
+        S.synthesize_aggregated_value aggregated None expr
     | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
         (* Sanity checks *)
         let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -605,7 +614,7 @@ let eval_rvalue_aggregate (config : C.config)
         (* Call the continuation *)
         let expr = cf aggregated ctx in
         (* Synthesize the symbolic AST *)
-        S.synthesize_aggregated_value aggregated expr
+        S.synthesize_aggregated_value aggregated None expr
   in
   (* Compose and apply *)
   comp eval_ops compute cf
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 300e50c5..8b103eb8 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -11,6 +11,7 @@ open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterBorrows
 open InterpreterExpansion
+module Synth = SynthesizeSymbolic
 
 (** The local logger *)
 let log = L.paths_log
@@ -473,6 +474,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config sp
+              (Some (Synth.mk_place p ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand [Bottom] values while reading them *)
             failwith "Found [Bottom] while reading a place"
@@ -502,6 +504,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config sp
+              (Some (Synth.mk_place p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the [Bottom] value *)
             fun cf ctx ->
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index b0d4e5e0..16c66094 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -155,7 +155,10 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
         (* Expand the symbolic value, then call the evaluation function for the
          * non-symbolic case *)
         let allow_branching = true in
-        let expand = expand_symbolic_value config allow_branching sv in
+        let expand =
+          expand_symbolic_value config allow_branching sv
+            (S.mk_opt_place_from_op assertion.cond ctx)
+        in
         comp expand (eval_assertion_concrete config assertion) cf ctx
     | _ -> failwith ("Expected a boolean, got: " ^ typed_value_to_string ctx v)
   in
@@ -804,6 +807,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 (** Evaluate a switch *)
 and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
     st_cm_fun =
+ fun cf ctx ->
   (* We evaluate the operand in two steps:
    * first we prepare it, then we check if its value is concrete or
    * symbolic. If it is concrete, we can then evaluate the operand
@@ -816,6 +820,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
   let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in
   (* Match on the targets *)
   let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
+   fun ctx ->
     match tgts with
     | A.If (st1, st2) -> (
         match op_v.value with
@@ -830,17 +835,19 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
               else eval_statement config st2 cf
             in
             (* Compose the continuations *)
-            comp cf_eval_op cf_branch cf
+            comp cf_eval_op cf_branch cf ctx
         | V.Symbolic sv ->
             (* Expand the symbolic value *)
             let allows_branching = true in
             let cf_expand cf =
-              expand_symbolic_value config allows_branching sv cf
+              expand_symbolic_value config allows_branching sv
+                (S.mk_opt_place_from_op op ctx)
+                cf
             in
             (* Retry *)
             let cf_eval_if cf = eval_switch config op tgts cf in
             (* Compose *)
-            comp cf_expand cf_eval_if cf
+            comp cf_expand cf_eval_if cf ctx
         | _ -> failwith "Inconsistent state")
     | A.SwitchInt (int_ty, stgts, otherwise) -> (
         match op_v.value with
@@ -858,7 +865,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
               | Some (_, tgt) -> eval_statement config tgt cf
             in
             (* Compose *)
-            comp cf_eval_op cf_eval_branch cf
+            comp cf_eval_op cf_eval_branch cf ctx
         | V.Symbolic sv ->
             (* Expand the symbolic value - note that contrary to the boolean
              * case, we can't expand then retry, because when switching over
@@ -871,11 +878,13 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
                 stgts
             in
             let otherwise = eval_statement config otherwise cf in
-            expand_symbolic_int config sv int_ty stgts otherwise
+            expand_symbolic_int config sv
+              (S.mk_opt_place_from_op op ctx)
+              int_ty stgts otherwise ctx
         | _ -> failwith "Inconsistent state")
   in
   (* Compose the continuations *)
-  comp cf_prepare_op cf_match
+  comp cf_prepare_op cf_match cf ctx
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
 and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
@@ -992,6 +1001,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   let ret_av regions =
     mk_aproj_loans_value_from_symbolic_value regions ret_spc
   in
+  let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in
+  let dest_place = Some (S.mk_place dest ctx) in
 
   (* Evaluate the input operands *)
   let cc = eval_operands config args in
@@ -1047,7 +1058,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (* Synthesize the symbolic AST *)
     let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in
     S.synthesize_regular_function_call fid call_id abs_ids type_params args
-      ret_spc expr
+      args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
 
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 3d41e67d..b631f940 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -183,7 +183,7 @@ let type_def_to_string (fmt : type_formatter) (def : type_def) : string =
       "enum " ^ name ^ params ^ " =\n" ^ variants
 
 let var_to_string (fmt : type_formatter) (v : var) : string =
-  "(" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")"
+  "(@" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")"
 
 let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string =
   match v with
@@ -218,7 +218,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
               "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
 
 let place_to_string (fmt : ast_formatter) (p : place) : string =
-  let var = fmt.var_id_to_string p.var in
+  let var = "@" ^ fmt.var_id_to_string p.var in
   projection_to_string fmt var p.projection
 
 let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index f0873aa3..a3aedeab 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -9,6 +9,25 @@ module V = Values
 module E = Expressions
 module A = CfimAst
 
+type place = {
+  bv : Contexts.binder;
+      (** It is important that we store the binder, and not just the variable id,
+          because the most important information in a place is the name of the
+          variable!
+       *)
+  projection : E.projection;
+      (** We store the projection because we can, but it is actually not that useful *)
+}
+(** In this module, [place] is meta information.
+
+    Whenever we need to introduce new symbolic variables, for instance because
+    of symbolic expansions, we try to store a "place", which gives information
+    about the origin of the values (this place information comes from assignment
+    information, etc.).
+    We later use this place information to generate meaningful name, to prettify
+    the generated code.
+ *)
+
 type call_id =
   | Fun of A.fun_id * V.FunCallId.id
       (** A "regular" function (i.e., a function which is not a primitive operation) *)
@@ -21,7 +40,9 @@ type call = {
   abstractions : V.AbstractionId.id list;
   type_params : T.ety list;
   args : V.typed_value list;
+  args_places : place option list;  (** Meta information *)
   dest : V.symbolic_value;
+  dest_place : place option;  (** Meta information *)
 }
 
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
@@ -37,7 +58,15 @@ type expression =
   | Panic
   | FunCall of call * expression
   | EndAbstraction of V.abs * expression
-  | Expansion of V.symbolic_value * expansion
+  | Expansion of place option * V.symbolic_value * expansion
+      (** Expansion of a symbolic value.
+    
+          The place is "meta": it gives the path to the symbolic value (if available)
+          which got expanded (this path is available when the symbolic expansion
+          comes from a path evaluation, during an assignment for instance).
+          We use it to compute meaningful names for the variables we introduce,
+          to prettify the generated code.
+       *)
   | Meta of meta * expression  (** Meta information *)
 
 and expansion =
@@ -63,4 +92,6 @@ and expansion =
     generate a pretty output.
  *)
 
-and meta = Aggregate of V.typed_value  (** We generated an aggregate value *)
+and meta =
+  | Aggregate of place option * V.typed_value
+      (** We generated an aggregate value *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 6aec95bd..7050c14b 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -5,7 +5,20 @@ module E = Expressions
 module A = CfimAst
 open SymbolicAst
 
-let synthesize_symbolic_expansion (sv : V.symbolic_value)
+let mk_place (p : E.place) (ctx : Contexts.eval_ctx) : place =
+  let bv = Contexts.ctx_lookup_binder ctx p.var_id in
+  { bv; projection = p.projection }
+
+let mk_opt_place (p : E.place option) (ctx : Contexts.eval_ctx) : place option =
+  match p with None -> None | Some p -> Some (mk_place p ctx)
+
+let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) :
+    place option =
+  match op with
+  | E.Copy p | E.Move p -> Some (mk_place p ctx)
+  | E.Constant _ -> None
+
+let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option)
     (seel : V.symbolic_expansion option list) (exprl : expression list option) :
     expression option =
   match exprl with
@@ -71,46 +84,62 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
         | T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
             failwith "Ill-formed symbolic expansion"
       in
-      Some (Expansion (sv, expansion))
+      Some (Expansion (place, sv, expansion))
 
 let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
-    (see : V.symbolic_expansion) (expr : expression option) : expression option
-    =
+    (place : place option) (see : V.symbolic_expansion)
+    (expr : expression option) : expression option =
   let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
-  synthesize_symbolic_expansion sv [ Some see ] exprl
+  synthesize_symbolic_expansion sv place [ Some see ] exprl
 
 let synthesize_function_call (call_id : call_id)
     (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
-    (args : V.typed_value list) (dest : V.symbolic_value)
+    (args : V.typed_value list) (args_places : place option list)
+    (dest : V.symbolic_value) (dest_place : place option)
     (expr : expression option) : expression option =
   match expr with
   | None -> None
   | Some expr ->
-      let call = { call_id; abstractions; type_params; args; dest } in
+      let call =
+        {
+          call_id;
+          abstractions;
+          type_params;
+          args;
+          dest;
+          args_places;
+          dest_place;
+        }
+      in
       Some (FunCall (call, expr))
 
 let synthesize_regular_function_call (fun_id : A.fun_id)
     (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
     (type_params : T.ety list) (args : V.typed_value list)
-    (dest : V.symbolic_value) (expr : expression option) : expression option =
+    (args_places : place option list) (dest : V.symbolic_value)
+    (dest_place : place option) (expr : expression option) : expression option =
   synthesize_function_call
     (Fun (fun_id, call_id))
-    abstractions type_params args dest expr
+    abstractions type_params args args_places dest dest_place expr
 
 let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
-    (dest : V.symbolic_value) (expr : expression option) : expression option =
-  synthesize_function_call (Unop unop) [] [] [ arg ] dest expr
+    (arg_place : place option) (dest : V.symbolic_value)
+    (dest_place : place option) (expr : expression option) : expression option =
+  synthesize_function_call (Unop unop) [] [] [ arg ] [ arg_place ] dest
+    dest_place expr
 
 let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
-    (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
-    : expression option =
-  synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr
+    (arg0_place : place option) (arg1 : V.typed_value)
+    (arg1_place : place option) (dest : V.symbolic_value)
+    (dest_place : place option) (expr : expression option) : expression option =
+  synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ]
+    [ arg0_place; arg1_place ] dest dest_place expr
 
-let synthesize_aggregated_value (aggr_v : V.typed_value)
+let synthesize_aggregated_value (aggr_v : V.typed_value) (place : place option)
     (expr : expression option) : expression option =
   match expr with
   | None -> None
-  | Some expr -> Some (Meta (Aggregate aggr_v, expr))
+  | Some expr -> Some (Meta (Aggregate (place, aggr_v), expr))
 
 let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
     expression option =