Go to the documentation of this file.
37 cur = (*next)->to_constant();
50 return std::make_shared<value_set_index_ranget>(vals);
55 const std::vector<abstract_object_pointert> &ops);
57 std::vector<abstract_object_sett>
81 template <
typename Con,
typename F>
83 const std::vector<Con> &super_con,
84 std::vector<typename Con::value_type> &sub_con,
87 size_t n = sub_con.size();
88 if(n == super_con.size())
92 for(
const auto &value : super_con[n])
94 sub_con.push_back(value);
106 template <
typename Con,
typename F>
109 std::vector<typename Con::value_type> sub_con;
137 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
152 const std::vector<abstract_object_pointert> &operands,
160 if(expr.
id() == ID_if)
162 expr.
type(), collective_operands, environment, ns);
169 [&resulting_objects, &dispatcher, &expr, &environment, &ns](
170 const std::vector<abstract_object_pointert> &ops) {
173 dispatcher->expression_transform(rewritten_expr, ops, environment, ns));
181 const std::vector<abstract_object_sett> &operands,
185 auto const condition = operands[0];
187 auto const true_result = operands[1];
188 auto const false_result = operands[2];
190 auto all_true =
true;
191 auto all_false =
true;
192 for(
auto v : condition)
194 auto expr = v->to_constant();
195 all_true = all_true && expr.is_true();
196 all_false = all_false && expr.is_false();
198 auto indeterminate = !all_true && !all_false;
201 if(all_true || indeterminate)
202 resulting_objects.
insert(true_result);
203 if(all_false || indeterminate)
204 resulting_objects.
insert(false_result);
211 const std::stack<exprt> &stack,
212 const exprt &specifier,
214 bool merging_write)
const
217 for(
const auto &st_value :
values)
220 st_value->write(environment, ns, stack, specifier, value, merging_write));
239 return shared_from_this();
253 std::dynamic_pointer_cast<value_set_abstract_objectt>(
mutable_clone());
254 result->set_values(unwrapped_values);
261 auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
264 auto union_values =
values;
265 union_values.
insert(cast_other->get_values());
279 for(
const auto &value : other_values)
281 const auto &value_expr = value->to_constant();
285 return std::make_shared<interval_abstract_valuet>(
313 out <<
"value-set-begin: ";
317 out <<
" :value-set-end";
323 const std::vector<abstract_object_pointert> &ops)
327 operands_expr.push_back(v->to_constant());
328 auto rewritten_expr =
exprt(expr.
id(), expr.
type(), std::move(operands_expr));
329 return rewritten_expr;
332 std::vector<abstract_object_sett>
335 auto unwrapped = std::vector<abstract_object_sett>{};
337 for(
const auto &op : operands)
341 INVARIANT(vsab,
"should be a value set abstract object");
342 unwrapped.push_back(vsab->get_values());
352 for(
auto const &value : values)
358 return unwrapped_values;
364 auto const &value_as_set =
365 std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
369 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
370 value_as_set->get_values().first()));
372 return value_as_set->get_values().first();
375 return maybe_singleton;
381 auto const &context_value =
382 std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
384 return context_value ? context_value->unwrap_context() : maybe_wrapped;
abstract_object_sett values
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
const abstract_object_sett & values
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
const_iterator begin() const
The type of an expression, extends irept.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
static exprt get_max(const exprt &a, const exprt &b)
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
const_iterator end() const
index_range_ptrt index_range(const namespacet &ns) const override
Base class for all expressions.
std::vector< abstract_object_sett > unwrap_operands(const std::vector< abstract_object_pointert > &operands)
value_sett::const_iterator const_iterator
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
std::shared_ptr< index_ranget > index_range_ptrt
bool advance_to_next() override
Represents an interval of values.
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 ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
Value Set Abstract Object.
abstract_object_pointert resolve_new_values(const abstract_object_sett &new_values, const abstract_environmentt &environment) const
Update the set of stored values to new_values.
#define PRECONDITION(CONDITION)
const exprt & current() const override
index_range_ptrt make_indeterminate_index_range()
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void insert(const abstract_object_pointert &o)
An abstraction of a pointer that tracks a single pointer.
abstract_object_pointert first() const
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
const irep_idt & id() const
std::vector< exprt > operandst
value_set_index_ranget(const abstract_object_sett &vals)
abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
abstract_object_sett::const_iterator next
An interval to represent a set of possible values.
The base type of all abstract array representations.
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
value_set_abstract_objectt(const typet &type)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const
static exprt get_min(const exprt &a, const exprt &b)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
exprt to_constant() const override
Converts to a constant expression if possible.
index_range_ptrt make_value_set_index_range(const abstract_object_sett &vals)
exprt rewrite_expression(const exprt &expr, const std::vector< abstract_object_pointert > &ops)
void apply_comb(const std::vector< Con > &super_con, std::vector< typename Con::value_type > &sub_con, F f)
Recursively construct a combination sub_con from super_con and once constructed call f.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
virtual internal_abstract_object_pointert mutable_clone() const
abstract_object_pointert maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped)
Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstr...
An abstraction of a single value that just stores a constant.
void for_each_comb(const std::vector< Con > &super_con, F f)
Call the function f on every combination of elements in super_con.