Skip to content

Commit aadd948

Browse files
author
Daniel Kroening
committed
simplifier: type remaining methods for unary expressions
This improves memory safety.
1 parent 90867d3 commit aadd948

File tree

4 files changed

+33
-44
lines changed

4 files changed

+33
-44
lines changed

‎src/util/simplify_expr.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2026,7 +2026,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
20262026
return unchanged(expr);
20272027
}
20282028

2029-
simplify_exprt::resultt<> simplify_exprt::simplify_complex(const exprt &expr)
2029+
simplify_exprt::resultt<>
2030+
simplify_exprt::simplify_complex(const unary_exprt &expr)
20302031
{
20312032
if(expr.id() == ID_complex_real)
20322033
{
@@ -2140,7 +2141,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
21402141
}
21412142
else if(expr.id()==ID_pointer_object)
21422143
{
2143-
r = simplify_pointer_object(expr);
2144+
r = simplify_pointer_object(to_unary_expr(expr));
21442145
}
21452146
else if(expr.id() == ID_is_dynamic_object)
21462147
{
@@ -2152,11 +2153,11 @@ bool simplify_exprt::simplify_node(exprt &expr)
21522153
}
21532154
else if(expr.id()==ID_object_size)
21542155
{
2155-
r = simplify_object_size(expr);
2156+
r = simplify_object_size(to_unary_expr(expr));
21562157
}
21572158
else if(expr.id()==ID_good_pointer)
21582159
{
2159-
r = simplify_good_pointer(expr);
2160+
r = simplify_good_pointer(to_unary_expr(expr));
21602161
}
21612162
else if(expr.id()==ID_div)
21622163
{
@@ -2213,7 +2214,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
22132214
}
22142215
else if(expr.id()==ID_unary_plus)
22152216
{
2216-
r = simplify_unary_plus(expr);
2217+
r = simplify_unary_plus(to_unary_expr(expr));
22172218
}
22182219
else if(expr.id()==ID_not)
22192220
{
@@ -2235,7 +2236,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
22352236
}
22362237
else if(expr.id()==ID_pointer_offset)
22372238
{
2238-
r = simplify_pointer_offset(expr);
2239+
r = simplify_pointer_offset(to_unary_expr(expr));
22392240
}
22402241
else if(expr.id()==ID_extractbit)
22412242
{
@@ -2288,7 +2289,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
22882289
}
22892290
else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
22902291
{
2291-
r = simplify_complex(expr);
2292+
r = simplify_complex(to_unary_expr(expr));
22922293
}
22932294

22942295
if(r.has_changed())

‎src/util/simplify_expr_class.h

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -162,27 +162,27 @@ class simplify_exprt
162162
NODISCARD resultt<> simplify_member(const member_exprt &);
163163
NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
164164
NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
165-
NODISCARD resultt<> simplify_pointer_object(const exprt &);
166-
NODISCARD resultt<> simplify_object_size(const exprt &);
167-
NODISCARD resultt<> simplify_dynamic_size(const exprt &);
165+
NODISCARD resultt<> simplify_pointer_object(const unary_exprt &);
166+
NODISCARD resultt<> simplify_object_size(const unary_exprt &);
167+
NODISCARD resultt<> simplify_dynamic_size(const unary_exprt &);
168168
NODISCARD resultt<> simplify_is_dynamic_object(const exprt &expr);
169169
NODISCARD resultt<> simplify_is_invalid_pointer(const exprt &expr);
170-
NODISCARD resultt<> simplify_same_object(const exprt &);
171-
NODISCARD resultt<> simplify_good_pointer(const exprt &);
170+
NODISCARD resultt<> simplify_same_object(const unary_exprt &);
171+
NODISCARD resultt<> simplify_good_pointer(const unary_exprt &);
172172
NODISCARD resultt<> simplify_object(const exprt &);
173173
NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
174-
NODISCARD resultt<> simplify_unary_plus(const exprt &);
174+
NODISCARD resultt<> simplify_unary_plus(const unary_exprt &);
175175
NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
176176
NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
177-
NODISCARD resultt<> simplify_pointer_offset(const exprt &);
177+
NODISCARD resultt<> simplify_pointer_offset(const unary_exprt &);
178178
NODISCARD resultt<> simplify_bswap(const bswap_exprt &);
179179
NODISCARD resultt<> simplify_isinf(const unary_exprt &);
180180
NODISCARD resultt<> simplify_isnan(const unary_exprt &);
181181
NODISCARD resultt<> simplify_isnormal(const unary_exprt &);
182182
NODISCARD resultt<> simplify_abs(const abs_exprt &);
183183
NODISCARD resultt<> simplify_sign(const sign_exprt &);
184184
NODISCARD resultt<> simplify_popcount(const popcount_exprt &);
185-
NODISCARD resultt<> simplify_complex(const exprt &);
185+
NODISCARD resultt<> simplify_complex(const unary_exprt &);
186186

187187
/// Attempt to simplify mathematical function applications if we have
188188
/// enough information to do so. Currently focused on constant comparisons.

‎src/util/simplify_expr_int.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1110,13 +1110,11 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
11101110
return unchanged(expr);
11111111
}
11121112

1113-
simplify_exprt::resultt<> simplify_exprt::simplify_unary_plus(const exprt &expr)
1113+
simplify_exprt::resultt<>
1114+
simplify_exprt::simplify_unary_plus(const unary_exprt &expr)
11141115
{
1115-
if(expr.operands().size()!=1)
1116-
return unchanged(expr);
1117-
11181116
// simply remove, this is always 'nop'
1119-
return expr.op0();
1117+
return expr.op();
11201118
}
11211119

11221120
simplify_exprt::resultt<>

‎src/util/simplify_expr_pointer.cpp

Lines changed: 14 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -244,18 +244,17 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr)
244244
}
245245

246246
simplify_exprt::resultt<>
247-
simplify_exprt::simplify_pointer_offset(const exprt &expr)
247+
simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
248248
{
249-
if(expr.operands().size()!=1)
250-
return unchanged(expr);
251-
252-
const exprt &ptr = expr.op0();
249+
const exprt &ptr = expr.op();
253250

254251
if(ptr.id()==ID_if && ptr.operands().size()==3)
255252
{
256253
if_exprt if_expr=lift_if(expr, 0);
257-
if_expr.true_case() = simplify_pointer_offset(if_expr.true_case());
258-
if_expr.false_case() = simplify_pointer_offset(if_expr.false_case());
254+
if_expr.true_case() =
255+
simplify_pointer_offset(to_unary_expr(if_expr.true_case()));
256+
if_expr.false_case() =
257+
simplify_pointer_offset(to_unary_expr(if_expr.false_case()));
259258
return changed(simplify_if(if_expr));
260259
}
261260

@@ -284,7 +283,7 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr)
284283
// Cast from pointer to pointer.
285284
// This just passes through, remove typecast.
286285
auto new_expr = expr;
287-
new_expr.op0() = ptr.op0();
286+
new_expr.op() = ptr.op0();
288287

289288
simplify_node(new_expr); // recursive call
290289
return new_expr;
@@ -537,12 +536,9 @@ simplify_exprt::simplify_inequality_pointer_object(const exprt &expr)
537536
}
538537

539538
simplify_exprt::resultt<>
540-
simplify_exprt::simplify_pointer_object(const exprt &expr)
539+
simplify_exprt::simplify_pointer_object(const unary_exprt &expr)
541540
{
542-
if(expr.operands().size()!=1)
543-
return unchanged(expr);
544-
545-
const exprt &op = expr.op0();
541+
const exprt &op = expr.op();
546542

547543
auto op_result = simplify_object(op);
548544

@@ -564,7 +560,7 @@ simplify_exprt::simplify_pointer_object(const exprt &expr)
564560
if(op_result.has_changed())
565561
{
566562
auto new_expr = expr;
567-
new_expr.op0() = op_result;
563+
new_expr.op() = op_result;
568564
return std::move(new_expr);
569565
}
570566
else
@@ -714,14 +710,11 @@ tvt simplify_exprt::objects_equal_address_of(const exprt &a, const exprt &b)
714710
}
715711

716712
simplify_exprt::resultt<>
717-
simplify_exprt::simplify_object_size(const exprt &expr)
713+
simplify_exprt::simplify_object_size(const unary_exprt &expr)
718714
{
719-
if(expr.operands().size()!=1)
720-
return unchanged(expr);
721-
722715
auto new_expr = expr;
723716
bool no_change = true;
724-
exprt &op = new_expr.op0();
717+
exprt &op = new_expr.op();
725718
auto op_result = simplify_object(op);
726719

727720
if(op_result.has_changed())
@@ -766,13 +759,10 @@ simplify_exprt::simplify_object_size(const exprt &expr)
766759
}
767760

768761
simplify_exprt::resultt<>
769-
simplify_exprt::simplify_good_pointer(const exprt &expr)
762+
simplify_exprt::simplify_good_pointer(const unary_exprt &expr)
770763
{
771-
if(expr.operands().size()!=1)
772-
return unchanged(expr);
773-
774764
// we expand the definition
775-
exprt def=good_pointer_def(expr.op0(), ns);
765+
exprt def = good_pointer_def(expr.op(), ns);
776766

777767
// recursive call
778768
simplify_node(def);

0 commit comments

Comments
 (0)