From b757b71ed0d04e3e8875d6d683fafe29515f1c1a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 19 Jan 2018 01:15:04 +0000 Subject: [PATCH 1/6] JSON streaming (cherry picked from commit 7c414911354eb228bfda985246b4b8c0bc419877) --- src/util/Makefile | 1 + src/util/json.cpp | 44 +++++++------ src/util/json.h | 6 +- src/util/json_stream.cpp | 123 +++++++++++++++++++++++++++++++++++++ src/util/json_stream.h | 129 +++++++++++++++++++++++++++++++++++++++ 5 files changed, 285 insertions(+), 18 deletions(-) create mode 100644 src/util/json_stream.cpp create mode 100644 src/util/json_stream.h diff --git a/src/util/Makefile b/src/util/Makefile index d5030ef2a48..18321a4ea81 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -33,6 +33,7 @@ SRC = arith_tools.cpp \ json.cpp \ json_expr.cpp \ json_irep.cpp \ + json_stream.cpp \ language.cpp \ language_file.cpp \ lispexpr.cpp \ diff --git a/src/util/json.cpp b/src/util/json.cpp index dcfa9858601..f8cad9886cc 100644 --- a/src/util/json.cpp +++ b/src/util/json.cpp @@ -67,23 +67,7 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const case kindt::J_OBJECT: out << '{'; - for(objectt::const_iterator o_it=object.begin(); - o_it!=object.end(); - o_it++) - { - if(o_it!=object.begin()) - out << ','; - - out << '\n'; - - out << std::string((indent+1)*2, ' '); - - out << '"'; - escape_string(o_it->first, out); - out << '"'; - out << ": "; - o_it->second.output_rec(out, indent+1); - } + output_object(out, object, indent); if(!object.empty()) { out << '\n'; @@ -134,6 +118,32 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const } } +void jsont::output_object(std::ostream &out, const objectt &object, unsigned indent) +{ + for(objectt::const_iterator o_it=object.begin(); + o_it!=object.end(); + o_it++) + { + if(o_it!=object.begin()) + out << ','; + + out << '\n'; + + out << std::string((indent+1)*2, ' '); + + jsont::output_key(out, o_it->first); + o_it->second.output_rec(out, indent+1); + } +} + +void jsont::output_key(std::ostream &out, const std::string &key) +{ + out << '"'; + jsont::escape_string(key, out); + out << '"'; + out << ": "; +} + void jsont::swap(jsont &other) { std::swap(other.kind, kind); diff --git a/src/util/json.h b/src/util/json.h index 5095a3044df..63a6e909744 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -109,7 +109,6 @@ class jsont protected: void output_rec(std::ostream &, unsigned indent) const; static void escape_string(const std::string &, std::ostream &); - static const jsont null_json_object; explicit jsont(kindt _kind):kind(_kind) @@ -127,8 +126,13 @@ class jsont typedef std::map objectt; objectt object; + static void output_object(std::ostream &out, const objectt &object, unsigned indent); + static void output_key(std::ostream &out, const std::string &key); std::string value; + + friend class json_stream_objectt; + friend class json_stream_arrayt; }; inline std::ostream &operator<<(std::ostream &out, const jsont &src) diff --git a/src/util/json_stream.cpp b/src/util/json_stream.cpp new file mode 100644 index 00000000000..8a6113b76c4 --- /dev/null +++ b/src/util/json_stream.cpp @@ -0,0 +1,123 @@ +/*******************************************************************\ + +Module: + +Author: Peter Schrammel + +\*******************************************************************/ + +#include "json_stream.h" + +#include + +void json_streamt::output_delimiter() +{ + if(!first) + out << ','; + else + first = false; + out << '\n'; + out << std::string((indent+1)*2, ' '); +} + +json_stream_arrayt::json_stream_arrayt(std::ostream &out, unsigned indent) + : json_streamt(out, indent) +{ + out << '['; +} + +void json_stream_arrayt::output_current() +{ + if(!object.empty()) + { + output_delimiter(); + object[""].output_rec(out, indent+1); + object.clear(); + } + if(current) + { + current->close(); + } +} + +void json_stream_arrayt::output_finalizer() +{ + out << '\n' << std::string(indent*2, ' '); + out << ']'; +} + +json_stream_objectt::json_stream_objectt(std::ostream &out, unsigned indent) + : json_streamt(out, indent) +{ + out << '{'; +} + +json_stream_arrayt &json_streamt::create_current_array() +{ + current = + std::unique_ptr(new json_stream_arrayt(out, indent + 1)); + return static_cast(*current); +} + +json_stream_objectt &json_streamt::create_current_object() +{ + current = + std::unique_ptr(new json_stream_objectt(out, indent + 1)); + return static_cast(*current); +} + +json_stream_objectt &json_stream_arrayt::push_back_stream_object() +{ + PRECONDITION(open); + output_current(); + output_delimiter(); + return create_current_object(); +} + +json_stream_arrayt &json_stream_arrayt::push_back_stream_array() +{ + PRECONDITION(open); + output_current(); + output_delimiter(); + return create_current_array(); +} + +json_stream_objectt &json_stream_objectt::push_back_stream_object(const std::string &key) +{ + PRECONDITION(open); + output_current(); + output_delimiter(); + jsont::output_key(out, key); + return create_current_object(); +} + +json_stream_arrayt &json_stream_objectt::push_back_stream_array(const std::string &key) +{ + PRECONDITION(open); + output_current(); + output_delimiter(); + jsont::output_key(out, key); + return create_current_array(); +} + +void json_stream_objectt::output_current() +{ + for(const auto &obj : object) + { + output_delimiter(); + jsont::output_key(out, obj.first); + obj.second.output_rec(out, indent+1); + } + object.clear(); + if(current) + { + current->close(); + } +} + +void json_stream_objectt::output_finalizer() +{ + jsont::output_object(out, object, indent); + out << '\n' << std::string(indent*2, ' '); + out << '}'; +} diff --git a/src/util/json_stream.h b/src/util/json_stream.h new file mode 100644 index 00000000000..88690a0e0a3 --- /dev/null +++ b/src/util/json_stream.h @@ -0,0 +1,129 @@ +/*******************************************************************\ + +Module: + +Author: Peter Schrammel + +\*******************************************************************/ + + +#ifndef CPROVER_UTIL_JSON_STREAM_H +#define CPROVER_UTIL_JSON_STREAM_H + +#include "json.h" +#include "invariant.h" + +class json_stream_objectt; +class json_stream_arrayt; + +class json_streamt +{ +public: + void close() + { + if(open) + { + output_current(); + output_finalizer(); + open = false; + } + } + +protected: + json_streamt(std::ostream &_out, unsigned _indent) + : open(true), out(_out), indent(_indent), first(true), current(nullptr) + { + } + + bool open; + std::ostream &out; + + unsigned indent; + bool first; + + typedef std::map objectt; + objectt object; + + std::unique_ptr current; + json_stream_arrayt &create_current_array(); + json_stream_objectt &create_current_object(); + + void output_delimiter(); + + virtual void output_current() + { + // no-op + } + + virtual void output_finalizer() + { + // no-op + } +}; + +class json_stream_arrayt : public json_streamt +{ +public: + json_stream_arrayt(std::ostream &out, unsigned indent = 0); + + ~json_stream_arrayt() + { + close(); + } + + void push_back(const jsont &json) + { + PRECONDITION(open); + output_current(); + output_delimiter(); + json.output_rec(out, indent+1); + } + + jsont &push_back() + { + PRECONDITION(open); + output_current(); + return object[""]; + } + + json_stream_objectt &push_back_stream_object(); + json_stream_arrayt &push_back_stream_array(); + +protected: + void output_current() override; + void output_finalizer() override; +}; + +class json_stream_objectt:public json_streamt +{ +public: + json_stream_objectt(std::ostream &out, unsigned indent = 0); + + jsont &operator[](const std::string &key) + { + return object[key]; + } + + ~json_stream_objectt() + { + close(); + } + + const jsont &operator[](const std::string &key) const + { + objectt::const_iterator it=object.find(key); + if(it==object.end()) + return jsont::null_json_object; + else + return it->second; + } + + json_stream_objectt &push_back_stream_object(const std::string &key); + json_stream_arrayt &push_back_stream_array(const std::string &key); + +protected: + void output_current() override; + void output_finalizer() override; +}; + +#endif // CPROVER_UTIL_JSON_STREAM_H From 3af85e836d3a8025c4a4adc97f417698b81d1958 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 22 Jan 2018 16:32:33 +0000 Subject: [PATCH 2/6] Base JSON UI message handler upon json_streamt (cherry picked from commit 3a1cfd4d5d81645bff22c1b138650286a261b9de) --- src/util/message.h | 12 +++++++++++ src/util/ui_message.cpp | 45 +++++++++++++++++++++++------------------ src/util/ui_message.h | 18 +++++++++++++---- 3 files changed, 51 insertions(+), 24 deletions(-) diff --git a/src/util/message.h b/src/util/message.h index 1d4b3d54e40..75af1f53e5c 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "json_stream.h" #include "source_location.h" class message_handlert @@ -25,6 +26,11 @@ class message_handlert virtual void print(unsigned level, const std::string &message) = 0; + virtual json_stream_arrayt &get_json_stream() + { + UNREACHABLE; + } + virtual void print( unsigned level, const std::string &message, @@ -184,6 +190,12 @@ class messaget { return func(*this); } + + json_stream_arrayt &json_stream() + { + *this << eom; // force end of previous message + return message.message_handler->get_json_stream(); + } }; // Feeding 'eom' into the stream triggers diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index e750c60e3bb..b83719bf1fa 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -13,37 +13,37 @@ Author: Daniel Kroening, kroening@kroening.com #include "xml.h" #include "json.h" #include "xml_expr.h" +#include "json_stream.h" #include "cout_message.h" #include "ui_message.h" #include "cmdline.h" ui_message_handlert::ui_message_handlert( - uit __ui, const std::string &program):_ui(__ui) + uit __ui, const std::string &program):ui_message_handlert() { - switch(__ui) + set_ui(__ui); + switch(_ui) { case uit::PLAIN: break; case uit::XML_UI: - std::cout << "" << "\n"; - std::cout << "" << "\n"; + out << "" << "\n"; + out << "" << "\n"; { xmlt program_xml; program_xml.name="program"; program_xml.data=program; - std::cout << program_xml; + out << program_xml; } break; case uit::JSON_UI: { - std::cout << "[\n"; - json_objectt json_program; - json_program["program"] = json_stringt(program); - std::cout << json_program; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream->push_back().make_object()["program"] = json_stringt(program); } break; } @@ -60,16 +60,24 @@ ui_message_handlert::ui_message_handlert( { } +ui_message_handlert::ui_message_handlert(): + _ui(uit::PLAIN), out(std::cout), json_stream(nullptr) +{ +} + ui_message_handlert::~ui_message_handlert() { switch(get_ui()) { case uit::XML_UI: - std::cout << "" << "\n"; + + out << "" << "\n"; break; case uit::JSON_UI: - std::cout << "\n]\n"; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream->close(); + out << '\n'; break; case uit::PLAIN: @@ -116,6 +124,7 @@ void ui_message_handlert::print( void ui_message_handlert::print( unsigned level, + json_stream->push_back(data); const std::string &message, int sequence_number, const source_locationt &location) @@ -188,8 +197,8 @@ void ui_message_handlert::xml_ui_msg( result.new_element("text").data=msg1; result.set_attribute("type", type); - std::cout << result; - std::cout << '\n'; + out << result; + out << '\n'; } void ui_message_handlert::json_ui_msg( @@ -198,7 +207,8 @@ void ui_message_handlert::json_ui_msg( const std::string &msg2, const source_locationt &location) { - json_objectt result; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_objectt &result = json_stream->push_back().make_object(); #if 0 if(location.is_not_nil() && @@ -208,11 +218,6 @@ void ui_message_handlert::json_ui_msg( result["messageType"] = json_stringt(type); result["messageText"] = json_stringt(msg1); - - // By convention a leading comma is created by every new array entry. - // The first entry is generated in the constructor and does not have - // a trailing comma. - std::cout << ",\n" << result; } void ui_message_handlert::flush(unsigned level) @@ -229,7 +234,7 @@ void ui_message_handlert::flush(unsigned level) case uit::XML_UI: case uit::JSON_UI: { - std::cout << std::flush; + out << std::flush; } break; } diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 757108483f1..0075f025484 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "message.h" +class json_stream_arrayt; + class ui_message_handlert:public message_handlert { public: @@ -19,10 +21,7 @@ class ui_message_handlert:public message_handlert ui_message_handlert(uit, const std::string &program); ui_message_handlert(const class cmdlinet &, const std::string &program); - ui_message_handlert(): - _ui(uit::PLAIN) - { - } + ui_message_handlert(); virtual ~ui_message_handlert(); @@ -34,12 +33,23 @@ class ui_message_handlert:public message_handlert void set_ui(uit __ui) { _ui=__ui; + if(_ui == uit::JSON_UI && !json_stream) + { + json_stream = std::unique_ptr(new json_stream_arrayt(out)); + } } virtual void flush(unsigned level); + json_stream_arrayt &get_json_stream() override + { + return *json_stream; + } + protected: uit _ui; + std::ostream &out; + std::unique_ptr json_stream; // overloading virtual void print( From f41ac45339367b5f55b8b62956e68cfae4d1fe21 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 19 Jan 2018 01:16:52 +0000 Subject: [PATCH 3/6] Use JSON streaming (cherry picked from commit 0a37dd90e383f49f3636916f5f6f376975487ce4) --- src/cbmc/all_properties.cpp | 13 +- src/cbmc/bmc.cpp | 10 +- src/cbmc/bmc_cover.cpp | 2 +- src/goto-programs/interpreter.cpp | 3 + src/goto-programs/json_goto_trace.cpp | 212 ++------------------ src/goto-programs/json_goto_trace.h | 278 +++++++++++++++++++++++++- 6 files changed, 302 insertions(+), 216 deletions(-) diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index bd9c5242dd4..4f86fbca0de 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -207,24 +207,23 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) case ui_message_handlert::uit::JSON_UI: { - json_objectt json_result; - json_arrayt &result_array=json_result["result"].make_array(); + json_stream_objectt &json_result = result().json_stream().push_back_stream_object(); + json_stream_arrayt &result_array = + json_result.push_back_stream_array("result"); for(const auto &g : goal_map) { - json_objectt &result=result_array.push_back().make_object(); + json_stream_objectt &result=result_array.push_back_stream_object(); result["property"]=json_stringt(id2string(g.first)); result["description"]=json_stringt(id2string(g.second.description)); result["status"]=json_stringt(g.second.status_string()); if(g.second.status==goalt::statust::FAILURE) { - jsont &json_trace=result["trace"]; - convert(bmc.ns, g.second.goto_trace, json_trace); + json_stream_arrayt &json_trace=result.push_back_stream_array("trace"); + convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options()); } } - - std::cout << ",\n" << json_result; } break; } diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index f92483d2441..1361dff4918 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -71,18 +72,15 @@ void bmct::error_trace() case ui_message_handlert::uit::JSON_UI: { - json_objectt json_result; - json_arrayt &result_array=json_result["results"].make_array(); - json_objectt &result=result_array.push_back().make_object(); + json_stream_objectt &json_result = status().json_stream().push_back_stream_object(); const goto_trace_stept &step=goto_trace.steps.back(); result["property"]= json_stringt(id2string(step.pc->source_location.get_property_id())); result["description"]= json_stringt(id2string(step.pc->source_location.get_comment())); result["status"]=json_stringt("failed"); - jsont &json_trace=result["trace"]; - convert(ns, goto_trace, json_trace); - std::cout << ",\n" << json_result; + json_stream_arrayt &json_trace=json_result.push_back_stream_array("trace"); + convert(ns, goto_trace, json_trace, trace_options()); } break; } diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 4c101cc2159..6585ee91226 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -378,7 +378,7 @@ bool bmc_covert::operator()() json_objectt &result=tests_array.push_back().make_object(); if(bmc.options.get_bool_option("trace")) { - jsont &json_trace=result["trace"]; + json_arrayt &json_trace=result["trace"].make_array(); convert(bmc.ns, test.goto_trace, json_trace); } else diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 8a5c23f1a62..08bfd6c7d39 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "interpreter.h" #include "interpreter_class.h" +#include "json_goto_trace.h" void interpretert::operator()() { @@ -79,6 +80,8 @@ void interpretert::command() if(ch=='q') done=true; + json_arrayt json_steps; + convert(ns, steps, json_steps); } void interpretert::step() diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index ddc9f44ad3b..48fa84c0e1e 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -11,204 +11,18 @@ Author: Daniel Kroening /// \file /// Traces of GOTO Programs -#include - -#include - -#include - #include "json_goto_trace.h" - -void convert( - const namespacet &ns, - const goto_tracet &goto_trace, - jsont &dest) -{ - json_arrayt &dest_array=dest.make_array(); - - source_locationt previous_source_location; - - for(const auto &step : goto_trace.steps) - { - const source_locationt &source_location=step.pc->source_location; - - jsont json_location; - - if(source_location.is_not_nil() && source_location.get_file()!="") - json_location=json(source_location); - else - json_location=json_nullt(); - - switch(step.type) - { - case goto_trace_stept::typet::ASSERT: - if(!step.cond_value) - { - irep_idt property_id; - - if(step.pc->is_assert()) - property_id=source_location.get_property_id(); - else if(step.pc->is_goto()) // unwinding, we suspect - { - property_id= - id2string(step.pc->source_location.get_function())+ - ".unwind."+std::to_string(step.pc->loop_number); - } - - json_objectt &json_failure=dest_array.push_back().make_object(); - - json_failure["stepType"]=json_stringt("failure"); - json_failure["hidden"]=jsont::json_boolean(step.hidden); - json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_failure["reason"]=json_stringt(id2string(step.comment)); - json_failure["property"]=json_stringt(id2string(property_id)); - - if(!json_location.is_null()) - json_failure["sourceLocation"]=json_location; - } - break; - - case goto_trace_stept::typet::ASSIGNMENT: - case goto_trace_stept::typet::DECL: - { - irep_idt identifier=step.lhs_object.get_identifier(); - json_objectt &json_assignment=dest_array.push_back().make_object(); - - json_assignment["stepType"]=json_stringt("assignment"); - - if(!json_location.is_null()) - json_assignment["sourceLocation"]=json_location; - - std::string value_string, binary_string, type_string, full_lhs_string; - json_objectt full_lhs_value; - - if(step.full_lhs.is_not_nil()) - full_lhs_string=from_expr(ns, identifier, step.full_lhs); - -#if 0 - if(it.full_lhs_value.is_not_nil()) - full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value); -#endif - - if(step.full_lhs_value.is_not_nil()) +/// Produce a json representation of a trace. +/// \param ns: a namespace + jsont &dest, + + DATA_INVARIANT( + step.full_lhs.is_not_nil(), + void operator()(exprt &expr) override + { + if(expr.id() == ID_symbol) + { + full_lhs_string=from_expr(ns, identifier, simplified); full_lhs_value = json(step.full_lhs_value, ns); - - const symbolt *symbol; - irep_idt base_name, display_name; - - if(!ns.lookup(identifier, symbol)) - { - base_name=symbol->base_name; - display_name=symbol->display_name(); - if(type_string=="") - type_string=from_type(ns, identifier, symbol->type); - - json_assignment["mode"]=json_stringt(id2string(symbol->mode)); - } - - json_assignment["value"]=full_lhs_value; - json_assignment["lhs"]=json_stringt(full_lhs_string); - json_assignment["hidden"]=jsont::json_boolean(step.hidden); - json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); - - json_assignment["assignmentType"]= - json_stringt( - step.assignment_type== - goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? - "actual-parameter": - "variable"); - } - break; - - case goto_trace_stept::typet::OUTPUT: - { - json_objectt &json_output=dest_array.push_back().make_object(); - - json_output["stepType"]=json_stringt("output"); - json_output["hidden"]=jsont::json_boolean(step.hidden); - json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_output["outputID"]=json_stringt(id2string(step.io_id)); - - json_arrayt &json_values=json_output["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns)); - } - - if(!json_location.is_null()) - json_output["sourceLocation"]=json_location; - } - break; - - case goto_trace_stept::typet::INPUT: - { - json_objectt &json_input=dest_array.push_back().make_object(); - - json_input["stepType"]=json_stringt("input"); - json_input["hidden"]=jsont::json_boolean(step.hidden); - json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_input["inputID"]=json_stringt(id2string(step.io_id)); - - json_arrayt &json_values=json_input["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns)); - } - - if(!json_location.is_null()) - json_input["sourceLocation"]=json_location; - } - break; - - case goto_trace_stept::typet::FUNCTION_CALL: - case goto_trace_stept::typet::FUNCTION_RETURN: - { - std::string tag= - (step.type==goto_trace_stept::typet::FUNCTION_CALL)? - "function-call":"function-return"; - json_objectt &json_call_return=dest_array.push_back().make_object(); - - json_call_return["stepType"]=json_stringt(tag); - json_call_return["hidden"]=jsont::json_boolean(step.hidden); - json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); - - const symbolt &symbol=ns.lookup(step.identifier); - json_objectt &json_function=json_call_return["function"].make_object(); - json_function["displayName"]= - json_stringt(id2string(symbol.display_name())); - json_function["identifier"]=json_stringt(id2string(step.identifier)); - json_function["sourceLocation"]=json(symbol.location); - - if(!json_location.is_null()) - json_call_return["sourceLocation"]=json_location; - } - break; - - default: - if(source_location!=previous_source_location) - { - // just the source location - if(!json_location.is_null()) - { - json_objectt &json_location_only=dest_array.push_back().make_object(); - json_location_only["stepType"]=json_stringt("location-only"); - json_location_only["hidden"]=jsont::json_boolean(step.hidden); - json_location_only["thread"]= - json_numbert(std::to_string(step.thread_nr)); - json_location_only["sourceLocation"]=json_location; - } - } - } - - if(source_location.is_not_nil() && source_location.get_file()!="") - previous_source_location=source_location; - } -} + json_values.push_back(json(arg, ns, mode)); + json_values.push_back(json(arg, ns, mode)); diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 102569b50e6..6cbae23b3af 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -15,12 +15,284 @@ Date: November 2005 #define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H #include +#include #include "goto_trace.h" +#include "json_goto_trace.h" + +#include +#include +#include +#include +#include + +#include +#include + +/// Produce a json representation of a trace. +/// \param ns: a namespace +/// \param goto_trace: a trace in a goto program +/// \param dest: referecence to a json stream in which the goto trace will be +/// added +template void convert( - const namespacet &, - const goto_tracet &, - jsont &); + const namespacet &ns, + const goto_tracet &goto_trace, + json_arrayT &dest_array, + trace_optionst trace_options = trace_optionst::default_options) +{ + source_locationt previous_source_location; + + for(const auto &step : goto_trace.steps) + { + const source_locationt &source_location=step.pc->source_location; + + jsont json_location; + + if(source_location.is_not_nil() && source_location.get_file()!="") + json_location=json(source_location); + else + json_location=json_nullt(); + + switch(step.type) + { + case goto_trace_stept::typet::ASSERT: + if(!step.cond_value) + { + irep_idt property_id; + + if(step.pc->is_assert()) + property_id=source_location.get_property_id(); + else if(step.pc->is_goto()) // unwinding, we suspect + { + property_id= + id2string(step.pc->source_location.get_function())+ + ".unwind."+std::to_string(step.pc->loop_number); + } + + json_objectt &json_failure=dest_array.push_back().make_object(); + + json_failure["stepType"]=json_stringt("failure"); + json_failure["hidden"]=jsont::json_boolean(step.hidden); + json_failure["internal"]=jsont::json_boolean(step.internal); + json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_failure["reason"]=json_stringt(id2string(step.comment)); + json_failure["property"]=json_stringt(id2string(property_id)); + + if(!json_location.is_null()) + json_failure["sourceLocation"]=json_location; + } + break; + + case goto_trace_stept::typet::ASSIGNMENT: + case goto_trace_stept::typet::DECL: + { + irep_idt identifier=step.lhs_object.get_identifier(); + json_objectt &json_assignment=dest_array.push_back().make_object(); + + json_assignment["stepType"]=json_stringt("assignment"); + + if(!json_location.is_null()) + json_assignment["sourceLocation"]=json_location; + + std::string value_string, binary_string, type_string, full_lhs_string; + json_objectt full_lhs_value; + + DATA_INVARIANT( + 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)); + if(expr.find(ID_C_base_name).is_not_nil()) + INVARIANT( + expr.find(ID_C_base_name).id() == symbol.base_name, + "base_name comment does not match symbol's base_name"); + else + expr.add(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; + irep_idt base_name, display_name; + + if(!ns.lookup(identifier, symbol)) + { + base_name=symbol->base_name; + display_name=symbol->display_name(); + if(type_string=="") + type_string=from_type(ns, identifier, symbol->type); + + json_assignment["mode"]=json_stringt(id2string(symbol->mode)); + exprt simplified=simplify_expr(step.full_lhs_value, ns); + + full_lhs_value=json(simplified, ns, symbol->mode); + } + else + { + DATA_INVARIANT( + step.full_lhs_value.is_not_nil(), + "full_lhs_value in assignment must not be nil"); + full_lhs_value=json(step.full_lhs_value, ns, ID_unknown); + } + + 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)); + + json_assignment["assignmentType"]= + json_stringt( + step.assignment_type== + goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? + "actual-parameter": + "variable"); + } + break; + + case goto_trace_stept::typet::OUTPUT: + { + json_objectt &json_output=dest_array.push_back().make_object(); + + json_output["stepType"]=json_stringt("output"); + json_output["hidden"]=jsont::json_boolean(step.hidden); + json_output["internal"]=jsont::json_boolean(step.internal); + json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_output["outputID"]=json_stringt(id2string(step.io_id)); + + // Recovering the mode from the function + irep_idt mode; + const symbolt *function_name; + if(ns.lookup(source_location.get_function(), function_name)) + // Failed to find symbol + mode=ID_unknown; + else + mode=function_name->mode; + json_output["mode"]=json_stringt(id2string(mode)); + json_arrayt &json_values=json_output["values"].make_array(); + + for(const auto &arg : step.io_args) + { + if(arg.is_nil()) + json_values.push_back(json_stringt("")); + else + json_values.push_back(json(arg, ns, mode)); + } + + if(!json_location.is_null()) + json_output["sourceLocation"]=json_location; + } + break; + + case goto_trace_stept::typet::INPUT: + { + json_objectt &json_input=dest_array.push_back().make_object(); + + json_input["stepType"]=json_stringt("input"); + json_input["hidden"]=jsont::json_boolean(step.hidden); + json_input["internal"]=jsont::json_boolean(step.internal); + json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_input["inputID"]=json_stringt(id2string(step.io_id)); + + // Recovering the mode from the function + irep_idt mode; + const symbolt *function_name; + if(ns.lookup(source_location.get_function(), function_name)) + // Failed to find symbol + mode=ID_unknown; + else + mode=function_name->mode; + json_input["mode"]=json_stringt(id2string(mode)); + json_arrayt &json_values=json_input["values"].make_array(); + + for(const auto &arg : step.io_args) + { + if(arg.is_nil()) + json_values.push_back(json_stringt("")); + else + json_values.push_back(json(arg, ns, mode)); + } + + if(!json_location.is_null()) + json_input["sourceLocation"]=json_location; + } + break; + + case goto_trace_stept::typet::FUNCTION_CALL: + case goto_trace_stept::typet::FUNCTION_RETURN: + { + std::string tag= + (step.type==goto_trace_stept::typet::FUNCTION_CALL)? + "function-call":"function-return"; + json_objectt &json_call_return=dest_array.push_back().make_object(); + + json_call_return["stepType"]=json_stringt(tag); + json_call_return["hidden"]=jsont::json_boolean(step.hidden); + json_call_return["internal"]=jsont::json_boolean(step.internal); + json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); + + const symbolt &symbol=ns.lookup(step.identifier); + json_objectt &json_function=json_call_return["function"].make_object(); + json_function["displayName"]= + json_stringt(id2string(symbol.display_name())); + json_function["identifier"]=json_stringt(id2string(step.identifier)); + json_function["sourceLocation"]=json(symbol.location); + + if(!json_location.is_null()) + json_call_return["sourceLocation"]=json_location; + } + break; + + default: + if(source_location!=previous_source_location) + { + // just the source location + if(!json_location.is_null()) + { + json_objectt &json_location_only=dest_array.push_back().make_object(); + json_location_only["stepType"]=json_stringt("location-only"); + json_location_only["hidden"]=jsont::json_boolean(step.hidden); + json_location_only["internal"]=jsont::json_boolean(step.internal); + json_location_only["thread"]= + json_numbert(std::to_string(step.thread_nr)); + json_location_only["sourceLocation"]=json_location; + } + } + } + + if(source_location.is_not_nil() && source_location.get_file()!="") + previous_source_location=source_location; + } +} #endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H From 846bb68d730795e4891957d8b6639933239db437 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 23 Jan 2018 11:17:58 +0000 Subject: [PATCH 4/6] Intermediate changes to make it compile. --- src/util/json_stream.h | 2 ++ src/util/message.h | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/util/json_stream.h b/src/util/json_stream.h index 88690a0e0a3..8c14478342d 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -10,6 +10,8 @@ Author: Peter Schrammel #ifndef CPROVER_UTIL_JSON_STREAM_H #define CPROVER_UTIL_JSON_STREAM_H +#include + #include "json.h" #include "invariant.h" diff --git a/src/util/message.h b/src/util/message.h index 75af1f53e5c..93238635742 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -14,8 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "invariant.h" +#include "json.h" #include "json_stream.h" #include "source_location.h" +#include "xml.h" class message_handlert { From 94b792ce1cd04a6c313b6f57dc5d2bec8172e561 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 25 Jan 2018 15:24:52 +0000 Subject: [PATCH 5/6] Implement necessary changes for goto-analyzer-develop branch. --- src/cbmc/all_properties.cpp | 7 +- src/cbmc/bmc.cpp | 14 +- src/goto-programs/interpreter.cpp | 3 - src/goto-programs/json_goto_trace.cpp | 22 +-- src/goto-programs/json_goto_trace.h | 202 +++++++++----------------- src/symex/symex_cover.cpp | 15 +- src/util/json.cpp | 3 +- src/util/json.h | 3 +- src/util/json_stream.cpp | 6 +- src/util/json_stream.h | 6 +- src/util/message.h | 5 +- src/util/ui_message.cpp | 4 - src/util/ui_message.h | 9 +- 13 files changed, 114 insertions(+), 185 deletions(-) diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 4f86fbca0de..2ce0f60e4f2 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -207,8 +207,9 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) case ui_message_handlert::uit::JSON_UI: { - json_stream_objectt &json_result = result().json_stream().push_back_stream_object(); - json_stream_arrayt &result_array = + json_stream_objectt &json_result= + result().json_stream().push_back_stream_object(); + json_stream_arrayt &result_array= json_result.push_back_stream_array("result"); for(const auto &g : goal_map) @@ -221,7 +222,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) if(g.second.status==goalt::statust::FAILURE) { json_stream_arrayt &json_trace=result.push_back_stream_array("trace"); - convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options()); + convert(bmc.ns, g.second.goto_trace, json_trace); } } } diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 1361dff4918..4e309dfaa0b 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -72,15 +72,17 @@ void bmct::error_trace() case ui_message_handlert::uit::JSON_UI: { - json_stream_objectt &json_result = status().json_stream().push_back_stream_object(); + json_stream_objectt &json_result= + status().json_stream().push_back_stream_object(); const goto_trace_stept &step=goto_trace.steps.back(); - result["property"]= + json_result["property"]= json_stringt(id2string(step.pc->source_location.get_property_id())); - result["description"]= + json_result["description"]= json_stringt(id2string(step.pc->source_location.get_comment())); - result["status"]=json_stringt("failed"); - json_stream_arrayt &json_trace=json_result.push_back_stream_array("trace"); - convert(ns, goto_trace, json_trace, trace_options()); + json_result["status"]=json_stringt("failed"); + json_stream_arrayt &json_trace= + json_result.push_back_stream_array("trace"); + convert(ns, goto_trace, json_trace); } break; } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 08bfd6c7d39..8a5c23f1a62 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "interpreter.h" #include "interpreter_class.h" -#include "json_goto_trace.h" void interpretert::operator()() { @@ -80,8 +79,6 @@ void interpretert::command() if(ch=='q') done=true; - json_arrayt json_steps; - convert(ns, steps, json_steps); } void interpretert::step() diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 48fa84c0e1e..dd9fe58ab8a 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -11,18 +11,12 @@ Author: Daniel Kroening /// \file /// Traces of GOTO Programs +#include + +#include + +#include + #include "json_goto_trace.h" -/// Produce a json representation of a trace. -/// \param ns: a namespace - jsont &dest, - - DATA_INVARIANT( - step.full_lhs.is_not_nil(), - void operator()(exprt &expr) override - { - if(expr.id() == ID_symbol) - { - full_lhs_string=from_expr(ns, identifier, simplified); - full_lhs_value = json(step.full_lhs_value, ns); - json_values.push_back(json(arg, ns, mode)); - json_values.push_back(json(arg, ns, mode)); + + diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 6cbae23b3af..9eb9969a1b7 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -30,17 +30,11 @@ Date: November 2005 #include #include -/// Produce a json representation of a trace. -/// \param ns: a namespace -/// \param goto_trace: a trace in a goto program -/// \param dest: referecence to a json stream in which the goto trace will be -/// added -template +template void convert( const namespacet &ns, const goto_tracet &goto_trace, - json_arrayT &dest_array, - trace_optionst trace_options = trace_optionst::default_options) + newJson &dest) { source_locationt previous_source_location; @@ -57,39 +51,38 @@ void convert( switch(step.type) { - case goto_trace_stept::typet::ASSERT: - if(!step.cond_value) + case goto_trace_stept::typet::ASSERT: + if(!step.cond_value) + { + irep_idt property_id; + + if(step.pc->is_assert()) + property_id=source_location.get_property_id(); + else if(step.pc->is_goto()) // unwinding, we suspect { - irep_idt property_id; - - if(step.pc->is_assert()) - property_id=source_location.get_property_id(); - else if(step.pc->is_goto()) // unwinding, we suspect - { - property_id= - id2string(step.pc->source_location.get_function())+ - ".unwind."+std::to_string(step.pc->loop_number); - } - - json_objectt &json_failure=dest_array.push_back().make_object(); - - json_failure["stepType"]=json_stringt("failure"); - json_failure["hidden"]=jsont::json_boolean(step.hidden); - json_failure["internal"]=jsont::json_boolean(step.internal); - json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_failure["reason"]=json_stringt(id2string(step.comment)); - json_failure["property"]=json_stringt(id2string(property_id)); - - if(!json_location.is_null()) - json_failure["sourceLocation"]=json_location; + property_id= + id2string(step.pc->source_location.get_function())+ + ".unwind."+std::to_string(step.pc->loop_number); } - break; - case goto_trace_stept::typet::ASSIGNMENT: - case goto_trace_stept::typet::DECL: + json_objectt &json_failure=dest.push_back().make_object(); + + json_failure["stepType"]=json_stringt("failure"); + json_failure["hidden"]=jsont::json_boolean(step.hidden); + json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_failure["reason"]=json_stringt(id2string(step.comment)); + json_failure["property"]=json_stringt(id2string(property_id)); + + if(!json_location.is_null()) + json_failure["sourceLocation"]=json_location; + } + break; + + case goto_trace_stept::typet::ASSIGNMENT: + case goto_trace_stept::typet::DECL: { irep_idt identifier=step.lhs_object.get_identifier(); - json_objectt &json_assignment=dest_array.push_back().make_object(); + json_objectt &json_assignment=dest.push_back().make_object(); json_assignment["stepType"]=json_stringt("assignment"); @@ -99,42 +92,16 @@ void convert( std::string value_string, binary_string, type_string, full_lhs_string; json_objectt full_lhs_value; - DATA_INVARIANT( - step.full_lhs.is_not_nil(), - "full_lhs in assignment must not be nil"); - exprt simplified=simplify_expr(step.full_lhs, ns); + if(step.full_lhs.is_not_nil()) + full_lhs_string=from_expr(ns, identifier, step.full_lhs); - 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)); - if(expr.find(ID_C_base_name).is_not_nil()) - INVARIANT( - expr.find(ID_C_base_name).id() == symbol.base_name, - "base_name comment does not match symbol's base_name"); - else - expr.add(ID_C_base_name, irept(symbol.base_name)); - } - } - }; - comment_base_name_visitort comment_base_name_visitor(ns); - simplified.visit(comment_base_name_visitor); - } +#if 0 + if(it.full_lhs_value.is_not_nil()) + full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value); +#endif - full_lhs_string=from_expr(ns, identifier, simplified); + if(step.full_lhs_value.is_not_nil()) + full_lhs_value = json(step.full_lhs_value, ns); const symbolt *symbol; irep_idt base_name, display_name; @@ -147,58 +114,31 @@ void convert( type_string=from_type(ns, identifier, symbol->type); json_assignment["mode"]=json_stringt(id2string(symbol->mode)); - exprt simplified=simplify_expr(step.full_lhs_value, ns); - - full_lhs_value=json(simplified, ns, symbol->mode); - } - else - { - DATA_INVARIANT( - step.full_lhs_value.is_not_nil(), - "full_lhs_value in assignment must not be nil"); - full_lhs_value=json(step.full_lhs_value, ns, ID_unknown); } 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)); json_assignment["assignmentType"]= json_stringt( step.assignment_type== - goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? + goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? "actual-parameter": "variable"); } - break; + break; - case goto_trace_stept::typet::OUTPUT: + case goto_trace_stept::typet::OUTPUT: { - json_objectt &json_output=dest_array.push_back().make_object(); + json_objectt &json_output=dest.push_back().make_object(); json_output["stepType"]=json_stringt("output"); json_output["hidden"]=jsont::json_boolean(step.hidden); - json_output["internal"]=jsont::json_boolean(step.internal); json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); json_output["outputID"]=json_stringt(id2string(step.io_id)); - // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode=ID_unknown; - else - mode=function_name->mode; - json_output["mode"]=json_stringt(id2string(mode)); json_arrayt &json_values=json_output["values"].make_array(); for(const auto &arg : step.io_args) @@ -206,33 +146,23 @@ void convert( if(arg.is_nil()) json_values.push_back(json_stringt("")); else - json_values.push_back(json(arg, ns, mode)); + json_values.push_back(json(arg, ns)); } if(!json_location.is_null()) json_output["sourceLocation"]=json_location; } - break; + break; - case goto_trace_stept::typet::INPUT: + case goto_trace_stept::typet::INPUT: { - json_objectt &json_input=dest_array.push_back().make_object(); + json_objectt &json_input=dest.push_back().make_object(); json_input["stepType"]=json_stringt("input"); json_input["hidden"]=jsont::json_boolean(step.hidden); - json_input["internal"]=jsont::json_boolean(step.internal); json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); json_input["inputID"]=json_stringt(id2string(step.io_id)); - // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode=ID_unknown; - else - mode=function_name->mode; - json_input["mode"]=json_stringt(id2string(mode)); json_arrayt &json_values=json_input["values"].make_array(); for(const auto &arg : step.io_args) @@ -240,25 +170,24 @@ void convert( if(arg.is_nil()) json_values.push_back(json_stringt("")); else - json_values.push_back(json(arg, ns, mode)); + json_values.push_back(json(arg, ns)); } if(!json_location.is_null()) json_input["sourceLocation"]=json_location; } - break; + break; - case goto_trace_stept::typet::FUNCTION_CALL: - case goto_trace_stept::typet::FUNCTION_RETURN: + case goto_trace_stept::typet::FUNCTION_CALL: + case goto_trace_stept::typet::FUNCTION_RETURN: { std::string tag= (step.type==goto_trace_stept::typet::FUNCTION_CALL)? - "function-call":"function-return"; - json_objectt &json_call_return=dest_array.push_back().make_object(); + "function-call":"function-return"; + json_objectt &json_call_return=dest.push_back().make_object(); json_call_return["stepType"]=json_stringt(tag); json_call_return["hidden"]=jsont::json_boolean(step.hidden); - json_call_return["internal"]=jsont::json_boolean(step.internal); json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); const symbolt &symbol=ns.lookup(step.identifier); @@ -271,23 +200,22 @@ void convert( if(!json_location.is_null()) json_call_return["sourceLocation"]=json_location; } - break; + break; - default: - if(source_location!=previous_source_location) + default: + if(source_location!=previous_source_location) + { + // just the source location + if(!json_location.is_null()) { - // just the source location - if(!json_location.is_null()) - { - json_objectt &json_location_only=dest_array.push_back().make_object(); - json_location_only["stepType"]=json_stringt("location-only"); - json_location_only["hidden"]=jsont::json_boolean(step.hidden); - json_location_only["internal"]=jsont::json_boolean(step.internal); - json_location_only["thread"]= - json_numbert(std::to_string(step.thread_nr)); - json_location_only["sourceLocation"]=json_location; - } + json_objectt &json_location_only=dest.push_back().make_object(); + json_location_only["stepType"]=json_stringt("location-only"); + json_location_only["hidden"]=jsont::json_boolean(step.hidden); + json_location_only["thread"]= + json_numbert(std::to_string(step.thread_nr)); + json_location_only["sourceLocation"]=json_location; } + } } if(source_location.is_not_nil() && source_location.get_file()!="") @@ -295,4 +223,4 @@ void convert( } } -#endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H +#endif diff --git a/src/symex/symex_cover.cpp b/src/symex/symex_cover.cpp index 50c6a549885..2ce08cff01a 100644 --- a/src/symex/symex_cover.cpp +++ b/src/symex/symex_cover.cpp @@ -129,13 +129,15 @@ void symex_parse_optionst::report_cover( } case ui_message_handlert::uit::JSON_UI: { - json_objectt json_result; - json_arrayt &result_array=json_result["results"].make_array(); + json_stream_objectt &json_result= + result().json_stream().push_back_stream_object(); + json_stream_arrayt &result_array= + json_result.push_back_stream_array("result"); for(const auto &prop_pair : property_map) { const auto &property=prop_pair.second; - json_objectt &result=result_array.push_back().make_object(); + json_stream_objectt &result=result_array.push_back_stream_object(); result["status"]= json_stringt(property.is_failure()?"satisfied":"failed"); result["goal"]=json_stringt(id2string(prop_pair.first)); @@ -150,8 +152,9 @@ void symex_parse_optionst::report_cover( if(cmdline.isset("trace")) { - jsont &json_trace=result["trace"]; - convert(ns, property.error_trace, json_trace); + json_stream_arrayt &json_trace= + result.push_back_stream_array("trace");; + convert(ns, property.error_trace, json_trace); } else { @@ -174,7 +177,7 @@ void symex_parse_optionst::report_cover( json_result["totalGoals"]= json_numbert(std::to_string(property_map.size())); json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); - std::cout << ",\n" << json_result; + break; } } diff --git a/src/util/json.cpp b/src/util/json.cpp index f8cad9886cc..a607e675bcf 100644 --- a/src/util/json.cpp +++ b/src/util/json.cpp @@ -118,7 +118,8 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const } } -void jsont::output_object(std::ostream &out, const objectt &object, unsigned indent) +void jsont::output_object(std::ostream &out, + const objectt &object, unsigned indent) { for(objectt::const_iterator o_it=object.begin(); o_it!=object.end(); diff --git a/src/util/json.h b/src/util/json.h index 63a6e909744..78c8b60be91 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -126,7 +126,8 @@ class jsont typedef std::map objectt; objectt object; - static void output_object(std::ostream &out, const objectt &object, unsigned indent); + static void output_object(std::ostream &out, + const objectt &object, unsigned indent); static void output_key(std::ostream &out, const std::string &key); std::string value; diff --git a/src/util/json_stream.cpp b/src/util/json_stream.cpp index 8a6113b76c4..2f666dc643c 100644 --- a/src/util/json_stream.cpp +++ b/src/util/json_stream.cpp @@ -82,7 +82,8 @@ json_stream_arrayt &json_stream_arrayt::push_back_stream_array() return create_current_array(); } -json_stream_objectt &json_stream_objectt::push_back_stream_object(const std::string &key) +json_stream_objectt &json_stream_objectt::push_back_stream_object( + const std::string &key) { PRECONDITION(open); output_current(); @@ -91,7 +92,8 @@ json_stream_objectt &json_stream_objectt::push_back_stream_object(const std::str return create_current_object(); } -json_stream_arrayt &json_stream_objectt::push_back_stream_array(const std::string &key) +json_stream_arrayt &json_stream_objectt::push_back_stream_array( + const std::string &key) { PRECONDITION(open); output_current(); diff --git a/src/util/json_stream.h b/src/util/json_stream.h index 8c14478342d..39669d3058e 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -63,10 +63,10 @@ class json_streamt } }; -class json_stream_arrayt : public json_streamt +class json_stream_arrayt:public json_streamt { public: - json_stream_arrayt(std::ostream &out, unsigned indent = 0); + explicit json_stream_arrayt(std::ostream &out, unsigned indent=0); ~json_stream_arrayt() { @@ -99,7 +99,7 @@ class json_stream_arrayt : public json_streamt class json_stream_objectt:public json_streamt { public: - json_stream_objectt(std::ostream &out, unsigned indent = 0); + explicit json_stream_objectt(std::ostream &out, unsigned indent=0); jsont &operator[](const std::string &key) { diff --git a/src/util/message.h b/src/util/message.h index 93238635742..4ff11833c12 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -29,9 +29,10 @@ class message_handlert virtual void print(unsigned level, const std::string &message) = 0; - virtual json_stream_arrayt &get_json_stream() + virtual json_stream_arrayt *get_json_stream() { UNREACHABLE; + return nullptr; } virtual void print( @@ -197,7 +198,7 @@ class messaget json_stream_arrayt &json_stream() { *this << eom; // force end of previous message - return message.message_handler->get_json_stream(); + return *message.message_handler->get_json_stream(); } }; diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index b83719bf1fa..6b6beededc2 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -42,7 +42,6 @@ ui_message_handlert::ui_message_handlert( case uit::JSON_UI: { - INVARIANT(json_stream, "JSON stream must be initialized before use"); json_stream->push_back().make_object()["program"] = json_stringt(program); } break; @@ -75,7 +74,6 @@ ui_message_handlert::~ui_message_handlert() break; case uit::JSON_UI: - INVARIANT(json_stream, "JSON stream must be initialized before use"); json_stream->close(); out << '\n'; break; @@ -124,7 +122,6 @@ void ui_message_handlert::print( void ui_message_handlert::print( unsigned level, - json_stream->push_back(data); const std::string &message, int sequence_number, const source_locationt &location) @@ -207,7 +204,6 @@ void ui_message_handlert::json_ui_msg( const std::string &msg2, const source_locationt &location) { - INVARIANT(json_stream, "JSON stream must be initialized before use"); json_objectt &result = json_stream->push_back().make_object(); #if 0 diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 0075f025484..e4afd4474ad 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_UI_MESSAGE_H #define CPROVER_UTIL_UI_MESSAGE_H +#include + #include "message.h" class json_stream_arrayt; @@ -35,15 +37,16 @@ class ui_message_handlert:public message_handlert _ui=__ui; if(_ui == uit::JSON_UI && !json_stream) { - json_stream = std::unique_ptr(new json_stream_arrayt(out)); + json_stream= + std::unique_ptr(new json_stream_arrayt(out)); } } virtual void flush(unsigned level); - json_stream_arrayt &get_json_stream() override + json_stream_arrayt *get_json_stream() override { - return *json_stream; + return json_stream.get(); } protected: From cafc3fc9bc82500f4c83f9b8785e8c675bddd1a1 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 26 Jan 2018 17:11:18 +0000 Subject: [PATCH 6/6] Refactor huge convert function into instruction specific ones --- src/goto-programs/json_goto_trace.cpp | 160 ++++++++++++++++++++++++ src/goto-programs/json_goto_trace.h | 167 ++++++-------------------- src/util/ui_message.h | 6 +- 3 files changed, 203 insertions(+), 130 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index dd9fe58ab8a..a73baabeca7 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -19,4 +19,164 @@ Author: Daniel Kroening #include "json_goto_trace.h" +void convert_assert(json_objectt &json_failure, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + const source_locationt &source_location=conversion_dependencies.source_location; + irep_idt property_id = step.pc->is_assert()? + source_location.get_property_id(): + step.pc->is_goto()? + id2string(step.pc->source_location.get_function())+ + ".unwind."+std::to_string(step.pc->loop_number): + ""; + + json_failure["stepType"]=json_stringt("failure"); + json_failure["hidden"]=jsont::json_boolean(step.hidden); + json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_failure["reason"]=json_stringt(id2string(step.comment)); + json_failure["property"]=json_stringt(id2string(property_id)); + + if(!location.is_null()) + json_failure["sourceLocation"]=location; +} + +void convert_decl(json_objectt &json_assignment, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + const namespacet &ns=conversion_dependencies.ns; + + irep_idt identifier=step.lhs_object.get_identifier(); + + json_assignment["stepType"]=json_stringt("assignment"); + + if(!location.is_null()) + json_assignment["sourceLocation"]=location; + + std::string value_string, binary_string, type_string, full_lhs_string; + json_objectt full_lhs_value; + + if(step.full_lhs.is_not_nil()) + full_lhs_string=from_expr(ns, identifier, step.full_lhs); + + if(step.full_lhs_value.is_not_nil()) + full_lhs_value = json(step.full_lhs_value, ns); + + const symbolt *symbol; + irep_idt base_name, display_name; + + if(!ns.lookup(identifier, symbol)) + { + base_name=symbol->base_name; + display_name=symbol->display_name(); + if(type_string=="") + type_string=from_type(ns, identifier, symbol->type); + + json_assignment["mode"]=json_stringt(id2string(symbol->mode)); + } + + json_assignment["value"]=full_lhs_value; + json_assignment["lhs"]=json_stringt(full_lhs_string); + json_assignment["hidden"]=jsont::json_boolean(step.hidden); + json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); + + json_assignment["assignmentType"]= + json_stringt( + step.assignment_type== + goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? + "actual-parameter": + "variable"); +} + + +void convert_output(json_objectt &json_output, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + const namespacet &ns=conversion_dependencies.ns; + + json_output["stepType"]=json_stringt("output"); + json_output["hidden"]=jsont::json_boolean(step.hidden); + json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_output["outputID"]=json_stringt(id2string(step.io_id)); + + json_arrayt &json_values=json_output["values"].make_array(); + + for(const auto &arg : step.io_args) + { + arg.is_nil()? + json_values.push_back(json_stringt("")): + json_values.push_back(json(arg, ns)); + } + + if(!location.is_null()) + json_output["sourceLocation"]=location; +} + +void convert_input(json_objectt &json_input, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + const namespacet &ns=conversion_dependencies.ns; + + json_input["stepType"]=json_stringt("input"); + json_input["hidden"]=jsont::json_boolean(step.hidden); + json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_input["inputID"]=json_stringt(id2string(step.io_id)); + + json_arrayt &json_values=json_input["values"].make_array(); + + for(const auto &arg : step.io_args) + { + arg.is_nil()? + json_values.push_back(json_stringt("")): + json_values.push_back(json(arg, ns)); + } + + if(!location.is_null()) + json_input["sourceLocation"]=location; + +} + +void convert_return(json_objectt &json_call_return, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + const namespacet &ns=conversion_dependencies.ns; + + std::string tag= (step.type==goto_trace_stept::typet::FUNCTION_CALL)? + "function-call" : "function-return"; + + json_call_return["stepType"]=json_stringt(tag); + json_call_return["hidden"]=jsont::json_boolean(step.hidden); + json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); + + const symbolt &symbol=ns.lookup(step.identifier); + json_objectt &json_function=json_call_return["function"].make_object(); + json_function["displayName"]= + json_stringt(id2string(symbol.display_name())); + json_function["identifier"]=json_stringt(id2string(step.identifier)); + json_function["sourceLocation"]=json(symbol.location); + + if(!location.is_null()) + json_call_return["sourceLocation"]=location; +} + +void convert_default(json_objectt &json_location_only, + conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept& step=conversion_dependencies.step; + jsont &location=conversion_dependencies.location; + + json_location_only["stepType"]=json_stringt("location-only"); + json_location_only["hidden"]=jsont::json_boolean(step.hidden); + json_location_only["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_location_only["sourceLocation"]=location; +} diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 9eb9969a1b7..5d967d4423f 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -30,6 +30,32 @@ Date: November 2005 #include #include +typedef struct +{ + jsont &location; + const goto_trace_stept& step; + const namespacet &ns; + const source_locationt &source_location; +} conversion_dependenciest; + +void convert_assert(json_objectt &json_failure, + conversion_dependenciest &conversion_dependencies); + +void convert_decl(json_objectt &json_assignment, + conversion_dependenciest &conversion_dependencies); + +void convert_output(json_objectt &json_output, + conversion_dependenciest &conversion_dependencies); + +void convert_input(json_objectt &json_input, + conversion_dependenciest &conversion_dependencies); + +void convert_return(json_objectt &json_call_return, + conversion_dependenciest &conversion_dependencies); + +void convert_default(json_objectt &json_location_only, + conversion_dependenciest &conversion_dependencies); + template void convert( const namespacet &ns, @@ -44,161 +70,52 @@ void convert( jsont json_location; - if(source_location.is_not_nil() && source_location.get_file()!="") - json_location=json(source_location); - else - json_location=json_nullt(); + source_location.is_not_nil()&&source_location.get_file()!=""? + json_location=json(source_location): + json_location=json_nullt(); + + conversion_dependenciest conversion_dependencies= + { + json_location, step, ns, source_location + }; switch(step.type) { case goto_trace_stept::typet::ASSERT: if(!step.cond_value) { - irep_idt property_id; - - if(step.pc->is_assert()) - property_id=source_location.get_property_id(); - else if(step.pc->is_goto()) // unwinding, we suspect - { - property_id= - id2string(step.pc->source_location.get_function())+ - ".unwind."+std::to_string(step.pc->loop_number); - } - json_objectt &json_failure=dest.push_back().make_object(); - - json_failure["stepType"]=json_stringt("failure"); - json_failure["hidden"]=jsont::json_boolean(step.hidden); - json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_failure["reason"]=json_stringt(id2string(step.comment)); - json_failure["property"]=json_stringt(id2string(property_id)); - - if(!json_location.is_null()) - json_failure["sourceLocation"]=json_location; + convert_assert(json_failure, conversion_dependencies); } break; case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::DECL: { - irep_idt identifier=step.lhs_object.get_identifier(); json_objectt &json_assignment=dest.push_back().make_object(); - - json_assignment["stepType"]=json_stringt("assignment"); - - if(!json_location.is_null()) - json_assignment["sourceLocation"]=json_location; - - std::string value_string, binary_string, type_string, full_lhs_string; - json_objectt full_lhs_value; - - if(step.full_lhs.is_not_nil()) - full_lhs_string=from_expr(ns, identifier, step.full_lhs); - -#if 0 - if(it.full_lhs_value.is_not_nil()) - full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value); -#endif - - if(step.full_lhs_value.is_not_nil()) - full_lhs_value = json(step.full_lhs_value, ns); - - const symbolt *symbol; - irep_idt base_name, display_name; - - if(!ns.lookup(identifier, symbol)) - { - base_name=symbol->base_name; - display_name=symbol->display_name(); - if(type_string=="") - type_string=from_type(ns, identifier, symbol->type); - - json_assignment["mode"]=json_stringt(id2string(symbol->mode)); - } - - json_assignment["value"]=full_lhs_value; - json_assignment["lhs"]=json_stringt(full_lhs_string); - json_assignment["hidden"]=jsont::json_boolean(step.hidden); - json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); - - json_assignment["assignmentType"]= - json_stringt( - step.assignment_type== - goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? - "actual-parameter": - "variable"); + convert_decl(json_assignment, conversion_dependencies); } break; case goto_trace_stept::typet::OUTPUT: { json_objectt &json_output=dest.push_back().make_object(); - - json_output["stepType"]=json_stringt("output"); - json_output["hidden"]=jsont::json_boolean(step.hidden); - json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_output["outputID"]=json_stringt(id2string(step.io_id)); - - json_arrayt &json_values=json_output["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns)); - } - - if(!json_location.is_null()) - json_output["sourceLocation"]=json_location; + convert_output(json_output, conversion_dependencies); } break; case goto_trace_stept::typet::INPUT: { json_objectt &json_input=dest.push_back().make_object(); - - json_input["stepType"]=json_stringt("input"); - json_input["hidden"]=jsont::json_boolean(step.hidden); - json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_input["inputID"]=json_stringt(id2string(step.io_id)); - - json_arrayt &json_values=json_input["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns)); - } - - if(!json_location.is_null()) - json_input["sourceLocation"]=json_location; + convert_input(json_input, conversion_dependencies); } break; case goto_trace_stept::typet::FUNCTION_CALL: case goto_trace_stept::typet::FUNCTION_RETURN: { - std::string tag= - (step.type==goto_trace_stept::typet::FUNCTION_CALL)? - "function-call":"function-return"; json_objectt &json_call_return=dest.push_back().make_object(); - - json_call_return["stepType"]=json_stringt(tag); - json_call_return["hidden"]=jsont::json_boolean(step.hidden); - json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); - - const symbolt &symbol=ns.lookup(step.identifier); - json_objectt &json_function=json_call_return["function"].make_object(); - json_function["displayName"]= - json_stringt(id2string(symbol.display_name())); - json_function["identifier"]=json_stringt(id2string(step.identifier)); - json_function["sourceLocation"]=json(symbol.location); - - if(!json_location.is_null()) - json_call_return["sourceLocation"]=json_location; + convert_return(json_call_return, conversion_dependencies); } break; @@ -209,11 +126,7 @@ void convert( if(!json_location.is_null()) { json_objectt &json_location_only=dest.push_back().make_object(); - json_location_only["stepType"]=json_stringt("location-only"); - json_location_only["hidden"]=jsont::json_boolean(step.hidden); - json_location_only["thread"]= - json_numbert(std::to_string(step.thread_nr)); - json_location_only["sourceLocation"]=json_location; + convert_default(json_location_only, conversion_dependencies); } } } diff --git a/src/util/ui_message.h b/src/util/ui_message.h index e4afd4474ad..3ebdd8927e9 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -42,7 +42,7 @@ class ui_message_handlert:public message_handlert } } - virtual void flush(unsigned level); + virtual void flush(unsigned level) override; json_stream_arrayt *get_json_stream() override { @@ -57,14 +57,14 @@ class ui_message_handlert:public message_handlert // overloading virtual void print( unsigned level, - const std::string &message); + const std::string &message) override; // overloading virtual void print( unsigned level, const std::string &message, int sequence_number, - const source_locationt &location); + const source_locationt &location) override; virtual void xml_ui_msg( const std::string &type,