Skip to content

Commit e261c0d

Browse files
kroeningkroening
committed
introduce instructiont::assign_lhs() and assign_rhs()
This mirrors the change in #5861 by replacing the use of code_assignt by directly returning the lhs and rhs expressions. The client code is simplified.
1 parent 818fdf2 commit e261c0d

21 files changed

+108
-117
lines changed

‎jbmc/src/java_bytecode/remove_java_new.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -364,14 +364,12 @@ goto_programt::targett remove_java_newt::lower_java_new(
364364
if(!target->is_assign())
365365
return target;
366366

367-
if(as_const(*target).get_assign().rhs().id() == ID_side_effect)
367+
if(as_const(*target).assign_rhs().id() == ID_side_effect)
368368
{
369369
// we make a copy, as we intend to destroy the assignment
370370
// inside lower_java_new and lower_java_new_array
371-
const auto code_assign = target->get_assign();
372-
373-
const exprt &lhs = code_assign.lhs();
374-
const exprt &rhs = code_assign.rhs();
371+
const exprt &lhs = target->assign_lhs();
372+
const exprt &rhs = target->assign_rhs();
375373

376374
const auto &side_effect_expr = to_side_effect_expr(rhs);
377375
const auto &statement = side_effect_expr.get_statement();

‎src/analyses/constant_propagator.cpp

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -163,9 +163,8 @@ void constant_propagator_domaint::transform(
163163
}
164164
else if(from->is_assign())
165165
{
166-
const auto &assignment = from->get_assign();
167-
const exprt &lhs=assignment.lhs();
168-
const exprt &rhs=assignment.rhs();
166+
const exprt &lhs = from->assign_lhs();
167+
const exprt &rhs = from->assign_rhs();
169168
assign_rec(values, lhs, rhs, ns, cp, true);
170169
}
171170
else if(from->is_assume())
@@ -769,14 +768,12 @@ void constant_propagator_ait::replace(
769768
}
770769
else if(it->is_assign())
771770
{
772-
auto assign = it->get_assign();
773-
exprt &rhs = assign.rhs();
771+
exprt &rhs = it->assign_rhs();
774772

775773
if(!constant_propagator_domaint::partial_evaluate(d.values, rhs, ns))
776774
{
777775
if(rhs.id() == ID_constant)
778-
rhs.add_source_location() = assign.lhs().source_location();
779-
it->set_assign(assign);
776+
rhs.add_source_location() = it->assign_lhs().source_location();
780777
}
781778
}
782779
else if(it->is_function_call())

‎src/goto-analyzer/static_simplifier.cpp

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -107,26 +107,21 @@ bool static_simplifier(
107107
}
108108
else if(i_it->is_assign())
109109
{
110-
auto assign = i_it->get_assign();
111-
112110
// Simplification needs to be aware of which side of the
113111
// expression it is handling as:
114112
// <i=0, j=1> i=j
115113
// should simplify to i=1, not to 0=1.
116114

117-
bool unchanged_lhs =
118-
ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);
115+
bool unchanged_lhs = ai.abstract_state_before(i_it)->ai_simplify_lhs(
116+
i_it->assign_lhs(), ns);
119117

120118
bool unchanged_rhs =
121-
ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
119+
ai.abstract_state_before(i_it)->ai_simplify(i_it->assign_rhs(), ns);
122120

123121
if(unchanged_lhs && unchanged_rhs)
124122
unmodified.assigns++;
125123
else
126-
{
127124
simplified.assigns++;
128-
i_it->set_assign(assign);
129-
}
130125
}
131126
else if(i_it->is_function_call())
132127
{

‎src/goto-instrument/accelerate/accelerate.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -367,7 +367,7 @@ void acceleratet::add_dirty_checks()
367367
// variables is clean _before_ clearing any dirty flags.
368368
if(it->is_assign())
369369
{
370-
const exprt &lhs = it->get_assign().lhs();
370+
const exprt &lhs = it->assign_lhs();
371371
expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
372372

373373
if(dirty_var!=dirty_vars_map.end())
@@ -387,7 +387,7 @@ void acceleratet::add_dirty_checks()
387387

388388
if(it->is_assign())
389389
{
390-
find_symbols_or_nexts(it->get_assign().rhs(), read);
390+
find_symbols_or_nexts(it->assign_rhs(), read);
391391
}
392392

393393
for(find_symbols_sett::iterator jt=read.begin();

‎src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -915,8 +915,8 @@ bool acceleration_utilst::do_nonrecursive(
915915
{
916916
if(it->is_assign())
917917
{
918-
exprt lhs = it->get_assign().lhs();
919-
exprt rhs = it->get_assign().rhs();
918+
exprt lhs = it->assign_lhs();
919+
exprt rhs = it->assign_rhs();
920920

921921
if(lhs.id()==ID_dereference)
922922
{

‎src/goto-instrument/code_contracts.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -408,7 +408,7 @@ void code_contractst::instrument_assigns_statement(
408408
instruction_iterator->is_assign(),
409409
"The first argument of instrument_assigns_statement should always be"
410410
" an assignment");
411-
const exprt &lhs = instruction_iterator->get_assign().lhs();
411+
const exprt &lhs = instruction_iterator->assign_lhs();
412412
if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
413413
{
414414
return;
@@ -450,10 +450,9 @@ void code_contractst::instrument_call_statement(
450450
local_instruction_iterator++;
451451
if(
452452
local_instruction_iterator->is_assign() &&
453-
local_instruction_iterator->get_assign().lhs().is_not_nil())
453+
local_instruction_iterator->assign_lhs().is_not_nil())
454454
{
455-
freely_assignable_exprs.insert(
456-
local_instruction_iterator->get_assign().lhs());
455+
freely_assignable_exprs.insert(local_instruction_iterator->assign_lhs());
457456
}
458457
return; // assume malloc edits no currently-existing memory objects.
459458
}

‎src/goto-instrument/count_eloc.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -173,9 +173,8 @@ void print_global_state_size(const goto_modelt &goto_model)
173173
{
174174
if(ins.is_assign())
175175
{
176-
const code_assignt &code_assign = ins.get_assign();
177176
object_descriptor_exprt ode;
178-
ode.build(code_assign.lhs(), ns);
177+
ode.build(ins.assign_lhs(), ns);
179178

180179
if(ode.root_object().id() == ID_symbol)
181180
{

‎src/goto-instrument/goto_program2code.cpp

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -108,8 +108,8 @@ void goto_program2codet::scan_for_varargs()
108108
{
109109
if(instruction.is_assign())
110110
{
111-
const exprt &l = instruction.get_assign().lhs();
112-
const exprt &r = instruction.get_assign().rhs();
111+
const exprt &l = instruction.assign_lhs();
112+
const exprt &r = instruction.assign_rhs();
113113

114114
// find va_start
115115
if(
@@ -287,7 +287,7 @@ goto_programt::const_targett goto_program2codet::convert_assign(
287287
goto_programt::const_targett upper_bound,
288288
code_blockt &dest)
289289
{
290-
const code_assignt &a = target->get_assign();
290+
const code_assignt a{target->assign_lhs(), target->assign_rhs()};
291291

292292
if(va_list_expr.find(a.lhs())!=va_list_expr.end())
293293
return convert_assign_varargs(target, upper_bound, dest);
@@ -302,10 +302,8 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
302302
goto_programt::const_targett upper_bound,
303303
code_blockt &dest)
304304
{
305-
const code_assignt &assign = target->get_assign();
306-
307-
const exprt this_va_list_expr=assign.lhs();
308-
const exprt &r=skip_typecast(assign.rhs());
305+
const exprt this_va_list_expr = target->assign_lhs();
306+
const exprt &r = skip_typecast(target->assign_rhs());
309307

310308
if(r.id()==ID_constant &&
311309
(r.is_zero() || to_constant_expr(r).get_value()==ID_NULL))
@@ -348,12 +346,12 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
348346
if(next!=upper_bound &&
349347
next->is_assign())
350348
{
351-
const exprt &n_r = next->get_assign().rhs();
349+
const exprt &n_r = next->assign_rhs();
352350
if(
353351
n_r.id() == ID_dereference &&
354352
skip_typecast(to_dereference_expr(n_r).pointer()) == this_va_list_expr)
355353
{
356-
f.lhs() = next->get_assign().lhs();
354+
f.lhs() = next->assign_lhs();
357355

358356
type_of.arguments().push_back(f.lhs());
359357
f.arguments().push_back(type_of);
@@ -468,14 +466,14 @@ goto_programt::const_targett goto_program2codet::convert_decl(
468466
!next->is_target() &&
469467
(next->is_assign() || next->is_function_call()))
470468
{
471-
exprt lhs = next->is_assign() ? next->get_assign().lhs()
472-
: next->get_function_call().lhs();
469+
exprt lhs =
470+
next->is_assign() ? next->assign_lhs() : next->get_function_call().lhs();
473471
if(lhs==symbol &&
474472
va_list_expr.find(lhs)==va_list_expr.end())
475473
{
476474
if(next->is_assign())
477475
{
478-
d.set_initial_value({next->get_assign().rhs()});
476+
d.set_initial_value({next->assign_rhs()});
479477
}
480478
else
481479
{

‎src/goto-instrument/replace_calls.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,7 @@ void replace_callst::operator()(
100100
goto_programt::const_targett next_it = std::next(it);
101101
if(next_it != goto_program.instructions.end() && next_it->is_assign())
102102
{
103-
const code_assignt &ca = next_it->get_assign();
104-
const exprt &rhs = ca.rhs();
103+
const exprt &rhs = next_it->assign_rhs();
105104

106105
INVARIANT(
107106
rhs != return_value_symbol(id, ns),

‎src/goto-instrument/rw_set.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,8 +49,7 @@ void _rw_set_loct::compute()
4949
{
5050
if(target->is_assign())
5151
{
52-
const auto &assignment = target->get_assign();
53-
assign(assignment.lhs(), assignment.rhs());
52+
assign(target->assign_lhs(), target->assign_rhs());
5453
}
5554
else if(target->is_goto() ||
5655
target->is_assume() ||

‎src/goto-programs/goto_program.cpp

Lines changed: 11 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -298,12 +298,9 @@ std::list<exprt> expressions_read(
298298
}
299299

300300
case ASSIGN:
301-
{
302-
const code_assignt &assignment = instruction.get_assign();
303-
dest.push_back(assignment.rhs());
304-
parse_lhs_read(assignment.lhs(), dest);
301+
dest.push_back(instruction.assign_rhs());
302+
parse_lhs_read(instruction.assign_lhs(), dest);
305303
break;
306-
}
307304

308305
case CATCH:
309306
case THROW:
@@ -342,7 +339,7 @@ std::list<exprt> expressions_written(
342339
break;
343340

344341
case ASSIGN:
345-
dest.push_back(instruction.get_assign().lhs());
342+
dest.push_back(instruction.assign_lhs());
346343
break;
347344

348345
case CATCH:
@@ -934,15 +931,12 @@ void goto_programt::instructiont::transform(
934931

935932
case ASSIGN:
936933
{
937-
auto new_assign_lhs = f(get_assign().lhs());
938-
auto new_assign_rhs = f(get_assign().rhs());
939-
if(new_assign_lhs.has_value() || new_assign_rhs.has_value())
940-
{
941-
auto new_assignment = get_assign();
942-
new_assignment.lhs() = new_assign_lhs.value_or(new_assignment.lhs());
943-
new_assignment.rhs() = new_assign_rhs.value_or(new_assignment.rhs());
944-
set_assign(new_assignment);
945-
}
934+
auto new_assign_lhs = f(assign_lhs());
935+
auto new_assign_rhs = f(assign_rhs());
936+
if(new_assign_lhs.has_value())
937+
assign_lhs() = new_assign_lhs.value();
938+
if(new_assign_rhs.has_value())
939+
assign_rhs() = new_assign_rhs.value();
946940
}
947941
break;
948942

@@ -1027,8 +1021,8 @@ void goto_programt::instructiont::apply(
10271021
break;
10281022

10291023
case ASSIGN:
1030-
f(get_assign().lhs());
1031-
f(get_assign().rhs());
1024+
f(assign_lhs());
1025+
f(assign_rhs());
10321026
break;
10331027

10341028
case DECL:

‎src/goto-programs/goto_program.h

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,13 +183,43 @@ class goto_programt
183183
codet code;
184184

185185
/// Get the assignment for ASSIGN
186+
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
186187
const code_assignt &get_assign() const
187188
{
188189
PRECONDITION(is_assign());
189190
return to_code_assign(code);
190191
}
191192

193+
/// Get the lhs of the assignment for ASSIGN
194+
const exprt &assign_lhs() const
195+
{
196+
PRECONDITION(is_assign());
197+
return to_code_assign(code).lhs();
198+
}
199+
200+
/// Get the lhs of the assignment for ASSIGN
201+
exprt &assign_lhs()
202+
{
203+
PRECONDITION(is_assign());
204+
return to_code_assign(code).lhs();
205+
}
206+
207+
/// Get the rhs of the assignment for ASSIGN
208+
const exprt &assign_rhs() const
209+
{
210+
PRECONDITION(is_assign());
211+
return to_code_assign(code).rhs();
212+
}
213+
214+
/// Get the rhs of the assignment for ASSIGN
215+
exprt &assign_rhs()
216+
{
217+
PRECONDITION(is_assign());
218+
return to_code_assign(code).rhs();
219+
}
220+
192221
/// Set the assignment for ASSIGN
222+
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
193223
void set_assign(code_assignt c)
194224
{
195225
PRECONDITION(is_assign());

‎src/goto-programs/graphml_witness.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -229,9 +229,9 @@ static bool filter_out(
229229
goto_tracet::stepst::const_iterator &it)
230230
{
231231
if(
232-
it->hidden && (!it->pc->is_assign() ||
233-
it->pc->get_assign().rhs().id() != ID_side_effect ||
234-
it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
232+
it->hidden &&
233+
(!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
234+
it->pc->assign_rhs().get(ID_statement) != ID_nondet))
235235
return true;
236236

237237
if(!it->is_assignment() && !it->is_goto() && !it->is_assert())

‎src/goto-programs/mm_io.cpp

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

4646
if(it->is_assign())
4747
{
48-
auto a = it->get_assign();
49-
collect_deref_expr(a.rhs(), deref_expr_r);
48+
auto &a_lhs = it->assign_lhs();
49+
auto &a_rhs = it->assign_rhs();
50+
collect_deref_expr(a_rhs, deref_expr_r);
5051

5152
if(mm_io_r.is_not_nil())
5253
{
@@ -59,8 +60,7 @@ void mm_io(
5960
irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
6061
auto return_value = return_value_symbol(identifier, ns);
6162
if_exprt if_expr(integer_address(d.pointer()), return_value, d);
62-
if(!replace_expr(d, if_expr, a.rhs()))
63-
it->set_assign(a);
63+
replace_expr(d, if_expr, a_rhs);
6464

6565
const typet &pt=ct.parameters()[0].type();
6666
const typet &st=ct.parameters()[1].type();
@@ -78,9 +78,9 @@ void mm_io(
7878

7979
if(mm_io_w.is_not_nil())
8080
{
81-
if(a.lhs().id()==ID_dereference)
81+
if(a_lhs.id() == ID_dereference)
8282
{
83-
const dereference_exprt &d=to_dereference_expr(a.lhs());
83+
const dereference_exprt &d = to_dereference_expr(a_lhs);
8484
source_locationt source_location=it->source_location;
8585
const code_typet &ct=to_code_type(mm_io_w.type());
8686
const typet &pt=ct.parameters()[0].type();
@@ -92,7 +92,7 @@ void mm_io(
9292
mm_io_w,
9393
{typecast_exprt(d.pointer(), pt),
9494
typecast_exprt(size_opt.value(), st),
95-
typecast_exprt(a.rhs(), vt)});
95+
typecast_exprt(a_rhs, vt)});
9696
goto_function.body.insert_before_swap(it);
9797
*it = goto_programt::make_function_call(fc, source_location);
9898
it++;

0 commit comments

Comments
 (0)