From 617ef0d6df4778356536d5bb70fd771c5754c5a8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 17 Jul 2019 00:50:33 +0000
Subject: [PATCH] Include SSA lhs and rhs in extended JSON trace

The full SSA identifiers will permit building tools that trace
assigned values back to inputs.
---
 .../trace_options_json_extended/extended.desc     |  2 ++
 src/goto-programs/goto_trace.h                    |  5 +++++
 src/goto-programs/json_goto_trace.cpp             | 15 +++++++++++++++
 src/goto-symex/build_goto_trace.cpp               |  9 +++++++++
 4 files changed, 31 insertions(+)

diff --git a/regression/cbmc/trace_options_json_extended/extended.desc b/regression/cbmc/trace_options_json_extended/extended.desc
index 51bef1274d1..d9313d36d34 100644
--- a/regression/cbmc/trace_options_json_extended/extended.desc
+++ b/regression/cbmc/trace_options_json_extended/extended.desc
@@ -4,4 +4,6 @@ test.c
 ^EXIT=10$
 ^SIGNAL=0$
 rawLhs
+"ssaLhs": "main::argc!0@1#1",
+"ssaRhs": "argc'#0",
 --
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index 2b6dd26ad28..ae826221e97 100644
--- a/src/goto-programs/goto_trace.h
+++ b/src/goto-programs/goto_trace.h
@@ -118,6 +118,9 @@ class goto_trace_stept
   bool cond_value;
   exprt cond_expr;
 
+  // for assignments and declarations (ssa_lhs only)
+  exprt ssa_lhs, ssa_rhs;
+
   // for assert
   irep_idt property_id;
   std::string comment;
@@ -161,6 +164,8 @@ class goto_trace_stept
     full_lhs.make_nil();
     full_lhs_value.make_nil();
     cond_expr.make_nil();
+    ssa_lhs.make_nil();
+    ssa_rhs.make_nil();
   }
 };
 
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index ca9267f84b5..61917b0f99b 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -14,8 +14,10 @@ Author: Daniel Kroening
 #include "json_goto_trace.h"
 
 #include <langapi/language_util.h>
+
 #include <util/arith_tools.h>
 #include <util/config.h>
+#include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
 
@@ -154,6 +156,19 @@ void convert_decl(
     step.assignment_type == goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
       ? "actual-parameter"
       : "variable");
+
+  if(trace_options.json_full_lhs)
+  {
+    std::ostringstream oss;
+    oss << format(step.ssa_lhs);
+    json_assignment["ssaLhs"] = json_stringt(oss.str());
+  }
+  if(trace_options.json_full_lhs && step.ssa_rhs.is_not_nil())
+  {
+    std::ostringstream oss;
+    oss << format(step.ssa_rhs);
+    json_assignment["ssaRhs"] = json_stringt(oss.str());
+  }
 }
 
 /// Convert an OUTPUT goto_trace step.
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 60be0403b6e..c058d32a122 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -407,6 +407,15 @@ void build_goto_trace(
         goto_trace_step.cond_value =
           decision_procedure.get(SSA_step.cond_handle).is_true();
       }
+      else if(SSA_step.is_assignment())
+      {
+        goto_trace_step.ssa_lhs = SSA_step.ssa_lhs;
+        goto_trace_step.ssa_rhs = SSA_step.ssa_rhs;
+      }
+      else if(SSA_step.is_decl())
+      {
+        goto_trace_step.ssa_lhs = SSA_step.ssa_lhs;
+      }
 
       if(ssa_step_it == last_step_to_keep)
         return;