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  locationt from,
33  locationt to,
34  ai_baset &ai,
35  const namespacet &ns) final;
36 
37  void output(
38  std::ostream &out,
39  const ai_baset &ai,
40  const namespacet &ns) const final;
41 
42  bool merge(
43  const escape_domaint &b,
44  locationt from,
45  locationt to);
46 
47  void make_bottom() final
48  {
49  cleanup_map.clear();
50  aliases.clear();
51  has_values=tvt(false);
52  }
53 
54  void make_top() final
55  {
56  cleanup_map.clear();
57  aliases.clear();
58  has_values=tvt(true);
59  }
60 
61  void make_entry() final
62  {
63  make_top();
64  }
65 
67  aliasest aliases;
68 
69  struct cleanupt
70  {
71  std::set<irep_idt> cleanup_functions;
72  };
73 
74  // We track a set of 'cleanup functions' for specific
75  // identifiers. The cleanup functions are executed
76  // once the last pointer to an object is lost.
77  typedef std::map<irep_idt, cleanupt> cleanup_mapt;
78  cleanup_mapt cleanup_map;
79 
80 private:
82  void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
83  void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
84  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
85  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
86  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
87  irep_idt get_function(const exprt &);
88  void check_lhs(const exprt &, std::set<irep_idt> &);
89 
90  friend class escape_analysist;
91 
92  bool is_tracked(const symbol_exprt &);
93 };
94 
95 class escape_analysist:public ait<escape_domaint>
96 {
97 public:
98  void instrument(
100  const namespacet &);
101 
102 protected:
103  virtual void initialize(const goto_functionst &_goto_functions)
104  {
105  }
106 
108 
109  void insert_cleanup(
112  const exprt &,
113  const std::set<irep_idt> &,
114  bool is_object,
115  const namespacet &);
116 };
117 
118 #endif // CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: ai.h:342
void make_top() final
numbering< irep_idt > bits
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
union_find< irep_idt > aliasest
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
void make_entry() final
Definition: threeval.h:19
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::set< irep_idt > cleanup_functions
cleanup_mapt cleanup_map
goto_function_templatet< goto_programt > goto_functiont
void clear()
Definition: union_find.h:238
virtual void initialize(const goto_functionst &_goto_functions)
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &)
Abstract Interpretation.
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
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.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
void make_bottom() final