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  trace_ptrt trace_from,
34  const irep_idt &function_to,
35  trace_ptrt trace_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(const escape_domaint &b, trace_ptrt from, trace_ptrt to);
45 
46  void make_bottom() final override
47  {
48  cleanup_map.clear();
49  aliases.clear();
50  has_values=tvt(false);
51  }
52 
53  void make_top() final override
54  {
55  cleanup_map.clear();
56  aliases.clear();
57  has_values=tvt(true);
58  }
59 
60  bool is_bottom() const override final
61  {
63  (cleanup_map.empty() && (aliases.size()==0)),
64  "If the domain is bottom, all maps must be empty");
65  return has_values.is_false();
66  }
67 
68  bool is_top() const override final
69  {
71  (cleanup_map.empty() && (aliases.size()==0)),
72  "If the domain is top, all maps must be empty");
73  return has_values.is_true();
74  }
75 
76  void make_entry() override final
77  {
78  make_top();
79  }
80 
83 
84  struct cleanupt
85  {
86  std::set<irep_idt> cleanup_functions;
87  };
88 
89  // We track a set of 'cleanup functions' for specific
90  // identifiers. The cleanup functions are executed
91  // once the last pointer to an object is lost.
92  typedef std::map<irep_idt, cleanupt> cleanup_mapt;
94 
95 private:
97  void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
98  void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
99  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
100  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
101  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
102  irep_idt get_function(const exprt &);
103  void check_lhs(const exprt &, std::set<irep_idt> &) const;
104 
105  friend class escape_analysist;
106 
107  bool is_tracked(const symbol_exprt &);
108 };
109 
110 class escape_analysist:public ait<escape_domaint>
111 {
112 public:
113  void instrument(goto_modelt &);
114 
115 protected:
116  virtual void initialize(const goto_functionst &)
117  {
118  }
119 
121 
122  void insert_cleanup(
125  const exprt &,
126  const std::set<irep_idt> &,
127  bool is_object,
128  const namespacet &);
129 };
130 
131 #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:283
escape_domaint::make_entry
void make_entry() override final
Make this domain a reasonable entry-point state.
Definition: escape_analysis.h:76
escape_domaint::aliasest
union_find< irep_idt > aliasest
Definition: escape_analysis.h:81
threeval.h
numberingt< irep_idt >
escape_domaint::check_lhs
void check_lhs(const exprt &, std::set< irep_idt > &) const
Definition: escape_analysis.cpp:382
escape_domaint::cleanupt::cleanup_functions
std::set< irep_idt > cleanup_functions
Definition: escape_analysis.h:86
escape_domaint::get_rhs_aliases
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:118
escape_domaint::assign_lhs_cleanup
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:48
exprt
Base class for all expressions.
Definition: expr.h:54
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
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:88
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
union_find< irep_idt >
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
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:53
union_find::clear
void clear()
Definition: union_find.h:247
escape_analysist
Definition: escape_analysis.h:111
escape_domaint::aliases
aliasest aliases
Definition: escape_analysis.h:82
escape_domaint::get_function
irep_idt get_function(const exprt &)
Definition: escape_analysis.cpp:33
escape_analysist::initialize
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
Definition: escape_analysis.h:116
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::merge
bool merge(const escape_domaint &b, trace_ptrt from, trace_ptrt to)
Definition: escape_analysis.cpp:329
escape_domaint::cleanupt
Definition: escape_analysis.h:85
escape_domaint::get_rhs_aliases_address_of
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:150
escape_domaint::make_bottom
void make_bottom() final override
no states
Definition: escape_analysis.h:46
escape_domaint::is_top
bool is_top() const override final
Definition: escape_analysis.h:68
escape_domaint::assign_lhs_aliases
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:67
escape_analysist::instrument
void instrument(goto_modelt &)
Definition: escape_analysis.cpp:452
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
escape_domaint::has_values
tvt has_values
Definition: escape_analysis.h:96
union_find::size
size_t size() const
Definition: union_find.h:268
escape_analysist::bits
numberingt< irep_idt > bits
Definition: escape_analysis.h:120
escape_domaint::is_bottom
bool is_bottom() const override final
Definition: escape_analysis.h:60
escape_domaint::cleanup_mapt
std::map< irep_idt, cleanupt > cleanup_mapt
Definition: escape_analysis.h:92
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
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:417
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
escape_domaint::transform
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...
Definition: escape_analysis.cpp:169
escape_domaint::cleanup_map
cleanup_mapt cleanup_map
Definition: escape_analysis.h:93
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
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:18