From 3d2efc0e68a9ef5318379eba0f7eec15356946ed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Jan 2019 16:48:11 +0000 Subject: [PATCH 1/3] goto-symex: use function and called_function fields goto_programt::instructionst::instructiont::function is going to go away, use the fields that are already available within goto-symex. --- src/goto-checker/symex_bmc.cpp | 2 +- src/goto-programs/goto_program.h | 5 +++-- src/goto-symex/goto_symex_state.cpp | 4 ++-- src/goto-symex/symex_goto.cpp | 6 ++++-- src/goto-symex/symex_main.cpp | 17 ++++++++++------- 5 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index e905aa0bf2e..fd9e369b148 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -110,7 +110,7 @@ bool symex_bmct::should_stop_unwind( const goto_symex_statet::call_stackt &context, unsigned unwind) { - const irep_idt id = goto_programt::loop_id(*source.pc); + const irep_idt id = goto_programt::loop_id(source.function, *source.pc); tvt abort_unwind_decision; unsigned this_loop_limit = std::numeric_limits::max(); diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index bdcbaafb438..88d21775026 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -694,9 +694,10 @@ class goto_programt void update(); /// Human-readable loop name - static irep_idt loop_id(const instructiont &instruction) + static irep_idt + loop_id(const irep_idt &function_id, const instructiont &instruction) { - return id2string(instruction.function)+"."+ + return id2string(function_id) + "." + std::to_string(instruction.loop_number); } diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 75910181510..2fa3af73ffc 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -759,7 +759,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const return; } - out << source.pc->function << " " << source.pc->location_number << "\n"; + out << source.function << " " << source.pc->location_number << "\n"; for(auto stackit = threads[source.thread_nr].call_stack.rbegin(), stackend = threads[source.thread_nr].call_stack.rend(); @@ -769,7 +769,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const const auto &frame = *stackit; if(frame.calling_location.is_set) { - out << frame.calling_location.pc->function << " " + out << frame.calling_location.function << " " << frame.calling_location.pc->location_number << "\n"; } } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index c5b67fe2c9f..1c8ffef60fa 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -85,8 +85,10 @@ void goto_symext::symex_goto(statet &state) return; } - unsigned &unwind= - frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count; + const auto loop_id = + goto_programt::loop_id(state.source.function, *state.source.pc); + + unsigned &unwind = frame.loop_iterations[loop_id].count; unwind++; if(should_stop_unwind(state.source, state.call_stack(), unwind)) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 8885bf2b85b..18bbde29c69 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -58,7 +58,11 @@ void symex_transition( if(i_e->is_goto() && i_e->is_backwards_goto() && (!is_backwards_goto || state.source.pc->location_number>i_e->location_number)) - frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0; + { + const auto loop_id = + goto_programt::loop_id(state.source.function, *i_e); + frame.loop_iterations[loop_id].count = 0; + } } state.source.pc=to; @@ -157,19 +161,18 @@ void goto_symext::initialize_entry_point( state.top().calling_location.pc=state.top().end_of_function; state.symex_target=⌖ - INVARIANT( - !pc->function.empty(), "all symexed instructions should have a function"); - - const goto_functiont &entry_point_function = get_goto_function(pc->function); + const goto_functiont &entry_point_function = + get_goto_function(function_identifier); state.top().hidden_function = entry_point_function.is_hidden(); auto emplace_safe_pointers_result = - state.safe_pointers.emplace(pc->function, local_safe_pointerst{ns}); + state.safe_pointers.emplace(function_identifier, local_safe_pointerst{ns}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(entry_point_function.body); - state.dirty.populate_dirty_for_function(pc->function, entry_point_function); + state.dirty.populate_dirty_for_function( + function_identifier, entry_point_function); symex_transition(state, state.source.pc, false); } From b7222def9c75bfe52e36358774f6a2ef6f6e68b3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 19 Jan 2019 10:47:16 +0000 Subject: [PATCH 2/3] Use goto_programt::loop_id This ensures we build loop identifiers in the same way everywhere. --- src/goto-instrument/unwind.cpp | 3 +-- src/goto-programs/loop_ids.cpp | 11 ++++------- 2 files changed, 5 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 723b08b6e78..ced24975192 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -288,8 +288,7 @@ void goto_unwindt::unwind( } PRECONDITION(!function_id.empty()); - const irep_idt loop_id = - id2string(function_id) + "." + std::to_string(i_it->loop_number); + const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it); auto limit=unwindset.get_limit(loop_id, 0); diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index 4e0ae79cc6e..9b6bbcecdb2 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -36,9 +36,8 @@ void show_loop_ids( { if(it->is_backwards_goto()) { - unsigned loop_id=it->loop_number; - - std::cout << "Loop " << function_identifier << "." << loop_id << ":" + std::cout << "Loop " + << goto_programt::loop_id(function_identifier, *it) << ":" << "\n"; std::cout << " " << it->source_location << "\n"; @@ -53,9 +52,8 @@ void show_loop_ids( { if(it->is_backwards_goto()) { - unsigned loop_id=it->loop_number; std::string id = - id2string(function_identifier) + "." + std::to_string(loop_id); + id2string(goto_programt::loop_id(function_identifier, *it)); xmlt xml_loop("loop", {{"name", id}}, {}); xml_loop.new_element("loop-id").data=id; @@ -82,9 +80,8 @@ void show_loop_ids_json( { if(it->is_backwards_goto()) { - unsigned loop_id=it->loop_number; std::string id = - id2string(function_identifier) + "." + std::to_string(loop_id); + id2string(goto_programt::loop_id(function_identifier, *it)); loops.push_back( json_objectt({{"name", json_stringt(id)}, From f33f64e76399820bb0dda394679f3e0bee6419cb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 20 Jan 2019 18:23:49 +0000 Subject: [PATCH 3/3] symex: Consistently use function_id "function" is too ambiguous and "function_identifier" is too long, and mixing them is even worse. --- src/goto-checker/symex_bmc.cpp | 4 +-- src/goto-programs/goto_trace.cpp | 33 ++++++++++++++-------- src/goto-programs/goto_trace.h | 2 +- src/goto-programs/graphml_witness.cpp | 11 ++++---- src/goto-programs/json_goto_trace.cpp | 6 ++-- src/goto-programs/loop_ids.cpp | 14 ++++----- src/goto-programs/loop_ids.h | 2 +- src/goto-programs/xml_goto_trace.cpp | 8 +++--- src/goto-symex/build_goto_trace.cpp | 4 +-- src/goto-symex/goto_symex_state.cpp | 4 +-- src/goto-symex/show_program.cpp | 8 +++--- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_dereference.cpp | 2 +- src/goto-symex/symex_function_call.cpp | 4 +-- src/goto-symex/symex_goto.cpp | 2 +- src/goto-symex/symex_main.cpp | 14 ++++----- src/goto-symex/symex_target.h | 16 +++++------ src/goto-symex/symex_target_equation.cpp | 18 ++++++------ src/goto-symex/symex_target_equation.h | 2 +- 19 files changed, 81 insertions(+), 75 deletions(-) diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index fd9e369b148..2de3b0144a7 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -69,7 +69,7 @@ void symex_bmct::symex_step( record_coverage && // avoid an invalid iterator in state.source.pc (!cur_pc->is_end_function() || - state.source.function != goto_functionst::entry_point())) + state.source.function_id != goto_functionst::entry_point())) { // forward goto will effectively be covered via phi function, // which does not invoke symex_step; as symex_step is called @@ -110,7 +110,7 @@ bool symex_bmct::should_stop_unwind( const goto_symex_statet::call_stackt &context, unsigned unwind) { - const irep_idt id = goto_programt::loop_id(source.function, *source.pc); + const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc); tvt abort_unwind_decision; unsigned this_loop_limit = std::numeric_limits::max(); diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index d40b226f428..8d69f672de3 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -292,9 +292,9 @@ state_location(const goto_trace_stept &state, const namespacet &ns) if(!source_location.get_file().empty()) result += "file " + id2string(source_location.get_file()); - if(!state.function.empty()) + if(!state.function_id.empty()) { - const symbolt &symbol = ns.lookup(state.function); + const symbolt &symbol = ns.lookup(state.function_id); if(!result.empty()) result += ' '; result += "function " + id2string(symbol.display_name()); @@ -333,7 +333,7 @@ void show_state_header( if(options.show_code) { - out << as_string(ns, state.function, *state.pc) << '\n'; + out << as_string(ns, state.function_id, *state.pc) << '\n'; out << "----------------------------------------------------" << '\n'; } } @@ -387,7 +387,10 @@ void show_compact_goto_trace( out << " " << messaget::red << step.comment << messaget::reset << '\n'; if(step.pc->is_assert()) - out << " " << from_expr(ns, step.function, step.pc->guard) << '\n'; + { + out << " " << from_expr(ns, step.function_id, step.pc->guard) + << '\n'; + } out << '\n'; } @@ -442,7 +445,7 @@ void show_compact_goto_trace( { auto arg_strings = make_range(step.function_arguments) .map([&ns, &step](const exprt &arg) { - return from_expr(ns, step.function, arg); + return from_expr(ns, step.function_id, arg); }); out << '('; @@ -507,7 +510,10 @@ void show_full_goto_trace( out << " " << messaget::red << step.comment << messaget::reset << '\n'; if(step.pc->is_assert()) - out << " " << from_expr(ns, step.function, step.pc->guard) << '\n'; + { + out << " " << from_expr(ns, step.function_id, step.pc->guard) + << '\n'; + } out << '\n'; } @@ -522,7 +528,10 @@ void show_full_goto_trace( out << " " << step.pc->source_location << '\n'; if(step.pc->is_assume()) - out << " " << from_expr(ns, step.function, step.pc->guard) << '\n'; + { + out << " " << from_expr(ns, step.function_id, step.pc->guard) + << '\n'; + } out << '\n'; } @@ -592,7 +601,7 @@ void show_full_goto_trace( if(l_it!=step.io_args.begin()) out << ';'; - out << ' ' << from_expr(ns, step.function, *l_it); + out << ' ' << from_expr(ns, step.function_id, *l_it); // the binary representation out << " (" << trace_numeric_value(*l_it, ns, options) << ')'; @@ -614,7 +623,7 @@ void show_full_goto_trace( if(l_it!=step.io_args.begin()) out << ';'; - out << ' ' << from_expr(ns, step.function, *l_it); + out << ' ' << from_expr(ns, step.function_id, *l_it); // the binary representation out << " (" << trace_numeric_value(*l_it, ns, options) << ')'; @@ -638,7 +647,7 @@ void show_full_goto_trace( else out << ", "; - out << from_expr(ns, step.function, arg); + out << from_expr(ns, step.function_id, arg); } out << ") (depth " << function_depth << ") ####\n"; @@ -649,7 +658,7 @@ void show_full_goto_trace( function_depth--; if(options.show_function_calls) { - out << "\n#### Function return from " << step.function << " (depth " + out << "\n#### Function return from " << step.function_id << " (depth " << function_depth << ") ####\n"; } break; @@ -732,7 +741,7 @@ static void show_goto_stack_trace( else out << ", "; - out << from_expr(ns, step.function, arg); + out << from_expr(ns, step.function_id, arg); } out << ')'; diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 09ff1646fb3..108bb52bf86 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -88,7 +88,7 @@ class goto_trace_stept // The instruction that created this step // (function calls are in the caller, function returns are in the callee) - irep_idt function; + irep_idt function_id; goto_programt::const_targett pc; // this transition done by given thread number diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 2f22933f523..a843f90d783 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -285,8 +285,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { xmlt &val=edge.new_element("data"); val.set_attribute("key", "assumption"); - val.data = from_expr(ns, it->function, it->full_lhs) + " = " + - from_expr(ns, it->function, it->full_lhs_value) + ";"; + val.data = from_expr(ns, it->function_id, it->full_lhs) + " = " + + from_expr(ns, it->function_id, it->full_lhs_value) + ";"; xmlt &val_s=edge.new_element("data"); val_s.set_attribute("key", "assumption.scope"); @@ -297,9 +297,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { xmlt &val=edge.new_element("data"); val.set_attribute("key", "sourcecode"); - const std::string cond = from_expr(ns, it->function, it->cond_expr); + const std::string cond = + from_expr(ns, it->function_id, it->cond_expr); const std::string neg_cond = - from_expr(ns, it->function, not_exprt(it->cond_expr)); + from_expr(ns, it->function_id, not_exprt(it->cond_expr)); val.data="["+(it->cond_value ? cond : neg_cond)+"]"; #if 0 @@ -483,7 +484,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) xmlt &val=edge.new_element("data"); val.set_attribute("key", "sourcecode"); const std::string cond = - from_expr(ns, it->source.function, it->cond_expr); + from_expr(ns, it->source.function_id, it->cond_expr); val.data="["+cond+"]"; } diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index d5072e2c388..46b761530c1 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -179,7 +179,7 @@ void convert_output( // Recovering the mode from the function irep_idt mode; const symbolt *function_name; - if(ns.lookup(step.function, function_name)) + if(ns.lookup(step.function_id, function_name)) // Failed to find symbol mode = ID_unknown; else @@ -221,7 +221,7 @@ void convert_input( // Recovering the mode from the function irep_idt mode; const symbolt *function_name; - if(ns.lookup(step.function, function_name)) + if(ns.lookup(step.function_id, function_name)) // Failed to find symbol mode = ID_unknown; else @@ -265,7 +265,7 @@ void convert_return( const irep_idt &function_identifier = (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function - : step.function; + : step.function_id; const symbolt &symbol = ns.lookup(function_identifier); json_call_return["function"] = diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index 9b6bbcecdb2..91b6a4db35a 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -25,7 +25,7 @@ void show_loop_ids( void show_loop_ids( ui_message_handlert::uit ui, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program) { switch(ui) @@ -36,8 +36,8 @@ void show_loop_ids( { if(it->is_backwards_goto()) { - std::cout << "Loop " - << goto_programt::loop_id(function_identifier, *it) << ":" + std::cout << "Loop " << goto_programt::loop_id(function_id, *it) + << ":" << "\n"; std::cout << " " << it->source_location << "\n"; @@ -52,8 +52,7 @@ void show_loop_ids( { if(it->is_backwards_goto()) { - std::string id = - id2string(goto_programt::loop_id(function_identifier, *it)); + std::string id = id2string(goto_programt::loop_id(function_id, *it)); xmlt xml_loop("loop", {{"name", id}}, {}); xml_loop.new_element("loop-id").data=id; @@ -70,7 +69,7 @@ void show_loop_ids( void show_loop_ids_json( ui_message_handlert::uit ui, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, json_arrayt &loops) { @@ -80,8 +79,7 @@ void show_loop_ids_json( { if(it->is_backwards_goto()) { - std::string id = - id2string(goto_programt::loop_id(function_identifier, *it)); + std::string id = id2string(goto_programt::loop_id(function_id, *it)); loops.push_back( json_objectt({{"name", json_stringt(id)}, diff --git a/src/goto-programs/loop_ids.h b/src/goto-programs/loop_ids.h index fbf0c0a4b00..ee21e9a11fb 100644 --- a/src/goto-programs/loop_ids.h +++ b/src/goto-programs/loop_ids.h @@ -26,7 +26,7 @@ void show_loop_ids( void show_loop_ids( ui_message_handlert::uit, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &); #endif // CPROVER_GOTO_PROGRAMS_LOOP_IDS_H diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 8fe74186cca..61164356bef 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -127,7 +127,7 @@ void convert( for(const auto &arg : step.io_args) { xml_output.new_element("value").data = - from_expr(ns, step.function, arg); + from_expr(ns, step.function_id, arg); xml_output.new_element("value_expression"). new_element(xml(arg, ns)); } @@ -146,7 +146,7 @@ void convert( for(const auto &arg : step.io_args) { xml_input.new_element("value").data = - from_expr(ns, step.function, arg); + from_expr(ns, step.function_id, arg); xml_input.new_element("value_expression"). new_element(xml(arg, ns)); } @@ -186,11 +186,11 @@ void convert( xml_call_return.set_attribute("thread", std::to_string(step.thread_nr)); xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr)); - const symbolt &symbol = ns.lookup(step.function); + const symbolt &symbol = ns.lookup(step.function_id); xmlt &xml_function=xml_call_return.new_element("function"); xml_function.set_attribute( "display_name", id2string(symbol.display_name())); - xml_function.set_attribute("identifier", id2string(step.function)); + xml_function.set_attribute("identifier", id2string(step.function_id)); xml_function.new_element()=xml(symbol.location); if(xml_location.name!="") diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index b09a77fb29d..77f64bc03bc 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -156,7 +156,7 @@ void update_internal_field( } // set internal field to _start function-return step - if(SSA_step.source.function == goto_functionst::entry_point()) + if(SSA_step.source.function_id == goto_functionst::entry_point()) { // "__CPROVER_*" function calls in __CPROVER_start are already marked as // internal. Don't mark any other function calls (i.e. "main"), function @@ -304,7 +304,7 @@ void build_goto_trace( goto_trace_step.thread_nr = SSA_step.source.thread_nr; goto_trace_step.pc = SSA_step.source.pc; - goto_trace_step.function = SSA_step.source.function; + goto_trace_step.function_id = SSA_step.source.function_id; if(SSA_step.is_assert()) { goto_trace_step.comment = SSA_step.comment; diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 2fa3af73ffc..44b3b58e4ca 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -759,7 +759,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const return; } - out << source.function << " " << source.pc->location_number << "\n"; + out << source.function_id << " " << source.pc->location_number << "\n"; for(auto stackit = threads[source.thread_nr].call_stack.rbegin(), stackend = threads[source.thread_nr].call_stack.rend(); @@ -769,7 +769,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const const auto &frame = *stackit; if(frame.calling_location.is_set) { - out << frame.calling_location.function << " " + out << frame.calling_location.function_id << " " << frame.calling_location.pc->location_number << "\n"; } } diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp index d6a596300c1..2d3a2943f04 100644 --- a/src/goto-symex/show_program.cpp +++ b/src/goto-symex/show_program.cpp @@ -28,11 +28,11 @@ static void show_step( const std::string &annotation, std::size_t &count) { - const irep_idt &function = step.source.function; + const irep_idt &function_id = step.source.function_id; std::string string_value = (step.is_shared_read() || step.is_shared_write()) - ? from_expr(ns, function, step.ssa_lhs) - : from_expr(ns, function, step.cond_expr); + ? from_expr(ns, function_id, step.ssa_lhs) + : from_expr(ns, function_id, step.cond_expr); std::cout << '(' << count << ") "; if(annotation.empty()) std::cout << string_value; @@ -42,7 +42,7 @@ static void show_step( if(!step.guard.is_true()) { - const std::string guard_string = from_expr(ns, function, step.guard); + const std::string guard_string = from_expr(ns, function_id, step.guard); std::cout << std::string(std::to_string(count).size() + 3, ' '); std::cout << "guard: " << guard_string << '\n'; } diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 32b3ec0160e..b2e5bc5afec 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -56,7 +56,7 @@ void goto_symext::symex_allocate( exprt size=code.op0(); typet object_type=nil_typet(); - auto function_symbol = outer_symbol_table.lookup(state.source.function); + auto function_symbol = outer_symbol_table.lookup(state.source.function_id); INVARIANT(function_symbol, "function associated with allocation not found"); const irep_idt &mode = function_symbol->mode; diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index b1e27e4acb0..f0395e45418 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -257,7 +257,7 @@ void goto_symext::dereference_rec( if(state.threads.size() == 1) { - const irep_idt &expr_function = state.source.function; + const irep_idt &expr_function = state.source.function_id; if(!expr_function.empty()) { state.get_original_name(to_check); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 1df1721f4c6..0d024c5f550 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -322,7 +322,7 @@ void goto_symext::symex_function_call_code( frame.loop_iterations[identifier].count++; state.source.is_set=true; - state.source.function = identifier; + state.source.function_id = identifier; symex_transition(state, goto_function.body.instructions.begin(), false); } @@ -336,7 +336,7 @@ void goto_symext::pop_frame(statet &state) // restore program counter symex_transition(state, frame.calling_location.pc, false); - state.source.function = frame.calling_location.function; + state.source.function_id = frame.calling_location.function_id; // restore L1 renaming state.level1.restore_from(frame.old_level1); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 1c8ffef60fa..1f18a25f313 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -86,7 +86,7 @@ void goto_symext::symex_goto(statet &state) } const auto loop_id = - goto_programt::loop_id(state.source.function, *state.source.pc); + goto_programt::loop_id(state.source.function_id, *state.source.pc); unsigned &unwind = frame.loop_iterations[loop_id].count; unwind++; diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 18bbde29c69..d5ebe73b7d5 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -60,7 +60,7 @@ void symex_transition( state.source.pc->location_number>i_e->location_number)) { const auto loop_id = - goto_programt::loop_id(state.source.function, *i_e); + goto_programt::loop_id(state.source.function_id, *i_e); frame.loop_iterations[loop_id].count = 0; } } @@ -150,29 +150,27 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state) void goto_symext::initialize_entry_point( statet &state, const get_goto_functiont &get_goto_function, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt::const_targett pc, const goto_programt::const_targett limit) { PRECONDITION(!state.threads.empty()); PRECONDITION(!state.call_stack().empty()); - state.source = symex_targett::sourcet(function_identifier, pc); + state.source = symex_targett::sourcet(function_id, pc); state.top().end_of_function=limit; state.top().calling_location.pc=state.top().end_of_function; state.symex_target=⌖ - const goto_functiont &entry_point_function = - get_goto_function(function_identifier); + const goto_functiont &entry_point_function = get_goto_function(function_id); state.top().hidden_function = entry_point_function.is_hidden(); auto emplace_safe_pointers_result = - state.safe_pointers.emplace(function_identifier, local_safe_pointerst{ns}); + state.safe_pointers.emplace(function_id, local_safe_pointerst{ns}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(entry_point_function.body); - state.dirty.populate_dirty_for_function( - function_identifier, entry_point_function); + state.dirty.populate_dirty_for_function(function_id, entry_point_function); symex_transition(state, state.source.pc, false); } diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index ba8b8af4157..d365893c47e 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -35,26 +35,26 @@ class symex_targett struct sourcet { unsigned thread_nr; - irep_idt function; + irep_idt function_id; // The program counter is an iterator which indicates where the execution // is in its program sequence goto_programt::const_targett pc; bool is_set; - sourcet() : thread_nr(0), function(irep_idt()), is_set(false) + sourcet() : thread_nr(0), function_id(irep_idt()), is_set(false) { } - sourcet(const irep_idt &_function, goto_programt::const_targett _pc) - : thread_nr(0), function(_function), pc(_pc), is_set(true) + sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc) + : thread_nr(0), function_id(_function_id), pc(_pc), is_set(true) { } explicit sourcet( - const irep_idt &_function, + const irep_idt &_function_id, const goto_programt &_goto_program) : thread_nr(0), - function(_function), + function_id(_function_id), pc(_goto_program.instructions.begin()), is_set(true) { @@ -144,14 +144,14 @@ class symex_targett /// Record a function call. /// \param guard: Precondition for calling a function - /// \param function_identifier: Name of the function + /// \param function_id: Name of the function /// \param ssa_function_arguments: Vector of arguments in SSA form /// \param source: To location in the input GOTO program of this /// \param hidden: Should this step be recorded as hidden? /// function call virtual void function_call( const exprt &guard, - const irep_idt &function_identifier, + const irep_idt &function_id, const std::vector &ssa_function_arguments, const sourcet &source, bool hidden) = 0; diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 4af05a3936a..e9a145e20f0 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -186,7 +186,7 @@ void symex_target_equationt::location( void symex_target_equationt::function_call( const exprt &guard, - const irep_idt &function_identifier, + const irep_idt &function_id, const std::vector &ssa_function_arguments, const sourcet &source, const bool hidden) @@ -195,7 +195,7 @@ void symex_target_equationt::function_call( SSA_stept &SSA_step=SSA_steps.back(); SSA_step.guard = guard; - SSA_step.called_function = function_identifier; + SSA_step.called_function = function_id; SSA_step.ssa_function_arguments = ssa_function_arguments; SSA_step.hidden = hidden; @@ -707,10 +707,10 @@ void symex_target_equationt::SSA_stept::output( switch(type) { case goto_trace_stept::typet::ASSERT: - out << "ASSERT " << from_expr(ns, source.function, cond_expr) << '\n'; + out << "ASSERT " << from_expr(ns, source.function_id, cond_expr) << '\n'; break; case goto_trace_stept::typet::ASSUME: - out << "ASSUME " << from_expr(ns, source.function, cond_expr) << '\n'; + out << "ASSUME " << from_expr(ns, source.function_id, cond_expr) << '\n'; break; case goto_trace_stept::typet::LOCATION: out << "LOCATION" << '\n'; break; @@ -721,7 +721,7 @@ void symex_target_equationt::SSA_stept::output( case goto_trace_stept::typet::DECL: out << "DECL" << '\n'; - out << from_expr(ns, source.function, ssa_lhs) << '\n'; + out << from_expr(ns, source.function_id, ssa_lhs) << '\n'; break; case goto_trace_stept::typet::ASSIGNMENT: @@ -775,22 +775,22 @@ void symex_target_equationt::SSA_stept::output( case goto_trace_stept::typet::MEMORY_BARRIER: out << "MEMORY_BARRIER\n"; break; case goto_trace_stept::typet::GOTO: - out << "IF " << from_expr(ns, source.function, cond_expr) << " GOTO\n"; + out << "IF " << from_expr(ns, source.function_id, cond_expr) << " GOTO\n"; break; default: UNREACHABLE; } if(is_assert() || is_assume() || is_assignment() || is_constraint()) - out << from_expr(ns, source.function, cond_expr) << '\n'; + out << from_expr(ns, source.function_id, cond_expr) << '\n'; if(is_assert() || is_constraint()) out << comment << '\n'; if(is_shared_read() || is_shared_write()) - out << from_expr(ns, source.function, ssa_lhs) << '\n'; + out << from_expr(ns, source.function_id, ssa_lhs) << '\n'; - out << "Guard: " << from_expr(ns, source.function, guard) << '\n'; + out << "Guard: " << from_expr(ns, source.function_id, guard) << '\n'; } void symex_target_equationt::SSA_stept::output(std::ostream &out) const diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index ca06a49852a..af334a69ff8 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -78,7 +78,7 @@ class symex_target_equationt:public symex_targett /// \copydoc symex_targett::function_call() virtual void function_call( const exprt &guard, - const irep_idt &function_identifier, + const irep_idt &function_id, const std::vector &ssa_function_arguments, const sourcet &source, bool hidden);