Skip to content

Commit afde693

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

10 files changed

+98
-60
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -790,8 +790,10 @@ void constant_propagator_ait::replace(
790790
{
791791
if(it->get_other().get_statement() == ID_expression)
792792
{
793+
auto c = to_code_expression(it->get_other());
793794
constant_propagator_domaint::partial_evaluate(
794-
d.values, it->get_other(), ns);
795+
d.values, c.expression(), ns);
796+
it->set_other(c);
795797
}
796798
}
797799
}

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: 2 additions & 1 deletion
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())
@@ -61,6 +61,7 @@ void mm_io(
6161
symbol_exprt return_value(r_identifier, ct.return_type());
6262
if_exprt if_expr(integer_address(d.pointer()), return_value, d);
6363
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: 10 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,15 @@ 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+
fix_return_type(function_id, new_call, new_code_calls);
397+
398+
auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
395399

396-
fix_return_type(function_id, t1->get_function_call(), new_code_calls);
397400
// goto final
398401
new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
399402

@@ -404,7 +407,7 @@ void remove_function_pointerst::remove_function_pointer(
404407
typecast_exprt::conditional_cast(address_of, pointer.type());
405408

406409
new_code_gotos.add(
407-
goto_programt::make_goto(t1, equal_exprt(pointer, casted_address)));
410+
goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
408411
}
409412

410413
// fall-through

src/goto-programs/remove_returns.cpp

Lines changed: 10 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,
@@ -191,6 +191,8 @@ void remove_returnst::do_function_calls(
191191
to_code_type(function_call.function().type()).return_type()=
192192
empty_typet();
193193

194+
i_it->set_function_call(function_call);
195+
194196
if(function_call.lhs().is_not_nil())
195197
{
196198
exprt rhs;
@@ -355,7 +357,8 @@ bool remove_returnst::restore_returns(
355357
{
356358
if(i_it->is_assign())
357359
{
358-
code_assignt &assign = i_it->get_assign();
360+
const auto &assign = i_it->get_assign();
361+
359362
if(assign.lhs().id()!=ID_symbol ||
360363
to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
361364
continue;
@@ -384,7 +387,7 @@ void remove_returnst::undo_function_calls(
384387
{
385388
if(i_it->is_function_call())
386389
{
387-
code_function_callt &function_call = i_it->get_function_call();
390+
code_function_callt function_call = i_it->get_function_call();
388391

389392
// ignore function pointers
390393
if(function_call.function().id()!=ID_symbol)
@@ -401,8 +404,8 @@ void remove_returnst::undo_function_calls(
401404

402405
// find "f(...); lhs=f#return_value; DEAD f#return_value;"
403406
// and revert to "lhs=f(...);"
404-
goto_programt::instructionst::iterator next=i_it;
405-
++next;
407+
goto_programt::instructionst::iterator next = std::next(i_it);
408+
406409
INVARIANT(
407410
next!=goto_program.instructions.end(),
408411
"non-void function call must be followed by #return_value read");
@@ -423,6 +426,8 @@ void remove_returnst::undo_function_calls(
423426
// restore the previous assignment
424427
function_call.lhs()=assign.lhs();
425428

429+
i_it->set_function_call(function_call);
430+
426431
// remove the assignment and subsequent dead
427432
// i_it remains valid
428433
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

src/goto-programs/string_abstraction.cpp

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -489,22 +489,27 @@ goto_programt::targett string_abstractiont::abstract_assign(
489489
goto_programt &dest,
490490
goto_programt::targett target)
491491
{
492-
code_assignt &assign = target->get_assign();
492+
{
493+
code_assignt assign = target->get_assign();
493494

494-
exprt &lhs=assign.lhs();
495-
exprt &rhs=assign.rhs();
495+
exprt &lhs = assign.lhs();
496+
exprt &rhs = assign.rhs();
496497

497-
if(has_string_macros(lhs))
498-
{
499-
replace_string_macros(lhs, true, target->source_location);
500-
move_lhs_arithmetic(lhs, rhs);
498+
if(has_string_macros(lhs))
499+
{
500+
replace_string_macros(lhs, true, target->source_location);
501+
move_lhs_arithmetic(lhs, rhs);
502+
}
503+
504+
if(has_string_macros(rhs))
505+
replace_string_macros(rhs, false, target->source_location);
506+
507+
target->set_assign(assign);
501508
}
502509

503-
if(has_string_macros(rhs))
504-
replace_string_macros(rhs, false, target->source_location);
510+
const typet &type = target->get_assign().lhs().type();
505511

506-
const typet &type = lhs.type();
507-
if(type.id()==ID_pointer || type.id()==ID_array)
512+
if(type.id() == ID_pointer)
508513
return abstract_pointer_assign(dest, target);
509514
else if(is_char_type(type))
510515
return abstract_char_assign(dest, target);
@@ -515,7 +520,8 @@ goto_programt::targett string_abstractiont::abstract_assign(
515520
void string_abstractiont::abstract_function_call(
516521
goto_programt::targett target)
517522
{
518-
code_function_callt &call = target->get_function_call();
523+
code_function_callt call = target->get_function_call();
524+
519525
code_function_callt::argumentst &arguments=call.arguments();
520526
code_function_callt::argumentst str_args;
521527

@@ -563,6 +569,8 @@ void string_abstractiont::abstract_function_call(
563569
}
564570

565571
arguments.insert(arguments.end(), str_args.begin(), str_args.end());
572+
573+
target->set_function_call(call);
566574
}
567575

568576
bool string_abstractiont::has_string_macros(const exprt &expr)

0 commit comments

Comments
 (0)