61 : value(val), available(true)
123 const std::vector<abstract_object_pointert> &operands,
128 const std::vector<abstract_object_pointert> &operands,
133 const std::vector<abstract_object_pointert> &operands,
137template <
class representation_type>
138bool any_of_type(
const std::vector<abstract_object_pointert> &operands)
144 return (!p->is_top()) &&
145 (std::dynamic_pointer_cast<const representation_type>(p) !=
147 }) != operands.end();
162 const std::vector<abstract_object_pointert> &operands,
175 const std::vector<abstract_object_pointert> &operands,
179 return transform(expr, operands, environment, ns);
185 const std::stack<exprt> &stack,
186 const exprt &specifier,
188 bool merging_write)
const
198 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
209 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
217template <
class representation_type>
220 return std::make_shared<representation_type>(type,
true,
false);
229 const std::vector<abstract_object_pointert> &ops,
251 auto operand_is_top =
false;
252 for(
size_t i = 0; i !=
operands.size(); ++i)
254 auto lhs_value =
operands[i]->to_constant();
259 if(lhs_value.is_not_nil())
260 expr.operands()[i] = lhs_value;
262 operand_is_top =
true;
267 if(simplified.has_operands() && operand_is_top)
268 return top(simplified.type());
271 return std::make_shared<constant_abstract_valuet>(
279 auto results_differ = [](
284 return prev->to_constant() != cur->to_constant();
290 auto child_operands =
296 if(result->is_top() || results_differ(last_result, result))
298 last_result = result;
327 return adjusted_expr;
335 auto reevaled_operands = std::vector<abstract_object_pointert>{};
339 std::back_inserter(reevaled_operands),
340 [&env, &
ns](
const exprt &op) { return env.eval(op, ns); });
341 return reevaled_operands;
353 return rounding_mode.is_nil();
357 mutable std::vector<abstract_object_pointert>
operands;
378 const std::vector<abstract_object_pointert> &operands,
393 const std::vector<abstract_object_pointert> &ops,
413 auto num_operands = interval_operands.size();
424 if(num_operands == 0)
430 if(num_operands == 1)
435 for(
size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
437 auto &interval_next = interval_operands[opIndex];
443 "Type of result interval should match expression type");
449 std::vector<constant_interval_exprt> interval_operands;
453 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
460 const auto op_as_constant = op->to_constant();
461 if(op_as_constant.is_nil())
462 return std::vector<constant_interval_exprt>();
467 !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
471 interval_operands.push_back(iav->to_interval());
474 return interval_operands;
478 const std::vector<constant_interval_exprt> &interval_operands)
const
480 auto const &condition_interval = interval_operands[0];
481 auto const &true_interval = interval_operands[1];
482 auto const &false_interval = interval_operands[2];
484 auto condition_result = condition_interval.is_definitely_true();
486 if(condition_result.is_unknown())
492 true_interval.get_lower(), false_interval.get_lower()),
494 true_interval.get_upper(), false_interval.get_upper())));
497 return condition_result.is_true() ?
make_interval(true_interval)
502 const std::vector<constant_interval_exprt> &interval_operands)
const
515 "Type of result interval should match expression type");
524 "Type of result interval should match expression type");
534 const std::vector<abstract_object_pointert> &
operands;
541 const std::vector<abstract_object_pointert> &operands,
556 const std::vector<abstract_object_pointert> &ops,
589 std::vector<abstract_object_pointert> combination;
596 const std::vector<value_ranget> &value_ranges,
597 std::vector<abstract_object_pointert> &combination)
const
599 size_t n = combination.size();
600 if(n == value_ranges.size())
608 for(
const auto &value : value_ranges[n])
610 combination.push_back(value);
612 combination.pop_back();
623 const auto &v = ops[i];
625 operands_expr.push_back(v->to_constant());
629 auto rewritten_expr =
631 return rewritten_expr;
636 return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
642 auto unwrapped = std::vector<value_ranget>{};
646 auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
647 op->unwrap_context());
648 INVARIANT(av,
"should be an abstract value object");
649 unwrapped.emplace_back(av->value_range());
658 auto const &condition = ops[0];
660 auto const &true_result = ops[1];
661 auto const &false_result = ops[2];
663 auto all_true =
true;
664 auto all_false =
true;
665 for(
const auto &v : condition)
667 auto expr = v->to_constant();
668 all_true = all_true && expr.is_true();
669 all_false = all_false && expr.is_false();
671 auto indeterminate = !all_true && !all_false;
674 if(all_true || indeterminate)
675 resulting_objects.
insert(true_result);
676 if(all_false || indeterminate)
677 resulting_objects.
insert(false_result);
682 const std::vector<abstract_object_pointert> &
operands;
689 const std::vector<abstract_object_pointert> &operands,
700 return std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
An abstract version of a program environment.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
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.
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
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.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
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.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
void insert(const abstract_object_pointert &o)
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
Represents an interval of values.
constant_interval_exprt typecast(const typet &type) const
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
sharing_ptrt< const interval_abstract_valuet > interval_abstract_value_pointert
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
const irep_idt & id() 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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
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.