Rename the meta-places to [mplace] and update some comments

8 files changed, 65 insertions, 41 deletions

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 77bf0bd8..625c63ef 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -265,7 +265,7 @@ 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) (original_sv_place : SA.place option)
+    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : T.rty) : cm_fun =
  fun cf ctx ->
   (* First, replace the projectors on borrows.
@@ -381,7 +381,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
 
 (** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
     (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
     cm_fun =
  fun cf ctx ->
@@ -426,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_place : SA.place option)
+    (sv : V.symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun =
  fun ctx ->
   assert (see_cf_l <> []);
@@ -467,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) (sp_place : SA.place option) : cm_fun =
+    (sp : V.symbolic_value) (sp_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
@@ -578,7 +578,7 @@ 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)
-    (sv_place : SA.place option) (int_type : T.integer_type)
+    (sv_place : SA.mplace 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);
@@ -600,7 +600,7 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
 
 (** See [expand_symbolic_value] *)
 let expand_symbolic_value_no_branching (config : C.config)
-    (sv : V.symbolic_value) (sv_place : SA.place option) : cm_fun =
+    (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
   let allow_branching = false in
   expand_symbolic_value config allow_branching sv sv_place
 
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 356bae2d..34bfd574 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -40,7 +40,8 @@ let expand_primitively_copyable_at_place (config : C.config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx))
+          expand_symbolic_value_no_branching config sv
+            (Some (S.mk_mplace p ctx))
         in
         comp cc expand cf ctx
   in
@@ -496,7 +497,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
         let allow_branching = true in
         let cc =
           expand_symbolic_value config allow_branching sv
-            (Some (S.mk_place p ctx))
+            (Some (S.mk_mplace p ctx))
         in
         (* This time the value is concrete: reevaluate *)
         comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 361ff981..bfb1aee3 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -482,7 +482,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
             in
             let prefix = { p with projection = proj } in
             expand_symbolic_value_no_branching config sp
-              (Some (Synth.mk_place prefix ctx))
+              (Some (Synth.mk_mplace prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand [Bottom] values while reading them *)
             failwith "Found [Bottom] while reading a place"
@@ -512,7 +512,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))
+              (Some (Synth.mk_mplace 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 16c66094..a1c58851 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -1002,7 +1002,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     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
+  let dest_place = Some (S.mk_mplace dest ctx) in
 
   (* Evaluate the input operands *)
   let cc = eval_operands config args in
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index f35ee2d6..cd64a288 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -33,11 +33,30 @@ open Pure
         }
       }
       ```
-      If `ls` maps to a symbolic value upon evaluating the match in symbolic
+      If `ls` maps to a symbolic value `s0` upon evaluating the match in symbolic
       mode, we expand this value upon evaluating `tmp = discriminant(ls)`.
       However, at this point, we don't know which should be the names of
-      the symbolic values we introduce for the fields of `Cons`! Still,
+      the symbolic values we introduce for the fields of `Cons`!
+      Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`.
+      The assigments lead to the following binding in the evaluation context:
+      ```
+      x -> s1
+      hd -> s2
+      ```
+      
+      If at any moment we use `x` (as an operand to a function, to return,
+      etc.) we ...
+      TODO: finish explanations
+      TODO: meta-information for:
+      - unop
+      - binop
+      - assignments
+      - discriminant
+      - ...
+      
       the subsequent assignments actually give us the naming information we
       were looking for.
+   - TODO: temporaries for binops which can fail/have preconditions
+   - TODO: reborrows just before calling functions.
  *)
 let compute_pretty_names () = ()
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index a3aedeab..c9ab87e0 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -9,7 +9,7 @@ module V = Values
 module E = Expressions
 module A = CfimAst
 
-type place = {
+type mplace = {
   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
@@ -18,7 +18,7 @@ type place = {
   projection : E.projection;
       (** We store the projection because we can, but it is actually not that useful *)
 }
-(** In this module, [place] is meta information.
+(** "Meta"-place: a place stored as meta-data.
 
     Whenever we need to introduce new symbolic variables, for instance because
     of symbolic expansions, we try to store a "place", which gives information
@@ -40,9 +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 *)
+  args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
-  dest_place : place option;  (** Meta information *)
+  dest_place : mplace option;  (** Meta information *)
 }
 
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
@@ -58,7 +58,7 @@ type expression =
   | Panic
   | FunCall of call * expression
   | EndAbstraction of V.abs * expression
-  | Expansion of place option * V.symbolic_value * expansion
+  | Expansion of mplace option * V.symbolic_value * expansion
       (** Expansion of a symbolic value.
     
           The place is "meta": it gives the path to the symbolic value (if available)
@@ -93,5 +93,5 @@ and expansion =
  *)
 
 and meta =
-  | Aggregate of place option * V.typed_value
+  | Aggregate of mplace option * V.typed_value
       (** We generated an aggregate value *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 5a3b3e96..63d0df1d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -743,12 +743,12 @@ let translate_mprojection (p : E.projection) : projection =
   List.filter_map translate_mprojection_elem p
 
 (** Translate a "meta"-place *)
-let translate_mplace (p : S.place) : mplace =
+let translate_mplace (p : S.mplace) : mplace =
   let name = p.bv.name in
   let projection = translate_mprojection p.projection in
   { name; projection }
 
-let translate_opt_mplace (p : S.place option) : mplace option =
+let translate_opt_mplace (p : S.mplace option) : mplace option =
   match p with None -> None | Some p -> Some (translate_mplace p)
 
 (** Explore an abstraction value and convert it to a given back value
@@ -1118,7 +1118,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
               e ))
         given_back_inputs e
 
-and translate_expansion (p : S.place option) (sv : V.symbolic_value)
+and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
     (exp : S.expansion) (ctx : bs_ctx) : expression =
   (* Translate the scrutinee *)
   let scrutinee_var = lookup_var_for_symbolic_value sv ctx in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 7050c14b..7ba1da7f 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -5,22 +5,23 @@ module E = Expressions
 module A = CfimAst
 open SymbolicAst
 
-let mk_place (p : E.place) (ctx : Contexts.eval_ctx) : place =
+let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace =
   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_mplace (p : E.place option) (ctx : Contexts.eval_ctx) : mplace option
+    =
+  match p with None -> None | Some p -> Some (mk_mplace p ctx)
 
 let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) :
-    place option =
+    mplace option =
   match op with
-  | E.Copy p | E.Move p -> Some (mk_place p ctx)
+  | E.Copy p | E.Move p -> Some (mk_mplace 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 =
+let synthesize_symbolic_expansion (sv : V.symbolic_value)
+    (place : mplace option) (seel : V.symbolic_expansion option list)
+    (exprl : expression list option) : expression option =
   match exprl with
   | None -> None
   | Some exprl ->
@@ -87,15 +88,15 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option)
       Some (Expansion (place, sv, expansion))
 
 let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
-    (place : place option) (see : V.symbolic_expansion)
+    (place : mplace 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 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) (args_places : place option list)
-    (dest : V.symbolic_value) (dest_place : place option)
+    (args : V.typed_value list) (args_places : mplace option list)
+    (dest : V.symbolic_value) (dest_place : mplace option)
     (expr : expression option) : expression option =
   match expr with
   | None -> None
@@ -116,26 +117,29 @@ let synthesize_function_call (call_id : call_id)
 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)
-    (args_places : place option list) (dest : V.symbolic_value)
-    (dest_place : place option) (expr : expression option) : expression option =
+    (args_places : mplace option list) (dest : V.symbolic_value)
+    (dest_place : mplace option) (expr : expression option) : expression option
+    =
   synthesize_function_call
     (Fun (fun_id, call_id))
     abstractions type_params args args_places dest dest_place expr
 
 let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
-    (arg_place : place option) (dest : V.symbolic_value)
-    (dest_place : place option) (expr : expression option) : expression option =
+    (arg_place : mplace option) (dest : V.symbolic_value)
+    (dest_place : mplace 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)
-    (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 =
+    (arg0_place : mplace option) (arg1 : V.typed_value)
+    (arg1_place : mplace option) (dest : V.symbolic_value)
+    (dest_place : mplace 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) (place : place option)
+let synthesize_aggregated_value (aggr_v : V.typed_value) (place : mplace option)
     (expr : expression option) : expression option =
   match expr with
   | None -> None