From cb2e20c2f3d49642ec9d34544577a616344f273b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Jul 2024 12:24:48 +0000 Subject: [PATCH] GOTO conversion: move out-only clean_expr parameter to return value Removes one side-effect of invoking clean_expr and instead expands on the return-value type. --- .../goto-conversion/builtin_functions.cpp | 10 +- .../goto-conversion/goto_clean_expr.cpp | 144 ++++++------ src/ansi-c/goto-conversion/goto_convert.cpp | 129 ++++++----- .../goto-conversion/goto_convert_class.h | 79 +++---- .../goto_convert_function_call.cpp | 12 +- .../goto_convert_side_effect.cpp | 210 ++++++++++-------- src/goto-instrument/contracts/utils.h | 4 +- 7 files changed, 308 insertions(+), 280 deletions(-) diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index ea6c30d173d..bf864fcdb1e 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -401,7 +401,7 @@ void goto_convertt::do_cpp_new( bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(new_array) { @@ -409,7 +409,8 @@ void goto_convertt::do_cpp_new( static_cast(rhs.find(ID_size)), object_size.type()); // might have side-effect - new_vars.add(clean_expr(count, dest, ID_cpp)); + side_effects.add(clean_expr(count, ID_cpp)); + dest.destructive_append(side_effects.side_effects); } exprt tmp_symbol_expr; @@ -495,9 +496,8 @@ void goto_convertt::do_cpp_new( typecast_exprt(tmp_symbol_expr, lhs.type()), rhs.find_source_location())); - new_vars.minimal_scope.push_front( - to_symbol_expr(tmp_symbol_expr).get_identifier()); - destruct_locals(new_vars.minimal_scope, dest, ns); + side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier()); + destruct_locals(side_effects.temporaries, dest, ns); // grab initializer goto_programt tmp_initializer; diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index d5569bb4b33..c015c1fe414 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -166,9 +166,8 @@ void goto_convertt::rewrite_boolean(exprt &expr) expr.swap(tmp); } -goto_convertt::needs_destructiont goto_convertt::clean_expr( +goto_convertt::clean_expr_resultt goto_convertt::clean_expr( exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -189,20 +188,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( rewrite_boolean(expr); // recursive call - return clean_expr(expr, dest, mode, result_is_used); + return clean_expr(expr, mode, result_is_used); } else if(expr.id() == ID_if) { // first clean condition - needs_destructiont new_vars = - clean_expr(to_if_expr(expr).cond(), dest, mode, true); + clean_expr_resultt side_effects = + clean_expr(to_if_expr(expr).cond(), mode, true); // possibly done now if( !needs_cleaning(to_if_expr(expr).true_case()) && !needs_cleaning(to_if_expr(expr).false_case())) { - return new_vars; + return side_effects; } // copy expression @@ -236,30 +235,32 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( } #endif - goto_programt tmp_true; - new_vars.add( - clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used)); + clean_expr_resultt tmp_true( + clean_expr(if_expr.true_case(), mode, result_is_used)); - goto_programt tmp_false; - new_vars.add( - clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used)); + clean_expr_resultt tmp_false( + clean_expr(if_expr.false_case(), mode, result_is_used)); if(result_is_used) { - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "if_expr", + side_effects.side_effects, + source_location, + mode); code_assignt assignment_true; assignment_true.lhs() = new_symbol.symbol_expr(); assignment_true.rhs() = if_expr.true_case(); assignment_true.add_source_location() = source_location; - convert(assignment_true, tmp_true, mode); + convert(assignment_true, tmp_true.side_effects, mode); code_assignt assignment_false; assignment_false.lhs() = new_symbol.symbol_expr(); assignment_false.rhs() = if_expr.false_case(); assignment_false.add_source_location() = source_location; - convert(assignment_false, tmp_false, mode); + convert(assignment_false, tmp_false.side_effects, mode); // overwrites expr expr = new_symbol.symbol_expr(); @@ -273,7 +274,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.true_case(), empty_typet())); - convert(code_expression, tmp_true, mode); + convert(code_expression, tmp_true.side_effects, mode); } if(if_expr.false_case().is_not_nil()) @@ -282,7 +283,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.false_case(), empty_typet())); - convert(code_expression, tmp_false, mode); + convert(code_expression, tmp_false.side_effects, mode); } expr = nil_exprt(); @@ -292,24 +293,26 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( generate_ifthenelse( if_expr.cond(), source_location, - tmp_true, + tmp_true.side_effects, if_expr.true_case().source_location(), - tmp_false, + tmp_false.side_effects, if_expr.false_case().source_location(), - dest, + side_effects.side_effects, mode); - destruct_locals(new_vars.minimal_scope, dest, ns); - new_vars.minimal_scope.clear(); + destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns); + destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns); + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); if(expr.is_not_nil()) - new_vars.minimal_scope.push_front(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); - return new_vars; + return side_effects; } else if(expr.id() == ID_comma) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result_is_used) { @@ -323,15 +326,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( if(last) { result.swap(*it); - new_vars.add(clean_expr(result, dest, mode, true)); + side_effects.add(clean_expr(result, mode, true)); } else { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // remember these for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } @@ -341,30 +344,30 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( { Forall_operands(it, expr) { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // remember as expression statement for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } expr = nil_exprt(); } - return new_vars; + return side_effects; } else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); // preserve 'result_is_used' - needs_destructiont new_vars = - clean_expr(typecast.op(), dest, mode, result_is_used); + clean_expr_resultt side_effects = + clean_expr(typecast.op(), mode, result_is_used); if(typecast.op().is_nil()) expr.make_nil(); - return new_vars; + return side_effects; } else if(expr.id() == ID_side_effect) { @@ -374,14 +377,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( if(statement == ID_gcc_conditional_expression) { // need to do separately - return remove_gcc_conditional_expression(expr, dest, mode); + return remove_gcc_conditional_expression(expr, mode); } else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' return remove_statement_expression( - to_side_effect_expr(expr), dest, mode, result_is_used); + to_side_effect_expr(expr), mode, result_is_used); } else if(statement == ID_assign) { @@ -397,16 +400,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( to_side_effect_expr(side_effect_assign.rhs()).get_statement() == ID_function_call) { - needs_destructiont new_vars = - clean_expr(side_effect_assign.lhs(), dest, mode); + clean_expr_resultt side_effects = + clean_expr(side_effect_assign.lhs(), mode); exprt lhs = side_effect_assign.lhs(); const bool must_use_rhs = assignment_lhs_needs_temporary(lhs); if(must_use_rhs) { - new_vars.add(remove_function_call( + side_effects.add(remove_function_call( to_side_effect_expr_function_call(side_effect_assign.rhs()), - dest, mode, true)); } @@ -417,14 +419,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( side_effect_assign.rhs(), new_lhs.type()); code_assignt assignment(std::move(new_lhs), new_rhs); assignment.add_source_location() = expr.source_location(); - convert_assign(assignment, dest, mode); + convert_assign(assignment, side_effects.side_effects, mode); if(result_is_used) expr = must_use_rhs ? new_rhs : lhs; else expr.make_nil(); - return new_vars; + return side_effects; } } } @@ -437,20 +439,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); - return clean_expr_address_of(addr.object(), dest, mode); + return clean_expr_address_of(addr.object(), mode); } - needs_destructiont new_vars; + clean_expr_resultt side_effects; // TODO: evaluation order Forall_operands(it, expr) - new_vars.add(clean_expr(*it, dest, mode)); + side_effects.add(clean_expr(*it, mode)); if(expr.id() == ID_side_effect) { - new_vars.add(remove_side_effect( - to_side_effect_expr(expr), dest, mode, result_is_used, false)); + side_effects.add(remove_side_effect( + to_side_effect_expr(expr), mode, result_is_used, false)); } else if(expr.id() == ID_compound_literal) { @@ -460,15 +462,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr( expr = to_unary_expr(expr).op(); } - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( - exprt &expr, - goto_programt &dest, - const irep_idt &mode) +goto_convertt::clean_expr_resultt +goto_convertt::clean_expr_address_of(exprt &expr, const irep_idt &mode) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; // The address of object constructors can be taken, // which is re-written into the address of a variable. @@ -477,8 +477,9 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); - new_vars.add(clean_expr(to_unary_expr(expr).op(), dest, mode)); - expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); + side_effects.add(clean_expr(to_unary_expr(expr).op(), mode)); + expr = make_compound_literal( + to_unary_expr(expr).op(), side_effects.side_effects, mode); } else if(expr.id() == ID_string_constant) { @@ -488,13 +489,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); - new_vars.add(clean_expr_address_of(index_expr.array(), dest, mode)); - new_vars.add(clean_expr(index_expr.index(), dest, mode)); + side_effects.add(clean_expr_address_of(index_expr.array(), mode)); + side_effects.add(clean_expr(index_expr.index(), mode)); } else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); - new_vars.add(clean_expr(deref_expr.pointer(), dest, mode)); + side_effects.add(clean_expr(deref_expr.pointer(), mode)); } else if(expr.id() == ID_comma) { @@ -512,44 +513,43 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of( result.swap(*it); else { - new_vars.add(clean_expr(*it, dest, mode, false)); + side_effects.add(clean_expr(*it, mode, false)); // get any side-effects if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } expr.swap(result); // do again - new_vars.add(clean_expr_address_of(expr, dest, mode)); + side_effects.add(clean_expr_address_of(expr, mode)); } else if(expr.id() == ID_side_effect) { - new_vars.add( - remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true)); + side_effects.add( + remove_side_effect(to_side_effect_expr(expr), mode, true, true)); } else Forall_operands(it, expr) - new_vars.add(clean_expr_address_of(*it, dest, mode)); + side_effects.add(clean_expr_address_of(*it, mode)); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont +goto_convertt::clean_expr_resultt goto_convertt::remove_gcc_conditional_expression( exprt &expr, - goto_programt &dest, const irep_idt &mode) { - needs_destructiont new_vars; + clean_expr_resultt side_effects; { auto &binary_expr = to_binary_expr(expr); // first remove side-effects from condition - new_vars = clean_expr(to_binary_expr(expr).op0(), dest, mode); + side_effects = clean_expr(to_binary_expr(expr).op0(), mode); // now we can copy op0 safely if_exprt if_expr( @@ -563,7 +563,7 @@ goto_convertt::remove_gcc_conditional_expression( } // there might still be junk in expr.op2() - new_vars.add(clean_expr(expr, dest, mode)); + side_effects.add(clean_expr(expr, mode)); - return new_vars; + return side_effects; } diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index ebe6286b6cd..d8b0db12aa8 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -761,7 +761,8 @@ void goto_convertt::convert_expression( else { // result _not_ used - needs_destructiont new_vars = clean_expr(expr, dest, mode, false); + clean_expr_resultt side_effects = clean_expr(expr, mode, false); + dest.destructive_append(side_effects.side_effects); // Any residual expression? // We keep it to add checks later. @@ -773,7 +774,7 @@ void goto_convertt::convert_expression( copy(tmp, OTHER, dest); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -809,7 +810,8 @@ void goto_convertt::convert_frontend_decl( const auto declaration_iterator = std::prev(dest.instructions.end()); auto initializer_location = initializer.find_source_location(); - needs_destructiont new_vars = clean_expr(initializer, dest, mode); + clean_expr_resultt side_effects = clean_expr(initializer, mode); + dest.destructive_append(side_effects.side_effects); if(initializer.is_not_nil()) { @@ -819,7 +821,7 @@ void goto_convertt::convert_frontend_decl( convert_assign(assign, dest, mode); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); return declaration_iterator; }(); @@ -860,7 +862,8 @@ void goto_convertt::convert_assign( { exprt lhs = code.lhs(), rhs = code.rhs(); - needs_destructiont new_vars = clean_expr(lhs, dest, mode); + clean_expr_resultt side_effects = clean_expr(lhs, mode); + dest.destructive_append(side_effects.side_effects); if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { @@ -872,7 +875,10 @@ void goto_convertt::convert_assign( rhs.find_source_location()); Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } do_function_call( lhs, @@ -886,7 +892,10 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } // TODO: This should be done in a separate pass do_cpp_new(lhs, to_side_effect_expr(rhs), dest); @@ -900,7 +909,8 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_gcc_conditional_expression)) { // handle above side effects - new_vars.add(clean_expr(rhs, dest, mode)); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -913,7 +923,10 @@ void goto_convertt::convert_assign( // preserve side effects that will be handled at later stages, // such as allocate, new operators of other languages, e.g. java, etc Forall_operands(it, rhs) - new_vars.add(clean_expr(*it, dest, mode)); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -924,7 +937,8 @@ void goto_convertt::convert_assign( else { // do everything else - new_vars.add(clean_expr(rhs, dest, mode)); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -933,7 +947,7 @@ void goto_convertt::convert_assign( copy(new_assign, ASSIGN, dest); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) @@ -945,7 +959,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) exprt tmp_op = code.op0(); - needs_destructiont new_vars = clean_expr(tmp_op, dest, ID_cpp); + clean_expr_resultt side_effects = clean_expr(tmp_op, ID_cpp); + dest.destructive_append(side_effects.side_effects); // we call the destructor, and then free const exprt &destructor = @@ -995,7 +1010,7 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) convert(delete_call, dest, ID_cpp); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_assert( @@ -1005,13 +1020,14 @@ void goto_convertt::convert_assert( { exprt cond = code.assertion(); - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); source_locationt annotated_location = code.source_location(); annotated_location.set("user-provided", true); dest.add(goto_programt::make_assertion(cond, annotated_location)); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_skip(const codet &code, goto_programt &dest) @@ -1027,11 +1043,12 @@ void goto_convertt::convert_assume( { exprt op = code.assumption(); - needs_destructiont new_vars = clean_expr(op, dest, mode); + clean_expr_resultt side_effects = clean_expr(op, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_assumption(op, code.source_location())); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_loop_contracts( @@ -1099,23 +1116,22 @@ void goto_convertt::convert_for( exprt cond = code.cond(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // save break/continue targets break_continue_targetst old_targets(targets); // do the u label - goto_programt::targett u = sideeffects.instructions.begin(); + goto_programt::targett u = side_effects.side_effects.instructions.begin(); // do the v label goto_programt tmp_v; goto_programt::targett v = tmp_v.add(goto_programt::instructiont()); - destruct_locals(new_vars.minimal_scope, tmp_v, ns); + destruct_locals(side_effects.temporaries, tmp_v, ns); // do the z and Z labels goto_programt tmp_z; - destruct_locals(new_vars.minimal_scope, tmp_z, ns); + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); goto_programt::targett Z = tmp_z.instructions.begin(); @@ -1131,15 +1147,16 @@ void goto_convertt::convert_for( { exprt tmp_B = code.iter(); - needs_destructiont new_vars_iter = clean_expr(tmp_B, tmp_x, mode, false); - destruct_locals(new_vars_iter.minimal_scope, tmp_x, ns); + clean_expr_resultt side_effects_iter = clean_expr(tmp_B, mode, false); + tmp_x.destructive_append(side_effects_iter.side_effects); + destruct_locals(side_effects_iter.temporaries, tmp_x, ns); if(tmp_x.instructions.empty()) tmp_x.add(goto_programt::make_skip(code.source_location())); } // optimize the v label - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) u = v; // set the targets @@ -1162,7 +1179,7 @@ void goto_convertt::convert_for( // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); dest.destructive_append(tmp_x); @@ -1244,8 +1261,7 @@ void goto_convertt::convert_dowhile( exprt cond = code.cond(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // do P while(c); //-------------------- @@ -1264,13 +1280,13 @@ void goto_convertt::convert_dowhile( goto_programt tmp_y; goto_programt::targett y = tmp_y.add(goto_programt::make_incomplete_goto( boolean_negate(cond), condition_location)); - destruct_locals(new_vars.minimal_scope, tmp_y, ns); + destruct_locals(side_effects.temporaries, tmp_y, ns); goto_programt::targett W = tmp_y.add( goto_programt::make_incomplete_goto(true_exprt{}, condition_location)); // do the z label and C labels goto_programt tmp_z; - destruct_locals(new_vars.minimal_scope, tmp_z, ns); + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); goto_programt::targett C = tmp_z.instructions.begin(); @@ -1280,10 +1296,10 @@ void goto_convertt::convert_dowhile( // do the x label goto_programt::targett x; - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) x = y; else - x = sideeffects.instructions.begin(); + x = side_effects.side_effects.instructions.begin(); // set the targets targets.set_break(z); @@ -1301,7 +1317,7 @@ void goto_convertt::convert_dowhile( convert_loop_contracts(code, y); dest.destructive_append(tmp_w); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_y); dest.destructive_append(tmp_z); @@ -1373,8 +1389,7 @@ void goto_convertt::convert_switch( // do the value we switch over exprt argument = code.value(); - goto_programt sideeffects; - needs_destructiont new_vars = clean_expr(argument, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(argument, mode); // Avoid potential performance penalties caused by evaluating the value // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't @@ -1386,17 +1401,16 @@ void goto_convertt::convert_switch( symbolt &new_symbol = new_tmp_symbol( argument.type(), "switch_value", - sideeffects, + side_effects.side_effects, code.source_location(), mode); code_assignt copy_value{ new_symbol.symbol_expr(), argument, code.source_location()}; - convert(copy_value, sideeffects, mode); + convert(copy_value, side_effects.side_effects, mode); argument = new_symbol.symbol_expr(); - new_vars.minimal_scope.push_front( - to_symbol_expr(argument).get_identifier()); + side_effects.add_temporary(to_symbol_expr(argument).get_identifier()); } // save break/default/cases targets @@ -1444,7 +1458,7 @@ void goto_convertt::convert_switch( source_location.set_case_number(std::to_string(case_number)); case_number++; - if(new_vars.minimal_scope.empty()) + if(side_effects.temporaries.empty()) { guard_expr.add_source_location() = source_location; @@ -1459,7 +1473,7 @@ void goto_convertt::convert_switch( goto_programt::targett try_next = tmp_cases.add(goto_programt::make_incomplete_goto( std::move(guard_expr), source_location)); - destruct_locals(new_vars.minimal_scope, tmp_cases, ns); + destruct_locals(side_effects.temporaries, tmp_cases, ns); tmp_cases.add(goto_programt::make_goto( case_pair.first, true_exprt{}, source_location)); goto_programt::targett next_case = @@ -1471,7 +1485,7 @@ void goto_convertt::convert_switch( tmp_cases.add(goto_programt::make_goto( targets.default_target, targets.default_target->source_location())); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_cases); dest.destructive_append(tmp); dest.destructive_append(tmp_z); @@ -1514,16 +1528,14 @@ void goto_convertt::convert_return( code.find_source_location()); code_frontend_returnt new_code(code); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(new_code.has_return_value()) { bool result_is_used = new_code.return_value().type().id() != ID_empty; - goto_programt sideeffects; - new_vars = - clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); - dest.destructive_append(sideeffects); + side_effects = clean_expr(new_code.return_value(), mode, result_is_used); + dest.destructive_append(side_effects.side_effects); // remove void-typed return value if(!result_is_used) @@ -1540,7 +1552,7 @@ void goto_convertt::convert_return( // Now add a 'set return value' instruction to set the return value. dest.add(goto_programt::make_set_return_value( new_code.return_value(), new_code.source_location())); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } else { @@ -1673,11 +1685,12 @@ void goto_convertt::convert_ifthenelse( } exprt tmp_guard = code.cond(); - needs_destructiont new_vars = clean_expr(tmp_guard, dest, mode); + clean_expr_resultt side_effects = clean_expr(tmp_guard, mode); + dest.destructive_append(side_effects.side_effects); // convert 'then'-branch goto_programt tmp_then; - destruct_locals(new_vars.minimal_scope, tmp_then, ns); + destruct_locals(side_effects.temporaries, tmp_then, ns); convert(code.then_case(), tmp_then, mode); source_locationt then_end_location = code.then_case().get_statement() == ID_block @@ -1685,7 +1698,7 @@ void goto_convertt::convert_ifthenelse( : code.then_case().source_location(); goto_programt tmp_else; - destruct_locals(new_vars.minimal_scope, tmp_else, ns); + destruct_locals(side_effects.temporaries, tmp_else, ns); source_locationt else_end_location; if(has_else) @@ -1938,13 +1951,14 @@ void goto_convertt::generate_conditional_branch( { // simple branch exprt cond = guard; - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_goto(target_true, cond, source_location)); goto_programt tmp_destruct; - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_true, tmp_destruct); - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -2014,17 +2028,18 @@ void goto_convertt::generate_conditional_branch( } exprt cond = guard; - needs_destructiont new_vars = clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); // true branch dest.add(goto_programt::make_goto(target_true, cond, source_location)); goto_programt tmp_destruct; - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_true, tmp_destruct); // false branch dest.add(goto_programt::make_goto(target_false, source_location)); - destruct_locals(new_vars.minimal_scope, tmp_destruct, ns); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); dest.insert_before_swap(target_false, tmp_destruct); } diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 750eb2a07ac..600938751f3 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -56,19 +56,29 @@ class goto_convertt : public messaget std::string tmp_symbol_prefix; lifetimet lifetime = lifetimet::STATIC_GLOBAL; - struct needs_destructiont + struct clean_expr_resultt { - std::list minimal_scope; - - needs_destructiont() = default; - - explicit needs_destructiont(irep_idt id) : minimal_scope({id}) + /// Identifiers of temporaries introduced while cleaning an expression. The + /// caller needs to add destructors for these (via `destruct_locals`) on all + /// control-flow paths as soon as the temporaries are no longer needed. + std::list temporaries; + /// Statements implementing side effects of the expression that was subject + /// to cleaning. The caller needs to merge (typically via + /// `destructive_append`) these statements into the destination GOTO + /// program. + goto_programt side_effects; + + clean_expr_resultt() = default; + + void add(clean_expr_resultt &&other) { + temporaries.splice(temporaries.begin(), other.temporaries); + side_effects.destructive_append(other.side_effects); } - void add(needs_destructiont &&other) + void add_temporary(const irep_idt &id) { - minimal_scope.splice(minimal_scope.begin(), other.minimal_scope); + temporaries.push_front(id); } }; @@ -97,14 +107,11 @@ class goto_convertt : public messaget // into the program logic // - [[nodiscard]] needs_destructiont clean_expr( - exprt &expr, - goto_programt &dest, - const irep_idt &mode, - bool result_is_used = true); + [[nodiscard]] clean_expr_resultt + clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used = true); - [[nodiscard]] needs_destructiont - clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt + clean_expr_address_of(exprt &expr, const irep_idt &mode); static bool needs_cleaning(const exprt &expr); @@ -125,58 +132,46 @@ class goto_convertt : public messaget void rewrite_boolean(exprt &dest); - [[nodiscard]] needs_destructiont remove_side_effect( + [[nodiscard]] clean_expr_resultt remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken); - [[nodiscard]] needs_destructiont remove_assignment( + [[nodiscard]] clean_expr_resultt remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_pre( + [[nodiscard]] clean_expr_resultt remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_post( + [[nodiscard]] clean_expr_resultt remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_function_call( + [[nodiscard]] clean_expr_resultt remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_cpp_new( + [[nodiscard]] clean_expr_resultt + remove_cpp_new(side_effect_exprt &expr, bool result_is_used); + [[nodiscard]] clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_malloc( side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used); - void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); - [[nodiscard]] needs_destructiont remove_malloc( - side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont - remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); - [[nodiscard]] needs_destructiont remove_statement_expression( + [[nodiscard]] clean_expr_resultt + remove_temporary_object(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - [[nodiscard]] needs_destructiont remove_gcc_conditional_expression( - exprt &expr, - goto_programt &dest, - const irep_idt &mode); - [[nodiscard]] needs_destructiont remove_overflow( + [[nodiscard]] clean_expr_resultt + remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode); diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp index badf8384a26..2fdc5c3e616 100644 --- a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp @@ -43,15 +43,17 @@ void goto_convertt::do_function_call( exprt::operandst new_arguments = arguments; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(!new_lhs.is_nil()) - new_vars.add(clean_expr(new_lhs, dest, mode)); + side_effects.add(clean_expr(new_lhs, mode)); - new_vars.add(clean_expr(new_function, dest, mode)); + side_effects.add(clean_expr(new_function, mode)); for(auto &new_argument : new_arguments) - new_vars.add(clean_expr(new_argument, dest, mode)); + side_effects.add(clean_expr(new_argument, mode)); + + dest.destructive_append(side_effects.side_effects); // split on the function @@ -83,7 +85,7 @@ void goto_convertt::do_function_call( function.find_source_location()); } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::do_function_call_if( diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index 61a8587fe0a..28943332d12 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -24,9 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" -goto_convertt::needs_destructiont goto_convertt::remove_assignment( +goto_convertt::clean_expr_resultt goto_convertt::remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -35,7 +34,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( std::optional replacement_expr_opt; - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(statement == ID_assign) { @@ -48,8 +47,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( { if(!old_assignment.rhs().is_constant()) { - new_vars.minimal_scope.push_front( - make_temp_symbol(old_assignment.rhs(), "assign", dest, mode)); + side_effects.add_temporary(make_temp_symbol( + old_assignment.rhs(), "assign", side_effects.side_effects, mode)); } replacement_expr_opt = @@ -61,7 +60,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs)); new_assignment.add_source_location() = expr.source_location(); - convert_assign(new_assignment, dest, mode); + convert_assign(new_assignment, side_effects.side_effects, mode); } else if( statement == ID_assign_plus || statement == ID_assign_minus || @@ -120,8 +119,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( result_is_used && !address_taken && assignment_lhs_needs_temporary(binary_expr.op0())) { - new_vars.minimal_scope.push_front( - make_temp_symbol(rhs, "assign", dest, mode)); + side_effects.add_temporary( + make_temp_symbol(rhs, "assign", side_effects.side_effects, mode)); replacement_expr_opt = typecast_exprt::conditional_cast(rhs, new_lhs.type()); } @@ -131,7 +130,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( code_assignt assignment(new_lhs, rhs); assignment.add_source_location() = expr.source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } else UNREACHABLE; @@ -143,10 +142,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type()); expr.swap(new_lhs); - return new_vars; + return side_effects; } - destruct_locals(new_vars.minimal_scope, dest, ns); + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); if(result_is_used) { @@ -173,12 +173,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment( else expr.make_nil(); - return {}; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_pre( +goto_convertt::clean_expr_resultt goto_convertt::remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -242,14 +241,15 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre( const bool cannot_use_lhs = result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(cannot_use_lhs) - new_vars.minimal_scope.push_front(make_temp_symbol(rhs, "pre", dest, mode)); + side_effects.add_temporary( + make_temp_symbol(rhs, "pre", side_effects.side_effects, mode)); code_assignt assignment(lhs, rhs); assignment.add_source_location() = expr.find_source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -268,12 +268,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre( else expr.make_nil(); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_post( +goto_convertt::clean_expr_resultt goto_convertt::remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -334,7 +333,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_post( // fix up the expression, if needed - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result_is_used) { @@ -346,32 +345,33 @@ goto_convertt::needs_destructiont goto_convertt::remove_post( suffix += "_" + id2string(base_name); } - new_vars.minimal_scope.push_front( - make_temp_symbol(tmp, suffix, dest, mode)); + side_effects.add_temporary( + make_temp_symbol(tmp, suffix, side_effects.side_effects, mode)); expr.swap(tmp); } else expr.make_nil(); - dest.destructive_append(tmp1); - dest.destructive_append(tmp2); + side_effects.side_effects.destructive_append(tmp1); + side_effects.side_effects.destructive_append(tmp2); - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_function_call( +goto_convertt::clean_expr_resultt goto_convertt::remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(!result_is_used) { code_function_callt call(expr.function(), expr.arguments()); call.add_source_location() = expr.source_location(); - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); expr.make_nil(); - return {}; + return side_effects; } // get name of function, if available @@ -398,7 +398,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call( symbol_table); PRECONDITION(expr.type().id() != ID_code); - dest.add( + side_effects.side_effects.add( goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); { @@ -406,12 +406,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call( code_function_callt call( new_symbol.symbol_expr(), expr.function(), expr.arguments()); call.add_source_location() = new_symbol.location; - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } void goto_convertt::replace_new_object(const exprt &object, exprt &dest) @@ -423,10 +425,8 @@ void goto_convertt::replace_new_object(const exprt &object, exprt &dest) replace_new_object(object, *it); } -goto_convertt::needs_destructiont goto_convertt::remove_cpp_new( - side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_new(side_effect_exprt &expr, bool result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), @@ -436,29 +436,29 @@ goto_convertt::needs_destructiont goto_convertt::remove_cpp_new( ID_cpp, symbol_table); + clean_expr_resultt side_effects; + PRECONDITION(expr.type().id() != ID_code); - dest.add( + side_effects.side_effects.add( goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); const code_assignt call(new_symbol.symbol_expr(), expr); - convert(call, dest, ID_cpp); + convert(call, side_effects.side_effects, ID_cpp); if(result_is_used) { static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); } else - { expr.make_nil(); - return {}; - } + + return side_effects; } -void goto_convertt::remove_cpp_delete( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_delete(side_effect_exprt &expr) { DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand"); @@ -467,17 +467,21 @@ void goto_convertt::remove_cpp_delete( tmp.copy_to_operands(to_unary_expr(expr).op()); tmp.set(ID_destructor, expr.find(ID_destructor)); - convert_cpp_delete(tmp, dest); + clean_expr_resultt side_effects; + convert_cpp_delete(tmp, side_effects.side_effects); expr.make_nil(); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_malloc( +goto_convertt::clean_expr_resultt goto_convertt::remove_malloc( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( @@ -490,44 +494,47 @@ goto_convertt::needs_destructiont goto_convertt::remove_malloc( code_frontend_declt decl(new_symbol.symbol_expr()); decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, mode); + convert_frontend_decl(decl, side_effects.side_effects, mode); code_assignt call(new_symbol.symbol_expr(), expr); call.add_source_location() = expr.source_location(); static_cast(expr) = new_symbol.symbol_expr(); - convert(call, dest, mode); + convert(call, side_effects.side_effects, mode); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); } else - { - convert(code_expressiont(std::move(expr)), dest, mode); + convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode); - return {}; - } + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_temporary_object( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_temporary_object(side_effect_exprt &expr) { + clean_expr_resultt side_effects; + const irep_idt &mode = expr.get(ID_mode); INVARIANT_WITH_DIAGNOSTICS( expr.operands().size() <= 1, "temporary_object takes zero or one operands", expr.find_source_location()); - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "obj", + side_effects.side_effects, + expr.find_source_location(), + mode); if(expr.operands().size() == 1) { const code_assignt assignment( new_symbol.symbol_expr(), to_unary_expr(expr).op()); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } if(expr.find(ID_initializer).is_not_nil()) @@ -539,20 +546,23 @@ goto_convertt::needs_destructiont goto_convertt::remove_temporary_object( exprt initializer = static_cast(expr.find(ID_initializer)); replace_new_object(new_symbol.symbol_expr(), initializer); - convert(to_code(initializer), dest, mode); + convert(to_code(initializer), side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( +goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + // This is a gcc extension of the form ({ ....; expr; }) // The value is that of the final expression. // The expression is copied into a temporary before the @@ -562,9 +572,9 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( if(!result_is_used) { - convert(code, dest, mode); + convert(code, side_effects.side_effects, mode); expr.make_nil(); - return {}; + return side_effects; } INVARIANT_WITH_DIAGNOSTICS( @@ -583,7 +593,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( source_locationt source_location = last.find_source_location(); symbolt &new_symbol = new_tmp_symbol( - expr.type(), "statement_expression", dest, source_location, mode); + expr.type(), + "statement_expression", + side_effects.side_effects, + source_location, + mode); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); tmp_symbol_expr.add_source_location() = source_location; @@ -607,20 +621,17 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression( UNREACHABLE; } - { - goto_programt tmp; - convert(code, tmp, mode); - dest.destructive_append(tmp); - } + convert(code, side_effects.side_effects, mode); static_cast(expr) = tmp_symbol_expr; - return needs_destructiont{to_symbol_expr(expr).get_identifier()}; + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_overflow( +goto_convertt::clean_expr_resultt goto_convertt::remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode) { @@ -629,14 +640,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( const exprt &rhs = expr.rhs(); const exprt &result = expr.result(); - needs_destructiont new_vars; + clean_expr_resultt side_effects; if(result.type().id() != ID_pointer) { // result of the arithmetic operation is _not_ used, just evaluate side // effects exprt tmp = result; - new_vars.add(clean_expr(tmp, dest, mode, false)); + side_effects.add(clean_expr(tmp, mode, false)); // the is-there-an-overflow result may be used if(result_is_used) @@ -667,8 +678,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( if(result_is_used) { - new_vars.minimal_scope.push_front( - make_temp_symbol(overflow_with_result, "overflow_result", dest, mode)); + side_effects.add_temporary(make_temp_symbol( + overflow_with_result, + "overflow_result", + side_effects.side_effects, + mode)); } const struct_typet::componentst &result_comps = @@ -679,7 +693,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( typecast_exprt::conditional_cast( member_exprt{overflow_with_result, result_comps[0]}, arith_type), expr.source_location()}; - convert_assign(result_assignment, dest, mode); + convert_assign(result_assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -692,12 +706,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow( expr.make_nil(); } - return new_vars; + return side_effects; } -goto_convertt::needs_destructiont goto_convertt::remove_side_effect( +goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken) @@ -707,7 +720,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( if(statement == ID_function_call) { return remove_function_call( - to_side_effect_expr_function_call(expr), dest, mode, result_is_used); + to_side_effect_expr_function_call(expr), mode, result_is_used); } else if( statement == ID_assign || statement == ID_assign_plus || @@ -717,36 +730,35 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( statement == ID_assign_lshr || statement == ID_assign_ashr || statement == ID_assign_shl || statement == ID_assign_mod) { - return remove_assignment(expr, dest, result_is_used, address_taken, mode); + return remove_assignment(expr, result_is_used, address_taken, mode); } else if(statement == ID_postincrement || statement == ID_postdecrement) { - return remove_post(expr, dest, mode, result_is_used); + return remove_post(expr, mode, result_is_used); } else if(statement == ID_preincrement || statement == ID_predecrement) { - return remove_pre(expr, dest, result_is_used, address_taken, mode); + return remove_pre(expr, result_is_used, address_taken, mode); } else if(statement == ID_cpp_new || statement == ID_cpp_new_array) { - return remove_cpp_new(expr, dest, result_is_used); + return remove_cpp_new(expr, result_is_used); } else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) { - remove_cpp_delete(expr, dest); - return {}; + return remove_cpp_delete(expr); } else if(statement == ID_allocate) { - return remove_malloc(expr, dest, mode, result_is_used); + return remove_malloc(expr, mode, result_is_used); } else if(statement == ID_temporary_object) { - return remove_temporary_object(expr, dest); + return remove_temporary_object(expr); } else if(statement == ID_statement_expression) { - return remove_statement_expression(expr, dest, mode, result_is_used); + return remove_statement_expression(expr, mode, result_is_used); } else if(statement == ID_nondet) { @@ -760,23 +772,25 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect( } else if(statement == ID_throw) { + clean_expr_resultt side_effects; + codet code = code_expressiont(side_effect_expr_throwt( expr.find(ID_exception_list), expr.type(), expr.source_location())); code.op0().operands().swap(expr.operands()); code.add_source_location() = expr.source_location(); - dest.add(goto_programt::instructiont( + side_effects.side_effects.add(goto_programt::instructiont( std::move(code), expr.source_location(), THROW, nil_exprt(), {})); // the result can't be used, these are void expr.make_nil(); - return {}; + return side_effects; } else if( statement == ID_overflow_plus || statement == ID_overflow_minus || statement == ID_overflow_mult) { return remove_overflow( - to_side_effect_expr_overflow(expr), dest, result_is_used, mode); + to_side_effect_expr_overflow(expr), result_is_used, mode); } else { diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index b25f43467d8..b6e859c1fdc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -46,7 +46,9 @@ class cleanert : public goto_convertt [[nodiscard]] std::list clean(exprt &guard, goto_programt &dest, const irep_idt &mode) { - return goto_convertt::clean_expr(guard, dest, mode, true).minimal_scope; + auto clean_result = goto_convertt::clean_expr(guard, mode, true); + dest.destructive_append(clean_result.side_effects); + return clean_result.temporaries; } void do_havoc_slice(