CBMC
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 {
19 public:
20  explicit max_value_exprt(const typet &_type)
21  : nullary_exprt(ID_max_value, _type)
22  {
23  }
24 
25  explicit max_value_exprt(const exprt &_expr)
26  : nullary_exprt(ID_max_value, _expr.type())
27  {
28  }
29 };
30 
33 {
34 public:
35  explicit min_value_exprt(const typet &_type)
36  : nullary_exprt(ID_min_value, _type)
37  {
38  }
39 
40  explicit min_value_exprt(const exprt &_expr)
41  : nullary_exprt(ID_min_value, _expr.type())
42  {
43  }
44 };
45 
52 {
53 public:
55  : binary_exprt(
56  std::move(lower),
57  ID_constant_interval,
58  std::move(upper),
59  std::move(type))
60  {
62  }
63 
68  type)
69  {
70  }
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 
120  static constant_interval_exprt tvt_to_interval(const tvt &val);
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 
140  constant_interval_exprt eval(const irep_idt &unary_operator) const;
142  eval(const irep_idt &binary_operator, const constant_interval_exprt &o) const;
143 
144  /* Unary arithmetic */
147 
149 
150  /* Logical */
151  tvt is_definitely_true() const;
152  tvt is_definitely_false() const;
153 
154  tvt logical_and(const constant_interval_exprt &o) const;
155  tvt logical_or(const constant_interval_exprt &o) const;
156  tvt logical_xor(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;
179  tvt greater_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 */
226  friend const constant_interval_exprt operator+(
229  friend const constant_interval_exprt operator-(
232  friend const constant_interval_exprt operator/(
235  friend const constant_interval_exprt operator*(
238  friend const constant_interval_exprt operator%(
241  friend const constant_interval_exprt operator!(
243  friend const constant_interval_exprt operator&(
246  friend const constant_interval_exprt operator|(
249  friend const constant_interval_exprt operator^(
252  friend const constant_interval_exprt operator<<(
255  friend const constant_interval_exprt operator>>(
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(
268  const constant_interval_exprt &a,
269  const constant_interval_exprt &b);
270  static tvt logical_or(
271  const constant_interval_exprt &a,
272  const constant_interval_exprt &b);
273  static tvt logical_xor(
274  const constant_interval_exprt &a,
275  const constant_interval_exprt &b);
276  static tvt logical_not(const constant_interval_exprt &a);
277 
280 
281  /* Binary */
292 
293  /* Binary shifts */
295  const constant_interval_exprt &a,
296  const constant_interval_exprt &b);
298  const constant_interval_exprt &a,
299  const constant_interval_exprt &b);
300 
301  /* Unary bitwise */
303 
304  /* Binary bitwise */
306  const constant_interval_exprt &a,
307  const constant_interval_exprt &b);
309  const constant_interval_exprt &a,
310  const constant_interval_exprt &b);
312  const constant_interval_exprt &a,
313  const constant_interval_exprt &b);
314 
315  static tvt
317  static tvt greater_than(
318  const constant_interval_exprt &a,
319  const constant_interval_exprt &b);
320  static tvt less_than_or_equal(
321  const constant_interval_exprt &a,
322  const constant_interval_exprt &b);
323  static tvt greater_than_or_equal(
324  const constant_interval_exprt &a,
325  const constant_interval_exprt &b);
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);
347  static constant_interval_exprt bottom(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);
400  static bool is_bitvector(const constant_interval_exprt &interval);
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 
436 private:
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);
446  static void append_multiply_expression_max(
447  const exprt &expr,
448  std::vector<exprt> &collection);
449  static void append_multiply_expression_min(
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 
461 inline const constant_interval_exprt &
463 {
464  PRECONDITION(expr.id() == ID_constant_interval);
465  return static_cast<const constant_interval_exprt &>(expr);
466 }
467 
468 #endif /* SRC_ANALYSES_INTERVAL_H_ */
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:2995
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
bool is_negative() const
Definition: interval.cpp:1925
constant_interval_exprt(exprt lower, exprt upper, typet type)
Definition: interval.h:54
max_value_exprt max() const
Definition: interval.cpp:1027
friend const constant_interval_exprt operator<<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1600
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:684
constant_interval_exprt bottom() const
Definition: interval.cpp:1058
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
Definition: interval.cpp:1022
friend const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1553
bool is_signed() const
Definition: interval.cpp:1181
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)
Definition: interval.cpp:1511
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)
Definition: interval.cpp:1567
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)
Definition: interval.cpp:1607
friend bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1525
bool has_no_upper_bound() const
Definition: interval.cpp:1206
friend bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1497
bool is_bottom() const
Definition: interval.cpp:1037
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1627
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition: interval.cpp:124
static constant_interval_exprt tvt_to_interval(const tvt &val)
Definition: interval.cpp:1966
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
bool is_numeric() const
Definition: interval.cpp:1080
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_positive() const
Definition: interval.cpp:1915
bool is_single_value_interval() const
Definition: interval.cpp:1865
constant_interval_exprt increment() const
Definition: interval.cpp:459
bool is_bitvector() const
Definition: interval.cpp:1191
std::string to_string() const
Definition: interval.cpp:1436
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1427
friend const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1574
bool is_well_formed() const
Definition: interval.h:78
friend bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1504
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1196
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
Definition: interval.cpp:1871
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)
Definition: interval.cpp:1539
friend bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1532
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
Definition: interval.cpp:1211
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:965
static bool is_max(const constant_interval_exprt &a)
Definition: interval.cpp:1825
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)
Definition: interval.cpp:1546
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
bool is_unsigned() const
Definition: interval.cpp:1186
static bool is_min(const constant_interval_exprt &a)
Definition: interval.cpp:1820
friend const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1560
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)
Definition: interval.cpp:1588
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
Definition: interval.cpp:1053
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1830
constant_interval_exprt unary_minus() const
Definition: interval.cpp:42
constant_exprt zero() const
Definition: interval.cpp:1017
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:376
static exprt abs(const exprt &expr)
Definition: interval.cpp:1300
friend const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1581
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
tvt logical_not() const
Definition: interval.cpp:283
const exprt & get_upper() const
Definition: interval.cpp:32
friend bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1518
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:431
friend const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
Definition: interval.cpp:1595
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
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
The Boolean constant false.
Definition: std_expr.h:3077
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:3068
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.