Merge pull request #1694 from NathanJPhillips/feature/add-raw-lhs-to-trace

smowton · web-flow · commit 85193a0e32bd · 2018-01-09T11:04:20.000Z
Add raw irept dump of lhs to trace
diff --git a/regression/cbmc-java/trace_options_json_extended/Test.class b/regression/cbmc-java/trace_options_json_extended/Test.class
diff --git a/regression/cbmc-java/trace_options_json_extended/Test.java b/regression/cbmc-java/trace_options_json_extended/Test.java
@@ -0,0 +1,5 @@
+public class Test {
+    public static void main(int x) {
+        assert(x == 0);
+    }
+}
diff --git a/regression/cbmc-java/trace_options_json_extended/extended.desc b/regression/cbmc-java/trace_options_json_extended/extended.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--trace --json-ui --trace-json-extended
+^EXIT=10$
+^SIGNAL=0$
+rawLhs
+--
diff --git a/regression/cbmc-java/trace_options_json_extended/non-extended.desc b/regression/cbmc-java/trace_options_json_extended/non-extended.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--trace --json-ui
+^EXIT=10$
+^SIGNAL=0$
+--
+rawLhs
diff --git a/regression/cbmc/trace_options_json_extended/extended.desc b/regression/cbmc/trace_options_json_extended/extended.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--trace --json-ui --trace-json-extended
+^EXIT=10$
+^SIGNAL=0$
+rawLhs
+--
diff --git a/regression/cbmc/trace_options_json_extended/non-extended.desc b/regression/cbmc/trace_options_json_extended/non-extended.desc
@@ -0,0 +1,7 @@
+CORE
+test.c
+--trace --json-ui
+^EXIT=10$
+^SIGNAL=0$
+--
+rawLhs
diff --git a/regression/cbmc/trace_options_json_extended/test.c b/regression/cbmc/trace_options_json_extended/test.c
@@ -0,0 +1,6 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  assert(argc == 0);
+}
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -219,7 +219,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         if(g.second.status==goalt::statust::FAILURE)
         {
           jsont &json_trace=result["trace"];
-          convert(bmc.ns, g.second.goto_trace, json_trace);
+          convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
         }
       }
 
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -91,7 +91,7 @@ void bmct::error_trace()
         json_stringt(id2string(step.pc->source_location.get_comment()));
       json_result["status"]=json_stringt("failed");
       jsont &json_trace=json_result["trace"];
-      convert(ns, goto_trace, json_trace);
+      convert(ns, goto_trace, json_trace, trace_options());
       status() << json_result;
     }
     break;
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
 
+#include <goto-programs/goto_trace.h>
+
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
@@ -98,6 +100,11 @@ class bmct:public safety_checkert
   virtual void show_vcc_plain(std::ostream &out);
   virtual void show_vcc_json(std::ostream &out);
 
+  trace_optionst trace_options()
+  {
+    return trace_optionst(options);
+  }
+
   virtual resultt all_properties(
     const goto_functionst &goto_functions,
     prop_convt &solver);
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -370,7 +370,7 @@ bool bmc_covert::operator()()
         if(bmc.options.get_bool_option("trace"))
         {
           jsont &json_trace=result["trace"];
-          convert(bmc.ns, test.goto_trace, json_trace);
+          convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
         }
         else
         {
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -408,6 +408,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option(
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
+
+  PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
 /// invoke main modules
@@ -1020,6 +1022,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_GOTO_TRACE
     " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <goto-programs/goto_trace.h>
+
 #include "xml_interface.h"
 
 class bmct;
@@ -65,6 +67,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
+  OPT_GOTO_TRACE \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -395,3 +395,6 @@ void show_goto_trace(
     }
   }
 }
+
+
+const trace_optionst trace_optionst::default_options = trace_optionst();
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
@@ -25,6 +25,7 @@ Date: July 2005
 #include <vector>
 
 #include <util/namespace.h>
+#include <util/options.h>
 #include <util/ssa_expr.h>
 
 #include <goto-programs/goto_program.h>
@@ -206,4 +207,33 @@ void trace_value(
   const exprt &full_lhs,
   const exprt &value);
 
+
+struct trace_optionst
+{
+  bool json_full_lhs;
+
+  static const trace_optionst default_options;
+
+  explicit trace_optionst(const optionst &options)
+  {
+    json_full_lhs = options.get_bool_option("trace-json-extended");
+  };
+
+private:
+  trace_optionst()
+  {
+    json_full_lhs = false;
+  };
+};
+
+#define OPT_GOTO_TRACE "(trace-json-extended)"
+
+#define HELP_GOTO_TRACE                                                        \
+  " --trace-json-extended        add rawLhs property to trace\n"
+
+#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)                             \
+  if(cmdline.isset("trace-json-extended"))                                     \
+    options.set_option("trace-json-extended", true);
+
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening
 #include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
+#include <util/json_irep.h>
 
 /// Produce a json representation of a trace.
 /// \param ns: a namespace
@@ -29,7 +30,8 @@ Author: Daniel Kroening
 void convert(
   const namespacet &ns,
   const goto_tracet &goto_trace,
-  jsont &dest)
+  jsont &dest,
+  trace_optionst trace_options)
 {
   json_arrayt &dest_array=dest.make_array();
 
@@ -94,6 +96,41 @@ void convert(
           step.full_lhs.is_not_nil(),
           "full_lhs in assignment must not be nil");
         exprt simplified=simplify_expr(step.full_lhs, ns);
+
+        if(trace_options.json_full_lhs)
+        {
+          class comment_base_name_visitort : public expr_visitort
+          {
+          private:
+            const namespacet &ns;
+
+          public:
+            explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
+            {
+            }
+
+            void operator()(exprt &expr) override
+            {
+              if(expr.id() == ID_symbol)
+              {
+                const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
+                // Don't break sharing unless need to write to it
+                const irept::named_subt &comments =
+                  static_cast<const exprt &>(expr).get_comments();
+                if(comments.count(ID_C_base_name) != 0)
+                  INVARIANT(
+                    comments.at(ID_C_base_name).id() == symbol.base_name,
+                    "base_name comment does not match symbol's base_name");
+                else
+                  expr.get_comments().emplace(
+                    ID_C_base_name, irept(symbol.base_name));
+              }
+            }
+          };
+          comment_base_name_visitort comment_base_name_visitor(ns);
+          simplified.visit(comment_base_name_visitor);
+        }
+
         full_lhs_string=from_expr(ns, identifier, simplified);
 
         const symbolt *symbol;
@@ -121,6 +158,12 @@ void convert(
 
         json_assignment["value"]=full_lhs_value;
         json_assignment["lhs"]=json_stringt(full_lhs_string);
+        if(trace_options.json_full_lhs)
+        {
+          // Not language specific, still mangled, fully-qualified name of lhs
+          json_assignment["rawLhs"] =
+            json_irept(true).convert_from_irep(simplified);
+        }
         json_assignment["hidden"]=jsont::json_boolean(step.hidden);
         json_assignment["internal"]=jsont::json_boolean(step.internal);
         json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));
diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h
@@ -21,6 +21,7 @@ Date: November 2005
 void convert(
   const namespacet &,
   const goto_tracet &,
-  jsont &);
+  jsont &,
+  trace_optionst trace_options = trace_optionst::default_options);
 
 #endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
@@ -387,6 +387,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option(
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
+
+  PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
 /// invoke main modules
@@ -950,6 +952,7 @@ void jbmc_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_GOTO_TRACE
     " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <goto-programs/goto_trace.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 
 class bmct;
@@ -62,7 +64,8 @@ class optionst;
   "(graphml-witness):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
-  "(localize-faults)(localize-faults-method):"
+  "(localize-faults)(localize-faults-method):" \
+  OPT_GOTO_TRACE
 
 class jbmc_parse_optionst:
   public parse_options_baset,

Original file line number	Diff line number	Diff line change
`@@ -219,7 +219,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`219`	`219`	`if(g.second.status==goalt::statust::FAILURE)`
`220`	`220`	`{`
`221`	`221`	`jsont &json_trace=result["trace"];`
`222`		`- convert(bmc.ns, g.second.goto_trace, json_trace);`
	`222`	`+ convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());`
`223`	`223`	`}`
`224`	`224`	`}`
`225`	`225`
Original file line number	Diff line number	Diff line change
`@@ -91,7 +91,7 @@ void bmct::error_trace()`
`91`	`91`	`json_stringt(id2string(step.pc->source_location.get_comment()));`
`92`	`92`	`json_result["status"]=json_stringt("failed");`
`93`	`93`	`jsont &json_trace=json_result["trace"];`
`94`		`- convert(ns, goto_trace, json_trace);`
	`94`	`+ convert(ns, goto_trace, json_trace, trace_options());`
`95`	`95`	`status() << json_result;`
`96`	`96`	`}`
`97`	`97`	`break;`