cprover
global_may_alias.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_GLOBAL_MAY_ALIAS_H
14 #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_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 
25 {
26 public:
28  {
29  }
30 
32  void transform(
33  const irep_idt &function_from,
34  locationt from,
35  const irep_idt &function_to,
36  locationt to,
37  ai_baset &ai,
38  const namespacet &ns) final override;
39 
45  void output(
46  std::ostream &out,
47  const ai_baset &ai,
48  const namespacet &ns) const final override;
49 
51  bool merge(
52  const global_may_alias_domaint &b,
53  locationt from,
54  locationt to);
55 
57  void make_bottom() final override
58  {
59  aliases.clear();
60  has_values=tvt(false);
61  }
62 
64  void make_top() final override
65  {
66  aliases.clear();
67  has_values=tvt(true);
68  }
69 
70  void make_entry() final override
71  {
72  make_top();
73  }
74 
76  bool is_bottom() const final override
77  {
79  "If the domain is bottom, there must be no aliases");
80  return has_values.is_false();
81  }
82 
84  bool is_top() const final override
85  {
87  "If the domain is top, there must be no aliases");
88  return has_values.is_true();
89  }
90 
93 
94 private:
96 
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 };
101 
106 class global_may_alias_analysist:public ait<global_may_alias_domaint>
107 {
108 protected:
109  virtual void initialize(const goto_functionst &)
110  {
111  }
112 };
113 
114 #endif // CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
global_may_alias_domaint::assign_lhs_aliases
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which an object is being written to.
Definition: global_may_alias.cpp:19
global_may_alias_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: global_may_alias.h:70
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
union_find.h
global_may_alias_domaint::is_bottom
bool is_bottom() const final override
Returns true if domain is bottom.
Definition: global_may_alias.h:76
threeval.h
union_find::size
size_t size() const
Definition: union_find.h:269
exprt
Base class for all expressions.
Definition: expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
global_may_alias_domaint::merge
bool merge(const global_may_alias_domaint &b, locationt from, locationt to)
Abstract Interpretation domain merge function.
Definition: global_may_alias.cpp:200
union_find< irep_idt >
global_may_alias_analysist::initialize
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
Definition: global_may_alias.h:109
global_may_alias_domaint::aliases
aliasest aliases
Definition: global_may_alias.h:92
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
union_find::clear
void clear()
Definition: union_find.h:248
numbering.h
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
global_may_alias_domaint::is_top
bool is_top() const final override
Returns false if domain is top.
Definition: global_may_alias.h:84
tvt
Definition: threeval.h:20
global_may_alias_analysist
This is a may analysis (i.e.
Definition: global_may_alias.h:107
global_may_alias_domaint::has_values
tvt has_values
Definition: global_may_alias.h:95
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
global_may_alias_domaint::global_may_alias_domaint
global_may_alias_domaint()
Definition: global_may_alias.h:27
global_may_alias_domaint::make_bottom
void make_bottom() final override
Clear list of aliases, and mark domain as bottom.
Definition: global_may_alias.h:57
global_may_alias_domaint::make_top
void make_top() final override
Clear list of aliases, and mark domain as top.
Definition: global_may_alias.h:64
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
global_may_alias_domaint
Definition: global_may_alias.h:25
global_may_alias_domaint::get_rhs_aliases_address_of
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.
Definition: global_may_alias.cpp:74
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
global_may_alias_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
Definition: global_may_alias.cpp:162
global_may_alias_domaint::aliasest
union_find< irep_idt > aliasest
Definition: global_may_alias.h:91
global_may_alias_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Abstract Interpretation domain transform function.
Definition: global_may_alias.cpp:93
global_may_alias_domaint::get_rhs_aliases
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which is an object is being read.
Definition: global_may_alias.cpp:41
tvt::is_true
bool is_true() const
Definition: threeval.h:25