CBMC
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 {
24 public:
26  {
27  }
28 
30  void transform(
31  const irep_idt &function_from,
32  trace_ptrt trace_from,
33  const irep_idt &function_to,
34  trace_ptrt trace_to,
35  ai_baset &ai,
36  const namespacet &ns) final override;
37 
43  void output(
44  std::ostream &out,
45  const ai_baset &ai,
46  const namespacet &ns) const final override;
47 
49  bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to);
50 
52  void make_bottom() final override
53  {
54  aliases.clear();
55  has_values=tvt(false);
56  }
57 
59  void make_top() final override
60  {
61  aliases.clear();
62  has_values=tvt(true);
63  }
64 
66  bool is_bottom() const final override
67  {
69  "If the domain is bottom, there must be no aliases");
70  return has_values.is_false();
71  }
72 
74  bool is_top() const final override
75  {
77  "If the domain is top, there must be no aliases");
78  return has_values.is_true();
79  }
80 
83 
84 private:
86 
87  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
88  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
89  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
90 };
91 
96 class global_may_alias_analysist:public ait<global_may_alias_domaint>
97 {
98 protected:
99  virtual void initialize(const goto_functionst &)
100  {
101  }
102 };
103 
104 #endif // CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:54
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:73
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
This is a may analysis (i.e.
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
bool is_bottom() const final override
Returns true if domain is bottom.
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
Abstract Interpretation domain transform function.
union_find< irep_idt > aliasest
void make_bottom() final override
Clear list of aliases, and mark domain as bottom.
void make_top() final override
Clear list of aliases, and mark domain as top.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
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.
bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
Abstract Interpretation domain merge function.
bool is_top() const final override
Returns false if domain is top.
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.
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.
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:534