35 if(lhs.
id()==ID_address_of)
37 else if(lhs.
id()==ID_typecast)
39 else if(lhs.
id()==ID_symbol)
50 const std::set<irep_idt> &cleanup_functions)
52 if(lhs.
id()==ID_symbol)
59 if(cleanup_functions.empty())
62 cleanup_map[identifier].cleanup_functions=cleanup_functions;
69 const std::set<irep_idt> &alias_set)
71 if(lhs.
id()==ID_symbol)
80 for(
const auto &alias : alias_set)
90 std::set<irep_idt> &cleanup_functions)
92 if(rhs.
id()==ID_symbol)
99 const escape_domaint::cleanup_mapt::const_iterator m_it=
103 cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
104 m_it->second.cleanup_functions.end());
107 else if(rhs.
id()==ID_if)
112 else if(rhs.
id()==ID_typecast)
120 std::set<irep_idt> &alias_set)
122 if(rhs.
id()==ID_symbol)
128 alias_set.insert(identifier);
130 for(
const auto &alias :
aliases)
132 alias_set.insert(alias);
135 else if(rhs.
id()==ID_if)
140 else if(rhs.
id()==ID_typecast)
144 else if(rhs.
id()==ID_address_of)
152 std::set<irep_idt> &alias_set)
154 if(rhs.
id()==ID_symbol)
157 alias_set.insert(
"&"+
id2string(identifier));
159 else if(rhs.
id()==ID_if)
164 else if(rhs.
id()==ID_dereference)
177 locationt from{trace_from->current_location()};
188 switch(instruction.
type)
194 std::set<irep_idt> cleanup_functions;
198 std::set<irep_idt> rhs_aliases;
220 if(
function.
id()==ID_symbol)
225 if(code_function_call.
arguments().size()==2)
232 if(!cleanup_function.
empty())
235 std::set<irep_idt> lhs_set;
238 for(
const auto &l : lhs_set)
240 cleanup_map[l].cleanup_functions.insert(cleanup_function);
257 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
273 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
278 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
296 out << cleanup.first <<
':';
297 for(
const auto &
id : cleanup.second.cleanup_functions)
317 out <<
"Aliases: " << *a_it1;
320 out <<
' ' << *a_it2;
339 const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
340 std::set<irep_idt> &a_cleanup=
cleanup_map[cleanup.first].cleanup_functions;
341 auto old_size=a_cleanup.size();
342 a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
343 if(a_cleanup.size()!=old_size)
349 for(cleanup_mapt::iterator a_it=
cleanup_map.begin();
353 if(a_it->second.cleanup_functions.empty())
387 std::set<irep_idt> &cleanup_functions)
const
389 if(lhs.
id()==ID_symbol)
394 const escape_domaint::cleanup_mapt::const_iterator m_it=
403 for(
const auto &alias :
aliases)
412 cleanup_functions.insert(
413 m_it->second.cleanup_functions.begin(),
414 m_it->second.cleanup_functions.end());
424 const std::set<irep_idt> &cleanup_functions,
430 for(
const auto &cleanup : cleanup_functions)
435 goto_function.body.insert_before_swap(location);
472 std::set<irep_idt> cleanup_functions;
484 const auto &dead_symbol = instruction.
dead_symbol();
486 std::set<irep_idt> cleanup_functions1;
490 const escape_domaint::cleanup_mapt::const_iterator m_it =
496 cleanup_functions1.insert(
497 m_it->second.cleanup_functions.begin(),
498 m_it->second.cleanup_functions.end());
501 std::set<irep_idt> cleanup_functions2;
503 d.
check_lhs(dead_symbol, cleanup_functions2);
506 gf_entry.second, i_it, dead_symbol, cleanup_functions1,
true, ns);
508 gf_entry.second, i_it, dead_symbol, cleanup_functions2,
false, ns);
510 for(
const auto &c : cleanup_functions1)
516 for(
const auto &c : cleanup_functions2)
Operator to return the address of an object.
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
const escape_domaint & operator[](locationt l) const
Find the analysis result for a given location.
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
A codet representing an assignment in the program.
codet representation of a function call statement.
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void instrument(goto_modelt &)
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &) const
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
irep_idt get_function(const exprt &)
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool is_tracked(const symbol_exprt &)
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
bool merge(const escape_domaint &b, locationt from, locationt to)
Base class for all expressions.
source_locationt & add_source_location()
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
goto_program_instruction_typet type
What kind of instruction?
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
instructionst::iterator targett
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const char * to_string() const
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
void isolate(const_iterator it)
const T & find(const_iterator it) const
bool make_union(const T &a, const T &b)
bool same_set(const T &a, const T &b) const
typename numbering_typet::const_iterator const_iterator
bool is_root(const T &a) const
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.