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));
std::vector< abstract_object_pointert > eval_operands(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
static std::size_t count_globals(const namespacet &ns)
An abstract version of a program environment.
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
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.
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
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...
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
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 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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
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_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
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 type of an expression, extends irept.
An abstraction of a single value that just stores a constant.
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::size_t number_of_globals
The base type of all abstract array representations.
The base of all structure abstractions.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...