diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index bd9c5242dd4..2ce0f60e4f2 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -207,24 +207,24 @@ 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); } } - - std::cout << ",\n" << json_result; } break; } diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index f92483d2441..4e309dfaa0b 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,17 @@ 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_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"); - jsont &json_trace=result["trace"]; - convert(ns, goto_trace, json_trace); - std::cout << ",\n" << json_result; + 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/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/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index ddc9f44ad3b..a73baabeca7 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -19,196 +19,164 @@ Author: Daniel Kroening #include "json_goto_trace.h" -void convert( - const namespacet &ns, - const goto_tracet &goto_trace, - jsont &dest) +void convert_assert(json_objectt &json_failure, + conversion_dependenciest &conversion_dependencies) { - json_arrayt &dest_array=dest.make_array(); + 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; - source_locationt previous_source_location; + 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)); - for(const auto &step : goto_trace.steps) + 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) { - 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()) - 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; + 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 102569b50e6..5d967d4423f 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -15,12 +15,125 @@ 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 + +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 &, - const goto_tracet &, - jsont &); + const namespacet &ns, + const goto_tracet &goto_trace, + newJson &dest) +{ + source_locationt previous_source_location; + + for(const auto &step : goto_trace.steps) + { + const source_locationt &source_location=step.pc->source_location; + + jsont json_location; + + 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) + { + json_objectt &json_failure=dest.push_back().make_object(); + convert_assert(json_failure, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::ASSIGNMENT: + case goto_trace_stept::typet::DECL: + { + json_objectt &json_assignment=dest.push_back().make_object(); + convert_decl(json_assignment, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::OUTPUT: + { + json_objectt &json_output=dest.push_back().make_object(); + convert_output(json_output, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::INPUT: + { + json_objectt &json_input=dest.push_back().make_object(); + convert_input(json_input, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::FUNCTION_CALL: + case goto_trace_stept::typet::FUNCTION_RETURN: + { + json_objectt &json_call_return=dest.push_back().make_object(); + convert_return(json_call_return, conversion_dependencies); + } + break; + + default: + if(source_location!=previous_source_location) + { + // just the source location + if(!json_location.is_null()) + { + json_objectt &json_location_only=dest.push_back().make_object(); + convert_default(json_location_only, conversion_dependencies); + } + } + } + + if(source_location.is_not_nil() && source_location.get_file()!="") + previous_source_location=source_location; + } +} -#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/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..a607e675bcf 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,33 @@ 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..78c8b60be91 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,14 @@ 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..2f666dc643c --- /dev/null +++ b/src/util/json_stream.cpp @@ -0,0 +1,125 @@ +/*******************************************************************\ + +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..39669d3058e --- /dev/null +++ b/src/util/json_stream.h @@ -0,0 +1,131 @@ +/*******************************************************************\ + +Module: + +Author: Peter Schrammel + +\*******************************************************************/ + + +#ifndef CPROVER_UTIL_JSON_STREAM_H +#define CPROVER_UTIL_JSON_STREAM_H + +#include + +#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: + explicit 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: + explicit 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 diff --git a/src/util/message.h b/src/util/message.h index 1d4b3d54e40..4ff11833c12 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -14,7 +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 { @@ -25,6 +29,12 @@ class message_handlert virtual void print(unsigned level, const std::string &message) = 0; + virtual json_stream_arrayt *get_json_stream() + { + UNREACHABLE; + return nullptr; + } + virtual void print( unsigned level, const std::string &message, @@ -184,6 +194,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..6b6beededc2 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -13,37 +13,36 @@ 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; + json_stream->push_back().make_object()["program"] = json_stringt(program); } break; } @@ -60,16 +59,23 @@ 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"; + json_stream->close(); + out << '\n'; break; case uit::PLAIN: @@ -188,8 +194,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 +204,7 @@ void ui_message_handlert::json_ui_msg( const std::string &msg2, const source_locationt &location) { - json_objectt result; + json_objectt &result = json_stream->push_back().make_object(); #if 0 if(location.is_not_nil() && @@ -208,11 +214,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 +230,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..3ebdd8927e9 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -10,8 +10,12 @@ 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; + class ui_message_handlert:public message_handlert { public: @@ -19,10 +23,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,24 +35,36 @@ 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); + virtual void flush(unsigned level) override; + + json_stream_arrayt *get_json_stream() override + { + return json_stream.get(); + } protected: uit _ui; + std::ostream &out; + std::unique_ptr json_stream; // 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,