From e5df37104c5ab1ccc06c35567626432b0412d002 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 May 2025 11:18:48 +0000 Subject: [PATCH] unwindsett: goto_model is only needed for options processing An `unwindsett` does not need an `abstract_goto_modelt` as part of its state. --- src/goto-checker/bmc_util.cpp | 5 ----- src/goto-checker/bmc_util.h | 6 +----- src/goto-checker/multi_path_symex_only_checker.cpp | 6 ++++-- .../single_loop_incremental_symex_checker.cpp | 6 ++++-- src/goto-checker/single_path_symex_only_checker.cpp | 8 +++++--- src/goto-checker/symex_bmc.h | 2 +- src/goto-instrument/contracts/contracts.cpp | 5 +++-- .../contracts/dynamic-frames/dfcc_instrument.cpp | 4 ++-- .../contracts/dynamic-frames/dfcc_library.cpp | 4 ++-- src/goto-instrument/goto_instrument_parse_options.cpp | 7 +++++-- src/goto-instrument/unwindset.cpp | 7 +++++-- src/goto-instrument/unwindset.h | 9 ++++----- unit/path_strategies.cpp | 9 ++++++--- 13 files changed, 42 insertions(+), 36 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 6e31d312d77..beb9f9880dd 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -178,7 +178,6 @@ get_memory_model(const optionst &options, const namespacet &ns) void setup_symex( symex_bmct &symex, const namespacet &ns, - const optionst &options, ui_message_handlert &ui_message_handler) { messaget msg(ui_message_handler); @@ -189,10 +188,6 @@ void setup_symex( msg.status() << "Starting Bounded Model Checking" << messaget::eom; symex.last_source_location.make_nil(); - - symex.unwindset.parse_unwind(options.get_option("unwind")); - symex.unwindset.parse_unwindset( - options.get_list_option("unwindset"), ui_message_handler); } void slice( diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 92e0e3a82de..0cdb1f48043 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -68,11 +68,7 @@ void output_graphml( std::unique_ptr get_memory_model(const optionst &options, const namespacet &); -void setup_symex( - symex_bmct &, - const namespacet &, - const optionst &, - ui_message_handlert &); +void setup_symex(symex_bmct &, const namespacet &, ui_message_handlert &); void slice( symex_bmct &, diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index ed094eb53e5..96dd05595cf 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -27,7 +27,6 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( goto_model(goto_model), ns(goto_model.get_symbol_table(), symex_symbol_table), equation(ui_message_handler), - unwindset(goto_model), symex( ui_message_handler, goto_model.get_symbol_table(), @@ -37,7 +36,10 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( guard_manager, unwindset) { - setup_symex(symex, ns, options, ui_message_handler); + unwindset.parse_unwind(options.get_option("unwind")); + unwindset.parse_unwindset( + options.get_list_option("unwindset"), goto_model, ui_message_handler); + setup_symex(symex, ns, ui_message_handler); } incremental_goto_checkert::resultt multi_path_symex_only_checkert:: diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index 47a2194d55d..612dba43d9f 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -28,7 +28,6 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( goto_model(goto_model), ns(goto_model.get_symbol_table(), symex_symbol_table), equation(ui_message_handler), - unwindset(goto_model), symex( ui_message_handler, goto_model.get_symbol_table(), @@ -40,7 +39,10 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( ui_message_handler.get_ui()), property_decider(options, ui_message_handler, equation, ns) { - setup_symex(symex, ns, options, ui_message_handler); + unwindset.parse_unwind(options.get_option("unwind")); + unwindset.parse_unwindset( + options.get_list_option("unwindset"), goto_model, ui_message_handler); + setup_symex(symex, ns, ui_message_handler); // Freeze all symbols if we are using a prop_conv_solvert prop_conv_solvert *prop_conv_solver = dynamic_cast( diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp index 3f8ad17627a..8648ffc4d1d 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -29,9 +29,11 @@ single_path_symex_only_checkert::single_path_symex_only_checkert( goto_model(goto_model), ns(goto_model.get_symbol_table(), symex_symbol_table), worklist(get_path_strategy(options.get_option("exploration-strategy"))), - symex_runtime(0), - unwindset(goto_model) + symex_runtime(0) { + unwindset.parse_unwind(options.get_option("unwind")); + unwindset.parse_unwindset( + options.get_list_option("unwindset"), goto_model, ui_message_handler); } incremental_goto_checkert::resultt single_path_symex_only_checkert:: @@ -152,7 +154,7 @@ void single_path_symex_only_checkert::equation_output( void single_path_symex_only_checkert::setup_symex(symex_bmct &symex) { - ::setup_symex(symex, ns, options, ui_message_handler); + ::setup_symex(symex, ns, ui_message_handler); } void single_path_symex_only_checkert::update_properties( diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h index 8f484482cf4..81d15eed13f 100644 --- a/src/goto-checker/symex_bmc.h +++ b/src/goto-checker/symex_bmc.h @@ -81,9 +81,9 @@ class symex_bmct : public goto_symext const bool record_coverage; +protected: unwindsett &unwindset; -protected: /// Callbacks that may provide an unwind/do-not-unwind decision for a loop std::vector loop_unwind_handlers; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index f99d87e4477..9a3de7e7a23 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1493,8 +1493,9 @@ void code_contractst::apply_loop_contracts( // unwind all transformed loops twice. if(loop_contract_config.unwind_transformed_loops) { - unwindsett unwindset{goto_model}; - unwindset.parse_unwindset(loop_names, log.get_message_handler()); + unwindsett unwindset; + unwindset.parse_unwindset( + loop_names, goto_model, log.get_message_handler()); goto_unwindt goto_unwind; goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 4b7302cd2c2..4f05c385ae1 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -1208,8 +1208,8 @@ void dfcc_instrumentt::apply_loop_contracts( // If required, unwind all transformed loops to yield base and step cases if(loop_contract_config.unwind_transformed_loops) { - unwindsett unwindset{goto_model}; - unwindset.parse_unwindset(to_unwind, log.get_message_handler()); + unwindsett unwindset; + unwindset.parse_unwindset(to_unwind, goto_model, log.get_message_handler()); goto_unwindt goto_unwind; goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index f9a5f51c2fe..5799e4605ef 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -439,7 +439,6 @@ void dfcc_libraryt::specialize(const std::size_t contract_assigns_size) "dfcc_libraryt::specialize_functions can only be called once"); specialized = true; - unwindsett unwindset{goto_model}; std::list loop_names; for(const auto &entry : to_unwind) @@ -452,7 +451,8 @@ void dfcc_libraryt::specialize(const std::size_t contract_assigns_size) const auto &str = stream.str(); loop_names.push_back(str); } - unwindset.parse_unwindset(loop_names, message_handler); + unwindsett unwindset; + unwindset.parse_unwindset(loop_names, goto_model, message_handler); goto_unwindt goto_unwind; goto_unwind( goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSERT_ASSUME); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3b60d0fe95d..e3f108d227b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -183,7 +183,7 @@ int goto_instrument_parse_optionst::doit() if(unwind_given || unwindset_given || unwindset_file_given) { - unwindsett unwindset{goto_model}; + unwindsett unwindset; if(unwind_given) unwindset.parse_unwind(cmdline.get_value("unwind")); @@ -191,13 +191,16 @@ int goto_instrument_parse_optionst::doit() if(unwindset_file_given) { unwindset.parse_unwindset_file( - cmdline.get_value("unwindset-file"), ui_message_handler); + cmdline.get_value("unwindset-file"), + goto_model, + ui_message_handler); } if(unwindset_given) { unwindset.parse_unwindset( cmdline.get_comma_separated_values("unwindset"), + goto_model, ui_message_handler); } diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 7dc097efd03..04eaaf1f513 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -28,6 +28,7 @@ void unwindsett::parse_unwind(const std::string &unwind) void unwindsett::parse_unwindset_one_loop( std::string val, + abstract_goto_modelt &goto_model, message_handlert &message_handler) { if(val.empty()) @@ -181,10 +182,11 @@ void unwindsett::parse_unwindset_one_loop( void unwindsett::parse_unwindset( const std::list &unwindset, + abstract_goto_modelt &goto_model, message_handlert &message_handler) { for(auto &element : unwindset) - parse_unwindset_one_loop(element, message_handler); + parse_unwindset_one_loop(element, goto_model, message_handler); } std::optional @@ -211,6 +213,7 @@ unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const void unwindsett::parse_unwindset_file( const std::string &file_name, + abstract_goto_modelt &goto_model, message_handlert &message_handler) { std::ifstream file(widen_if_needed(file_name)); @@ -225,5 +228,5 @@ void unwindsett::parse_unwindset_file( split_string(buffer.str(), ',', true, true); for(auto &element : unwindset_elements) - parse_unwindset_one_loop(element, message_handler); + parse_unwindset_one_loop(element, goto_model, message_handler); } diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h index 4e3ffde0445..a4af6e161ec 100644 --- a/src/goto-instrument/unwindset.h +++ b/src/goto-instrument/unwindset.h @@ -30,9 +30,7 @@ class unwindsett // 2) a limit per loop, all threads // 3) a limit for a particular thread. // We use the most specific of the above. - explicit unwindsett(abstract_goto_modelt &goto_model) : goto_model(goto_model) - { - } + unwindsett() = default; // global limit for all loops void parse_unwind(const std::string &unwind); @@ -40,6 +38,7 @@ class unwindsett // limit for instances of a loop void parse_unwindset( const std::list &unwindset, + abstract_goto_modelt &goto_model, message_handlert &message_handler); // queries @@ -49,11 +48,10 @@ class unwindsett // read unwindset directives from a file void parse_unwindset_file( const std::string &file_name, + abstract_goto_modelt &goto_model, message_handlert &message_handler); protected: - abstract_goto_modelt &goto_model; - std::optional global_limit; // Limit for all instances of a loop. @@ -68,6 +66,7 @@ class unwindsett void parse_unwindset_one_loop( std::string loop_limit, + abstract_goto_modelt &goto_model, message_handlert &message_handler); }; diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 4b9ff978e99..ca6e49e58b4 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -415,7 +415,10 @@ void _check_with_strategy( propertiest properties(initialize_properties(goto_model)); std::unique_ptr worklist = get_path_strategy(strategy); guard_managert guard_manager; - unwindsett unwindset{goto_model}; + unwindsett unwindset; + unwindset.parse_unwind(options.get_option("unwind")); + unwindset.parse_unwindset( + options.get_list_option("unwindset"), goto_model, ui_message_handler); { // Put initial state into the work list @@ -428,7 +431,7 @@ void _check_with_strategy( *worklist, guard_manager, unwindset); - setup_symex(symex, ns, options, ui_message_handler); + setup_symex(symex, ns, ui_message_handler); symex.initialize_path_storage_from_entry_point_of( goto_symext::get_goto_function(goto_model), @@ -451,7 +454,7 @@ void _check_with_strategy( *worklist, guard_manager, unwindset); - setup_symex(symex, ns, options, ui_message_handler); + setup_symex(symex, ns, ui_message_handler); symex_symbol_table = symex.resume_symex_from_saved_state( goto_symext::get_goto_function(goto_model),