Skip to content

Commit 05f5627

Browse files
committed
fixup! Assignment side effects may require additional temporaries
The fixes in diffblue#5858 addressed the problem of assignments having side effects, but did not consider function calls or pre-increment/decrement, which eventually also yield assignments, and thus may have similar side effects.
1 parent a4c81ef commit 05f5627

File tree

4 files changed

+44
-5
lines changed

4 files changed

+44
-5
lines changed

regression/cbmc/Sideeffects8/main.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,30 @@ struct A
66
struct A *p;
77
};
88

9+
struct A *return_null()
10+
{
11+
return NULL;
12+
}
13+
914
int main(void)
1015
{
1116
struct A x = {&x};
1217
struct A *r = x.p->p = NULL;
1318
assert(r == NULL);
1419

20+
struct A x2 = {&x2};
21+
r = x2.p->p = return_null();
22+
assert(r == NULL);
23+
1524
struct A arr[2] = {arr, 0};
1625
r = arr[0].p->p += 1;
1726
assert(r == &arr[1]);
27+
28+
struct A arr2[2] = {arr2, 0};
29+
r = ++(arr2[0].p->p);
30+
assert(r == &arr2[1]);
31+
32+
struct A arr3[2] = {arr3, 0};
33+
r = (arr3[0].p->p)++;
34+
assert(r == &arr3[0]);
1835
}

src/goto-programs/goto_clean_expr.cpp

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -374,6 +374,16 @@ void goto_convertt::clean_expr(
374374
clean_expr(side_effect_assign.lhs(), dest, mode);
375375
exprt lhs = side_effect_assign.lhs();
376376

377+
const bool must_use_rhs = needs_cleaning(lhs);
378+
if(must_use_rhs)
379+
{
380+
remove_function_call(
381+
to_side_effect_expr_function_call(side_effect_assign.rhs()),
382+
dest,
383+
mode,
384+
true);
385+
}
386+
377387
// turn into code
378388
code_assignt assignment;
379389
assignment.lhs()=lhs;
@@ -382,7 +392,7 @@ void goto_convertt::clean_expr(
382392
convert_assign(assignment, dest, mode);
383393

384394
if(result_is_used)
385-
expr.swap(lhs);
395+
expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
386396
else
387397
expr.make_nil();
388398
return;

src/goto-programs/goto_convert_class.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,7 @@ class goto_convertt:public messaget
114114
side_effect_exprt &expr,
115115
goto_programt &dest,
116116
bool result_is_used,
117+
bool address_taken,
117118
const irep_idt &mode);
118119
void remove_post(
119120
side_effect_exprt &expr,

src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,7 @@ void goto_convertt::remove_pre(
181181
side_effect_exprt &expr,
182182
goto_programt &dest,
183183
bool result_is_used,
184+
bool address_taken,
184185
const irep_idt &mode)
185186
{
186187
INVARIANT_WITH_DIAGNOSTICS(
@@ -234,16 +235,26 @@ void goto_convertt::remove_pre(
234235
rhs.add_to_operands(op, std::move(constant));
235236
rhs.type() = op.type();
236237

238+
const bool cannot_use_lhs =
239+
result_is_used && !address_taken && needs_cleaning(op);
240+
if(cannot_use_lhs)
241+
make_temp_symbol(rhs, "pre", dest, mode);
242+
237243
code_assignt assignment(op, rhs);
238244
assignment.add_source_location()=expr.find_source_location();
239245

240246
convert(assignment, dest, mode);
241247

242248
if(result_is_used)
243249
{
244-
// revert to argument of pre-inc/pre-dec
245-
exprt tmp = op;
246-
expr.swap(tmp);
250+
if(cannot_use_lhs)
251+
expr.swap(rhs);
252+
else
253+
{
254+
// revert to argument of pre-inc/pre-dec
255+
exprt tmp = op;
256+
expr.swap(tmp);
257+
}
247258
}
248259
else
249260
expr.make_nil();
@@ -607,7 +618,7 @@ void goto_convertt::remove_side_effect(
607618
remove_post(expr, dest, mode, result_is_used);
608619
else if(statement==ID_preincrement ||
609620
statement==ID_predecrement)
610-
remove_pre(expr, dest, result_is_used, mode);
621+
remove_pre(expr, dest, result_is_used, address_taken, mode);
611622
else if(statement==ID_cpp_new ||
612623
statement==ID_cpp_new_array)
613624
remove_cpp_new(expr, dest, result_is_used);

0 commit comments

Comments
 (0)