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 
23 {
24 public:
26  {
27  }
28 
29  void transform(
30  const irep_idt &function_from,
31  trace_ptrt trace_from,
32  const irep_idt &function_to,
33  trace_ptrt trace_to,
34  ai_baset &ai,
35  const namespacet &ns) final override;
36 
37  void output(
38  std::ostream &out,
39  const ai_baset &ai,
40  const namespacet &ns) const final override;
41 
42  bool merge(const escape_domaint &b, trace_ptrt from, trace_ptrt to);
43 
44  void make_bottom() final override
45  {
46  cleanup_map.clear();
47  aliases.clear();
48  has_values=tvt(false);
49  }
50 
51  void make_top() final override
52  {
53  cleanup_map.clear();
54  aliases.clear();
55  has_values=tvt(true);
56  }
57 
58  bool is_bottom() const override final
59  {
61  (cleanup_map.empty() && (aliases.size()==0)),
62  "If the domain is bottom, all maps must be empty");
63  return has_values.is_false();
64  }
65 
66  bool is_top() const override final
67  {
69  (cleanup_map.empty() && (aliases.size()==0)),
70  "If the domain is top, all maps must be empty");
71  return has_values.is_true();
72  }
73 
74  void make_entry() override final
75  {
76  make_top();
77  }
78 
81 
82  struct cleanupt
83  {
84  std::set<irep_idt> cleanup_functions;
85  };
86 
87  // We track a set of 'cleanup functions' for specific
88  // identifiers. The cleanup functions are executed
89  // once the last pointer to an object is lost.
90  typedef std::map<irep_idt, cleanupt> cleanup_mapt;
92 
93 private:
95  void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
96  void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
97  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
98  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
99  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
100  irep_idt get_function(const exprt &);
101  void check_lhs(const exprt &, std::set<irep_idt> &) const;
102 
103  friend class escape_analysist;
104 
105  bool is_tracked(const symbol_exprt &);
106 };
107 
108 class escape_analysist:public ait<escape_domaint>
109 {
110 public:
111  void instrument(goto_modelt &);
112 
113 protected:
114  virtual void initialize(const goto_functionst &)
115  {
116  }
117 
119 
120  void insert_cleanup(
123  const exprt &,
124  const std::set<irep_idt> &,
125  bool is_object,
126  const namespacet &);
127 };
128 
129 #endif // CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void instrument(goto_modelt &)
numberingt< irep_idt > bits
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
void make_bottom() final override
no states
bool is_bottom() const override final
bool is_top() const override final
std::map< irep_idt, cleanupt > cleanup_mapt
bool merge(const escape_domaint &b, trace_ptrt from, trace_ptrt to)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &) const
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
irep_idt get_function(const exprt &)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
cleanup_mapt cleanup_map
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
bool is_tracked(const symbol_exprt &)
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void make_entry() override final
Make this domain a reasonable entry-point state.
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
union_find< irep_idt > aliasest
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
::goto_functiont goto_functiont
instructionst::iterator targett
Definition: goto_program.h:592
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
size_t size() const
Definition: union_find.h:268
void clear()
Definition: union_find.h:247
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
std::set< irep_idt > cleanup_functions