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/invariant.h>
13 #include <util/std_expr.h>
14 
15 #include "abstract_environment.h"
16 
19 
21 {
22 public:
24  const constant_interval_exprt &interval,
25  const namespacet &n)
26  : index(nil_exprt()),
27  next(interval.get_lower()),
28  upper(interval.get_upper()),
29  ns(n)
30  {
31  }
32 
33  const exprt &current() const override
34  {
35  return index;
36  }
37  bool advance_to_next() override
38  {
39  index = next;
42  .is_true();
43  }
44 
45 private:
46  static exprt next_element(const exprt &cur, const namespacet &ns)
47  {
48  return simplify_expr(plus_exprt(cur, from_integer(1, cur.type())), ns);
49  }
50 
54  const namespacet &ns;
55 };
56 
58  const constant_interval_exprt &interval,
59  const namespacet &n)
60 {
61  return std::make_shared<interval_index_ranget>(interval, n);
62 }
63 
64 static inline exprt look_through_casts(exprt e)
65 {
66  while(e.id() == ID_typecast)
67  {
68  e = to_typecast_expr(e).op();
69  }
70  return e;
71 }
72 
73 static inline bool
74 bvint_value_is_max(const typet &type, const mp_integer &value)
75 {
76  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
77  if(type.id() == ID_signedbv)
78  {
79  return to_signedbv_type(type).largest() == value;
80  }
81  else
82  {
83  return to_unsignedbv_type(type).largest() == value;
84  }
85 }
86 
87 static inline bool
88 bvint_value_is_min(const typet &type, const mp_integer &value)
89 {
90  PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
91  if(type.id() == ID_signedbv)
92  {
93  return to_signedbv_type(type).smallest() == value;
94  }
95  else
96  {
97  return to_unsignedbv_type(type).smallest() == value;
98  }
99 }
100 
101 static inline constant_interval_exprt
103 {
104  return constant_interval_exprt(min_exprt(value.type()), value);
105 }
106 
107 static inline constant_interval_exprt
109 {
110  return constant_interval_exprt(value, max_exprt(value.type()));
111 }
112 
113 static inline mp_integer force_value_from_expr(const exprt &value)
114 {
116  optionalt<mp_integer> maybe_integer_value = numeric_cast<mp_integer>(value);
117  INVARIANT(maybe_integer_value.has_value(), "Input has to have a value");
118  return maybe_integer_value.value();
119 }
120 
121 static inline constant_interval_exprt
123 {
124  mp_integer integer_value = force_value_from_expr(value);
125  if(!bvint_value_is_min(value.type(), integer_value))
127  min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
128  else
129  return constant_interval_exprt::bottom(value.type());
130 }
131 
132 static inline constant_interval_exprt
134 {
135  mp_integer integer_value = force_value_from_expr(value);
136  if(!bvint_value_is_max(value.type(), integer_value))
138  from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
139  else
140  return constant_interval_exprt::bottom(value.type());
141 }
142 
143 static inline bool represents_interval(exprt e)
144 {
145  e = look_through_casts(e);
146  return (e.id() == ID_constant_interval || e.id() == ID_constant);
147 }
148 
150 {
151  e = look_through_casts(e);
152  if(e.id() == ID_constant_interval)
153  {
154  return to_constant_interval_expr(e);
155  }
156  else if(e.id() == ID_constant)
157  {
158  return constant_interval_exprt(e, e);
159  }
160  else
161  {
162  // not directly representable, so just return TOP
163  return constant_interval_exprt(e.type());
164  }
165 }
166 
167 static inline irep_idt invert_relation(const irep_idt &relation)
168 {
169  PRECONDITION(
170  relation == ID_le || relation == ID_lt || relation == ID_ge ||
171  relation == ID_gt || relation == ID_equal);
172  if(relation == ID_le)
173  return ID_ge;
174  if(relation == ID_ge)
175  return ID_le;
176  if(relation == ID_lt)
177  return ID_gt;
178  if(relation == ID_gt)
179  return ID_lt;
180  return relation;
181 }
182 
189 {
190  PRECONDITION(e.operands().size() == 2);
191  const auto &relation = e.id();
192  const auto &binary_e = to_binary_expr(e);
193  const auto &lhs = binary_e.lhs();
194  const auto &rhs = binary_e.rhs();
195  PRECONDITION(
196  relation == ID_le || relation == ID_lt || relation == ID_ge ||
197  relation == ID_gt || relation == ID_equal);
198  PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
199  PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
200  PRECONDITION(lhs.id() != rhs.id());
201 
202  const auto the_constant_part_of_the_relation =
203  (rhs.id() == ID_symbol ? lhs : rhs);
204  const auto maybe_inverted_relation =
205  (rhs.id() == ID_symbol ? invert_relation(relation) : relation);
206 
207  if(maybe_inverted_relation == ID_le)
208  return interval_from_x_le_value(the_constant_part_of_the_relation);
209  if(maybe_inverted_relation == ID_lt)
210  return interval_from_x_lt_value(the_constant_part_of_the_relation);
211  if(maybe_inverted_relation == ID_ge)
212  return interval_from_x_ge_value(the_constant_part_of_the_relation);
213  if(maybe_inverted_relation == ID_gt)
214  return interval_from_x_gt_value(the_constant_part_of_the_relation);
215  INVARIANT(
216  maybe_inverted_relation == ID_equal, "We excluded other cases above");
218  the_constant_part_of_the_relation, the_constant_part_of_the_relation);
219 }
220 
222  : abstract_value_objectt(t), interval(t)
223 {
224 }
225 
227  const typet &t,
228  bool tp,
229  bool bttm)
230  : abstract_value_objectt(t, tp, bttm), interval(t)
231 {
232 }
233 
235  const constant_interval_exprt &e)
236  : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e)
237 {
238 }
239 
241  const exprt &e,
242  const abstract_environmentt &environment,
243  const namespacet &ns)
246  ? make_interval_expr(e)
247  : (e.operands().size() == 2 ? interval_from_relation(e)
248  : constant_interval_exprt(e.type())))
249 {
250 }
251 
253 {
254  // Attempt to reduce this interval to a constant expression
256  {
257  // Interval is the equivalent of a constant, so reduce it to a constant
259  }
261 #if 0
262  if(!is_top() && !is_bottom())
263  {
264  return this->interval;
265  }
266  else
267  {
269  }
270 #endif
271 }
272 
274  const exprt &expr,
275  const std::vector<abstract_object_pointert> &operands,
276  const abstract_environmentt &environment,
277  const namespacet &ns) const
278 {
279  std::size_t num_operands = expr.operands().size();
280  PRECONDITION(operands.size() == num_operands);
281 
282  std::vector<sharing_ptrt<interval_abstract_valuet>> interval_operands;
283 
284  for(const auto &op : operands)
285  {
286  auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
287  if(!iav)
288  {
289  // The operand isn't an interval - if it's an integral constant we can
290  // convert it into an interval.
291 
292  if(constant_interval_exprt::is_int(op->type()))
293  {
294  const auto op_as_constant = op->to_constant();
295  if(op_as_constant.is_nil())
296  {
297  auto top_object =
298  environment.abstract_object_factory(expr.type(), ns, true, false);
299  auto top_context_object =
300  std::dynamic_pointer_cast<const context_abstract_objectt>(
301  top_object);
302  CHECK_RETURN(top_context_object);
303  return top_context_object->get_child();
304  }
305  const auto ivop =
306  environment.abstract_object_factory(op->type(), op_as_constant, ns);
307  const auto ivop_context =
308  std::dynamic_pointer_cast<const context_abstract_objectt>(ivop);
309  if(ivop_context)
310  {
311  iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(
312  ivop_context->get_child());
313  }
314  else
315  iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(ivop);
316  }
317  CHECK_RETURN(
318  !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
319 
320  if(!iav)
321  {
322  // If we could not convert the operand into an interval,
323  // e.g. if its type is not something we can represent as an interval,
324  // try dispatching the expression_transform under that type instead.
325  return op->expression_transform(expr, operands, environment, ns);
326  }
327  }
328 
329  INVARIANT(iav, "Should be an interval abstract value");
330  interval_operands.push_back(iav);
331  }
332 
333  if(num_operands == 0)
334  return environment.abstract_object_factory(expr.type(), ns, true, false);
335 
336  if(expr.id() == ID_if)
337  return evaluate_conditional(expr, interval_operands, environment, ns);
338 
339  if(num_operands == 1)
340  return evaluate_unary_expr(expr, interval_operands, environment, ns);
341 
342  constant_interval_exprt result = interval_operands[0]->interval;
343 
344  for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
345  {
346  auto &interval_next = interval_operands[opIndex]->interval;
347  result = result.eval(expr.id(), interval_next);
348  }
349 
350  INVARIANT(
351  result.type() == expr.type(),
352  "Type of result interval should match expression type");
353  return environment.abstract_object_factory(expr.type(), result, ns);
354 }
355 
357  const exprt &expr,
358  const std::vector<interval_abstract_value_pointert> &interval_operands,
359  const abstract_environmentt &env,
360  const namespacet &ns)
361 {
362  auto const &condition_interval = interval_operands[0]->interval;
363  auto const &true_interval = interval_operands[1]->interval;
364  auto const &false_interval = interval_operands[2]->interval;
365 
366  auto condition_result = condition_interval.is_definitely_true();
367 
368  if(condition_result.is_unknown())
369  {
370  // Value of the condition is both true and false, so
371  // combine the intervals of both the true and false expressions
372  return env.abstract_object_factory(
373  expr.type(),
376  true_interval.get_lower(), false_interval.get_lower()),
378  true_interval.get_upper(), false_interval.get_upper())),
379  ns);
380  }
381 
382  return condition_result.is_true()
384  true_interval.type(), true_interval, ns)
386  false_interval.type(), false_interval, ns);
387 }
388 
390  const exprt &expr,
391  const std::vector<interval_abstract_value_pointert> &interval_operands,
392  const abstract_environmentt &environment,
393  const namespacet &ns)
394 {
395  const constant_interval_exprt &operand_expr = interval_operands[0]->interval;
396 
397  if(expr.id() == ID_typecast)
398  {
399  const typecast_exprt &tce = to_typecast_expr(expr);
400 
401  const constant_interval_exprt &new_interval =
402  operand_expr.typecast(tce.type());
403 
404  INVARIANT(
405  new_interval.type() == expr.type(),
406  "Type of result interval should match expression type");
407 
408  return environment.abstract_object_factory(tce.type(), new_interval, ns);
409  }
410 
411  const constant_interval_exprt &interval_result = operand_expr.eval(expr.id());
412  INVARIANT(
413  interval_result.type() == expr.type(),
414  "Type of result interval should match expression type");
415  return environment.abstract_object_factory(expr.type(), interval_result, ns);
416 }
417 
419  std::ostream &out,
420  const ai_baset &ai,
421  const namespacet &ns) const
422 {
423  if(!is_top() && !is_bottom())
424  {
425  std::string lower_string;
426  std::string upper_string;
427 
428  if(interval.get_lower().id() == ID_min)
429  {
430  lower_string = "-INF";
431  }
432  else
433  {
434  INVARIANT(
435  interval.get_lower().id() == ID_constant,
436  "We only support constant limits");
437  lower_string =
439  }
440 
441  if(interval.get_upper().id() == ID_max)
442  {
443  upper_string = "+INF";
444  }
445  else
446  {
447  INVARIANT(
448  interval.get_lower().id() == ID_constant,
449  "We only support constant limits");
450  upper_string =
452  }
453 
454  out << "[" << lower_string << ", " << upper_string << "]";
455  }
456  else
457  {
458  abstract_objectt::output(out, ai, ns);
459  }
460 }
461 
464 {
466  std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
467  if(cast_other)
468  {
469  return merge_intervals(cast_other);
470  }
471  else
472  {
473  return abstract_objectt::merge(other);
474  }
475 }
476 
486 {
487  if(is_bottom() || other->interval.contains(interval))
488  {
489  return other;
490  }
491  else if(other->is_bottom() || interval.contains(other->interval))
492  {
493  return shared_from_this();
494  }
495  else
496  {
497  return std::make_shared<interval_abstract_valuet>(constant_interval_exprt(
499  interval.get_lower(), other->interval.get_lower()),
501  interval.get_upper(), other->interval.get_upper())));
502  }
503 }
504 
507 {
509  std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
510  if(cast_other)
511  {
512  return meet_intervals(cast_other);
513  }
514  else
515  {
516  return abstract_objectt::meet(other);
517  }
518 }
519 
528 {
529  if(is_bottom() || other->interval.contains(interval))
530  {
531  return shared_from_this();
532  }
533  else if(other->is_bottom() || interval.contains(other->interval))
534  {
535  return other;
536  }
537  else
538  {
539  auto lower_bound = constant_interval_exprt::get_max(
540  interval.get_lower(), other->interval.get_lower());
541  auto upper_bound = constant_interval_exprt::get_min(
542  interval.get_upper(), other->interval.get_upper());
543 
544  if(constant_interval_exprt::less_than(upper_bound, lower_bound))
545  return std::make_shared<interval_abstract_valuet>(
546  interval.type(), false, true);
547  return std::make_shared<interval_abstract_valuet>(
548  constant_interval_exprt(lower_bound, upper_bound));
549  }
550 }
551 
554 {
555  if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
556  return make_empty_index_range();
557  if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
558  return make_empty_index_range();
559 
561 }
562 
564 {
565  return interval;
566 }
567 
569  abstract_object_statisticst &statistics,
570  abstract_object_visitedt &visited,
571  const abstract_environmentt &env,
572  const namespacet &ns) const
573 {
574  abstract_objectt::get_statistics(statistics, visited, env, ns);
577  {
579  }
580  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
581 }
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_ptrt make_empty_index_range()
std::shared_ptr< index_ranget > index_range_ptrt
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
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.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
const irep_idt & get_value() const
Definition: std_expr.h:2676
Represents an interval of values.
Definition: interval.h:56
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1811
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1806
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1623
bool is_single_value_interval() const
Definition: interval.cpp:1861
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1423
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:792
const exprt & get_lower() const
Definition: interval.cpp:29
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:377
const exprt & get_upper() const
Definition: interval.cpp:34
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:47
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:185
mp_integer smallest() const
Return the smallest value that can be represented using this type.
Definition: std_types.cpp:180
static abstract_object_pointert evaluate_conditional(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
static abstract_object_pointert evaluate_unary_expr(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
const constant_interval_exprt & get_interval() const
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
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,...
abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const
Merge another interval abstract object with this one.
index_range_ptrt index_range(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
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,...
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
constant_interval_exprt interval
const exprt & current() const override
interval_index_ranget(const constant_interval_exprt &interval, const namespacet &n)
static exprt next_element(const exprt &cur, const namespacet &ns)
const irep_idt & id() const
Definition: irep.h:407
+∞ upper bound for intervals
Definition: interval.h:26
static memory_sizet from_bytes(std::size_t bytes)
-∞ upper bound for intervals
Definition: interval.h:39
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
The plus expression Associativity is not specified.
Definition: std_expr.h:831
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:294
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition: interval.h:466
static exprt look_through_casts(exprt e)
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
static mp_integer force_value_from_expr(const exprt &value)
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
static bool represents_interval(exprt e)
static irep_idt invert_relation(const irep_idt &relation)
static index_range_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
static constant_interval_exprt make_interval_expr(exprt e)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
An interval to represent a set of possible values.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1305
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1255
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.