diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 210bf8dcf2a..e9ba3b202be 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -668,7 +668,8 @@ void code_contractst::apply_function_contract( // new program where all contract-derived instructions are added goto_programt new_program; - is_fresh_replacet is_fresh(*this, log, target_function); + is_fresh_replacet is_fresh( + goto_model, log.get_message_handler(), target_function); is_fresh.create_declarations(); is_fresh.add_memory_map_decl(new_program); @@ -1072,16 +1073,6 @@ void code_contractst::apply_loop_contract( } } -symbol_tablet &code_contractst::get_symbol_table() -{ - return symbol_table; -} - -goto_functionst &code_contractst::get_goto_functions() -{ - return goto_functions; -} - void code_contractst::check_frame_conditions_function(const irep_idt &function) { // Get the function object before instrumentation. @@ -1302,7 +1293,8 @@ void code_contractst::add_contract_check( instantiation_values.push_back(p); } - is_fresh_enforcet visitor(*this, log, wrapper_function); + is_fresh_enforcet visitor( + goto_model, log.get_message_handler(), wrapper_function); visitor.create_declarations(); visitor.add_memory_map_decl(check); diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 50cd1adb33f..3302dcf3074 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -126,10 +126,6 @@ class code_contractst exprt decreases_clause, const irep_idt &mode); - // for "helper" classes to update symbol table. - symbol_tablet &get_symbol_table(); - goto_functionst &get_goto_functions(); - std::unordered_map get_original_loop_number_map() const { diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index 48bc998d902..ad0a154c6ba 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -23,7 +23,6 @@ Date: July 2021 #include #include -#include "contracts.h" #include "instrument_spec_assigns.h" #include "utils.h" @@ -34,6 +33,8 @@ std::set &functions_in_scope_visitort::function_calls() void functions_in_scope_visitort::operator()(const goto_programt &prog) { + messaget log{message_handler}; + forall_goto_program_instructions(ins, prog) { if(ins->is_function_call()) @@ -163,12 +164,13 @@ void is_fresh_baset::add_memory_map_dead(goto_programt &program) void is_fresh_baset::add_declarations(const std::string &decl_string) { + messaget log{message_handler}; log.debug() << "Creating declarations: \n" << decl_string << "\n"; std::istringstream iss(decl_string); ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(log.get_message_handler()); + ansi_c_language.set_message_handler(message_handler); configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor; config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE; ansi_c_language.parse(iss, ""); @@ -181,10 +183,10 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) goto_functionst tmp_functions; // Add the new functions into the goto functions table. - parent.get_goto_functions().function_map[ensures_fn_name].copy_from( + goto_model.goto_functions.function_map[ensures_fn_name].copy_from( tmp_functions.function_map[ensures_fn_name]); - parent.get_goto_functions().function_map[requires_fn_name].copy_from( + goto_model.goto_functions.function_map[requires_fn_name].copy_from( tmp_functions.function_map[requires_fn_name]); for(const auto &symbol_pair : tmp_symbol_table.symbols) @@ -194,7 +196,7 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) symbol_pair.first == ensures_fn_name || symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc") { - this->parent.get_symbol_table().insert(symbol_pair.second); + goto_model.symbol_table.insert(symbol_pair.second); } // Parameters are stored as scoped names in the symbol table. else if( @@ -202,23 +204,23 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") || has_prefix( id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) && - parent.get_symbol_table().add(symbol_pair.second)) + goto_model.symbol_table.add(symbol_pair.second)) { UNREACHABLE; } } - if(parent.get_goto_functions().function_map.erase(INITIALIZE_FUNCTION) != 0) + if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0) { static_lifetime_init( - parent.get_symbol_table(), - parent.get_symbol_table().lookup_ref(INITIALIZE_FUNCTION).location); + goto_model.symbol_table, + goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); goto_convert( INITIALIZE_FUNCTION, - parent.get_symbol_table(), - parent.get_goto_functions(), + goto_model.symbol_table, + goto_model.goto_functions, log.get_message_handler()); - parent.get_goto_functions().update(); + goto_model.goto_functions.update(); } } @@ -247,10 +249,10 @@ void is_fresh_baset::update_fn_call( /* Declarations for contract enforcement */ is_fresh_enforcet::is_fresh_enforcet( - code_contractst &_parent, - messaget _log, - irep_idt _fun_id) - : is_fresh_baset(_parent, _log, _fun_id) + goto_modelt &goto_model, + message_handlert &message_handler, + const irep_idt &_fun_id) + : is_fresh_baset(goto_model, message_handler, _fun_id) { std::stringstream ssreq, ssensure, ssmemmap; ssreq << CPROVER_PREFIX "enforce_requires_is_fresh"; @@ -262,12 +264,12 @@ is_fresh_enforcet::is_fresh_enforcet( ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id; this->memmap_name = ssmemmap.str(); - const auto &mode = parent.get_symbol_table().lookup_ref(_fun_id).mode; + const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode; this->memmap_symbol = new_tmp_symbol( get_memmap_type(), source_locationt(), mode, - parent.get_symbol_table(), + goto_model.symbol_table, this->memmap_name, true); } @@ -275,7 +277,7 @@ is_fresh_enforcet::is_fresh_enforcet( void is_fresh_enforcet::create_declarations() { // Check if symbols are already declared - if(parent.get_symbol_table().lookup(requires_fn_name) != nullptr) + if(goto_model.symbol_table.has_symbol(requires_fn_name)) return; std::ostringstream oss; @@ -326,10 +328,10 @@ void is_fresh_enforcet::create_ensures_fn_call(goto_programt::targett &ins) } is_fresh_replacet::is_fresh_replacet( - code_contractst &_parent, - messaget _log, - irep_idt _fun_id) - : is_fresh_baset(_parent, _log, _fun_id) + goto_modelt &goto_model, + message_handlert &message_handler, + const irep_idt &_fun_id) + : is_fresh_baset(goto_model, message_handler, _fun_id) { std::stringstream ssreq, ssensure, ssmemmap; ssreq << CPROVER_PREFIX "replace_requires_is_fresh"; @@ -341,12 +343,12 @@ is_fresh_replacet::is_fresh_replacet( ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id; this->memmap_name = ssmemmap.str(); - const auto &mode = parent.get_symbol_table().lookup_ref(_fun_id).mode; + const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode; this->memmap_symbol = new_tmp_symbol( get_memmap_type(), source_locationt(), mode, - parent.get_symbol_table(), + goto_model.symbol_table, this->memmap_name, true); } @@ -354,8 +356,9 @@ is_fresh_replacet::is_fresh_replacet( void is_fresh_replacet::create_declarations() { // Check if symbols are already declared - if(parent.get_symbol_table().lookup(requires_fn_name) != nullptr) + if(goto_model.symbol_table.has_symbol(requires_fn_name)) return; + std::ostringstream oss; std::string cprover_prefix(CPROVER_PREFIX); oss << "static _Bool " << requires_fn_name diff --git a/src/goto-instrument/contracts/memory_predicates.h b/src/goto-instrument/contracts/memory_predicates.h index 4953f0fb5a3..2493f92da89 100644 --- a/src/goto-instrument/contracts/memory_predicates.h +++ b/src/goto-instrument/contracts/memory_predicates.h @@ -14,22 +14,22 @@ Date: July 2021 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H -#include #include #include -class code_contractst; class goto_functionst; +class goto_modelt; +class message_handlert; class is_fresh_baset { public: is_fresh_baset( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id) - : parent(_parent), log(_log), fun_id(_fun_id) + goto_modelt &goto_model, + message_handlert &message_handler, + const irep_idt &_fun_id) + : goto_model(goto_model), message_handler(message_handler), fun_id(_fun_id) { } @@ -51,9 +51,9 @@ class is_fresh_baset virtual void create_requires_fn_call(goto_programt::targett &target) = 0; virtual void create_ensures_fn_call(goto_programt::targett &target) = 0; - code_contractst &parent; - messaget log; - irep_idt fun_id; + goto_modelt &goto_model; + message_handlert &message_handler; + const irep_idt &fun_id; // written by the child classes. std::string memmap_name; @@ -68,9 +68,9 @@ class is_fresh_enforcet : public is_fresh_baset { public: is_fresh_enforcet( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id); + goto_modelt &goto_model, + message_handlert &message_handler, + const irep_idt &_fun_id); virtual void create_declarations(); @@ -83,9 +83,9 @@ class is_fresh_replacet : public is_fresh_baset { public: is_fresh_replacet( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id); + goto_modelt &goto_model, + message_handlert &message_handler, + const irep_idt &_fun_id); virtual void create_declarations(); @@ -121,8 +121,8 @@ class functions_in_scope_visitort public: functions_in_scope_visitort( const goto_functionst &goto_functions, - messaget &log) - : goto_functions(goto_functions), log(log) + message_handlert &message_handler) + : goto_functions(goto_functions), message_handler(message_handler) { } @@ -133,7 +133,7 @@ class functions_in_scope_visitort protected: const goto_functionst &goto_functions; - messaget &log; + message_handlert &message_handler; std::set function_set; };