78 return std::make_unique<empty_index_ranget>();
83 return std::make_unique<indeterminate_index_ranget>();
117 return std::make_unique<single_value_value_ranget>(value);
122 const std::vector<abstract_object_pointert> &operands,
127 const std::vector<abstract_object_pointert> &operands,
132 const std::vector<abstract_object_pointert> &operands,
136template <
class representation_type>
137bool any_of_type(
const std::vector<abstract_object_pointert> &operands)
143 return (!p->is_top()) &&
144 (std::dynamic_pointer_cast<const representation_type>(p) !=
146 }) != operands.end();
137bool any_of_type(
const std::vector<abstract_object_pointert> &operands) {
…}
161 const std::vector<abstract_object_pointert> &operands,
174 const std::vector<abstract_object_pointert> &operands,
178 return transform(expr, operands, environment, ns);
184 const std::stack<exprt> &stack,
197 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
208 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
216template <
class representation_type>
219 return std::make_shared<representation_type>(type,
true,
false);
228 const std::vector<abstract_object_pointert> &
ops,
251 for(
size_t i = 0; i !=
operands.size(); ++i)
270 return std::make_shared<constant_abstract_valuet>(
283 return prev->to_constant() != cur->to_constant();
339 [&
env, &
ns](
const exprt &op) { return env.eval(op, ns); });
352 return rounding_mode.is_nil();
356 mutable std::vector<abstract_object_pointert>
operands;
377 const std::vector<abstract_object_pointert> &operands,
392 const std::vector<abstract_object_pointert> &
ops,
442 "Type of result interval should match expression type");
452 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
461 return std::vector<constant_interval_exprt>();
466 !std::dynamic_pointer_cast<const context_abstract_objectt>(
iav));
514 "Type of result interval should match expression type");
523 "Type of result interval should match expression type");
533 const std::vector<abstract_object_pointert> &
operands;
540 const std::vector<abstract_object_pointert> &operands,
555 const std::vector<abstract_object_pointert> &
ops,
596 std::vector<abstract_object_pointert> &
combination)
const
620 for(
size_t i = 0; i !=
expression.operands().size(); ++i)
622 const auto &v =
ops[i];
635 return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
641 auto unwrapped = std::vector<value_ranget>{};
645 auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
646 op->unwrap_context());
647 INVARIANT(
av,
"should be an abstract value object");
657 auto const &condition =
ops[0];
662 auto all_true =
true;
663 auto all_false =
true;
664 for(
const auto &v : condition)
666 auto expr = v->to_constant();
667 all_true = all_true && expr.is_true();
668 all_false = all_false && expr.is_false();
681 const std::vector<abstract_object_pointert> &
operands;
688 const std::vector<abstract_object_pointert> &operands,
699 return std::dynamic_pointer_cast<const abstract_value_objectt>(
obj);
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
bool any_value_sets(const std::vector< abstract_object_pointert > &operands)
static abstract_object_pointert intervals_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
index_range_implementation_ptrt make_indeterminate_index_range()
static abstract_object_pointert constants_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert make_top(const typet &type)
static abstract_object_pointert value_set_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
index_range_implementation_ptrt make_empty_index_range()
bool any_intervals(const std::vector< abstract_object_pointert > &operands)
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
bool any_of_type(const std::vector< abstract_object_pointert > &operands)
Common behaviour for abstract objects modelling values - constants, intervals, etc.
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Pre-defined bitvector types.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
static combine_result meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Interface method for the meet operation.
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const final
Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge.
virtual abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const =0
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
Interface for transforms.
abstract_object_pointert meet(const abstract_object_pointert &other) const final
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
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 final
A helper function to evaluate writing to a component of an abstract object.
virtual abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const =0
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Represents an interval of values.
static bool is_top(const constant_interval_exprt &a)
static exprt get_max(const exprt &a, const exprt &b)
static exprt get_min(const exprt &a, const exprt &b)
constant_interval_exprt eval(const irep_idt &unary_operator) const
abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
abstract_object_pointert transform() const
static const rounding_modes all_rounding_modes
bool rounding_mode_is_not_set() const
constants_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
abstract_object_pointert operator()() const
exprt adjust_expression_for_rounding_mode() const
std::vector< abstract_object_pointert > operands
std::vector< ieee_floatt::rounding_modet > rounding_modes
static const symbol_exprt rounding_mode_symbol
abstract_environmentt environment_with_rounding_mode(ieee_floatt::rounding_modet rm) const
const abstract_environmentt & environment
abstract_object_pointert top(const typet &type) const
static std::vector< abstract_object_pointert > reeval_operands(const exprt::operandst &ops, const abstract_environmentt &env, const namespacet &ns)
const exprt & current() const override
bool advance_to_next() override
index_range_implementation_ptrt reset() const override
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
index_range_implementation_ptrt reset() const override
indeterminate_index_ranget()
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
std::vector< constant_interval_exprt > operands_as_intervals() const
abstract_object_pointert operator()() const
const abstract_environmentt & environment
const std::vector< abstract_object_pointert > & operands
abstract_object_pointert evaluate_unary_expr(const std::vector< constant_interval_exprt > &interval_operands) const
abstract_object_pointert transform() const
abstract_object_pointert evaluate_conditional(const std::vector< constant_interval_exprt > &interval_operands) const
interval_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
interval_abstract_value_pointert make_interval(const exprt &expr) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Fixed-width bit-vector with two's complement interpretation.
bool advance_to_next() override
single_value_index_ranget(const exprt &val)
const exprt & current() const override
const abstract_object_pointert value
single_value_value_ranget(const abstract_object_pointert &val)
bool advance_to_next() override
const abstract_object_pointert & current() const override
value_range_implementation_ptrt reset() const override
Expression to hold a symbol (variable)
Semantic type conversion.
The type of an expression, extends irept.
static abstract_object_pointert make_value_set(const abstract_object_sett &initial_values)
abstract_object_pointert transform() const
const std::vector< abstract_object_pointert > & operands
static abstract_object_pointert evaluate_conditional(const std::vector< value_ranget > &ops)
const abstract_environmentt & environment
std::vector< value_ranget > operands_as_ranges() const
value_set_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
static bool is_constant_value(const abstract_object_pointert &v)
void evaluate_combination(abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const
abstract_object_sett evaluate_each_combination(const std::vector< value_ranget > &value_ranges) const
Evaluate expression for every combination of values in value_ranges.
abstract_object_pointert operator()() const
exprt rewrite_expression(const std::vector< abstract_object_pointert > &ops) const
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...
static exprt evaluator(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
An interval to represent a set of possible values.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Value Set Abstract Object.