cprover
Loading...
Searching...
No Matches
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 <iostream>
15
17class max_exprt : public exprt
18{
19public:
20 explicit max_exprt(const typet &_type) : exprt(ID_max, _type)
21 {
22 }
23
24 explicit max_exprt(const exprt &_expr) : exprt(ID_max, _expr.type())
25 {
26 }
27};
28
30class min_exprt : public exprt
31{
32public:
33 explicit min_exprt(const typet &_type) : exprt(ID_min, _type)
34 {
35 }
36
37 explicit min_exprt(const exprt &_expr) : exprt(ID_min, _expr.type())
38 {
39 }
40};
41
48{
49public:
51 const exprt &lower,
52 const exprt &upper,
53 const typet type)
54 : binary_exprt(lower, ID_constant_interval, upper, type)
55 {
57 }
58
61 {
62 }
63
64 explicit constant_interval_exprt(const exprt &x)
65 : constant_interval_exprt(x, x, x.type())
66 {
67 }
68
71 {
72 }
73
74 constant_interval_exprt(const exprt &lower, const exprt &upper)
75 : constant_interval_exprt(lower, upper, lower.type())
76 {
77 }
78
79 bool is_well_formed() const
80 {
81 bool b = true;
82
83 const typet &type = this->type();
84 const exprt &lower = get_lower();
85 const exprt &upper = get_upper();
86
87 b &= is_numeric() || type.id() == ID_bool || type.is_nil();
88
89 b &= type == lower.type();
90 b &= type == upper.type();
91
92 b &= is_valid_bound(lower);
93 b &= is_valid_bound(upper);
94
95 b &= !is_numeric() || is_bottom() || less_than_or_equal(lower, upper);
96
97 return b;
98 }
99
100 bool is_valid_bound(const exprt &expr) const
101 {
102 const irep_idt &id = expr.id();
103
104 bool b = true;
105
106 b &= id == ID_constant || id == ID_min || id == ID_max;
107
108 if(type().id() == ID_bool && id == ID_constant)
109 {
110 b &= expr == true_exprt() || expr == false_exprt();
111 }
112
113 return b;
114 }
115
117
118 /* Naming scheme
119 * is_[X]? Returns bool / tvt
120 * get_[X]? Returns relevant object
121 * [X] Generator of some object.
122 * generate_[X] generator used for evaluation
123 */
124
125 /* Getters */
126 const exprt &get_lower() const;
127 const exprt &get_upper() const;
128
133 const constant_interval_exprt &other,
134 const irep_idt &) const;
135
136 constant_interval_exprt eval(const irep_idt &unary_operator) const;
138 eval(const irep_idt &binary_operator, const constant_interval_exprt &o) const;
139
140 /* Unary arithmetic */
143
145
146 /* Logical */
147 tvt is_definitely_true() const;
148 tvt is_definitely_false() const;
149
151 tvt logical_or(const constant_interval_exprt &o) const;
153 tvt logical_not() const;
154
155 /* Binary */
161
162 /* Binary shifts */
165
166 /* Unary bitwise */
168
169 /* Binary bitwise */
173
174 tvt less_than(const constant_interval_exprt &o) const;
178 tvt equal(const constant_interval_exprt &o) const;
179 tvt not_equal(const constant_interval_exprt &o) const;
180
183
184 bool is_empty() const;
185 bool is_single_value_interval() const;
188 // tvt contains(constant_interval_exprt &o) const;
189
190 /* SET OF EXPR COMPARATORS */
191 static bool equal(const exprt &a, const exprt &b);
192 static bool not_equal(const exprt &a, const exprt &b);
193 static bool less_than(const exprt &a, const exprt &b);
194 static bool less_than_or_equal(const exprt &a, const exprt &b);
195 static bool greater_than(const exprt &a, const exprt &b);
196 static bool greater_than_or_equal(const exprt &a, const exprt &b);
197 /* END SET OF EXPR COMPS */
198
199 /* INTERVAL COMPARISONS, returns tvt.is_true(). False cannot be trusted
200 * (could be false or unknown, either use less_than, etc method or use the correct
201 * operator)! */
202 friend bool operator<(
205 friend bool operator>(
208 friend bool operator<=(
211 friend bool operator>=(
214 friend bool operator==(
217 friend bool operator!=(
220
221 /* Operator override for intervals */
254
255 friend std::ostream &
256 operator<<(std::ostream &out, const constant_interval_exprt &i);
257 std::string to_string() const;
258
259 /* Now static equivalents! */
260 static tvt is_true(const constant_interval_exprt &a);
261 static tvt is_false(const constant_interval_exprt &a);
262
263 static tvt logical_and(
265 const constant_interval_exprt &b);
266 static tvt logical_or(
268 const constant_interval_exprt &b);
269 static tvt logical_xor(
271 const constant_interval_exprt &b);
272 static tvt logical_not(const constant_interval_exprt &a);
273
276
277 /* Binary */
288
289 /* Binary shifts */
292 const constant_interval_exprt &b);
295 const constant_interval_exprt &b);
296
297 /* Unary bitwise */
299
300 /* Binary bitwise */
303 const constant_interval_exprt &b);
306 const constant_interval_exprt &b);
309 const constant_interval_exprt &b);
310
311 static tvt
313 static tvt greater_than(
315 const constant_interval_exprt &b);
316 static tvt less_than_or_equal(
318 const constant_interval_exprt &b);
321 const constant_interval_exprt &b);
322 static tvt
324 static tvt
326
329
330 static bool is_empty(const constant_interval_exprt &a);
332
333 static bool is_top(const constant_interval_exprt &a);
334 static bool is_bottom(const constant_interval_exprt &a);
335
336 static bool is_min(const constant_interval_exprt &a);
337 static bool is_max(const constant_interval_exprt &a);
338 /* End static equivalents */
339
340 bool is_top() const;
341 bool is_bottom() const;
342 static constant_interval_exprt top(const typet &type);
346
347 bool has_no_lower_bound() const;
348 bool has_no_upper_bound() const;
349 static bool is_min(const exprt &expr);
350 static bool is_max(const exprt &expr);
351
352 /* Generate min and max exprt according to current type */
353 min_exprt min() const;
354 max_exprt max() const;
355
356 constant_exprt zero() const;
357 static constant_exprt zero(const typet &type);
358 static constant_exprt zero(const exprt &expr);
359 static constant_exprt zero(const constant_interval_exprt &interval);
360
361 /* Private? */
365 const irep_idt &operation);
366 static exprt get_extreme(std::vector<exprt> values, bool min = true);
367 static exprt get_max(const exprt &a, const exprt &b);
368 static exprt get_min(const exprt &a, const exprt &b);
369 static exprt get_min(std::vector<exprt> &values);
370 static exprt get_max(std::vector<exprt> &values);
371
372 /* we don't simplify in the constructor otherwise */
374 static exprt simplified_expr(exprt expr);
375
376 /* Helpers */
377 /* Four common params: self, static: type, expr, interval */
378
379 bool is_numeric() const;
380 static bool is_numeric(const typet &type);
381 static bool is_numeric(const exprt &expr);
382 static bool is_numeric(const constant_interval_exprt &interval);
383
384 bool is_int() const;
385 static bool is_int(const typet &type);
386 static bool is_int(const exprt &expr);
387 static bool is_int(const constant_interval_exprt &interval);
388
389 bool is_float() const;
390 static bool is_float(const typet &type);
391 static bool is_float(const exprt &expr);
392 static bool is_float(const constant_interval_exprt &interval);
393
394 bool is_bitvector() const;
395 static bool is_bitvector(const typet &type);
396 static bool is_bitvector(const constant_interval_exprt &interval);
397 static bool is_bitvector(const exprt &expr);
398
399 bool is_signed() const;
400 static bool is_signed(const typet &type);
401 static bool is_signed(const exprt &expr);
402 static bool is_signed(const constant_interval_exprt &interval);
403
404 bool is_unsigned() const;
405 static bool is_unsigned(const typet &type);
406 static bool is_unsigned(const exprt &expr);
407 static bool is_unsigned(const constant_interval_exprt &interval);
408
409 bool contains_zero() const;
410 bool contains(const constant_interval_exprt &interval) const;
411
412 static bool is_extreme(const exprt &expr);
413 static bool is_extreme(const exprt &expr1, const exprt &expr2);
414
415 static bool contains_extreme(const exprt expr);
416 static bool contains_extreme(const exprt expr1, const exprt expr2);
417
418 bool is_positive() const;
419 static bool is_positive(const exprt &expr);
420 static bool is_positive(const constant_interval_exprt &interval);
421
422 bool is_zero() const;
423 static bool is_zero(const exprt &expr);
424 static bool is_zero(const constant_interval_exprt &interval);
425
426 bool is_negative() const;
427 static bool is_negative(const exprt &expr);
428 static bool is_negative(const constant_interval_exprt &interval);
429
430 static exprt abs(const exprt &expr);
431
432private:
433 static void generate_expression(
434 const exprt &lhs,
435 const exprt &rhs,
436 const irep_idt &operation,
437 std::vector<exprt> &collection);
438 static void append_multiply_expression(
439 const exprt &lower,
440 const exprt &upper,
441 std::vector<exprt> &collection);
443 const exprt &expr,
444 std::vector<exprt> &collection);
446 const exprt &min,
447 const exprt &other,
448 std::vector<exprt> &collection);
449 static exprt generate_division_expression(const exprt &lhs, const exprt &rhs);
450 static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs);
452 const exprt &lhs,
453 const exprt &rhs,
454 const irep_idt &operation);
455};
456
457inline const constant_interval_exprt &
459{
460 PRECONDITION(expr.id() == ID_constant_interval);
461 return static_cast<const constant_interval_exprt &>(expr);
462}
463
464#endif /* SRC_ANALYSES_INTERVAL_H_ */
A base class for binary expressions.
Definition: std_expr.h:550
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
A constant literal expression.
Definition: std_expr.h:2807
Represents an interval of values.
Definition: interval.h:48
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:470
bool is_negative() const
Definition: interval.cpp:1924
friend const constant_interval_exprt operator<<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1599
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:683
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
constant_interval_exprt minus(const constant_interval_exprt &other) const
Definition: interval.cpp:114
tvt greater_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:426
friend const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1552
bool is_signed() const
Definition: interval.cpp:1180
constant_interval_exprt(const typet &type)
Definition: interval.h:69
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:398
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
Definition: interval.cpp:346
constant_interval_exprt decrement() const
Definition: interval.cpp:465
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:404
friend bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1510
tvt is_definitely_false() const
Definition: interval.cpp:224
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:302
friend const constant_interval_exprt operator%(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1566
tvt not_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:455
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:898
friend const constant_interval_exprt operator>>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1606
friend bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1524
bool has_no_upper_bound() const
Definition: interval.cpp:1205
friend bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1496
bool is_bottom() const
Definition: interval.cpp:1036
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1626
constant_interval_exprt(const exprt &x)
Definition: interval.h:64
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition: interval.cpp:126
static constant_interval_exprt tvt_to_interval(const tvt &val)
Definition: interval.cpp:1965
constant_interval_exprt unary_plus() const
Definition: interval.cpp:39
constant_interval_exprt plus(const constant_interval_exprt &o) const
Definition: interval.cpp:76
static exprt get_extreme(std::vector< exprt > values, bool min=true)
Definition: interval.cpp:496
bool is_numeric() const
Definition: interval.cpp:1079
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:600
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:335
bool is_positive() const
Definition: interval.cpp:1914
bool is_single_value_interval() const
Definition: interval.cpp:1864
constant_interval_exprt increment() const
Definition: interval.cpp:460
bool is_bitvector() const
Definition: interval.cpp:1190
std::string to_string() const
Definition: interval.cpp:1435
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1426
friend const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1573
bool is_well_formed() const
Definition: interval.h:79
friend bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1503
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1195
tvt logical_or(const constant_interval_exprt &o) const
Definition: interval.cpp:255
static exprt simplified_expr(exprt expr)
Definition: interval.cpp:986
bool contains_zero() const
Definition: interval.cpp:1870
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
Definition: interval.cpp:938
friend const constant_interval_exprt operator+(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1538
friend bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1531
constant_interval_exprt modulo(const constant_interval_exprt &o) const
Definition: interval.cpp:154
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
constant_interval_exprt(const constant_interval_exprt &x)
Definition: interval.h:59
bool has_no_lower_bound() const
Definition: interval.cpp:1210
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
static bool is_max(const constant_interval_exprt &a)
Definition: interval.cpp:1824
constant_interval_exprt(const exprt &lower, const exprt &upper)
Definition: interval.h:74
friend const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1545
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
Definition: interval.cpp:571
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:792
tvt is_definitely_true() const
Definition: interval.cpp:218
bool is_unsigned() const
Definition: interval.cpp:1185
min_exprt min() const
Definition: interval.cpp:1021
max_exprt max() const
Definition: interval.cpp:1026
static bool is_min(const constant_interval_exprt &a)
Definition: interval.cpp:1819
friend const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1559
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:738
tvt logical_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:274
friend const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1587
const exprt & get_lower() const
Definition: interval.cpp:29
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:663
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:319
tvt logical_and(const constant_interval_exprt &o) const
Definition: interval.cpp:266
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:638
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
Definition: interval.cpp:357
constant_interval_exprt top() const
Definition: interval.cpp:1052
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1829
constant_interval_exprt(const exprt &lower, const exprt &upper, const typet type)
Definition: interval.h:50
constant_interval_exprt unary_minus() const
Definition: interval.cpp:44
constant_exprt zero() const
Definition: interval.cpp:1016
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:377
static exprt abs(const exprt &expr)
Definition: interval.cpp:1299
friend const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1580
constant_interval_exprt bitwise_not() const
Definition: interval.cpp:367
constant_interval_exprt divide(const constant_interval_exprt &o) const
Definition: interval.cpp:137
bool is_valid_bound(const exprt &expr) const
Definition: interval.h:100
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
Definition: interval.cpp:981
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
Definition: interval.cpp:950
tvt logical_not() const
Definition: interval.cpp:284
const exprt & get_upper() const
Definition: interval.cpp:34
friend bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1517
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:432
friend const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
Definition: interval.cpp:1594
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
+∞ upper bound for intervals
Definition: interval.h:18
max_exprt(const typet &_type)
Definition: interval.h:20
max_exprt(const exprt &_expr)
Definition: interval.h:24
-∞ upper bound for intervals
Definition: interval.h:31
min_exprt(const typet &_type)
Definition: interval.h:33
min_exprt(const exprt &_expr)
Definition: interval.h:37
The Boolean constant true.
Definition: std_expr.h:2856
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:458
static int8_t r
Definition: irep_hash.h:60
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.