1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
/*******************************************************************\
Module: Unit tests for variable/sensitivity/abstract_object::merge
Author: DiffBlue Limited
\*******************************************************************/
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/interval.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true))
#define V_(X) (bvrep2integer(X.c_str(), 32, true))
#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32)))
SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]")
{
GIVEN("Two single element internvals")
{
constant_interval_exprt a = constant_interval_exprt::singleton(CEV(5));
constant_interval_exprt b = constant_interval_exprt::singleton(CEV(10));
constant_interval_exprt zero = constant_interval_exprt::singleton(CEV(0));
const auto a_mod_b = a.modulo(b);
REQUIRE(V(a_mod_b.get_upper()) == 5);
const auto b_mod_a = b.modulo(a);
// TODO: precision with single element modulo
REQUIRE(V(b_mod_a.get_upper()) == 4);
const auto zero_mod_a = zero.modulo(a);
REQUIRE(zero_mod_a == constant_interval_exprt::singleton(CEV(0)));
// TODO: this causes an invariant as it is unable to simplify the
// TODO: simplify(a % 0) == a % 0
// REQUIRE(a.modulo(zero).is_top());
}
GIVEN("Two simple signed intervals")
{
symbol_tablet symbol_table;
namespacet ns(symbol_table);
WHEN("Positive RHS")
{
THEN("Ensure result is consistent.")
{
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(10), CEV(20)),
constant_interval_exprt(CEV(5), CEV(5))) ==
constant_interval_exprt(CEV(0), CEV(4)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(10), CEV(20)),
constant_interval_exprt(CEV(4), CEV(5))) ==
constant_interval_exprt(CEV(0), CEV(4)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(10), CEV(20)),
constant_interval_exprt(CEV(0), CEV(5))) ==
constant_interval_exprt::top(signedbv_typet(32)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(10), CEV(20)),
constant_interval_exprt(CEV(-5), CEV(5))) ==
constant_interval_exprt::top(signedbv_typet(32)));
INFO("Taking modulo on interval that contains zero results in top");
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(-10), CEV(20)),
constant_interval_exprt(CEV(0), CEV(5))) ==
constant_interval_exprt::top(signedbv_typet(32)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(-10), CEV(20)),
constant_interval_exprt(CEV(1), CEV(5))) ==
constant_interval_exprt(CEV(-10), CEV(20)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(-10), CEV(-1)),
constant_interval_exprt(CEV(-5), CEV(-1))) ==
constant_interval_exprt(CEV(-5), CEV(0)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(-20), CEV(-10)),
constant_interval_exprt(CEV(0), CEV(5))) ==
constant_interval_exprt::top(signedbv_typet(32)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(-20), CEV(-10)),
constant_interval_exprt(CEV(1), CEV(1))) ==
constant_interval_exprt::singleton(CEV(0)));
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(CEV(30), CEV(50)),
constant_interval_exprt(CEV(2), CEV(2))) ==
constant_interval_exprt(CEV(0), CEV(1)));
// Problems
REQUIRE(
constant_interval_exprt::modulo(
constant_interval_exprt(
CEV(30), max_value_exprt(signedbv_typet(32))),
constant_interval_exprt(CEV(2), CEV(2))) ==
constant_interval_exprt(CEV(0), CEV(1)));
}
}
}
}
|
