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  dirty(_goto_function),
31  locals(_goto_function),
32  cfg(_goto_function.body)
33  {
34  build(_goto_function);
35  }
36 
37  void output(
38  std::ostream &out,
39  const goto_functiont &goto_function,
40  const namespacet &ns) const;
41 
45 
46  // categories of things one can point to
47  struct flagst
48  {
49  flagst():bits(0)
50  {
51  }
52 
53  void clear()
54  {
55  bits=0;
56  }
57 
58  // the bits for the "bitvector analysis"
59  enum bitst
60  {
61  B_unknown=1<<0,
66  B_null=1<<5,
69  };
70 
71  explicit flagst(const bitst _bits):bits(_bits)
72  {
73  }
74 
75  unsigned bits;
76 
77  bool merge(const flagst &other)
78  {
79  unsigned old=bits;
80  bits|=other.bits; // bit-wise or
81  return old!=bits;
82  }
83 
84  static flagst mk_unknown()
85  {
86  return flagst(B_unknown);
87  }
88 
89  bool is_unknown() const
90  {
91  return (bits&B_unknown)!=0;
92  }
93 
95  {
96  return flagst(B_uninitialized);
97  }
98 
99  bool is_uninitialized() const
100  {
101  return (bits&B_uninitialized)!=0;
102  }
103 
105  {
106  return flagst(B_uses_offset);
107  }
108 
109  bool is_uses_offset() const
110  {
111  return (bits&B_uses_offset)!=0;
112  }
113 
115  {
116  return flagst(B_dynamic_local);
117  }
118 
119  bool is_dynamic_local() const
120  {
121  return (bits&B_dynamic_local)!=0;
122  }
123 
125  {
126  return flagst(B_dynamic_heap);
127  }
128 
129  bool is_dynamic_heap() const
130  {
131  return (bits&B_dynamic_heap)!=0;
132  }
133 
134  static flagst mk_null()
135  {
136  return flagst(B_null);
137  }
138 
139  bool is_null() const
140  {
141  return (bits&B_null)!=0;
142  }
143 
145  {
146  return flagst(B_static_lifetime);
147  }
148 
149  bool is_static_lifetime() const
150  {
151  return (bits&B_static_lifetime)!=0;
152  }
153 
155  {
156  return flagst(B_integer_address);
157  }
158 
159  bool is_integer_address() const
160  {
161  return (bits&B_integer_address)!=0;
162  }
163 
164  void print(std::ostream &) const;
165 
166  flagst operator|(const flagst other) const
167  {
168  flagst result(*this);
169  result.bits|=other.bits;
170  return result;
171  }
172  };
173 
174  flagst get(
176  const exprt &src);
177 
178 protected:
179  void build(const goto_functiont &goto_function);
180 
181  typedef std::stack<unsigned> work_queuet;
182 
184 
185  // pointers -> flagst
186  // This is a vector, so it's fast.
188 
189  // the information tracked per program location
190  class loc_infot
191  {
192  public:
194 
195  bool merge(const loc_infot &src);
196  };
197 
198  typedef std::vector<loc_infot> loc_infost;
200 
201  void assign_lhs(
202  const exprt &lhs,
203  const exprt &rhs,
204  const loc_infot &loc_info_src,
205  loc_infot &loc_info_dest);
206 
207  flagst get_rec(
208  const exprt &rhs,
209  const loc_infot &loc_info_src);
210 
211  bool is_tracked(const irep_idt &identifier);
212 };
213 
214 inline std::ostream &operator<<(
215  std::ostream &out,
217 {
218  flags.print(out);
219  return out;
220 }
221 
222 #endif // CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
void build(const goto_functiont &goto_function)
Variables whose address is taken.
bool is_tracked(const irep_idt &identifier)
goto_functionst::goto_functiont goto_functiont
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
Definition: locals.h:19
flagst operator|(const flagst other) const
CFG for One Function.
instructionst::const_iterator const_targett
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::vector< loc_infot > loc_infost
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
goto_function_templatet< goto_programt > goto_functiont
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
Base class for all expressions.
Definition: expr.h:46
expanding_vectort< flagst > points_tot
Definition: dirty.h:22
flagst get_rec(const exprt &rhs, const loc_infot &loc_info_src)
Local variables whose address is taken.
local_bitvector_analysist(const goto_functiont &_goto_function)
std::stack< unsigned > work_queuet