Go to the documentation of this file.
45 const irep_idt simplified_id = simplified_expr.
id();
46 if(simplified_id == ID_symbol)
50 simplified_id == ID_member || simplified_id == ID_index ||
51 simplified_id == ID_dereference)
53 auto access_expr = simplified_expr;
54 auto target =
eval(access_expr.operands()[0], ns);
56 return target->expression_transform(
57 access_expr,
eval_operands(access_expr, *
this, ns), *
this, ns);
61 simplified_id == ID_array || simplified_id == ID_struct ||
62 simplified_id == ID_constant || simplified_id == ID_address_of)
69 if(!simplified_expr.
operands().empty())
88 if(symbol_entry.has_value())
89 return symbol_entry.value();
100 if(value->is_bottom())
102 bool bottom_at_start = this->
is_bottom();
104 return !bottom_at_start;
111 std::stack<exprt> stactions;
112 while(s.
id() != ID_symbol)
114 if(s.
id() == ID_index || s.
id() == ID_member || s.
id() == ID_dereference)
121 lhs_value =
eval(s, ns);
128 INVARIANT(s.
id() == ID_symbol,
"Have a symbol or a stack");
137 if(!stactions.empty())
140 final_value =
write(lhs_value, value, stactions, ns,
false);
147 if(s.
id() != ID_symbol)
149 throw std::runtime_error(
"invalid l-value");
155 const typet &lhs_type = ns.
follow(lhs_value->type());
156 const typet &rhs_type = ns.
follow(final_value->type());
160 lhs_type == rhs_type,
161 "Assignment types must match"
170 if(s.
id() == ID_symbol)
174 if(final_value != lhs_value)
186 std::stack<exprt> remaining_stack,
191 const exprt &next_expr = remaining_stack.top();
192 remaining_stack.pop();
194 const irep_idt &stack_head_id = next_expr.
id();
196 stack_head_id == ID_index || stack_head_id == ID_member ||
197 stack_head_id == ID_dereference,
198 "Write stack expressions must be index, member, or dereference");
200 return lhs->write(*
this, ns, remaining_stack, next_expr, rhs, merge_write);
214 exprt possibly_constant = res->to_constant();
216 if(possibly_constant.
id() != ID_nil)
220 possibly_constant.
type().
id() == ID_bool,
"simplication preserves type");
226 return !currently_bottom;
259 type, top, bttm, empty_constant_expr, *
this, ns);
279 type, top, bttm, e, environment, ns);
306 bool modified =
false;
307 decltype(env.
map)::delta_viewt delta_view;
308 env.
map.get_delta_view(
map, delta_view);
309 for(
const auto &entry : delta_view)
311 bool object_modified =
false;
313 entry.get_other_map_value(), entry.m, object_modified);
314 modified |= object_modified;
315 map.replace(entry.k, new_object);
358 decltype(
map)::viewt view;
360 for(
const auto &entry : view)
362 out << entry.first <<
" () -> ";
363 entry.second->output(out, ai, ns);
371 decltype(
map)::viewt view;
373 for(
const auto &entry : view)
375 if(entry.second ==
nullptr)
395 return eval_obj->expression_transform(e, operands, *
this, ns);
403 std::vector<abstract_environmentt::map_keyt>
409 std::vector<abstract_environmentt::map_keyt> symbols_diff;
410 decltype(first.
map)::viewt view;
411 first.
map.get_view(view);
412 for(
const auto &entry : view)
414 const auto &second_entry = second.
map.find(entry.first);
415 if(second_entry.has_value())
417 if(second_entry.value().get()->has_been_modified(entry.second))
420 symbols_diff.push_back(entry.first);
426 for(
const auto &entry : second.
map.get_view())
428 const auto &second_entry = first.
map.find(entry.first);
429 if(!second_entry.has_value())
432 symbols_diff.push_back(entry.first);
441 auto val = std::count_if(
444 [](
const symbol_tablet::const_iteratort::value_type &sym) {
445 return sym.second.is_lvalue && sym.second.is_static_lifetime;
455 decltype(
map)::viewt view;
458 for(
auto const &
object : view)
460 if(visited.find(
object.second) == visited.end())
462 object.second->get_statistics(statistics, visited, *
this, ns);
473 std::vector<abstract_object_pointert> operands;
475 for(
const auto &op : expr.
operands())
476 operands.push_back(env.
eval(op, ns));
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::size_t number_of_globals
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...
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 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.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
The base of all structure abstractions.
abstract_object_pointert resolve_symbol(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.
bool verify() const
Check the structural invariants are maintained.
Base class for all expressions.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
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...
Expression to hold a symbol (variable)
void make_top()
Set the domain to top (i.e. everything)
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
bool is_false() const
Return whether the expression is a constant representing false.
virtual abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
variable_sensitivity_object_factory_ptrt object_factory
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.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
API to expression classes for Pointers.
An abstract version of a program environment.
exprt simplify_expr(exprt src, const namespacet &ns)
sharing_mapt< map_keyt, abstract_object_pointert > map
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const irep_idt & id() const
std::set< abstract_object_pointert > abstract_object_visitedt
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Statistics gathering for the variable senstivity domain.
The base type of all abstract array representations.
This is the basic interface of the abstract interpreter with default implementations of the core func...
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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static std::size_t count_globals(const namespacet &ns)
std::vector< abstract_object_pointert > eval_operands(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
abstract_object_statisticst gather_statistics(const namespacet &ns) const
bool is_bottom() const
Gets whether the domain is bottom.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
An abstraction of a single value that just stores a constant.
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.