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 |
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 |
void | make_top () final override |
bool | is_bottom () const override final |
bool | is_top () const override final |
void | make_entry () override final |
![]() | |
ai_domain_baset () | |
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 |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. 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 |
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 |
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 |
|
inlinefinaloverridevirtual |
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 |
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().