cprover
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 
17 class max_exprt : public exprt
18 {
19 public:
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 
30 class min_exprt : public exprt
31 {
32 public:
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 {
49 public:
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 
116  static constant_interval_exprt tvt_to_interval(const tvt &val);
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 
150  tvt logical_and(const constant_interval_exprt &o) const;
151  tvt logical_or(const constant_interval_exprt &o) const;
152  tvt logical_xor(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;
175  tvt greater_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 */
222  friend const constant_interval_exprt operator+(
225  friend const constant_interval_exprt operator-(
228  friend const constant_interval_exprt operator/(
231  friend const constant_interval_exprt operator*(
234  friend const constant_interval_exprt operator%(
237  friend const constant_interval_exprt operator!(
239  friend const constant_interval_exprt operator&(
242  friend const constant_interval_exprt operator|(
245  friend const constant_interval_exprt operator^(
248  friend const constant_interval_exprt operator<<(
251  friend const constant_interval_exprt operator>>(
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(
264  const constant_interval_exprt &a,
265  const constant_interval_exprt &b);
266  static tvt logical_or(
267  const constant_interval_exprt &a,
268  const constant_interval_exprt &b);
269  static tvt logical_xor(
270  const constant_interval_exprt &a,
271  const constant_interval_exprt &b);
272  static tvt logical_not(const constant_interval_exprt &a);
273 
276 
277  /* Binary */
288 
289  /* Binary shifts */
291  const constant_interval_exprt &a,
292  const constant_interval_exprt &b);
294  const constant_interval_exprt &a,
295  const constant_interval_exprt &b);
296 
297  /* Unary bitwise */
299 
300  /* Binary bitwise */
302  const constant_interval_exprt &a,
303  const constant_interval_exprt &b);
305  const constant_interval_exprt &a,
306  const constant_interval_exprt &b);
308  const constant_interval_exprt &a,
309  const constant_interval_exprt &b);
310 
311  static tvt
313  static tvt greater_than(
314  const constant_interval_exprt &a,
315  const constant_interval_exprt &b);
316  static tvt less_than_or_equal(
317  const constant_interval_exprt &a,
318  const constant_interval_exprt &b);
319  static tvt greater_than_or_equal(
320  const constant_interval_exprt &a,
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);
343  static constant_interval_exprt bottom(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 
432 private:
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);
442  static void append_multiply_expression_max(
443  const exprt &expr,
444  std::vector<exprt> &collection);
445  static void append_multiply_expression_min(
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 
457 inline 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:2753
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:1921
friend const constant_interval_exprt operator<<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1596
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:1549
bool is_signed() const
Definition: interval.cpp:1177
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:1507
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:1563
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:1603
friend bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1521
bool has_no_upper_bound() const
Definition: interval.cpp:1202
friend bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1493
bool is_bottom() const
Definition: interval.cpp:1036
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1623
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:1962
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:1911
bool is_single_value_interval() const
Definition: interval.cpp:1861
constant_interval_exprt increment() const
Definition: interval.cpp:460
bool is_bitvector() const
Definition: interval.cpp:1187
std::string to_string() const
Definition: interval.cpp:1432
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1423
friend const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1570
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:1500
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1192
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:1867
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:1535
friend bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1528
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:1207
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:1821
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:1542
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:1182
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:1816
friend const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1556
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:1584
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:1826
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:1296
friend const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1577
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:1514
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:1591
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:2811
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
+∞ 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:2802
Definition: threeval.h:20
The type of an expression, extends irept.
Definition: type.h:28
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.