58 std::set<exprt>::const_iterator
next;
64 return util_make_unique<value_set_index_ranget>(vals);
106 return util_make_unique<value_set_value_ranget>(vals);
153 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
168 std::make_shared<value_set_abstract_objectt>(
type,
false,
false);
169 value_set->set_values(
values);
180 std::set<exprt> flattened;
181 for(
const auto &o :
values)
184 for(
auto e : v->index_range(ns))
205 if(interval.is_single_value_interval())
206 return interval.get_lower();
222 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
224 union_values.insert(other_value_set->get_values());
226 union_values.insert(other);
229 return !v->is_top() && !v->is_bottom();
246 if(other->is_bottom())
247 return shared_from_this();
252 meet_values.
insert(other);
256 auto other_interval = other->to_interval();
259 this_interval.get_lower(), other_interval.get_lower());
261 this_interval.get_upper(), other_interval.get_upper());
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);
275 if(meet_values.empty())
276 return std::make_shared<value_set_abstract_objectt>(
type(),
false,
true);
287 return shared_from_this();
317 const exprt &upper)
const
325 auto constrained =
as_value(value)->constrain(lower, upper);
326 auto constrained_interval = constrained->to_interval();
333 constrained_values.insert(constrained);
342 if(compacted.size() == 1)
343 return compacted.first()->to_predicate(name);
349 std::back_inserter(all_predicates),
351 return value->to_predicate(name);
353 std::sort(all_predicates.begin(), all_predicates.end());
373 out <<
"value-set-begin: ";
377 out <<
" :value-set-end";
385 for(
auto const &value : values)
388 return unwrapped_values;
394 auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
395 maybe_singleton->unwrap_context());
399 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
400 value_as_set->get_values().first()));
402 return value_as_set->get_values().first();
405 return maybe_singleton;
412 return value->is_top();
424 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
444 if(type.
id() == ID_bool)
450 return c.
is_false() || (c.id() == ID_min);
454 return c.
is_true() || (c.id() == ID_max);
458 if(type.
id() == ID_c_bool)
464 return c.
is_zero() || (c.id() == ID_min);
468 return c.
is_one() || (c.id() == ID_max);
482 const std::vector<constant_interval_exprt> &intervals);
503 const std::vector<constant_interval_exprt> &intervals);
507 static std::vector<constant_interval_exprt>
510 auto intervals = std::vector<constant_interval_exprt>{};
511 for(
auto const &
object : values)
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);
526 std::vector<constant_interval_exprt> &intervals)
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());
538 while(index < intervals.size())
540 auto &lhs = intervals[index - 1];
541 auto &rhs = intervals[index];
550 intervals.erase(intervals.begin() + index);
561 if(intervals.empty())
569 const std::vector<constant_interval_exprt> &intervals)
577 std::back_inserter(collapsed),
579 return value_is_not_contained_in(object, intervals);
584 std::back_inserter(collapsed),
586 return interval_abstract_valuet::make_interval(interval);
594 auto value_count = values.
size();
615 if(compacted.size() == value_count)
623 const std::vector<constant_interval_exprt> &intervals)
625 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(
object);
626 auto as_expr = value->to_interval();
632 return interval.contains(as_expr);
662 auto widened_ends = std::vector<constant_interval_exprt>{};
667 if(range.is_lower_widened)
669 auto extended_lower_bound =
672 widened_ends.push_back(extended_lower_bound);
673 for(
auto &obj : values)
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);
682 if(range.is_upper_widened)
684 auto extended_upper_bound =
686 widened_ends.push_back(extended_upper_bound);
687 for(
auto &obj : values)
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);
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
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
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...
Represents an interval of values.
tvt less_than_or_equal(const constant_interval_exprt &o) const
bool contains(const constant_interval_exprt &interval) const
static exprt get_max(const exprt &a, const exprt &b)
static exprt get_min(const exprt &a, const exprt &b)
const exprt & get_lower() const
const exprt & get_upper() const
tvt equal(const constant_interval_exprt &o) const
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
The type of an expression, extends irept.
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_object_sett values
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
void set_top_internal() 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
value_set_abstract_objectt(const typet &type)
exprt to_constant() const override
Converts to a constant expression if possible.
const exprt & current() const override
std::set< exprt >::const_iterator next
bool advance_to_next() override
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
bool advance_to_next() override
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)
binary_relation_exprt less_than(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
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.