Skip to content

Commit 5b6a99e

Browse files
author
Daniel Kroening
authored
Merge pull request #5109 from diffblue/protect-exprt-opX
Protect exprt::opX()
2 parents 71d55b5 + 91d941b commit 5b6a99e

File tree

5 files changed

+124
-46
lines changed

5 files changed

+124
-46
lines changed

‎src/assembler/remove_asm.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,8 @@ void remove_asmt::gcc_asm_function_call(
8585
{
8686
if(it->operands().size() == 2)
8787
{
88-
arguments.push_back(
89-
typecast_exprt(address_of_exprt(it->op1()), void_pointer));
88+
arguments.push_back(typecast_exprt(
89+
address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
9090
}
9191
}
9292

@@ -95,8 +95,8 @@ void remove_asmt::gcc_asm_function_call(
9595
{
9696
if(it->operands().size() == 2)
9797
{
98-
arguments.push_back(
99-
typecast_exprt(address_of_exprt(it->op1()), void_pointer));
98+
arguments.push_back(typecast_exprt(
99+
address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
100100
}
101101
}
102102

‎src/linking/linking.cpp

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -201,7 +201,14 @@ void linkingt::detailed_conflict_report_rec(
201201
e.id()==ID_index)
202202
{
203203
parent_types.insert(e.type());
204-
e=e.op0();
204+
if(e.id() == ID_dereference)
205+
e = to_dereference_expr(e).pointer();
206+
else if(e.id() == ID_member)
207+
e = to_member_expr(e).compound();
208+
else if(e.id() == ID_index)
209+
e = to_index_expr(e).array();
210+
else
211+
UNREACHABLE;
205212
}
206213

207214
conflict_path=conflict_path_before;

‎src/solvers/floatbv/float_bv.cpp

Lines changed: 109 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -20,76 +20,145 @@ exprt float_bvt::convert(const exprt &expr) const
2020
else if(expr.id()==ID_unary_minus)
2121
return negation(to_unary_minus_expr(expr).op(), get_spec(expr));
2222
else if(expr.id()==ID_ieee_float_equal)
23-
return is_equal(expr.op0(), expr.op1(), get_spec(expr.op0()));
23+
{
24+
const auto &equal_expr = to_ieee_float_equal_expr(expr);
25+
return is_equal(
26+
equal_expr.lhs(), equal_expr.rhs(), get_spec(equal_expr.lhs()));
27+
}
2428
else if(expr.id()==ID_ieee_float_notequal)
25-
return not_exprt(is_equal(expr.op0(), expr.op1(), get_spec(expr.op0())));
29+
{
30+
const auto &notequal_expr = to_ieee_float_notequal_expr(expr);
31+
return not_exprt(is_equal(
32+
notequal_expr.lhs(), notequal_expr.rhs(), get_spec(notequal_expr.lhs())));
33+
}
2634
else if(expr.id()==ID_floatbv_typecast)
2735
{
28-
const typet &src_type=expr.op0().type();
29-
const typet &dest_type=expr.type();
36+
const auto &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
37+
const auto &op = floatbv_typecast_expr.op();
38+
const typet &src_type = floatbv_typecast_expr.op().type();
39+
const typet &dest_type = floatbv_typecast_expr.type();
40+
const auto &rounding_mode = floatbv_typecast_expr.rounding_mode();
3041

3142
if(dest_type.id()==ID_signedbv &&
3243
src_type.id()==ID_floatbv) // float -> signed
33-
return
34-
to_signed_integer(
35-
expr.op0(),
36-
to_signedbv_type(dest_type).get_width(),
37-
expr.op1(),
38-
get_spec(expr.op0()));
44+
return to_signed_integer(
45+
op,
46+
to_signedbv_type(dest_type).get_width(),
47+
rounding_mode,
48+
get_spec(op));
3949
else if(dest_type.id()==ID_unsignedbv &&
4050
src_type.id()==ID_floatbv) // float -> unsigned
41-
return
42-
to_unsigned_integer(
43-
expr.op0(),
44-
to_unsignedbv_type(dest_type).get_width(),
45-
expr.op1(),
46-
get_spec(expr.op0()));
51+
return to_unsigned_integer(
52+
op,
53+
to_unsignedbv_type(dest_type).get_width(),
54+
rounding_mode,
55+
get_spec(op));
4756
else if(src_type.id()==ID_signedbv &&
4857
dest_type.id()==ID_floatbv) // signed -> float
49-
return from_signed_integer(
50-
expr.op0(), expr.op1(), get_spec(expr));
58+
return from_signed_integer(op, rounding_mode, get_spec(expr));
5159
else if(src_type.id()==ID_unsignedbv &&
5260
dest_type.id()==ID_floatbv) // unsigned -> float
53-
return from_unsigned_integer(
54-
expr.op0(), expr.op1(), get_spec(expr));
61+
{
62+
return from_unsigned_integer(op, rounding_mode, get_spec(expr));
63+
}
5564
else if(dest_type.id()==ID_floatbv &&
5665
src_type.id()==ID_floatbv) // float -> float
57-
return
58-
conversion(
59-
expr.op0(), expr.op1(), get_spec(expr.op0()), get_spec(expr));
66+
{
67+
return conversion(op, rounding_mode, get_spec(op), get_spec(expr));
68+
}
6069
else
6170
return nil_exprt();
6271
}
63-
else if(expr.id()==ID_typecast &&
64-
expr.type().id()==ID_bool &&
65-
expr.op0().type().id()==ID_floatbv) // float -> bool
66-
return not_exprt(is_zero(expr.op0()));
72+
else if(
73+
expr.id() == ID_typecast && expr.type().id() == ID_bool &&
74+
to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> bool
75+
{
76+
return not_exprt(is_zero(to_typecast_expr(expr).op()));
77+
}
6778
else if(expr.id()==ID_floatbv_plus)
68-
return add_sub(false, expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
79+
{
80+
const auto &float_expr = to_ieee_float_op_expr(expr);
81+
return add_sub(
82+
false,
83+
float_expr.lhs(),
84+
float_expr.rhs(),
85+
float_expr.rounding_mode(),
86+
get_spec(expr));
87+
}
6988
else if(expr.id()==ID_floatbv_minus)
70-
return add_sub(true, expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
89+
{
90+
const auto &float_expr = to_ieee_float_op_expr(expr);
91+
return add_sub(
92+
true,
93+
float_expr.lhs(),
94+
float_expr.rhs(),
95+
float_expr.rounding_mode(),
96+
get_spec(expr));
97+
}
7198
else if(expr.id()==ID_floatbv_mult)
72-
return mul(expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
99+
{
100+
const auto &float_expr = to_ieee_float_op_expr(expr);
101+
return mul(
102+
float_expr.lhs(),
103+
float_expr.rhs(),
104+
float_expr.rounding_mode(),
105+
get_spec(expr));
106+
}
73107
else if(expr.id()==ID_floatbv_div)
74-
return div(expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
108+
{
109+
const auto &float_expr = to_ieee_float_op_expr(expr);
110+
return div(
111+
float_expr.lhs(),
112+
float_expr.rhs(),
113+
float_expr.rounding_mode(),
114+
get_spec(expr));
115+
}
75116
else if(expr.id()==ID_isnan)
76-
return isnan(expr.op0(), get_spec(expr.op0()));
117+
{
118+
const auto &op = to_unary_expr(expr).op();
119+
return isnan(op, get_spec(op));
120+
}
77121
else if(expr.id()==ID_isfinite)
78-
return isfinite(expr.op0(), get_spec(expr.op0()));
122+
{
123+
const auto &op = to_unary_expr(expr).op();
124+
return isfinite(op, get_spec(op));
125+
}
79126
else if(expr.id()==ID_isinf)
80-
return isinf(expr.op0(), get_spec(expr.op0()));
127+
{
128+
const auto &op = to_unary_expr(expr).op();
129+
return isinf(op, get_spec(op));
130+
}
81131
else if(expr.id()==ID_isnormal)
82-
return isnormal(expr.op0(), get_spec(expr.op0()));
132+
{
133+
const auto &op = to_unary_expr(expr).op();
134+
return isnormal(op, get_spec(op));
135+
}
83136
else if(expr.id()==ID_lt)
84-
return relation(expr.op0(), relt::LT, expr.op1(), get_spec(expr.op0()));
137+
{
138+
const auto &rel_expr = to_binary_relation_expr(expr);
139+
return relation(
140+
rel_expr.lhs(), relt::LT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
141+
}
85142
else if(expr.id()==ID_gt)
86-
return relation(expr.op0(), relt::GT, expr.op1(), get_spec(expr.op0()));
143+
{
144+
const auto &rel_expr = to_binary_relation_expr(expr);
145+
return relation(
146+
rel_expr.lhs(), relt::GT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
147+
}
87148
else if(expr.id()==ID_le)
88-
return relation(expr.op0(), relt::LE, expr.op1(), get_spec(expr.op0()));
149+
{
150+
const auto &rel_expr = to_binary_relation_expr(expr);
151+
return relation(
152+
rel_expr.lhs(), relt::LE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
153+
}
89154
else if(expr.id()==ID_ge)
90-
return relation(expr.op0(), relt::GE, expr.op1(), get_spec(expr.op0()));
155+
{
156+
const auto &rel_expr = to_binary_relation_expr(expr);
157+
return relation(
158+
rel_expr.lhs(), relt::GE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
159+
}
91160
else if(expr.id()==ID_sign)
92-
return sign_bit(expr.op0());
161+
return sign_bit(to_unary_expr(expr).op());
93162

94163
return nil_exprt();
95164
}

‎src/statement-list/statement_list_parser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ static void find_instructions(
260260
for(const exprt &instruction_expr : instructions.operands())
261261
{
262262
statement_list_parse_treet::instructiont instruction;
263-
codet code_token(instruction_expr.op0().id());
263+
codet code_token(to_multi_ary_expr(instruction_expr).op0().id());
264264
for(const exprt &operand : instruction_expr.operands())
265265
{
266266
if(operand.is_not_nil() && operand.id() != code_token.get_statement())

‎src/util/expr.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,7 @@ class exprt:public irept
9898
const operandst &operands() const
9999
{ return (const operandst &)get_sub(); }
100100

101+
protected:
101102
exprt &op0()
102103
{ return operands().front(); }
103104

@@ -122,6 +123,7 @@ class exprt:public irept
122123
const exprt &op3() const
123124
{ return operands()[3]; }
124125

126+
public:
125127
void reserve_operands(operandst::size_type n)
126128
{ operands().reserve(n) ; }
127129

0 commit comments

Comments
 (0)