Go to the documentation of this file.
58 : value(val), available(true)
76 return util_make_unique<empty_index_ranget>();
81 return util_make_unique<indeterminate_index_ranget>();
115 return util_make_unique<single_value_value_ranget>(value);
120 const std::vector<abstract_object_pointert> &operands,
125 const std::vector<abstract_object_pointert> &operands,
130 const std::vector<abstract_object_pointert> &operands,
134 template <
class representation_type>
135 bool any_of_type(
const std::vector<abstract_object_pointert> &operands)
141 return (!p->is_top()) &&
142 (std::dynamic_pointer_cast<const representation_type>(p) !=
144 }) != operands.end();
149 return any_of_type<value_set_abstract_objectt>(operands);
154 return any_of_type<interval_abstract_valuet>(operands);
159 const std::vector<abstract_object_pointert> &operands,
172 const std::vector<abstract_object_pointert> &operands,
176 auto result =
transform(expr, operands, environment, ns);
181 template <
class representation_type>
184 return std::make_shared<representation_type>(type,
true,
false);
218 for(
const exprt &op : operands)
224 expr.
operands().push_back(lhs_value.is_nil() ? op : lhs_value);
231 if(lhs_value.is_nil())
236 return std::make_shared<constant_abstract_valuet>(
242 std::vector<abstract_object_pointert> possible_results;
246 possible_results.push_back(
250 auto first = possible_results.front()->to_constant();
251 for(
auto const &possible_result : possible_results)
253 auto current = possible_result->to_constant();
254 if(current.is_nil() || current != first)
257 return possible_results.front();
279 return adjusted_expr;
289 return make_top<constant_abstract_valuet>(type);
295 return rounding_mode.is_nil();
319 const std::vector<abstract_object_pointert> &operands,
334 const std::vector<abstract_object_pointert> &ops,
354 auto num_operands = interval_operands.size();
365 if(num_operands == 0)
371 if(num_operands == 1)
376 for(
size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
378 auto &interval_next = interval_operands[opIndex];
384 "Type of result interval should match expression type");
390 std::vector<constant_interval_exprt> interval_operands;
394 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
401 const auto op_as_constant = op->to_constant();
402 if(op_as_constant.is_nil())
403 return std::vector<constant_interval_exprt>();
408 !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
412 interval_operands.push_back(iav->to_interval());
415 return interval_operands;
419 const std::vector<constant_interval_exprt> &interval_operands)
const
421 auto const &condition_interval = interval_operands[0];
422 auto const &true_interval = interval_operands[1];
423 auto const &false_interval = interval_operands[2];
425 auto condition_result = condition_interval.is_definitely_true();
427 if(condition_result.is_unknown())
433 true_interval.get_lower(), false_interval.get_lower()),
435 true_interval.get_upper(), false_interval.get_upper())));
438 return condition_result.is_true() ?
make_interval(true_interval)
443 const std::vector<constant_interval_exprt> &interval_operands)
const
456 "Type of result interval should match expression type");
465 "Type of result interval should match expression type");
471 return std::make_shared<interval_abstract_valuet>(expr,
environment,
ns);
475 const std::vector<abstract_object_pointert> &
operands;
482 const std::vector<abstract_object_pointert> &operands,
497 const std::vector<abstract_object_pointert> &ops,
530 std::vector<abstract_object_pointert> combination;
537 const std::vector<value_ranget> &value_ranges,
538 std::vector<abstract_object_pointert> &combination)
const
540 size_t n = combination.size();
541 if(n == value_ranges.size())
549 for(
const auto &value : value_ranges[n])
551 combination.push_back(value);
553 combination.pop_back();
564 const auto &v = ops[i];
566 operands_expr.push_back(v->to_constant());
570 auto rewritten_expr =
572 return rewritten_expr;
577 return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
583 auto unwrapped = std::vector<value_ranget>{};
587 auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
588 op->unwrap_context());
589 INVARIANT(av,
"should be an abstract value object");
590 unwrapped.emplace_back(av->value_range());
600 for(
auto const &value : values)
606 return unwrapped_values;
612 auto const &value_as_set =
613 std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
617 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
618 value_as_set->get_values().first()));
620 return value_as_set->get_values().first();
623 return maybe_singleton;
642 return std::make_shared<interval_abstract_valuet>(values.
to_interval());
648 const auto &type = values.
first()->type();
649 auto value_set = std::make_shared<value_set_abstract_objectt>(type);
650 value_set->set_values(values);
657 auto const &condition = ops[0];
659 auto const &true_result = ops[1];
660 auto const &false_result = ops[2];
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();
670 auto indeterminate = !all_true && !all_false;
673 if(all_true || indeterminate)
674 resulting_objects.
insert(true_result);
675 if(all_false || indeterminate)
676 resulting_objects.
insert(false_result);
681 const std::vector<abstract_object_pointert> &
operands;
688 const std::vector<abstract_object_pointert> &operands,
void evaluate_combination(abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const
sharing_ptrt< class abstract_objectt > abstract_object_pointert
abstract_object_pointert evaluate_conditional(const std::vector< constant_interval_exprt > &interval_operands) const
exprt eval_constant(const exprt &op) const
interval_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
const abstract_environmentt & environment
static exprt get_max(const exprt &a, const exprt &b)
static abstract_object_pointert make_value_set(const abstract_object_sett &values)
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
indeterminate_index_ranget()
const exprt & current() const override
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
abstract_environmentt environment_with_rounding_mode(ieee_floatt::rounding_modet rm) const
bool any_intervals(const std::vector< abstract_object_pointert > &operands)
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
abstract_object_pointert top(const typet &type) const
const abstract_object_pointert value
exprt adjust_expression_for_rounding_mode() const
const abstract_environmentt & environment
Expression to hold a symbol (variable)
static abstract_object_pointert evaluate_conditional(const std::vector< value_ranget > &ops)
sharing_ptrt< const interval_abstract_valuet > interval_abstract_value_pointert
abstract_object_pointert operator()() const
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 ...
static abstract_object_pointert intervals_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
abstract_object_pointert transform() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool advance_to_next() override
interval_abstract_value_pointert make_interval(const exprt &expr) const
const abstract_environmentt & environment
index_range_implementation_ptrt make_empty_index_range()
typet & type()
Return the type of the expression.
abstract_object_pointert transform() const
const std::vector< abstract_object_pointert > & operands
single_value_index_ranget(const exprt &val)
bool any_value_sets(const std::vector< abstract_object_pointert > &operands)
abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
index_range_implementation_ptrt reset() const override
std::vector< ieee_floatt::rounding_modet > rounding_modes
Value Set Abstract Object.
abstract_object_pointert evaluate_unary_expr(const std::vector< constant_interval_exprt > &interval_operands) const
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
single_value_value_ranget(const abstract_object_pointert &val)
#define PRECONDITION(CONDITION)
Pre-defined bitvector types.
constant_interval_exprt eval(const irep_idt &unary_operator) const
Fixed-width bit-vector with two's complement interpretation.
void insert(const abstract_object_pointert &o)
abstract_object_pointert first() const
An abstract version of a program environment.
bool rounding_mode_is_not_set() const
exprt simplify_expr(exprt src, const namespacet &ns)
static abstract_object_pointert make_interval(const abstract_object_sett &values)
abstract_object_pointert make_top(const typet &type)
abstract_object_pointert operator()() const
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const irep_idt & id() const
std::vector< exprt > operandst
index_range_implementation_ptrt reset() const override
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
exprt rewrite_expression(const std::vector< abstract_object_pointert > &ops) const
std::vector< constant_interval_exprt > operands_as_intervals() const
abstract_object_pointert transform() const
static const symbol_exprt rounding_mode_symbol
abstract_object_pointert operator()() const
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_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.
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
value_set_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
constant_interval_exprt typecast(const typet &type) const
const exprt & current() const override
value_range_implementation_ptrt reset() const override
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
An interval to represent a set of possible values.
const abstract_object_pointert & current() const override
static bool is_constant_value(const abstract_object_pointert &v)
bool advance_to_next() override
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)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
static exprt get_min(const exprt &a, const exprt &b)
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::vector< value_ranget > operands_as_ranges() const
bool any_of_type(const std::vector< abstract_object_pointert > &operands)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static abstract_object_pointert resolve_values(const abstract_object_sett &new_values)
Semantic type conversion.
static const rounding_modes all_rounding_modes
constants_evaluator(const exprt &e, const abstract_environmentt &env, const namespacet &n)
bool advance_to_next() override
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
index_range_implementation_ptrt make_indeterminate_index_range()
const std::vector< abstract_object_pointert > & operands
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_sett evaluate_each_combination(const std::vector< value_ranget > &value_ranges) const
Evaluate expression for every combination of values in value_ranges.
An abstraction of a single value that just stores a constant.
Common behaviour for abstract objects modelling values - constants, intervals, etc.