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>(
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_ptrt make_empty_index_range()
std::shared_ptr< index_ranget > index_range_ptrt
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 exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
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 get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const irep_idt & get_value() const
Represents an interval of values.
static bool is_bottom(const constant_interval_exprt &a)
constant_interval_exprt bottom() const
static bool is_top(const constant_interval_exprt &a)
constant_interval_exprt typecast(const typet &type) const
bool is_single_value_interval() const
bool contains(const constant_interval_exprt &interval) 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
const exprt & get_lower() const
tvt less_than(const constant_interval_exprt &o) const
const exprt & get_upper() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
mp_integer largest() const
Return the largest value that can be represented using this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
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)
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)
const constant_interval_exprt & get_interval() const
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
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,...
abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const
Merge another interval abstract object with this one.
index_range_ptrt index_range(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
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,...
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.
constant_interval_exprt interval
interval_abstract_valuet(const typet &t)
const exprt & current() const override
interval_index_ranget(const constant_interval_exprt &interval, const namespacet &n)
static exprt next_element(const exprt &cur, const namespacet &ns)
bool advance_to_next() override
const irep_idt & id() const
+∞ upper bound for intervals
static memory_sizet from_bytes(std::size_t bytes)
-∞ upper bound for intervals
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
Semantic type conversion.
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...
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
static exprt look_through_casts(exprt e)
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
static mp_integer force_value_from_expr(const exprt &value)
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
static bool represents_interval(exprt e)
static irep_idt invert_relation(const irep_idt &relation)
static index_range_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
static constant_interval_exprt make_interval_expr(exprt e)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
An interval to represent a set of possible values.
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
std::size_t number_of_single_value_intervals
std::size_t number_of_interval_abstract_objects