72 auto const &
id = expr.
id();
113 auto const operands =
eval_operands(simplified_expr, *
this, ns);
114 auto const &target = operands.front();
116 return target->expression_transform(simplified_expr, operands, *
this, ns);
130 if(!simplified_expr.
operands().empty())
157 if(value->is_bottom())
161 return !bottom_at_start;
206 throw std::runtime_error(
"invalid l-value");
218 "Assignment types must match"
255 "Write stack expressions must be index, member, or dereference");
270 if(assumption.id() !=
ID_nil)
273 INVARIANT(assumption.is_boolean(),
"simplification preserves type");
275 if(assumption.is_false())
309 return fn(*
this, expr, ns);
311 return eval(expr, ns)->to_constant();
342 type, top,
bttm, e, environment, ns);
368 bool modified =
false;
369 for(
const auto &entry :
env.map.get_delta_view(
map))
417 for(
const auto &entry :
map.get_view())
419 out << entry.first <<
" () -> ";
420 entry.second->output(out,
ai, ns);
435 for(
const auto &entry :
map.get_view())
437 auto sym = entry.first;
438 auto val = entry.second;
453 for(
const auto &entry :
map.get_view())
455 if(entry.second ==
nullptr)
475 return eval_obj->expression_transform(e, operands, *
this, ns);
483std::vector<abstract_environmentt::map_keyt>
489 std::vector<abstract_environmentt::map_keyt>
symbols_diff;
490 for(
const auto &entry : first.
map.get_view())
495 if(
second_entry.value().get()->has_been_modified(entry.second))
504 for(
const auto &entry : second.
map.get_view())
519 auto val = std::count_if(
522 [](
const symbol_tablet::const_iteratort::value_type &
sym) {
523 return sym.second.is_lvalue && sym.second.is_static_lifetime;
534 for(
auto const &
object :
map.get_view())
536 if(visited.find(
object.second) == visited.end())
538 object.second->get_statistics(statistics, visited, *
this, ns);
549 std::vector<abstract_object_pointert> operands;
551 for(
const auto &op : expr.
operands())
552 operands.push_back(
env.eval(op, ns));
560 return std::dynamic_pointer_cast<const abstract_value_objectt>(
561 obj->unwrap_context());
609 std::dynamic_pointer_cast<const context_abstract_objectt>(previous);
610 if(context !=
nullptr)
611 obj = context->envelop(
obj);
640 if(result.is_false())
642 nil |= result.is_nil();
682 return left ==
nullptr ||
right ==
nullptr ||
689 return left->is_top() ||
right->is_top();
702 auto left =
env.eval(lhs, ns);
703 auto right =
env.eval(rhs, ns);
705 if(left->is_top() && right->is_top())
708 return {lhs, rhs, left, right};
719 auto constrained = std::make_shared<interval_abstract_valuet>(
726 auto constrained = std::make_shared<interval_abstract_valuet>(
740 if(operands.are_bad())
743 if(operands.has_top())
746 auto meet = operands.left->meet(operands.right);
748 if(meet->is_bottom())
768 if(left->is_top() || right->is_top())
773 auto meet = left->meet(right);
775 if(meet->is_bottom())
792 operands.
left->type());
803 operands.
right->type());
818 if(operands.are_bad())
821 if(operands.has_top())
824 auto left_interval = operands.left_interval();
825 auto right_interval = operands.right_interval();
827 const auto &
left_lower = left_interval.get_lower();
828 const auto &
right_upper = right_interval.get_upper();
std::vector< abstract_object_pointert > eval_operands(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
static auto assume_functions
static bool is_value(const abstract_object_pointert &obj)
static exprt assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static auto inverse_operations
static exprt invert_expr(const exprt &expr)
static abstract_value_pointert as_value(const abstract_object_pointert &obj)
static bool is_object_creation(const irep_idt &id)
static auto symmetric_operations
static bool is_access_expr(const irep_idt &id)
left_and_right_valuest eval_operands_as_values(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_noteq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static std::size_t count_globals(const namespacet &ns)
static exprt assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
exprt(* assume_function)(abstract_environmentt &, const exprt &, const namespacet &)
static exprt assume_less_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt invert_result(const exprt &result)
exprt assume_less_than_unbounded(abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns)
static exprt assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
bool is_ptr_comparison(const exprt &expr)
void prune_assign(abstract_environmentt &env, const abstract_object_pointert &previous, const exprt &destination, abstract_object_pointert obj, const namespacet &ns)
static bool is_dynamic_allocation(const exprt &expr)
exprt assume_eq_unbounded(abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns)
static exprt assume_greater_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
bool is_ptr_diff(const exprt &expr)
An abstract version of a program environment.
bool is_ptr_comparison(const exprt &expr)
bool is_ptr_diff(const exprt &expr)
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
bool is_bottom() const
Gets whether the domain is bottom.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
exprt to_predicate() const
Gives a boolean condition that is true for all values represented by the environment.
void make_top()
Set the domain to top (i.e. everything)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
bool verify() const
Check the structural invariants are maintained.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
exprt do_assume(const exprt &e, const namespacet &ns)
const vsd_configt & configuration() const
Exposes the environment configuration.
variable_sensitivity_object_factory_ptrt object_factory
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
abstract_object_statisticst gather_statistics(const namespacet &ns) const
virtual bool merge(const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode)
Computes the join between "this" and "b".
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
bool is_top() const
Gets whether the domain is top.
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 abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
sharing_mapt< map_keyt, abstract_object_pointert > map
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Represents an interval of values.
static exprt get_max(const exprt &a, const exprt &b)
static exprt get_min(const exprt &a, const exprt &b)
const exprt & get_lower() 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.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
typet & type()
Return the type of the expression.
The Boolean constant false.
instructionst::const_iterator const_targett
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
+∞ upper bound for intervals
-∞ upper bound for intervals
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The Boolean constant true.
The type of an expression, extends irept.
abstract_object_pointert get_abstract_object(const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const
Get the appropriate abstract object for the variable under consideration.
const vsd_configt & config() const
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Deprecated expression utility functions.
An interval to represent a set of possible values.
exprt simplify_expr(exprt src, const namespacet &ns)
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::size_t number_of_globals
abstract_object_pointert right
constant_interval_exprt right_interval() const
constant_interval_exprt left_interval() const
abstract_object_pointert left
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...