65 return (expr.
id() == ID_minus) &&
66 (expr.
operands()[0].type().id() == ID_pointer) &&
67 (expr.
operands()[1].type().id() == ID_pointer);
72 auto const &
id = expr.
id();
73 bool is_comparison =
id == ID_equal ||
id == ID_notequal ||
id == ID_lt ||
74 id == ID_le ||
id == ID_gt ||
id == ID_ge;
76 return is_comparison && (expr.
operands()[0].type().id() == ID_pointer) &&
77 (expr.
operands()[1].type().id() == ID_pointer);
82 return id == ID_member ||
id == ID_index ||
id == ID_dereference;
87 return id == ID_array ||
id == ID_struct ||
id == ID_constant ||
93 return expr.
id() == ID_side_effect && expr.
get(ID_statement) == ID_allocate;
105 const irep_idt simplified_id = simplified_expr.
id();
106 if(simplified_id == ID_symbol)
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);
124 typet(ID_dynamic_object),
125 exprt(ID_dynamic_object, simplified_expr.
type()),
130 if(!simplified_expr.
operands().empty())
145 if(symbol_entry.has_value())
146 return symbol_entry.value();
157 if(value->is_bottom())
159 bool bottom_at_start = this->
is_bottom();
161 return !bottom_at_start;
168 std::stack<exprt> stactions;
169 while(s.
id() != ID_symbol)
171 if(s.
id() == ID_index || s.
id() == ID_member || s.
id() == ID_dereference)
178 lhs_value =
eval(s, ns);
185 INVARIANT(s.
id() == ID_symbol,
"Have a symbol or a stack");
194 if(!stactions.empty())
197 final_value =
write(lhs_value, value, stactions, ns,
false);
204 if(s.
id() != ID_symbol)
206 throw std::runtime_error(
"invalid l-value");
212 const typet &lhs_type = ns.
follow(lhs_value->type());
213 const typet &rhs_type = ns.
follow(final_value->type());
217 lhs_type == rhs_type,
218 "Assignment types must match"
227 if(s.
id() == ID_symbol)
231 if(final_value != lhs_value)
243 std::stack<exprt> remaining_stack,
248 const exprt &next_expr = remaining_stack.top();
249 remaining_stack.pop();
251 const irep_idt &stack_head_id = next_expr.
id();
253 stack_head_id == ID_index || stack_head_id == ID_member ||
254 stack_head_id == ID_dereference,
255 "Write stack expressions must be index, member, or dereference");
257 return lhs->write(*
this, ns, remaining_stack, next_expr, rhs, merge_write);
268 auto assumption =
do_assume(simplified, ns);
270 if(assumption.id() != ID_nil)
273 INVARIANT(assumption.is_boolean(),
"simplification preserves type");
275 if(assumption.is_false())
279 return !currently_bottom;
287 std::map<irep_idt, assume_function>{{ID_not,
assume_not},
304 auto expr_id = expr.
id();
309 return fn(*
this, expr, ns);
311 return eval(expr, ns)->to_constant();
322 type, top, bttm, empty_constant_expr, *
this, ns);
342 type, top, bttm, e, environment, ns);
368 bool modified =
false;
369 for(
const auto &entry : env.
map.get_delta_view(
map))
372 entry.get_other_map_value(), entry.m, merge_location, widen_mode);
374 modified |= merge_result.modified;
375 map.replace(entry.k, merge_result.object);
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;
439 auto pred = val->to_predicate(
symbol_exprt(sym, val->type()));
441 predicates.push_back(pred);
444 if(predicates.size() == 1)
445 return predicates.front();
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())
492 const auto &second_entry = second.
map.find(entry.first);
493 if(second_entry.has_value())
495 if(second_entry.value().get()->has_been_modified(entry.second))
498 symbols_diff.push_back(entry.first);
504 for(
const auto &entry : second.
map.get_view())
506 const auto &second_entry = first.
map.find(entry.first);
507 if(!second_entry.has_value())
510 symbols_diff.push_back(entry.first);
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());
570 std::map<irep_idt, irep_idt>{{ID_equal, ID_notequal},
571 {ID_notequal, ID_equal},
589 auto expr_id = expr.
id();
596 auto inverse_op = inverse_operation->second;
598 relation_expr.lhs(), inverse_op, relation_expr.rhs());
604 const exprt &destination,
609 std::dynamic_pointer_cast<const context_abstract_objectt>(previous);
610 if(context !=
nullptr)
611 obj = context->envelop(obj);
612 env.
assign(destination, obj, ns);
622 auto inverse_expression =
invert_expr(not_expr.op());
623 if(inverse_expression.is_not_nil())
624 return env.
do_assume(inverse_expression, ns);
626 auto result = env.
do_assume(not_expr.op(), ns);
637 for(
auto const &operand : and_expr.operands())
639 auto result = env.
do_assume(operand, ns);
640 if(result.is_false())
657 for(
auto const &operand : or_expr.operands())
682 return left ==
nullptr ||
right ==
nullptr ||
689 return left->is_top() ||
right->is_top();
700 auto lhs = relationship_expr.lhs();
701 auto rhs = relationship_expr.rhs();
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())
752 prune_assign(env, operands.left, operands.lhs, meet, ns);
754 prune_assign(env, operands.right, operands.rhs, meet, ns);
765 auto left = env.
eval(notequal_expr.lhs(), ns);
766 auto right = env.
eval(notequal_expr.rhs(), ns);
768 if(left->is_top() || right->is_top())
773 auto meet = left->meet(right);
775 if(meet->is_bottom())
792 operands.
left->type());
794 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
803 operands.
right->type());
805 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
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();
830 auto reduced_le_expr =
832 auto result = env.
eval(reduced_le_expr, ns)->to_constant();
838 left_interval.get_upper(), right_upper);
840 as_value(operands.left)->constrain(left_lower, pruned_upper);
841 prune_assign(env, operands.left, operands.lhs, constrained, ns);
846 left_lower, right_interval.get_lower());
848 as_value(operands.right)->constrain(pruned_lower, right_upper);
849 prune_assign(env, operands.right, operands.rhs, constrained, ns);
856 std::map<irep_idt, irep_idt>{{ID_ge, ID_le}, {ID_gt, ID_lt}};
866 auto symmetric_expr =
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.
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
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...
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
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
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...