From 66a5a4244b1097a0b0edbdf2155fd4003ef16039 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 13 May 2022 16:58:01 -0700 Subject: [PATCH] instructiont::get_code -> code This renames the field code to _code, introduces instructiont::code() as a replacement for get_code(), changes the uses of get_code to code, and marks get_code as deprecated. The rationale is to match the pattern of the other accessor methods of the class. --- jbmc/src/java_bytecode/remove_exceptions.cpp | 8 +-- jbmc/src/java_bytecode/remove_instanceof.cpp | 4 +- .../src/java_bytecode/replace_java_nondet.cpp | 4 +- .../virtual_call_null_checks.cpp | 4 +- .../java_replace_nondet/replace_nondet.cpp | 2 +- src/analyses/cfg_dominators.h | 2 +- src/analyses/invariant_set_domain.cpp | 6 +- src/analyses/uncaught_exceptions_analysis.cpp | 6 +- .../contracts/instrument_spec_assigns.cpp | 3 +- src/goto-instrument/dot.cpp | 2 +- .../goto_instrument_parse_options.cpp | 4 +- src/goto-instrument/wmm/fence.cpp | 18 ++--- src/goto-instrument/wmm/goto2graph.cpp | 17 +++-- src/goto-instrument/wmm/shared_buffers.cpp | 16 ++--- src/goto-programs/goto_convert.cpp | 14 ++-- src/goto-programs/goto_program.cpp | 40 ++++++------ src/goto-programs/goto_program.h | 65 ++++++++++--------- src/goto-programs/interpreter.cpp | 12 ++-- src/goto-programs/remove_returns.cpp | 2 +- src/goto-programs/remove_skip.cpp | 5 +- .../show_goto_functions_json.cpp | 8 +-- src/goto-programs/show_goto_functions_xml.cpp | 4 +- src/goto-programs/validate_goto_model.cpp | 2 +- src/goto-programs/write_goto_binary.cpp | 2 +- src/goto-symex/build_goto_trace.cpp | 2 +- src/goto-symex/memory_model_tso.cpp | 2 +- src/goto-symex/solver_hardness.cpp | 18 ++--- src/goto-symex/symex_goto.cpp | 8 +-- src/goto-symex/symex_main.cpp | 6 +- src/pointer-analysis/value_set_domain.h | 2 +- src/pointer-analysis/value_set_domain_fi.cpp | 2 +- .../goto_program_function_call.cpp | 3 +- 32 files changed, 148 insertions(+), 145 deletions(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index e237ba82eb0..167cbe3ce53 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -234,7 +234,7 @@ void remove_exceptionst::instrument_exception_handler( { // retrieve the exception variable const exprt &thrown_exception_local = - to_code_landingpad(instr_it->get_code()).catch_expr(); + to_code_landingpad(instr_it->code()).catch_expr(); const symbol_exprt thrown_global_symbol= get_inflight_exception_global(); @@ -407,7 +407,7 @@ bool remove_exceptionst::instrument_throw( PRECONDITION(instr_it->type() == THROW); const exprt &exc_expr = - uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code()); + uncaught_exceptions_domaint::get_exception_symbol(instr_it->code()); add_exception_dispatch_sequence( function_identifier, goto_program, instr_it, stack_catch, locals); @@ -512,7 +512,7 @@ void remove_exceptionst::instrument_exceptions( // Is it a handler push/pop or catch landing-pad? else if(instr_it->type() == CATCH) { - const irep_idt &statement = instr_it->get_code().get_statement(); + const irep_idt &statement = instr_it->code().get_statement(); // Is it an exception landing pad (start of a catch block)? if(statement==ID_exception_landingpad) { @@ -553,7 +553,7 @@ void remove_exceptionst::instrument_exceptions( // copy targets const code_push_catcht::exception_listt &exception_list = - to_code_push_catch(instr_it->get_code()).exception_list(); + to_code_push_catch(instr_it->code()).exception_list(); // The target list can be empty if `finish_catch_push_targets` found that // the targets were unreachable (in which case no exception can truly diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index 04a5707c0e5..3e1ddd142c8 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -242,8 +242,8 @@ bool remove_instanceoft::lower_instanceof( goto_programt::targett target) { if( - target->is_target() && (contains_instanceof(target->get_code()) || - contains_instanceof(target->guard))) + target->is_target() && + (contains_instanceof(target->code()) || contains_instanceof(target->guard))) { // If this is a branch target, add a skip beforehand so we can splice new // GOTO programs before the target instruction without inserting into the diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index 4c7eef857fc..ab66e64cd6a 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -89,11 +89,11 @@ is_nondet_returning_object(const code_function_callt &function_call) static nondet_instruction_infot get_nondet_instruction_info(const goto_programt::const_targett &instr) { - if(!(instr->is_function_call() && instr->get_code().id() == ID_code)) + if(!(instr->is_function_call() && instr->code().id() == ID_code)) { return nondet_instruction_infot(); } - const auto &code = instr->get_code(); + const auto &code = instr->code(); INVARIANT( code.get_statement() == ID_function_call, "function_call should have ID_function_call"); diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp index a0636862d0a..72e38b37169 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp @@ -79,8 +79,8 @@ SCENARIO( instrend = main_function.body.instructions.end(); instrit != instrend; ++instrit) { - for(auto it = instrit->get_code().depth_begin(), - itend = instrit->get_code().depth_end(); + for(auto it = instrit->code().depth_begin(), + itend = instrit->code().depth_end(); it != itend; ++it) { diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index 551bce0424a..1368a14874e 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -93,7 +93,7 @@ void validate_nondets_converted( exprt target_expression = (inst.is_assign() ? inst.assign_rhs() - : inst.is_set_return_value() ? inst.return_value() : inst.get_code()); + : inst.is_set_return_value() ? inst.return_value() : inst.code()); if( const auto side_effect = diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index e98f9111e6c..ccf5eee9ca5 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -267,7 +267,7 @@ inline void dominators_pretty_print_node( const goto_programt::targett& target, std::ostream& out) { - out << target->get_code().pretty(); + out << target->code().pretty(); } /// Print the result of the dominator computation diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index 5e28c7d11c2..cdcb145d02a 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -60,15 +60,15 @@ void invariant_set_domaint::transform( case OTHER: if(from_l->get_other().is_not_nil()) - invariant_set.apply_code(from_l->get_code()); + invariant_set.apply_code(from_l->code()); break; case DECL: - invariant_set.apply_code(from_l->get_code()); + invariant_set.apply_code(from_l->code()); break; case FUNCTION_CALL: - invariant_set.apply_code(from_l->get_code()); + invariant_set.apply_code(from_l->code()); break; case START_THREAD: diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index ce2573017c9..c8eb3185241 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -71,7 +71,7 @@ void uncaught_exceptions_domaint::transform( { case THROW: { - const exprt &exc_symbol = get_exception_symbol(instruction.get_code()); + const exprt &exc_symbol = get_exception_symbol(instruction.code()); // retrieve the static type of the thrown exception const irep_idt &type_id = get_exception_type(to_pointer_type(exc_symbol.type())); @@ -85,7 +85,7 @@ void uncaught_exceptions_domaint::transform( } case CATCH: { - if(!instruction.get_code().has_operands()) + if(!instruction.code().has_operands()) { if(!instruction.targets.empty()) // push { @@ -93,7 +93,7 @@ void uncaught_exceptions_domaint::transform( stack_caught.push_back(caught); std::set &last_caught=stack_caught.back(); const irept::subt &exception_list = - instruction.get_code().find(ID_exception_list).get_sub(); + instruction.code().find(ID_exception_list).get_sub(); for(const auto &exc : exception_list) { diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index b6726116865..26e93618a67 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -1021,8 +1021,7 @@ void instrument_spec_assignst::instrument_call_statement( if(callee_name == "malloc") { - const auto &function_call = - to_code_function_call(instruction_it->get_code()); + const auto &function_call = to_code_function_call(instruction_it->code()); if(function_call.lhs().is_not_nil()) { // grab the returned pointer from malloc diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index cc8025b948e..d63496a81cd 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -160,7 +160,7 @@ void dott::write_dot_subgraph( it->is_assign() || it->is_decl() || it->is_set_return_value() || it->is_other()) { - std::string t = from_expr(ns, function_id, it->get_code()); + std::string t = from_expr(ns, function_id, it->code()); while(t[ t.size()-1 ]=='\n') t = t.substr(0, t.size()-1); tmp.str(escape(t)); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3b7828cad4e..9090caa8cbb 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -658,8 +658,8 @@ int goto_instrument_parse_optionst::doit() for(auto const &pair : goto_model.goto_functions.function_map) for(auto const &ins : pair.second.body.instructions) { - if(ins.get_code().is_not_nil()) - log.status() << ins.get_code().pretty() << messaget::eom; + if(ins.code().is_not_nil()) + log.status() << ins.code().pretty() << messaget::eom; if(ins.has_condition()) { log.status() << "[guard] " << ins.condition().pretty() diff --git a/src/goto-instrument/wmm/fence.cpp b/src/goto-instrument/wmm/fence.cpp index 55795f4df4c..7ea127db240 100644 --- a/src/goto-instrument/wmm/fence.cpp +++ b/src/goto-instrument/wmm/fence.cpp @@ -25,11 +25,11 @@ bool is_fence( "fence") /* if assembly-sensitive algorithms are not available */ || (instruction.is_other() && - instruction.get_code().get_statement() == ID_fence && - instruction.get_code().get_bool(ID_WWfence) && - instruction.get_code().get_bool(ID_WRfence) && - instruction.get_code().get_bool(ID_RWfence) && - instruction.get_code().get_bool(ID_RRfence)); + instruction.code().get_statement() == ID_fence && + instruction.code().get_bool(ID_WWfence) && + instruction.code().get_bool(ID_WRfence) && + instruction.code().get_bool(ID_RWfence) && + instruction.code().get_bool(ID_RRfence)); } bool is_lwfence( @@ -41,8 +41,8 @@ bool is_lwfence( "lwfence") /* if assembly-sensitive algorithms are not available */ || (instruction.is_other() && - instruction.get_code().get_statement() == ID_fence && - instruction.get_code().get_bool(ID_WWfence) && - instruction.get_code().get_bool(ID_RWfence) && - instruction.get_code().get_bool(ID_RRfence)); + instruction.code().get_statement() == ID_fence && + instruction.code().get_bool(ID_WWfence) && + instruction.code().get_bool(ID_RWfence) && + instruction.code().get_bool(ID_RRfence)); } diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 19e941cf308..08e6c6bed47 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -235,8 +235,7 @@ void instrumentert::cfg_visitort::visit_cfg_function( visit_cfg_skip(i_it); } else if( - instruction.is_other() && - instruction.get_code().get_statement() == ID_fence) + instruction.is_other() && instruction.code().get_statement() == ID_fence) { visit_cfg_asm_fence(i_it, function_id); } @@ -792,13 +791,13 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence( const irep_idt &function_id) { const goto_programt::instructiont &instruction=*i_it; - bool WRfence = instruction.get_code().get_bool(ID_WRfence); - bool WWfence = instruction.get_code().get_bool(ID_WWfence); - bool RRfence = instruction.get_code().get_bool(ID_RRfence); - bool RWfence = instruction.get_code().get_bool(ID_RWfence); - bool WWcumul = instruction.get_code().get_bool(ID_WWcumul); - bool RRcumul = instruction.get_code().get_bool(ID_RRcumul); - bool RWcumul = instruction.get_code().get_bool(ID_RWcumul); + bool WRfence = instruction.code().get_bool(ID_WRfence); + bool WWfence = instruction.code().get_bool(ID_WWfence); + bool RRfence = instruction.code().get_bool(ID_RRfence); + bool RWfence = instruction.code().get_bool(ID_RWfence); + bool WWcumul = instruction.code().get_bool(ID_WWcumul); + bool RRcumul = instruction.code().get_bool(ID_RRcumul); + bool RWcumul = instruction.code().get_bool(ID_RWcumul); const abstract_eventt new_fence_event( abstract_eventt::operationt::ASMfence, thread, diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 5713924b18f..05e279cbfe4 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -282,7 +282,7 @@ void shared_bufferst::write( target, source_location, vars.w_buff0, - original_instruction.get_code().op1()); + original_instruction.code().op1()); // We update the used flags assignment( @@ -1219,7 +1219,7 @@ void shared_bufferst::cfg_visitort::weak_memory( choice1_expr, dereference_exprt{new_read_expr}, to_replace_expr), - to_replace_expr); // original_instruction.get_code().op1()); + to_replace_expr); // original_instruction.code().op1()); shared_buffers.assignment( goto_program, @@ -1237,7 +1237,7 @@ void shared_bufferst::cfg_visitort::weak_memory( i_it, source_location, w_entry.second.object, - original_instruction.get_code().op1()); + original_instruction.code().op1()); } } @@ -1286,11 +1286,11 @@ void shared_bufferst::cfg_visitort::weak_memory( else if( is_fence(instruction, ns) || (instruction.is_other() && - instruction.get_code().get_statement() == ID_fence && - (instruction.get_code().get_bool("WRfence") || - instruction.get_code().get_bool("WWfence") || - instruction.get_code().get_bool("RWfence") || - instruction.get_code().get_bool("RRfence")))) + instruction.code().get_statement() == ID_fence && + (instruction.code().get_bool("WRfence") || + instruction.code().get_bool("WWfence") || + instruction.code().get_bool("RWfence") || + instruction.code().get_bool("RRfence")))) { goto_programt::instructiont original_instruction; original_instruction.swap(instruction); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 55567c9bb24..60e88072ce6 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -60,7 +60,7 @@ static void finish_catch_push_targets(goto_programt &dest) { if( instruction.is_catch() && - instruction.get_code().get_statement() == ID_push_catch) + instruction.code().get_statement() == ID_push_catch) { // Populate `targets` with a GOTO instruction target per // exception handler if it isn't already populated. @@ -71,7 +71,7 @@ static void finish_catch_push_targets(goto_programt &dest) { bool handler_added=true; const code_push_catcht::exception_listt &handler_list = - to_code_push_catch(instruction.get_code()).exception_list(); + to_code_push_catch(instruction.code()).exception_list(); for(const auto &handler : handler_list) { @@ -114,7 +114,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) if(i.is_start_thread()) { - const irep_idt &goto_label = i.get_code().get(ID_destination); + const irep_idt &goto_label = i.code().get(ID_destination); labelst::const_iterator l_it= targets.labels.find(goto_label); @@ -123,14 +123,14 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) { throw incorrect_goto_program_exceptiont( "goto label \'" + id2string(goto_label) + "\' not found", - i.get_code().find_source_location()); + i.code().find_source_location()); } i.targets.push_back(l_it->second.first); } else if(i.is_incomplete_goto()) { - const irep_idt &goto_label = i.get_code().get(ID_destination); + const irep_idt &goto_label = i.code().get(ID_destination); labelst::const_iterator l_it=targets.labels.find(goto_label); @@ -138,7 +138,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) { throw incorrect_goto_program_exceptiont( "goto label \'" + id2string(goto_label) + "\' not found", - i.get_code().find_source_location()); + i.code().find_source_location()); } i.complete_goto(l_it->second.first); @@ -204,7 +204,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) for(auto &g_it : targets.computed_gotos) { goto_programt::instructiont &i=*g_it; - dereference_exprt destination = to_dereference_expr(i.get_code().op0()); + dereference_exprt destination = to_dereference_expr(i.code().op0()); const exprt pointer = destination.pointer(); // remember the expression for later checks diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 8ef40e45b27..eb47b2da203 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -206,33 +206,33 @@ std::ostream &goto_programt::output_instruction( { const irept::subt &exception_list = - instruction.get_code().find(ID_exception_list).get_sub(); + instruction.code().find(ID_exception_list).get_sub(); for(const auto &ex : exception_list) out << " " << ex.id(); } - if(instruction.get_code().operands().size() == 1) - out << ": " << format(instruction.get_code().op0()); + if(instruction.code().operands().size() == 1) + out << ": " << format(instruction.code().op0()); out << '\n'; break; case CATCH: { - if(instruction.get_code().get_statement() == ID_exception_landingpad) + if(instruction.code().get_statement() == ID_exception_landingpad) { - const auto &landingpad = to_code_landingpad(instruction.get_code()); + const auto &landingpad = to_code_landingpad(instruction.code()); out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type()) << ' ' << format(landingpad.catch_expr()) << ")"; } - else if(instruction.get_code().get_statement() == ID_push_catch) + else if(instruction.code().get_statement() == ID_push_catch) { out << "CATCH-PUSH "; unsigned i=0; const irept::subt &exception_list = - instruction.get_code().find(ID_exception_list).get_sub(); + instruction.code().find(ID_exception_list).get_sub(); DATA_INVARIANT( instruction.targets.size() == exception_list.size(), "unexpected discrepancy between sizes of instruction" @@ -248,7 +248,7 @@ std::ostream &goto_programt::output_instruction( << (*gt_it)->target_number; } } - else if(instruction.get_code().get_statement() == ID_pop_catch) + else if(instruction.code().get_statement() == ID_pop_catch) { out << "CATCH-POP"; } @@ -291,10 +291,10 @@ void goto_programt::get_decl_identifiers( if(instruction.is_decl()) { DATA_INVARIANT( - instruction.get_code().get_statement() == ID_decl, + instruction.code().get_statement() == ID_decl, "expected statement to be declaration statement"); DATA_INVARIANT( - instruction.get_code().operands().size() == 1, + instruction.code().operands().size() == 1, "declaration statement expects one operand"); decl_identifiers.insert(instruction.decl_symbol().get_identifier()); } @@ -516,7 +516,7 @@ std::string as_string( case DEAD: case FUNCTION_CALL: case ASSIGN: - return from_expr(ns, function, i.get_code()); + return from_expr(ns, function, i.code()); case ASSUME: case ASSERT: @@ -744,7 +744,7 @@ bool goto_programt::instructiont::equals(const instructiont &other) const // clang-format off return _type == other._type && - code == other.code && + _code == other._code && guard == other.guard && targets.size() == other.targets.size() && labels == other.labels; @@ -755,7 +755,7 @@ void goto_programt::instructiont::validate( const namespacet &ns, const validation_modet vm) const { - validate_full_code(code, ns, vm); + validate_full_code(_code, ns, vm); validate_full_expr(guard, ns, vm); auto expr_symbol_finder = [&](const exprt &e) { @@ -895,14 +895,14 @@ void goto_programt::instructiont::validate( case SET_RETURN_VALUE: DATA_CHECK_WITH_DIAGNOSTICS( vm, - code.get_statement() == ID_return, + _code.get_statement() == ID_return, "SET_RETURN_VALUE instruction should contain a return statement", source_location()); break; case ASSIGN: DATA_CHECK( vm, - code.get_statement() == ID_assign, + _code.get_statement() == ID_assign, "assign instruction should contain an assign statement"); DATA_CHECK( vm, targets.empty(), "assign instruction should not have a target"); @@ -910,7 +910,7 @@ void goto_programt::instructiont::validate( case DECL: DATA_CHECK_WITH_DIAGNOSTICS( vm, - code.get_statement() == ID_decl, + _code.get_statement() == ID_decl, "declaration instructions should contain a declaration statement", source_location()); DATA_CHECK_WITH_DIAGNOSTICS( @@ -923,7 +923,7 @@ void goto_programt::instructiont::validate( case DEAD: DATA_CHECK_WITH_DIAGNOSTICS( vm, - code.get_statement() == ID_dead, + _code.get_statement() == ID_dead, "dead instructions should contain a dead statement", source_location()); DATA_CHECK_WITH_DIAGNOSTICS( @@ -936,12 +936,12 @@ void goto_programt::instructiont::validate( case FUNCTION_CALL: DATA_CHECK_WITH_DIAGNOSTICS( vm, - code.get_statement() == ID_function_call, + _code.get_statement() == ID_function_call, "function call instruction should contain a call statement", source_location()); - std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder); - std::for_each(code.depth_begin(), code.depth_end(), type_finder); + std::for_each(_code.depth_begin(), _code.depth_end(), expr_symbol_finder); + std::for_each(_code.depth_begin(), _code.depth_end(), type_finder); break; case THROW: break; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 25d0b1b9073..676eeb682ea 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -180,55 +180,62 @@ class goto_programt class instructiont final { protected: - /// Do not read or modify directly -- use get_X() instead - goto_instruction_codet code; + /// Do not read or modify directly -- use code() and code_nonconst() instead + goto_instruction_codet _code; public: /// Get the code represented by this instruction + DEPRECATED(SINCE(2021, 10, 12, "Use code() instead")) const goto_instruction_codet &get_code() const { - return code; + return _code; + } + + /// Get the code represented by this instruction + const goto_instruction_codet &code() const + { + return _code; } /// Set the code represented by this instruction goto_instruction_codet &code_nonconst() { - return code; + return _code; } /// Get the lhs of the assignment for ASSIGN const exprt &assign_lhs() const { PRECONDITION(is_assign()); - return to_code_assign(code).lhs(); + return to_code_assign(_code).lhs(); } /// Get the lhs of the assignment for ASSIGN exprt &assign_lhs_nonconst() { PRECONDITION(is_assign()); - return to_code_assign(code).lhs(); + return to_code_assign(_code).lhs(); } /// Get the rhs of the assignment for ASSIGN const exprt &assign_rhs() const { PRECONDITION(is_assign()); - return to_code_assign(code).rhs(); + return to_code_assign(_code).rhs(); } /// Get the rhs of the assignment for ASSIGN exprt &assign_rhs_nonconst() { PRECONDITION(is_assign()); - return to_code_assign(code).rhs(); + return to_code_assign(_code).rhs(); } /// Get the declared symbol for DECL const symbol_exprt &decl_symbol() const { PRECONDITION(is_decl()); - auto &decl = expr_checked_cast(code); + auto &decl = expr_checked_cast(_code); return decl.symbol(); } @@ -236,7 +243,7 @@ class goto_programt symbol_exprt &decl_symbol() { PRECONDITION(is_decl()); - auto &decl = expr_checked_cast(code); + auto &decl = expr_checked_cast(_code); return decl.symbol(); } @@ -244,84 +251,84 @@ class goto_programt const symbol_exprt &dead_symbol() const { PRECONDITION(is_dead()); - return to_code_dead(code).symbol(); + return to_code_dead(_code).symbol(); } /// Get the symbol for DEAD symbol_exprt &dead_symbol() { PRECONDITION(is_dead()); - return to_code_dead(code).symbol(); + return to_code_dead(_code).symbol(); } /// Get the return value of a SET_RETURN_VALUE instruction const exprt &return_value() const { PRECONDITION(is_set_return_value()); - return to_code_return(code).return_value(); + return to_code_return(_code).return_value(); } /// Get the return value of a SET_RETURN_VALUE instruction exprt &return_value() { PRECONDITION(is_set_return_value()); - return to_code_return(code).return_value(); + return to_code_return(_code).return_value(); } /// Get the function that is called for FUNCTION_CALL const exprt &call_function() const { PRECONDITION(is_function_call()); - return to_code_function_call(code).function(); + return to_code_function_call(_code).function(); } /// Get the function that is called for FUNCTION_CALL exprt &call_function() { PRECONDITION(is_function_call()); - return to_code_function_call(code).function(); + return to_code_function_call(_code).function(); } /// Get the lhs of a FUNCTION_CALL (may be nil) const exprt &call_lhs() const { PRECONDITION(is_function_call()); - return to_code_function_call(code).lhs(); + return to_code_function_call(_code).lhs(); } /// Get the lhs of a FUNCTION_CALL (may be nil) exprt &call_lhs() { PRECONDITION(is_function_call()); - return to_code_function_call(code).lhs(); + return to_code_function_call(_code).lhs(); } /// Get the arguments of a FUNCTION_CALL const exprt::operandst &call_arguments() const { PRECONDITION(is_function_call()); - return to_code_function_call(code).arguments(); + return to_code_function_call(_code).arguments(); } /// Get the arguments of a FUNCTION_CALL exprt::operandst &call_arguments() { PRECONDITION(is_function_call()); - return to_code_function_call(code).arguments(); + return to_code_function_call(_code).arguments(); } /// Get the statement for OTHER const goto_instruction_codet &get_other() const { PRECONDITION(is_other()); - return code; + return _code; } /// Set the statement for OTHER void set_other(goto_instruction_codet &c) { PRECONDITION(is_other()); - code = std::move(c); + _code = std::move(c); } /// The location of the instruction in the source file. @@ -425,7 +432,7 @@ class goto_programt _type = __type; targets.clear(); guard=true_exprt(); - code.make_nil(); + _code.make_nil(); } /// Transforms an existing instruction into a skip, @@ -442,13 +449,13 @@ class goto_programt PRECONDITION(_type == GOTO || _type == ASSERT); _type = ASSUME; targets.clear(); - code.make_nil(); + _code.make_nil(); } void complete_goto(targett _target) { PRECONDITION(_type == INCOMPLETE_GOTO); - code.make_nil(); + _code.make_nil(); targets.push_back(_target); _type = GOTO; } @@ -481,7 +488,7 @@ class goto_programt } explicit instructiont(goto_program_instruction_typet __type) - : code(static_cast(get_nil_irep())), + : _code(static_cast(get_nil_irep())), _source_location(source_locationt::nil()), _type(__type), guard(true_exprt()) @@ -490,12 +497,12 @@ class goto_programt /// Constructor that can set all members, passed by value instructiont( - goto_instruction_codet _code, + goto_instruction_codet __code, source_locationt __source_location, goto_program_instruction_typet __type, exprt _guard, targetst _targets) - : code(std::move(_code)), + : _code(std::move(__code)), _source_location(std::move(__source_location)), _type(__type), guard(std::move(_guard)), @@ -507,7 +514,7 @@ class goto_programt void swap(instructiont &instruction) { using std::swap; - swap(instruction.code, code); + swap(instruction._code, _code); swap(instruction._source_location, _source_location); swap(instruction._type, _type); swap(instruction.guard, guard); diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index f93ab27d0e5..9fb07183076 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -388,15 +388,15 @@ void interpretert::execute_other() if(statement==ID_expression) { DATA_INVARIANT( - pc->get_code().operands().size() == 1, + pc->code().operands().size() == 1, "expression statement expected to have one operand"); - mp_vectort rhs = evaluate(pc->get_code().op0()); + mp_vectort rhs = evaluate(pc->code().op0()); } else if(statement==ID_array_set) { - mp_vectort tmp = evaluate(pc->get_code().op1()); - mp_integer address = evaluate_address(pc->get_code().op0()); - mp_integer size = get_size(pc->get_code().op0().type()); + mp_vectort tmp = evaluate(pc->code().op1()); + mp_integer address = evaluate_address(pc->code().op0()); + mp_integer size = get_size(pc->code().op0().type()); mp_vectort rhs; while(rhs.size()get_code().get_statement() == ID_decl); + PRECONDITION(pc->code().get_statement() == ID_decl); } /// Retrieves the member at \p offset of an object of type \p object_type. diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 13a9e4fc065..2d47e827b75 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -119,7 +119,7 @@ void remove_returnst::replace_returns( if(instruction.is_set_return_value()) { INVARIANT( - instruction.get_code().operands().size() == 1, + instruction.code().operands().size() == 1, "return instructions should have one operand"); if(return_symbol.has_value()) diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 5e213840233..604a80ee990 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -33,7 +33,7 @@ bool is_skip( return false; if(it->is_skip()) - return !it->get_code().get_bool(ID_explicit); + return !it->code().get_bool(ID_explicit); if(it->is_goto()) { @@ -62,8 +62,7 @@ bool is_skip( return true; else if(statement==ID_expression) { - const code_expressiont &code_expression = - to_code_expression(it->get_code()); + const code_expressiont &code_expression = to_code_expression(it->code()); const exprt &expr=code_expression.expression(); if(expr.id()==ID_typecast && expr.type().id()==ID_empty && diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 209d851efd1..9c2d8f3e3e1 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -69,10 +69,10 @@ json_objectt show_goto_functions_jsont::convert( json_objectt instruction_entry{ {"instructionId", json_stringt(instruction.to_string())}}; - if(instruction.get_code().source_location().is_not_nil()) + if(instruction.code().source_location().is_not_nil()) { instruction_entry["sourceLocation"] = - json(instruction.get_code().source_location()); + json(instruction.code().source_location()); } std::ostringstream instruction_builder; @@ -82,10 +82,10 @@ json_objectt show_goto_functions_jsont::convert( instruction_entry["instruction"]= json_stringt(instruction_builder.str()); - if(!instruction.get_code().operands().empty()) + if(!instruction.code().operands().empty()) { json_arrayt operand_array; - for(const exprt &operand : instruction.get_code().operands()) + for(const exprt &operand : instruction.code().operands()) { json_objectt operand_object= no_comments_irep_converter.convert_from_irep( diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index e4bfdad105a..3821ee8cf2a 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -74,10 +74,10 @@ xmlt show_goto_functions_xmlt::convert( instruction_entry.set_attribute( "instruction_id", instruction.to_string()); - if(instruction.get_code().source_location().is_not_nil()) + if(instruction.code().source_location().is_not_nil()) { instruction_entry.new_element( - xml(instruction.get_code().source_location())); + xml(instruction.code().source_location())); } std::ostringstream instruction_builder; diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 7fc772b1b7d..4048c679d20 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -133,7 +133,7 @@ void validate_goto_modelt::check_called_functions() } // check functions of which the address is taken - const auto &src = static_cast(instr.get_code()); + const auto &src = static_cast(instr.code()); src.visit_pre(test_for_function_address); } } diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 4355bc3c459..939ddf046b4 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -95,7 +95,7 @@ bool write_goto_binary( for(const auto &instruction : fct.second.body.instructions) { - irepconverter.reference_convert(instruction.get_code(), out); + irepconverter.reference_convert(instruction.code(), out); irepconverter.reference_convert(instruction.source_location(), out); write_gb_word(out, (long)instruction.type()); diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index c6ab22b65a7..6830f352344 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -172,7 +172,7 @@ static void update_internal_field( // "__CPROVER_*" function calls in __CPROVER_start are already marked as // internal. Don't mark any other function calls (i.e. "main"), function // arguments or any other parts of a code_function_callt as internal. - if(SSA_step.source.pc->get_code().get_statement() != ID_function_call) + if(SSA_step.source.pc->code().get_statement() != ID_function_call) goto_trace_step.internal=true; } } diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index d26a9182a2c..54d6b58b677 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -108,7 +108,7 @@ void memory_model_tsot::program_order( if((*e_it2)->is_memory_barrier()) { - const codet &code = (*e_it2)->source.pc->get_code(); + const codet &code = (*e_it2)->source.pc->code(); if((*e_it)->is_shared_read() && !code.get_bool(ID_RRfence) && diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp index 9c75a200af1..ef8fcb4a951 100644 --- a/src/goto-symex/solver_hardness.cpp +++ b/src/goto-symex/solver_hardness.cpp @@ -277,7 +277,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) case DEAD: case FUNCTION_CALL: case ASSIGN: - out << format(instruction.get_code()); + out << format(instruction.code()); break; case ASSUME: @@ -307,32 +307,32 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) { const irept::subt &exception_list = - instruction.get_code().find(ID_exception_list).get_sub(); + instruction.code().find(ID_exception_list).get_sub(); for(const auto &ex : exception_list) out << " " << ex.id(); } - if(instruction.get_code().operands().size() == 1) - out << ": " << format(instruction.get_code().op0()); + if(instruction.code().operands().size() == 1) + out << ": " << format(instruction.code().op0()); break; case CATCH: { - if(instruction.get_code().get_statement() == ID_exception_landingpad) + if(instruction.code().get_statement() == ID_exception_landingpad) { - const auto &landingpad = to_code_landingpad(instruction.get_code()); + const auto &landingpad = to_code_landingpad(instruction.code()); out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type()) << ' ' << format(landingpad.catch_expr()) << ")"; } - else if(instruction.get_code().get_statement() == ID_push_catch) + else if(instruction.code().get_statement() == ID_push_catch) { out << "CATCH-PUSH "; unsigned i = 0; const irept::subt &exception_list = - instruction.get_code().find(ID_exception_list).get_sub(); + instruction.code().find(ID_exception_list).get_sub(); DATA_INVARIANT( instruction.targets.size() == exception_list.size(), "unexpected discrepancy between sizes of instruction" @@ -346,7 +346,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) out << exception_list[i].id() << "->" << (*gt_it)->target_number; } } - else if(instruction.get_code().get_statement() == ID_pop_catch) + else if(instruction.code().get_statement() == ID_pop_catch) { out << "CATCH-POP"; } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 5439cc6a228..5c5b59967b1 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -340,7 +340,7 @@ void goto_symext::symex_goto(statet &state) DATA_INVARIANT( instruction.targets.size() > 0, "Instruction is an unconditional goto with no target: " + - instruction.get_code().pretty()); + instruction.code().pretty()); symex_transition(state, instruction.get_target(), true); return; } @@ -383,13 +383,13 @@ void goto_symext::symex_goto(statet &state) "Tried to explore the other path of a branch, but the next " "instruction along that path is not the same as the instruction " "that we saved at the branch point. Saved instruction is " + - state.saved_target->get_code().pretty() + + state.saved_target->code().pretty() + "\nwe were intending " "to explore " + - new_state_pc->get_code().pretty() + + new_state_pc->code().pretty() + "\nthe " "instruction we think we saw on a previous path exploration is " + - state_pc->get_code().pretty()); + state_pc->code().pretty()); goto_programt::const_targett tmp = new_state_pc; new_state_pc = state_pc; state_pc = tmp; diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 648de566760..3be0f67f28e 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -515,13 +515,13 @@ void goto_symext::print_symex_step(statet &state) if( !symex_config.show_symex_steps || !state.reachable || state.source.pc->type() == DEAD || - (state.source.pc->get_code().is_nil() && + (state.source.pc->code().is_nil() && state.source.pc->type() != END_FUNCTION)) { return; } - if(state.source.pc->get_code().is_not_nil()) + if(state.source.pc->code().is_not_nil()) { auto guard_expression = state.guard.as_expr(); std::size_t size = 0; @@ -533,7 +533,7 @@ void goto_symext::print_symex_step(statet &state) } log.status() << "[Guard size: " << size << "] " - << format(state.source.pc->get_code()); + << format(state.source.pc->code()); if( state.source.pc->source_location().is_not_nil() && diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index a77154ebcd3..9e45e057fd0 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -88,7 +88,7 @@ void value_set_domain_templatet::transform( case ASSIGN: case DECL: case DEAD: - value_set.apply_code(from_l->get_code(), ns); + value_set.apply_code(from_l->code(), ns); break; case ASSUME: diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index eaff53f58fc..a0d88d9f81c 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -43,7 +43,7 @@ bool value_set_domain_fit::transform( case SET_RETURN_VALUE: case OTHER: case ASSIGN: - value_set.apply_code(from_l->get_code(), ns); + value_set.apply_code(from_l->code(), ns); break; case FUNCTION_CALL: diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index 978f517d5d9..03bf2661e7b 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -55,8 +55,7 @@ SCENARIO( { code_function_callt function_call(var_a, fun_foo, {}); instructions.back() = goto_programt::make_function_call(function_call); - REQUIRE( - instructions.back().get_code().get_statement() == ID_function_call); + REQUIRE(instructions.back().code().get_statement() == ID_function_call); THEN("The consistency check succeeds") {