diff --git a/regression/cbmc-java/trace_options_json_extended/Test.class b/regression/cbmc-java/trace_options_json_extended/Test.class new file mode 100644 index 00000000000..7aa195d8d93 Binary files /dev/null and b/regression/cbmc-java/trace_options_json_extended/Test.class differ diff --git a/regression/cbmc-java/trace_options_json_extended/Test.java b/regression/cbmc-java/trace_options_json_extended/Test.java new file mode 100644 index 00000000000..495a921ff20 --- /dev/null +++ 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 new file mode 100644 index 00000000000..a0234582e1d --- /dev/null +++ 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 new file mode 100644 index 00000000000..d13bdcd5f3f --- /dev/null +++ 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 new file mode 100644 index 00000000000..beafa0649de --- /dev/null +++ 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 new file mode 100644 index 00000000000..5d03ca97bc1 --- /dev/null +++ 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 new file mode 100644 index 00000000000..c88cbcda616 --- /dev/null +++ b/regression/cbmc/trace_options_json_extended/test.c @@ -0,0 +1,6 @@ +#include + +int main(int argc, char *argv[]) +{ + assert(argc == 0); +} diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index cce96904495..2a67d388caf 100644 --- 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 index 63b53e394b2..cc107f813c0 100644 --- 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 index f45d7ab5e4c..40673724703 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -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 index 7758c49dafd..a91eeed2c9a 100644 --- 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 index 052017763ff..29493dd0dbb 100644 --- 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 index 4fd131422c6..9c46c7ee2ab 100644 --- 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 +#include + #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 index b6649e97ffc..651db1fef48 100644 --- 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 index 08dd5234e76..5af74abbe8f 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -25,6 +25,7 @@ Date: July 2005 #include #include +#include #include #include @@ -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 index 52c18d36e6b..b1c4547d3aa 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening #include #include +#include /// 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(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 index 102569b50e6..2777ec44673 100644 --- 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 index e406a373c46..0d0d1975eb4 100644 --- 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 @@ -949,6 +951,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 index 5c722e0821a..87089d88aa2 100644 --- 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 +#include + #include 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,