58 std::set<exprt>::const_iterator
next;
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);
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);
229 return !v->is_top() && !v->is_bottom();
246 if(other->is_bottom())
270 meet_value = std::make_shared<constant_abstract_valuet>(lower_bound);
276 return std::make_shared<value_set_abstract_objectt>(
type(),
false,
true);
317 const exprt &upper)
const
343 return compacted.first()->to_predicate(name);
351 return value->to_predicate(name);
373 out <<
"value-set-begin: ";
377 out <<
" :value-set-end";
385 for(
auto const &value : values)
394 auto const &
value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
399 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
412 return value->is_top();
424 std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
450 return c.is_false() || (
c.id() ==
ID_min);
454 return c.is_true() || (
c.id() ==
ID_max);
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);
507static 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)
579 return value_is_not_contained_in(object, intervals);
586 return interval_abstract_valuet::make_interval(interval);
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)
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
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
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.
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 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.