cprover
value_set_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: diffblue
6 
7 \*******************************************************************/
8 
11 
18 
19 #include <util/arith_tools.h>
20 #include <util/make_unique.h>
21 #include <util/simplify_expr.h>
22 
23 #include <algorithm>
24 
26 make_value_set_index_range(const std::set<exprt> &vals);
27 
29 {
30 public:
31  explicit value_set_index_ranget(const std::set<exprt> &vals)
32  : values(vals), cur(), next(values.begin())
33  {
34  PRECONDITION(!values.empty());
35  }
36 
37  const exprt &current() const override
38  {
39  return cur;
40  }
41  bool advance_to_next() override
42  {
43  if(next == values.end())
44  return false;
45 
46  cur = *next;
47  ++next;
48  return true;
49  }
51  {
53  }
54 
55 private:
56  std::set<exprt> values;
58  std::set<exprt>::const_iterator next;
59 };
60 
62 make_value_set_index_range(const std::set<exprt> &vals)
63 {
64  return util_make_unique<value_set_index_ranget>(vals);
65 }
66 
69 
71 {
72 public:
74  : values(vals), cur(), next(values.begin())
75  {
77  }
78 
79  const abstract_object_pointert &current() const override
80  {
81  return cur;
82  }
83  bool advance_to_next() override
84  {
85  if(next == values.end())
86  return false;
87 
88  cur = *next;
89  ++next;
90  return true;
91  }
93  {
95  }
96 
97 private:
101 };
102 
105 {
106  return util_make_unique<value_set_value_ranget>(vals);
107 }
108 
111 
117 
118 static bool are_any_top(const abstract_object_sett &set);
119 static bool is_set_extreme(const typet &type, const abstract_object_sett &set);
120 
125  const abstract_object_sett &values,
126  const constant_interval_exprt &lhs,
127  const constant_interval_exprt &rhs);
128 
130  : abstract_value_objectt(type)
131 {
132  values.insert(std::make_shared<constant_abstract_valuet>(type));
133  verify();
134 }
135 
137  const typet &type,
138  bool top,
139  bool bottom)
140  : abstract_value_objectt(type, top, bottom)
141 {
142  values.insert(std::make_shared<constant_abstract_valuet>(type, top, bottom));
143  verify();
144 }
145 
147  const exprt &expr,
148  const abstract_environmentt &environment,
149  const namespacet &ns)
150  : abstract_value_objectt(expr.type(), false, false)
151 {
152  values.insert(
153  std::make_shared<constant_abstract_valuet>(expr, environment, ns));
154  verify();
155 }
156 
158  const abstract_object_sett &initial_values)
159 {
160  PRECONDITION(!initial_values.empty());
161 
162  auto values = unwrap_and_extract_values(initial_values);
163 
165 
166  const auto &type = values.first()->type();
167  auto value_set =
168  std::make_shared<value_set_abstract_objectt>(type, false, false);
169  value_set->set_values(values);
170  return value_set;
171 }
172 
175  const namespacet &ns) const
176 {
177  if(values.empty())
179 
180  std::set<exprt> flattened;
181  for(const auto &o : values)
182  {
183  const auto &v = as_value(o);
184  for(auto e : v->index_range(ns))
185  flattened.insert(e);
186  }
187 
188  return make_value_set_index_range(flattened);
189 }
190 
193 {
195 }
196 
198 {
199  verify();
200 
201  if(values.size() == 1)
202  return values.first()->to_constant();
203 
204  auto interval = to_interval();
205  if(interval.is_single_value_interval())
206  return interval.get_lower();
207 
209 }
210 
212 {
213  return values.to_interval();
214 }
215 
217  const abstract_value_pointert &other,
218  const widen_modet &widen_mode) const
219 {
220  auto union_values = !is_bottom() ? values : abstract_object_sett{};
221 
222  auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
223  if(other_value_set)
224  union_values.insert(other_value_set->get_values());
225  else
226  union_values.insert(other);
227 
228  auto has_values = [](const abstract_object_pointert &v) {
229  return !v->is_top() && !v->is_bottom();
230  };
231 
232  if(
233  widen_mode == widen_modet::could_widen && has_values(shared_from_this()) &&
234  has_values(other))
235  {
236  union_values =
237  widen_value_set(union_values, to_interval(), other->to_interval());
238  }
239 
240  return resolve_values(union_values);
241 }
242 
244  const abstract_value_pointert &other) const
245 {
246  if(other->is_bottom())
247  return shared_from_this();
248 
249  auto meet_values = abstract_object_sett{};
250 
251  if(is_bottom())
252  meet_values.insert(other);
253  else
254  {
255  auto this_interval = to_interval();
256  auto other_interval = other->to_interval();
257 
258  auto lower_bound = constant_interval_exprt::get_max(
259  this_interval.get_lower(), other_interval.get_lower());
260  auto upper_bound = constant_interval_exprt::get_min(
261  this_interval.get_upper(), other_interval.get_upper());
262 
263  // if the interval is valid, we have a meet!
264  if(constant_interval_exprt::less_than_or_equal(lower_bound, upper_bound))
265  {
266  auto meet_interval = constant_interval_exprt(lower_bound, upper_bound);
267  abstract_object_pointert meet_value =
268  std::make_shared<interval_abstract_valuet>(meet_interval);
269  if(meet_interval.is_single_value_interval())
270  meet_value = std::make_shared<constant_abstract_valuet>(lower_bound);
271  meet_values.insert(meet_value);
272  }
273  }
274 
275  if(meet_values.empty()) // no meet :(
276  return std::make_shared<value_set_abstract_objectt>(type(), false, true);
277 
278  return resolve_values(meet_values);
279 }
280 
282  const abstract_object_sett &new_values) const
283 {
284  PRECONDITION(!new_values.empty());
285 
286  if(new_values == values)
287  return shared_from_this();
288 
289  return make_value_set(new_values);
290 }
291 
293 {
294  values.clear();
295  values.insert(std::make_shared<constant_abstract_valuet>(type()));
296 }
297 
299  const abstract_object_sett &other_values)
300 {
301  PRECONDITION(!other_values.empty());
302  if(are_any_top(other_values) || is_set_extreme(type(), other_values))
303  {
304  set_top();
305  }
306  else
307  {
308  set_not_top();
309  values = other_values;
310  }
311  set_not_bottom();
312  verify();
313 }
314 
316  const exprt &lower,
317  const exprt &upper) const
318 {
319  using cie = constant_interval_exprt;
320 
321  auto constrained_values = abstract_object_sett{};
322 
323  for(auto const &value : unwrap_and_extract_values(values))
324  {
325  auto constrained = as_value(value)->constrain(lower, upper);
326  auto constrained_interval = constrained->to_interval();
327 
328  if(cie::less_than(constrained_interval.get_lower(), lower))
329  continue;
330  if(cie::greater_than(constrained_interval.get_upper(), upper))
331  continue;
332 
333  constrained_values.insert(constrained);
334  }
335 
336  return as_value(resolve_values(constrained_values));
337 }
338 
340 {
341  auto compacted = non_destructive_compact(values);
342  if(compacted.size() == 1)
343  return compacted.first()->to_predicate(name);
344 
345  auto all_predicates = exprt::operandst{};
347  compacted.begin(),
348  compacted.end(),
349  std::back_inserter(all_predicates),
350  [&name](const abstract_object_pointert &value) {
351  return value->to_predicate(name);
352  });
353  std::sort(all_predicates.begin(), all_predicates.end());
354 
355  return or_exprt(all_predicates);
356 }
357 
359  std::ostream &out,
360  const ai_baset &ai,
361  const namespacet &ns) const
362 {
363  if(is_top())
364  {
365  out << "TOP";
366  }
367  else if(is_bottom())
368  {
369  out << "BOTTOM";
370  }
371  else
372  {
373  out << "value-set-begin: ";
374 
375  values.output(out, ai, ns);
376 
377  out << " :value-set-end";
378  }
379 }
380 
383 {
384  abstract_object_sett unwrapped_values;
385  for(auto const &value : values)
386  unwrapped_values.insert(maybe_extract_single_value(value));
387 
388  return unwrapped_values;
389 }
390 
393 {
394  auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
395  maybe_singleton->unwrap_context());
396  if(value_as_set)
397  {
398  PRECONDITION(value_as_set->get_values().size() == 1);
399  PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
400  value_as_set->get_values().first()));
401 
402  return value_as_set->get_values().first();
403  }
404  else
405  return maybe_singleton;
406 }
407 
408 static bool are_any_top(const abstract_object_sett &set)
409 {
410  return std::find_if(
411  set.begin(), set.end(), [](const abstract_object_pointert &value) {
412  return value->is_top();
413  }) != set.end();
414 }
415 
416 using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
418 {
419  return std::find_if(
420  set.begin(),
421  set.end(),
422  [&pred](const abstract_object_pointert &obj) {
423  const auto &value =
424  std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
425  return pred(*value);
426  }) != set.end();
427 }
428 
429 static bool set_has_extremes(
430  const abstract_object_sett &set,
431  set_predicate_fn lower_fn,
432  set_predicate_fn upper_fn)
433 {
434  bool has_lower = set_contains(set, lower_fn);
435  if(!has_lower)
436  return false;
437 
438  bool has_upper = set_contains(set, upper_fn);
439  return has_upper;
440 }
441 
442 static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
443 {
444  if(type.id() == ID_bool)
445  {
446  return set_has_extremes(
447  set,
448  [](const abstract_value_objectt &value) {
449  auto c = value.to_constant();
450  return c.is_false() || (c.id() == ID_min);
451  },
452  [](const abstract_value_objectt &value) {
453  auto c = value.to_constant();
454  return c.is_true() || (c.id() == ID_max);
455  });
456  }
457 
458  if(type.id() == ID_c_bool)
459  {
460  return set_has_extremes(
461  set,
462  [](const abstract_value_objectt &value) {
463  auto c = value.to_constant();
464  return c.is_zero() || (c.id() == ID_min);
465  },
466  [](const abstract_value_objectt &value) {
467  auto c = value.to_constant();
468  return c.is_one() || (c.id() == ID_max);
469  });
470  }
471 
472  return false;
473 }
474 
480 static bool value_is_not_contained_in(
481  const abstract_object_pointert &object,
482  const std::vector<constant_interval_exprt> &intervals);
483 
485 {
487  return values;
488 
489  auto compacted = non_destructive_compact(values);
490  if(compacted.size() <= value_set_abstract_objectt::max_value_set_size)
491  return compacted;
492 
493  compacted = destructive_compact(values);
494 
495  return compacted;
496 }
497 
498 static exprt eval_expr(const exprt &e);
499 static bool is_eq(const exprt &lhs, const exprt &rhs);
500 static bool is_le(const exprt &lhs, const exprt &rhs);
502  const abstract_object_sett &values,
503  const std::vector<constant_interval_exprt> &intervals);
504 static void
505 collapse_overlapping_intervals(std::vector<constant_interval_exprt> &intervals);
506 
507 static std::vector<constant_interval_exprt>
509 {
510  auto intervals = std::vector<constant_interval_exprt>{};
511  for(auto const &object : values)
512  {
513  auto value =
514  std::dynamic_pointer_cast<const abstract_value_objectt>(object);
515  auto as_expr = value->to_interval();
516  if(!as_expr.is_single_value_interval())
517  intervals.push_back(as_expr);
518  }
519 
521 
522  return intervals;
523 }
524 
526  std::vector<constant_interval_exprt> &intervals)
527 {
528  std::sort(
529  intervals.begin(),
530  intervals.end(),
531  [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
532  if(is_eq(lhs.get_lower(), rhs.get_lower()))
533  return is_le(lhs.get_upper(), rhs.get_upper());
534  return is_le(lhs.get_lower(), rhs.get_lower());
535  });
536 
537  size_t index = 1;
538  while(index < intervals.size())
539  {
540  auto &lhs = intervals[index - 1];
541  auto &rhs = intervals[index];
542 
543  bool overlap = is_le(rhs.get_lower(), lhs.get_upper());
544  if(overlap)
545  {
546  auto upper = is_le(lhs.get_upper(), rhs.get_upper()) ? rhs.get_upper()
547  : lhs.get_upper();
548  auto expanded = constant_interval_exprt(lhs.get_lower(), upper);
549  lhs = expanded;
550  intervals.erase(intervals.begin() + index);
551  }
552  else
553  ++index;
554  }
555 }
556 
559 {
560  auto intervals = collect_intervals(values);
561  if(intervals.empty())
562  return values;
563 
564  return collapse_values_in_intervals(values, intervals);
565 }
566 
568  const abstract_object_sett &values,
569  const std::vector<constant_interval_exprt> &intervals)
570 {
571  auto collapsed = abstract_object_sett{};
572  // for each value, including the intervals
573  // keep it if it is not in any of the intervals
574  std::copy_if(
575  values.begin(),
576  values.end(),
577  std::back_inserter(collapsed),
578  [&intervals](const abstract_object_pointert &object) {
579  return value_is_not_contained_in(object, intervals);
580  });
582  intervals.begin(),
583  intervals.end(),
584  std::back_inserter(collapsed),
585  [](const constant_interval_exprt &interval) {
586  return interval_abstract_valuet::make_interval(interval);
587  });
588  return collapsed;
589 }
590 
593 {
594  auto value_count = values.size();
595  auto width = values.to_interval();
596  auto slice_width = eval_expr(div_exprt(
597  minus_exprt(width.get_upper(), width.get_lower()),
598  from_integer(slice, width.type())));
599 
600  auto lower_boundary = eval_expr(plus_exprt(width.get_lower(), slice_width));
601  auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
602  if(
603  lower_boundary ==
604  upper_start) // adjust boundary so intervals aren't immediately combined
605  upper_start = eval_expr(
606  plus_exprt(upper_start, from_integer(1, lower_boundary.type())));
607 
608  auto lower_slice = constant_interval_exprt(width.get_lower(), lower_boundary);
609  auto upper_slice = constant_interval_exprt(upper_start, width.get_upper());
610 
611  values.insert(interval_abstract_valuet::make_interval(lower_slice));
612  values.insert(interval_abstract_valuet::make_interval(upper_slice));
613 
614  auto compacted = non_destructive_compact(values);
615  if(compacted.size() == value_count)
616  return destructive_compact(compacted, --slice);
617 
618  return compacted;
619 } // destructive_compact
620 
622  const abstract_object_pointert &object,
623  const std::vector<constant_interval_exprt> &intervals)
624 {
625  auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(object);
626  auto as_expr = value->to_interval();
627 
628  return std::none_of(
629  intervals.begin(),
630  intervals.end(),
631  [&as_expr](const constant_interval_exprt &interval) {
632  return interval.contains(as_expr);
633  });
634 }
635 
636 static exprt eval_expr(const exprt &e)
637 {
638  auto symbol_table = symbol_tablet{};
639  auto ns = namespacet{symbol_table};
640 
641  return simplify_expr(e, ns);
642 }
643 
644 static bool is_eq(const exprt &lhs, const exprt &rhs)
645 {
646  return constant_interval_exprt::equal(lhs, rhs);
647 }
648 
649 static bool is_le(const exprt &lhs, const exprt &rhs)
650 {
652 }
653 
655  const abstract_object_sett &values,
656  const constant_interval_exprt &lhs,
657  const constant_interval_exprt &rhs)
658 {
659  if(lhs.contains(rhs))
660  return values;
661 
662  auto widened_ends = std::vector<constant_interval_exprt>{};
663 
664  auto range = widened_ranget(lhs, rhs);
665 
666  // should extend lower bound?
667  if(range.is_lower_widened)
668  {
669  auto extended_lower_bound =
670  constant_interval_exprt(range.widened_lower_bound, range.lower_bound);
671 
672  widened_ends.push_back(extended_lower_bound);
673  for(auto &obj : values)
674  {
675  auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
676  auto as_expr = value->to_interval();
677  if(is_le(as_expr.get_lower(), range.lower_bound))
678  widened_ends.push_back(as_expr);
679  }
680  }
681  // should extend upper bound?
682  if(range.is_upper_widened)
683  {
684  auto extended_upper_bound =
685  constant_interval_exprt(range.upper_bound, range.widened_upper_bound);
686  widened_ends.push_back(extended_upper_bound);
687  for(auto &obj : values)
688  {
689  auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
690  auto as_expr = value->to_interval();
691  if(is_le(range.upper_bound, as_expr.get_upper()))
692  widened_ends.push_back(as_expr);
693  }
694  }
695 
696  collapse_overlapping_intervals(widened_ends);
697  return collapse_values_in_intervals(values, widened_ends);
698 }
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_implementation_ptrt make_indeterminate_index_range()
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:198
const_iterator begin() const
value_sett::size_type size() const
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void insert(const abstract_object_pointert &o)
value_sett::const_iterator const_iterator
abstract_object_pointert first() const
const_iterator end() const
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
Represents an interval of values.
Definition: interval.h:48
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:404
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
const exprt & get_lower() const
Definition: interval.cpp:29
const exprt & get_upper() const
Definition: interval.cpp:34
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:432
Division.
Definition: std_expr.h:1064
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
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
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
const irep_idt & id() const
Definition: irep.h:407
Binary minus.
Definition: std_expr.h:973
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean OR.
Definition: std_expr.h:2028
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:28
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
constant_interval_exprt to_interval() const override
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
value_range_implementation_ptrt value_range_implementation() const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
static abstract_object_pointert make_value_set(const abstract_object_sett &initial_values)
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
const exprt & current() const override
std::set< exprt >::const_iterator next
value_set_index_ranget(const std::set< exprt > &vals)
index_range_implementation_ptrt reset() const override
abstract_object_pointert cur
value_range_implementation_ptrt reset() const override
abstract_object_sett::const_iterator next
value_set_value_ranget(const abstract_object_sett &vals)
const abstract_object_pointert & current() const override
const abstract_object_sett & values
An abstraction of a single value that just stores a constant.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
An interval to represent a set of possible values.
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
static abstract_object_sett destructive_compact(abstract_object_sett values, int slice=3)
static exprt eval_expr(const exprt &e)
static abstract_object_sett collapse_values_in_intervals(const abstract_object_sett &values, const std::vector< constant_interval_exprt > &intervals)
static bool is_le(const exprt &lhs, const exprt &rhs)
static void collapse_overlapping_intervals(std::vector< constant_interval_exprt > &intervals)
static abstract_object_sett non_destructive_compact(const abstract_object_sett &values)
static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
static bool value_is_not_contained_in(const abstract_object_pointert &object, const std::vector< constant_interval_exprt > &intervals)
static bool is_eq(const exprt &lhs, const exprt &rhs)
static index_range_implementation_ptrt make_value_set_index_range(const std::set< exprt > &vals)
std::function< bool(const abstract_value_objectt &)> set_predicate_fn
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
static abstract_object_sett widen_value_set(const abstract_object_sett &values, const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static std::vector< constant_interval_exprt > collect_intervals(const abstract_object_sett &values)
static bool set_has_extremes(const abstract_object_sett &set, set_predicate_fn lower_fn, set_predicate_fn upper_fn)
static bool are_any_top(const abstract_object_sett &set)
static abstract_object_sett compact_values(const abstract_object_sett &values)
static value_range_implementation_ptrt make_value_set_value_range(const abstract_object_sett &vals)
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
static bool set_contains(const abstract_object_sett &set, set_predicate_fn pred)
Value Set Abstract Object.