Skip to content

Commit 9ff5919

Browse files
kroeningtautschnig
kroening
authored and
tautschnig
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 e9b5f5c commit 9ff5919

23 files changed

+113
-126
lines changed

‎jbmc/src/java_bytecode/remove_java_new.cpp

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

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

377375
const auto &side_effect_expr = to_side_effect_expr(rhs);
378376
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
@@ -162,9 +162,8 @@ void constant_propagator_domaint::transform(
162162
}
163163
else if(from->is_assign())
164164
{
165-
const auto &assignment = from->get_assign();
166-
const exprt &lhs=assignment.lhs();
167-
const exprt &rhs=assignment.rhs();
165+
const exprt &lhs = from->assign_lhs();
166+
const exprt &rhs = from->assign_rhs();
168167
assign_rec(values, lhs, rhs, ns, cp, true);
169168
}
170169
else if(from->is_assume())
@@ -768,14 +767,12 @@ void constant_propagator_ait::replace(
768767
}
769768
else if(it->is_assign())
770769
{
771-
auto assign = it->get_assign();
772-
exprt &rhs = assign.rhs();
770+
exprt &rhs = it->assign_rhs_nonconst();
773771

774772
if(!constant_propagator_domaint::partial_evaluate(d.values, rhs, ns))
775773
{
776774
if(rhs.id() == ID_constant)
777-
rhs.add_source_location() = assign.lhs().source_location();
778-
it->set_assign(assign);
775+
rhs.add_source_location() = it->assign_lhs().source_location();
779776
}
780777
}
781778
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
@@ -365,7 +365,7 @@ void acceleratet::add_dirty_checks()
365365
// variables is clean _before_ clearing any dirty flags.
366366
if(it->is_assign())
367367
{
368-
const exprt &lhs = it->get_assign().lhs();
368+
const exprt &lhs = it->assign_lhs();
369369
expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
370370

371371
if(dirty_var!=dirty_vars_map.end())
@@ -385,7 +385,7 @@ void acceleratet::add_dirty_checks()
385385

386386
if(it->is_assign())
387387
{
388-
find_symbols_or_nexts(it->get_assign().rhs(), read);
388+
find_symbols_or_nexts(it->assign_rhs(), read);
389389
}
390390

391391
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
@@ -905,8 +905,8 @@ bool acceleration_utilst::do_nonrecursive(
905905
{
906906
if(it->is_assign())
907907
{
908-
exprt lhs = it->get_assign().lhs();
909-
exprt rhs = it->get_assign().rhs();
908+
exprt lhs = it->assign_lhs();
909+
exprt rhs = it->assign_rhs();
910910

911911
if(lhs.id()==ID_dereference)
912912
{

‎src/goto-instrument/code_contracts.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -534,7 +534,7 @@ void code_contractst::instrument_assign_statement(
534534
"The first instruction of instrument_assign_statement should always be"
535535
" an assignment");
536536

537-
const exprt &lhs = instruction_iterator->get_assign().lhs();
537+
const exprt &lhs = instruction_iterator->assign_lhs();
538538

539539
goto_programt alias_assertion;
540540
alias_assertion.add(goto_programt::make_assertion(
@@ -573,7 +573,7 @@ void code_contractst::instrument_call_statement(
573573
local_instruction_iterator++;
574574
if(local_instruction_iterator->is_assign())
575575
{
576-
const exprt &rhs = local_instruction_iterator->get_assign().rhs();
576+
const exprt &rhs = local_instruction_iterator->assign_rhs();
577577
INVARIANT(
578578
rhs.id() == ID_typecast,
579579
"malloc is called but the result is not cast. Excluding result from "

‎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
@@ -107,8 +107,8 @@ void goto_program2codet::scan_for_varargs()
107107
{
108108
if(instruction.is_assign())
109109
{
110-
const exprt &l = instruction.get_assign().lhs();
111-
const exprt &r = instruction.get_assign().rhs();
110+
const exprt &l = instruction.assign_lhs();
111+
const exprt &r = instruction.assign_rhs();
112112

113113
// find va_start
114114
if(
@@ -286,7 +286,7 @@ goto_programt::const_targett goto_program2codet::convert_assign(
286286
goto_programt::const_targett upper_bound,
287287
code_blockt &dest)
288288
{
289-
const code_assignt &a = target->get_assign();
289+
const code_assignt a{target->assign_lhs(), target->assign_rhs()};
290290

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

309307
if(r.id()==ID_constant &&
310308
(r.is_zero() || to_constant_expr(r).get_value()==ID_NULL))
@@ -347,12 +345,12 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
347345
if(next!=upper_bound &&
348346
next->is_assign())
349347
{
350-
const exprt &n_r = next->get_assign().rhs();
348+
const exprt &n_r = next->assign_rhs();
351349
if(
352350
n_r.id() == ID_dereference &&
353351
skip_typecast(to_dereference_expr(n_r).pointer()) == this_va_list_expr)
354352
{
355-
f.lhs() = next->get_assign().lhs();
353+
f.lhs() = next->assign_lhs();
356354

357355
type_of.arguments().push_back(f.lhs());
358356
f.arguments().push_back(type_of);
@@ -467,14 +465,14 @@ goto_programt::const_targett goto_program2codet::convert_decl(
467465
!next->is_target() &&
468466
(next->is_assign() || next->is_function_call()))
469467
{
470-
exprt lhs = next->is_assign() ? next->get_assign().lhs()
471-
: next->get_function_call().lhs();
468+
exprt lhs =
469+
next->is_assign() ? next->assign_lhs() : next->get_function_call().lhs();
472470
if(lhs==symbol &&
473471
va_list_expr.find(lhs)==va_list_expr.end())
474472
{
475473
if(next->is_assign())
476474
{
477-
d.set_initial_value({next->get_assign().rhs()});
475+
d.set_initial_value({next->assign_rhs()});
478476
}
479477
else
480478
{

‎src/goto-instrument/nondet_volatile.cpp

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -228,15 +228,9 @@ void nondet_volatilet::nondet_volatile(
228228
if(instruction.is_assign())
229229
{
230230
nondet_volatile_rhs(
231-
symbol_table,
232-
to_code_assign(instruction.code_nonconst()).rhs(),
233-
pre,
234-
post);
231+
symbol_table, instruction.assign_rhs_nonconst(), pre, post);
235232
nondet_volatile_lhs(
236-
symbol_table,
237-
to_code_assign(instruction.code_nonconst()).lhs(),
238-
pre,
239-
post);
233+
symbol_table, instruction.assign_lhs_nonconst(), pre, post);
240234
}
241235
else if(instruction.is_function_call())
242236
{

‎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
@@ -47,8 +47,7 @@ void _rw_set_loct::compute()
4747
{
4848
if(target->is_assign())
4949
{
50-
const auto &assignment = target->get_assign();
51-
assign(assignment.lhs(), assignment.rhs());
50+
assign(target->assign_lhs(), target->assign_rhs());
5251
}
5352
else if(target->is_goto() ||
5453
target->is_assume() ||

‎src/goto-programs/goto_program.cpp

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

297297
case ASSIGN:
298-
{
299-
const code_assignt &assignment = instruction.get_assign();
300-
dest.push_back(assignment.rhs());
301-
parse_lhs_read(assignment.lhs(), dest);
298+
dest.push_back(instruction.assign_rhs());
299+
parse_lhs_read(instruction.assign_lhs(), dest);
302300
break;
303-
}
304301

305302
case CATCH:
306303
case THROW:
@@ -339,7 +336,7 @@ std::list<exprt> expressions_written(
339336
break;
340337

341338
case ASSIGN:
342-
dest.push_back(instruction.get_assign().lhs());
339+
dest.push_back(instruction.assign_lhs());
343340
break;
344341

345342
case CATCH:
@@ -931,15 +928,12 @@ void goto_programt::instructiont::transform(
931928

932929
case ASSIGN:
933930
{
934-
auto new_assign_lhs = f(get_assign().lhs());
935-
auto new_assign_rhs = f(get_assign().rhs());
936-
if(new_assign_lhs.has_value() || new_assign_rhs.has_value())
937-
{
938-
auto new_assignment = get_assign();
939-
new_assignment.lhs() = new_assign_lhs.value_or(new_assignment.lhs());
940-
new_assignment.rhs() = new_assign_rhs.value_or(new_assignment.rhs());
941-
set_assign(new_assignment);
942-
}
931+
auto new_assign_lhs = f(assign_lhs());
932+
auto new_assign_rhs = f(assign_rhs());
933+
if(new_assign_lhs.has_value())
934+
assign_lhs_nonconst() = new_assign_lhs.value();
935+
if(new_assign_rhs.has_value())
936+
assign_rhs_nonconst() = new_assign_rhs.value();
943937
}
944938
break;
945939

@@ -1031,8 +1025,8 @@ void goto_programt::instructiont::apply(
10311025
break;
10321026

10331027
case ASSIGN:
1034-
f(get_assign().lhs());
1035-
f(get_assign().rhs());
1028+
f(assign_lhs());
1029+
f(assign_rhs());
10361030
break;
10371031

10381032
case DECL:

‎src/goto-programs/goto_program.h

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -194,13 +194,43 @@ class goto_programt
194194
}
195195

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

204+
/// Get the lhs of the assignment for ASSIGN
205+
const exprt &assign_lhs() const
206+
{
207+
PRECONDITION(is_assign());
208+
return to_code_assign(code).lhs();
209+
}
210+
211+
/// Get the lhs of the assignment for ASSIGN
212+
exprt &assign_lhs_nonconst()
213+
{
214+
PRECONDITION(is_assign());
215+
return to_code_assign(code).lhs();
216+
}
217+
218+
/// Get the rhs of the assignment for ASSIGN
219+
const exprt &assign_rhs() const
220+
{
221+
PRECONDITION(is_assign());
222+
return to_code_assign(code).rhs();
223+
}
224+
225+
/// Get the rhs of the assignment for ASSIGN
226+
exprt &assign_rhs_nonconst()
227+
{
228+
PRECONDITION(is_assign());
229+
return to_code_assign(code).rhs();
230+
}
231+
203232
/// Set the assignment for ASSIGN
233+
DEPRECATED(SINCE(2021, 2, 24, "Use assign_lhs/rhs instead"))
204234
void set_assign(code_assignt c)
205235
{
206236
PRECONDITION(is_assign());

‎src/goto-programs/graphml_witness.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -231,9 +231,9 @@ static bool filter_out(
231231
goto_tracet::stepst::const_iterator &it)
232232
{
233233
if(
234-
it->hidden && (!it->pc->is_assign() ||
235-
it->pc->get_assign().rhs().id() != ID_side_effect ||
236-
it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
234+
it->hidden &&
235+
(!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
236+
it->pc->assign_rhs().get(ID_statement) != ID_nondet))
237237
return true;
238238

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

0 commit comments

Comments
 (0)