From 9ca2e6649ff02cfd57e0ec4ef2de4dba5d5787b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 May 2023 11:30:23 +0000 Subject: [PATCH] Code contracts: cleanup get_fresh_aux_symbol wrappers 1. Consistently either use the wrappers or get_fresh_aux_symbol directly. 2. Remove wrappers that did not yield significant simplification. 3. Make remaining wrappers do all work that was previously done by each caller. --- src/goto-instrument/contracts/contracts.cpp | 59 ++++-- .../dynamic-frames/dfcc_cfg_info.cpp | 32 ++- .../dynamic-frames/dfcc_instrument.cpp | 89 +++------ .../dynamic-frames/dfcc_instrument_loop.cpp | 99 +++------- .../dynamic-frames/dfcc_instrument_loop.h | 4 +- .../dynamic-frames/dfcc_spec_functions.cpp | 46 ++--- .../dynamic-frames/dfcc_spec_functions.h | 4 - .../contracts/dynamic-frames/dfcc_utils.cpp | 63 +++--- .../contracts/dynamic-frames/dfcc_utils.h | 24 ++- .../dynamic-frames/dfcc_wrapper_program.cpp | 183 +++++++----------- .../contracts/instrument_spec_assigns.cpp | 31 +-- .../contracts/instrument_spec_assigns.h | 7 - .../contracts/memory_predicates.cpp | 17 +- src/goto-instrument/contracts/utils.cpp | 29 ++- src/goto-instrument/contracts/utils.h | 17 -- 15 files changed, 281 insertions(+), 423 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index e23cd3de23e..929dc8382a6 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -139,12 +139,13 @@ void code_contractst::check_apply_loop_contracts( // Create a temporary to track if we entered the loop, // i.e., the loop guard was satisfied. const auto entered_loop = - new_tmp_symbol( + get_fresh_aux_symbol( bool_typet(), + id2string(loop_head_location.get_function()), + std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number), loop_head_location, mode, - symbol_table, - std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number)) + symbol_table) .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(entered_loop, loop_head_location)); @@ -154,8 +155,13 @@ void code_contractst::check_apply_loop_contracts( // Create a snapshot of the invariant so that we can check the base case, // if the loop is not vacuous and must be abstracted with contracts. const auto initial_invariant_val = - new_tmp_symbol( - bool_typet(), loop_head_location, mode, symbol_table, INIT_INVARIANT) + get_fresh_aux_symbol( + bool_typet(), + id2string(loop_head_location.get_function()), + INIT_INVARIANT, + loop_head_location, + mode, + symbol_table) .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(initial_invariant_val, loop_head_location)); @@ -173,10 +179,14 @@ void code_contractst::check_apply_loop_contracts( // Create a temporary variable to track base case vs inductive case // instrumentation of the loop. - const auto in_base_case = - new_tmp_symbol( - bool_typet(), loop_head_location, mode, symbol_table, "__in_base_case") - .symbol_expr(); + const auto in_base_case = get_fresh_aux_symbol( + bool_typet(), + id2string(loop_head_location.get_function()), + "__in_base_case", + loop_head_location, + mode, + symbol_table) + .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(in_base_case, loop_head_location)); pre_loop_head_instrs.add( @@ -298,12 +308,13 @@ void code_contractst::check_apply_loop_contracts( // havoc (assigns_set); // ASSIGN in_loop_havoc_block = false; const auto in_loop_havoc_block = - new_tmp_symbol( + get_fresh_aux_symbol( bool_typet(), + id2string(loop_head_location.get_function()), + std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number), loop_head_location, mode, - symbol_table, - std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number)) + symbol_table) .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(in_loop_havoc_block, loop_head_location)); @@ -335,14 +346,26 @@ void code_contractst::check_apply_loop_contracts( for(const auto &clause : decreases_clause.operands()) { const auto old_decreases_var = - new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table) + get_fresh_aux_symbol( + clause.type(), + id2string(loop_head_location.get_function()), + "tmp_cc", + loop_head_location, + mode, + symbol_table) .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(old_decreases_var, loop_head_location)); old_decreases_vars.push_back(old_decreases_var); const auto new_decreases_var = - new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table) + get_fresh_aux_symbol( + clause.type(), + id2string(loop_head_location.get_function()), + "tmp_cc", + loop_head_location, + mode, + symbol_table) .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(new_decreases_var, loop_head_location)); @@ -1251,8 +1274,10 @@ void code_contractst::add_contract_check( optionalt return_stmt; if(code_type.return_type() != empty_typet()) { - symbol_exprt r = new_tmp_symbol( + symbol_exprt r = get_fresh_aux_symbol( code_type.return_type(), + id2string(source_location.get_function()), + "tmp_cc", source_location, function_symbol.mode, symbol_table) @@ -1275,8 +1300,10 @@ void code_contractst::add_contract_check( { PRECONDITION(!parameter.empty()); const symbolt ¶meter_symbol = ns.lookup(parameter); - symbol_exprt p = new_tmp_symbol( + symbol_exprt p = get_fresh_aux_symbol( parameter_symbol.type, + id2string(source_location.get_function()), + "tmp_cc", source_location, parameter_symbol.mode, symbol_table) 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 bfa1569d32e..29826a21b73 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -471,30 +471,22 @@ 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 = - dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; // Generate "write set" variable - const auto &write_set_var = - get_fresh_aux_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET], - id2string(function_id), - "__write_set_loop_" + std::to_string(cbmc_loop_number), - loop.head->source_location(), - language_mode, - symbol_table) - .symbol_expr(); + const auto write_set_var = dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + function_id, + "__write_set_loop_" + std::to_string(cbmc_loop_number), + loop.head->source_location()); // Generate "address of write set" variable - const auto &addr_of_write_set_var = - get_fresh_aux_symbol( - library.dfcc_type[dfcc_typet::WRITE_SET_PTR], - id2string(function_id), - "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number), - loop.head->source_location(), - language_mode, - symbol_table) - .symbol_expr(); + const auto &addr_of_write_set_var = dfcc_utilst::create_symbol( + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + function_id, + "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number), + loop.head->source_location()); return { loop_id, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 244497014aa..3c072519701 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -256,16 +256,12 @@ void dfcc_instrumentt::instrument_harness_function( // create a local write set symbol 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(); + 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); std::set local_statics = get_local_statics(function_id); @@ -663,7 +659,7 @@ void dfcc_instrumentt::instrument_lhs( goto_programt &goto_program, dfcc_cfg_infot &cfg_info) { - const auto &mode = + const irep_idt &mode = dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; goto_programt payload; @@ -691,18 +687,12 @@ void dfcc_instrumentt::instrument_lhs( // ASSIGN lhs := rhs; // ``` - auto &check_sym = dfcc_utilst::create_symbol( + const auto check_var = dfcc_utilst::create_symbol( goto_model.symbol_table, bool_typet(), - id2string(function_id), + function_id, "__check_lhs_assignment", - lhs_source_location, - mode, - dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) - .module, - false); - - const auto &check_var = check_sym.symbol_expr(); + lhs_source_location); payload.add(goto_programt::make_decl(check_var, lhs_source_location)); @@ -950,22 +940,17 @@ void dfcc_instrumentt::instrument_deallocate_call( // ---- // CALL __CPROVER_deallocate(ptr); // ``` - 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( dfcc_utilst::make_null_check_expr(write_set), target_location)); - auto &check_sym = get_fresh_aux_symbol( + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, bool_typet(), - id2string(function_id), + function_id, "__check_deallocate", - target_location, - mode, - goto_model.symbol_table); - - const auto &check_var = check_sym.symbol_expr(); + target_location); payload.add(goto_programt::make_decl(check_var, target_location)); @@ -977,6 +962,8 @@ void dfcc_instrumentt::instrument_deallocate_call( target_location)); // add property class on assertion source_location + const irep_idt &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; source_locationt check_location(target_location); check_location.set_property_class("frees"); std::string comment = @@ -1040,6 +1027,8 @@ void dfcc_instrumentt::instrument_other( const auto &target_location = target->source_location(); auto &statement = target->get_other().get_statement(); auto &write_set = cfg_info.get_write_set(target); + const irep_idt &mode = + dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode; if(statement == ID_array_set || statement == ID_array_copy) { @@ -1054,23 +1043,17 @@ void dfcc_instrumentt::instrument_other( // ---- // OTHER {statement = array_set, args = {dest, value}}; // ``` - 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( dfcc_utilst::make_null_check_expr(write_set), target_location)); - auto &check_sym = get_fresh_aux_symbol( + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, bool_typet(), - id2string(function_id), + function_id, is_array_set ? "__check_array_set" : "__check_array_copy", - target_location, - mode, - goto_model.symbol_table); - - const auto &check_var = check_sym.symbol_expr(); + target_location); payload.add(goto_programt::make_decl(check_var, target_location)); @@ -1115,23 +1098,17 @@ void dfcc_instrumentt::instrument_other( // ---- // OTHER {statement = array_replace, args = {dest, src}}; // ``` - 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( dfcc_utilst::make_null_check_expr(write_set), target_location)); - auto &check_sym = get_fresh_aux_symbol( + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, bool_typet(), - id2string(function_id), + function_id, "__check_array_replace", - target_location, - mode, - goto_model.symbol_table); - - const auto &check_var = check_sym.symbol_expr(); + target_location); payload.add(goto_programt::make_decl(check_var, target_location)); @@ -1170,23 +1147,17 @@ void dfcc_instrumentt::instrument_other( // ASSERT(check_havoc_object); // DEAD check_havoc_object; // ``` - 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( dfcc_utilst::make_null_check_expr(write_set), target_location)); - auto &check_sym = get_fresh_aux_symbol( + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, bool_typet(), - id2string(function_id), + function_id, "__check_havoc_object", - target_location, - mode, - goto_model.symbol_table); - - const auto &check_var = check_sym.symbol_expr(); + target_location); payload.add(goto_programt::make_decl(check_var, target_location)); 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 82b45843d24..5a91b122b43 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -50,8 +50,6 @@ 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 = - 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()); @@ -60,37 +58,22 @@ void dfcc_instrument_loopt::operator()( // Temporary variables: // Create a temporary to track if we entered the loop, // i.e., the loop guard was satisfied. - const auto entered_loop = - get_fresh_aux_symbol( - bool_typet(), - id2string(function_id), - std::string(ENTERED_LOOP) + "__" + std::to_string(cbmc_loop_id), - head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto entered_loop = dfcc_utilst::create_symbol( + symbol_table, + bool_typet(), + function_id, + std::string(ENTERED_LOOP) + "__" + std::to_string(cbmc_loop_id), + head_location); // Create a snapshot of the invariant so that we can check the base case, // if the loop is not vacuous and must be abstracted with contracts. - const auto initial_invariant = get_fresh_aux_symbol( - bool_typet(), - id2string(function_id), - INIT_INVARIANT, - head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto initial_invariant = dfcc_utilst::create_symbol( + symbol_table, bool_typet(), function_id, INIT_INVARIANT, head_location); // Create a temporary variable to track base case vs inductive case // instrumentation of the loop. - const auto in_base_case = get_fresh_aux_symbol( - bool_typet(), - id2string(function_id), - IN_BASE_CASE, - head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto in_base_case = dfcc_utilst::create_symbol( + symbol_table, bool_typet(), function_id, IN_BASE_CASE, head_location); // Temporary variables for storing the multidimensional decreases clause // at the start of and end of a loop body. @@ -99,24 +82,12 @@ void dfcc_instrument_loopt::operator()( for(const auto &clause : decreases_clauses) { // old - const auto old_decreases_var = get_fresh_aux_symbol( - clause.type(), - id2string(function_id), - "tmp_cc", - head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto old_decreases_var = dfcc_utilst::create_symbol( + symbol_table, clause.type(), function_id, "tmp_cc", head_location); old_decreases_vars.push_back(old_decreases_var); // new - const auto new_decreases_var = get_fresh_aux_symbol( - clause.type(), - id2string(function_id), - "tmp_cc", - head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto new_decreases_var = dfcc_utilst::create_symbol( + symbol_table, clause.type(), function_id, "tmp_cc", head_location); new_decreases_vars.push_back(new_decreases_var); } @@ -137,6 +108,8 @@ void dfcc_instrument_loopt::operator()( // in the result __CPROVER_contracts_write_set_t should be the set of CAR // of the loop assign targets. goto_programt write_set_populate_instrs; + const irep_idt &language_mode = + dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; contract_clauses_codegen.gen_spec_assigns_instructions( language_mode, assigns, write_set_populate_instrs); @@ -146,8 +119,6 @@ void dfcc_instrument_loopt::operator()( spec_functions.generate_havoc_instructions( function_id, - language_mode, - symbol_table.get_writeable_ref(function_id).module, write_set_populate_instrs, loop.addr_of_write_set_var, havoc_instrs, @@ -198,8 +169,7 @@ void dfcc_instrument_loopt::operator()( outer_write_set, initial_invariant, in_base_case, - old_decreases_vars, - language_mode); + old_decreases_vars); add_body_instructions( loop_id, @@ -365,8 +335,7 @@ dfcc_instrument_loopt::add_step_instructions( const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, - const std::vector &old_decreases_vars, - const irep_idt &language_mode) + const std::vector &old_decreases_vars) { auto loop_head_location(loop_head->source_location()); dfcc_remove_loop_tags(loop_head_location); @@ -414,15 +383,12 @@ dfcc_instrument_loopt::add_step_instructions( null_pointer_exprt(to_pointer_type(outer_write_set.type()))), loop_head_location)); - auto check_var = - get_fresh_aux_symbol( - bool_typet(), - id2string(function_id), - "__check_assigns_clause_incl_loop_" + std::to_string(cbmc_loop_id), - loop_head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto check_var = dfcc_utilst::create_symbol( + symbol_table, + bool_typet(), + function_id, + "__check_assigns_clause_incl_loop_" + std::to_string(cbmc_loop_id), + loop_head_location); step_instrs.add(goto_programt::make_decl(check_var, loop_head_location)); step_instrs.add(goto_programt::make_function_call( @@ -446,15 +412,12 @@ dfcc_instrument_loopt::add_step_instructions( { // Generate havocing code for assigns targets. - const auto in_loop_havoc_block = - get_fresh_aux_symbol( - bool_typet(), - id2string(function_id), - std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(cbmc_loop_id), - loop_head_location, - language_mode, - symbol_table) - .symbol_expr(); + const auto in_loop_havoc_block = dfcc_utilst::create_symbol( + symbol_table, + bool_typet(), + function_id, + std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(cbmc_loop_id), + loop_head_location); step_instrs.add( goto_programt::make_decl(in_loop_havoc_block, loop_head_location)); step_instrs.add( @@ -465,6 +428,8 @@ dfcc_instrument_loopt::add_step_instructions( } goto_convertt converter(symbol_table, log.get_message_handler()); + const irep_idt &language_mode = + dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; { // Assume the loop invariant after havocing the state. code_assumet assumption{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 64ce8674b57..523aeb1fdca 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -240,7 +240,6 @@ class dfcc_instrument_loopt /// \param[in] initial_invariant temporary variable `initial_invariant`. /// \param[in] in_base_case temporary variable `in_base_case`. /// \param[in] old_decreases_vars temporary vars of decreases clauses. - /// \param[in] symbol_mode Language mode of the function. /// \return The STEP jump target. goto_programt::instructiont::targett add_step_instructions( const std::size_t loop_id, @@ -257,8 +256,7 @@ class dfcc_instrument_loopt const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, - const std::vector &old_decreases_vars, - const irep_idt &symbol_mode); + const std::vector &old_decreases_vars); /// \brief Adds instructions of the body block. /// 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 df28667317e..9c4e666f1b0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -54,22 +54,11 @@ void dfcc_spec_functionst::generate_havoc_function( 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 = dfcc_utilst::create_symbol( - goto_model.symbol_table, - library.dfcc_type[dfcc_typet::CAR_SET_PTR], - id2string(havoc_function_id), - "__write_set_to_havoc", - function_symbol.location, - function_symbol.mode, - function_symbol.module, - true); - // create the code type that goes on the function symbol - code_typet::parametert write_set_param(write_set_symbol.type); - write_set_param.set_base_name(write_set_symbol.base_name); - write_set_param.set_identifier(write_set_symbol.name); - code_typet havoc_code_type({write_set_param}, empty_typet()); + const typet &write_set_param_type = + library.dfcc_type[dfcc_typet::CAR_SET_PTR]; + code_typet::parametert write_set_param{write_set_param_type}; + code_typet havoc_code_type({std::move(write_set_param)}, empty_typet()); // create the havoc function symbol symbolt havoc_function_symbol; @@ -87,9 +76,20 @@ void dfcc_spec_functionst::generate_havoc_function( "DFCC: could not insert havoc function '" + id2string(havoc_function_id) + "' in the symbol table"); + // create the write_set symbol used as input by the havoc function + const auto &write_set_symbol = dfcc_utilst::create_new_parameter_symbol( + goto_model.symbol_table, + havoc_function_id, + "__write_set_to_havoc", + write_set_param_type); + to_code_type( + goto_model.symbol_table.get_writeable_ref(havoc_function_id).type) + .parameters()[0] + .set_identifier(write_set_symbol.name); + // create new goto_function goto_functiont dummy_havoc_function; - dummy_havoc_function.set_parameter_identifiers(havoc_code_type); + dummy_havoc_function.parameter_identifiers = {write_set_symbol.name}; goto_model.goto_functions.function_map[havoc_function_id].copy_from( dummy_havoc_function); @@ -102,8 +102,6 @@ void dfcc_spec_functionst::generate_havoc_function( generate_havoc_instructions( havoc_function_id, - havoc_function_symbol.mode, - havoc_function_symbol.module, original_program, write_set_symbol.symbol_expr(), havoc_program, @@ -145,8 +143,6 @@ void dfcc_spec_functionst::generate_havoc_function( void dfcc_spec_functionst::generate_havoc_instructions( const irep_idt &function_id, - const irep_idt &mode, - const irep_idt &module, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, @@ -202,17 +198,13 @@ 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 = dfcc_utilst::create_symbol( + const auto target_expr = dfcc_utilst::create_symbol( goto_model.symbol_table, pointer_type(target_type), - id2string(function_id), + function_id, "__havoc_target", - location, - mode, - module, - false); + location); - auto target_expr = target_symbol.symbol_expr(); havoc_program.add(goto_programt::make_decl(target_expr)); call.lhs() = target_expr; 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 cbd89910e32..e75f025f800 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -87,8 +87,6 @@ class dfcc_spec_functionst /// write set \p write_set_to_havoc. /// /// \param[in] function_id function id to use for prefixing fresh variables - /// \param[in] mode function id to use for prefixing fresh variables - /// \param[in] module function id to use for prefixing fresh variables /// \param[in] original_program program from which to derive the havoc program /// \param[in] write_set_to_havoc write set symbol to havoc /// \param[out] havoc_program destination program for havoc instructions @@ -96,8 +94,6 @@ class dfcc_spec_functionst /// void generate_havoc_instructions( const irep_idt &function_id, - const irep_idt &mode, - const irep_idt &module, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index aab26a621c0..703515a5ead 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -78,38 +78,33 @@ symbolt &dfcc_utilst::get_function_symbol( return function_symbol; } -const symbolt &dfcc_utilst::create_symbol( +symbol_exprt dfcc_utilst::create_symbol( symbol_table_baset &symbol_table, const typet &type, - const irep_idt &prefix, - const irep_idt &base_name, - const source_locationt &source_location, - const irep_idt &mode, - const irep_idt &module, - bool is_parameter) + const irep_idt &function_id, + const std::string &base_name, + const source_locationt &source_location) { + const symbolt &function_symbol = + get_function_symbol(symbol_table, function_id); + symbolt &symbol = get_fresh_aux_symbol( type, - id2string(prefix), - id2string(base_name), + id2string(function_id), + base_name, source_location, - mode, + function_symbol.mode, symbol_table); - symbol.module = module; - symbol.is_lvalue = true; - symbol.is_state_var = true; - symbol.is_thread_local = true; - symbol.is_file_local = true; - symbol.is_auxiliary = true; - symbol.is_parameter = is_parameter; - return symbol; + symbol.module = function_symbol.module; + + return symbol.symbol_expr(); } const symbolt &dfcc_utilst::create_static_symbol( symbol_table_baset &symbol_table, const typet &type, - const irep_idt &prefix, - const irep_idt &base_name, + const std::string &prefix, + const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, @@ -117,21 +112,11 @@ const symbolt &dfcc_utilst::create_static_symbol( const bool no_nondet_initialization) { symbolt &symbol = get_fresh_aux_symbol( - type, - id2string(prefix), - id2string(base_name), - source_location, - mode, - symbol_table); + type, prefix, base_name, source_location, mode, symbol_table); symbol.module = module; symbol.is_static_lifetime = true; symbol.value = initial_value; symbol.value.set(ID_C_no_nondet_initialization, no_nondet_initialization); - symbol.is_lvalue = true; - symbol.is_state_var = true; - symbol.is_thread_local = true; - symbol.is_file_local = true; - symbol.is_auxiliary = true; symbol.is_parameter = false; return symbol; } @@ -139,21 +124,21 @@ const symbolt &dfcc_utilst::create_static_symbol( const symbolt &dfcc_utilst::create_new_parameter_symbol( symbol_table_baset &symbol_table, const irep_idt &function_id, - const irep_idt &base_name, + const std::string &base_name, const typet &type) { - symbolt &function_symbol = get_function_symbol(symbol_table, function_id); + const symbolt &function_symbol = + get_function_symbol(symbol_table, function_id); - // insert new parameter in the symbol table - const symbolt &symbol = create_symbol( - symbol_table, + symbolt &symbol = get_fresh_aux_symbol( type, id2string(function_id), base_name, function_symbol.location, function_symbol.mode, - function_symbol.module, - true); + symbol_table); + symbol.is_parameter = true; + symbol.module = function_symbol.module; return symbol; } @@ -185,7 +170,7 @@ void dfcc_utilst::add_parameter( const symbolt &dfcc_utilst::add_parameter( goto_modelt &goto_model, const irep_idt &function_id, - const irep_idt &base_name, + const std::string &base_name, const typet &type) { const symbolt &symbol = create_new_parameter_symbol( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index b60f998cc69..2b0bec8dbcb 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -37,19 +37,17 @@ struct dfcc_utilst 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. + /// Adds a new symbol named `function_id::base_name` of type `type` + /// with given attributes in the symbol table, and returns a symbol expression + /// for the created symbol. /// If a symbol of the same name already exists the name will be decorated /// with a unique suffix. - static const symbolt &create_symbol( + static symbol_exprt create_symbol( symbol_table_baset &, const typet &type, - const irep_idt &prefix, - const irep_idt &base_name, - const source_locationt &source_location, - const irep_idt &mode, - const irep_idt &module, - bool is_parameter); + const irep_idt &function_id, + const std::string &base_name, + const source_locationt &source_location); /// Adds a new static symbol named `prefix::base_name` of type `type` with /// value `initial_value` in the symbol table, returns the created symbol. @@ -65,8 +63,8 @@ struct dfcc_utilst static const symbolt &create_static_symbol( symbol_table_baset &, const typet &type, - const irep_idt &prefix, - const irep_idt &base_name, + const std::string &prefix, + const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, @@ -77,7 +75,7 @@ struct dfcc_utilst static const symbolt &create_new_parameter_symbol( symbol_table_baset &, const irep_idt &function_id, - const irep_idt &base_name, + const std::string &base_name, const typet &type); /// \brief Adds the given symbol as parameter to the function symbol's @@ -93,7 +91,7 @@ struct dfcc_utilst static const symbolt &add_parameter( goto_modelt &, const irep_idt &function_id, - const irep_idt &base_name, + const std::string &base_name, const typet &type); /// \brief Creates a new function symbol and goto_function 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 70648724a55..ac16aa1a76b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -11,7 +11,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include #include -#include #include #include #include @@ -37,15 +36,11 @@ static symbol_exprt create_contract_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + wrapper_symbol.name, + "__contract_write_set", + wrapper_symbol.location); } /// Generate the contract write set pointer @@ -55,15 +50,11 @@ static symbol_exprt create_addr_of_contract_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + wrapper_symbol.name, + "__address_of_contract_write_set", + wrapper_symbol.location); } // Generate the write set to check for side effects in requires clauses @@ -73,15 +64,11 @@ static symbol_exprt create_requires_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + wrapper_symbol.name, + "__requires_write_set", + wrapper_symbol.location); } /// Generate the write set pointer to check side effects in requires clauses @@ -91,15 +78,11 @@ static symbol_exprt create_addr_of_requires_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + wrapper_symbol.name, + "__address_of_requires_write_set", + wrapper_symbol.location); } /// Generate the write set to check side effects in ensures clauses @@ -109,15 +92,11 @@ static symbol_exprt create_ensures_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET], + wrapper_symbol.name, + "__ensures_write_set", + wrapper_symbol.location); } /// Generate the write set pointer to check side effects in ensures clauses @@ -127,15 +106,11 @@ static symbol_exprt create_addr_of_ensures_write_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + wrapper_symbol.name, + "__address_of_ensures_write_set", + wrapper_symbol.location); } /// Generate object set used to support is_fresh predicates @@ -145,15 +120,11 @@ static symbol_exprt create_is_fresh_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::OBJ_SET], + wrapper_symbol.name, + "__is_fresh_set", + wrapper_symbol.location); } /// Generate object set pointer used to support is_fresh predicates @@ -163,15 +134,11 @@ static symbol_exprt create_addr_of_is_fresh_set( const symbolt &wrapper_symbol) { 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(); + symbol_table, + library.dfcc_type[dfcc_typet::OBJ_SET_PTR], + wrapper_symbol.name, + "__address_of_is_fresh_set", + wrapper_symbol.location); } dfcc_wrapper_programt::dfcc_wrapper_programt( @@ -238,15 +205,11 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( if(contract_code_type.return_type().id() != ID_empty) { 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(); + goto_model.symbol_table, + contract_code_type.return_type(), + wrapper_symbol.name, + "__contract_return_value", + wrapper_symbol.location); // build contract_lambda_parameters contract_lambda_parameters.push_back(return_value_opt.value()); @@ -336,14 +299,12 @@ void dfcc_wrapper_programt::encode_requires_write_set() // ASSERT __check_no_alloc; // DEAD __check_no_alloc: bool; // ``` - auto check_var = get_fresh_aux_symbol( - bool_typet(), - id2string(wrapper_symbol.name), - "__no_alloc_dealloc_in_requires", - wrapper_sl, - wrapper_symbol.mode, - goto_model.symbol_table) - .symbol_expr(); + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, + bool_typet(), + wrapper_symbol.name, + "__no_alloc_dealloc_in_requires", + wrapper_sl); postamble.add(goto_programt::make_decl(check_var, wrapper_sl)); @@ -418,14 +379,12 @@ void dfcc_wrapper_programt::encode_ensures_write_set() // ASSERT __check_no_alloc; // DEAD __check_no_alloc: bool; // ``` - auto check_var = get_fresh_aux_symbol( - bool_typet(), - id2string(wrapper_symbol.name), - "__no_alloc_dealloc_in_ensures_clauses", - wrapper_sl, - wrapper_symbol.mode, - goto_model.symbol_table) - .symbol_expr(); + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, + bool_typet(), + wrapper_symbol.name, + "__no_alloc_dealloc_in_ensures_clauses", + wrapper_sl); postamble.add(goto_programt::make_decl(check_var, wrapper_sl)); @@ -758,14 +717,12 @@ void dfcc_wrapper_programt::encode_havoced_function_call() { // assigns clause inclusion - auto check_var = get_fresh_aux_symbol( - bool_typet(), - id2string(wrapper_symbol.name), - "__check_assigns_clause_incl", - wrapper_sl, - wrapper_symbol.mode, - goto_model.symbol_table) - .symbol_expr(); + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, + bool_typet(), + wrapper_symbol.name, + "__check_assigns_clause_incl", + wrapper_sl); write_set_checks.add(goto_programt::make_decl(check_var, wrapper_sl)); @@ -786,14 +743,12 @@ void dfcc_wrapper_programt::encode_havoced_function_call() { // frees clause inclusion - auto check_var = get_fresh_aux_symbol( - bool_typet(), - id2string(wrapper_symbol.name), - "__check_frees_clause_incl", - wrapper_sl, - wrapper_symbol.mode, - goto_model.symbol_table) - .symbol_expr(); + const auto check_var = dfcc_utilst::create_symbol( + goto_model.symbol_table, + bool_typet(), + wrapper_symbol.name, + "__check_frees_clause_incl", + wrapper_sl); write_set_checks.add(goto_programt::make_decl(check_var, wrapper_sl)); diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 8d97b354355..e941c0732d3 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -16,6 +16,7 @@ Date: January 2022 #include #include #include +#include #include #include #include @@ -441,12 +442,23 @@ void instrument_spec_assignst::track_plain_spec_target( create_snapshot(car, dest); } -const symbolt instrument_spec_assignst::create_fresh_symbol( +/// Creates a fresh symbolt with given suffix, scoped to the function of +/// \p location. +static symbol_exprt create_fresh_symbol( const std::string &suffix, const typet &type, - const source_locationt &location) const + const source_locationt &location, + const irep_idt &mode, + symbol_table_baset &symbol_table) { - return new_tmp_symbol(type, location, mode, st, suffix); + return get_fresh_aux_symbol( + type, + id2string(location.get_function()), + suffix, + location, + mode, + symbol_table) + .symbol_expr(); } car_exprt instrument_spec_assignst::create_car_expr( @@ -455,16 +467,13 @@ car_exprt instrument_spec_assignst::create_car_expr( { const source_locationt &source_location = target.source_location(); const auto &valid_var = - create_fresh_symbol("__car_valid", bool_typet(), source_location) - .symbol_expr(); + create_fresh_symbol("__car_valid", bool_typet(), source_location, mode, st); - const auto &lower_bound_var = - create_fresh_symbol("__car_lb", pointer_type(char_type()), source_location) - .symbol_expr(); + const auto &lower_bound_var = create_fresh_symbol( + "__car_lb", pointer_type(char_type()), source_location, mode, st); - const auto &upper_bound_var = - create_fresh_symbol("__car_ub", pointer_type(char_type()), source_location) - .symbol_expr(); + const auto &upper_bound_var = create_fresh_symbol( + "__car_ub", pointer_type(char_type()), source_location, mode, st); if(target.id() == ID_pointer_object) { diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index d899d005fed..2534f61427d 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -501,13 +501,6 @@ class instrument_spec_assignst /// checking assertions for a conditional target group from an assigns clause void track_plain_spec_target(const exprt &expr, goto_programt &dest); - /// Creates a fresh symbolt with given suffix, - /// scoped to \ref function_id. - const symbolt create_fresh_symbol( - const std::string &suffix, - const typet &type, - const source_locationt &location) const; - /// Returns snapshot instructions for a car_exprt void create_snapshot(const car_exprt &car, goto_programt &dest) const; diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index 47108333ab5..706e25a7b09 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -16,6 +16,7 @@ Date: July 2021 #include #include #include +#include #include #include @@ -255,13 +256,13 @@ is_fresh_enforcet::is_fresh_enforcet( this->memmap_name = ssmemmap.str(); const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode; - this->memmap_symbol = new_tmp_symbol( + this->memmap_symbol = get_fresh_aux_symbol( get_memmap_type(), + "", + this->memmap_name, source_locationt(), mode, - goto_model.symbol_table, - this->memmap_name, - true); + goto_model.symbol_table); } void is_fresh_enforcet::create_declarations() @@ -334,13 +335,13 @@ is_fresh_replacet::is_fresh_replacet( this->memmap_name = ssmemmap.str(); const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode; - this->memmap_symbol = new_tmp_symbol( + this->memmap_symbol = get_fresh_aux_symbol( get_memmap_type(), + "", + this->memmap_name, source_locationt(), mode, - goto_model.symbol_table, - this->memmap_name, - true); + goto_model.symbol_table); } void is_fresh_replacet::create_declarations() diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 2bc96a8c29a..1de892e76d7 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -253,20 +253,6 @@ void insert_before_and_update_jumps( } } -const symbolt &new_tmp_symbol( - const typet &type, - const source_locationt &location, - const irep_idt &mode, - symbol_table_baset &symtab, - std::string suffix, - bool is_auxiliary) -{ - symbolt &new_symbol = get_fresh_aux_symbol( - type, id2string(location.get_function()), suffix, location, mode, symtab); - new_symbol.is_auxiliary = is_auxiliary; - return new_symbol; -} - void simplify_gotos(goto_programt &goto_program, namespacet &ns) { for(auto &instruction : goto_program.instructions) @@ -427,8 +413,10 @@ void add_quantified_variable( for(const auto &quantified_variable : quantifier_expression.variables()) { // 1. create fresh symbol - symbolt new_symbol = new_tmp_symbol( + symbolt new_symbol = get_fresh_aux_symbol( quantified_variable.type(), + id2string(quantified_variable.source_location().get_function()), + "tmp_cc", quantified_variable.source_location(), mode, symbol_table); @@ -486,9 +474,14 @@ static void replace_history_parameter_rec( { // 1. Create a temporary symbol expression that represents the // history variable - entry.first->second = - new_tmp_symbol(parameter.type(), location, mode, symbol_table) - .symbol_expr(); + entry.first->second = get_fresh_aux_symbol( + parameter.type(), + id2string(location.get_function()), + "tmp_cc", + location, + mode, + symbol_table) + .symbol_expr(); // 2. Add the required instructions to the instructions list // 2.1. Declare the newly created temporary variable diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 5a8aaa93004..1d3ab53f8cc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -187,23 +187,6 @@ void insert_before_and_update_jumps( goto_programt::targett &target, const goto_programt::instructiont &i); -/// \brief Adds a fresh and uniquely named symbol to the symbol table. -/// -/// \param type: The type of the new symbol. -/// \param location: The source location for the new symbol. -/// \param mode: The mode for the new symbol, e.g. ID_C, ID_java. -/// \param symtab: The symbol table to which the new symbol is to be added. -/// \param suffix: Suffix to use to generate the unique name -/// \param is_auxiliary: Do not print symbol in traces if true (default = true) -/// \return The new symbolt object. -const symbolt &new_tmp_symbol( - const typet &type, - const source_locationt &location, - const irep_idt &mode, - symbol_table_baset &symtab, - std::string suffix = "tmp_cc", - bool is_auxiliary = true); - /// Turns goto instructions `IF cond GOTO label` where the condition /// statically simplifies to `false` into SKIP instructions. void simplify_gotos(goto_programt &goto_program, namespacet &ns);