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> &);
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
bool is_false() const
Definition: threeval.h:26
void make_bottom() final override
no states
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
void make_entry() override final
Make this domain a reasonable entry-point state.
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: ai.h:365
size_t size() const
Definition: union_find.h:269
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
numbering< irep_idt > bits
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
union_find< irep_idt > aliasest
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
instructionst::iterator targett
Definition: goto_program.h:414
Definition: threeval.h:19
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
std::set< irep_idt > cleanup_functions
cleanup_mapt cleanup_map
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bool is_top() const override final
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
bool is_true() const
Definition: threeval.h:25
void clear()
Definition: union_find.h:248
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &)
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
bool merge(const escape_domaint &b, locationt from, locationt to)
std::map< irep_idt, cleanupt > cleanup_mapt
irep_idt get_function(const exprt &)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void instrument(goto_modelt &)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
bool is_bottom() const override final