cprover
local_bitvector_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive bitvector analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
13 #define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
14 
15 #include <stack>
16 
17 #include <util/expanding_vector.h>
18 
19 #include "locals.h"
20 #include "dirty.h"
21 #include "local_cfg.h"
22 
24 {
25 public:
27 
29  const goto_functiont &_goto_function,
30  const namespacet &ns)
31  : dirty(_goto_function),
32  locals(_goto_function),
33  cfg(_goto_function.body),
34  ns(ns)
35  {
36  build();
37  }
38 
39  void output(
40  std::ostream &out,
41  const goto_functiont &goto_function,
42  const namespacet &ns) const;
43 
47 
48  // categories of things one can point to
49  struct flagst
50  {
51  flagst():bits(0)
52  {
53  }
54 
55  void clear()
56  {
57  bits=0;
58  }
59 
60  // the bits for the "bitvector analysis"
61  enum bitst
62  {
63  B_unknown=1<<0,
68  B_null=1<<5,
71  };
72 
73  explicit flagst(const bitst _bits):bits(_bits)
74  {
75  }
76 
77  unsigned bits;
78 
79  bool merge(const flagst &other)
80  {
81  unsigned old=bits;
82  bits|=other.bits; // bit-wise or
83  return old!=bits;
84  }
85 
86  static flagst mk_unknown()
87  {
88  return flagst(B_unknown);
89  }
90 
91  bool is_unknown() const
92  {
93  return (bits&B_unknown)!=0;
94  }
95 
97  {
98  return flagst(B_uninitialized);
99  }
100 
101  bool is_uninitialized() const
102  {
103  return (bits&B_uninitialized)!=0;
104  }
105 
107  {
108  return flagst(B_uses_offset);
109  }
110 
111  bool is_uses_offset() const
112  {
113  return (bits&B_uses_offset)!=0;
114  }
115 
117  {
118  return flagst(B_dynamic_local);
119  }
120 
121  bool is_dynamic_local() const
122  {
123  return (bits&B_dynamic_local)!=0;
124  }
125 
127  {
128  return flagst(B_dynamic_heap);
129  }
130 
131  bool is_dynamic_heap() const
132  {
133  return (bits&B_dynamic_heap)!=0;
134  }
135 
136  static flagst mk_null()
137  {
138  return flagst(B_null);
139  }
140 
141  bool is_null() const
142  {
143  return (bits&B_null)!=0;
144  }
145 
147  {
148  return flagst(B_static_lifetime);
149  }
150 
151  bool is_static_lifetime() const
152  {
153  return (bits&B_static_lifetime)!=0;
154  }
155 
157  {
158  return flagst(B_integer_address);
159  }
160 
161  bool is_integer_address() const
162  {
163  return (bits&B_integer_address)!=0;
164  }
165 
166  void print(std::ostream &) const;
167 
168  flagst operator|(const flagst other) const
169  {
170  flagst result(*this);
171  result.bits|=other.bits;
172  return result;
173  }
174  };
175 
176  flagst get(
178  const exprt &src);
179 
180 protected:
181  const namespacet &ns;
182  void build();
183 
184  typedef std::stack<unsigned> work_queuet;
185 
187 
188  // pointers -> flagst
189  // This is a vector, so it's fast.
191 
192  static bool merge(points_tot &a, points_tot &b);
193 
194  typedef std::vector<points_tot> loc_infost;
196 
197  void assign_lhs(
198  const exprt &lhs,
199  const exprt &rhs,
200  points_tot &loc_info_src,
201  points_tot &loc_info_dest);
202 
203  flagst get_rec(
204  const exprt &rhs,
205  points_tot &loc_info_src);
206 
207  bool is_tracked(const irep_idt &identifier);
208 };
209 
210 inline std::ostream &operator<<(
211  std::ostream &out,
213 {
214  flags.print(out);
215  return out;
216 }
217 
218 #endif // CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
instructionst::const_iterator const_targett
Definition: goto_program.h:551
std::stack< unsigned > work_queuet
std::vector< points_tot > loc_infost
expanding_vectort< flagst > points_tot
static bool merge(points_tot &a, points_tot &b)
goto_functionst::goto_functiont goto_functiont
local_bitvector_analysist(const goto_functiont &_goto_function, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
bool is_tracked(const irep_idt &identifier)
Definition: locals.h:20
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Variables whose address is taken.
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
CFG for One Function.
Local variables whose address is taken.
flagst operator|(const flagst other) const