From 921218f8dcfb9edf8d0c5e7732d50d4859b66d66 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 May 2025 12:52:52 +0000 Subject: [PATCH] Make goto_symext::language_mode protected This should be set via constructors. Remove bmc_util/setup_symex as all work is done through constructors. --- src/goto-checker/bmc_util.cpp | 26 +++---------------- src/goto-checker/bmc_util.h | 2 -- .../multi_path_symex_only_checker.cpp | 1 - .../single_loop_incremental_symex_checker.cpp | 1 - .../single_path_symex_only_checker.cpp | 5 ---- .../single_path_symex_only_checker.h | 5 +++- src/goto-checker/symex_bmc.cpp | 9 +++++++ src/goto-symex/goto_symex.h | 3 --- unit/path_strategies.cpp | 2 -- 9 files changed, 17 insertions(+), 37 deletions(-) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index beb9f9880dd..4a3b24fdccf 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -11,7 +11,8 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" -#include +#include +#include #include #include @@ -21,17 +22,13 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include - -#include - #include -#include -#include - #include "goto_symex_property_decider.h" #include "symex_bmc.h" +#include + void message_building_error_trace(messaget &log) { log.status() << "Building error trace" << messaget::eom; @@ -175,21 +172,6 @@ get_memory_model(const optionst &options, const namespacet &ns) } } -void setup_symex( - symex_bmct &symex, - const namespacet &ns, - ui_message_handlert &ui_message_handler) -{ - messaget msg(ui_message_handler); - const symbolt *init_symbol; - if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) - symex.language_mode = init_symbol->mode; - - msg.status() << "Starting Bounded Model Checking" << messaget::eom; - - symex.last_source_location.make_nil(); -} - void slice( symex_bmct &symex, symex_target_equationt &symex_target_equation, diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index f1bf8f0832f..c604856d7ba 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -69,8 +69,6 @@ void output_graphml( std::unique_ptr get_memory_model(const optionst &options, const namespacet &); -void setup_symex(symex_bmct &, const namespacet &, ui_message_handlert &); - void slice( symex_bmct &, symex_target_equationt &symex_target_equation, diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 96dd05595cf..ce81e072e1d 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -39,7 +39,6 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( 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 612dba43d9f..f264a728f58 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -42,7 +42,6 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( 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 8648ffc4d1d..7a5e8ffe5b7 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -152,11 +152,6 @@ void single_path_symex_only_checkert::equation_output( } } -void single_path_symex_only_checkert::setup_symex(symex_bmct &symex) -{ - ::setup_symex(symex, ns, ui_message_handler); -} - void single_path_symex_only_checkert::update_properties( propertiest &properties, std::unordered_set &updated_properties, diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h index aee94cbbb68..6ead770bdd0 100644 --- a/src/goto-checker/single_path_symex_only_checker.h +++ b/src/goto-checker/single_path_symex_only_checker.h @@ -48,7 +48,10 @@ class single_path_symex_only_checkert : public incremental_goto_checkert const symex_bmct &symex, const symex_target_equationt &equation); - virtual void setup_symex(symex_bmct &symex); + virtual void setup_symex(symex_bmct &symex) + { + // deriving classes may do extra work here + } /// Adds the initial goto-symex state as a path to the worklist virtual void initialize_worklist(); diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index de4ecdd28b4..58e1f734c21 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include symex_bmct::symex_bmct( @@ -33,10 +35,17 @@ symex_bmct::symex_bmct( options, path_storage, guard_manager), + last_source_location(source_locationt::nil()), record_coverage(!options.get_option("symex-coverage-report").empty()), unwindset(unwindset), symex_coverage(ns) { + const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION); + if(init_symbol) + language_mode = init_symbol->mode; + + messaget msg{mh}; + msg.status() << "Starting Bounded Model Checking" << messaget::eom; } /// show progress diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 28518580aec..5980573f0cd 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -235,13 +235,10 @@ class goto_symext messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target); -public: - /// language_mode: ID_java, ID_C or another language identifier /// if we know the source language in use, irep_idt() otherwise. irep_idt language_mode; -protected: /// The symbol table associated with the goto-program being executed. /// This symbol table will not have objects that are dynamically created as /// part of symbolic execution added to it; those object are stored in the diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index fd1e33b55d9..b0b99b94d69 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -425,7 +425,6 @@ void _check_with_strategy( *worklist, guard_manager, unwindset); - setup_symex(symex, ns, ui_message_handler); symex.initialize_path_storage_from_entry_point_of( goto_symext::get_goto_function(goto_model), @@ -448,7 +447,6 @@ void _check_with_strategy( *worklist, guard_manager, unwindset); - setup_symex(symex, ns, ui_message_handler); symex_symbol_table = symex.resume_symex_from_saved_state( goto_symext::get_goto_function(goto_model),