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 #include <util/numbering.h>
19 
20 #include "locals.h"
21 #include "dirty.h"
22 #include "local_cfg.h"
23 
25 {
26 public:
28 
30  const goto_functiont &_goto_function,
31  const namespacet &ns)
32  : dirty(_goto_function),
33  locals(_goto_function),
34  cfg(_goto_function.body),
35  ns(ns)
36  {
37  build();
38  }
39 
40  void output(
41  std::ostream &out,
42  const goto_functiont &goto_function,
43  const namespacet &ns) const;
44 
48 
49  // categories of things one can point to
50  struct flagst
51  {
52  flagst():bits(0)
53  {
54  }
55 
56  void clear()
57  {
58  bits=0;
59  }
60 
61  // the bits for the "bitvector analysis"
62  enum bitst
63  {
64  B_unknown=1<<0,
69  B_null=1<<5,
72  };
73 
74  explicit flagst(const bitst _bits):bits(_bits)
75  {
76  }
77 
78  unsigned bits;
79 
80  bool merge(const flagst &other)
81  {
82  unsigned old=bits;
83  bits|=other.bits; // bit-wise or
84  return old!=bits;
85  }
86 
87  static flagst mk_unknown()
88  {
89  return flagst(B_unknown);
90  }
91 
92  bool is_unknown() const
93  {
94  return (bits&B_unknown)!=0;
95  }
96 
98  {
99  return flagst(B_uninitialized);
100  }
101 
102  bool is_uninitialized() const
103  {
104  return (bits&B_uninitialized)!=0;
105  }
106 
108  {
109  return flagst(B_uses_offset);
110  }
111 
112  bool is_uses_offset() const
113  {
114  return (bits&B_uses_offset)!=0;
115  }
116 
118  {
119  return flagst(B_dynamic_local);
120  }
121 
122  bool is_dynamic_local() const
123  {
124  return (bits&B_dynamic_local)!=0;
125  }
126 
128  {
129  return flagst(B_dynamic_heap);
130  }
131 
132  bool is_dynamic_heap() const
133  {
134  return (bits&B_dynamic_heap)!=0;
135  }
136 
137  static flagst mk_null()
138  {
139  return flagst(B_null);
140  }
141 
142  bool is_null() const
143  {
144  return (bits&B_null)!=0;
145  }
146 
148  {
149  return flagst(B_static_lifetime);
150  }
151 
152  bool is_static_lifetime() const
153  {
154  return (bits&B_static_lifetime)!=0;
155  }
156 
158  {
159  return flagst(B_integer_address);
160  }
161 
162  bool is_integer_address() const
163  {
164  return (bits&B_integer_address)!=0;
165  }
166 
167  void print(std::ostream &) const;
168 
169  flagst operator|(const flagst other) const
170  {
171  flagst result(*this);
172  result.bits|=other.bits;
173  return result;
174  }
175  };
176 
177  flagst get(
179  const exprt &src);
180 
181 protected:
182  const namespacet &ns;
183  void build();
184 
185  typedef std::stack<unsigned> work_queuet;
186 
188 
189  // pointers -> flagst
190  // This is a vector, so it's fast.
192 
193  static bool merge(points_tot &a, points_tot &b);
194 
195  typedef std::vector<points_tot> loc_infost;
197 
198  void assign_lhs(
199  const exprt &lhs,
200  const exprt &rhs,
201  points_tot &loc_info_src,
202  points_tot &loc_info_dest);
203 
204  flagst get_rec(
205  const exprt &rhs,
206  points_tot &loc_info_src);
207 
208  bool is_tracked(const irep_idt &identifier);
209 };
210 
211 inline std::ostream &operator<<(
212  std::ostream &out,
214 {
215  flags.print(out);
216  return out;
217 }
218 
219 #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:24
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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:25
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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