cprover
interval_abstract_value.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity intervals
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <limits.h>
10 #include <ostream>
11 
12 #include <util/bitvector_types.h>
13 #include <util/invariant.h>
14 #include <util/make_unique.h>
15 
16 #include "abstract_environment.h"
17 
20 
22  const constant_interval_exprt &interval,
23  const namespacet &n);
24 
26 {
27 public:
29  const constant_interval_exprt &interval_,
30  const namespacet &n)
31  : interval(interval_),
32  index(nil_exprt()),
33  next(interval.get_lower()),
34  upper(interval.get_upper()),
35  ns(n)
36  {
37  }
38 
39  const exprt &current() const override
40  {
41  return index;
42  }
43  bool advance_to_next() override
44  {
45  index = next;
48  .is_true();
49  }
50 
52  {
54  }
55 
56 private:
57  static exprt next_element(const exprt &cur, const namespacet &ns)
58  {
59  return simplify_expr(plus_exprt(cur, from_integer(1, cur.type())), ns);
60  }
61 
66  const namespacet &ns;
67 };
68 
70  const constant_interval_exprt &interval,
71  const namespacet &n)
72 {
73  return util_make_unique<interval_index_ranget>(interval, n);
74 }
75 
76 static inline exprt look_through_casts(exprt e)
77 {
78  while(e.id() == ID_typecast)
79  {
80  e = to_typecast_expr(e).op();
81  }
82  return e;
83 }
84 
85 static inline bool
86 bvint_value_is_max(const typet &type, const mp_integer &value)
87 {
88  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
89  if(type.id() == ID_signedbv)
90  {
91  return to_signedbv_type(type).largest() == value;
92  }
93  else
94  {
95  return to_unsignedbv_type(type).largest() == value;
96  }
97 }
98 
99 static inline bool
100 bvint_value_is_min(const typet &type, const mp_integer &value)
101 {
102  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
103  if(type.id() == ID_signedbv)
104  {
105  return to_signedbv_type(type).smallest() == value;
106  }
107  else
108  {
109  return to_unsignedbv_type(type).smallest() == value;
110  }
111 }
112 
113 static inline constant_interval_exprt
115 {
116  return constant_interval_exprt(min_exprt(value.type()), value);
117 }
118 
119 static inline constant_interval_exprt
121 {
122  return constant_interval_exprt(value, max_exprt(value.type()));
123 }
124 
125 static inline mp_integer force_value_from_expr(const exprt &value)
126 {
128  optionalt<mp_integer> maybe_integer_value = numeric_cast<mp_integer>(value);
129  INVARIANT(maybe_integer_value.has_value(), "Input has to have a value");
130  return maybe_integer_value.value();
131 }
132 
133 static inline constant_interval_exprt
135 {
136  mp_integer integer_value = force_value_from_expr(value);
137  if(!bvint_value_is_min(value.type(), integer_value))
139  min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
140  else
141  return constant_interval_exprt::bottom(value.type());
142 }
143 
144 static inline constant_interval_exprt
146 {
147  mp_integer integer_value = force_value_from_expr(value);
148  if(!bvint_value_is_max(value.type(), integer_value))
150  from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
151  else
152  return constant_interval_exprt::bottom(value.type());
153 }
154 
155 static inline bool represents_interval(exprt e)
156 {
157  e = look_through_casts(e);
158  return (e.id() == ID_constant_interval || e.id() == ID_constant);
159 }
160 
162 {
163  e = look_through_casts(e);
164  if(e.id() == ID_constant_interval)
165  {
166  return to_constant_interval_expr(e);
167  }
168  else if(e.id() == ID_constant)
169  {
170  return constant_interval_exprt(e, e);
171  }
172  else
173  {
174  // not directly representable, so just return TOP
175  return constant_interval_exprt(e.type());
176  }
177 }
178 
179 static inline irep_idt invert_relation(const irep_idt &relation)
180 {
181  PRECONDITION(
182  relation == ID_le || relation == ID_lt || relation == ID_ge ||
183  relation == ID_gt || relation == ID_equal);
184  if(relation == ID_le)
185  return ID_ge;
186  if(relation == ID_ge)
187  return ID_le;
188  if(relation == ID_lt)
189  return ID_gt;
190  if(relation == ID_gt)
191  return ID_lt;
192  return relation;
193 }
194 
201 {
202  PRECONDITION(e.operands().size() == 2);
203  const auto &relation = e.id();
204  const auto &binary_e = to_binary_expr(e);
205  const auto &lhs = binary_e.lhs();
206  const auto &rhs = binary_e.rhs();
207  PRECONDITION(
208  relation == ID_le || relation == ID_lt || relation == ID_ge ||
209  relation == ID_gt || relation == ID_equal);
210  PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
211  PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
212  PRECONDITION(lhs.id() != rhs.id());
213 
214  const auto the_constant_part_of_the_relation =
215  (rhs.id() == ID_symbol ? lhs : rhs);
216  const auto maybe_inverted_relation =
217  (rhs.id() == ID_symbol ? invert_relation(relation) : relation);
218 
219  if(maybe_inverted_relation == ID_le)
220  return interval_from_x_le_value(the_constant_part_of_the_relation);
221  if(maybe_inverted_relation == ID_lt)
222  return interval_from_x_lt_value(the_constant_part_of_the_relation);
223  if(maybe_inverted_relation == ID_ge)
224  return interval_from_x_ge_value(the_constant_part_of_the_relation);
225  if(maybe_inverted_relation == ID_gt)
226  return interval_from_x_gt_value(the_constant_part_of_the_relation);
227  INVARIANT(
228  maybe_inverted_relation == ID_equal, "We excluded other cases above");
230  the_constant_part_of_the_relation, the_constant_part_of_the_relation);
231 }
232 
234  : abstract_value_objectt(t), interval(t)
235 {
236 }
237 
239  const typet &t,
240  bool tp,
241  bool bttm)
242  : abstract_value_objectt(t, tp, bttm), interval(t)
243 {
244 }
245 
247  const constant_interval_exprt &e)
248  : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e)
249 {
250 }
251 
253  const exprt &e,
254  const abstract_environmentt &environment,
255  const namespacet &ns)
258  ? make_interval_expr(e)
259  : (e.operands().size() == 2 ? interval_from_relation(e)
260  : constant_interval_exprt(e.type())))
261 {
262 }
263 
265 {
266  // Attempt to reduce this interval to a constant expression
268  {
269  // Interval is the equivalent of a constant, so reduce it to a constant
271  }
273 #if 0
274  if(!is_top() && !is_bottom())
275  {
276  return this->interval;
277  }
278  else
279  {
281  }
282 #endif
283 }
284 
286 {
287  return std::hash<std::string>{}(interval.pretty());
288 }
289 
291  const abstract_object_pointert &other) const
292 {
293  auto cast_other =
294  std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
295  return cast_other && interval == cast_other->interval;
296 }
297 
299  std::ostream &out,
300  const ai_baset &ai,
301  const namespacet &ns) const
302 {
303  if(!is_top() && !is_bottom())
304  {
305  std::string lower_string;
306  std::string upper_string;
307 
308  if(interval.get_lower().id() == ID_min)
309  {
310  lower_string = "-INF";
311  }
312  else
313  {
314  INVARIANT(
315  interval.get_lower().id() == ID_constant,
316  "We only support constant limits");
317  lower_string =
319  }
320 
321  if(interval.get_upper().id() == ID_max)
322  {
323  upper_string = "+INF";
324  }
325  else
326  {
327  INVARIANT(
328  interval.get_lower().id() == ID_constant,
329  "We only support constant limits");
330  upper_string =
332  }
333 
334  out << "[" << lower_string << ", " << upper_string << "]";
335  }
336  else
337  {
338  abstract_objectt::output(out, ai, ns);
339  }
340 }
341 
344 {
345  abstract_value_pointert cast_other =
346  std::dynamic_pointer_cast<const abstract_value_objectt>(other);
347  if(cast_other)
348  {
349  return merge_intervals(cast_other);
350  }
351  else
352  {
353  return abstract_objectt::merge(other);
354  }
355 }
356 
366 {
367  if(other->is_bottom())
368  return shared_from_this();
369 
370  auto other_interval = other->to_interval();
371 
372  if(is_bottom())
373  return std::make_shared<interval_abstract_valuet>(other_interval);
374 
375  if(interval.contains(other_interval))
376  return shared_from_this();
377 
378  return std::make_shared<interval_abstract_valuet>(constant_interval_exprt(
380  interval.get_lower(), other_interval.get_lower()),
382  interval.get_upper(), other_interval.get_upper())));
383 }
384 
387 {
389  std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
390  if(cast_other)
391  {
392  return meet_intervals(cast_other);
393  }
394  else
395  {
396  return abstract_objectt::meet(other);
397  }
398 }
399 
408 {
409  if(is_bottom() || other->interval.contains(interval))
410  {
411  return shared_from_this();
412  }
413  else if(other->is_bottom() || interval.contains(other->interval))
414  {
415  return other;
416  }
417  else
418  {
419  auto lower_bound = constant_interval_exprt::get_max(
420  interval.get_lower(), other->interval.get_lower());
421  auto upper_bound = constant_interval_exprt::get_min(
422  interval.get_upper(), other->interval.get_upper());
423 
424  if(constant_interval_exprt::less_than(upper_bound, lower_bound))
425  return std::make_shared<interval_abstract_valuet>(
426  interval.type(), false, true);
427  return std::make_shared<interval_abstract_valuet>(
428  constant_interval_exprt(lower_bound, upper_bound));
429  }
430 }
431 
434 {
435  if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
436  return make_empty_index_range();
437  if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
438  return make_empty_index_range();
439 
441 }
442 
445 {
446  return make_single_value_range(shared_from_this());
447 }
448 
450  abstract_object_statisticst &statistics,
451  abstract_object_visitedt &visited,
452  const abstract_environmentt &env,
453  const namespacet &ns) const
454 {
455  abstract_objectt::get_statistics(statistics, visited, env, ns);
458  {
460  }
461  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
462 }
interval_abstract_valuet::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: interval_abstract_value.cpp:433
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
interval_index_ranget::index
exprt index
Definition: interval_abstract_value.cpp:63
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
abstract_value_pointert
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
Definition: abstract_value_object.h:297
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
index_range_implementationt
Definition: abstract_value_object.h:28
abstract_objectt::merge
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
Definition: abstract_object.cpp:189
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:170
interval_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
Definition: interval_abstract_value.cpp:298
integer_bitvector_typet::smallest
mp_integer smallest() const
Return the smallest value that can be represented using this type.
Definition: bitvector_types.cpp:33
typet
The type of an expression, extends irept.
Definition: type.h:28
interval_index_ranget::advance_to_next
bool advance_to_next() override
Definition: interval_abstract_value.cpp:43
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
constant_interval_exprt::get_max
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
constant_interval_exprt::is_bottom
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1811
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
max_exprt
+∞ upper bound for intervals
Definition: interval.h:26
constant_interval_exprt::contains
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1423
invariant.h
interval_abstract_valuet
Definition: interval_abstract_value.h:24
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
min_exprt
-∞ upper bound for intervals
Definition: interval.h:39
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
bvint_value_is_max
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
Definition: interval_abstract_value.cpp:86
interval_abstract_valuet::merge_intervals
abstract_object_pointert merge_intervals(abstract_value_pointert &other) const
Merge another interval abstract object with this one.
Definition: interval_abstract_value.cpp:365
interval_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: interval_abstract_value.cpp:264
make_interval_index_range
static index_range_implementation_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
Definition: interval_abstract_value.cpp:69
interval_from_relation
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
Definition: interval_abstract_value.cpp:200
interval_index_ranget::interval
const constant_interval_exprt & interval
Definition: interval_abstract_value.cpp:62
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
constant_interval_exprt::is_int
bool is_int() const
Definition: interval.cpp:1064
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
interval_from_x_le_value
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
Definition: interval_abstract_value.cpp:114
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
interval_abstract_valuet::internal_hash
size_t internal_hash() const override
Definition: interval_abstract_value.cpp:285
interval_abstract_valuet::meet_intervals
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
Definition: interval_abstract_value.cpp:406
make_empty_index_range
index_range_implementation_ptrt make_empty_index_range()
Definition: abstract_value_object.cpp:74
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
interval_abstract_valuet::interval_abstract_value_pointert
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
Definition: interval_abstract_value.h:71
make_unique.h
force_value_from_expr
static mp_integer force_value_from_expr(const exprt &value)
Definition: interval_abstract_value.cpp:125
interval_from_x_gt_value
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
Definition: interval_abstract_value.cpp:145
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
abstract_value_objectt
Definition: abstract_value_object.h:240
interval_index_ranget::ns
const namespacet & ns
Definition: interval_abstract_value.cpp:66
constant_interval_exprt::is_single_value_interval
bool is_single_value_interval() const
Definition: interval.cpp:1861
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
bitvector_types.h
Pre-defined bitvector types.
look_through_casts
static exprt look_through_casts(exprt e)
Definition: interval_abstract_value.cpp:76
interval_index_ranget::next
exprt next
Definition: interval_abstract_value.cpp:64
interval_index_ranget::next_element
static exprt next_element(const exprt &cur, const namespacet &ns)
Definition: interval_abstract_value.cpp:57
abstract_environment.h
An abstract version of a program environment.
constant_interval_exprt::bottom
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
interval_abstract_valuet::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: interval_abstract_value.cpp:449
constant_interval_exprt::less_than
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:377
irept::id
const irep_idt & id() const
Definition: irep.h:407
make_interval_expr
static constant_interval_exprt make_interval_expr(exprt e)
Definition: interval_abstract_value.cpp:161
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
interval_index_ranget
Definition: interval_abstract_value.cpp:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
interval_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: interval_abstract_value.cpp:51
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
interval_abstract_valuet::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
Definition: interval_abstract_value.cpp:343
interval_from_x_ge_value
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
Definition: interval_abstract_value.cpp:120
represents_interval
static bool represents_interval(exprt e)
Definition: interval_abstract_value.cpp:155
constant_interval_exprt::is_top
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1806
make_single_value_range
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
Definition: abstract_value_object.cpp:113
interval_index_ranget::upper
exprt upper
Definition: interval_abstract_value.cpp:65
interval_abstract_valuet::internal_equality
bool internal_equality(const abstract_object_pointert &other) const override
Definition: interval_abstract_value.cpp:290
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
bvint_value_is_min
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
Definition: interval_abstract_value.cpp:100
interval_abstract_value.h
An interval to represent a set of possible values.
to_constant_interval_expr
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition: interval.h:466
interval_from_x_lt_value
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
Definition: interval_abstract_value.cpp:134
abstract_object_statisticst::objects_memory_usage
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
Definition: abstract_object_statistics.h:28
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
interval_abstract_valuet::interval_abstract_valuet
interval_abstract_valuet(const typet &t)
Definition: interval_abstract_value.cpp:233
interval_abstract_valuet::meet
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
Definition: interval_abstract_value.cpp:386
abstract_object_statisticst::number_of_single_value_intervals
std::size_t number_of_single_value_intervals
Definition: abstract_object_statistics.h:21
constant_interval_exprt::get_lower
const exprt & get_lower() const
Definition: interval.cpp:29
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: bitvector_types.cpp:38
interval_index_ranget::current
const exprt & current() const override
Definition: interval_abstract_value.cpp:39
abstract_objectt::meet
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
Definition: abstract_object.cpp:217
constant_interval_exprt::get_upper
const exprt & get_upper() const
Definition: interval.cpp:34
constant_interval_exprt::get_min
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
exprt::operands
operandst & operands()
Definition: expr.h:96
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
interval_abstract_valuet::interval
constant_interval_exprt interval
Definition: interval_abstract_value.h:78
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
interval_abstract_valuet::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: interval_abstract_value.cpp:444
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
interval_index_ranget::interval_index_ranget
interval_index_ranget(const constant_interval_exprt &interval_, const namespacet &n)
Definition: interval_abstract_value.cpp:28
invert_relation
static irep_idt invert_relation(const irep_idt &relation)
Definition: interval_abstract_value.cpp:179
abstract_object_statisticst::number_of_interval_abstract_objects
std::size_t number_of_interval_abstract_objects
Definition: abstract_object_statistics.h:20
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700