Skip to content

Commit 27742dd

Browse files
authored
Merge pull request #3264 from diffblue/exprt_opX_accesses
avoid direct access to exprt::opX
2 parents b55b44d + d6603d3 commit 27742dd

12 files changed

+76
-62
lines changed

src/goto-symex/build_goto_trace.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -92,12 +92,9 @@ exprt build_full_lhs_rec(
9292
else if(id==ID_byte_extract_little_endian ||
9393
id==ID_byte_extract_big_endian)
9494
{
95-
exprt tmp=src_original;
96-
tmp.op0() = build_full_lhs_rec(
97-
prop_conv,
98-
ns,
99-
to_byte_extract_expr(tmp).op(),
100-
to_byte_extract_expr(src_ssa).op());
95+
byte_extract_exprt tmp = to_byte_extract_expr(src_original);
96+
tmp.op() = build_full_lhs_rec(
97+
prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
10198

10299
// re-write into big case-split
103100
}

src/goto-symex/goto_symex_state.cpp

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -132,13 +132,20 @@ static bool check_renaming(const exprt &expr)
132132
if(check_renaming(expr.type()))
133133
return true;
134134

135-
if(expr.id()==ID_address_of &&
136-
expr.op0().id()==ID_symbol)
137-
return check_renaming_l1(expr.op0());
138-
else if(expr.id()==ID_address_of &&
139-
expr.op0().id()==ID_index)
140-
return check_renaming_l1(expr.op0().op0()) ||
141-
check_renaming(expr.op0().op1());
135+
if(
136+
expr.id() == ID_address_of &&
137+
to_address_of_expr(expr).object().id() == ID_symbol)
138+
{
139+
return check_renaming_l1(to_address_of_expr(expr).object());
140+
}
141+
else if(
142+
expr.id() == ID_address_of &&
143+
to_address_of_expr(expr).object().id() == ID_index)
144+
{
145+
const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
146+
return check_renaming_l1(index_expr.array()) ||
147+
check_renaming(index_expr.index());
148+
}
142149
else if(expr.id()==ID_symbol)
143150
{
144151
if(!expr.get_bool(ID_C_SSA_symbol))

src/goto-symex/symex_dead.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ void goto_symext::symex_dead(statet &state)
3030
state.rename(ssa, ns, goto_symex_statet::L1);
3131

3232
// in case of pointers, put something into the value set
33-
if(ns.follow(code.op0().type()).id()==ID_pointer)
33+
if(ns.follow(code.symbol().type()).id() == ID_pointer)
3434
{
3535
exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
3636

src/goto-symex/symex_decl.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,8 @@ void goto_symext::symex_decl(statet &state)
2828
// two-operand decl not supported here
2929
// we handle the decl with only one operand
3030
PRECONDITION(code.operands().size() == 1);
31-
PRECONDITION(code.op0().id() == ID_symbol);
3231

33-
symex_decl(state, to_symbol_expr(code.op0()));
32+
symex_decl(state, to_symbol_expr(to_code_decl(code).symbol()));
3433
}
3534

3635
void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)

src/goto-symex/symex_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -270,7 +270,7 @@ void goto_symext::dereference_rec(
270270
}
271271

272272
exprt tmp1;
273-
tmp1.swap(expr.op0());
273+
tmp1.swap(to_dereference_expr(expr).pointer());
274274

275275
// first make sure there are no dereferences in there
276276
dereference_rec(tmp1, state, guard, false);

src/goto-symex/symex_function_call.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -435,7 +435,7 @@ void goto_symext::return_assignment(statet &state)
435435

436436
PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
437437

438-
exprt value = code.op0();
438+
exprt value = code.return_value();
439439

440440
if(frame.return_value.is_not_nil())
441441
{

src/goto-symex/symex_goto.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -233,11 +233,13 @@ void goto_symext::symex_goto(statet &state)
233233
// produce new guard symbol
234234
exprt guard_expr;
235235

236-
if(new_guard.id()==ID_symbol ||
237-
(new_guard.id()==ID_not &&
238-
new_guard.operands().size()==1 &&
239-
new_guard.op0().id()==ID_symbol))
236+
if(
237+
new_guard.id() == ID_symbol ||
238+
(new_guard.id() == ID_not &&
239+
to_not_expr(new_guard).op().id() == ID_symbol))
240+
{
240241
guard_expr=new_guard;
242+
}
241243
else
242244
{
243245
symbol_exprt guard_symbol_expr=

src/util/config.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1101,13 +1101,14 @@ static irep_idt string_from_ns(
11011101
const exprt &tmp=symbol->value;
11021102

11031103
INVARIANT(
1104-
tmp.id() == ID_address_of && tmp.operands().size() == 1 &&
1105-
tmp.op0().id() == ID_index && tmp.op0().operands().size() == 2 &&
1106-
tmp.op0().op0().id() == ID_string_constant,
1104+
tmp.id() == ID_address_of &&
1105+
to_address_of_expr(tmp).object().id() == ID_index &&
1106+
to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1107+
ID_string_constant,
11071108
"symbol table configuration entry `" + id2string(id) +
11081109
"' must be a string constant");
11091110

1110-
return tmp.op0().op0().get(ID_value);
1111+
return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
11111112
}
11121113

11131114
static unsigned unsigned_from_ns(

src/util/expr_util.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,8 @@ exprt make_binary(const exprt &expr)
5656
exprt tmp=expr;
5757
tmp.operands().clear();
5858
tmp.operands().resize(2);
59-
tmp.op0().swap(previous);
60-
tmp.op1()=*it;
59+
to_binary_expr(tmp).op0().swap(previous);
60+
to_binary_expr(tmp).op1() = *it;
6161
previous.swap(tmp);
6262
}
6363

@@ -126,8 +126,8 @@ exprt is_not_zero(
126126

127127
exprt boolean_negate(const exprt &src)
128128
{
129-
if(src.id()==ID_not && src.operands().size()==1)
130-
return src.op0();
129+
if(src.id() == ID_not)
130+
return to_not_expr(src).op();
131131
else if(src.is_true())
132132
return false_exprt();
133133
else if(src.is_false())

src/util/json_expr.cpp

Lines changed: 35 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -39,42 +39,47 @@ static exprt simplify_json_expr(
3939
{
4040
const irep_idt &value=to_constant_expr(src).get_value();
4141

42-
if(value!=ID_NULL &&
43-
(value!=std::string(value.size(), '0') ||
44-
!config.ansi_c.NULL_is_zero) &&
45-
src.operands().size()==1 &&
46-
src.op0().id()!=ID_constant)
47-
// try to simplify the constant pointer
48-
return simplify_json_expr(src.op0(), ns);
42+
if(
43+
value != ID_NULL &&
44+
(value != std::string(value.size(), '0') ||
45+
!config.ansi_c.NULL_is_zero) &&
46+
src.operands().size() == 1 &&
47+
to_unary_expr(src).op().id() != ID_constant)
48+
// try to simplify the constant pointer
49+
{
50+
return simplify_json_expr(to_unary_expr(src).op(), ns);
51+
}
4952
}
5053
}
51-
else if(src.id()==ID_address_of &&
52-
src.operands().size()==1 &&
53-
src.op0().id()==ID_member &&
54-
id2string(to_member_expr(
55-
src.op0()).get_component_name()).find("@")!=std::string::npos)
54+
else if(
55+
src.id() == ID_address_of &&
56+
to_address_of_expr(src).object().id() == ID_member &&
57+
id2string(
58+
to_member_expr(to_address_of_expr(src).object()).get_component_name())
59+
.find("@") != std::string::npos)
5660
{
5761
// simplify expressions of the form &member_expr(object, @class_identifier)
58-
return simplify_json_expr(src.op0(), ns);
62+
return simplify_json_expr(to_address_of_expr(src).object(), ns);
5963
}
60-
else if(src.id()==ID_address_of &&
61-
src.operands().size()==1 &&
62-
src.op0().id()==ID_index &&
63-
to_index_expr(src.op0()).index().id()==ID_constant &&
64-
to_constant_expr(
65-
to_index_expr(src.op0()).index()).value_is_zero_string())
64+
else if(
65+
src.id() == ID_address_of &&
66+
to_address_of_expr(src).object().id() == ID_index &&
67+
to_index_expr(to_address_of_expr(src).object()).index().id() ==
68+
ID_constant &&
69+
to_constant_expr(to_index_expr(to_address_of_expr(src).object()).index())
70+
.value_is_zero_string())
6671
{
6772
// simplify expressions of the form &array[0]
68-
return simplify_json_expr(to_index_expr(src.op0()).array(), ns);
73+
return simplify_json_expr(
74+
to_index_expr(to_address_of_expr(src).object()).array(), ns);
6975
}
7076
else if(src.id()==ID_member &&
71-
src.operands().size()==1 &&
7277
id2string(
7378
to_member_expr(src).get_component_name())
7479
.find("@")!=std::string::npos)
7580
{
7681
// simplify expressions of the form member_expr(object, @class_identifier)
77-
return simplify_json_expr(src.op0(), ns);
82+
return simplify_json_expr(to_member_expr(src).struct_op(), ns);
7883
}
7984

8085
return src;
@@ -317,11 +322,15 @@ json_objectt json(
317322
result["name"]=json_stringt("pointer");
318323
result["type"]=json_stringt(type_string);
319324
exprt simpl_expr=simplify_json_expr(expr, ns);
320-
if(simpl_expr.get(ID_value)==ID_NULL ||
321-
// remove typecast on NULL
322-
(simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer &&
323-
simpl_expr.op0().get(ID_value)==ID_NULL))
325+
if(
326+
simpl_expr.get(ID_value) == ID_NULL ||
327+
// remove typecast on NULL
328+
(simpl_expr.id() == ID_constant &&
329+
simpl_expr.type().id() == ID_pointer &&
330+
to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
331+
{
324332
result["data"]=json_stringt(value_string);
333+
}
325334
else if(simpl_expr.id()==ID_symbol)
326335
{
327336
const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();

src/util/ssa_expr.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,9 +77,10 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
7777
{
7878
if(expr.id()==ID_symbol)
7979
return true;
80-
else if(expr.id()==ID_member ||
81-
expr.id()==ID_index)
82-
return can_build_identifier(expr.op0());
80+
else if(expr.id() == ID_member)
81+
return can_build_identifier(to_member_expr(expr).compound());
82+
else if(expr.id() == ID_index)
83+
return can_build_identifier(to_index_expr(expr).array());
8384
else
8485
return false;
8586
}

src/util/std_code.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -134,9 +134,7 @@ codet &code_blockt::find_last_statement()
134134
}
135135
else if(statement==ID_label)
136136
{
137-
DATA_INVARIANT(
138-
last->operands().size() == 1, "label must have one operand");
139-
last=&(to_code(last->op0()));
137+
last = &(to_code_label(*last).code());
140138
}
141139
else
142140
break;

0 commit comments

Comments
 (0)