From d5735d6566e8d186484948d4e66e8e67bf0c06fb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Dec 2023 17:48:21 +0000 Subject: [PATCH] Remove default messaget value from goto_program_dereferencet Use a message_handlert throughout, and firmly require that instead of using a default value (of a deprecated messaget()). --- .../src/janalyzer/janalyzer_parse_options.cpp | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 5 +- jbmc/src/jdiff/jdiff_parse_options.cpp | 6 +- src/analyses/dependence_graph.cpp | 19 ++++-- src/analyses/dependence_graph.h | 11 +++- src/analyses/goto_rw.cpp | 2 +- src/analyses/goto_rw.h | 18 +++--- src/analyses/reaching_definitions.cpp | 15 +++-- src/analyses/reaching_definitions.h | 12 +++- src/cbmc/cbmc_parse_options.cpp | 7 ++- src/goto-analyzer/build_analyzer.cpp | 2 +- src/goto-diff/change_impact.cpp | 36 ++++++----- src/goto-diff/change_impact.h | 4 +- src/goto-diff/goto_diff_parse_options.cpp | 3 +- src/goto-instrument/full_slicer.cpp | 29 +++++---- src/goto-instrument/full_slicer.h | 16 ++--- src/goto-instrument/full_slicer_class.h | 3 +- .../goto_instrument_parse_options.cpp | 22 +++---- src/goto-instrument/interrupt.cpp | 19 +++--- src/goto-instrument/interrupt.h | 4 +- src/goto-instrument/mmio.cpp | 16 ++--- src/goto-instrument/mmio.h | 5 +- src/goto-instrument/race_check.cpp | 21 +++++-- src/goto-instrument/race_check.h | 6 +- src/goto-instrument/rw_set.cpp | 9 ++- src/goto-instrument/rw_set.h | 59 +++++++++++++------ src/goto-instrument/wmm/goto2graph.cpp | 14 ++--- src/goto-instrument/wmm/shared_buffers.cpp | 15 +++-- src/goto-instrument/wmm/weak_memory.cpp | 7 +-- src/goto-symex/precondition.cpp | 20 +++++-- src/goto-symex/precondition.h | 4 +- src/goto-symex/symex_clean_expr.cpp | 7 ++- src/goto-symex/symex_dereference.cpp | 2 +- src/goto-synthesizer/cegis_verifier.cpp | 2 +- .../goto_program_dereference.cpp | 15 ++--- .../goto_program_dereference.h | 20 +++---- .../value_set_dereference.cpp | 4 +- src/pointer-analysis/value_set_dereference.h | 8 +-- unit/analyses/dependence_graph.cpp | 2 +- 39 files changed, 283 insertions(+), 188 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 0b3eee5c96ce..ef5f2b755f93 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -276,7 +276,7 @@ ai_baset *janalyzer_parse_optionst::build_analyzer( } else if(options.get_bool_option("dependence-graph")) { - domain = new dependence_grapht(ns); + domain = new dependence_grapht(ns, ui_message_handler); } else if(options.get_bool_option("intervals")) { diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index bbc225ca5f02..127d2baa290d 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -897,9 +897,10 @@ bool jbmc_parse_optionst::process_goto_functions( << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(cmdline.isset("property")) - property_slicer(goto_model, cmdline.get_values("property")); + property_slicer( + goto_model, cmdline.get_values("property"), ui_message_handler); else - full_slicer(goto_model); + full_slicer(goto_model, ui_message_handler); } // remove any skips introduced diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 512e7320f123..3c2e515dd54a 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -144,7 +144,11 @@ int jdiff_parse_optionst::doit() : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD : impact_modet::BOTH); change_impact( - goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output")); + goto_model1, + goto_model2, + impact_mode, + cmdline.isset("compact-output"), + ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 621dbdfeeb8a..efb7c6ae8fca 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -164,7 +164,7 @@ void dep_graph_domaint::data_dependencies( // TODO use (future) reaching-definitions-dereferencing rw_set value_setst &value_sets= dep_graph.reaching_definitions().get_value_sets(); - rw_range_set_value_sett rw_set(ns, value_sets); + rw_range_set_value_sett rw_set(ns, value_sets, message_handler); goto_rw(function_to, to, rw_set); for(const auto &read_object_entry : rw_set.get_r_set()) @@ -341,7 +341,10 @@ jsont dep_graph_domaint::output_json( class dep_graph_domain_factoryt : public ai_domain_factoryt { public: - explicit dep_graph_domain_factoryt(dependence_grapht &_dg) : dg(_dg) + dep_graph_domain_factoryt( + dependence_grapht &_dg, + message_handlert &message_handler) + : dg(_dg), message_handler(message_handler) { } @@ -349,7 +352,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt { auto node_id = dg.add_node(); dg.nodes[node_id].PC = l; - auto p = std::make_unique(node_id); + auto p = std::make_unique(node_id, message_handler); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); @@ -357,12 +360,16 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt private: dependence_grapht &dg; + message_handlert &message_handler; }; -dependence_grapht::dependence_grapht(const namespacet &_ns) - : ait(std::make_unique(*this)), +dependence_grapht::dependence_grapht( + const namespacet &_ns, + message_handlert &message_handler) + : ait( + std::make_unique(*this, message_handler)), ns(_ns), - rd(ns) + rd(ns, message_handler) { } diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index be2ed63a40b3..c053dc2a699e 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -68,8 +68,11 @@ class dep_graph_domaint:public ai_domain_baset public: typedef grapht::node_indext node_indext; - explicit dep_graph_domaint(node_indext id) - : has_values(false), node_id(id), has_changed(false) + dep_graph_domaint(node_indext id, message_handlert &message_handler) + : has_values(false), + node_id(id), + has_changed(false), + message_handler(message_handler) { } @@ -189,6 +192,8 @@ class dep_graph_domaint:public ai_domain_baset // location has a data dependency on depst data_deps; + message_handlert &message_handler; + friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &); friend const depst & @@ -220,7 +225,7 @@ class dependence_grapht: typedef std::map post_dominators_mapt; - explicit dependence_grapht(const namespacet &_ns); + dependence_grapht(const namespacet &_ns, message_handlert &); void initialize(const goto_functionst &goto_functions) { diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 0f81ecaf6325..cbd36d3ccb60 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -682,7 +682,7 @@ void rw_range_set_value_sett::get_objects_dereference( size); exprt object=deref; - dereference(function, target, object, ns, value_sets); + dereference(function, target, object, ns, value_sets, message_handler); auto type_bits = pointer_offset_bits(object.type(), ns); diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index fdb53deb3140..a6c1bf227fbe 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -21,7 +21,7 @@ Date: April 2010 #include class goto_functionst; - +class message_handlert; class rw_range_sett; void goto_rw( @@ -212,8 +212,8 @@ class rw_range_sett virtual ~rw_range_sett(); - explicit rw_range_sett(const namespacet &_ns): - ns(_ns) + rw_range_sett(const namespacet &_ns, message_handlert &message_handler) + : ns(_ns), message_handler(message_handler) { } @@ -263,6 +263,7 @@ class rw_range_sett protected: const namespacet &ns; + message_handlert &message_handler; objectst r_range_set, w_range_set; @@ -370,9 +371,9 @@ class rw_range_set_value_sett:public rw_range_sett public: rw_range_set_value_sett( const namespacet &_ns, - value_setst &_value_sets): - rw_range_sett(_ns), - value_sets(_value_sets) + value_setst &_value_sets, + message_handlert &message_handler) + : rw_range_sett(_ns, message_handler), value_sets(_value_sets) { } @@ -463,8 +464,9 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett rw_guarded_range_set_value_sett( const namespacet &_ns, value_setst &_value_sets, - guard_managert &guard_manager) - : rw_range_set_value_sett(_ns, _value_sets), + guard_managert &guard_manager, + message_handlert &message_handler) + : rw_range_set_value_sett(_ns, _value_sets, message_handler), guard_manager(guard_manager), guard(true_exprt(), guard_manager) { diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 5dc71d4aab42..f44562ed90f0 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -32,27 +32,30 @@ class rd_range_domain_factoryt : public ai_domain_factoryt { public: rd_range_domain_factoryt( - sparse_bitvector_analysist *_bv_container) - : bv_container(_bv_container) + sparse_bitvector_analysist *_bv_container, + message_handlert &message_handler) + : bv_container(_bv_container), message_handler(message_handler) { PRECONDITION(bv_container != nullptr); } std::unique_ptr make(locationt) const override { - auto p = std::make_unique(bv_container); + auto p = std::make_unique(bv_container, message_handler); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); } private: sparse_bitvector_analysist *const bv_container; + message_handlert &message_handler; }; reaching_definitions_analysist::reaching_definitions_analysist( - const namespacet &_ns) + const namespacet &_ns, + message_handlert &message_handler) : concurrency_aware_ait( - std::make_unique(this)), + std::make_unique(this, message_handler)), ns(_ns) { } @@ -306,7 +309,7 @@ void rd_range_domaint::transform_assign( locationt to, reaching_definitions_analysist &rd) { - rw_range_set_value_sett rw_set(ns, rd.get_value_sets()); + rw_range_set_value_sett rw_set(ns, rd.get_value_sets(), message_handler); goto_rw(function_to, to, rw_set); const bool is_must_alias=rw_set.get_w_set().size()==1; diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 0421a0f4fca3..fb8e0a78374a 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -159,8 +159,12 @@ class rd_range_domaint:public ai_domain_baset { public: rd_range_domaint( - sparse_bitvector_analysist *_bv_container) - : ai_domain_baset(), has_values(false), bv_container(_bv_container) + sparse_bitvector_analysist *_bv_container, + message_handlert &message_handler) + : ai_domain_baset(), + has_values(false), + bv_container(_bv_container), + message_handler(message_handler) { PRECONDITION(bv_container != nullptr); } @@ -346,6 +350,8 @@ class rd_range_domaint:public ai_domain_baset bool merge_inner( values_innert &dest, const values_innert &other); + + message_handlert &message_handler; }; class reaching_definitions_analysist: @@ -354,7 +360,7 @@ class reaching_definitions_analysist: { public: // constructor - explicit reaching_definitions_analysist(const namespacet &_ns); + reaching_definitions_analysist(const namespacet &_ns, message_handlert &); virtual ~reaching_definitions_analysist(); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e8579a519eb2..a89d0ddd885f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -906,9 +906,12 @@ bool cbmc_parse_optionst::process_goto_program( << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(options.is_set("property")) - property_slicer(goto_model, options.get_list_option("property")); + property_slicer( + goto_model, + options.get_list_option("property"), + log.get_message_handler()); else - full_slicer(goto_model); + full_slicer(goto_model, log.get_message_handler()); } // remove any skips introduced since coverage instrumentation diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index 1b110e78dba7..ac8dd2244620 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -123,7 +123,7 @@ std::unique_ptr build_analyzer( } else if(options.get_bool_option("dependence-graph")) { - return std::make_unique(ns); + return std::make_unique(ns, mh); } else if(options.get_bool_option("dependence-graph-vs")) { diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index 2ef7f3d7240f..1a0d7c1ffb24 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -207,7 +207,8 @@ class change_impactt const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, - bool compact_output); + bool compact_output, + message_handlert &message_handler); void operator()(); @@ -289,19 +290,20 @@ class change_impactt }; change_impactt::change_impactt( - const goto_modelt &model_old, - const goto_modelt &model_new, - impact_modet _impact_mode, - bool _compact_output): - impact_mode(_impact_mode), - compact_output(_compact_output), - old_goto_functions(model_old.goto_functions), - ns_old(model_old.symbol_table), - new_goto_functions(model_new.goto_functions), - ns_new(model_new.symbol_table), - unified_diff(model_old, model_new), - old_dep_graph(ns_old), - new_dep_graph(ns_new) + const goto_modelt &model_old, + const goto_modelt &model_new, + impact_modet _impact_mode, + bool _compact_output, + message_handlert &message_handler) + : impact_mode(_impact_mode), + compact_output(_compact_output), + old_goto_functions(model_old.goto_functions), + ns_old(model_old.symbol_table), + new_goto_functions(model_new.goto_functions), + ns_new(model_new.symbol_table), + unified_diff(model_old, model_new), + old_dep_graph(ns_old, message_handler), + new_dep_graph(ns_new, message_handler) { // syntactic difference? if(!unified_diff()) @@ -757,8 +759,10 @@ void change_impact( const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, - bool compact_output) + bool compact_output, + message_handlert &message_handler) { - change_impactt c(model_old, model_new, impact_mode, compact_output); + change_impactt c( + model_old, model_new, impact_mode, compact_output, message_handler); c(); } diff --git a/src/goto-diff/change_impact.h b/src/goto-diff/change_impact.h index d56e57184e14..bb26edafe45a 100644 --- a/src/goto-diff/change_impact.h +++ b/src/goto-diff/change_impact.h @@ -15,12 +15,14 @@ Date: April 2016 #define CPROVER_GOTO_DIFF_CHANGE_IMPACT_H class goto_modelt; +class message_handlert; enum class impact_modet { FORWARD, BACKWARD, BOTH }; void change_impact( const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, - bool compact_output); + bool compact_output, + message_handlert &message_handler); #endif // CPROVER_GOTO_DIFF_CHANGE_IMPACT_H diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index b30a71df7d37..39f37c784f80 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -147,7 +147,8 @@ int goto_diff_parse_optionst::doit() goto_model1, goto_model2, impact_mode, - cmdline.isset("compact-output")); + cmdline.isset("compact-output"), + ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 9516bdaf0604..f8b8c8a64140 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -254,7 +254,8 @@ static bool implicit(goto_programt::const_targett target) void full_slicert::operator()( goto_functionst &goto_functions, const namespacet &ns, - const slicing_criteriont &criterion) + const slicing_criteriont &criterion, + message_handlert &message_handler) { // build the CFG data structure cfg(goto_functions); @@ -296,7 +297,7 @@ void full_slicert::operator()( } // compute program dependence graph (and post-dominators) - dependence_grapht dep_graph(ns); + dependence_grapht dep_graph(ns, message_handler); dep_graph(goto_functions, ns); // compute the fixedpoint @@ -347,41 +348,45 @@ void full_slicert::operator()( void full_slicer( goto_functionst &goto_functions, const namespacet &ns, - const slicing_criteriont &criterion) + const slicing_criteriont &criterion, + message_handlert &message_handler) { - full_slicert()(goto_functions, ns, criterion); + full_slicert()(goto_functions, ns, criterion, message_handler); } void full_slicer( goto_functionst &goto_functions, - const namespacet &ns) + const namespacet &ns, + message_handlert &message_handler) { assert_criteriont a; - full_slicert()(goto_functions, ns, a); + full_slicert()(goto_functions, ns, a, message_handler); } -void full_slicer(goto_modelt &goto_model) +void full_slicer(goto_modelt &goto_model, message_handlert &message_handler) { assert_criteriont a; const namespacet ns(goto_model.symbol_table); - full_slicert()(goto_model.goto_functions, ns, a); + full_slicert()(goto_model.goto_functions, ns, a, message_handler); } void property_slicer( goto_functionst &goto_functions, const namespacet &ns, - const std::list &properties) + const std::list &properties, + message_handlert &message_handler) { properties_criteriont p(properties); - full_slicert()(goto_functions, ns, p); + full_slicert()(goto_functions, ns, p, message_handler); } void property_slicer( goto_modelt &goto_model, - const std::list &properties) + const std::list &properties, + message_handlert &message_handler) { const namespacet ns(goto_model.symbol_table); - property_slicer(goto_model.goto_functions, ns, properties); + property_slicer(goto_model.goto_functions, ns, properties, message_handler); } slicing_criteriont::~slicing_criteriont() diff --git a/src/goto-instrument/full_slicer.h b/src/goto-instrument/full_slicer.h index 630d7ec8243b..e18f37f1103a 100644 --- a/src/goto-instrument/full_slicer.h +++ b/src/goto-instrument/full_slicer.h @@ -16,21 +16,22 @@ Author: Daniel Kroening, kroening@kroening.com class goto_functionst; class goto_modelt; +class message_handlert; -void full_slicer( - goto_functionst &, - const namespacet &); +void full_slicer(goto_functionst &, const namespacet &, message_handlert &); -void full_slicer(goto_modelt &); +void full_slicer(goto_modelt &, message_handlert &); void property_slicer( goto_functionst &, const namespacet &, - const std::list &properties); + const std::list &properties, + message_handlert &); void property_slicer( goto_modelt &, - const std::list &properties); + const std::list &properties, + message_handlert &); class slicing_criteriont { @@ -44,6 +45,7 @@ class slicing_criteriont void full_slicer( goto_functionst &goto_functions, const namespacet &ns, - const slicing_criteriont &criterion); + const slicing_criteriont &criterion, + message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index c4abd515610d..4ad06772ce61 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -41,7 +41,8 @@ class full_slicert void operator()( goto_functionst &goto_functions, const namespacet &ns, - const slicing_criteriont &criterion); + const slicing_criteriont &criterion, + message_handlert &message_handler); protected: struct cfg_nodet diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 55721374ce63..81dacb0d4383 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -550,8 +550,8 @@ int goto_instrument_parse_optionst::doit() const symbolt &symbol=ns.lookup(ID_main); symbol_exprt main(symbol.name, symbol.type); - std::cout << - rw_set_functiont(value_set_analysis, goto_model, main); + std::cout << rw_set_functiont( + value_set_analysis, goto_model, main, ui_message_handler); return CPROVER_EXIT_SUCCESS; } @@ -567,7 +567,7 @@ int goto_instrument_parse_optionst::doit() rewrite_rw_ok(goto_model); const namespacet ns(goto_model.symbol_table); - reaching_definitions_analysist rd_analysis(ns); + reaching_definitions_analysist rd_analysis(ns, ui_message_handler); rd_analysis(goto_model); rd_analysis.output(goto_model, std::cout); @@ -580,7 +580,7 @@ int goto_instrument_parse_optionst::doit() rewrite_rw_ok(goto_model); const namespacet ns(goto_model.symbol_table); - dependence_grapht dependence_graph(ns); + dependence_grapht dependence_graph(ns, ui_message_handler); dependence_graph(goto_model); dependence_graph.output(goto_model, std::cout); dependence_graph.output_dot(std::cout); @@ -1524,13 +1524,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() { // removing pointers log.status() << "Removing Pointers" << messaget::eom; - remove_pointers(goto_model, value_set_analysis); + remove_pointers(goto_model, value_set_analysis, ui_message_handler); } if(cmdline.isset("race-check")) { log.status() << "Adding Race Checks" << messaget::eom; - race_check(value_set_analysis, goto_model); + race_check(value_set_analysis, goto_model, ui_message_handler); } if(cmdline.isset("mm")) @@ -1627,14 +1627,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() interrupt( value_set_analysis, goto_model, - cmdline.get_value("isr")); + cmdline.get_value("isr"), + ui_message_handler); } // Memory-mapped I/O if(cmdline.isset("mmio")) { log.status() << "Instrumenting memory-mapped I/O" << messaget::eom; - mmio(value_set_analysis, goto_model); + mmio(value_set_analysis, goto_model, ui_message_handler); } if(cmdline.isset("concurrency")) @@ -1759,12 +1760,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() << messaget::eom; log.status() << "Performing a full slice" << messaget::eom; if(cmdline.isset("property")) - property_slicer(goto_model, cmdline.get_values("property")); + property_slicer( + goto_model, cmdline.get_values("property"), ui_message_handler); else { // full_slicer requires that the model has unique location numbers: goto_model.goto_functions.update(); - full_slicer(goto_model); + full_slicer(goto_model, ui_message_handler); } } diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index acd6a01211cc..4f082d05ac74 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -64,7 +64,8 @@ static void interrupt( #endif goto_programt &goto_program, const symbol_exprt &interrupt_handler, - const rw_set_baset &isr_rw_set) + const rw_set_baset &isr_rw_set, + message_handlert &message_handler) { namespacet ns(symbol_table); @@ -79,12 +80,11 @@ static void interrupt( ns, value_sets, function_id, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + message_handler); // NOLINT(whitespace/parens) // potential race? bool race_on_read=potential_race_on_read(rw_set, isr_rw_set); @@ -188,15 +188,15 @@ get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler) void interrupt( value_setst &value_sets, goto_modelt &goto_model, - const irep_idt &interrupt_handler) + const irep_idt &interrupt_handler, + message_handlert &message_handler) { // look up the ISR symbol_exprt isr= get_isr(goto_model.symbol_table, interrupt_handler); // we first figure out which objects are read/written by the ISR - rw_set_functiont isr_rw_set( - value_sets, goto_model, isr); + rw_set_functiont isr_rw_set(value_sets, goto_model, isr, message_handler); // now instrument @@ -216,7 +216,8 @@ void interrupt( #endif gf_entry.second.body, isr, - isr_rw_set); + isr_rw_set, + message_handler); } } diff --git a/src/goto-instrument/interrupt.h b/src/goto-instrument/interrupt.h index 082b4e0b4f5b..9d2446a60b0d 100644 --- a/src/goto-instrument/interrupt.h +++ b/src/goto-instrument/interrupt.h @@ -17,11 +17,13 @@ Date: September 2011 #include class goto_modelt; +class message_handlert; class value_setst; void interrupt( value_setst &, goto_modelt &, - const irep_idt &interrupt_handler); + const irep_idt &interrupt_handler, + message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_INTERRUPT_H diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index a067c79f4bb1..65ecad0c63b3 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -28,7 +28,8 @@ static void mmio( #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif - goto_programt &goto_program) + goto_programt &goto_program, + message_handlert &message_handler) { namespacet ns(symbol_table); @@ -46,12 +47,11 @@ static void mmio( ns, value_sets, function_id, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + message_handler); // NOLINT(whitespace/parens) if(rw_set.empty()) continue; @@ -158,7 +158,8 @@ static void mmio( void mmio( value_setst &value_sets, - goto_modelt &goto_model) + goto_modelt &goto_model, + message_handlert &message_handler) { // now instrument @@ -175,7 +176,8 @@ void mmio( #ifdef LOCAL_MAY gf_entry.second, #endif - gf_entry.second.body); + gf_entry.second.body, + message_handler); } } diff --git a/src/goto-instrument/mmio.h b/src/goto-instrument/mmio.h index f2fbec84fa13..1e671b4a42bb 100644 --- a/src/goto-instrument/mmio.h +++ b/src/goto-instrument/mmio.h @@ -14,11 +14,10 @@ Date: September 2011 #ifndef CPROVER_GOTO_INSTRUMENT_MMIO_H #define CPROVER_GOTO_INSTRUMENT_MMIO_H +class message_handlert; class value_setst; class goto_modelt; -void mmio( - value_setst &, - goto_modelt &); +void mmio(value_setst &, goto_modelt &, message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_MMIO_H diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 85bc08ff0f11..7dccfe38fed9 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -164,7 +164,8 @@ static void race_check( const irep_idt &function_id, L_M_ARG(const goto_functionst::goto_functiont &goto_function) goto_programt &goto_program, - w_guardst &w_guards) + w_guardst &w_guards, + message_handlert &message_handler) // clang-format on { namespacet ns(symbol_table); @@ -180,7 +181,11 @@ static void race_check( if(instruction.is_assign()) { rw_set_loct rw_set( - ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may)); + ns, + value_sets, + function_id, + i_it L_M_LAST_ARG(local_may), + message_handler); if(!has_shared_entries(ns, rw_set)) continue; @@ -269,7 +274,8 @@ void race_check( #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif - goto_programt &goto_program) + goto_programt &goto_program, + message_handlert &message_handler) { w_guardst w_guards(symbol_table); @@ -278,7 +284,8 @@ void race_check( symbol_table, function_id, L_M_ARG(goto_function) goto_program, - w_guards); + w_guards, + message_handler); w_guards.add_initialization(goto_program); goto_program.update(); @@ -286,7 +293,8 @@ void race_check( void race_check( value_setst &value_sets, - goto_modelt &goto_model) + goto_modelt &goto_model, + message_handlert &message_handler) { w_guardst w_guards(goto_model.symbol_table); @@ -301,7 +309,8 @@ void race_check( goto_model.symbol_table, gf_entry.first, L_M_ARG(gf_entry.second) gf_entry.second.body, - w_guards); + w_guards, + message_handler); } } diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index 98e9bfd52d93..e4d6daa34439 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -22,6 +22,7 @@ Date: February 2006 class goto_modelt; class goto_programt; +class message_handlert; class value_setst; void race_check( @@ -31,8 +32,9 @@ void race_check( #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif - goto_programt &goto_program); + goto_programt &goto_program, + message_handlert &); -void race_check(value_setst &, goto_modelt &); +void race_check(value_setst &, goto_modelt &, message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index ca98c2ef60af..b1c03a6c273b 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -155,7 +155,7 @@ void _rw_set_loct::read_write_rec( read_write_rec(*it, r, w, suffix, guard_conjuncts); } #else - dereference(function_id, target, tmp, ns, value_sets); + dereference(function_id, target, tmp, ns, value_sets, message_handler); read_write_rec(tmp, r, w, suffix, guard_conjuncts); #endif @@ -219,12 +219,11 @@ void rw_set_functiont::compute_rec(const exprt &function) ns, value_sets, function_id, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + message_handler); // NOLINT(whitespace/parens) } } } diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index aea642266979..3eefa66b5541 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -26,6 +26,7 @@ Date: February 2006 #include #endif +class message_handlert; class value_setst; // a container for read/write sets @@ -33,8 +34,8 @@ class value_setst; class rw_set_baset { public: - explicit rw_set_baset(const namespacet &_ns) - :ns(_ns) + rw_set_baset(const namespacet &_ns, message_handlert &message_handler) + : ns(_ns), message_handler(message_handler) { } @@ -97,6 +98,7 @@ class rw_set_baset virtual void reset_track_deref() {} const namespacet &ns; + message_handlert &message_handler; }; inline std::ostream &operator<<( @@ -117,8 +119,9 @@ class _rw_set_loct:public rw_set_baset value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may) - : rw_set_baset(_ns), + local_may_aliast &may, + message_handlert &message_handler) + : rw_set_baset(_ns, message_handler), value_sets(_value_sets), function_id(_function_id), target(_target), @@ -128,8 +131,9 @@ class _rw_set_loct:public rw_set_baset const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, - goto_programt::const_targett _target) - : rw_set_baset(_ns), + goto_programt::const_targett _target, + message_handlert &message_handler) + : rw_set_baset(_ns, message_handler), value_sets(_value_sets), function_id(_function_id), target(_target) @@ -182,15 +186,23 @@ class rw_set_loct:public _rw_set_loct value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may) - : _rw_set_loct(_ns, _value_sets, _function_id, _target, may) + local_may_aliast &may, + message_handlert &message_handler) + : _rw_set_loct( + _ns, + _value_sets, + _function_id, + _target, + may, + message_handler) #else rw_set_loct( const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, - goto_programt::const_targett _target) - : _rw_set_loct(_ns, _value_sets, _function_id, _target) + goto_programt::const_targett _target, + message_handlert &message_handler) + : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler) #endif { compute(); @@ -205,11 +217,12 @@ class rw_set_functiont:public rw_set_baset rw_set_functiont( value_setst &_value_sets, const goto_modelt &_goto_model, - const exprt &function): - rw_set_baset(ns), - ns(_goto_model.symbol_table), - value_sets(_value_sets), - goto_functions(_goto_model.goto_functions) + const exprt &function, + message_handlert &message_handler) + : rw_set_baset(ns, message_handler), + ns(_goto_model.symbol_table), + value_sets(_value_sets), + goto_functions(_goto_model.goto_functions) { compute_rec(function); } @@ -243,16 +256,24 @@ class rw_set_with_trackt:public _rw_set_loct value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may) - : _rw_set_loct(_ns, _value_sets, _function_id, _target, may), + local_may_aliast &may, + message_handlert &message_handler) + : _rw_set_loct( + _ns, + _value_sets, + _function_id, + _target, + may, + message_handler), dereferencing(false) #else rw_set_with_trackt( const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, - goto_programt::const_targett _target) - : _rw_set_loct(_ns, _value_sets, _function_id, _target), + goto_programt::const_targett _target, + message_handlert &message_handler) + : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler), dereferencing(false) #endif { diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 3850c969da6f..fc33f29f75b6 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -428,12 +428,11 @@ bool instrumentert::cfg_visitort::contains_shared_array( ns, value_sets, function_id, - cur + cur, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + instrumenter.message.get_message_handler()); // NOLINT(whitespace/parens) instrumenter.message.debug() << "Writes: "<::max(); event_idt previous_gnode=std::numeric_limits::max(); diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 05e279cbfe47..4d73b57efd26 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -1023,12 +1023,11 @@ void shared_bufferst::affected_by_delay( ns, value_sets, gf_entry.first, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + message.get_message_handler()); // NOLINT(whitespace/parens) for(const auto &w_entry : rw_set.w_entries) { for(const auto &r_entry : rw_set.r_entries) @@ -1090,12 +1089,12 @@ void shared_bufferst::cfg_visitort::weak_memory( ns, value_sets, function_id, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + shared_buffers.message + .get_message_handler()); // NOLINT(whitespace/parens) if(rw_set.empty()) continue; diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 0e4946b5337d..bf4b85c69fe8 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -65,12 +65,11 @@ void introduce_temporaries( ns, value_sets, function_id, - i_it + i_it, #ifdef LOCAL_MAY - , - local_may + local_may, #endif - ); // NOLINT(whitespace/parens) + message.get_message_handler()); // NOLINT(whitespace/parens) if(rw_set.empty()) continue; diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index afe0677f9891..76fc7f48a834 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -27,12 +27,14 @@ class preconditiont value_setst &_value_sets, const goto_programt::const_targett _target, const SSA_stept &_SSA_step, - const goto_symex_statet &_s) + const goto_symex_statet &_s, + message_handlert &message_handler) : ns(_ns), value_sets(_value_sets), target(_target), SSA_step(_SSA_step), - s(_s) + s(_s), + message_handler(message_handler) { } @@ -42,6 +44,7 @@ class preconditiont const goto_programt::const_targett target; const SSA_stept &SSA_step; const goto_symex_statet &s; + message_handlert &message_handler; void compute_rec(exprt &dest); public: @@ -57,14 +60,15 @@ void precondition( const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, - exprt &dest) + exprt &dest, + message_handlert &message_handler) { for(symex_target_equationt::SSA_stepst::const_reverse_iterator it=equation.SSA_steps.rbegin(); it!=equation.SSA_steps.rend(); it++) { - preconditiont precondition(ns, value_sets, target, *it, s); + preconditiont precondition(ns, value_sets, target, *it, s, message_handler); precondition.compute(dest); if(dest.is_false()) return; @@ -128,7 +132,13 @@ void preconditiont::compute_rec(exprt &dest) { exprt tmp; tmp.swap(deref_expr.pointer()); - dereference(SSA_step.source.function_id, target, tmp, ns, value_sets); + dereference( + SSA_step.source.function_id, + target, + tmp, + ns, + value_sets, + message_handler); deref_expr.swap(tmp); compute_rec(deref_expr); } diff --git a/src/goto-symex/precondition.h b/src/goto-symex/precondition.h index aef6d5cf5bac..11501147c4e2 100644 --- a/src/goto-symex/precondition.h +++ b/src/goto-symex/precondition.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto-programs/goto_program.h" class exprt; +class message_handlert; class namespacet; class symex_target_equationt; class value_setst; @@ -25,6 +26,7 @@ void precondition( const goto_programt::const_targett target, const symex_target_equationt &equation, const class goto_symex_statet &s, - exprt &dest); + exprt &dest, + message_handlert &message_handler); #endif // CPROVER_GOTO_SYMEX_PRECONDITION_H diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 7806a7202695..5c1ff7134a92 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -131,7 +131,12 @@ void goto_symext::process_array_expr(statet &state, exprt &expr) symex_dereference_statet symex_dereference_state(state, ns); value_set_dereferencet dereference( - ns, state.symbol_table, symex_dereference_state, language_mode, false, log); + ns, + state.symbol_table, + symex_dereference_state, + language_mode, + false, + log.get_message_handler()); expr = dereference.dereference(expr, symex_config.show_points_to_sets); lift_lets(state, expr); diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 51d64fb3e240..f4beccfb669f 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -329,7 +329,7 @@ void goto_symext::dereference_rec( symex_dereference_state, language_mode, expr_is_not_null, - log); + log.get_message_handler()); // std::cout << "**** " << format(tmp1) << '\n'; exprt tmp2 = diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 176343c61526..2f1d15c5bf3d 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -178,7 +178,7 @@ std::list cegis_verifiert::get_cause_loop_id( std::list result; // build the dependence graph - dependence_grapht dependence_graph(ns); + dependence_grapht dependence_graph(ns, log.get_message_handler()); dependence_graph(goto_model); // Checking if `to` is dependent on `from`. diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 672f749c576a..efa02a890462 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -259,15 +259,15 @@ void goto_program_dereferencet::dereference_expression( /// may be pointing to. void remove_pointers( goto_modelt &goto_model, - value_setst &value_sets) + value_setst &value_sets, + message_handlert &message_handler) { namespacet ns(goto_model.symbol_table); optionst options; - goto_program_dereferencet - goto_program_dereference( - ns, goto_model.symbol_table, options, value_sets); + goto_program_dereferencet goto_program_dereference( + ns, goto_model.symbol_table, options, value_sets, message_handler); for(auto &gf_entry : goto_model.goto_functions.function_map) goto_program_dereference.dereference_program(gf_entry.second.body); @@ -280,11 +280,12 @@ void dereference( goto_programt::const_targett target, exprt &expr, const namespacet &ns, - value_setst &value_sets) + value_setst &value_sets, + message_handlert &message_handler) { optionst options; symbol_tablet new_symbol_table; - goto_program_dereferencet - goto_program_dereference(ns, new_symbol_table, options, value_sets); + goto_program_dereferencet goto_program_dereference( + ns, new_symbol_table, options, value_sets, message_handler); goto_program_dereference.dereference_expression(function_id, target, expr); } diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index a77e8483e1f7..1818323d0de2 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H -#include - #include "dereference_callback.h" #include "value_set_dereference.h" @@ -35,24 +33,23 @@ class goto_program_dereferencet:protected dereference_callbackt // for the final argument to value_set_dereferencet. // This means that language-inappropriate values such as // (struct A*)some_integer_value in Java, may be returned. - // Note: value_set_dereferencet requires a messaget instance - // as on of its arguments to display the points-to set + // Note: value_set_dereferencet requires a message_handlert instance + // as one of its arguments to display the points-to set // during symex. Display is not done during goto-program // conversion. To ensure this the display_points_to_sets // parameter in value_set_dereferencet::dereference() // is set to false by default and is not changed by the - // goto program conversion modules. Similarly, here we set - // _log to be a default messaget instance. + // goto program conversion modules. goto_program_dereferencet( const namespacet &_ns, symbol_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, - const messaget &_log = messaget()) + message_handlert &message_handler) : options(_options), ns(_ns), value_sets(_value_sets), - dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log) + dereference(_ns, _new_symbol_table, *this, ID_nil, false, message_handler) { } @@ -101,11 +98,10 @@ void dereference( goto_programt::const_targett target, exprt &expr, const namespacet &, - value_setst &); + value_setst &, + message_handlert &); -void remove_pointers( - goto_modelt &, - value_setst &); +void remove_pointers(goto_modelt &, value_setst &, message_handlert &); #define OPT_REMOVE_POINTERS "(remove-pointers)" diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 924480fbe254..d132d32f3e50 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -282,8 +282,10 @@ exprt value_set_dereferencet::handle_dereference_base_case( if(display_points_to_sets) { + messaget log{message_handler}; log.status() << value_set_dereference_stats_to_json( - pointer, points_to_set, retained_values, result_value); + pointer, points_to_set, retained_values, result_value) + << messaget::eom; } return result_value; diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index d33abf35f04c..ed7a0fca61c6 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class dereference_callbackt; -class messaget; +class message_handlert; class symbol_table_baset; /// Wrapper for a function dereferencing pointer expressions using a value set. @@ -37,13 +37,13 @@ class value_set_dereferencet final dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, - const messaget &_log) + message_handlert &_message_handler) : ns(_ns), new_symbol_table(_new_symbol_table), dereference_callback(_dereference_callback), language_mode(_language_mode), exclude_null_derefs(_exclude_null_derefs), - log(_log) + message_handler(_message_handler) { } virtual ~value_set_dereferencet() { } @@ -105,7 +105,7 @@ class value_set_dereferencet final /// Flag indicating whether `value_set_dereferencet::dereference` should /// disregard an apparent attempt to dereference NULL const bool exclude_null_derefs; - const messaget &log; + message_handlert &message_handler; valuet get_failure_value(const exprt &pointer, const typet &type); exprt handle_dereference_base_case( const exprt &pointer, diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index ab67479d312c..ddcd12af2e70 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -87,7 +87,7 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]") WHEN("Constructing a dependence graph") { - dependence_grapht dep_graph(ns); + dependence_grapht dep_graph(ns, null_message_handler); dep_graph(goto_model.goto_functions, ns); THEN("The function call and assignment instructions "