Generate meta-information for the assignments

5 files changed, 69 insertions, 17 deletions

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index e31a2152..09f13240 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -730,11 +730,22 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
         let cf_assign cf (res : (V.typed_value, eval_error) result) ctx =
           match res with
           | Error EPanic -> cf Panic ctx
-          | Ok rvalue ->
-              let expr = assign_to_place config rvalue p (cf Unit) ctx in
-              (* Update the synthesized AST - here we store meta-information *)
-              S.synthesize_assignment (S.mk_mplace p ctx) rvalue expr
+          | Ok rv -> (
+              let expr = assign_to_place config rv p (cf Unit) ctx in
+              (* Update the synthesized AST - here we store meta-information.
+               * We do it only in specific cases (it is not always useful, and
+               * also it can lead to issues - for instance, if we borrow an
+               * inactivated borrow, we later can't translate it to pure values...) *)
+              match rvalue with
+              | E.Use _
+              | E.Ref (_, (E.Shared | E.Mut))
+              | 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)
         in
+
         (* Compose and apply *)
         comp cf_eval_rvalue cf_assign cf ctx
     | A.FakeRead p ->
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 6f56c379..5223fb21 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -333,6 +333,23 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
   | Binop (binop, int_ty) ->
       binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">"
 
+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 meta_to_string (fmt : ast_formatter) (meta : meta) : string =
+  let meta =
+    match meta with
+    | Aggregate (p, rv) ->
+        let p = match p with None -> "_" | Some p -> mplace_to_string fmt p in
+        "@aggregate(" ^ p ^ " := " ^ typed_rvalue_to_string fmt rv ^ ")"
+    | Assignment (p, rv) ->
+        "@assign(" ^ mplace_to_string fmt p ^ " := "
+        ^ typed_rvalue_to_string fmt rv
+        ^ ")"
+  in
+  "@meta[" ^ meta ^ "]"
+
 let rec expression_to_string (fmt : ast_formatter) (indent : string)
     (indent_incr : string) (e : expression) : string =
   match e with
@@ -341,6 +358,10 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string)
   | Let (lb, e) -> let_to_string fmt indent indent_incr lb e
   | Switch (scrutinee, _, body) ->
       switch_to_string fmt indent indent_incr scrutinee body
+  | Meta (meta, e) ->
+      let meta = meta_to_string fmt meta in
+      let e = expression_to_string fmt indent indent_incr e in
+      indent ^ meta ^ "\n" ^ e
 
 and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
     (lb : let_bindings) (e : expression) : string =
diff --git a/src/Pure.ml b/src/Pure.ml
index ba0c9837..89748bdd 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -200,6 +200,11 @@ type let_bindings =
           code if we detect there is exactly one variant?...
        *)
 
+(** Meta-information stored in the AST *)
+type meta =
+  | Aggregate of mplace option * typed_rvalue
+  | Assignment of mplace * typed_rvalue
+
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
     used in CFIM. They are lambda-calculus expressions, and are thus actually
     more general than the CFIM statements, in a sense.
@@ -215,6 +220,7 @@ type expression =
   | Let of let_bindings * expression
       (** Let bindings include the let-bindings introduced because of function calls *)
   | Switch of typed_rvalue * mplace option * switch_body
+  | Meta of meta * expression  (** Meta-information *)
 
 and switch_body =
   | If of expression * expression
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 3148f833..07afd914 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -45,6 +45,16 @@ type call = {
   dest_place : mplace option;  (** Meta information *)
 }
 
+(** Meta information, not necessary for synthesis but useful to guide it to
+    generate a pretty output.
+ *)
+
+type meta =
+  | Aggregate of mplace option * V.typed_value
+      (** We generated an aggregate value *)
+  | Assignment of mplace * V.typed_value
+      (** We generated an assignment (destination, assigned value) *)
+
 (** **Rk.:** here, [expression] is not at all equivalent to the expressions
     used in CFIM: they are a first step towards lambda-calculus expressions.
  *)
@@ -87,13 +97,3 @@ and expansion =
       T.integer_type * (V.scalar_value * expression) list * expression
       (** An integer expansion (i.e, a switch over an integer). The last
           expression is for the "otherwise" branch. *)
-
-(** Meta information, not necessary for synthesis but useful to guide it to
-    generate a pretty output.
- *)
-
-and meta =
-  | Aggregate of mplace option * V.typed_value
-      (** We generated an aggregate value *)
-  | Assignment of mplace * V.typed_value
-      (** We generated an assignment (destination, assigned value) *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 63d0df1d..4fa8e54c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -879,9 +879,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
   | FunCall (call, e) -> translate_function_call call e ctx
   | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
-  | Meta (_, e) ->
-      (* We ignore the meta information *)
-      translate_expression e ctx
+  | Meta (meta, e) -> translate_meta meta e ctx
 
 and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : expression
     =
@@ -1243,6 +1241,22 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       Switch
         (scrutinee, scrutinee_mplace, SwitchInt (int_ty, branches, otherwise))
 
+and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+    expression =
+  let e = translate_expression e ctx in
+  let meta =
+    match meta with
+    | S.Aggregate (p, rv) ->
+        let p = translate_opt_mplace p in
+        let rv = typed_value_to_rvalue ctx rv in
+        Aggregate (p, rv)
+    | S.Assignment (p, rv) ->
+        let p = translate_mplace p in
+        let rv = typed_value_to_rvalue ctx rv in
+        Assignment (p, rv)
+  in
+  Meta (meta, e)
+
 let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
   let def = ctx.fun_def in
   let bid = ctx.bid in