CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
interval.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: intervals
4
5 Author: Daniel Neville (2017)
6
7\*******************************************************************/
8#ifndef CPROVER_UTIL_INTERVAL_H
9#define CPROVER_UTIL_INTERVAL_H
10
11#include <util/std_expr.h>
12#include <util/threeval.h>
13
14#include <iosfwd>
15
18{
19public:
20 explicit max_value_exprt(const typet &_type)
22 {
23 }
24
25 explicit max_value_exprt(const exprt &_expr)
27 {
28 }
29};
30
33{
34public:
35 explicit min_value_exprt(const typet &_type)
37 {
38 }
39
40 explicit min_value_exprt(const exprt &_expr)
42 {
43 }
44};
45
52{
53public:
56 std::move(lower),
58 std::move(upper),
59 std::move(type))
60 {
62 }
63
71
72 constant_interval_exprt(const exprt &lower, const exprt &upper)
73 : constant_interval_exprt(lower, upper, lower.type())
74 {
76 }
77
78 bool is_well_formed() const
79 {
80 bool b = true;
81
82 const typet &type = this->type();
83 const exprt &lower = get_lower();
84 const exprt &upper = get_upper();
85
86 b &= is_numeric() || is_boolean() || type.is_nil();
87
88 b &= type == lower.type();
89 b &= type == upper.type();
90
91 b &= is_valid_bound(lower);
92 b &= is_valid_bound(upper);
93
94 b &= !is_numeric() || is_bottom() || less_than_or_equal(lower, upper);
95
96 return b;
97 }
98
100 {
101 return constant_interval_exprt{x, x, x.type()};
102 }
103
104 static bool is_valid_bound(const exprt &expr)
105 {
106 const irep_idt &id = expr.id();
107
108 bool b = true;
109
110 b &= expr.is_constant() || id == ID_min_value || id == ID_max_value;
111
112 if(expr.is_boolean() && id == ID_constant)
113 {
114 b &= expr == true_exprt() || expr == false_exprt();
115 }
116
117 return b;
118 }
119
121
122 /* Naming scheme
123 * is_[X]? Returns bool / tvt
124 * get_[X]? Returns relevant object
125 * [X] Generator of some object.
126 * generate_[X] generator used for evaluation
127 */
128
129 /* Getters */
130 const exprt &get_lower() const;
131 const exprt &get_upper() const;
132
137 const constant_interval_exprt &other,
138 const irep_idt &) const;
139
143
144 /* Unary arithmetic */
147
149
150 /* Logical */
151 tvt is_definitely_true() const;
152 tvt is_definitely_false() const;
153
155 tvt logical_or(const constant_interval_exprt &o) const;
157 tvt logical_not() const;
158
159 /* Binary */
165
166 /* Binary shifts */
169
170 /* Unary bitwise */
172
173 /* Binary bitwise */
177
178 tvt less_than(const constant_interval_exprt &o) const;
182 tvt equal(const constant_interval_exprt &o) const;
183 tvt not_equal(const constant_interval_exprt &o) const;
184
187
188 bool is_empty() const;
189 bool is_single_value_interval() const;
192 // tvt contains(constant_interval_exprt &o) const;
193
194 /* SET OF EXPR COMPARATORS */
195 static bool equal(const exprt &a, const exprt &b);
196 static bool not_equal(const exprt &a, const exprt &b);
197 static bool less_than(const exprt &a, const exprt &b);
198 static bool less_than_or_equal(const exprt &a, const exprt &b);
199 static bool greater_than(const exprt &a, const exprt &b);
200 static bool greater_than_or_equal(const exprt &a, const exprt &b);
201 /* END SET OF EXPR COMPS */
202
203 /* INTERVAL COMPARISONS, returns tvt.is_true(). False cannot be trusted
204 * (could be false or unknown, either use less_than, etc method or use the correct
205 * operator)! */
206 friend bool operator<(
209 friend bool operator>(
212 friend bool operator<=(
215 friend bool operator>=(
218 friend bool operator==(
221 friend bool operator!=(
224
225 /* Operator override for intervals */
258
259 friend std::ostream &
260 operator<<(std::ostream &out, const constant_interval_exprt &i);
261 std::string to_string() const;
262
263 /* Now static equivalents! */
264 static tvt is_true(const constant_interval_exprt &a);
265 static tvt is_false(const constant_interval_exprt &a);
266
267 static tvt logical_and(
270 static tvt logical_or(
273 static tvt logical_xor(
277
280
281 /* Binary */
292
293 /* Binary shifts */
300
301 /* Unary bitwise */
303
304 /* Binary bitwise */
314
315 static tvt
317 static tvt greater_than(
320 static tvt less_than_or_equal(
326 static tvt
328 static tvt
330
333
334 static bool is_empty(const constant_interval_exprt &a);
336
337 static bool is_top(const constant_interval_exprt &a);
338 static bool is_bottom(const constant_interval_exprt &a);
339
340 static bool is_min(const constant_interval_exprt &a);
341 static bool is_max(const constant_interval_exprt &a);
342 /* End static equivalents */
343
344 bool is_top() const;
345 bool is_bottom() const;
346 static constant_interval_exprt top(const typet &type);
350
351 bool has_no_lower_bound() const;
352 bool has_no_upper_bound() const;
353 static bool is_min(const exprt &expr);
354 static bool is_max(const exprt &expr);
355
356 /* Generate min and max exprt according to current type */
357 min_value_exprt min() const;
358 max_value_exprt max() const;
359
360 constant_exprt zero() const;
361 static constant_exprt zero(const typet &type);
362 static constant_exprt zero(const exprt &expr);
364
365 /* Private? */
369 const irep_idt &operation);
370 static exprt get_extreme(std::vector<exprt> values, bool min = true);
371 static exprt get_max(const exprt &a, const exprt &b);
372 static exprt get_min(const exprt &a, const exprt &b);
373 static exprt get_min(std::vector<exprt> &values);
374 static exprt get_max(std::vector<exprt> &values);
375
376 /* we don't simplify in the constructor otherwise */
378 static exprt simplified_expr(exprt expr);
379
380 /* Helpers */
381 /* Four common params: self, static: type, expr, interval */
382
383 bool is_numeric() const;
384 static bool is_numeric(const typet &type);
385 static bool is_numeric(const exprt &expr);
386 static bool is_numeric(const constant_interval_exprt &interval);
387
388 bool is_int() const;
389 static bool is_int(const typet &type);
390 static bool is_int(const exprt &expr);
391 static bool is_int(const constant_interval_exprt &interval);
392
393 bool is_float() const;
394 static bool is_float(const typet &type);
395 static bool is_float(const exprt &expr);
396 static bool is_float(const constant_interval_exprt &interval);
397
398 bool is_bitvector() const;
399 static bool is_bitvector(const typet &type);
401 static bool is_bitvector(const exprt &expr);
402
403 bool is_signed() const;
404 static bool is_signed(const typet &type);
405 static bool is_signed(const exprt &expr);
406 static bool is_signed(const constant_interval_exprt &interval);
407
408 bool is_unsigned() const;
409 static bool is_unsigned(const typet &type);
410 static bool is_unsigned(const exprt &expr);
411 static bool is_unsigned(const constant_interval_exprt &interval);
412
413 bool contains_zero() const;
414 bool contains(const constant_interval_exprt &interval) const;
415
416 static bool is_extreme(const exprt &expr);
417 static bool is_extreme(const exprt &expr1, const exprt &expr2);
418
419 static bool contains_extreme(const exprt expr);
420 static bool contains_extreme(const exprt expr1, const exprt expr2);
421
422 bool is_positive() const;
423 static bool is_positive(const exprt &expr);
424 static bool is_positive(const constant_interval_exprt &interval);
425
426 bool is_zero() const;
427 static bool is_zero(const exprt &expr);
428 static bool is_zero(const constant_interval_exprt &interval);
429
430 bool is_negative() const;
431 static bool is_negative(const exprt &expr);
432 static bool is_negative(const constant_interval_exprt &interval);
433
434 static exprt abs(const exprt &expr);
435
436private:
437 static void generate_expression(
438 const exprt &lhs,
439 const exprt &rhs,
440 const irep_idt &operation,
441 std::vector<exprt> &collection);
442 static void append_multiply_expression(
443 const exprt &lower,
444 const exprt &upper,
445 std::vector<exprt> &collection);
447 const exprt &expr,
448 std::vector<exprt> &collection);
450 const exprt &min,
451 const exprt &other,
452 std::vector<exprt> &collection);
453 static exprt generate_division_expression(const exprt &lhs, const exprt &rhs);
454 static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs);
456 const exprt &lhs,
457 const exprt &rhs,
458 const irep_idt &operation);
459};
460
461inline const constant_interval_exprt &
463{
465 return static_cast<const constant_interval_exprt &>(expr);
466}
467
468#endif /* SRC_ANALYSES_INTERVAL_H_ */
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
A constant literal expression.
Definition std_expr.h:3117
Represents an interval of values.
Definition interval.h:52
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
Definition interval.cpp:471
constant_interval_exprt(exprt lower, exprt upper, typet type)
Definition interval.h:54
max_value_exprt max() const
friend const constant_interval_exprt operator<<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition interval.cpp:684
constant_interval_exprt bottom() const
constant_interval_exprt minus(const constant_interval_exprt &other) const
Definition interval.cpp:112
tvt greater_than_or_equal(const constant_interval_exprt &o) const
Definition interval.cpp:425
min_value_exprt min() const
friend const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt(const typet &type)
Definition interval.h:64
tvt greater_than(const constant_interval_exprt &o) const
Definition interval.cpp:397
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
Definition interval.cpp:345
constant_interval_exprt decrement() const
Definition interval.cpp:465
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition interval.cpp:403
friend bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
tvt is_definitely_false() const
Definition interval.cpp:223
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
Definition interval.cpp:301
friend const constant_interval_exprt operator%(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
tvt not_equal(const constant_interval_exprt &o) const
Definition interval.cpp:454
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
Definition interval.cpp:899
friend const constant_interval_exprt operator>>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
friend bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool has_no_upper_bound() const
friend bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt typecast(const typet &type) const
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition interval.cpp:124
static constant_interval_exprt tvt_to_interval(const tvt &val)
constant_interval_exprt unary_plus() const
Definition interval.cpp:37
constant_interval_exprt plus(const constant_interval_exprt &o) const
Definition interval.cpp:74
static exprt get_extreme(std::vector< exprt > values, bool min=true)
Definition interval.cpp:497
static void append_multiply_expression(const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
Adds all possible values that may arise from multiplication (more than one, in case of past the type ...
Definition interval.cpp:601
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
Definition interval.cpp:334
bool is_single_value_interval() const
constant_interval_exprt increment() const
Definition interval.cpp:459
bool is_bitvector() const
std::string to_string() const
bool contains(const constant_interval_exprt &interval) const
friend const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
bool is_well_formed() const
Definition interval.h:78
friend bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static bool is_extreme(const exprt &expr)
tvt logical_or(const constant_interval_exprt &o) const
Definition interval.cpp:254
static constant_interval_exprt singleton(const exprt &x)
Definition interval.h:99
static exprt simplified_expr(exprt expr)
Definition interval.cpp:987
bool contains_zero() const
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
Definition interval.cpp:939
friend const constant_interval_exprt operator+(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
friend bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static bool is_valid_bound(const exprt &expr)
Definition interval.h:104
constant_interval_exprt modulo(const constant_interval_exprt &o) const
Definition interval.cpp:152
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:960
bool has_no_lower_bound() const
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:965
static bool is_max(const constant_interval_exprt &a)
constant_interval_exprt(const exprt &lower, const exprt &upper)
Definition interval.h:72
friend const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
Definition interval.cpp:572
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition interval.cpp:793
tvt is_definitely_true() const
Definition interval.cpp:217
static bool is_min(const constant_interval_exprt &a)
friend const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
Definition interval.cpp:739
tvt logical_xor(const constant_interval_exprt &o) const
Definition interval.cpp:273
friend const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
const exprt & get_lower() const
Definition interval.cpp:27
static void append_multiply_expression_min(const exprt &min, const exprt &other, std::vector< exprt > &collection)
Appends interval bounds that could arise from MIN * other.
Definition interval.cpp:664
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
Definition interval.cpp:318
tvt logical_and(const constant_interval_exprt &o) const
Definition interval.cpp:265
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
Definition interval.cpp:639
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
Definition interval.cpp:356
constant_interval_exprt top() const
static bool contains_extreme(const exprt expr)
constant_interval_exprt unary_minus() const
Definition interval.cpp:42
constant_exprt zero() const
tvt less_than(const constant_interval_exprt &o) const
Definition interval.cpp:376
static exprt abs(const exprt &expr)
friend const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
constant_interval_exprt bitwise_not() const
Definition interval.cpp:366
constant_interval_exprt divide(const constant_interval_exprt &o) const
Definition interval.cpp:135
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
Definition interval.cpp:982
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
Definition interval.cpp:951
const exprt & get_upper() const
Definition interval.cpp:32
friend bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
tvt equal(const constant_interval_exprt &o) const
Definition interval.cpp:431
friend const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3199
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
+∞ upper bound for intervals
Definition interval.h:18
max_value_exprt(const typet &_type)
Definition interval.h:20
max_value_exprt(const exprt &_expr)
Definition interval.h:25
-∞ upper bound for intervals
Definition interval.h:33
min_value_exprt(const typet &_type)
Definition interval.h:35
min_value_exprt(const exprt &_expr)
Definition interval.h:40
An expression without operands.
Definition std_expr.h:22
The Boolean constant true.
Definition std_expr.h:3190
Definition threeval.h:20
The type of an expression, extends irept.
Definition type.h:29
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition interval.h:462
static int8_t r
Definition irep_hash.h:60
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.