diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index b4e4232f43d..d361272f09f 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -761,37 +761,50 @@ void constant_propagator_ait::replace( { exprt c = it->get_condition(); replace_types_rec(d.values.replace_const, c); - constant_propagator_domaint::partial_evaluate(d.values, c, ns); - it->set_condition(c); + if(!constant_propagator_domaint::partial_evaluate(d.values, c, ns)) + it->set_condition(c); } else if(it->is_assign()) { - exprt &rhs=to_code_assign(it->code).rhs(); - constant_propagator_domaint::partial_evaluate(d.values, rhs, ns); + auto assign = it->get_assign(); + exprt &rhs = assign.rhs(); - if(rhs.id()==ID_constant) - rhs.add_source_location() = - to_code_assign(it->code).lhs().source_location(); + if(!constant_propagator_domaint::partial_evaluate(d.values, rhs, ns)) + { + if(rhs.id() == ID_constant) + rhs.add_source_location() = assign.lhs().source_location(); + it->set_assign(assign); + } } else if(it->is_function_call()) { - exprt &function = to_code_function_call(it->code).function(); - constant_propagator_domaint::partial_evaluate(d.values, function, ns); + auto call = it->get_function_call(); - exprt::operandst &args= - to_code_function_call(it->code).arguments(); + bool call_changed = false; - for(auto &arg : args) + if(!constant_propagator_domaint::partial_evaluate( + d.values, call.function(), ns)) { - constant_propagator_domaint::partial_evaluate(d.values, arg, ns); + call_changed = true; } + + for(auto &arg : call.arguments()) + if(!constant_propagator_domaint::partial_evaluate(d.values, arg, ns)) + call_changed = true; + + if(call_changed) + it->set_function_call(call); } else if(it->is_other()) { if(it->get_other().get_statement() == ID_expression) { - constant_propagator_domaint::partial_evaluate( - d.values, it->get_other(), ns); + auto c = to_code_expression(it->get_other()); + if(!constant_propagator_domaint::partial_evaluate( + d.values, c.expression(), ns)) + { + it->set_other(c); + } } } } diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 7ff249b5639..f8aa0749f72 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -95,7 +95,7 @@ bool static_simplifier( } else if(i_it->is_assign()) { - code_assignt &assign = i_it->get_assign(); + auto assign = i_it->get_assign(); // Simplification needs to be aware of which side of the // expression it is handling as: @@ -111,11 +111,14 @@ bool static_simplifier( if(unchanged_lhs && unchanged_rhs) unmodified.assigns++; else + { simplified.assigns++; + i_it->set_assign(assign); + } } else if(i_it->is_function_call()) { - code_function_callt &fcall = i_it->get_function_call(); + auto fcall = i_it->get_function_call(); bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns); @@ -128,7 +131,10 @@ bool static_simplifier( if(unchanged) unmodified.function_calls++; else + { simplified.function_calls++; + i_it->set_function_call(fcall); + } } } } diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 2d3597cb527..3a8d70f3135 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -188,11 +188,11 @@ class goto_programt return to_code_assign(code); } - /// Get the assignment for ASSIGN - code_assignt &get_assign() + /// Set the assignment for ASSIGN + void set_assign(code_assignt c) { PRECONDITION(is_assign()); - return to_code_assign(code); + code = std::move(c); } /// Get the declaration for DECL @@ -202,11 +202,11 @@ class goto_programt return to_code_decl(code); } - /// Get the declaration for DECL - code_declt &get_decl() + /// Set the declaration for DECL + void set_decl(code_declt c) { PRECONDITION(is_decl()); - return to_code_decl(code); + code = std::move(c); } /// Get the dead statement for DEAD @@ -216,11 +216,11 @@ class goto_programt return to_code_dead(code); } - /// Get the dead statement for DEAD - code_deadt &get_dead() + /// Set the dead statement for DEAD + void set_dead(code_deadt c) { PRECONDITION(is_dead()); - return to_code_dead(code); + code = std::move(c); } /// Get the return statement for READ @@ -230,11 +230,11 @@ class goto_programt return to_code_return(code); } - /// Get the return statement for READ - code_returnt &get_return() + /// Set the return statement for READ + void set_return(code_returnt c) { PRECONDITION(is_return()); - return to_code_return(code); + code = std::move(c); } /// Get the function call for FUNCTION_CALL @@ -244,11 +244,11 @@ class goto_programt return to_code_function_call(code); } - /// Get the function call for FUNCTION_CALL - code_function_callt &get_function_call() + /// Set the function call for FUNCTION_CALL + void set_function_call(code_function_callt c) { PRECONDITION(is_function_call()); - return to_code_function_call(code); + code = std::move(c); } /// Get the statement for OTHER @@ -258,11 +258,11 @@ class goto_programt return code; } - /// Get the statement for OTHER - codet &get_other() + /// Set the statement for OTHER + void set_other(codet &c) { PRECONDITION(is_other()); - return code; + code = std::move(c); } /// The location of the instruction in the source file diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 3c5d6b28e7f..cc4d6c6b976 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -45,7 +45,7 @@ void mm_io( if(it->is_assign()) { - auto &a = it->get_assign(); + auto a = it->get_assign(); collect_deref_expr(a.rhs(), deref_expr_r); if(mm_io_r.is_not_nil()) @@ -60,7 +60,8 @@ void mm_io( irep_idt r_identifier=id2string(identifier)+RETURN_VALUE_SUFFIX; symbol_exprt return_value(r_identifier, ct.return_type()); if_exprt if_expr(integer_address(d.pointer()), return_value, d); - replace_expr(d, if_expr, a.rhs()); + if(!replace_expr(d, if_expr, a.rhs())) + it->set_assign(a); const typet &pt=ct.parameters()[0].type(); const typet &st=ct.parameters()[1].type(); diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 99ae6bab71b..6f23b39384a 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -319,7 +319,9 @@ void remove_function_pointerst::remove_function_pointer( if(functions.size()==1) { - target->get_function_call().function() = *functions.cbegin(); + auto call = target->get_function_call(); + call.function() = *functions.cbegin(); + target->set_function_call(call); return; } } @@ -386,14 +388,18 @@ void remove_function_pointerst::remove_function_pointer( for(const auto &fun : functions) { // call function - goto_programt::targett t1 = - new_code_calls.add(goto_programt::make_function_call(code)); - t1->get_function_call().function() = fun; + auto new_call = code; + new_call.function() = fun; // the signature of the function might not match precisely - fix_argument_types(t1->get_function_call()); + fix_argument_types(new_call); + + goto_programt tmp; + fix_return_type(function_id, new_call, tmp); + + auto call = new_code_calls.add(goto_programt::make_function_call(new_call)); + new_code_calls.destructive_append(tmp); - fix_return_type(function_id, t1->get_function_call(), new_code_calls); // goto final new_code_calls.add(goto_programt::make_goto(t_final, true_exprt())); @@ -404,7 +410,7 @@ void remove_function_pointerst::remove_function_pointer( typecast_exprt::conditional_cast(address_of, pointer.type()); new_code_gotos.add( - goto_programt::make_goto(t1, equal_exprt(pointer, casted_address))); + goto_programt::make_goto(call, equal_exprt(pointer, casted_address))); } // fall-through diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 415d64d5039..b48c02b9557 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -150,7 +150,7 @@ void remove_returnst::do_function_calls( { if(i_it->is_function_call()) { - code_function_callt &function_call = i_it->get_function_call(); + code_function_callt function_call = i_it->get_function_call(); INVARIANT( function_call.function().id() == ID_symbol, @@ -222,6 +222,9 @@ void remove_returnst::do_function_calls( goto_programt::make_dead(*return_value, i_it->source_location)); } } + + // update the call + i_it->set_function_call(function_call); } } } @@ -355,7 +358,8 @@ bool remove_returnst::restore_returns( { if(i_it->is_assign()) { - code_assignt &assign = i_it->get_assign(); + const auto &assign = i_it->get_assign(); + if(assign.lhs().id()!=ID_symbol || to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id) continue; @@ -384,7 +388,7 @@ void remove_returnst::undo_function_calls( { if(i_it->is_function_call()) { - code_function_callt &function_call = i_it->get_function_call(); + code_function_callt function_call = i_it->get_function_call(); // ignore function pointers if(function_call.function().id()!=ID_symbol) @@ -401,8 +405,8 @@ void remove_returnst::undo_function_calls( // find "f(...); lhs=f#return_value; DEAD f#return_value;" // and revert to "lhs=f(...);" - goto_programt::instructionst::iterator next=i_it; - ++next; + goto_programt::instructionst::iterator next = std::next(i_it); + INVARIANT( next!=goto_program.instructions.end(), "non-void function call must be followed by #return_value read"); @@ -423,6 +427,8 @@ void remove_returnst::undo_function_calls( // restore the previous assignment function_call.lhs()=assign.lhs(); + i_it->set_function_call(function_call); + // remove the assignment and subsequent dead // i_it remains valid next=goto_program.instructions.erase(next); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 0677fabf964..9405a7f59d9 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -190,8 +190,9 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( } else { - create_static_function_call( - target->get_function_call(), *functions.front().symbol_expr, ns); + auto c = target->get_function_call(); + create_static_function_call(c, *functions.front().symbol_expr, ns); + target->set_function_call(c); } return next_target; } @@ -250,11 +251,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( if(fun.symbol_expr.has_value()) { // call function - goto_programt::targett t1 = new_code_calls.add( - goto_programt::make_function_call(code, vcall_source_loc)); + auto new_call = code; + + create_static_function_call(new_call, *fun.symbol_expr, ns); - create_static_function_call( - t1->get_function_call(), *fun.symbol_expr, ns); + goto_programt::targett t1 = new_code_calls.add( + goto_programt::make_function_call(new_call, vcall_source_loc)); insertit.first->second = t1; } diff --git a/src/goto-programs/replace_calls.cpp b/src/goto-programs/replace_calls.cpp index 954f7f62cb8..b2adf3baa27 100644 --- a/src/goto-programs/replace_calls.cpp +++ b/src/goto-programs/replace_calls.cpp @@ -70,7 +70,7 @@ void replace_callst::operator()( if(!ins.is_function_call()) continue; - code_function_callt &cfc = ins.get_function_call(); + auto cfc = ins.get_function_call(); exprt &function = cfc.function(); PRECONDITION(function.id() == ID_symbol); @@ -114,6 +114,8 @@ void replace_callst::operator()( // Finally modify the call function.type() = f_it2->second.type; se.set_identifier(new_id); + + ins.set_function_call(cfc); } } diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index d9ac1469244..613d38ecc59 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -489,22 +489,27 @@ goto_programt::targett string_abstractiont::abstract_assign( goto_programt &dest, goto_programt::targett target) { - code_assignt &assign = target->get_assign(); + { + code_assignt assign = target->get_assign(); - exprt &lhs=assign.lhs(); - exprt &rhs=assign.rhs(); + exprt &lhs = assign.lhs(); + exprt &rhs = assign.rhs(); - if(has_string_macros(lhs)) - { - replace_string_macros(lhs, true, target->source_location); - move_lhs_arithmetic(lhs, rhs); + if(has_string_macros(lhs)) + { + replace_string_macros(lhs, true, target->source_location); + move_lhs_arithmetic(lhs, rhs); + } + + if(has_string_macros(rhs)) + replace_string_macros(rhs, false, target->source_location); + + target->set_assign(assign); } - if(has_string_macros(rhs)) - replace_string_macros(rhs, false, target->source_location); + const typet &type = target->get_assign().lhs().type(); - const typet &type = lhs.type(); - if(type.id()==ID_pointer || type.id()==ID_array) + if(type.id() == ID_pointer) return abstract_pointer_assign(dest, target); else if(is_char_type(type)) return abstract_char_assign(dest, target); @@ -515,7 +520,8 @@ goto_programt::targett string_abstractiont::abstract_assign( void string_abstractiont::abstract_function_call( goto_programt::targett target) { - code_function_callt &call = target->get_function_call(); + code_function_callt call = target->get_function_call(); + code_function_callt::argumentst &arguments=call.arguments(); code_function_callt::argumentst str_args; @@ -563,6 +569,8 @@ void string_abstractiont::abstract_function_call( } arguments.insert(arguments.end(), str_args.begin(), str_args.end()); + + target->set_function_call(call); } bool string_abstractiont::has_string_macros(const exprt &expr) diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 6b8cc639843..fbe3870b96a 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -220,14 +220,14 @@ void goto_program_dereferencet::dereference_instruction( if(i.is_assign()) { - auto &assignment = i.get_assign(); - + auto assignment = i.get_assign(); dereference_expr(assignment.lhs(), checks_only); dereference_expr(assignment.rhs(), checks_only); + i.set_assign(assignment); } else if(i.is_function_call()) { - code_function_callt &function_call = i.get_function_call(); + code_function_callt function_call = i.get_function_call(); if(function_call.lhs().is_not_nil()) dereference_expr(function_call.lhs(), checks_only); @@ -236,15 +236,22 @@ void goto_program_dereferencet::dereference_instruction( for(auto &arg : function_call.arguments()) dereference_expr(arg, checks_only); + + i.set_function_call(function_call); } else if(i.is_return()) { - Forall_operands(it, i.get_return()) - dereference_expr(*it, checks_only); + auto r = i.get_return(); + + if(r.return_value().is_not_nil()) + { + dereference_expr(r.return_value(), checks_only); + i.set_return(r); + } } else if(i.is_other()) { - auto &code = i.get_other(); + auto code = i.get_other(); const irep_idt &statement = code.get_statement(); if(statement==ID_expression) @@ -252,13 +259,15 @@ void goto_program_dereferencet::dereference_instruction( if(code.operands().size() != 1) throw "expression expects one operand"; - dereference_expr(code.op0(), checks_only); + dereference_expr(to_code_expression(code).expression(), checks_only); } else if(statement==ID_printf) { for(auto &op : code.operands()) dereference_expr(op, checks_only); } + + i.set_other(code); } }