From f4be7b853546c449d44ca39bc97c71ce33f492ac Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 19:53:16 +0000 Subject: [PATCH 1/4] Change uit configuration to xml-specific Boolean choice --- .../instantiate_not_contains.cpp | 3 +-- src/cbmc/cbmc_solvers.cpp | 4 ++-- src/solvers/refinement/bv_refinement.h | 4 +--- src/solvers/refinement/bv_refinement_loop.cpp | 4 +--- src/solvers/refinement/string_refinement_util.h | 2 ++ 5 files changed, 7 insertions(+), 10 deletions(-) diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 6b23f790191..c86bca770de 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -152,8 +152,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) bv_refinementt::infot info; info.ns=&ns; info.prop=&sat_check; - const auto ui=ui_message_handlert::uit::PLAIN; - info.ui=ui; + info.output_xml = false; bv_refinementt solver(info); solver << expr; return solver(); diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index fe1d40179aa..6776cf7032f 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -118,7 +118,7 @@ std::unique_ptr cbmc_solverst::get_bv_refinement() bv_refinementt::infot info; info.ns=&ns; info.prop=prop.get(); - info.ui=ui; + info.output_xml = ui == ui_message_handlert::uit::XML_UI; // we allow setting some parameters if(options.get_bool_option("max-node-refinement")) @@ -144,7 +144,7 @@ std::unique_ptr cbmc_solverst::get_string_refinement() prop->set_message_handler(get_message_handler()); info.prop=prop.get(); info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT; - info.ui=ui; + info.output_xml = ui == ui_message_handlert::uit::XML_UI; if(options.get_bool_option("max-node-refinement")) info.max_node_refinement= options.get_unsigned_int_option("max-node-refinement"); diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 05b4c056d9b..b371a9feda8 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H -#include - #include #define MAX_STATE 10000 @@ -23,7 +21,7 @@ class bv_refinementt:public bv_pointerst private: struct configt { - ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN; + bool output_xml = false; /// Max number of times we refine a formula node unsigned max_node_refinement=5; /// Enable array refinement diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index c49875d152f..de898bca4cc 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_refinement.h" -#include - #include bv_refinementt::bv_refinementt(const infot &info): @@ -41,7 +39,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve() status() << "BV-Refinement: iteration " << iteration << eom; // output the very same information in a structured fashion - if(config_.ui==ui_message_handlert::uit::XML_UI) + if(config_.output_xml) { xmlt xml("refinement-iteration"); xml.data=std::to_string(iteration); diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index fc045299cc7..86e3003cb4f 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -9,6 +9,8 @@ #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H +#include + #include "string_builtin_function.h" #include "string_constraint.h" #include "string_constraint_generator.h" From 49920a4361b19e50ec29cb5106e2c38f629bde1f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 21 Jun 2018 12:46:15 +0100 Subject: [PATCH 2/4] Do not artificially separate message handler and uit They were passed around independently, even though they originated from the very same object. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 22 +++++------- jbmc/src/jdiff/java_syntactic_diff.h | 2 +- jbmc/src/jdiff/jdiff_parse_options.cpp | 3 +- src/cbmc/all_properties.cpp | 2 +- src/cbmc/bmc.cpp | 34 +++++++++++-------- src/cbmc/bmc.h | 21 +++++------- src/cbmc/bmc_cover.cpp | 4 +-- src/cbmc/cbmc_parse_options.cpp | 6 +--- src/cbmc/cbmc_solvers.cpp | 16 ++++----- src/cbmc/cbmc_solvers.h | 23 ++++++------- src/cbmc/fault_localization.cpp | 4 +-- src/goto-diff/goto_diff.h | 11 +++--- src/goto-diff/goto_diff_base.cpp | 25 ++++++++------ src/goto-diff/goto_diff_parse_options.cpp | 3 +- src/goto-diff/syntactic_diff.h | 2 +- .../goto_instrument_parse_options.cpp | 3 +- src/goto-programs/class_hierarchy.cpp | 5 ++- src/goto-programs/class_hierarchy.h | 4 +-- src/goto-programs/show_symbol_table.cpp | 4 +-- src/goto-symex/show_vcc.cpp | 7 ++-- src/goto-symex/show_vcc.h | 3 +- src/util/ui_message.h | 10 ------ unit/path_strategies.cpp | 7 ++-- 23 files changed, 96 insertions(+), 125 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ddfa8cbe9fc..307530f64c4 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -523,8 +523,7 @@ int jbmc_parse_optionst::doit() path_strategy_chooser, options, goto_model, - ui_message_handler.get_ui(), - *this, + ui_message_handler, configure_bmc); } else @@ -557,15 +556,13 @@ int jbmc_parse_optionst::doit() // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. - return - bmct::do_language_agnostic_bmc( - path_strategy_chooser, - options, - lazy_goto_model, - ui_message_handler.get_ui(), - *this, - configure_bmc, - callback_after_symex); + return bmct::do_language_agnostic_bmc( + path_strategy_chooser, + options, + lazy_goto_model, + ui_message_handler, + configure_bmc, + callback_after_symex); } } @@ -618,8 +615,7 @@ int jbmc_parse_optionst::get_goto_program( { class_hierarchyt hierarchy; hierarchy(lazy_goto_model.symbol_table); - show_class_hierarchy( - hierarchy, get_message_handler(), ui_message_handler.get_ui()); + show_class_hierarchy(hierarchy, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/jdiff/java_syntactic_diff.h b/jbmc/src/jdiff/java_syntactic_diff.h index 9d886b447cc..fc68949ff29 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.h +++ b/jbmc/src/jdiff/java_syntactic_diff.h @@ -21,7 +21,7 @@ class java_syntactic_difft : public goto_difft const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, const optionst &_options, - message_handlert &_message_handler) + ui_message_handlert &_message_handler) : goto_difft(_goto_model1, _goto_model2, _options, _message_handler) { } diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 1fdeb659850..6464c51c7e3 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -274,8 +274,7 @@ int jdiff_parse_optionst::doit() } java_syntactic_difft sd( - goto_model1, goto_model2, options, get_message_handler()); - sd.set_ui(get_ui()); + goto_model1, goto_model2, options, ui_message_handler); sd(); sd.output_functions(); diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 260be88b829..13ce24a5090 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -152,7 +152,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()() void bmc_all_propertiest::report(const cover_goalst &cover_goals) { - switch(bmc.ui) + switch(bmc.ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: { diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 0bb68a80439..b0856cf5011 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -54,7 +54,7 @@ void bmct::error_trace() goto_tracet &goto_trace=safety_checkert::error_trace; build_goto_trace(equation, prop_conv, ns, goto_trace); - switch(ui) + switch(ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: result() << "Counterexample:" << eom; @@ -153,7 +153,7 @@ void bmct::report_success() { result() << "VERIFICATION SUCCESSFUL" << eom; - switch(ui) + switch(ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: break; @@ -180,7 +180,7 @@ void bmct::report_failure() { result() << "VERIFICATION FAILED" << eom; - switch(ui) + switch(ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: break; @@ -294,7 +294,7 @@ safety_checkert::resultt bmct::execute( if(options.get_bool_option("show-vcc")) { - show_vcc(options, get_message_handler(), ui, ns, equation); + show_vcc(options, ui_message_handler, ns, equation); return safety_checkert::resultt::SAFE; // to indicate non-error } @@ -420,7 +420,7 @@ void bmct::show() { if(options.get_bool_option("show-vcc")) { - show_vcc(options, get_message_handler(), ui, ns, equation); + show_vcc(options, ui_message_handler, ns, equation); } if(options.get_bool_option("program-only")) @@ -478,15 +478,14 @@ int bmct::do_language_agnostic_bmc( const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &model, - const ui_message_handlert::uit &ui, - messaget &message, + ui_message_handlert &ui, std::function driver_configure_bmc, std::function callback_after_symex) { safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN; safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN; const symbol_tablet &symbol_table = model.get_symbol_table(); - message_handlert &mh = message.get_message_handler(); + messaget message(ui); std::unique_ptr worklist; std::string strategy = opts.get_option("exploration-strategy"); INVARIANT( @@ -496,13 +495,15 @@ int bmct::do_language_agnostic_bmc( try { { - cbmc_solverst solvers(opts, symbol_table, message.get_message_handler()); - solvers.set_ui(ui); + cbmc_solverst solvers( + opts, + symbol_table, + ui, + ui.get_ui() == ui_message_handlert::uit::XML_UI); std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex); - bmc.set_ui(ui); + bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex); if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); tmp_result = bmc.run(model); @@ -546,8 +547,11 @@ int bmct::do_language_agnostic_bmc( << "Starting new path (" << worklist->size() << " to go)\n" << message.eom; - cbmc_solverst solvers(opts, symbol_table, message.get_message_handler()); - solvers.set_ui(ui); + cbmc_solverst solvers( + opts, + symbol_table, + ui, + ui.get_ui() == ui_message_handlert::uit::XML_UI); std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); @@ -555,7 +559,7 @@ int bmct::do_language_agnostic_bmc( path_explorert pe( opts, symbol_table, - mh, + ui, pc, resume.equation, resume.state, diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 91cc217a85d..142967c4b1e 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -66,7 +66,7 @@ class bmct:public safety_checkert bmct( const optionst &_options, const symbol_tablet &outer_symbol_table, - message_handlert &_message_handler, + ui_message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, std::function callback_after_symex) @@ -83,7 +83,7 @@ class bmct:public safety_checkert options, path_storage), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN), + ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) { symex.constant_propagation=options.get_bool_option("propagation"); @@ -103,8 +103,6 @@ class bmct:public safety_checkert safety_checkert::resultt execute(abstract_goto_modelt &); virtual ~bmct() { } - void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } - // the safety_checkert interface virtual resultt operator()( const goto_functionst &goto_functions) @@ -127,10 +125,9 @@ class bmct:public safety_checkert const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, - const ui_message_handlert::uit &ui, - messaget &message, - std::function - driver_configure_bmc = nullptr, + ui_message_handlert &ui, + std::function driver_configure_bmc = + nullptr, std::function callback_after_symex = nullptr); protected: @@ -144,7 +141,7 @@ class bmct:public safety_checkert bmct( const optionst &_options, const symbol_tablet &outer_symbol_table, - message_handlert &_message_handler, + ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, @@ -162,7 +159,7 @@ class bmct:public safety_checkert options, path_storage), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN), + ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) { symex.constant_propagation = options.get_bool_option("propagation"); @@ -186,7 +183,7 @@ class bmct:public safety_checkert prop_convt &prop_conv; std::unique_ptr memory_model; // use gui format - ui_message_handlert::uit ui; + ui_message_handlert &ui_message_handler; virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv); @@ -259,7 +256,7 @@ class path_explorert : public bmct path_explorert( const optionst &_options, const symbol_tablet &outer_symbol_table, - message_handlert &_message_handler, + ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 3bb617e7bd1..1e1e8658f02 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -261,7 +261,7 @@ bool bmc_covert::operator()() if(g.second.satisfied) goals_covered++; - switch(bmc.ui) + switch(bmc.ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: { @@ -406,7 +406,7 @@ bool bmc_covert::operator()() << (cover_goals.iterations()==1?"":"s") << eom; - if(bmc.ui==ui_message_handlert::uit::PLAIN) + if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN) { result() << "Test suite:" << '\n'; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b59f801b08e..09cc717343d 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -527,11 +527,7 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_SET_PROPERTIES_FAILED; return bmct::do_language_agnostic_bmc( - path_strategy_chooser, - options, - goto_model, - ui_message_handler.get_ui(), - *this); + path_strategy_chooser, options, goto_model, ui_message_handler); } bool cbmc_parse_optionst::set_properties() diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 6776cf7032f..0b07ba147da 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -72,7 +72,7 @@ std::unique_ptr cbmc_solverst::get_default() solver->set_prop(util_make_unique()); } - solver->prop().set_message_handler(get_message_handler()); + solver->prop().set_message_handler(message_handler); auto bv_pointers = util_make_unique(ns, solver->prop()); @@ -92,7 +92,7 @@ std::unique_ptr cbmc_solverst::get_dimacs() no_incremental_check(); auto prop=util_make_unique(); - prop->set_message_handler(get_message_handler()); + prop->set_message_handler(message_handler); std::string filename=options.get_option("outfile"); @@ -113,12 +113,12 @@ std::unique_ptr cbmc_solverst::get_bv_refinement() return util_make_unique(); }(); - prop->set_message_handler(get_message_handler()); + prop->set_message_handler(message_handler); bv_refinementt::infot info; info.ns=&ns; info.prop=prop.get(); - info.output_xml = ui == ui_message_handlert::uit::XML_UI; + info.output_xml = output_xml_in_refinement; // we allow setting some parameters if(options.get_bool_option("max-node-refinement")) @@ -141,10 +141,10 @@ std::unique_ptr cbmc_solverst::get_string_refinement() string_refinementt::infot info; info.ns=&ns; auto prop=util_make_unique(); - prop->set_message_handler(get_message_handler()); + prop->set_message_handler(message_handler); info.prop=prop.get(); info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT; - info.output_xml = ui == ui_message_handlert::uit::XML_UI; + info.output_xml = output_xml_in_refinement; if(options.get_bool_option("max-node-refinement")) info.max_node_refinement= options.get_unsigned_int_option("max-node-refinement"); @@ -197,7 +197,7 @@ std::unique_ptr cbmc_solverst::get_smt2( if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory=true; - smt2_conv->set_message_handler(get_message_handler()); + smt2_conv->set_message_handler(message_handler); return util_make_unique(std::move(smt2_conv)); } @@ -226,7 +226,7 @@ std::unique_ptr cbmc_solverst::get_smt2( if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory=true; - smt2_conv->set_message_handler(get_message_handler()); + smt2_conv->set_message_handler(message_handler); return util_make_unique(std::move(smt2_conv), std::move(out)); } diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 54bf3805e30..8a19735d343 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -26,18 +25,19 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class cbmc_solverst:public messaget +class cbmc_solverst { public: cbmc_solverst( const optionst &_options, const symbol_tablet &_symbol_table, - message_handlert &_message_handler): - messaget(_message_handler), - options(_options), - symbol_table(_symbol_table), - ns(_symbol_table), - ui(ui_message_handlert::uit::PLAIN) + message_handlert &_message_handler, + bool _output_xml_in_refinement) + : options(_options), + symbol_table(_symbol_table), + ns(_symbol_table), + message_handler(_message_handler), + output_xml_in_refinement(_output_xml_in_refinement) { } @@ -117,15 +117,12 @@ class cbmc_solverst:public messaget { } - void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } - protected: const optionst &options; const symbol_tablet &symbol_table; namespacet ns; - - // use gui format - ui_message_handlert::uit ui; + message_handlert &message_handler; + const bool output_xml_in_refinement; std::unique_ptr get_default(); std::unique_ptr get_dimacs(); diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 8df3fcbd61f..3ffa1eb0479 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -288,7 +288,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail() // localize faults run(ID_nil); - switch(bmc.ui) + switch(bmc.ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: { @@ -353,7 +353,7 @@ void fault_localizationt::report( { bmc_all_propertiest::report(cover_goals); - switch(bmc.ui) + switch(bmc.ui_message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: if(cover_goals.number_covered()>0) diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h index efb90d1ed1d..3a446f0bf5d 100644 --- a/src/goto-diff/goto_diff.h +++ b/src/goto-diff/goto_diff.h @@ -22,34 +22,31 @@ class json_arrayt; class json_objectt; class optionst; -class goto_difft:public messaget +class goto_difft { public: goto_difft( const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, const optionst &_options, - message_handlert &_message_handler) - : messaget(_message_handler), + ui_message_handlert &_message_handler) + : message_handler(_message_handler), goto_model1(_goto_model1), goto_model2(_goto_model2), options(_options), - ui(ui_message_handlert::uit::PLAIN), total_functions_count(0) { } virtual bool operator()()=0; - void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } - virtual void output_functions() const; protected: + ui_message_handlert &message_handler; const goto_modelt &goto_model1; const goto_modelt &goto_model2; const optionst &options; - ui_message_handlert::uit ui; unsigned total_functions_count; std::set new_functions, modified_functions, deleted_functions; diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 16a8f523979..734ce4bd9ea 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -20,18 +20,20 @@ Author: Peter Schrammel /// Output diff result void goto_difft::output_functions() const { - switch(ui) + messaget msg(message_handler); + + switch(message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: { - result() << "total number of functions: " << total_functions_count - << '\n'; + msg.result() << "total number of functions: " << total_functions_count + << '\n' << messaget::eom; output_function_group("new functions", new_functions, goto_model2); output_function_group( "modified functions", modified_functions, goto_model2); output_function_group( "deleted functions", deleted_functions, goto_model1); - result() << eom; + msg.result() << messaget::eom; break; } case ui_message_handlert::uit::JSON_UI: @@ -49,12 +51,12 @@ void goto_difft::output_functions() const json_result["deletedFunctions"].make_array(), deleted_functions, goto_model1); - result() << json_result; + msg.result() << json_result << messaget::eom; break; } case ui_message_handlert::uit::XML_UI: { - error() << "XML output not supported yet" << eom; + msg.error() << "XML output not supported yet" << messaget::eom; } } } @@ -68,7 +70,7 @@ void goto_difft::output_function_group( const std::set &function_group, const goto_modelt &goto_model) const { - result() << group_name << ":\n"; + messaget(message_handler).result() << group_name << ':' << messaget::eom; for(const auto &function_name : function_group) { output_function(function_name, goto_model); @@ -82,11 +84,12 @@ void goto_difft::output_function( const irep_idt &function_name, const goto_modelt &goto_model) const { + messaget msg(message_handler); + namespacet ns(goto_model.symbol_table); const symbolt &symbol = ns.lookup(function_name); - result() << " " << symbol.location.get_file() << ": " << function_name - << '\n'; + msg.result() << " " << symbol.location.get_file() << ": " << function_name; if(options.get_bool_option("show-properties")) { @@ -103,9 +106,11 @@ void goto_difft::output_function( const source_locationt &source_location = ins.source_location; irep_idt property_id = source_location.get_property_id(); - result() << " " << property_id << '\n'; + msg.result() << "\n " << property_id; } } + + msg.result() << messaget::eom; } /// Convert a function group to JSON diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index b307272be0e..f32e3a33015 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -317,8 +317,7 @@ int goto_diff_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } - syntactic_difft sd(goto_model1, goto_model2, options, get_message_handler()); - sd.set_ui(get_ui()); + syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler); sd(); sd.output_functions(); diff --git a/src/goto-diff/syntactic_diff.h b/src/goto-diff/syntactic_diff.h index b5a2b3216e2..7c1648490d3 100644 --- a/src/goto-diff/syntactic_diff.h +++ b/src/goto-diff/syntactic_diff.h @@ -21,7 +21,7 @@ class syntactic_difft:public goto_difft const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, const optionst &_options, - message_handlert &_message_handler) + ui_message_handlert &_message_handler) : goto_difft(_goto_model1, _goto_model2, _options, _message_handler) { } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 80f7d0b2491..d7cadc121f1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -696,8 +696,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("dot")) hierarchy.output_dot(std::cout); else - show_class_hierarchy( - hierarchy, get_message_handler(), ui_message_handler.get_ui()); + show_class_hierarchy(hierarchy, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index db7cb2c5d90..9c996afb5b6 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -262,12 +262,11 @@ void class_hierarchyt::output( void show_class_hierarchy( const class_hierarchyt &hierarchy, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &message_handler, bool children_only) { messaget msg(message_handler); - switch(ui) + switch(message_handler.get_ui()) { case ui_message_handlert::uit::PLAIN: hierarchy.output(msg.result(), children_only); diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 74d991730ea..abc3b390290 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -32,7 +32,6 @@ Date: April 2016 class symbol_tablet; class json_stream_arrayt; -class message_handlert; /// Non-graph-based representation of the class hierarchy. /// \deprecated `class_hierarchy_grapht` is a more advanced graph-based @@ -135,8 +134,7 @@ class class_hierarchy_grapht : public grapht /// \param children_only: print the children only and do not print the parents void show_class_hierarchy( const class_hierarchyt &hierarchy, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &message_handler, bool children_only = false); #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 9f5aaac1ec9..b5016e74b24 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -157,7 +157,7 @@ void show_symbol_table_plain( static void show_symbol_table_json_ui( const symbol_tablet &symbol_table, - message_handlert &message_handler) + ui_message_handlert &message_handler) { json_stream_arrayt &out = message_handler.get_json_stream(); @@ -232,7 +232,7 @@ static void show_symbol_table_json_ui( static void show_symbol_table_brief_json_ui( const symbol_tablet &symbol_table, - message_handlert &message_handler) + ui_message_handlert &message_handler) { json_stream_arrayt &out = message_handler.get_json_stream(); diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp index 6116759b66c..6af3513c79e 100644 --- a/src/goto-symex/show_vcc.cpp +++ b/src/goto-symex/show_vcc.cpp @@ -149,12 +149,11 @@ void show_vcc_json( void show_vcc( const optionst &options, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation) { - messaget msg(message_handler); + messaget msg(ui_message_handler); const std::string &filename = options.get_option("outfile"); bool have_file = !filename.empty() && filename != "-"; @@ -170,7 +169,7 @@ void show_vcc( std::ostream &out = have_file ? of : std::cout; - switch(ui) + switch(ui_message_handler.get_ui()) { case ui_message_handlert::uit::XML_UI: msg.error() << "XML UI not supported" << messaget::eom; diff --git a/src/goto-symex/show_vcc.h b/src/goto-symex/show_vcc.h index da3fe20a7aa..a428941cd15 100644 --- a/src/goto-symex/show_vcc.h +++ b/src/goto-symex/show_vcc.h @@ -20,8 +20,7 @@ class symex_target_equationt; void show_vcc( const optionst &options, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation); diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 4a4fc104dd3..67670c3a340 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -39,16 +39,6 @@ class ui_message_handlert : public message_handlert return _ui; } - 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) override; json_stream_arrayt &get_json_stream() override diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 1ad321d6887..74221617055 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -362,14 +362,12 @@ void _check_with_strategy( ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh); REQUIRE(ret == -1); - cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); - solvers.set_ui(mh.get_ui()); + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh, false); std::unique_ptr cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); std::function callback = []() { return false; }; bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback); - bmc.set_ui(mh.get_ui()); safety_checkert::resultt result = bmc.run(gm); symex_eventt::validate_result(events, result); @@ -382,8 +380,7 @@ void _check_with_strategy( while(!worklist->empty()) { - cbmc_solverst solvers(opts, gm.get_symbol_table(), mh); - solvers.set_ui(mh.get_ui()); + cbmc_solverst solvers(opts, gm.get_symbol_table(), mh, false); cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); path_storaget::patht &resume = worklist->peek(); From 2518473ec5e70440fa947ca3b984e84ebbd10356 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Sep 2018 11:39:08 +0000 Subject: [PATCH 3/4] Restrict get_json_stream to ui_message_handler ... now that we properly pass around ui_message_handlert we can clean up the JSON stream handling as well. --- src/cbmc/all_properties.cpp | 4 +++- src/cbmc/bmc.cpp | 4 +++- src/cbmc/bmc_cover.cpp | 4 +++- src/goto-programs/class_hierarchy.cpp | 4 +++- src/util/message.h | 17 +---------------- src/util/ui_message.cpp | 9 ++------- src/util/ui_message.h | 2 +- 7 files changed, 16 insertions(+), 28 deletions(-) diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 13ce24a5090..126be18cf3d 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -202,8 +202,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) case ui_message_handlert::uit::JSON_UI: { + if(result().tellp() > 0) + result() << eom; // force end of previous message json_stream_objectt &json_result = - result().json_stream().push_back_stream_object(); + bmc.ui_message_handler.get_json_stream().push_back_stream_object(); json_stream_arrayt &result_array = json_result.push_back_stream_array("result"); diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index b0856cf5011..48a8e2784d3 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -72,8 +72,10 @@ void bmct::error_trace() case ui_message_handlert::uit::JSON_UI: { + if(status().tellp() > 0) + status() << eom; // force end of previous message json_stream_objectt &json_result = - status().json_stream().push_back_stream_object(); + ui_message_handler.get_json_stream().push_back_stream_object(); const goto_trace_stept &step=goto_trace.steps.back(); json_result["property"] = json_stringt(step.pc->source_location.get_property_id()); diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 1e1e8658f02..ec27fb22fb4 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -341,8 +341,10 @@ bool bmc_covert::operator()() case ui_message_handlert::uit::JSON_UI: { + if(status().tellp() > 0) + status() << eom; // force end of previous message json_stream_objectt &json_result = - status().json_stream().push_back_stream_object(); + bmc.ui_message_handler.get_json_stream().push_back_stream_object(); for(const auto &goal_pair : goal_map) { const goalt &goal=goal_pair.second; diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index 9c996afb5b6..99d92c33694 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -273,7 +273,9 @@ void show_class_hierarchy( msg.result() << messaget::eom; break; case ui_message_handlert::uit::JSON_UI: - hierarchy.output(msg.result().json_stream(), children_only); + if(msg.result().tellp() > 0) + msg.result() << messaget::eom; // force end of previous message + hierarchy.output(message_handler.get_json_stream(), children_only); break; case ui_message_handlert::uit::XML_UI: UNIMPLEMENTED; diff --git a/src/util/message.h b/src/util/message.h index 18bb60fda95..09f3e098f7d 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -18,9 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "json.h" #include "source_location.h" -#include "xml.h" -class json_stream_arrayt; +class xmlt; class message_handlert { @@ -36,12 +35,6 @@ class message_handlert // no-op by default } - /// Return the underlying JSON stream - virtual json_stream_arrayt &get_json_stream() - { - UNREACHABLE; - } - virtual void print(unsigned level, const jsont &json) { // no-op by default @@ -246,14 +239,6 @@ class messaget return func(*this); } - /// Returns a reference to the top-level JSON array stream - json_stream_arrayt &json_stream() - { - if(this->tellp() > 0) - *this << eom; // force end of previous message - return message.message_handler->get_json_stream(); - } - private: void assign_from(const mstreamt &other) { diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 48303308e9e..06aaa401a6f 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -61,13 +61,8 @@ ui_message_handlert::ui_message_handlert( case uit::JSON_UI: { - if(!json_stream) - { - json_stream = - std::unique_ptr(new json_stream_arrayt(out)); - } - - INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream = + std::unique_ptr(new json_stream_arrayt(out)); json_stream->push_back().make_object()["program"] = json_stringt(program); } break; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 67670c3a340..1d35e5221dd 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -41,7 +41,7 @@ class ui_message_handlert : public message_handlert virtual void flush(unsigned level) override; - json_stream_arrayt &get_json_stream() override + json_stream_arrayt &get_json_stream() { PRECONDITION(json_stream!=nullptr); return *json_stream; From 0c8b10880f63bc1d709b912f23a60caff4349a0f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 20 Sep 2018 20:48:33 +0100 Subject: [PATCH 4/4] Make ui_message_handlert parameterizable in the underlying message handler --- src/util/ui_message.cpp | 48 ++++++++++++++++++---------- src/util/ui_message.h | 17 +++++----- unit/analyses/ai/ai_simplify_lhs.cpp | 3 +- 3 files changed, 43 insertions(+), 25 deletions(-) diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 06aaa401a6f..2e99eec0dd7 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -19,21 +19,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "cout_message.h" #include "cmdline.h" -ui_message_handlert::ui_message_handlert() - : _ui(uit::PLAIN), - always_flush(false), - time(timestampert::make(timestampert::clockt::NONE)), - out(std::cout), - json_stream(nullptr) -{ -} - ui_message_handlert::ui_message_handlert( + message_handlert *message_handler, uit __ui, const std::string &program, bool always_flush, timestampert::clockt clock_type) - : _ui(__ui), + : message_handler(message_handler), + _ui(__ui), always_flush(always_flush), time(timestampert::make(clock_type)), out(std::cout), @@ -73,6 +66,7 @@ ui_message_handlert::ui_message_handlert( const class cmdlinet &cmdline, const std::string &program) : ui_message_handlert( + nullptr, cmdline.isset("xml-ui") ? uit::XML_UI : cmdline.isset("json-ui") ? uit::JSON_UI : uit::PLAIN, @@ -88,6 +82,12 @@ ui_message_handlert::ui_message_handlert( { } +ui_message_handlert::ui_message_handlert(message_handlert &message_handler) + : ui_message_handlert( + &message_handler, uit::PLAIN, "", false, timestampert::clockt::NONE) +{ +} + ui_message_handlert::~ui_message_handlert() { switch(get_ui()) @@ -129,13 +129,22 @@ void ui_message_handlert::print( { case uit::PLAIN: { - console_message_handlert console_message_handler(always_flush); std::stringstream ss; const std::string timestamp = time->stamp(); ss << timestamp << (timestamp.empty() ? "" : " ") << message; - console_message_handler.print(level, ss.str()); - if(always_flush) - console_message_handler.flush(level); + if(message_handler) + { + message_handler->print(level, ss.str()); + if(always_flush) + message_handler->flush(level); + } + else + { + console_message_handlert msg(always_flush); + msg.print(level, ss.str()); + if(always_flush) + msg.flush(level); + } } break; @@ -298,8 +307,15 @@ void ui_message_handlert::flush(unsigned level) { case uit::PLAIN: { - console_message_handlert console_message_handler(always_flush); - console_message_handler.flush(level); + if(message_handler) + { + message_handler->flush(level); + } + else + { + console_message_handlert msg(always_flush); + msg.flush(level); + } } break; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 1d35e5221dd..8278eaa4937 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -21,16 +21,9 @@ class ui_message_handlert : public message_handlert public: enum class uit { PLAIN, XML_UI, JSON_UI }; - ui_message_handlert( - uit, - const std::string &program, - const bool always_flush, - timestampert::clockt clock_type); - ui_message_handlert(const class cmdlinet &, const std::string &program); - /// Default constructor; implementation is in .cpp file - ui_message_handlert(); + explicit ui_message_handlert(message_handlert &); virtual ~ui_message_handlert(); @@ -48,12 +41,20 @@ class ui_message_handlert : public message_handlert } protected: + message_handlert *message_handler; uit _ui; const bool always_flush; std::unique_ptr time; std::ostream &out; std::unique_ptr json_stream; + ui_message_handlert( + message_handlert *, + uit, + const std::string &program, + const bool always_flush, + timestampert::clockt clock_type); + virtual void print( unsigned level, const std::string &message) override; diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 72da63050ae..115c724aac4 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -10,6 +10,7 @@ /// Unit tests for ai_domain_baset::ai_simplify_lhs #include +#include #include @@ -64,7 +65,7 @@ bool constant_simplification_mockt::ai_simplify( SCENARIO("ai_domain_baset::ai_simplify_lhs", "[core][analyses][ai][ai_simplify_lhs]") { - ui_message_handlert message_handler; + ui_message_handlert message_handler(null_message_handler); ansi_c_languaget language; language.set_message_handler(message_handler);