cprover
|
#include <escape_analysis.h>
Classes | |
struct | cleanupt |
Public Types | |
typedef union_find< irep_idt > | aliasest |
typedef std::map< irep_idt, cleanupt > | cleanup_mapt |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
escape_domaint () | |
void | transform (locationt from, locationt 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 is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More... | |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override |
bool | merge (const escape_domaint &b, locationt from, locationt to) |
void | make_bottom () final override |
no states More... | |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
bool | is_bottom () const override final |
bool | is_top () const override final |
void | make_entry () override final |
a reasonable entry-point state More... | |
![]() | |
virtual | ~ai_domain_baset () |
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const |
also add More... | |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Simplifies the expression but keeps it as an l-value. More... | |
virtual exprt | to_predicate (void) const |
Gives a Boolean condition that is true for all values represented by the domain. More... | |
Public Attributes | |
aliasest | aliases |
cleanup_mapt | cleanup_map |
Private Member Functions | |
void | assign_lhs_cleanup (const exprt &, const std::set< irep_idt > &) |
void | get_rhs_cleanup (const exprt &, std::set< irep_idt > &) |
void | assign_lhs_aliases (const exprt &, const std::set< irep_idt > &) |
void | get_rhs_aliases (const exprt &, std::set< irep_idt > &) |
void | get_rhs_aliases_address_of (const exprt &, std::set< irep_idt > &) |
irep_idt | get_function (const exprt &) |
void | check_lhs (const exprt &, std::set< irep_idt > &) |
bool | is_tracked (const symbol_exprt &) |
Private Attributes | |
tvt | has_values |
Friends | |
class | escape_analysist |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
Definition at line 24 of file escape_analysis.h.
typedef union_find<irep_idt> escape_domaint::aliasest |
Definition at line 80 of file escape_analysis.h.
typedef std::map<irep_idt, cleanupt> escape_domaint::cleanup_mapt |
Definition at line 91 of file escape_analysis.h.
|
inline |
Definition at line 27 of file escape_analysis.h.
|
private |
Definition at line 62 of file escape_analysis.cpp.
References aliases, symbol_exprt::get_identifier(), irept::id(), is_tracked(), union_find< T >::isolate(), union_find< T >::make_union(), and to_symbol_expr().
Referenced by transform().
|
private |
Definition at line 43 of file escape_analysis.cpp.
References cleanup_map, symbol_exprt::get_identifier(), irept::id(), is_tracked(), and to_symbol_expr().
Referenced by transform().
|
private |
Definition at line 358 of file escape_analysis.cpp.
References aliases, cleanup_map, symbol_exprt::get_identifier(), irept::id(), union_find< T >::same_set(), and to_symbol_expr().
Referenced by escape_analysist::instrument().
Definition at line 28 of file escape_analysis.cpp.
References symbol_exprt::get_identifier(), irept::id(), address_of_exprt::object(), unary_exprt::op(), to_address_of_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by transform().
|
private |
Definition at line 113 of file escape_analysis.cpp.
References aliases, symbol_exprt::get_identifier(), get_rhs_aliases_address_of(), irept::id(), is_tracked(), union_find< T >::same_set(), to_address_of_expr(), to_if_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by transform().
|
private |
Definition at line 145 of file escape_analysis.cpp.
References symbol_exprt::get_identifier(), irept::id(), id2string(), to_if_expr(), and to_symbol_expr().
Referenced by get_rhs_aliases().
|
private |
Definition at line 83 of file escape_analysis.cpp.
References cleanup_map, symbol_exprt::get_identifier(), irept::id(), is_tracked(), to_if_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 59 of file escape_analysis.h.
References aliases, cleanup_map, DATA_INVARIANT, has_values, tvt::is_false(), and union_find< T >::size().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 67 of file escape_analysis.h.
References aliases, cleanup_map, DATA_INVARIANT, has_values, tvt::is_true(), and union_find< T >::size().
|
private |
Definition at line 16 of file escape_analysis.cpp.
References symbol_exprt::get_identifier().
Referenced by assign_lhs_aliases(), assign_lhs_cleanup(), get_rhs_aliases(), and get_rhs_cleanup().
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 45 of file escape_analysis.h.
References aliases, cleanup_map, union_find< T >::clear(), and has_values.
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 75 of file escape_analysis.h.
References make_top().
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 52 of file escape_analysis.h.
References aliases, cleanup_map, union_find< T >::clear(), and has_values.
Referenced by make_entry().
bool escape_domaint::merge | ( | const escape_domaint & | b, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 302 of file escape_analysis.cpp.
References aliases, union_find< T >::begin(), cleanup_map, union_find< T >::end(), union_find< T >::find(), has_values, tvt::is_false(), union_find< T >::isolate(), union_find< T >::make_union(), union_find< T >::same_set(), and tvt::unknown().
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 256 of file escape_analysis.cpp.
References aliases, union_find< T >::begin(), cleanup_map, union_find< T >::end(), has_values, tvt::is_known(), union_find< T >::is_root(), union_find< T >::same_set(), and tvt::to_string().
|
finaloverridevirtual |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
Implements ai_domain_baset.
Definition at line 164 of file escape_analysis.cpp.
References aliases, code_function_callt::arguments(), ASSIGN, assign_lhs_aliases(), assign_lhs_cleanup(), cleanup_map, goto_programt::instructiont::code, DEAD, DECL, dstringt::empty(), END_FUNCTION, code_function_callt::function(), FUNCTION_CALL, get_function(), symbol_exprt::get_identifier(), code_declt::get_identifier(), code_deadt::get_identifier(), get_rhs_aliases(), get_rhs_cleanup(), has_values, tvt::is_false(), union_find< T >::isolate(), code_assignt::lhs(), code_assignt::rhs(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_symbol_expr(), and goto_programt::instructiont::type.
|
friend |
Definition at line 104 of file escape_analysis.h.
aliasest escape_domaint::aliases |
Definition at line 81 of file escape_analysis.h.
Referenced by assign_lhs_aliases(), check_lhs(), get_rhs_aliases(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().
cleanup_mapt escape_domaint::cleanup_map |
Definition at line 92 of file escape_analysis.h.
Referenced by assign_lhs_cleanup(), check_lhs(), get_rhs_cleanup(), escape_analysist::instrument(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().
|
private |
Definition at line 95 of file escape_analysis.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().