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
32  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
33  final override;
34 
35  void output(
36  std::ostream &out,
37  const ai_baset &ai,
38  const namespacet &ns) const final override;
39 
40  bool merge(
41  const escape_domaint &b,
42  locationt from,
43  locationt to);
44 
45  void make_bottom() final override
46  {
47  cleanup_map.clear();
48  aliases.clear();
49  has_values=tvt(false);
50  }
51 
52  void make_top() final override
53  {
54  cleanup_map.clear();
55  aliases.clear();
56  has_values=tvt(true);
57  }
58 
59  bool is_bottom() const override final
60  {
62  (cleanup_map.empty() && (aliases.size()==0)),
63  "If the domain is bottom, all maps must be empty");
64  return has_values.is_false();
65  }
66 
67  bool is_top() const override final
68  {
70  (cleanup_map.empty() && (aliases.size()==0)),
71  "If the domain is top, all maps must be empty");
72  return has_values.is_true();
73  }
74 
75  void make_entry() override final
76  {
77  make_top();
78  }
79 
82 
83  struct cleanupt
84  {
85  std::set<irep_idt> cleanup_functions;
86  };
87 
88  // We track a set of 'cleanup functions' for specific
89  // identifiers. The cleanup functions are executed
90  // once the last pointer to an object is lost.
91  typedef std::map<irep_idt, cleanupt> cleanup_mapt;
93 
94 private:
96  void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
97  void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
98  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
99  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
100  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
101  irep_idt get_function(const exprt &);
102  void check_lhs(const exprt &, std::set<irep_idt> &);
103 
104  friend class escape_analysist;
105 
106  bool is_tracked(const symbol_exprt &);
107 };
108 
109 class escape_analysist:public ait<escape_domaint>
110 {
111 public:
112  void instrument(goto_modelt &);
113 
114 protected:
115  virtual void initialize(const goto_functionst &)
116  {
117  }
118 
120 
121  void insert_cleanup(
124  const exprt &,
125  const std::set<irep_idt> &,
126  bool is_object,
127  const namespacet &);
128 };
129 
130 #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 &)
void make_entry() override final
a reasonable entry-point state
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: ai.h:294
size_t size() const
Definition: union_find.h:265
void transform(locationt from, 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 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:397
Definition: threeval.h:19
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
std::set< irep_idt > cleanup_functions
cleanup_mapt cleanup_map
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool is_top() const override final
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it.
bool is_true() const
Definition: threeval.h:25
void clear()
Definition: union_find.h:244
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:42
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:90
void instrument(goto_modelt &)
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
bool is_bottom() const override final