Go to the documentation of this file.
27 next(interval.get_lower()),
28 upper(interval.get_upper()),
61 return std::make_shared<interval_index_ranget>(interval, n);
66 while(e.
id() == ID_typecast)
77 if(type.
id() == ID_signedbv)
91 if(type.
id() == ID_signedbv)
117 INVARIANT(maybe_integer_value.has_value(),
"Input has to have a value");
118 return maybe_integer_value.value();
146 return (e.
id() == ID_constant_interval || e.
id() == ID_constant);
152 if(e.
id() == ID_constant_interval)
156 else if(e.
id() == ID_constant)
170 relation == ID_le || relation == ID_lt || relation == ID_ge ||
171 relation == ID_gt || relation == ID_equal);
172 if(relation == ID_le)
174 if(relation == ID_ge)
176 if(relation == ID_lt)
178 if(relation == ID_gt)
191 const auto &relation = e.
id();
193 const auto &lhs = binary_e.lhs();
194 const auto &rhs = binary_e.rhs();
196 relation == ID_le || relation == ID_lt || relation == ID_ge ||
197 relation == ID_gt || relation == ID_equal);
198 PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
199 PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
202 const auto the_constant_part_of_the_relation =
203 (rhs.id() == ID_symbol ? lhs : rhs);
204 const auto maybe_inverted_relation =
207 if(maybe_inverted_relation == ID_le)
209 if(maybe_inverted_relation == ID_lt)
211 if(maybe_inverted_relation == ID_ge)
213 if(maybe_inverted_relation == ID_gt)
216 maybe_inverted_relation == ID_equal,
"We excluded other cases above");
218 the_constant_part_of_the_relation, the_constant_part_of_the_relation);
275 const std::vector<abstract_object_pointert> &operands,
279 std::size_t num_operands = expr.
operands().size();
282 std::vector<sharing_ptrt<interval_abstract_valuet>> interval_operands;
284 for(
const auto &op : operands)
286 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
294 const auto op_as_constant = op->to_constant();
295 if(op_as_constant.is_nil())
299 auto top_context_object =
300 std::dynamic_pointer_cast<const context_abstract_objectt>(
303 return top_context_object->get_child();
307 const auto ivop_context =
308 std::dynamic_pointer_cast<const context_abstract_objectt>(ivop);
311 iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(
312 ivop_context->get_child());
315 iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(ivop);
318 !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
325 return op->expression_transform(expr, operands, environment, ns);
329 INVARIANT(iav,
"Should be an interval abstract value");
330 interval_operands.push_back(iav);
333 if(num_operands == 0)
336 if(expr.
id() == ID_if)
339 if(num_operands == 1)
344 for(
size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
346 auto &interval_next = interval_operands[opIndex]->interval;
347 result = result.
eval(expr.
id(), interval_next);
352 "Type of result interval should match expression type");
358 const std::vector<interval_abstract_value_pointert> &interval_operands,
362 auto const &condition_interval = interval_operands[0]->interval;
363 auto const &true_interval = interval_operands[1]->interval;
364 auto const &false_interval = interval_operands[2]->interval;
366 auto condition_result = condition_interval.is_definitely_true();
368 if(condition_result.is_unknown())
376 true_interval.get_lower(), false_interval.get_lower()),
378 true_interval.get_upper(), false_interval.get_upper())),
382 return condition_result.is_true()
384 true_interval.type(), true_interval, ns)
386 false_interval.type(), false_interval, ns);
391 const std::vector<interval_abstract_value_pointert> &interval_operands,
397 if(expr.
id() == ID_typecast)
406 "Type of result interval should match expression type");
413 interval_result.
type() == expr.
type(),
414 "Type of result interval should match expression type");
425 std::string lower_string;
426 std::string upper_string;
430 lower_string =
"-INF";
436 "We only support constant limits");
443 upper_string =
"+INF";
449 "We only support constant limits");
454 out <<
"[" << lower_string <<
", " << upper_string <<
"]";
466 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
493 return shared_from_this();
509 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
531 return shared_from_this();
545 return std::make_shared<interval_abstract_valuet>(
547 return std::make_shared<interval_abstract_valuet>(
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
mp_integer smallest() const
Return the smallest value that can be represented using this type.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
bool advance_to_next() override
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)
static bool is_bottom(const constant_interval_exprt &a)
static abstract_object_pointert evaluate_conditional(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
+∞ upper bound for intervals
bool contains(const constant_interval_exprt &interval) const
The plus expression Associativity is not specified.
Base class for all expressions.
-∞ upper bound for intervals
bool is_true() const
Return whether the expression is a constant representing true.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
exprt to_constant() const override
Converts to a constant expression if possible.
std::shared_ptr< index_ranget > index_range_ptrt
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
Represents an interval of values.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
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.
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
typet & type()
Return the type of the expression.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
static mp_integer force_value_from_expr(const exprt &value)
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
const std::string & id2string(const irep_idt &d)
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.
bool is_single_value_interval() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
constant_interval_exprt eval(const irep_idt &unary_operator) const
static exprt look_through_casts(exprt e)
static exprt next_element(const exprt &cur, const namespacet &ns)
An abstract version of a program environment.
constant_interval_exprt bottom() const
virtual exprt to_constant() const
Converts to a constant expression if possible.
exprt simplify_expr(exprt src, const namespacet &ns)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
static index_range_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
tvt less_than(const constant_interval_exprt &o) const
const irep_idt & id() const
static constant_interval_exprt make_interval_expr(exprt e)
std::set< abstract_object_pointert > abstract_object_visitedt
nonstd::optional< T > optionalt
static abstract_object_pointert evaluate_unary_expr(const exprt &expr, const std::vector< interval_abstract_value_pointert > &interval_operands, const abstract_environmentt &environment, const namespacet &ns)
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
const constant_interval_exprt & get_interval() const
static bool represents_interval(exprt e)
static bool is_top(const constant_interval_exprt &a)
constant_interval_exprt typecast(const typet &type) const
index_range_ptrt make_empty_index_range()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
An interval to represent a set of possible values.
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
This is the basic interface of the abstract interpreter with default implementations of the core func...
interval_abstract_valuet(const typet &t)
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
std::size_t number_of_single_value_intervals
const exprt & get_lower() const
mp_integer largest() const
Return the largest value that can be represented using this type.
interval_index_ranget(const constant_interval_exprt &interval, const namespacet &n)
const exprt & current() const override
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
const exprt & get_upper() const
static exprt get_min(const exprt &a, const exprt &b)
constant_interval_exprt interval
#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.
Semantic type conversion.
API to expression classes.
const irep_idt & get_value() const
static memory_sizet from_bytes(std::size_t bytes)
abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const
Merge another interval abstract object with this one.
static irep_idt invert_relation(const irep_idt &relation)
index_range_ptrt index_range(const namespacet &ns) const override
std::size_t number_of_interval_abstract_objects
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.