Skip to content

Commit c6ead88

Browse files
author
Daniel Kroening
committed
simplify_abs now has new interface
This improves memory safety.
1 parent ab071ae commit c6ead88

File tree

2 files changed

+16
-14
lines changed

2 files changed

+16
-14
lines changed

src/util/simplify_expr.cpp

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -63,21 +63,17 @@ struct simplify_expr_cachet
6363
simplify_expr_cachet simplify_expr_cache;
6464
#endif
6565

66-
bool simplify_exprt::simplify_abs(exprt &expr)
66+
simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
6767
{
68-
if(expr.operands().size()!=1)
69-
return true;
70-
71-
if(to_unary_expr(expr).op().is_constant())
68+
if(expr.op().is_constant())
7269
{
7370
const typet &type = to_unary_expr(expr).op().type();
7471

7572
if(type.id()==ID_floatbv)
7673
{
7774
ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
7875
value.set_sign(false);
79-
expr=value.to_expr();
80-
return false;
76+
return value.to_expr();
8177
}
8278
else if(type.id()==ID_signedbv ||
8379
type.id()==ID_unsignedbv)
@@ -87,20 +83,18 @@ bool simplify_exprt::simplify_abs(exprt &expr)
8783
{
8884
if(*value >= 0)
8985
{
90-
expr = to_unary_expr(expr).op();
91-
return false;
86+
return to_unary_expr(expr).op();
9287
}
9388
else
9489
{
9590
value->negate();
96-
expr = from_integer(*value, type);
97-
return false;
91+
return from_integer(*value, type);
9892
}
9993
}
10094
}
10195
}
10296

103-
return true;
97+
return unchanged(expr);
10498
}
10599

106100
bool simplify_exprt::simplify_sign(exprt &expr)
@@ -2528,7 +2522,14 @@ bool simplify_exprt::simplify_node(exprt &expr)
25282522
else if(expr.id()==ID_isnormal)
25292523
no_change = simplify_isnormal(expr) && no_change;
25302524
else if(expr.id()==ID_abs)
2531-
no_change = simplify_abs(expr) && no_change;
2525+
{
2526+
auto r = simplify_abs(to_abs_expr(expr));
2527+
if(r.has_changed())
2528+
{
2529+
no_change = false;
2530+
expr = r.expr;
2531+
}
2532+
}
25322533
else if(expr.id()==ID_sign)
25332534
no_change = simplify_sign(expr) && no_change;
25342535
else if(expr.id() == ID_popcount)

src/util/simplify_expr_class.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include "replace_expr.h"
2626
#endif
2727

28+
class abs_exprt;
2829
class array_exprt;
2930
class bswap_exprt;
3031
class byte_extract_exprt;
@@ -159,7 +160,7 @@ class simplify_exprt
159160
bool simplify_isinf(exprt &expr);
160161
bool simplify_isnan(exprt &expr);
161162
bool simplify_isnormal(exprt &expr);
162-
bool simplify_abs(exprt &expr);
163+
resultt<> simplify_abs(const abs_exprt &);
163164
bool simplify_sign(exprt &expr);
164165
bool simplify_popcount(popcount_exprt &expr);
165166
bool simplify_complex(exprt &expr);

0 commit comments

Comments
 (0)