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
12#include <util/arith_tools.h>
13#include <util/make_unique.h>
14#include <util/simplify_expr.h>
15
21
22#include "context_abstract_object.h" // IWYU pragma: keep
23
24#include <algorithm>
25
27make_value_set_index_range(const std::set<exprt> &vals);
28
30{
31public:
32 explicit value_set_index_ranget(const std::set<exprt> &vals)
33 : values(vals), cur(), next(values.begin())
34 {
35 PRECONDITION(!values.empty());
36 }
37
38 const exprt &current() const override
39 {
40 return cur;
41 }
42 bool advance_to_next() override
43 {
44 if(next == values.end())
45 return false;
46
47 cur = *next;
48 ++next;
49 return true;
50 }
55
56private:
57 std::set<exprt> values;
59 std::set<exprt>::const_iterator next;
60};
61
63make_value_set_index_range(const std::set<exprt> &vals)
64{
66}
67
70
72{
73public:
75 : values(vals), cur(), next(values.begin())
76 {
78 }
79
80 const abstract_object_pointert &current() const override
81 {
82 return cur;
83 }
84 bool advance_to_next() override
85 {
86 if(next == values.end())
87 return false;
88
89 cur = *next;
90 ++next;
91 return true;
92 }
97
98private:
102};
103
109
112
118
119static bool are_any_top(const abstract_object_sett &set);
120static bool is_set_extreme(const typet &type, const abstract_object_sett &set);
121
126 const abstract_object_sett &values,
127 const constant_interval_exprt &lhs,
128 const constant_interval_exprt &rhs);
129
131 const typet &type,
132 bool top,
133 bool bottom)
134 : abstract_value_objectt(type, top, bottom)
135{
136 values.insert(std::make_shared<constant_abstract_valuet>(type, top, bottom));
137 verify();
138}
139
141 const exprt &expr,
142 const abstract_environmentt &environment,
143 const namespacet &ns)
144 : abstract_value_objectt(expr.type(), false, false)
145{
147 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
148 verify();
149}
150
152 const abstract_object_sett &initial_values)
153{
154 PRECONDITION(!initial_values.empty());
155
156 auto values = unwrap_and_extract_values(initial_values);
157
159
160 const auto &type = values.first()->type();
161 auto value_set =
162 std::make_shared<value_set_abstract_objectt>(type, false, false);
163 value_set->set_values(values);
164 return value_set;
165}
166
169 const namespacet &ns) const
170{
171 if(values.empty())
173
174 std::set<exprt> flattened;
175 for(const auto &o : values)
176 {
177 const auto &v = as_value(o);
178 for(auto e : v->index_range(ns))
179 flattened.insert(e);
180 }
181
182 return make_value_set_index_range(flattened);
183}
184
190
192{
193 verify();
194
195 if(values.size() == 1)
196 return values.first()->to_constant();
197
198 auto interval = to_interval();
199 if(interval.is_single_value_interval())
200 return interval.get_lower();
201
203}
204
209
211 const abstract_value_pointert &other,
212 const widen_modet &widen_mode) const
213{
214 auto union_values = !is_bottom() ? values : abstract_object_sett{};
215
216 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
217 if(other_value_set)
218 union_values.insert(other_value_set->get_values());
219 else
220 union_values.insert(other);
221
222 auto has_values = [](const abstract_object_pointert &v) {
223 return !v->is_top() && !v->is_bottom();
224 };
225
226 if(
227 widen_mode == widen_modet::could_widen && has_values(shared_from_this()) &&
228 has_values(other))
229 {
230 union_values =
231 widen_value_set(union_values, to_interval(), other->to_interval());
232 }
233
234 return resolve_values(union_values);
235}
236
238 const abstract_value_pointert &other) const
239{
240 if(other->is_bottom())
241 return shared_from_this();
242
243 auto meet_values = abstract_object_sett{};
244
245 if(is_bottom())
246 meet_values.insert(other);
247 else
248 {
249 auto this_interval = to_interval();
250 auto other_interval = other->to_interval();
251
252 auto lower_bound = constant_interval_exprt::get_max(
253 this_interval.get_lower(), other_interval.get_lower());
254 auto upper_bound = constant_interval_exprt::get_min(
255 this_interval.get_upper(), other_interval.get_upper());
256
257 // if the interval is valid, we have a meet!
258 if(constant_interval_exprt::less_than_or_equal(lower_bound, upper_bound))
259 {
260 auto meet_interval = constant_interval_exprt(lower_bound, upper_bound);
261 abstract_object_pointert meet_value =
262 std::make_shared<interval_abstract_valuet>(meet_interval);
263 if(meet_interval.is_single_value_interval())
264 meet_value = std::make_shared<constant_abstract_valuet>(lower_bound);
265 meet_values.insert(meet_value);
266 }
267 }
268
269 if(meet_values.empty()) // no meet :(
270 return std::make_shared<value_set_abstract_objectt>(type(), false, true);
271
272 return resolve_values(meet_values);
273}
274
276 const abstract_object_sett &new_values) const
277{
278 PRECONDITION(!new_values.empty());
279
280 if(new_values == values)
281 return shared_from_this();
282
283 return make_value_set(new_values);
284}
285
287{
288 values.clear();
290 std::make_shared<constant_abstract_valuet>(type(), true, false));
291}
292
294 const abstract_object_sett &other_values)
295{
296 PRECONDITION(!other_values.empty());
297 if(are_any_top(other_values) || is_set_extreme(type(), other_values))
298 {
299 set_top();
300 }
301 else
302 {
303 set_not_top();
304 values = other_values;
305 }
307 verify();
308}
309
311 const exprt &lower,
312 const exprt &upper) const
313{
314 using cie = constant_interval_exprt;
315
316 auto constrained_values = abstract_object_sett{};
317
318 for(auto const &value : unwrap_and_extract_values(values))
319 {
320 auto constrained = as_value(value)->constrain(lower, upper);
321 auto constrained_interval = constrained->to_interval();
322
323 if(cie::less_than(constrained_interval.get_lower(), lower))
324 continue;
325 if(cie::greater_than(constrained_interval.get_upper(), upper))
326 continue;
327
328 constrained_values.insert(constrained);
329 }
330
331 return as_value(resolve_values(constrained_values));
332}
333
335{
336 auto compacted = non_destructive_compact(values);
337 if(compacted.size() == 1)
338 return compacted.first()->to_predicate(name);
339
340 auto all_predicates = exprt::operandst{};
341 std::transform(
342 compacted.begin(),
343 compacted.end(),
344 std::back_inserter(all_predicates),
345 [&name](const abstract_object_pointert &value) {
346 return value->to_predicate(name);
347 });
348 std::sort(all_predicates.begin(), all_predicates.end());
349
350 return or_exprt(all_predicates);
351}
352
354 std::ostream &out,
355 const ai_baset &ai,
356 const namespacet &ns) const
357{
358 if(is_top())
359 {
360 out << "TOP";
361 }
362 else if(is_bottom())
363 {
364 out << "BOTTOM";
365 }
366 else
367 {
368 out << "value-set-begin: ";
369
370 values.output(out, ai, ns);
371
372 out << " :value-set-end";
373 }
374}
375
378{
379 abstract_object_sett unwrapped_values;
380 for(auto const &value : values)
381 unwrapped_values.insert(maybe_extract_single_value(value));
382
383 return unwrapped_values;
384}
385
388{
389 auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
390 maybe_singleton->unwrap_context());
391 if(value_as_set)
392 {
393 PRECONDITION(value_as_set->get_values().size() == 1);
394 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
395 value_as_set->get_values().first()));
396
397 return value_as_set->get_values().first();
398 }
399 else
400 return maybe_singleton;
401}
402
403static bool are_any_top(const abstract_object_sett &set)
404{
405 return std::find_if(
406 set.begin(), set.end(), [](const abstract_object_pointert &value) {
407 return value->is_top();
408 }) != set.end();
409}
410
411using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
413{
414 return std::find_if(
415 set.begin(),
416 set.end(),
417 [&pred](const abstract_object_pointert &obj) {
418 const auto &value =
419 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
420 return pred(*value);
421 }) != set.end();
422}
423
425 const abstract_object_sett &set,
426 set_predicate_fn lower_fn,
427 set_predicate_fn upper_fn)
428{
429 bool has_lower = set_contains(set, lower_fn);
430 if(!has_lower)
431 return false;
432
433 bool has_upper = set_contains(set, upper_fn);
434 return has_upper;
435}
436
437static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
438{
439 if(type.id() == ID_bool)
440 {
441 return set_has_extremes(
442 set,
443 [](const abstract_value_objectt &value) {
444 auto c = value.to_constant();
445 return c.is_false() || (c.id() == ID_min_value);
446 },
447 [](const abstract_value_objectt &value) {
448 auto c = value.to_constant();
449 return c.is_true() || (c.id() == ID_max_value);
450 });
451 }
452
453 if(type.id() == ID_c_bool)
454 {
455 return set_has_extremes(
456 set,
457 [](const abstract_value_objectt &value) {
458 auto c = value.to_constant();
459 return c.is_zero() || (c.id() == ID_min_value);
460 },
461 [](const abstract_value_objectt &value) {
462 auto c = value.to_constant();
463 return c.is_one() || (c.id() == ID_max_value);
464 });
465 }
466
467 return false;
468}
469
475static bool value_is_not_contained_in(
476 const abstract_object_pointert &object,
477 const std::vector<constant_interval_exprt> &intervals);
478
480{
482 return values;
483
484 auto compacted = non_destructive_compact(values);
486 return compacted;
487
488 compacted = destructive_compact(values);
489
490 return compacted;
491}
492
493static exprt eval_expr(const exprt &e);
494static bool is_eq(const exprt &lhs, const exprt &rhs);
495static bool is_le(const exprt &lhs, const exprt &rhs);
496static bool is_lt(const exprt &lhs, const exprt &rhs);
498 const abstract_object_sett &values,
499 const std::vector<constant_interval_exprt> &intervals);
500static void
501collapse_overlapping_intervals(std::vector<constant_interval_exprt> &intervals);
502
503static std::vector<constant_interval_exprt>
505{
506 auto intervals = std::vector<constant_interval_exprt>{};
507 for(auto const &object : values)
508 {
509 auto value =
510 std::dynamic_pointer_cast<const abstract_value_objectt>(object);
511 auto as_expr = value->to_interval();
512 if(!as_expr.is_single_value_interval())
513 intervals.push_back(as_expr);
514 }
515
517
518 return intervals;
519}
520
522 std::vector<constant_interval_exprt> &intervals)
523{
524 std::sort(
525 intervals.begin(),
526 intervals.end(),
527 [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
528 if(is_eq(lhs.get_lower(), rhs.get_lower()))
529 return is_lt(lhs.get_upper(), rhs.get_upper());
530 return is_lt(lhs.get_lower(), rhs.get_lower());
531 });
532
533 size_t index = 1;
534 while(index < intervals.size())
535 {
536 auto &lhs = intervals[index - 1];
537 auto &rhs = intervals[index];
538
539 bool overlap = is_le(rhs.get_lower(), lhs.get_upper());
540 if(overlap)
541 {
542 auto upper = is_le(lhs.get_upper(), rhs.get_upper()) ? rhs.get_upper()
543 : lhs.get_upper();
544 auto expanded = constant_interval_exprt(lhs.get_lower(), upper);
545 lhs = expanded;
546 intervals.erase(intervals.begin() + index);
547 }
548 else
549 ++index;
550 }
551}
552
555{
556 auto intervals = collect_intervals(values);
557 if(intervals.empty())
558 return values;
559
560 return collapse_values_in_intervals(values, intervals);
561}
562
564 const abstract_object_sett &values,
565 const std::vector<constant_interval_exprt> &intervals)
566{
567 auto collapsed = abstract_object_sett{};
568 // for each value, including the intervals
569 // keep it if it is not in any of the intervals
570 std::copy_if(
571 values.begin(),
572 values.end(),
573 std::back_inserter(collapsed),
574 [&intervals](const abstract_object_pointert &object) {
575 return value_is_not_contained_in(object, intervals);
576 });
577 std::transform(
578 intervals.begin(),
579 intervals.end(),
580 std::back_inserter(collapsed),
581 [](const constant_interval_exprt &interval) {
582 return interval_abstract_valuet::make_interval(interval);
583 });
584 return collapsed;
585}
586
589{
590 auto value_count = values.size();
591 auto width = values.to_interval();
592 auto slice_width = eval_expr(div_exprt(
593 minus_exprt(width.get_upper(), width.get_lower()),
594 from_integer(slice, width.type())));
595
596 auto lower_boundary = eval_expr(plus_exprt(width.get_lower(), slice_width));
597 auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
598 if(
599 lower_boundary ==
600 upper_start) // adjust boundary so intervals aren't immediately combined
601 upper_start = eval_expr(
602 plus_exprt(upper_start, from_integer(1, lower_boundary.type())));
603
604 auto lower_slice = constant_interval_exprt(width.get_lower(), lower_boundary);
605 auto upper_slice = constant_interval_exprt(upper_start, width.get_upper());
606
609
610 auto compacted = non_destructive_compact(values);
611 if(compacted.size() == value_count)
612 return destructive_compact(compacted, --slice);
613
614 return compacted;
615} // destructive_compact
616
618 const abstract_object_pointert &object,
619 const std::vector<constant_interval_exprt> &intervals)
620{
621 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(object);
622 auto as_expr = value->to_interval();
623
624 return std::none_of(
625 intervals.begin(),
626 intervals.end(),
627 [&as_expr](const constant_interval_exprt &interval) {
628 return interval.contains(as_expr);
629 });
630}
631
632static exprt eval_expr(const exprt &e)
633{
634 auto symbol_table = symbol_tablet{};
635 auto ns = namespacet{symbol_table};
636
637 return simplify_expr(e, ns);
638}
639
640static bool is_eq(const exprt &lhs, const exprt &rhs)
641{
642 return constant_interval_exprt::equal(lhs, rhs);
643}
644
645static bool is_le(const exprt &lhs, const exprt &rhs)
646{
648}
649
650static bool is_lt(const exprt &lhs, const exprt &rhs)
651{
652 return constant_interval_exprt::less_than(lhs, rhs);
653}
654
656 const abstract_object_sett &values,
657 const constant_interval_exprt &lhs,
658 const constant_interval_exprt &rhs)
659{
660 if(lhs.contains(rhs))
661 return values;
662
663 auto widened_ends = std::vector<constant_interval_exprt>{};
664
665 auto range = widened_ranget(lhs, rhs);
666
667 // should extend lower bound?
668 if(range.is_lower_widened)
669 {
670 auto extended_lower_bound =
671 constant_interval_exprt(range.widened_lower_bound, range.lower_bound);
672
673 widened_ends.push_back(extended_lower_bound);
674 for(auto &obj : values)
675 {
676 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
677 auto as_expr = value->to_interval();
678 if(is_le(as_expr.get_lower(), range.lower_bound))
679 widened_ends.push_back(as_expr);
680 }
681 }
682 // should extend upper bound?
683 if(range.is_upper_widened)
684 {
685 auto extended_upper_bound =
686 constant_interval_exprt(range.upper_bound, range.widened_upper_bound);
687 widened_ends.push_back(extended_upper_bound);
688 for(auto &obj : values)
689 {
690 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
691 auto as_expr = value->to_interval();
692 if(is_le(range.upper_bound, as_expr.get_upper()))
693 widened_ends.push_back(as_expr);
694 }
695 }
696
697 collapse_overlapping_intervals(widened_ends);
698 return collapse_values_in_intervals(values, widened_ends);
699}
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:118
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:1097
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition expr.cpp:96
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
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:1006
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:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
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
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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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.