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 |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
bool | merge (const escape_domaint &b, locationt from, locationt to) |
void | make_bottom () final |
void | make_top () final |
void | make_entry () final |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
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 66 of file escape_analysis.h.
typedef std::map<irep_idt, cleanupt> escape_domaint::cleanup_mapt |
Definition at line 77 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 366 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(), typecast_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().
|
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().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 47 of file escape_analysis.h.
References aliases, cleanup_map, union_find< T >::clear(), and has_values.
|
inlinefinalvirtual |
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 54 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, cleanup_map, union_find< T >::find(), has_values, tvt::is_false(), union_find< T >::isolate(), union_find< T >::make_union(), and union_find< T >::same_set().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 256 of file escape_analysis.cpp.
References aliases, cleanup_map, has_values, tvt::is_known(), union_find< T >::is_root(), union_find< T >::same_set(), and tvt::to_string().
|
final |
Definition at line 164 of file escape_analysis.cpp.
References aliases, code_function_callt::arguments(), ASSIGN, assign_lhs_aliases(), assign_lhs_cleanup(), cleanup_map, 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(), and to_symbol_expr().
|
friend |
Definition at line 90 of file escape_analysis.h.
aliasest escape_domaint::aliases |
Definition at line 67 of file escape_analysis.h.
Referenced by assign_lhs_aliases(), check_lhs(), get_rhs_aliases(), make_bottom(), make_top(), merge(), output(), and transform().
cleanup_mapt escape_domaint::cleanup_map |
Definition at line 78 of file escape_analysis.h.
Referenced by assign_lhs_cleanup(), check_lhs(), get_rhs_cleanup(), escape_analysist::instrument(), make_bottom(), make_top(), merge(), output(), and transform().
|
private |
Definition at line 81 of file escape_analysis.h.
Referenced by make_bottom(), make_top(), merge(), output(), and transform().