cprover
Loading...
Searching...
No Matches
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
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
66
69
71{
72public:
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 }
96
97private:
101};
102
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
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{
153 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
154 verify();
155}
156
159{
161
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
189}
190
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
215
217 const abstract_value_pointert &other,
218 const widen_modet &widen_mode) const
219{
221
222 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
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(
234 has_values(other))
235 {
237 widen_value_set(union_values, to_interval(), other->to_interval());
238 }
239
241}
242
244 const abstract_value_pointert &other) const
245{
246 if(other->is_bottom())
247 return shared_from_this();
248
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);
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
279}
280
291
293{
294 values.clear();
295 values.insert(std::make_shared<constant_abstract_valuet>(type()));
296}
297
300{
301 PRECONDITION(!other_values.empty());
303 {
304 set_top();
305 }
306 else
307 {
308 set_not_top();
310 }
312 verify();
313}
314
316 const exprt &lower,
317 const exprt &upper) const
318{
320
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
334 }
335
337}
338
340{
342 if(compacted.size() == 1)
343 return compacted.first()->to_predicate(name);
344
346 std::transform(
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{
385 for(auto const &value : values)
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
408static 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
416using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
418{
419 return std::find_if(
420 set.begin(),
421 set.end(),
423 const auto &value =
424 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
425 return pred(*value);
426 }) != set.end();
427}
428
430 const abstract_object_sett &set,
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
442static 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
480static 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);
491 return compacted;
492
494
495 return compacted;
496}
497
498static exprt eval_expr(const exprt &e);
499static bool is_eq(const exprt &lhs, const exprt &rhs);
500static bool is_le(const exprt &lhs, const exprt &rhs);
502 const abstract_object_sett &values,
503 const std::vector<constant_interval_exprt> &intervals);
504static void
505collapse_overlapping_intervals(std::vector<constant_interval_exprt> &intervals);
506
507static 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{
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 });
581 std::transform(
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();
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(
604 upper_start) // adjust boundary so intervals aren't immediately combined
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
613
614 auto compacted = non_destructive_compact(values);
615 if(compacted.size() == value_count)
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
636static 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
644static bool is_eq(const exprt &lhs, const exprt &rhs)
645{
646 return constant_interval_exprt::equal(lhs, rhs);
647}
648
649static 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 {
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:199
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
const irep_idt & id() const
Definition irep.h:396
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:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
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
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.
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 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.