Include SSA lhs and rhs in extended JSON trace

The full SSA identifiers will permit building tools that trace
assigned values back to inputs.

Author: tautschnig

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",
 --

src/goto-programs/goto_trace.h

@@ -118,6 +118,9 @@ class goto_trace_stept
   bool cond_value;
   exprt cond_expr;
 
+  // for assignments
+  exprt lhs, 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();
+    lhs.make_nil();
+    rhs.make_nil();
   }
 };
 

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.lhs);
+    json_assignment["ssaLhs"] = json_stringt(oss.str());
+  }
+  if(trace_options.json_full_lhs && step.rhs.is_not_nil())
+  {
+    std::ostringstream oss;
+    oss << format(step.rhs);
+    json_assignment["ssaRhs"] = json_stringt(oss.str());
+  }
 }
 
 /// Convert an OUTPUT goto_trace step.

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.lhs = SSA_step.ssa_lhs;
+        goto_trace_step.rhs = SSA_step.ssa_rhs;
+      }
+      else if(SSA_step.is_decl())
+      {
+        goto_trace_step.lhs = SSA_step.ssa_lhs;
+      }
 
       if(ssa_step_it == last_step_to_keep)
         return;