Skip to content

Commit 3ce2140

Browse files
tautschnigtautschnig
authored
Merge pull request #7925 from tautschnig/cleanup/interval-exprt
Interval expressions: cleanup type hierarchy
2 parents 45fa2ca + b1267b5 commit 3ce2140

File tree

11 files changed

+99
-81
lines changed

11 files changed

+99
-81
lines changed

‎src/util/interval.cpp‎

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -165,10 +165,11 @@ constant_interval_exprt::modulo(const constant_interval_exprt &o) const
165165

166166
// If the RHS is 1, or -1 (signed only), then return zero.
167167
if(
168-
o == constant_interval_exprt(from_integer(1, o.type())) ||
169-
(o.is_signed() && o == constant_interval_exprt(from_integer(-1, o.type()))))
168+
o.is_single_value_interval() &&
169+
(o.get_lower() == from_integer(1, o.type()) ||
170+
(o.is_signed() && o.get_lower() == from_integer(-1, o.type()))))
170171
{
171-
return constant_interval_exprt(zero());
172+
return constant_interval_exprt::singleton(zero());
172173
}
173174

174175
// If other might be modulo by zero, set everything to top.
@@ -179,7 +180,7 @@ constant_interval_exprt::modulo(const constant_interval_exprt &o) const
179180

180181
if(is_zero())
181182
{
182-
return constant_interval_exprt(zero());
183+
return constant_interval_exprt::singleton(zero());
183184
}
184185

185186
exprt lower = min();
@@ -233,12 +234,12 @@ tvt constant_interval_exprt::is_definitely_false() const
233234
}
234235
}
235236

236-
if(equal(constant_interval_exprt(zero())).is_true())
237+
if(is_single_value_interval() && get_lower() == zero())
237238
{
238239
return tvt(true);
239240
}
240241

241-
if(contains(constant_interval_exprt(zero())))
242+
if(contains(constant_interval_exprt::singleton(zero())))
242243
{
243244
INVARIANT(
244245
is_positive(get_upper()) || is_negative(get_lower()),
@@ -457,12 +458,14 @@ tvt constant_interval_exprt::not_equal(const constant_interval_exprt &o) const
457458

458459
constant_interval_exprt constant_interval_exprt::increment() const
459460
{
460-
return plus(constant_interval_exprt(from_integer(mp_integer(1), type())));
461+
return plus(
462+
constant_interval_exprt::singleton(from_integer(mp_integer(1), type())));
461463
}
462464

463465
constant_interval_exprt constant_interval_exprt::decrement() const
464466
{
465-
return minus(constant_interval_exprt(from_integer(mp_integer(1), type())));
467+
return minus(
468+
constant_interval_exprt::singleton(from_integer(mp_integer(1), type())));
466469
}
467470

468471
constant_interval_exprt constant_interval_exprt::get_extremes(
@@ -939,7 +942,7 @@ constant_interval_exprt::handle_constant_unary_expression(
939942
if(is_single_value_interval())
940943
{
941944
auto expr = unary_exprt(op, get_lower());
942-
return constant_interval_exprt(simplified_expr(expr));
945+
return constant_interval_exprt::singleton(simplified_expr(expr));
943946
}
944947
return top();
945948
}
@@ -951,7 +954,7 @@ constant_interval_exprt::handle_constant_binary_expression(
951954
{
952955
PRECONDITION(is_single_value_interval() && other.is_single_value_interval());
953956
auto expr = binary_exprt(get_lower(), op, other.get_lower());
954-
return constant_interval_exprt(simplified_expr(expr));
957+
return constant_interval_exprt::singleton(simplified_expr(expr));
955958
}
956959

957960
exprt constant_interval_exprt::get_max(const exprt &a, const exprt &b)
@@ -1964,11 +1967,11 @@ constant_interval_exprt constant_interval_exprt::tvt_to_interval(const tvt &val)
19641967
{
19651968
if(val.is_true())
19661969
{
1967-
return constant_interval_exprt(true_exprt());
1970+
return constant_interval_exprt::singleton(true_exprt());
19681971
}
19691972
else if(val.is_false())
19701973
{
1971-
return constant_interval_exprt(false_exprt());
1974+
return constant_interval_exprt::singleton(false_exprt());
19721975
}
19731976
else
19741977
{

‎src/util/interval.h‎

Lines changed: 19 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -11,30 +11,30 @@
1111
#include <util/std_expr.h>
1212
#include <util/threeval.h>
1313

14-
#include <iostream>
14+
#include <iosfwd>
1515

1616
/// +∞ upper bound for intervals
17-
class max_exprt : public exprt
17+
class max_exprt : public nullary_exprt
1818
{
1919
public:
20-
explicit max_exprt(const typet &_type) : exprt(ID_max, _type)
20+
explicit max_exprt(const typet &_type) : nullary_exprt(ID_max, _type)
2121
{
2222
}
2323

24-
explicit max_exprt(const exprt &_expr) : exprt(ID_max, _expr.type())
24+
explicit max_exprt(const exprt &_expr) : nullary_exprt(ID_max, _expr.type())
2525
{
2626
}
2727
};
2828

2929
/// -∞ upper bound for intervals
30-
class min_exprt : public exprt
30+
class min_exprt : public nullary_exprt
3131
{
3232
public:
33-
explicit min_exprt(const typet &_type) : exprt(ID_min, _type)
33+
explicit min_exprt(const typet &_type) : nullary_exprt(ID_min, _type)
3434
{
3535
}
3636

37-
explicit min_exprt(const exprt &_expr) : exprt(ID_min, _expr.type())
37+
explicit min_exprt(const exprt &_expr) : nullary_exprt(ID_min, _expr.type())
3838
{
3939
}
4040
};
@@ -47,25 +47,16 @@ class min_exprt : public exprt
4747
class constant_interval_exprt : public binary_exprt
4848
{
4949
public:
50-
constant_interval_exprt(
51-
const exprt &lower,
52-
const exprt &upper,
53-
const typet type)
54-
: binary_exprt(lower, ID_constant_interval, upper, type)
50+
constant_interval_exprt(exprt lower, exprt upper, typet type)
51+
: binary_exprt(
52+
std::move(lower),
53+
ID_constant_interval,
54+
std::move(upper),
55+
std::move(type))
5556
{
5657
PRECONDITION(is_well_formed());
5758
}
5859

59-
constant_interval_exprt(const constant_interval_exprt &x)
60-
: constant_interval_exprt(x.get_lower(), x.get_upper(), x.type())
61-
{
62-
}
63-
64-
explicit constant_interval_exprt(const exprt &x)
65-
: constant_interval_exprt(x, x, x.type())
66-
{
67-
}
68-
6960
explicit constant_interval_exprt(const typet &type)
7061
: constant_interval_exprt(min_exprt(type), max_exprt(type), type)
7162
{
@@ -74,6 +65,7 @@ class constant_interval_exprt : public binary_exprt
7465
constant_interval_exprt(const exprt &lower, const exprt &upper)
7566
: constant_interval_exprt(lower, upper, lower.type())
7667
{
68+
PRECONDITION(is_well_formed());
7769
}
7870

7971
bool is_well_formed() const
@@ -97,6 +89,11 @@ class constant_interval_exprt : public binary_exprt
9789
return b;
9890
}
9991

92+
static constant_interval_exprt singleton(const exprt &x)
93+
{
94+
return constant_interval_exprt{x, x, x.type()};
95+
}
96+
10097
static bool is_valid_bound(const exprt &expr)
10198
{
10299
const irep_idt &id = expr.id();

‎unit/util/interval/bitwise.cpp‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,9 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
1515
{
1616
const unsignedbv_typet &unsigned_int = unsignedbv_typet(32);
1717
constant_interval_exprt five =
18-
constant_interval_exprt(from_integer(5, unsigned_int));
18+
constant_interval_exprt::singleton(from_integer(5, unsigned_int));
1919
constant_interval_exprt nine =
20-
constant_interval_exprt(from_integer(9, unsigned_int));
20+
constant_interval_exprt::singleton(from_integer(9, unsigned_int));
2121

2222
constant_interval_exprt five_to_nine(
2323
from_integer(5, unsigned_int), from_integer(9, unsigned_int));
@@ -26,7 +26,7 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
2626
{
2727
REQUIRE(
2828
constant_interval_exprt::bitwise_or(five, nine) ==
29-
constant_interval_exprt(from_integer(13, unsigned_int)));
29+
constant_interval_exprt::singleton(from_integer(13, unsigned_int)));
3030

3131
REQUIRE(constant_interval_exprt::bitwise_or(five_to_nine, nine).is_top());
3232
}
@@ -35,10 +35,10 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
3535
{
3636
REQUIRE(
3737
constant_interval_exprt::bitwise_and(five, nine) ==
38-
constant_interval_exprt(from_integer(1, unsigned_int)));
38+
constant_interval_exprt::singleton(from_integer(1, unsigned_int)));
3939
REQUIRE(
4040
(five & nine) ==
41-
constant_interval_exprt(from_integer(1, unsigned_int)));
41+
constant_interval_exprt::singleton(from_integer(1, unsigned_int)));
4242

4343
REQUIRE(
4444
constant_interval_exprt::bitwise_and(five_to_nine, nine).is_top());
@@ -48,7 +48,7 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
4848
{
4949
REQUIRE(
5050
constant_interval_exprt::bitwise_xor(five, nine) ==
51-
constant_interval_exprt(from_integer(12, unsigned_int)));
51+
constant_interval_exprt::singleton(from_integer(12, unsigned_int)));
5252

5353
REQUIRE(
5454
constant_interval_exprt::bitwise_xor(five_to_nine, nine).is_top());

‎unit/util/interval/comparisons.cpp‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,8 @@ SCENARIO("comparison interval domain", "[core][analyses][interval][comparison]")
121121
constant_interval_exprt(CEV(10), CEV(20)) >
122122
constant_interval_exprt(CEV(30), CEV(40)));
123123
REQUIRE(
124-
constant_interval_exprt(CEV(10)) < constant_interval_exprt(CEV(30)));
124+
constant_interval_exprt::singleton(CEV(10)) <
125+
constant_interval_exprt::singleton(CEV(30)));
125126
}
126127

127128
THEN(
@@ -186,8 +187,8 @@ SCENARIO("comparison interval domain", "[core][analyses][interval][comparison]")
186187
constant_interval_exprt(CEV(10), CEV(31))
187188
.less_than_or_equal(constant_interval_exprt(CEV(30), CEV(40))) ==
188189
tvt::unknown());
189-
CHECK(constant_interval_exprt(CEV(10))
190-
.less_than_or_equal(constant_interval_exprt(CEV(30)))
190+
CHECK(constant_interval_exprt::singleton(CEV(10))
191+
.less_than_or_equal(constant_interval_exprt::singleton(CEV(30)))
191192
.is_true());
192193
}
193194

@@ -222,7 +223,8 @@ SCENARIO("comparison interval domain", "[core][analyses][interval][comparison]")
222223
REQUIRE(includes_zero_negative.is_definitely_true().is_unknown());
223224
REQUIRE(includes_zero_negative.is_definitely_false().is_unknown());
224225

225-
constant_interval_exprt zero(CEV(0));
226+
constant_interval_exprt zero =
227+
constant_interval_exprt::singleton(CEV(0));
226228
REQUIRE(zero.is_definitely_false().is_true());
227229
REQUIRE(zero.is_definitely_true().is_false());
228230

@@ -242,8 +244,8 @@ TEST_CASE("interval::equality", "[core][analyses][interval]")
242244
{
243245
SECTION("Single element intervals")
244246
{
245-
constant_interval_exprt two(CEV(2));
246-
constant_interval_exprt four(CEV(4));
247+
constant_interval_exprt two = constant_interval_exprt::singleton(CEV(2));
248+
constant_interval_exprt four = constant_interval_exprt::singleton(CEV(4));
247249

248250
REQUIRE_FALSE(two.equal(four).is_true());
249251
REQUIRE(two.equal(two).is_true());

‎unit/util/interval/divide.cpp‎

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -38,11 +38,16 @@ TEST_CASE("interval::divide", "[core][util][interval][divide]")
3838

3939
SECTION("Single element intervals")
4040
{
41-
const constant_interval_exprt zero_interval(zero);
42-
const constant_interval_exprt one_interval(one);
43-
const constant_interval_exprt four_interval(four);
44-
const constant_interval_exprt eight_interval(eight);
45-
const constant_interval_exprt negative_twelve_interval(negative_twelve);
41+
const constant_interval_exprt zero_interval =
42+
constant_interval_exprt::singleton(zero);
43+
const constant_interval_exprt one_interval =
44+
constant_interval_exprt::singleton(one);
45+
const constant_interval_exprt four_interval =
46+
constant_interval_exprt::singleton(four);
47+
const constant_interval_exprt eight_interval =
48+
constant_interval_exprt::singleton(eight);
49+
const constant_interval_exprt negative_twelve_interval =
50+
constant_interval_exprt::singleton(negative_twelve);
4651

4752
REQUIRE(value_of(zero_interval.divide(four_interval)) == 0);
4853
REQUIRE(value_of(four_interval.divide(four_interval)) == 1);
@@ -61,8 +66,10 @@ TEST_CASE("interval::divide", "[core][util][interval][divide]")
6166

6267
SECTION("Max & Min")
6368
{
64-
const constant_interval_exprt min_interval{min_exprt{signed_int_type}};
65-
const constant_interval_exprt max_interval{max_exprt{signed_int_type}};
69+
const constant_interval_exprt min_interval =
70+
constant_interval_exprt::singleton(min_exprt{signed_int_type});
71+
const constant_interval_exprt max_interval =
72+
constant_interval_exprt::singleton(max_exprt{signed_int_type});
6673
// TODO: division of single max or min don't work as expected
6774
// CHECK(max_interval.divide(max_interval).is_top());
6875
// CHECK(max_interval.divide(min_interval).is_top());
@@ -82,7 +89,8 @@ TEST_CASE("interval::divide", "[core][util][interval][divide]")
8289
const constant_interval_exprt negative_range(
8390
negative_sixteen, negative_twelve);
8491
const constant_interval_exprt range_containing_zero(negative_twelve, four);
85-
const constant_interval_exprt zero_interval(zero);
92+
const constant_interval_exprt zero_interval =
93+
constant_interval_exprt::singleton(zero);
8694

8795
const constant_exprt &two = from_integer(2, signed_int_type);
8896
REQUIRE(matching_range(

‎unit/util/interval/eval.cpp‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]")
1414
WHEN("Negating a boolean interval")
1515
{
1616
constant_interval_exprt true_interval =
17-
constant_interval_exprt(true_exprt());
17+
constant_interval_exprt::singleton(true_exprt());
1818
constant_interval_exprt false_interval =
19-
constant_interval_exprt(false_exprt());
19+
constant_interval_exprt::singleton(false_exprt());
2020
constant_interval_exprt bool_top_interval =
2121
constant_interval_exprt(bool_typet());
2222

@@ -37,11 +37,11 @@ SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]")
3737
WHEN("Unary operations to an single element interval")
3838
{
3939
constant_interval_exprt five =
40-
constant_interval_exprt(from_integer(5, signedbv_typet(32)));
40+
constant_interval_exprt::singleton(from_integer(5, signedbv_typet(32)));
4141
const constant_interval_exprt &max_interval =
42-
constant_interval_exprt(max_exprt{signedbv_typet(32)});
42+
constant_interval_exprt::singleton(max_exprt{signedbv_typet(32)});
4343
const constant_interval_exprt &min_interval =
44-
constant_interval_exprt(min_exprt{signedbv_typet(32)});
44+
constant_interval_exprt::singleton(min_exprt{signedbv_typet(32)});
4545

4646
THEN("When we apply unary addition to it, nothing should happen")
4747
{
@@ -102,7 +102,8 @@ SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]")
102102
TEST_CASE("binary eval switch", "[core][analyses][interval]")
103103
{
104104
const auto interval_of = [](const int value) {
105-
return constant_interval_exprt(from_integer(value, signedbv_typet(32)));
105+
return constant_interval_exprt::singleton(
106+
from_integer(value, signedbv_typet(32)));
106107
};
107108

108109
const auto interval_from_to = [](const int lower, const int upper) {

‎unit/util/interval/modulo.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]")
1919
{
2020
GIVEN("Two single element internvals")
2121
{
22-
constant_interval_exprt a(CEV(5));
23-
constant_interval_exprt b(CEV(10));
24-
constant_interval_exprt zero(CEV(0));
22+
constant_interval_exprt a = constant_interval_exprt::singleton(CEV(5));
23+
constant_interval_exprt b = constant_interval_exprt::singleton(CEV(10));
24+
constant_interval_exprt zero = constant_interval_exprt::singleton(CEV(0));
2525
const auto a_mod_b = a.modulo(b);
2626
REQUIRE(V(a_mod_b.get_upper()) == 5);
2727

@@ -30,7 +30,7 @@ SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]")
3030
REQUIRE(V(b_mod_a.get_upper()) == 4);
3131

3232
const auto zero_mod_a = zero.modulo(a);
33-
REQUIRE(zero_mod_a == constant_interval_exprt(CEV(0)));
33+
REQUIRE(zero_mod_a == constant_interval_exprt::singleton(CEV(0)));
3434

3535
// TODO: this causes an invariant as it is unable to simplify the
3636
// TODO: simplify(a % 0) == a % 0
@@ -95,7 +95,7 @@ SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]")
9595
constant_interval_exprt::modulo(
9696
constant_interval_exprt(CEV(-20), CEV(-10)),
9797
constant_interval_exprt(CEV(1), CEV(1))) ==
98-
constant_interval_exprt(CEV(0)));
98+
constant_interval_exprt::singleton(CEV(0)));
9999

100100
REQUIRE(
101101
constant_interval_exprt::modulo(

‎unit/util/interval/multiply.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@ SCENARIO("multiply interval domain", "[core][analyses][interval][multiply]")
2424

2525
WHEN("Single element multiplication")
2626
{
27-
constant_interval_exprt a(CEV(5));
28-
constant_interval_exprt b(CEV(10));
27+
constant_interval_exprt a = constant_interval_exprt::singleton(CEV(5));
28+
constant_interval_exprt b = constant_interval_exprt::singleton(CEV(10));
2929
const auto a_times_b = a.multiply(b);
3030
REQUIRE(a_times_b == constant_interval_exprt(CEV(50), CEV(50)));
3131
}

0 commit comments

Comments
 (0)