From 4fcc9f5ca26bec31d1c4d6ead1578e96337dd329 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 00:02:15 +0100
Subject: Generate meta-information for the assignments

---
 src/InterpreterStatements.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'src/InterpreterStatements.ml')

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 ->
-- 
cgit v1.2.3