Skip to content

Commit 4bf03bb

Browse files
committed
Cleanup get_values (renaming it to collect_constants) and test it
We can substantially simplify the logic here as there is no need to compare all values when working with sorted containers.
1 parent 3f2a6bb commit 4bf03bb

File tree

3 files changed

+68
-45
lines changed

3 files changed

+68
-45
lines changed
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
3+
#ifdef _MSC_VER
4+
# define _Static_assert(x, m) static_assert(x, m)
5+
#endif
6+
7+
int main()
8+
{
9+
_Bool b1, b2;
10+
11+
int nc = (b1 ? 1 : 2) == (b2 ? 1 : 2);
12+
assert(b1 != b2 || nc != 0);
13+
14+
// The following are true for all values of b1, b2, and the simplifier should
15+
// be able to figure this out.
16+
_Static_assert((b1 ? 1 : 1) == (b2 ? 1 : 1), "");
17+
_Static_assert(((b1 ? 2 : 3) >= (b2 ? 1 : 2)) != 0, "");
18+
_Static_assert(((b1 ? 0 : 1) >= (b2 ? 2 : 3)) == 0, "");
19+
_Static_assert(((b1 ? 0 : 1) >= 2) == 0, "");
20+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/util/simplify_expr_int.cpp

Lines changed: 40 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -1460,25 +1460,31 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
14601460
return true;
14611461
}
14621462

1463-
typedef std::set<mp_integer> value_listt;
1464-
static bool get_values(const exprt &expr, value_listt &value_list)
1463+
/// Collect integer-typed constants in \p values when \p expr either itself is a
1464+
/// constant or an if-expression; for an if-expression recursively collect those
1465+
/// values in the true- and false case, respectively.
1466+
/// \param expr: expression to collect constants from
1467+
/// \param [out] values: set of integer constants
1468+
/// \return false, iff all sub-expressions were either integer constants or if
1469+
/// expressions with true/false cases being constants or if expressions.
1470+
static bool collect_constants(const exprt &expr, std::set<mp_integer> &values)
14651471
{
14661472
if(expr.is_constant())
14671473
{
1468-
mp_integer int_value;
1469-
if(to_integer(to_constant_expr(expr), int_value))
1474+
const auto int_value_opt = numeric_cast<mp_integer>(to_constant_expr(expr));
1475+
if(!int_value_opt.has_value())
14701476
return true;
14711477

1472-
value_list.insert(int_value);
1478+
values.insert(*int_value_opt);
14731479

14741480
return false;
14751481
}
14761482
else if(expr.id() == ID_if)
14771483
{
14781484
const auto &if_expr = to_if_expr(expr);
14791485

1480-
return get_values(if_expr.true_case(), value_list) ||
1481-
get_values(if_expr.false_case(), value_list);
1486+
return collect_constants(if_expr.true_case(), values) ||
1487+
collect_constants(if_expr.false_case(), values);
14821488
}
14831489

14841490
return true;
@@ -1539,51 +1545,40 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
15391545

15401546
// try constants
15411547

1542-
value_listt values0, values1;
1548+
std::set<mp_integer> values0, values1;
1549+
bool ok = !collect_constants(expr.op0(), values0);
1550+
if(ok)
1551+
ok = !collect_constants(expr.op1(), values1);
15431552

1544-
bool ok0=!get_values(expr.op0(), values0);
1545-
bool ok1=!get_values(expr.op1(), values1);
1546-
1547-
if(ok0 && ok1)
1553+
if(ok)
15481554
{
1549-
bool first=true;
1550-
bool result=false; // dummy initialization to prevent warning
1551-
bool ok=true;
1552-
1553-
// compare possible values
1554-
1555-
for(const mp_integer &int_value0 : values0)
1555+
// We can simplify equality if both sides have exactly one constant value.
1556+
// This rule most likely never kicks in as we will already have simplified
1557+
// this case elsewhere (equalities with at least one side being constant are
1558+
// handled by other functions, and if expressions with multiple branches
1559+
// having the same value are simplified to remove the if expression).
1560+
if(expr.id() == ID_equal)
15561561
{
1557-
for(const mp_integer &int_value1 : values1)
1562+
if(values0.size() == 1 && values1.size() == 1)
15581563
{
1559-
bool tmp;
1560-
1561-
if(expr.id()==ID_ge)
1562-
tmp=(int_value0>=int_value1);
1563-
else if(expr.id()==ID_equal)
1564-
tmp=(int_value0==int_value1);
1565-
else
1566-
{
1567-
tmp=false;
1568-
UNREACHABLE;
1569-
}
1570-
1571-
if(first)
1572-
{
1573-
result=tmp;
1574-
first=false;
1575-
}
1576-
else if(result!=tmp)
1577-
{
1578-
ok=false;
1579-
break;
1580-
}
1564+
return make_boolean_expr(*values0.begin() == *values1.begin());
15811565
}
15821566
}
1583-
1584-
if(ok)
1567+
else
15851568
{
1586-
return make_boolean_expr(result);
1569+
// ID_ge, as ensured by the above INVARIANT: the smallest value in values0
1570+
// must be >= the largest value in values1
1571+
if(*values0.begin() >= *values1.rbegin())
1572+
{
1573+
return make_boolean_expr(true);
1574+
}
1575+
// If all entries in values0 are smaller than the smallest entry in
1576+
// values1 then the result must be false.
1577+
else if(*values0.rbegin() < *values1.begin())
1578+
{
1579+
return make_boolean_expr(false);
1580+
}
1581+
// Else we don't know for sure.
15871582
}
15881583
}
15891584

0 commit comments

Comments
 (0)