diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index af0308edc4a..db97996db2b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -188,23 +188,20 @@ dfcct::dfcct( to_exclude_from_nondet_static(to_exclude_from_nondet_static), message_handler(message_handler), log(message_handler), - utils(goto_model, message_handler), - library(goto_model, utils, message_handler), + library(goto_model, message_handler), ns(goto_model.symbol_table), - spec_functions(goto_model, message_handler, utils, library), - contract_clauses_codegen(goto_model, message_handler, utils, library), + spec_functions(goto_model, message_handler, library), + contract_clauses_codegen(goto_model, message_handler, library), instrument( goto_model, message_handler, - utils, library, spec_functions, contract_clauses_codegen), - memory_predicates(goto_model, utils, library, instrument, message_handler), + memory_predicates(goto_model, library, instrument, message_handler), contract_handler( goto_model, message_handler, - utils, library, instrument, memory_predicates, @@ -213,7 +210,6 @@ dfcct::dfcct( swap_and_wrap( goto_model, message_handler, - utils, library, instrument, spec_functions, @@ -227,7 +223,7 @@ void dfcct::check_transform_goto_model_preconditions() { // check that harness function exists PRECONDITION_WITH_DIAGNOSTICS( - utils.function_symbol_with_body_exists(harness_id), + dfcc_utilst::function_symbol_with_body_exists(goto_model, harness_id), "Harness function '" + id2string(harness_id) + "' either not found or has no body"); @@ -235,7 +231,7 @@ void dfcct::check_transform_goto_model_preconditions() { auto pair = to_check.value(); PRECONDITION_WITH_DIAGNOSTICS( - utils.function_symbol_with_body_exists(pair.first), + dfcc_utilst::function_symbol_with_body_exists(goto_model, pair.first), "Function to check '" + id2string(pair.first) + "' either not found or has no body"); @@ -268,7 +264,7 @@ void dfcct::check_transform_goto_model_preconditions() // for functions to replace with contracts we don't require the replaced // function to have a body because only the contract is actually used PRECONDITION_WITH_DIAGNOSTICS( - utils.function_symbol_exists(pair.first), + dfcc_utilst::function_symbol_exists(goto_model, pair.first), "Function to replace '" + id2string(pair.first) + "' not found"); // triggers signature compatibility checking @@ -454,7 +450,7 @@ void dfcct::wrap_discovered_function_pointer_contracts() { // we need to swap it with itself PRECONDITION_WITH_DIAGNOSTICS( - utils.function_symbol_exists(str), + dfcc_utilst::function_symbol_exists(goto_model, str), "Function pointer contract '" + str + "' not found."); // triggers signature compatibility checking @@ -581,7 +577,7 @@ void dfcct::reinitialize_model() goto_model.symbol_table.symbols.find(goto_functionst::entry_point())); // regenerate the CPROVER start function generate_ansi_c_start_function( - utils.get_function_symbol(harness_id), + dfcc_utilst::get_function_symbol(goto_model.symbol_table, harness_id), goto_model.symbol_table, message_handler, c_object_factory_parameterst(options)); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 83ff4b8a2b7..46f0ad9846f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -41,7 +41,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_loop_contract_mode.h" #include "dfcc_spec_functions.h" #include "dfcc_swap_and_wrap.h" -#include "dfcc_utils.h" #include #include @@ -217,7 +216,6 @@ class dfcct // Singletons that hold the global state of the program transformation // (caches etc.) - dfcc_utilst utils; dfcc_libraryt library; namespacet ns; dfcc_spec_functionst spec_functions; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 67857f71548..bfa1569d32e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -436,9 +436,8 @@ static dfcc_loop_infot gen_dfcc_loop_info( dirtyt &dirty, local_may_aliast &local_may_alias, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, - symbol_tablet &symbol_table) + symbol_table_baset &symbol_table) { std::unordered_set loop_locals = gen_loop_locals_set(loop_nesting_graph, loop_id); @@ -472,7 +471,8 @@ static dfcc_loop_infot gen_dfcc_loop_info( auto &loop = loop_nesting_graph[loop_id]; const auto cbmc_loop_number = loop.latch->loop_number; - const auto &language_mode = utils.get_function_symbol(function_id).mode; + const auto &language_mode = + dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; // Generate "write set" variable const auto &write_set_var = @@ -515,9 +515,8 @@ dfcc_cfg_infot::dfcc_cfg_infot( goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library) : function_id(function_id), goto_function(goto_function), @@ -581,7 +580,6 @@ dfcc_cfg_infot::dfcc_cfg_infot( dirty, local_may_alias, message_handler, - utils, library, symbol_table)}); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index 3c36c55d9d2..b51da60a041 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -29,7 +29,6 @@ Date: March 2023 #include #include -class dfcc_utilst; class dfcc_libraryt; class goto_functiont; class message_handlert; @@ -240,9 +239,8 @@ class dfcc_cfg_infot goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library); void output(std::ostream &out) const; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp index e18b949ed3c..6c0d8baf321 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -30,12 +30,10 @@ Date: February 2023 dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library) : goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), ns(goto_model.symbol_table) { @@ -233,7 +231,9 @@ void dfcc_contract_clauses_codegent::encode_freeable_target( { // A plain `target` becomes `CALL __CPROVER_freeable(target);` code_function_callt code_function_call( - utils.get_function_symbol(CPROVER_PREFIX "freeable").symbol_expr()); + dfcc_utilst::get_function_symbol( + goto_model.symbol_table, CPROVER_PREFIX "freeable") + .symbol_expr()); auto &arguments = code_function_call.arguments(); arguments.emplace_back(target); @@ -258,12 +258,14 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings( std::set recursive_call; std::set not_enough_arguments; - utils.inline_program( + dfcc_utilst::inline_program( + goto_model, goto_program, no_body, recursive_call, missing_function, - not_enough_arguments); + not_enough_arguments, + message_handler); // check that the only no body / missing functions are the cprover builtins for(const auto &id : no_body) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h index 4609569a1d6..09cf3cd0143 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h @@ -28,7 +28,6 @@ Date: February 2023 class goto_modelt; class message_handlert; class dfcc_libraryt; -class dfcc_utilst; class code_with_contract_typet; class conditional_target_group_exprt; @@ -39,12 +38,10 @@ class dfcc_contract_clauses_codegent public: /// \param goto_model GOTO model being transformed /// \param message_handler Used debug/warning/error messages - /// \param utils Utility class for dynamic frames /// \param library The contracts instrumentation library dfcc_contract_clauses_codegent( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library); /// \brief Generates instructions encoding the \p assigns_clause targets and @@ -81,7 +78,6 @@ class dfcc_contract_clauses_codegent goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; namespacet ns; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp index 9e2c545dfd9..33b4cec65db 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp @@ -26,13 +26,11 @@ Date: August 2022 #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_spec_functions.h" -#include "dfcc_utils.h" dfcc_contract_functionst::dfcc_contract_functionst( const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen, @@ -48,7 +46,6 @@ dfcc_contract_functionst::dfcc_contract_functionst( goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), spec_functions(spec_functions), contract_clauses_codegen(contract_clauses_codegen), @@ -122,8 +119,11 @@ const std::size_t dfcc_contract_functionst::get_nof_frees_targets() const void dfcc_contract_functionst::gen_spec_assigns_function() { - const auto &spec_function_symbol = utils.clone_and_rename_function( - pure_contract_symbol.name, spec_assigns_function_id, empty_typet()); + const auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function( + goto_model, + pure_contract_symbol.name, + spec_assigns_function_id, + empty_typet()); const auto &spec_function_id = spec_function_symbol.name; @@ -171,8 +171,11 @@ void dfcc_contract_functionst::gen_spec_frees_function() const auto &code_with_contract = to_code_with_contract_type(pure_contract_symbol.type); - auto &spec_function_symbol = utils.clone_and_rename_function( - pure_contract_symbol.name, spec_frees_function_id, empty_typet()); + auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function( + goto_model, + pure_contract_symbol.name, + spec_frees_function_id, + empty_typet()); const auto &spec_function_id = spec_function_symbol.name; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h index d0a811c6b56..f274aa5f8f0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h @@ -28,7 +28,6 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; -class dfcc_utilst; class dfcc_instrumentt; class dfcc_spec_functionst; class dfcc_contract_clauses_codegent; @@ -68,7 +67,6 @@ class dfcc_contract_functionst /// \param pure_contract_symbol the contract to generate code from /// \param goto_model goto model being transformed /// \param message_handler used debug/warning/error messages - /// \param utils utility class for dynamic frames /// \param library the contracts instrumentation library /// \param spec_functions provides translation methods for assignable set /// \param contract_clauses_codegen provides GOTO code generation methods @@ -78,7 +76,6 @@ class dfcc_contract_functionst const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen, @@ -126,7 +123,6 @@ class dfcc_contract_functionst goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_spec_functionst &spec_functions; dfcc_contract_clauses_codegent &contract_clauses_codegen; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index 91096acb576..c3add8fb8ed 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -30,7 +30,6 @@ Date: August 2022 #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_spec_functions.h" -#include "dfcc_utils.h" #include "dfcc_wrapper_program.h" std::map @@ -39,7 +38,6 @@ std::map dfcc_contract_handlert::dfcc_contract_handlert( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, @@ -48,7 +46,6 @@ dfcc_contract_handlert::dfcc_contract_handlert( : goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), instrument(instrument), memory_predicates(memory_predicates), @@ -75,7 +72,6 @@ dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id) get_pure_contract_symbol(contract_id), goto_model, message_handler, - utils, library, spec_functions, contract_clauses_codegen, @@ -100,13 +96,12 @@ void dfcc_contract_handlert::add_contract_instructions( { dfcc_wrapper_programt( contract_mode, - utils.get_function_symbol(wrapper_id), - utils.get_function_symbol(wrapped_id), + dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id), + dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapped_id), get_contract_functions(contract_id), wrapper_write_set_symbol, goto_model, message_handler, - utils, library, instrument, memory_predicates) @@ -124,7 +119,8 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol( if(function_id_opt.has_value()) { auto function_id = function_id_opt.value(); - const auto &function_symbol = utils.get_function_symbol(function_id); + const auto &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); check_signature_compat( function_id, to_code_type(function_symbol.type), @@ -145,7 +141,8 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol( "to derive a default contract"); auto function_id = function_id_opt.value(); - const auto &function_symbol = utils.get_function_symbol(function_id); + const auto &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); log.warning() << "Contract '" << contract_id << "' not found, deriving empty pure contract '" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index 4535f00c4f4..51020c9547e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -27,7 +27,6 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; -class dfcc_utilst; class dfcc_instrumentt; class dfcc_lift_memory_predicatest; class dfcc_spec_functionst; @@ -69,7 +68,6 @@ class dfcc_contract_handlert dfcc_contract_handlert( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, @@ -119,7 +117,6 @@ class dfcc_contract_handlert goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; dfcc_lift_memory_predicatest &memory_predicates; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index fe3bc6b1a19..244497014aa 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -48,21 +48,18 @@ std::set dfcc_instrumentt::function_cache; dfcc_instrumentt::dfcc_instrumentt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen) : goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), spec_functions(spec_functions), contract_clauses_codegen(contract_clauses_codegen), instrument_loop( goto_model, message_handler, - utils, library, spec_functions, contract_clauses_codegen), @@ -257,16 +254,17 @@ void dfcc_instrumentt::instrument_harness_function( to_pointer_type(library.dfcc_type[dfcc_typet::WRITE_SET_PTR])); // create a local write set symbol - const auto &function_symbol = utils.get_function_symbol(function_id); - const auto &write_set = utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET_PTR], - function_id, - "__write_set_to_check", - function_symbol.location, - function_symbol.mode, - function_symbol.module, - false) + const auto &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); + const auto &write_set = dfcc_utilst::create_symbol( + goto_model.symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + function_id, + "__write_set_to_check", + function_symbol.location, + function_symbol.mode, + function_symbol.module, + false) .symbol_expr(); std::set local_statics = get_local_statics(function_id); @@ -335,11 +333,11 @@ void dfcc_instrumentt::instrument_function( found != goto_model.goto_functions.function_map.end(), "Function '" + id2string(function_id) + "' must exist in the model."); - const auto &write_set = utils - .add_parameter( - function_id, - "__write_set_to_check", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + const auto &write_set = dfcc_utilst::add_parameter( + goto_model, + function_id, + "__write_set_to_check", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) .symbol_expr(); std::set local_statics = get_local_statics(function_id); @@ -373,11 +371,11 @@ void dfcc_instrumentt::instrument_wrapped_function( "Function '" + id2string(wrapped_function_id) + "' must exist in the model."); - const auto &write_set = utils - .add_parameter( - wrapped_function_id, - "__write_set_to_check", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + const auto &write_set = dfcc_utilst::add_parameter( + goto_model, + wrapped_function_id, + "__write_set_to_check", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) .symbol_expr(); std::set local_statics = get_local_statics(initial_function_id); @@ -411,7 +409,6 @@ void dfcc_instrumentt::instrument_goto_program( dfcc_loop_contract_modet::NONE, goto_model.symbol_table, message_handler, - utils, library); // instrument instructions @@ -461,7 +458,6 @@ void dfcc_instrumentt::instrument_goto_function( loop_contract_mode, goto_model.symbol_table, message_handler, - utils, library); // instrument instructions @@ -577,7 +573,7 @@ void dfcc_instrumentt::insert_add_decl_call( goto_programt payload; const auto &target_location = target->source_location(); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_add_decl_call( @@ -624,7 +620,7 @@ void dfcc_instrumentt::insert_record_dead_call( goto_programt payload; const auto &target_location = target->source_location(); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_record_dead_call( @@ -667,14 +663,15 @@ void dfcc_instrumentt::instrument_lhs( goto_programt &goto_program, dfcc_cfg_infot &cfg_info) { - const auto &mode = utils.get_function_symbol(function_id).mode; + const auto &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; goto_programt payload; const auto &lhs_source_location = target->source_location(); auto &write_set = cfg_info.get_write_set(target); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), lhs_source_location)); + dfcc_utilst::make_null_check_expr(write_set), lhs_source_location)); source_locationt check_source_location(target->source_location()); check_source_location.set_property_class("assigns"); @@ -694,13 +691,15 @@ void dfcc_instrumentt::instrument_lhs( // ASSIGN lhs := rhs; // ``` - auto &check_sym = utils.create_symbol( + auto &check_sym = dfcc_utilst::create_symbol( + goto_model.symbol_table, bool_typet(), id2string(function_id), "__check_lhs_assignment", lhs_source_location, mode, - utils.get_function_symbol(function_id).module, + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) + .module, false); const auto &check_var = check_sym.symbol_expr(); @@ -713,7 +712,7 @@ void dfcc_instrumentt::instrument_lhs( write_set, typecast_exprt::conditional_cast( address_of_exprt(lhs), pointer_type(empty_typet{})), - utils.make_sizeof_expr(lhs), + dfcc_utilst::make_sizeof_expr(lhs, ns), lhs_source_location), lhs_source_location)); @@ -798,7 +797,7 @@ void dfcc_instrumentt::instrument_assign( goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_record_dead_call( @@ -831,7 +830,7 @@ void dfcc_instrumentt::instrument_assign( goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_add_allocated_call(write_set, lhs, target_location), @@ -951,11 +950,12 @@ void dfcc_instrumentt::instrument_deallocate_call( // ---- // CALL __CPROVER_deallocate(ptr); // ``` - const auto &mode = utils.get_function_symbol(function_id).mode; + const auto &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); auto &check_sym = get_fresh_aux_symbol( bool_typet(), @@ -1054,11 +1054,13 @@ void dfcc_instrumentt::instrument_other( // ---- // OTHER {statement = array_set, args = {dest, value}}; // ``` - const auto &mode = utils.get_function_symbol(function_id).mode; + const auto &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) + .mode; goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); auto &check_sym = get_fresh_aux_symbol( bool_typet(), @@ -1113,11 +1115,13 @@ void dfcc_instrumentt::instrument_other( // ---- // OTHER {statement = array_replace, args = {dest, src}}; // ``` - const auto &mode = utils.get_function_symbol(function_id).mode; + const auto &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) + .mode; goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); auto &check_sym = get_fresh_aux_symbol( bool_typet(), @@ -1166,11 +1170,13 @@ void dfcc_instrumentt::instrument_other( // ASSERT(check_havoc_object); // DEAD check_havoc_object; // ``` - const auto &mode = utils.get_function_symbol(function_id).mode; + const auto &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) + .mode; goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target_location)); + dfcc_utilst::make_null_check_expr(write_set), target_location)); auto &check_sym = get_fresh_aux_symbol( bool_typet(), diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index c02f1e6a55c..a65aaece8c0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -35,9 +35,6 @@ class conditional_target_group_exprt; class dfcc_libraryt; class dfcc_spec_functionst; class dfcc_contract_clauses_codegent; -class dfcc_utilst; -class dfcc_loop_utilst; -class dirtyt; class dfcc_cfg_infot; /// This class instruments GOTO functions or instruction sequences @@ -48,7 +45,6 @@ class dfcc_instrumentt dfcc_instrumentt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen); @@ -169,7 +165,6 @@ class dfcc_instrumentt goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_spec_functionst &spec_functions; dfcc_contract_clauses_codegent &contract_clauses_codegen; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index dbdfc4f6597..82b45843d24 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -27,13 +27,11 @@ Date: April 2023 dfcc_instrument_loopt::dfcc_instrument_loopt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen) : goto_model(goto_model), log(message_handler), - utils(utils), library(library), spec_functions(spec_functions), contract_clauses_codegen(contract_clauses_codegen), @@ -52,7 +50,8 @@ void dfcc_instrument_loopt::operator()( const dfcc_loop_infot &loop = cfg_info.get_loop_info(loop_id); const std::size_t cbmc_loop_id = loop.cbmc_loop_id; const exprt &outer_write_set = cfg_info.get_outer_write_set(loop_id); - const irep_idt language_mode = utils.get_function_symbol(function_id).mode; + const irep_idt language_mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; goto_programt::targett head = loop.find_head(goto_function.body).value(); auto head_location(head->source_location()); @@ -137,26 +136,27 @@ void dfcc_instrument_loopt::operator()( // Construct the write set from loop assigns target. That is, contract_assigns // in the result __CPROVER_contracts_write_set_t should be the set of CAR // of the loop assign targets. - goto_programt assigns_instrs; goto_programt write_set_populate_instrs; + contract_clauses_codegen.gen_spec_assigns_instructions( + language_mode, assigns, write_set_populate_instrs); // havoc(w_loop); // The generated GOTO instructions havoc the write set of the loop. goto_programt havoc_instrs; - contract_clauses_codegen.gen_spec_assigns_instructions( - language_mode, assigns, assigns_instrs); spec_functions.generate_havoc_instructions( function_id, language_mode, symbol_table.get_writeable_ref(function_id).module, - assigns_instrs, + write_set_populate_instrs, loop.addr_of_write_set_var, havoc_instrs, nof_targets); spec_functions.to_spec_assigns_instructions( - loop.addr_of_write_set_var, language_mode, assigns_instrs, nof_targets); - write_set_populate_instrs.copy_from(assigns_instrs); + loop.addr_of_write_set_var, + language_mode, + write_set_populate_instrs, + nof_targets); // Replace bound variables by fresh instances in quantified formulas. exprt invariant = loop.invariant; @@ -238,7 +238,7 @@ std::unordered_map dfcc_instrument_loopt::add_prehead_instructions( const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, @@ -355,7 +355,7 @@ dfcc_instrument_loopt::add_step_instructions( const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, @@ -493,7 +493,7 @@ void dfcc_instrument_loopt::add_body_instructions( const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, const exprt &invariant, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h index 050e1690ce6..64ce8674b57 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -24,7 +24,6 @@ Date: April 2023 #include class dfcc_spec_functionst; -class dfcc_utilst; class dfcc_libraryt; class dfcc_instrumentt; class dfcc_spec_functionst; @@ -39,7 +38,6 @@ class dfcc_instrument_loopt /// \brief Constructor for the loop contract instrumentation class. /// \param[inout] goto_model GOTO model being instrumented /// \param[inout] message_handler For status/debug output - /// \param[inout] utils DFCC utility methods /// \param[inout] library DFCC instrumentation library functions /// \param[inout] spec_functions Class used to translate assigns clauses /// to GOTO instructions. @@ -48,7 +46,6 @@ class dfcc_instrument_loopt dfcc_instrument_loopt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen); @@ -151,7 +148,6 @@ class dfcc_instrument_loopt std::size_t max_assigns_clause_size = 0; goto_modelt &goto_model; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_spec_functionst &spec_functions; dfcc_contract_clauses_codegent &contract_clauses_codegen; @@ -200,7 +196,7 @@ class dfcc_instrument_loopt std::unordered_map add_prehead_instructions( const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, @@ -251,7 +247,7 @@ class dfcc_instrument_loopt const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, @@ -299,7 +295,7 @@ class dfcc_instrument_loopt const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, const exprt &invariant, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index bdcb74865b2..c4c5e8902bc 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -173,10 +173,8 @@ const std::set create_assignable_builtin_names() /// Class constructor dfcc_libraryt::dfcc_libraryt( goto_modelt &goto_model, - dfcc_utilst &utils, message_handlert &message_handler) : goto_model(goto_model), - utils(utils), message_handler(message_handler), log(message_handler), dfcc_type_to_name(create_dfcc_type_to_name()), @@ -411,7 +409,8 @@ void dfcc_libraryt::inline_functions() inlined = true; for(const auto &function_id : to_inline) { - utils.inline_function(dfcc_fun_to_name.at(function_id)); + dfcc_utilst::inline_function( + goto_model, dfcc_fun_to_name.at(function_id), message_handler); } } @@ -523,7 +522,8 @@ const symbolt &dfcc_libraryt::get_instrumented_functions_map_symbol() auto map_type = array_typet(unsigned_char_type(), infinity_exprt(size_type())); - return utils.create_static_symbol( + return dfcc_utilst::create_static_symbol( + goto_model.symbol_table, map_type, "", "__dfcc_instrumented_functions", @@ -544,8 +544,9 @@ void dfcc_libraryt::add_instrumented_functions_map_init_instructions( for(auto &function_id : instrumented_functions) { - auto object_id = pointer_object( - address_of_exprt(utils.get_function_symbol(function_id).symbol_expr())); + auto object_id = pointer_object(address_of_exprt( + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) + .symbol_expr())); auto index_expr = index_exprt(instrumented_functions_map, object_id); dest.add(goto_programt::make_assignment( index_expr, from_integer(1, unsigned_char_type()), source_location)); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index 8e59fa78dbf..615d88785d4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -148,7 +148,6 @@ class message_handlert; class symbolt; class symbol_exprt; class typet; -class dfcc_utilst; /// Class interface to library types and functions defined in /// `cprover_contracts.c`. @@ -157,7 +156,6 @@ class dfcc_libraryt public: dfcc_libraryt( goto_modelt &goto_model, - dfcc_utilst &utils, message_handlert &lmessage_handler); protected: @@ -175,7 +173,6 @@ class dfcc_libraryt static bool malloc_free_fixed; goto_modelt &goto_model; - dfcc_utilst &utils; message_handlert &message_handler; messaget log; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index afe413858dd..47953afeda8 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -24,12 +24,10 @@ Date: August 2022 dfcc_lift_memory_predicatest::dfcc_lift_memory_predicatest( goto_modelt &goto_model, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler) : goto_model(goto_model), - utils(utils), library(library), instrument(instrument), log(message_handler) @@ -214,7 +212,8 @@ static optionalt is_param_expr( void dfcc_lift_memory_predicatest::collect_parameters_to_lift( const irep_idt &function_id) { - const symbolt &function_symbol = utils.get_function_symbol(function_id); + const symbolt &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); // map of parameter name to its rank in the signature std::map parameter_rank; const auto ¶meters = to_code_type(function_symbol.type).parameters(); @@ -279,7 +278,8 @@ void dfcc_lift_memory_predicatest::add_pointer_type( const std::size_t parameter_rank, replace_symbolt &replace_lifted_param) { - symbolt &function_symbol = utils.get_function_symbol(function_id); + symbolt &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); code_typet &code_type = to_code_type(function_symbol.type); auto ¶meters = code_type.parameters(); auto ¶meter_id = parameters[parameter_rank].get_identifier(); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h index e18cfab729a..7b59b2c16d1 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h @@ -26,7 +26,6 @@ Date: November 2022 #include #include -class dfcc_utilst; class dfcc_libraryt; class dfcc_instrumentt; class message_handlert; @@ -38,13 +37,11 @@ class dfcc_lift_memory_predicatest { public: /// \param goto_model The goto model to process - /// \param utils Utility methods /// \param library The contracts instrumentation library /// \param instrument The DFCC instrumenter object /// \param message_handler Used for messages dfcc_lift_memory_predicatest( goto_modelt &goto_model, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler); @@ -70,7 +67,6 @@ class dfcc_lift_memory_predicatest protected: goto_modelt &goto_model; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; messaget log; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index eb1ddd428dd..df28667317e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -18,17 +18,14 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_library.h" #include "dfcc_loop_contract_mode.h" -#include "dfcc_utils.h" dfcc_spec_functionst::dfcc_spec_functionst( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library) : goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), ns(goto_model.symbol_table) { @@ -54,10 +51,12 @@ void dfcc_spec_functionst::generate_havoc_function( "DFCC: havoc function id '" + id2string(havoc_function_id) + "' already exists"); - const auto &function_symbol = utils.get_function_symbol(function_id); + const auto &function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); // create the write_set symbol used as input by the havoc function - const auto &write_set_symbol = utils.create_symbol( + const auto &write_set_symbol = dfcc_utilst::create_symbol( + goto_model.symbol_table, library.dfcc_type[dfcc_typet::CAR_SET_PTR], id2string(havoc_function_id), "__write_set_to_havoc", @@ -118,12 +117,14 @@ void dfcc_spec_functionst::generate_havoc_function( std::set missing_function; std::set recursive_call; std::set not_enough_arguments; - utils.inline_function( + dfcc_utilst::inline_function( + goto_model, havoc_function_id, no_body, recursive_call, missing_function, - not_enough_arguments); + not_enough_arguments, + message_handler); INVARIANT( no_body.empty(), "no body warnings when inlining " + id2string(havoc_function_id)); @@ -201,7 +202,8 @@ void dfcc_spec_functionst::generate_havoc_instructions( // declare a local var to store targets havoced via nondet assignment auto &target_type = get_target_type(ins_it->call_arguments().at(0)); - const auto &target_symbol = utils.create_symbol( + const auto &target_symbol = dfcc_utilst::create_symbol( + goto_model.symbol_table, pointer_type(target_type), id2string(function_id), "__havoc_target", @@ -218,7 +220,7 @@ void dfcc_spec_functionst::generate_havoc_instructions( auto goto_instruction = havoc_program.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(target_expr), location)); + dfcc_utilst::make_null_check_expr(target_expr), location)); // create nondet assignment to the target side_effect_expr_nondett nondet(target_type, location); @@ -257,16 +259,16 @@ void dfcc_spec_functionst::to_spec_assigns_function( // add write_set parameter const exprt write_set_to_fill = - utils - .add_parameter( - function_id, - "__write_set_to_fill", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + dfcc_utilst::add_parameter( + goto_model, + function_id, + "__write_set_to_fill", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) .symbol_expr(); to_spec_assigns_instructions( write_set_to_fill, - utils.get_function_symbol(function_id).mode, + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode, goto_function.body, nof_targets); @@ -340,16 +342,16 @@ void dfcc_spec_functionst::to_spec_frees_function( // add __dfcc_set parameter const exprt &write_set_to_fill = - utils - .add_parameter( - function_id, - "__write_set_to_fill", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + dfcc_utilst::add_parameter( + goto_model, + function_id, + "__write_set_to_fill", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) .symbol_expr(); to_spec_frees_instructions( write_set_to_fill, - utils.get_function_symbol(function_id).mode, + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode, goto_function.body, nof_targets); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index 42d188cb762..cbd89910e32 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -46,7 +46,6 @@ class dfcc_spec_functionst dfcc_spec_functionst( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library); /// From a function: @@ -207,7 +206,6 @@ class dfcc_spec_functionst goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; namespacet ns; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index e2a9f22cd7f..8a74801b169 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -38,7 +38,6 @@ Author: Remi Delmas, delmarsd@amazon.com dfcc_swap_and_wrapt::dfcc_swap_and_wrapt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_spec_functionst &spec_functions, @@ -46,7 +45,6 @@ dfcc_swap_and_wrapt::dfcc_swap_and_wrapt( : goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), instrument(instrument), spec_functions(spec_functions), @@ -165,33 +163,34 @@ void dfcc_swap_and_wrapt::check_contract( const irep_idt &wrapper_id = function_id; const irep_idt wrapped_id = id2string(wrapper_id) + "_wrapped_for_contract_checking"; - utils.wrap_function(wrapper_id, wrapped_id); + dfcc_utilst::wrap_function(goto_model, wrapper_id, wrapped_id); // wrapper body goto_programt body; - const auto &wrapper_symbol = utils.get_function_symbol(wrapper_id); + const auto &wrapper_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id); + + auto check_started = dfcc_utilst::create_static_symbol( + goto_model.symbol_table, + bool_typet(), + id2string(function_id), + "__contract_check_in_progress", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false_exprt()) + .symbol_expr(); - auto check_started = utils - .create_static_symbol( + auto check_completed = dfcc_utilst::create_static_symbol( + goto_model.symbol_table, bool_typet(), id2string(function_id), - "__contract_check_in_progress", + "__contract_checked_once", wrapper_symbol.location, wrapper_symbol.mode, wrapper_symbol.module, false_exprt()) - .symbol_expr(); - - auto check_completed = utils - .create_static_symbol( - bool_typet(), - id2string(function_id), - "__contract_checked_once", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false_exprt()) .symbol_expr(); auto check_started_goto = body.add(goto_programt::make_incomplete_goto( @@ -213,7 +212,8 @@ void dfcc_swap_and_wrapt::check_contract( body.add(goto_programt::make_assignment( check_started, true_exprt(), wrapper_symbol.location)); - const auto write_set_symbol = utils.create_new_parameter_symbol( + const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol( + goto_model.symbol_table, function_id, "__write_set_to_check", library.dfcc_type[dfcc_typet::CAR_SET_PTR]); @@ -273,7 +273,7 @@ void dfcc_swap_and_wrapt::check_contract( goto_model.goto_functions.function_map.at(function_id).body.swap(body); // extend the signature of the wrapper function with the write set parameter - utils.add_parameter(write_set_symbol, function_id); + dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id); goto_model.goto_functions.function_map.at(wrapper_id).make_hidden(); @@ -292,9 +292,10 @@ void dfcc_swap_and_wrapt::replace_with_contract( const irep_idt &wrapper_id = function_id; const irep_idt wrapped_id = id2string(function_id) + "_wrapped_for_replacement_with_contract"; - utils.wrap_function(function_id, wrapped_id); + dfcc_utilst::wrap_function(goto_model, function_id, wrapped_id); - const auto write_set_symbol = utils.create_new_parameter_symbol( + const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol( + goto_model.symbol_table, function_id, "__write_set_to_check", library.dfcc_type[dfcc_typet::CAR_SET_PTR]); @@ -311,7 +312,8 @@ void dfcc_swap_and_wrapt::replace_with_contract( function_pointer_contracts); body.add(goto_programt::make_end_function( - utils.get_function_symbol(wrapper_id).location)); + dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id) + .location)); goto_model.goto_functions.function_map.at(wrapper_id).make_hidden(); @@ -319,5 +321,5 @@ void dfcc_swap_and_wrapt::replace_with_contract( goto_model.goto_functions.function_map.at(function_id).body.swap(body); // extend the signature with the new write set parameter - utils.add_parameter(write_set_symbol, function_id); + dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h index 06987fbcf7e..391ea29db93 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h @@ -28,7 +28,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_spec_functions.h" -#include "dfcc_utils.h" #include #include @@ -45,7 +44,6 @@ class dfcc_swap_and_wrapt dfcc_swap_and_wrapt( goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_spec_functionst &spec_functions, @@ -88,7 +86,6 @@ class dfcc_swap_and_wrapt goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; dfcc_spec_functionst &spec_functions; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index f0a21c3b254..aab26a621c0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -13,7 +13,6 @@ Date: August 2022 #include #include #include -#include #include #include #include @@ -24,29 +23,21 @@ Date: August 2022 #include #include -#include #include #include -#include #include #include -dfcc_utilst::dfcc_utilst( - goto_modelt &goto_model, - message_handlert &message_handler) - : goto_model(goto_model), - message_handler(message_handler), - log(message_handler), - ns(goto_model.symbol_table) -{ -} - -const bool dfcc_utilst::symbol_exists( +/// Returns true iff the given symbol exists and satisfies requirements. +static bool symbol_exists( + const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available) { + const namespacet ns{goto_model.symbol_table}; + const symbolt *sym; if(ns.lookup(name, sym)) return false; @@ -64,27 +55,31 @@ const bool dfcc_utilst::symbol_exists( return true; } -const bool dfcc_utilst::function_symbol_exists(const irep_idt &function_id) +bool dfcc_utilst::function_symbol_exists( + const goto_modelt &goto_model, + const irep_idt &function_id) { - return symbol_exists(function_id, true, false); + return symbol_exists(goto_model, function_id, true, false); } -const bool -dfcc_utilst::function_symbol_with_body_exists(const irep_idt &function_id) +bool dfcc_utilst::function_symbol_with_body_exists( + const goto_modelt &goto_model, + const irep_idt &function_id) { - return symbol_exists(function_id, true, true); + return symbol_exists(goto_model, function_id, true, true); } -symbolt &dfcc_utilst::get_function_symbol(const irep_idt &function_id) +symbolt &dfcc_utilst::get_function_symbol( + symbol_table_baset &symbol_table, + const irep_idt &function_id) { - auto &symbol_table = goto_model.symbol_table; - PRECONDITION(symbol_table.has_symbol(function_id)); symbolt &function_symbol = symbol_table.get_writeable_ref(function_id); - PRECONDITION(function_symbol.type.id() == ID_code); + CHECK_RETURN(function_symbol.type.id() == ID_code); return function_symbol; } const symbolt &dfcc_utilst::create_symbol( + symbol_table_baset &symbol_table, const typet &type, const irep_idt &prefix, const irep_idt &base_name, @@ -99,7 +94,7 @@ const symbolt &dfcc_utilst::create_symbol( id2string(base_name), source_location, mode, - goto_model.symbol_table); + symbol_table); symbol.module = module; symbol.is_lvalue = true; symbol.is_state_var = true; @@ -111,6 +106,7 @@ const symbolt &dfcc_utilst::create_symbol( } const symbolt &dfcc_utilst::create_static_symbol( + symbol_table_baset &symbol_table, const typet &type, const irep_idt &prefix, const irep_idt &base_name, @@ -126,7 +122,7 @@ const symbolt &dfcc_utilst::create_static_symbol( id2string(base_name), source_location, mode, - goto_model.symbol_table); + symbol_table); symbol.module = module; symbol.is_static_lifetime = true; symbol.value = initial_value; @@ -140,44 +136,17 @@ const symbolt &dfcc_utilst::create_static_symbol( return symbol; } -void dfcc_utilst::fix_parameters_symbols(const irep_idt &function_id) -{ - auto &function_symbol = get_function_symbol(function_id); - auto &code_type = to_code_type(function_symbol.type); - // create parameter symbols - std::size_t anon_counter = 0; - for(auto &p : code_type.parameters()) - { - // may be anonymous - if(p.get_base_name().empty()) - { - p.set_base_name("#anon" + std::to_string(anon_counter++)); - } - - // produce identifier - const irep_idt &base_name = p.get_base_name(); - irep_idt parameter_identifier = - id2string(function_id) + "::" + id2string(base_name); - - p.set_identifier(parameter_identifier); - - if(!goto_model.symbol_table.has_symbol(p.get_identifier())) - { - create_new_parameter_symbol( - function_id, id2string(p.get_base_name()), p.type()); - } - } -} - const symbolt &dfcc_utilst::create_new_parameter_symbol( + symbol_table_baset &symbol_table, const irep_idt &function_id, const irep_idt &base_name, const typet &type) { - symbolt &function_symbol = get_function_symbol(function_id); + symbolt &function_symbol = get_function_symbol(symbol_table, function_id); // insert new parameter in the symbol table const symbolt &symbol = create_symbol( + symbol_table, type, id2string(function_id), base_name, @@ -188,7 +157,8 @@ const symbolt &dfcc_utilst::create_new_parameter_symbol( return symbol; } -void dfcc_utilst::add_parameter(const symbolt &symbol, code_typet &code_type) +/// \brief Adds the given symbol as parameter to the given code_typet. +static void add_parameter(const symbolt &symbol, code_typet &code_type) { PRECONDITION(symbol.is_parameter); code_typet::parametert parameter(symbol.type); @@ -199,78 +169,35 @@ void dfcc_utilst::add_parameter(const symbolt &symbol, code_typet &code_type) } void dfcc_utilst::add_parameter( + goto_modelt &goto_model, const symbolt &symbol, const irep_idt &function_id) { - PRECONDITION(symbol.is_parameter); - auto &function_symbol = get_function_symbol(function_id); + auto &function_symbol = + get_function_symbol(goto_model.symbol_table, function_id); code_typet &code_type = to_code_type(function_symbol.type); - add_parameter(symbol, code_type); + ::add_parameter(symbol, code_type); auto found = goto_model.goto_functions.function_map.find(function_id); if(found != goto_model.goto_functions.function_map.end()) found->second.set_parameter_identifiers(code_type); } const symbolt &dfcc_utilst::add_parameter( + goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &base_name, const typet &type) { - const symbolt &symbol = - create_new_parameter_symbol(function_id, base_name, type); - add_parameter(symbol, function_id); + const symbolt &symbol = create_new_parameter_symbol( + goto_model.symbol_table, function_id, base_name, type); + add_parameter(goto_model, symbol, function_id); return symbol; } -const symbolt &dfcc_utilst::clone_and_rename_function( - const irep_idt &function_id, - std::function &trans_fun, - std::function &trans_param, - std::function &trans_ret_type, - std::function &trans_loc) -{ - const symbolt &old_function_symbol = get_function_symbol(function_id); - code_typet old_code_type = to_code_type(old_function_symbol.type); - - irep_idt new_function_id = trans_fun(function_id); - - code_typet::parameterst new_params; - source_locationt new_location = trans_loc(old_function_symbol.location); - clone_parameters( - old_code_type.parameters(), - old_function_symbol.mode, - old_function_symbol.mode, - new_location, - trans_param, - new_function_id, - new_params); - - // build new function symbol - code_typet new_code_type( - new_params, trans_ret_type(old_code_type.return_type())); - symbolt new_function_symbol; - new_function_symbol.base_name = new_function_id; - new_function_symbol.name = new_function_id; - new_function_symbol.pretty_name = new_function_id; - new_function_symbol.type = new_code_type; - new_function_symbol.mode = old_function_symbol.mode; - new_function_symbol.module = old_function_symbol.module; - new_function_symbol.location = trans_loc(old_function_symbol.location); - new_function_symbol.set_compiled(); - - INVARIANT( - !goto_model.symbol_table.add(new_function_symbol), - "DFCC: renamed function " + id2string(new_function_id) + " already exists"); - - // create new goto_function - goto_functiont new_goto_function; - new_goto_function.set_parameter_identifiers(new_code_type); - goto_model.goto_functions.function_map[new_function_id].copy_from( - new_goto_function); - return goto_model.symbol_table.lookup_ref(new_function_id); -} - -void dfcc_utilst::clone_parameters( +/// \brief Clones the old_params into the new_params list, applying the +/// trans_param function to generate the names of the cloned params. +static void clone_parameters( + symbol_table_baset &symbol_table, const code_typet::parameterst &old_params, const irep_idt &mode, const irep_idt &module, @@ -309,7 +236,7 @@ void dfcc_utilst::clone_parameters( new_param_symbol.mode = mode; new_param_symbol.module = module; new_param_symbol.location = location; - bool add_failed = goto_model.symbol_table.add(new_param_symbol); + bool add_failed = symbol_table.add(new_param_symbol); INVARIANT( !add_failed, "DFCC: renamed parameter " + id2string(new_base_name) + @@ -317,7 +244,76 @@ void dfcc_utilst::clone_parameters( } } +/// \brief Creates a new symbol in the `symbol_table` by cloning +/// the given `function_id` function and transforming the existing +/// function's name, parameter names, return type and source location +/// using the given `trans_fun`, `trans_param` and `trans_ret_type` and +/// `trans_loc` functions. +/// +/// Also creates a new `goto_function` under the transformed name in +/// the `function_map` with new parameters and an empty body. +/// Returns the new symbol. +/// +/// \param goto_model: target goto_model holding the symbol table +/// \param function_id function to clone +/// \param trans_fun transformation function for the function name +/// \param trans_param transformation function for the parameter names +/// \param trans_ret_type transformation function for the return type +/// \param trans_loc transformation function for the source location +/// \return the new function symbol +static const symbolt &clone_and_rename_function( + goto_modelt &goto_model, + const irep_idt &function_id, + std::function &trans_fun, + std::function &trans_param, + std::function &trans_ret_type, + std::function &trans_loc) +{ + const symbolt &old_function_symbol = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id); + code_typet old_code_type = to_code_type(old_function_symbol.type); + + irep_idt new_function_id = trans_fun(function_id); + + code_typet::parameterst new_params; + source_locationt new_location = trans_loc(old_function_symbol.location); + clone_parameters( + goto_model.symbol_table, + old_code_type.parameters(), + old_function_symbol.mode, + old_function_symbol.mode, + new_location, + trans_param, + new_function_id, + new_params); + + code_typet new_code_type( + new_params, trans_ret_type(old_code_type.return_type())); + + // create new goto_function + goto_functiont new_goto_function; + new_goto_function.set_parameter_identifiers(new_code_type); + goto_model.goto_functions.function_map[new_function_id].copy_from( + new_goto_function); + + // build new function symbol + symbolt new_function_symbol{ + new_function_id, std::move(new_code_type), old_function_symbol.mode}; + new_function_symbol.base_name = new_function_id; + new_function_symbol.pretty_name = new_function_id; + new_function_symbol.module = old_function_symbol.module; + new_function_symbol.location = trans_loc(old_function_symbol.location); + new_function_symbol.set_compiled(); + + INVARIANT( + !goto_model.symbol_table.add(new_function_symbol), + "DFCC: renamed function " + id2string(new_function_id) + " already exists"); + + return goto_model.symbol_table.lookup_ref(new_function_id); +} + const symbolt &dfcc_utilst::clone_and_rename_function( + goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, optionalt new_return_type = {}) @@ -336,11 +332,12 @@ const symbolt &dfcc_utilst::clone_and_rename_function( std::function trans_loc = [&](const source_locationt &old_location) { return old_location; }; - return clone_and_rename_function( - function_id, trans_fun, trans_param, trans_ret_type, trans_loc); + return ::clone_and_rename_function( + goto_model, function_id, trans_fun, trans_param, trans_ret_type, trans_loc); } void dfcc_utilst::wrap_function( + goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id) { @@ -365,8 +362,7 @@ void dfcc_utilst::wrap_function( source_locationt sl(old_sym->location); sl.set_file("wrapped functions for code contracts"); sl.set_line("0"); - symbolt wrapped_sym; - wrapped_sym = *old_sym; + symbolt wrapped_sym = *old_sym; wrapped_sym.name = wrapped_function_id; wrapped_sym.base_name = wrapped_function_id; wrapped_sym.location = sl; @@ -377,8 +373,7 @@ void dfcc_utilst::wrap_function( " already exists in the symbol table"); // Re-insert a symbol for `function_id` which is now the wrapper function - symbolt wrapper_sym; - wrapper_sym = *old_sym; + symbolt wrapper_sym = *old_sym; std::function trans_param = [&](const irep_idt &old_param) { @@ -389,6 +384,7 @@ void dfcc_utilst::wrap_function( const auto &old_code_type = to_code_type(old_sym->type); code_typet::parameterst new_params; clone_parameters( + symbol_table, old_code_type.parameters(), wrapper_sym.mode, wrapper_sym.module, @@ -427,21 +423,23 @@ const exprt dfcc_utilst::make_null_check_expr(const exprt &ptr) return equal_exprt(ptr, null_pointer_exprt(to_pointer_type(ptr.type()))); } -exprt dfcc_utilst::make_sizeof_expr(const exprt &expr) +exprt dfcc_utilst::make_sizeof_expr(const exprt &expr, const namespacet &ns) { - const auto &size = - size_of_expr(expr.type(), namespacet(goto_model.symbol_table)); + const auto &size = size_of_expr(expr.type(), ns); if(!size.has_value()) { throw invalid_source_file_exceptiont( - "DFCC: no definite size for lvalue target" + from_expr(expr), + "DFCC: no definite size for lvalue target" + format_to_string(expr), expr.source_location()); } return size.value(); } -void dfcc_utilst::inline_function(const irep_idt &function_id) +static inlining_decoratort inline_function( + goto_modelt &goto_model, + const irep_idt &function_id, + message_handlert &message_handler) { auto &goto_function = goto_model.goto_functions.function_map.at(function_id); @@ -450,10 +448,22 @@ void dfcc_utilst::inline_function(const irep_idt &function_id) "dfcc_utilst::inline_function: '" + id2string(function_id) + "' must have a body"); - inlining_decoratort decorated(log.get_message_handler()); - namespacet ns{goto_model.symbol_table}; + const namespacet ns{goto_model.symbol_table}; + inlining_decoratort decorated(message_handler); goto_function_inline(goto_model.goto_functions, function_id, ns, decorated); + return decorated; +} + +void dfcc_utilst::inline_function( + goto_modelt &goto_model, + const irep_idt &function_id, + message_handlert &message_handler) +{ + inlining_decoratort decorated = + ::inline_function(goto_model, function_id, message_handler); + + messaget log{message_handler}; decorated.throw_on_recursive_calls(log, 0); decorated.throw_on_no_body(log, 0); decorated.throw_on_missing_function(log, 0); @@ -463,22 +473,17 @@ void dfcc_utilst::inline_function(const irep_idt &function_id) } void dfcc_utilst::inline_function( + goto_modelt &goto_model, const irep_idt &function_id, std::set &no_body, std::set &recursive_call, std::set &missing_function, - std::set ¬_enough_arguments) + std::set ¬_enough_arguments, + message_handlert &message_handler) { - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); + inlining_decoratort decorated = + ::inline_function(goto_model, function_id, message_handler); - PRECONDITION_WITH_DIAGNOSTICS( - goto_function.body_available(), - "dfcc_utilst::inline_function: '" + id2string(function_id) + - "' must have a body"); - - inlining_decoratort decorated(log.get_message_handler()); - namespacet ns{goto_model.symbol_table}; - goto_function_inline(goto_model.goto_functions, function_id, ns, decorated); no_body.insert( decorated.get_no_body_set().begin(), decorated.get_no_body_set().end()); recursive_call.insert( @@ -490,30 +495,21 @@ void dfcc_utilst::inline_function( not_enough_arguments.insert( decorated.get_not_enough_arguments_set().begin(), decorated.get_not_enough_arguments_set().end()); - goto_model.goto_functions.update(); -} -void dfcc_utilst::inline_program(goto_programt &program) -{ - inlining_decoratort decorated(log.get_message_handler()); - namespacet ns{goto_model.symbol_table}; - goto_program_inline(goto_model.goto_functions, program, ns, decorated); - - decorated.throw_on_recursive_calls(log, 0); - decorated.throw_on_no_body(log, 0); - decorated.throw_on_missing_function(log, 0); - decorated.throw_on_not_enough_arguments(log, 0); + goto_model.goto_functions.update(); } void dfcc_utilst::inline_program( + goto_modelt &goto_model, goto_programt &goto_program, std::set &no_body, std::set &recursive_call, std::set &missing_function, - std::set ¬_enough_arguments) + std::set ¬_enough_arguments, + message_handlert &message_handler) { - inlining_decoratort decorated(log.get_message_handler()); - namespacet ns{goto_model.symbol_table}; + const namespacet ns{goto_model.symbol_table}; + inlining_decoratort decorated(message_handler); goto_program_inline(goto_model.goto_functions, goto_program, ns, decorated); no_body.insert( decorated.get_no_body_set().begin(), decorated.get_no_body_set().end()); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 36aee99ee26..b60f998cc69 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -24,35 +24,25 @@ class goto_programt; class message_handlert; class symbolt; -class dfcc_utilst +struct dfcc_utilst { -public: - dfcc_utilst(goto_modelt &goto_model, message_handlert &message_handler); - -protected: - goto_modelt &goto_model; - message_handlert &message_handler; - messaget log; - namespacet ns; - -public: /// Returns true iff the given symbol exists and satisfies requirements. - const bool symbol_exists( - const irep_idt &function_id, - const bool require_has_code_type = false, - const bool require_body_available = false); - - const bool function_symbol_exists(const irep_idt &function_id); - const bool function_symbol_with_body_exists(const irep_idt &function_id); + static bool + function_symbol_exists(const goto_modelt &, const irep_idt &function_id); + static bool function_symbol_with_body_exists( + const goto_modelt &, + const irep_idt &function_id); /// Returns the `symbolt` for `function_id`. - symbolt &get_function_symbol(const irep_idt &function_id); + static symbolt & + get_function_symbol(symbol_table_baset &, const irep_idt &function_id); /// Adds a new symbol named `prefix::base_name` of type `type` /// with given attributes in the symbol table, and returns the created symbol. /// If a symbol of the same name already exists the name will be decorated /// with a unique suffix. - const symbolt &create_symbol( + static const symbolt &create_symbol( + symbol_table_baset &, const typet &type, const irep_idt &prefix, const irep_idt &base_name, @@ -72,7 +62,8 @@ class dfcc_utilst /// keep their initial values for the instrumentation to work as intended. /// To allow nondet-initialisation of the symbol, /// just set \p no_nondet_initialization to `false` when calling the method. - const symbolt &create_static_symbol( + static const symbolt &create_static_symbol( + symbol_table_baset &, const typet &type, const irep_idt &prefix, const irep_idt &base_name, @@ -83,7 +74,8 @@ class dfcc_utilst const bool no_nondet_initialization = true); /// Creates a new parameter symbol for the given function_id - const symbolt &create_new_parameter_symbol( + static const symbolt &create_new_parameter_symbol( + symbol_table_baset &, const irep_idt &function_id, const irep_idt &base_name, const typet &type); @@ -91,64 +83,27 @@ class dfcc_utilst /// \brief Adds the given symbol as parameter to the function symbol's /// code_type. Also adds the corresponding parameter to its goto_function if /// it exists in the function map of the goto model. - void add_parameter(const symbolt &symbol, const irep_idt &function_id); - - /// \brief Adds the given symbol as parameter to the given code_typet. - void add_parameter(const symbolt &symbol, code_typet &code_type); + static void add_parameter( + goto_modelt &, + const symbolt &symbol, + const irep_idt &function_id); /// \brief Adds a parameter with given `base_name` and `type` to the given /// `function_id`. Both the symbol and the goto_function are updated. - const symbolt &add_parameter( + static const symbolt &add_parameter( + goto_modelt &, const irep_idt &function_id, const irep_idt &base_name, const typet &type); - /// \brief Creates a new symbol in the `symbol_table` by cloning - /// the given `function_id` function and transforming the existing's - /// function's name, parameter names, return type and source location - /// using the given `trans_fun`, `trans_param` and `trans_ret_type` and - /// `trans_loc` functions. - /// - /// Also creates a new `goto_function` under the transformed name in - /// the `function_map` with new parameters and an empty body. - /// Returns the new symbol. - /// - /// \param function_id function to clone - /// \param trans_fun transformation function for the function name - /// \param trans_param transformation function for the parameter names - /// \param trans_ret_type transformation function for the return type - /// \param trans_loc transformation function for the source location - /// \return the new function symbol - const symbolt &clone_and_rename_function( - const irep_idt &function_id, - std::function &trans_fun, - std::function &trans_param, - std::function &trans_ret_type, - std::function &trans_loc); - - /// \brief Clones the old_params into the new_params list, applying the - /// trans_param function to generate the names of the cloned params. - void clone_parameters( - const code_typet::parameterst &old_params, - const irep_idt &mode, - const irep_idt &module, - const source_locationt &location, - std::function &trans_param, - const irep_idt &new_function_id, - code_typet::parameterst &new_params); - - /// \brief Creates names for anonymous parameters and declares them - /// in the symbol table if needed (using goto_convert requires all function - /// parameters to have names). - void fix_parameters_symbols(const irep_idt &function_id); - - /// \brief Creates a new function symbol and and goto_function + /// \brief Creates a new function symbol and goto_function /// entry in the `goto_functions_map` by cloning the given `function_id`. /// /// The cloned function symbol has `new_function_id` as name /// The cloned parameters symbols have `new_function_id::name` as name /// Returns the new function symbol - const symbolt &clone_and_rename_function( + static const symbolt &clone_and_rename_function( + goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, optionalt new_return_type); @@ -181,41 +136,45 @@ class dfcc_utilst /// /// By generating a new body for `foo`, one can implement contract /// checking logic, contract replacement logic, etc. - void wrap_function( + static void wrap_function( + goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id); /// \brief Returns the expression `expr == NULL`. - const exprt make_null_check_expr(const exprt &ptr); + static const exprt make_null_check_expr(const exprt &ptr); /// \brief Returns the expression `sizeof(expr)`. - exprt make_sizeof_expr(const exprt &expr); + static exprt make_sizeof_expr(const exprt &expr, const namespacet &); /// \brief Inlines the given function, aborts on recursive calls during /// inlining. - void inline_function(const irep_idt &function_id); + static void inline_function( + goto_modelt &goto_model, + const irep_idt &function_id, + message_handlert &message_handler); /// \brief Inlines the given function, and returns function symbols that /// caused warnings. - void inline_function( + static void inline_function( + goto_modelt &goto_model, const irep_idt &function_id, std::set &no_body, std::set &recursive_call, std::set &missing_function, - std::set ¬_enough_arguments); - - /// \brief Inlines the given program, aborts on recursive calls during - /// inlining. - void inline_program(goto_programt &program); + std::set ¬_enough_arguments, + message_handlert &message_handler); /// \brief Inlines the given program, and returns function symbols that /// caused warnings. - void inline_program( + static void inline_program( + goto_modelt &goto_model, goto_programt &goto_program, std::set &no_body, std::set &recursive_call, std::set &missing_function, - std::set ¬_enough_arguments); + std::set ¬_enough_arguments, + message_handlert &message_handler); }; #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index ab39b874757..70648724a55 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -31,146 +31,146 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_utils.h" /// Generate the contract write set -const symbol_exprt create_contract_write_set( - dfcc_utilst &utils, +static symbol_exprt create_contract_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET], - id2string(wrapper_symbol.name), - "__contract_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + id2string(wrapper_symbol.name), + "__contract_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate the contract write set pointer -const symbol_exprt create_addr_of_contract_write_set( - dfcc_utilst &utils, +static symbol_exprt create_addr_of_contract_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET_PTR], - id2string(wrapper_symbol.name), - "__address_of_contract_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + id2string(wrapper_symbol.name), + "__address_of_contract_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } // Generate the write set to check for side effects in requires clauses -const symbol_exprt create_requires_write_set( - dfcc_utilst &utils, +static symbol_exprt create_requires_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET], - id2string(wrapper_symbol.name), - "__requires_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + id2string(wrapper_symbol.name), + "__requires_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate the write set pointer to check side effects in requires clauses -const symbol_exprt create_addr_of_requires_write_set( - dfcc_utilst &utils, +static symbol_exprt create_addr_of_requires_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET_PTR], - id2string(wrapper_symbol.name), - "__address_of_requires_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + id2string(wrapper_symbol.name), + "__address_of_requires_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate the write set to check side effects in ensures clauses -const symbol_exprt create_ensures_write_set( - dfcc_utilst &utils, +static symbol_exprt create_ensures_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET], - id2string(wrapper_symbol.name), - "__ensures_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + id2string(wrapper_symbol.name), + "__ensures_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate the write set pointer to check side effects in ensures clauses -const symbol_exprt create_addr_of_ensures_write_set( - dfcc_utilst &utils, +static symbol_exprt create_addr_of_ensures_write_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET_PTR], - id2string(wrapper_symbol.name), - "__address_of_ensures_write_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + id2string(wrapper_symbol.name), + "__address_of_ensures_write_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate object set used to support is_fresh predicates -const symbol_exprt create_is_fresh_set( - dfcc_utilst &utils, +static symbol_exprt create_is_fresh_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::OBJ_SET], - id2string(wrapper_symbol.name), - "__is_fresh_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::OBJ_SET], + id2string(wrapper_symbol.name), + "__is_fresh_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } /// Generate object set pointer used to support is_fresh predicates -const symbol_exprt create_addr_of_is_fresh_set( - dfcc_utilst &utils, +static symbol_exprt create_addr_of_is_fresh_set( + symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) { - return utils - .create_symbol( - library.dfcc_type[dfcc_typet::OBJ_SET_PTR], - id2string(wrapper_symbol.name), - "__address_of_is_fresh_set", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::OBJ_SET_PTR], + id2string(wrapper_symbol.name), + "__address_of_is_fresh_set", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); } @@ -182,7 +182,6 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates) @@ -195,25 +194,40 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( caller_write_set(caller_write_set_symbol.symbol_expr()), wrapper_sl(wrapper_symbol.location), return_value_opt(), - contract_write_set( - create_contract_write_set(utils, library, wrapper_symbol)), - addr_of_contract_write_set( - create_addr_of_contract_write_set(utils, library, wrapper_symbol)), - requires_write_set( - create_requires_write_set(utils, library, wrapper_symbol)), - addr_of_requires_write_set( - create_addr_of_requires_write_set(utils, library, wrapper_symbol)), - ensures_write_set(create_ensures_write_set(utils, library, wrapper_symbol)), - addr_of_ensures_write_set( - create_addr_of_ensures_write_set(utils, library, wrapper_symbol)), - is_fresh_set(create_is_fresh_set(utils, library, wrapper_symbol)), - addr_of_is_fresh_set( - create_addr_of_is_fresh_set(utils, library, wrapper_symbol)), + contract_write_set(create_contract_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + addr_of_contract_write_set(create_addr_of_contract_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + requires_write_set(create_requires_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + addr_of_requires_write_set(create_addr_of_requires_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + ensures_write_set(create_ensures_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + addr_of_ensures_write_set(create_addr_of_ensures_write_set( + goto_model.symbol_table, + library, + wrapper_symbol)), + is_fresh_set( + create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)), + addr_of_is_fresh_set(create_addr_of_is_fresh_set( + goto_model.symbol_table, + library, + wrapper_symbol)), function_pointer_contracts(), goto_model(goto_model), message_handler(message_handler), log(message_handler), - utils(utils), library(library), instrument(instrument), memory_predicates(memory_predicates), @@ -223,15 +237,15 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( // generate a return value symbol (needed to instantiate all contract lambdas) if(contract_code_type.return_type().id() != ID_empty) { - return_value_opt = utils - .create_symbol( - contract_code_type.return_type(), - id2string(wrapper_symbol.name), - "__contract_return_value", - wrapper_symbol.location, - wrapper_symbol.mode, - wrapper_symbol.module, - false) + return_value_opt = dfcc_utilst::create_symbol( + goto_model.symbol_table, + contract_code_type.return_type(), + id2string(wrapper_symbol.name), + "__contract_return_value", + wrapper_symbol.location, + wrapper_symbol.mode, + wrapper_symbol.module, + false) .symbol_expr(); // build contract_lambda_parameters @@ -566,7 +580,8 @@ void dfcc_wrapper_programt::encode_requires_clauses() // we use this empty requires write set to check for the absence of side // effects in the requires clauses const auto &wrapper_id = wrapper_symbol.name; - const auto &language_mode = utils.get_function_symbol(wrapper_id).mode; + const auto &language_mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id).mode; // if in replacement mode, check that assertions hold in the current context, // otherwise assume @@ -739,7 +754,7 @@ void dfcc_wrapper_programt::encode_havoced_function_call() auto goto_instruction = write_set_checks.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(caller_write_set), wrapper_sl)); + dfcc_utilst::make_null_check_expr(caller_write_set), wrapper_sl)); { // assigns clause inclusion diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index 6bfb51432fb..09ff311dbfa 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -31,7 +31,6 @@ class message_handlert; class dfcc_instrumentt; class dfcc_libraryt; class dfcc_lift_memory_predicatest; -class dfcc_utilst; class code_with_contract_typet; class conditional_target_group_exprt; @@ -106,7 +105,6 @@ class dfcc_wrapper_programt /// to the wrapper function by its caller. /// \param goto_model the goto model being transformed /// \param message_handler used for debug/warning/error messages - /// \param utils utility functions for contracts transformation /// \param library the contracts instrumentation library /// \param instrument the instrumenter class for goto functions/goto programs /// \param memory_predicates handler for user-defed memory predicates, used to @@ -120,7 +118,6 @@ class dfcc_wrapper_programt const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, - dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates); @@ -175,7 +172,6 @@ class dfcc_wrapper_programt goto_modelt &goto_model; message_handlert &message_handler; messaget log; - dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; dfcc_lift_memory_predicatest &memory_predicates;