cprover
escape_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive, over-approximative
4  escape analysis
5 
6 Author: Daniel Kroening, kroening@kroening.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
14 #define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
15 
16 #include <util/numbering.h>
17 #include <util/threeval.h>
18 #include <util/union_find.h>
19 
20 #include "ai.h"
21 
22 class escape_analysist;
23 
25 {
26 public:
28  {
29  }
30 
31  void transform(
32  const irep_idt &function_from,
33  locationt from,
34  const irep_idt &function_to,
35  locationt to,
36  ai_baset &ai,
37  const namespacet &ns) final override;
38 
39  void output(
40  std::ostream &out,
41  const ai_baset &ai,
42  const namespacet &ns) const final override;
43 
44  bool merge(
45  const escape_domaint &b,
46  locationt from,
47  locationt to);
48 
49  void make_bottom() final override
50  {
51  cleanup_map.clear();
52  aliases.clear();
53  has_values=tvt(false);
54  }
55 
56  void make_top() final override
57  {
58  cleanup_map.clear();
59  aliases.clear();
60  has_values=tvt(true);
61  }
62 
63  bool is_bottom() const override final
64  {
66  (cleanup_map.empty() && (aliases.size()==0)),
67  "If the domain is bottom, all maps must be empty");
68  return has_values.is_false();
69  }
70 
71  bool is_top() const override final
72  {
74  (cleanup_map.empty() && (aliases.size()==0)),
75  "If the domain is top, all maps must be empty");
76  return has_values.is_true();
77  }
78 
79  void make_entry() override final
80  {
81  make_top();
82  }
83 
86 
87  struct cleanupt
88  {
89  std::set<irep_idt> cleanup_functions;
90  };
91 
92  // We track a set of 'cleanup functions' for specific
93  // identifiers. The cleanup functions are executed
94  // once the last pointer to an object is lost.
95  typedef std::map<irep_idt, cleanupt> cleanup_mapt;
97 
98 private:
100  void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
101  void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
102  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
103  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
104  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
105  irep_idt get_function(const exprt &);
106  void check_lhs(const exprt &, std::set<irep_idt> &) const;
107 
108  friend class escape_analysist;
109 
110  bool is_tracked(const symbol_exprt &);
111 };
112 
113 class escape_analysist:public ait<escape_domaint>
114 {
115 public:
116  void instrument(goto_modelt &);
117 
118 protected:
119  virtual void initialize(const goto_functionst &)
120  {
121  }
122 
124 
125  void insert_cleanup(
128  const exprt &,
129  const std::set<irep_idt> &,
130  bool is_object,
131  const namespacet &);
132 };
133 
134 #endif // CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
escape_domaint::escape_domaint
escape_domaint()
Definition: escape_analysis.h:27
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
escape_domaint
Definition: escape_analysis.h:25
union_find.h
escape_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: escape_analysis.cpp:286
escape_domaint::make_entry
void make_entry() override final
Make this domain a reasonable entry-point state.
Definition: escape_analysis.h:79
escape_domaint::aliasest
union_find< irep_idt > aliasest
Definition: escape_analysis.h:84
threeval.h
union_find::size
size_t size() const
Definition: union_find.h:269
escape_domaint::check_lhs
void check_lhs(const exprt &, std::set< irep_idt > &) const
Definition: escape_analysis.cpp:388
template_numberingt
Definition: numbering.h:22
escape_domaint::cleanupt::cleanup_functions
std::set< irep_idt > cleanup_functions
Definition: escape_analysis.h:89
escape_domaint::get_rhs_aliases
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:117
escape_domaint::assign_lhs_cleanup
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:47
exprt
Base class for all expressions.
Definition: expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
goto_modelt
Definition: goto_model.h:26
escape_domaint::get_rhs_cleanup
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:87
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
union_find< irep_idt >
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
escape_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: escape_analysis.h:56
escape_analysist
Definition: escape_analysis.h:114
escape_domaint::aliases
aliasest aliases
Definition: escape_analysis.h:85
escape_domaint::get_function
irep_idt get_function(const exprt &)
Definition: escape_analysis.cpp:32
escape_analysist::initialize
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
Definition: escape_analysis.h:119
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
escape_domaint::cleanupt
Definition: escape_analysis.h:88
escape_domaint::get_rhs_aliases_address_of
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:149
escape_domaint::make_bottom
void make_bottom() final override
no states
Definition: escape_analysis.h:49
escape_domaint::is_top
bool is_top() const override final
Definition: escape_analysis.h:71
escape_domaint::merge
bool merge(const escape_domaint &b, locationt from, locationt to)
Definition: escape_analysis.cpp:332
union_find::clear
void clear()
Definition: union_find.h:248
escape_domaint::assign_lhs_aliases
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:66
escape_analysist::instrument
void instrument(goto_modelt &)
Definition: escape_analysis.cpp:458
escape_analysist::bits
numbering< irep_idt > bits
Definition: escape_analysis.h:123
numbering.h
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
tvt
Definition: threeval.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
escape_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Definition: escape_analysis.cpp:168
escape_domaint::has_values
tvt has_values
Definition: escape_analysis.h:99
escape_domaint::is_bottom
bool is_bottom() const override final
Definition: escape_analysis.h:63
escape_domaint::cleanup_mapt
std::map< irep_idt, cleanupt > cleanup_mapt
Definition: escape_analysis.h:95
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
escape_analysist::insert_cleanup
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
Definition: escape_analysis.cpp:423
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
escape_domaint::cleanup_map
cleanup_mapt cleanup_map
Definition: escape_analysis.h:96
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
tvt::is_true
bool is_true() const
Definition: threeval.h:25
escape_domaint::is_tracked
bool is_tracked(const symbol_exprt &)
Definition: escape_analysis.cpp:17