From 777f54fa007dfc0ec92cf8e7c6b7c36931775d68 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 23:44:08 +0100
Subject: Generate meta-information for assignments in the symbolic AST

---
 src/InterpreterStatements.ml | 38 +++++++++++++++++++++-----------------
 src/SymbolicAst.ml           |  2 ++
 src/SynthesizeSymbolic.ml    |  6 ++++++
 3 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index a1c58851..e31a2152 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -721,33 +721,37 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
+   fun ctx ->
     match st with
     | A.Assign (p, rvalue) ->
         (* Evaluate the rvalue *)
         let cf_eval_rvalue = eval_rvalue config rvalue in
         (* Assign *)
-        let cf_assign cf (res : (V.typed_value, eval_error) result) =
+        let cf_assign cf (res : (V.typed_value, eval_error) result) ctx =
           match res with
-          | Error EPanic -> cf Panic
-          | Ok rvalue -> assign_to_place config rvalue p (cf Unit)
+          | 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
         in
         (* Compose and apply *)
-        comp cf_eval_rvalue cf_assign cf
+        comp cf_eval_rvalue cf_assign cf ctx
     | A.FakeRead p ->
         let expand_prim_copy = false in
         let cf_prepare = prepare_rplace config expand_prim_copy Read p in
         let cf_continue cf _ = cf in
-        comp cf_prepare cf_continue (cf Unit)
+        comp cf_prepare cf_continue (cf Unit) ctx
     | A.SetDiscriminant (p, variant_id) ->
-        set_discriminant config p variant_id cf
-    | A.Drop p -> drop_value config p (cf Unit)
-    | A.Assert assertion -> eval_assertion config assertion cf
-    | A.Call call -> eval_function_call config call cf
-    | A.Panic -> cf Panic
-    | A.Return -> cf Return
-    | A.Break i -> cf (Break i)
-    | A.Continue i -> cf (Continue i)
-    | A.Nop -> cf Unit
+        set_discriminant config p variant_id cf ctx
+    | A.Drop p -> drop_value config p (cf Unit) ctx
+    | A.Assert assertion -> eval_assertion config assertion cf ctx
+    | A.Call call -> eval_function_call config call cf ctx
+    | A.Panic -> cf Panic ctx
+    | A.Return -> cf Return ctx
+    | A.Break i -> cf (Break i) ctx
+    | A.Continue i -> cf (Continue i) ctx
+    | A.Nop -> cf Unit ctx
     | A.Sequence (st1, st2) ->
         (* Evaluate the first statement *)
         let cf_st1 = eval_statement config st1 in
@@ -760,7 +764,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
           | Panic | Break _ | Continue _ | Return -> cf res
         in
         (* Compose and apply *)
-        comp cf_st1 cf_st2 cf
+        comp cf_st1 cf_st2 cf ctx
     | A.Loop loop_body ->
         (* For now, we don't support loops in symbolic mode *)
         assert (config.C.mode = C.ConcreteMode);
@@ -798,8 +802,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
               failwith "Unreachable"
         in
         (* Apply *)
-        eval_statement config loop_body reeval_loop_body
-    | A.Switch (op, tgts) -> eval_switch config op tgts cf
+        eval_statement config loop_body reeval_loop_body ctx
+    | A.Switch (op, tgts) -> eval_switch config op tgts cf ctx
   in
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index c9ab87e0..3148f833 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -95,3 +95,5 @@ and expansion =
 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/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 7ba1da7f..f86d40f0 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -150,3 +150,9 @@ let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
   match expr with
   | None -> None
   | Some expr -> Some (EndAbstraction (abs, expr))
+
+let synthesize_assignment (place : mplace) (rvalue : V.typed_value)
+    (expr : expression option) : expression option =
+  match expr with
+  | None -> None
+  | Some expr -> Some (Meta (Assignment (place, rvalue), expr))
-- 
cgit v1.2.3