Skip to content

Commit e70816e

Browse files
author
Daniel Kroening
committed
introduce instructiont::set_X
This avoids accidental disruption of sharing.
1 parent 2168964 commit e70816e

10 files changed

+128
-75
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 28 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -761,37 +761,50 @@ void constant_propagator_ait::replace(
761761
{
762762
exprt c = it->get_condition();
763763
replace_types_rec(d.values.replace_const, c);
764-
constant_propagator_domaint::partial_evaluate(d.values, c, ns);
765-
it->set_condition(c);
764+
if(!constant_propagator_domaint::partial_evaluate(d.values, c, ns))
765+
it->set_condition(c);
766766
}
767767
else if(it->is_assign())
768768
{
769-
exprt &rhs=to_code_assign(it->code).rhs();
770-
constant_propagator_domaint::partial_evaluate(d.values, rhs, ns);
769+
auto assign = it->get_assign();
770+
exprt &rhs = assign.rhs();
771771

772-
if(rhs.id()==ID_constant)
773-
rhs.add_source_location() =
774-
to_code_assign(it->code).lhs().source_location();
772+
if(!constant_propagator_domaint::partial_evaluate(d.values, rhs, ns))
773+
{
774+
if(rhs.id() == ID_constant)
775+
rhs.add_source_location() = assign.lhs().source_location();
776+
it->set_assign(assign);
777+
}
775778
}
776779
else if(it->is_function_call())
777780
{
778-
exprt &function = to_code_function_call(it->code).function();
779-
constant_propagator_domaint::partial_evaluate(d.values, function, ns);
781+
auto call = it->get_function_call();
780782

781-
exprt::operandst &args=
782-
to_code_function_call(it->code).arguments();
783+
bool call_changed = false;
783784

784-
for(auto &arg : args)
785+
if(!constant_propagator_domaint::partial_evaluate(
786+
d.values, call.function(), ns))
785787
{
786-
constant_propagator_domaint::partial_evaluate(d.values, arg, ns);
788+
call_changed = true;
787789
}
790+
791+
for(auto &arg : call.arguments())
792+
if(!constant_propagator_domaint::partial_evaluate(d.values, arg, ns))
793+
call_changed = true;
794+
795+
if(call_changed)
796+
it->set_function_call(call);
788797
}
789798
else if(it->is_other())
790799
{
791800
if(it->get_other().get_statement() == ID_expression)
792801
{
793-
constant_propagator_domaint::partial_evaluate(
794-
d.values, it->get_other(), ns);
802+
auto c = to_code_expression(it->get_other());
803+
if(!constant_propagator_domaint::partial_evaluate(
804+
d.values, c.expression(), ns))
805+
{
806+
it->set_other(c);
807+
}
795808
}
796809
}
797810
}

src/goto-analyzer/static_simplifier.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ bool static_simplifier(
9595
}
9696
else if(i_it->is_assign())
9797
{
98-
code_assignt &assign = i_it->get_assign();
98+
auto assign = i_it->get_assign();
9999

100100
// Simplification needs to be aware of which side of the
101101
// expression it is handling as:
@@ -111,11 +111,14 @@ bool static_simplifier(
111111
if(unchanged_lhs && unchanged_rhs)
112112
unmodified.assigns++;
113113
else
114+
{
114115
simplified.assigns++;
116+
i_it->set_assign(assign);
117+
}
115118
}
116119
else if(i_it->is_function_call())
117120
{
118-
code_function_callt &fcall = i_it->get_function_call();
121+
auto fcall = i_it->get_function_call();
119122

120123
bool unchanged =
121124
ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
@@ -128,7 +131,10 @@ bool static_simplifier(
128131
if(unchanged)
129132
unmodified.function_calls++;
130133
else
134+
{
131135
simplified.function_calls++;
136+
i_it->set_function_call(fcall);
137+
}
132138
}
133139
}
134140
}

src/goto-programs/goto_program.h

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -188,11 +188,11 @@ class goto_programt
188188
return to_code_assign(code);
189189
}
190190

191-
/// Get the assignment for ASSIGN
192-
code_assignt &get_assign()
191+
/// Set the assignment for ASSIGN
192+
void set_assign(code_assignt c)
193193
{
194194
PRECONDITION(is_assign());
195-
return to_code_assign(code);
195+
code = std::move(c);
196196
}
197197

198198
/// Get the declaration for DECL
@@ -202,11 +202,11 @@ class goto_programt
202202
return to_code_decl(code);
203203
}
204204

205-
/// Get the declaration for DECL
206-
code_declt &get_decl()
205+
/// Set the declaration for DECL
206+
void set_decl(code_declt c)
207207
{
208208
PRECONDITION(is_decl());
209-
return to_code_decl(code);
209+
code = std::move(c);
210210
}
211211

212212
/// Get the dead statement for DEAD
@@ -216,11 +216,11 @@ class goto_programt
216216
return to_code_dead(code);
217217
}
218218

219-
/// Get the dead statement for DEAD
220-
code_deadt &get_dead()
219+
/// Set the dead statement for DEAD
220+
void set_dead(code_deadt c)
221221
{
222222
PRECONDITION(is_dead());
223-
return to_code_dead(code);
223+
code = std::move(c);
224224
}
225225

226226
/// Get the return statement for READ
@@ -230,11 +230,11 @@ class goto_programt
230230
return to_code_return(code);
231231
}
232232

233-
/// Get the return statement for READ
234-
code_returnt &get_return()
233+
/// Set the return statement for READ
234+
void set_return(code_returnt c)
235235
{
236236
PRECONDITION(is_return());
237-
return to_code_return(code);
237+
code = std::move(c);
238238
}
239239

240240
/// Get the function call for FUNCTION_CALL
@@ -244,11 +244,11 @@ class goto_programt
244244
return to_code_function_call(code);
245245
}
246246

247-
/// Get the function call for FUNCTION_CALL
248-
code_function_callt &get_function_call()
247+
/// Set the function call for FUNCTION_CALL
248+
void set_function_call(code_function_callt c)
249249
{
250250
PRECONDITION(is_function_call());
251-
return to_code_function_call(code);
251+
code = std::move(c);
252252
}
253253

254254
/// Get the statement for OTHER
@@ -258,11 +258,11 @@ class goto_programt
258258
return code;
259259
}
260260

261-
/// Get the statement for OTHER
262-
codet &get_other()
261+
/// Set the statement for OTHER
262+
void set_other(codet &c)
263263
{
264264
PRECONDITION(is_other());
265-
return code;
265+
code = std::move(c);
266266
}
267267

268268
/// The location of the instruction in the source file

src/goto-programs/mm_io.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ void mm_io(
4545

4646
if(it->is_assign())
4747
{
48-
auto &a = it->get_assign();
48+
auto a = it->get_assign();
4949
collect_deref_expr(a.rhs(), deref_expr_r);
5050

5151
if(mm_io_r.is_not_nil())
@@ -60,7 +60,8 @@ void mm_io(
6060
irep_idt r_identifier=id2string(identifier)+RETURN_VALUE_SUFFIX;
6161
symbol_exprt return_value(r_identifier, ct.return_type());
6262
if_exprt if_expr(integer_address(d.pointer()), return_value, d);
63-
replace_expr(d, if_expr, a.rhs());
63+
if(!replace_expr(d, if_expr, a.rhs()))
64+
it->set_assign(a);
6465

6566
const typet &pt=ct.parameters()[0].type();
6667
const typet &st=ct.parameters()[1].type();

src/goto-programs/remove_function_pointers.cpp

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,9 @@ void remove_function_pointerst::remove_function_pointer(
319319

320320
if(functions.size()==1)
321321
{
322-
target->get_function_call().function() = *functions.cbegin();
322+
auto call = target->get_function_call();
323+
call.function() = *functions.cbegin();
324+
target->set_function_call(call);
323325
return;
324326
}
325327
}
@@ -386,14 +388,18 @@ void remove_function_pointerst::remove_function_pointer(
386388
for(const auto &fun : functions)
387389
{
388390
// call function
389-
goto_programt::targett t1 =
390-
new_code_calls.add(goto_programt::make_function_call(code));
391-
t1->get_function_call().function() = fun;
391+
auto new_call = code;
392+
new_call.function() = fun;
392393

393394
// the signature of the function might not match precisely
394-
fix_argument_types(t1->get_function_call());
395+
fix_argument_types(new_call);
396+
397+
goto_programt tmp;
398+
fix_return_type(function_id, new_call, tmp);
399+
400+
auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
401+
new_code_calls.destructive_append(tmp);
395402

396-
fix_return_type(function_id, t1->get_function_call(), new_code_calls);
397403
// goto final
398404
new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
399405

@@ -404,7 +410,7 @@ void remove_function_pointerst::remove_function_pointer(
404410
typecast_exprt::conditional_cast(address_of, pointer.type());
405411

406412
new_code_gotos.add(
407-
goto_programt::make_goto(t1, equal_exprt(pointer, casted_address)));
413+
goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
408414
}
409415

410416
// fall-through

src/goto-programs/remove_returns.cpp

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ void remove_returnst::do_function_calls(
150150
{
151151
if(i_it->is_function_call())
152152
{
153-
code_function_callt &function_call = i_it->get_function_call();
153+
code_function_callt function_call = i_it->get_function_call();
154154

155155
INVARIANT(
156156
function_call.function().id() == ID_symbol,
@@ -222,6 +222,9 @@ void remove_returnst::do_function_calls(
222222
goto_programt::make_dead(*return_value, i_it->source_location));
223223
}
224224
}
225+
226+
// update the call
227+
i_it->set_function_call(function_call);
225228
}
226229
}
227230
}
@@ -355,7 +358,8 @@ bool remove_returnst::restore_returns(
355358
{
356359
if(i_it->is_assign())
357360
{
358-
code_assignt &assign = i_it->get_assign();
361+
const auto &assign = i_it->get_assign();
362+
359363
if(assign.lhs().id()!=ID_symbol ||
360364
to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
361365
continue;
@@ -384,7 +388,7 @@ void remove_returnst::undo_function_calls(
384388
{
385389
if(i_it->is_function_call())
386390
{
387-
code_function_callt &function_call = i_it->get_function_call();
391+
code_function_callt function_call = i_it->get_function_call();
388392

389393
// ignore function pointers
390394
if(function_call.function().id()!=ID_symbol)
@@ -401,8 +405,8 @@ void remove_returnst::undo_function_calls(
401405

402406
// find "f(...); lhs=f#return_value; DEAD f#return_value;"
403407
// and revert to "lhs=f(...);"
404-
goto_programt::instructionst::iterator next=i_it;
405-
++next;
408+
goto_programt::instructionst::iterator next = std::next(i_it);
409+
406410
INVARIANT(
407411
next!=goto_program.instructions.end(),
408412
"non-void function call must be followed by #return_value read");
@@ -423,6 +427,8 @@ void remove_returnst::undo_function_calls(
423427
// restore the previous assignment
424428
function_call.lhs()=assign.lhs();
425429

430+
i_it->set_function_call(function_call);
431+
426432
// remove the assignment and subsequent dead
427433
// i_it remains valid
428434
next=goto_program.instructions.erase(next);

src/goto-programs/remove_virtual_functions.cpp

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -190,8 +190,9 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
190190
}
191191
else
192192
{
193-
create_static_function_call(
194-
target->get_function_call(), *functions.front().symbol_expr, ns);
193+
auto c = target->get_function_call();
194+
create_static_function_call(c, *functions.front().symbol_expr, ns);
195+
target->set_function_call(c);
195196
}
196197
return next_target;
197198
}
@@ -250,11 +251,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
250251
if(fun.symbol_expr.has_value())
251252
{
252253
// call function
253-
goto_programt::targett t1 = new_code_calls.add(
254-
goto_programt::make_function_call(code, vcall_source_loc));
254+
auto new_call = code;
255+
256+
create_static_function_call(new_call, *fun.symbol_expr, ns);
255257

256-
create_static_function_call(
257-
t1->get_function_call(), *fun.symbol_expr, ns);
258+
goto_programt::targett t1 = new_code_calls.add(
259+
goto_programt::make_function_call(new_call, vcall_source_loc));
258260

259261
insertit.first->second = t1;
260262
}

src/goto-programs/replace_calls.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ void replace_callst::operator()(
7070
if(!ins.is_function_call())
7171
continue;
7272

73-
code_function_callt &cfc = ins.get_function_call();
73+
auto cfc = ins.get_function_call();
7474
exprt &function = cfc.function();
7575

7676
PRECONDITION(function.id() == ID_symbol);
@@ -114,6 +114,8 @@ void replace_callst::operator()(
114114
// Finally modify the call
115115
function.type() = f_it2->second.type;
116116
se.set_identifier(new_id);
117+
118+
ins.set_function_call(cfc);
117119
}
118120
}
119121

0 commit comments

Comments
 (0)