58 std::set<exprt>::const_iterator
next;
64 return std::make_unique<value_set_index_ranget>(
vals);
106 return std::make_unique<value_set_value_ranget>(
vals);
146 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
161 std::make_shared<value_set_abstract_objectt>(
type,
false,
false);
162 value_set->set_values(
values);
174 for(
const auto &o :
values)
177 for(
auto e : v->index_range(ns))
198 if(
interval.is_single_value_interval())
215 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
222 return !v->is_top() && !v->is_bottom();
239 if(other->is_bottom())
263 meet_value = std::make_shared<constant_abstract_valuet>(lower_bound);
269 return std::make_shared<value_set_abstract_objectt>(
type(),
false,
true);
289 std::make_shared<constant_abstract_valuet>(
type(),
true,
false));
311 const exprt &upper)
const
337 return compacted.first()->to_predicate(name);
345 return value->to_predicate(name);
367 out <<
"value-set-begin: ";
371 out <<
" :value-set-end";
379 for(
auto const &value : values)
388 auto const &
value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
393 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
406 return value->is_top();
418 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
476 const std::vector<constant_interval_exprt> &intervals);
498 const std::vector<constant_interval_exprt> &intervals);
502static std::vector<constant_interval_exprt>
505 auto intervals = std::vector<constant_interval_exprt>{};
506 for(
auto const &
object : values)
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);
521 std::vector<constant_interval_exprt> &intervals)
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());
533 while(index < intervals.size())
535 auto &lhs = intervals[index - 1];
536 auto &rhs = intervals[index];
545 intervals.erase(intervals.begin() + index);
556 if(intervals.empty())
564 const std::vector<constant_interval_exprt> &intervals)
574 return value_is_not_contained_in(object, intervals);
581 return interval_abstract_valuet::make_interval(interval);
618 const std::vector<constant_interval_exprt> &intervals)
620 auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(
object);
621 auto as_expr = value->to_interval();
627 return interval.contains(as_expr);
662 auto widened_ends = std::vector<constant_interval_exprt>{};
667 if(range.is_lower_widened)
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))
682 if(range.is_upper_widened)
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()))
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
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...
ait supplies three of the four components needed: an abstract interpreter (in this case handling 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
tvt less_than(const constant_interval_exprt &o) const
const exprt & get_upper() const
tvt equal(const constant_interval_exprt &o) const
Base class for all expressions.
std::vector< exprt > operandst
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
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_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
exprt to_constant() const override
Converts to a constant expression if possible.
std::set< exprt >::const_iterator next
const exprt & current() const override
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
const abstract_object_pointert & current() const override
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_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)
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.