Skip to content

Commit 32a78bf

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 1ea6f18 commit 32a78bf

23 files changed

+112
-128
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_nonconst();
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: 4 additions & 9 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_nonconst(), ns);
119117

120-
bool unchanged_rhs =
121-
ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
118+
bool unchanged_rhs = ai.abstract_state_before(i_it)->ai_simplify(
119+
i_it->assign_rhs_nonconst(), 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
@@ -392,7 +392,7 @@ void code_contractst::instrument_assigns_statement(
392392
instruction_iterator->is_assign(),
393393
"The first argument of instrument_assigns_statement should always be"
394394
" an assignment");
395-
const exprt &lhs = instruction_iterator->get_assign().lhs();
395+
const exprt &lhs = instruction_iterator->assign_lhs();
396396
if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
397397
{
398398
return;
@@ -434,10 +434,9 @@ void code_contractst::instrument_call_statement(
434434
local_instruction_iterator++;
435435
if(
436436
local_instruction_iterator->is_assign() &&
437-
local_instruction_iterator->get_assign().lhs().is_not_nil())
437+
local_instruction_iterator->assign_lhs().is_not_nil())
438438
{
439-
freely_assignable_exprs.insert(
440-
local_instruction_iterator->get_assign().lhs());
439+
freely_assignable_exprs.insert(local_instruction_iterator->assign_lhs());
441440
}
442441
return; // assume malloc edits no currently-existing memory objects.
443442
}

‎src/goto-instrument/concurrency.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -108,8 +108,7 @@ void concurrency_instrumentationt::instrument(
108108
{
109109
if(it->is_assign())
110110
{
111-
code_assignt &code = to_code_assign(it->code_nonconst());
112-
instrument(code.rhs());
111+
instrument(it->assign_rhs_nonconst());
113112
}
114113
else if(it->is_assume() || it->is_assert() || it->is_goto())
115114
{

‎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/nondet_volatile.cpp

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -226,15 +226,9 @@ void nondet_volatilet::nondet_volatile(
226226
if(instruction.is_assign())
227227
{
228228
nondet_volatile_rhs(
229-
symbol_table,
230-
to_code_assign(instruction.code_nonconst()).rhs(),
231-
pre,
232-
post);
229+
symbol_table, instruction.assign_rhs_nonconst(), pre, post);
233230
nondet_volatile_lhs(
234-
symbol_table,
235-
to_code_assign(instruction.code_nonconst()).lhs(),
236-
pre,
237-
post);
231+
symbol_table, instruction.assign_lhs_nonconst(), pre, post);
238232
}
239233
else if(instruction.is_function_call())
240234
{

‎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_nonconst() = new_assign_lhs.value();
938+
if(new_assign_rhs.has_value())
939+
assign_rhs_nonconst() = 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
@@ -196,13 +196,43 @@ class goto_programt
196196
}
197197

198198
/// Get the assignment for ASSIGN
199+
DEPRECATED(SINCE(2021, 2, 24, "Use assign_lhs/rhs instead"))
199200
const code_assignt &get_assign() const
200201
{
201202
PRECONDITION(is_assign());
202203
return to_code_assign(code);
203204
}
204205

206+
/// Get the lhs of the assignment for ASSIGN
207+
const exprt &assign_lhs() const
208+
{
209+
PRECONDITION(is_assign());
210+
return to_code_assign(code).lhs();
211+
}
212+
213+
/// Get the lhs of the assignment for ASSIGN
214+
exprt &assign_lhs_nonconst()
215+
{
216+
PRECONDITION(is_assign());
217+
return to_code_assign(code).lhs();
218+
}
219+
220+
/// Get the rhs of the assignment for ASSIGN
221+
const exprt &assign_rhs() const
222+
{
223+
PRECONDITION(is_assign());
224+
return to_code_assign(code).rhs();
225+
}
226+
227+
/// Get the rhs of the assignment for ASSIGN
228+
exprt &assign_rhs_nonconst()
229+
{
230+
PRECONDITION(is_assign());
231+
return to_code_assign(code).rhs();
232+
}
233+
205234
/// Set the assignment for ASSIGN
235+
DEPRECATED(SINCE(2021, 2, 24, "Use assign_lhs/rhs instead"))
206236
void set_assign(code_assignt c)
207237
{
208238
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())

0 commit comments

Comments
 (0)