CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
12#include <util/arith_tools.h>
13#include <util/simplify_expr.h>
14
20
21#include "context_abstract_object.h" // IWYU pragma: keep
22
23#include <algorithm>
24
26make_value_set_index_range(const std::set<exprt> &vals);
27
29{
30public:
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 }
54
55private:
56 std::set<exprt> values;
58 std::set<exprt>::const_iterator next;
59};
60
62make_value_set_index_range(const std::set<exprt> &vals)
63{
64 return std::make_unique<value_set_index_ranget>(vals);
65}
66
69
71{
72public:
74 : values(vals), cur(), next(values.begin())
75 {
76 PRECONDITION(!values.empty());
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 }
96
97private:
101};
102
105{
106 return std::make_unique<value_set_value_ranget>(vals);
107}
108
111
117
118static bool are_any_top(const abstract_object_sett &set);
119static 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 const typet &type,
131 bool top,
132 bool bottom)
133 : abstract_value_objectt(type, top, bottom)
134{
135 values.insert(std::make_shared<constant_abstract_valuet>(type, top, bottom));
136 verify();
137}
138
140 const exprt &expr,
141 const abstract_environmentt &environment,
142 const namespacet &ns)
143 : abstract_value_objectt(expr.type(), false, false)
144{
146 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
147 verify();
148}
149
152{
154
156
158
159 const auto &type = values.first()->type();
160 auto value_set =
161 std::make_shared<value_set_abstract_objectt>(type, false, false);
162 value_set->set_values(values);
163 return value_set;
164}
165
168 const namespacet &ns) const
169{
170 if(values.empty())
172
173 std::set<exprt> flattened;
174 for(const auto &o : values)
175 {
176 const auto &v = as_value(o);
177 for(auto e : v->index_range(ns))
178 flattened.insert(e);
179 }
180
182}
183
189
191{
192 verify();
193
194 if(values.size() == 1)
195 return values.first()->to_constant();
196
197 auto interval = to_interval();
198 if(interval.is_single_value_interval())
199 return interval.get_lower();
200
202}
203
208
210 const abstract_value_pointert &other,
211 const widen_modet &widen_mode) const
212{
214
215 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
217 union_values.insert(other_value_set->get_values());
218 else
219 union_values.insert(other);
220
221 auto has_values = [](const abstract_object_pointert &v) {
222 return !v->is_top() && !v->is_bottom();
223 };
224
225 if(
227 has_values(other))
228 {
230 widen_value_set(union_values, to_interval(), other->to_interval());
231 }
232
234}
235
237 const abstract_value_pointert &other) const
238{
239 if(other->is_bottom())
240 return shared_from_this();
241
243
244 if(is_bottom())
245 meet_values.insert(other);
246 else
247 {
248 auto this_interval = to_interval();
249 auto other_interval = other->to_interval();
250
251 auto lower_bound = constant_interval_exprt::get_max(
252 this_interval.get_lower(), other_interval.get_lower());
253 auto upper_bound = constant_interval_exprt::get_min(
254 this_interval.get_upper(), other_interval.get_upper());
255
256 // if the interval is valid, we have a meet!
257 if(constant_interval_exprt::less_than_or_equal(lower_bound, upper_bound))
258 {
259 auto meet_interval = constant_interval_exprt(lower_bound, upper_bound);
261 std::make_shared<interval_abstract_valuet>(meet_interval);
262 if(meet_interval.is_single_value_interval())
263 meet_value = std::make_shared<constant_abstract_valuet>(lower_bound);
264 meet_values.insert(meet_value);
265 }
266 }
267
268 if(meet_values.empty()) // no meet :(
269 return std::make_shared<value_set_abstract_objectt>(type(), false, true);
270
272}
273
284
286{
287 values.clear();
289 std::make_shared<constant_abstract_valuet>(type(), true, false));
290}
291
294{
295 PRECONDITION(!other_values.empty());
297 {
298 set_top();
299 }
300 else
301 {
302 set_not_top();
304 }
306 verify();
307}
308
310 const exprt &lower,
311 const exprt &upper) const
312{
314
316
317 for(auto const &value : unwrap_and_extract_values(values))
318 {
319 auto constrained = as_value(value)->constrain(lower, upper);
320 auto constrained_interval = constrained->to_interval();
321
322 if(cie::less_than(constrained_interval.get_lower(), lower))
323 continue;
324 if(cie::greater_than(constrained_interval.get_upper(), upper))
325 continue;
326
328 }
329
331}
332
334{
336 if(compacted.size() == 1)
337 return compacted.first()->to_predicate(name);
338
340 std::transform(
341 compacted.begin(),
342 compacted.end(),
343 std::back_inserter(all_predicates),
344 [&name](const abstract_object_pointert &value) {
345 return value->to_predicate(name);
346 });
347 std::sort(all_predicates.begin(), all_predicates.end());
348
349 return or_exprt(all_predicates);
350}
351
353 std::ostream &out,
354 const ai_baset &ai,
355 const namespacet &ns) const
356{
357 if(is_top())
358 {
359 out << "TOP";
360 }
361 else if(is_bottom())
362 {
363 out << "BOTTOM";
364 }
365 else
366 {
367 out << "value-set-begin: ";
368
369 values.output(out, ai, ns);
370
371 out << " :value-set-end";
372 }
373}
374
377{
379 for(auto const &value : values)
381
382 return unwrapped_values;
383}
384
387{
388 auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
389 maybe_singleton->unwrap_context());
390 if(value_as_set)
391 {
392 PRECONDITION(value_as_set->get_values().size() == 1);
393 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
394 value_as_set->get_values().first()));
395
396 return value_as_set->get_values().first();
397 }
398 else
399 return maybe_singleton;
400}
401
402static bool are_any_top(const abstract_object_sett &set)
403{
404 return std::find_if(
405 set.begin(), set.end(), [](const abstract_object_pointert &value) {
406 return value->is_top();
407 }) != set.end();
408}
409
410using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
412{
413 return std::find_if(
414 set.begin(),
415 set.end(),
417 const auto &value =
418 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
419 return pred(*value);
420 }) != set.end();
421}
422
424 const abstract_object_sett &set,
427{
428 bool has_lower = set_contains(set, lower_fn);
429 if(!has_lower)
430 return false;
431
432 bool has_upper = set_contains(set, upper_fn);
433 return has_upper;
434}
435
436static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
437{
438 if(type.id() == ID_bool)
439 {
440 return set_has_extremes(
441 set,
442 [](const abstract_value_objectt &value) {
443 auto c = value.to_constant();
444 return c.is_false() || (c.id() == ID_min_value);
445 },
446 [](const abstract_value_objectt &value) {
447 auto c = value.to_constant();
448 return c.is_true() || (c.id() == ID_max_value);
449 });
450 }
451
452 if(type.id() == ID_c_bool)
453 {
454 return set_has_extremes(
455 set,
456 [](const abstract_value_objectt &value) {
457 auto c = value.to_constant();
458 return c.is_zero() || (c.id() == ID_min_value);
459 },
460 [](const abstract_value_objectt &value) {
461 auto c = value.to_constant();
462 return c.is_one() || (c.id() == ID_max_value);
463 });
464 }
465
466 return false;
467}
468
474static bool value_is_not_contained_in(
475 const abstract_object_pointert &object,
476 const std::vector<constant_interval_exprt> &intervals);
477
479{
481 return values;
482
483 auto compacted = non_destructive_compact(values);
485 return compacted;
486
488
489 return compacted;
490}
491
492static exprt eval_expr(const exprt &e);
493static bool is_eq(const exprt &lhs, const exprt &rhs);
494static bool is_le(const exprt &lhs, const exprt &rhs);
495static bool is_lt(const exprt &lhs, const exprt &rhs);
497 const abstract_object_sett &values,
498 const std::vector<constant_interval_exprt> &intervals);
499static void
500collapse_overlapping_intervals(std::vector<constant_interval_exprt> &intervals);
501
502static std::vector<constant_interval_exprt>
504{
505 auto intervals = std::vector<constant_interval_exprt>{};
506 for(auto const &object : values)
507 {
508 auto value =
509 std::dynamic_pointer_cast<const abstract_value_objectt>(object);
510 auto as_expr = value->to_interval();
511 if(!as_expr.is_single_value_interval())
512 intervals.push_back(as_expr);
513 }
514
516
517 return intervals;
518}
519
521 std::vector<constant_interval_exprt> &intervals)
522{
523 std::sort(
524 intervals.begin(),
525 intervals.end(),
526 [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
527 if(is_eq(lhs.get_lower(), rhs.get_lower()))
528 return is_lt(lhs.get_upper(), rhs.get_upper());
529 return is_lt(lhs.get_lower(), rhs.get_lower());
530 });
531
532 size_t index = 1;
533 while(index < intervals.size())
534 {
535 auto &lhs = intervals[index - 1];
536 auto &rhs = intervals[index];
537
538 bool overlap = is_le(rhs.get_lower(), lhs.get_upper());
539 if(overlap)
540 {
541 auto upper = is_le(lhs.get_upper(), rhs.get_upper()) ? rhs.get_upper()
542 : lhs.get_upper();
543 auto expanded = constant_interval_exprt(lhs.get_lower(), upper);
544 lhs = expanded;
545 intervals.erase(intervals.begin() + index);
546 }
547 else
548 ++index;
549 }
550}
551
554{
555 auto intervals = collect_intervals(values);
556 if(intervals.empty())
557 return values;
558
559 return collapse_values_in_intervals(values, intervals);
560}
561
563 const abstract_object_sett &values,
564 const std::vector<constant_interval_exprt> &intervals)
565{
567 // for each value, including the intervals
568 // keep it if it is not in any of the intervals
569 std::copy_if(
570 values.begin(),
571 values.end(),
572 std::back_inserter(collapsed),
573 [&intervals](const abstract_object_pointert &object) {
574 return value_is_not_contained_in(object, intervals);
575 });
576 std::transform(
577 intervals.begin(),
578 intervals.end(),
579 std::back_inserter(collapsed),
581 return interval_abstract_valuet::make_interval(interval);
582 });
583 return collapsed;
584}
585
588{
589 auto value_count = values.size();
590 auto width = values.to_interval();
592 minus_exprt(width.get_upper(), width.get_lower()),
593 from_integer(slice, width.type())));
594
595 auto lower_boundary = eval_expr(plus_exprt(width.get_lower(), slice_width));
596 auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
597 if(
599 upper_start) // adjust boundary so intervals aren't immediately combined
602
603 auto lower_slice = constant_interval_exprt(width.get_lower(), lower_boundary);
604 auto upper_slice = constant_interval_exprt(upper_start, width.get_upper());
605
608
609 auto compacted = non_destructive_compact(values);
610 if(compacted.size() == value_count)
612
613 return compacted;
614} // destructive_compact
615
617 const abstract_object_pointert &object,
618 const std::vector<constant_interval_exprt> &intervals)
619{
620 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(object);
621 auto as_expr = value->to_interval();
622
623 return std::none_of(
624 intervals.begin(),
625 intervals.end(),
626 [&as_expr](const constant_interval_exprt &interval) {
627 return interval.contains(as_expr);
628 });
629}
630
631static exprt eval_expr(const exprt &e)
632{
633 auto symbol_table = symbol_tablet{};
634 auto ns = namespacet{symbol_table};
635
636 return simplify_expr(e, ns);
637}
638
639static bool is_eq(const exprt &lhs, const exprt &rhs)
640{
641 return constant_interval_exprt::equal(lhs, rhs);
642}
643
644static bool is_le(const exprt &lhs, const exprt &rhs)
645{
647}
648
649static bool is_lt(const exprt &lhs, const exprt &rhs)
650{
651 return constant_interval_exprt::less_than(lhs, rhs);
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 {
670 constant_interval_exprt(range.widened_lower_bound, range.lower_bound);
671
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 {
685 constant_interval_exprt(range.upper_bound, range.widened_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
698}
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_implementation_ptrt make_indeterminate_index_range()
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)
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:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Represents an interval of values.
Definition interval.h:52
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition interval.cpp:403
bool contains(const constant_interval_exprt &interval) const
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:960
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:965
const exprt & get_lower() const
Definition interval.cpp:27
tvt less_than(const constant_interval_exprt &o) const
Definition interval.cpp:376
const exprt & get_upper() const
Definition interval.cpp:32
tvt equal(const constant_interval_exprt &o) const
Definition interval.cpp:431
Division.
Definition std_expr.h:1157
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
const irep_idt & id() const
Definition irep.h:388
Binary minus.
Definition std_expr.h:1061
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:2270
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
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
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
value_set_abstract_objectt(const typet &type, bool top, bool bottom)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
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.
std::set< exprt >::const_iterator next
const exprt & current() const override
value_set_index_ranget(const std::set< exprt > &vals)
index_range_implementation_ptrt reset() const override
const abstract_object_pointert & current() const override
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_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
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 bool is_lt(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 bool set_has_extremes(const abstract_object_sett &set, set_predicate_fn lower_fn, set_predicate_fn upper_fn)
static std::vector< constant_interval_exprt > collect_intervals(const abstract_object_sett &values)
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.