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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
local_bitvector_analysist::local_bitvector_analysist
local_bitvector_analysist(const goto_functiont &_goto_function, const namespacet &ns)
Definition: local_bitvector_analysis.h:29
localst
Definition: locals.h:25
local_bitvector_analysist::flagst::B_null
@ B_null
Definition: local_bitvector_analysis.h:69
local_bitvector_analysist::flagst::flagst
flagst(const bitst _bits)
Definition: local_bitvector_analysis.h:74
local_bitvector_analysist::ns
const namespacet & ns
Definition: local_bitvector_analysis.h:182
dirty.h
Variables whose address is taken.
local_bitvector_analysist::points_tot
expanding_vectort< flagst > points_tot
Definition: local_bitvector_analysis.h:191
local_bitvector_analysist::flagst::mk_null
static flagst mk_null()
Definition: local_bitvector_analysis.h:137
dirtyt
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
local_bitvector_analysist::flagst::flagst
flagst()
Definition: local_bitvector_analysis.h:52
local_bitvector_analysist::flagst::mk_dynamic_local
static flagst mk_dynamic_local()
Definition: local_bitvector_analysis.h:117
local_bitvector_analysist::assign_lhs
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
Definition: local_bitvector_analysis.cpp:64
numberingt< irep_idt >
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:132
local_bitvector_analysist::flagst::B_dynamic_local
@ B_dynamic_local
Definition: local_bitvector_analysis.h:67
local_bitvector_analysist::flagst::clear
void clear()
Definition: local_bitvector_analysis.h:56
local_bitvector_analysist::flagst::bits
unsigned bits
Definition: local_bitvector_analysis.h:78
local_bitvector_analysist::build
void build()
Definition: local_bitvector_analysis.cpp:240
exprt
Base class for all expressions.
Definition: expr.h:54
local_bitvector_analysist::flagst::B_uses_offset
@ B_uses_offset
Definition: local_bitvector_analysis.h:66
local_bitvector_analysist::flagst::B_uninitialized
@ B_uninitialized
Definition: local_bitvector_analysis.h:65
local_cfgt
Definition: local_cfg.h:20
local_bitvector_analysist::flagst::merge
bool merge(const flagst &other)
Definition: local_bitvector_analysis.h:80
local_bitvector_analysist::flagst::mk_unknown
static flagst mk_unknown()
Definition: local_bitvector_analysis.h:87
local_bitvector_analysist::is_tracked
bool is_tracked(const irep_idt &identifier)
Definition: local_bitvector_analysis.cpp:57
expanding_vectort
Definition: expanding_vector.h:17
local_bitvector_analysist::pointers
numberingt< irep_idt > pointers
Definition: local_bitvector_analysis.h:187
local_bitvector_analysist::loc_infos
loc_infost loc_infos
Definition: local_bitvector_analysis.h:196
local_bitvector_analysist::cfg
local_cfgt cfg
Definition: local_bitvector_analysis.h:47
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
local_bitvector_analysist::flagst::bitst
bitst
Definition: local_bitvector_analysis.h:63
local_bitvector_analysist::flagst::B_unknown
@ B_unknown
Definition: local_bitvector_analysis.h:64
local_bitvector_analysist::flagst::B_dynamic_heap
@ B_dynamic_heap
Definition: local_bitvector_analysis.h:68
local_bitvector_analysist::flagst::operator|
flagst operator|(const flagst other) const
Definition: local_bitvector_analysis.h:169
local_bitvector_analysist::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: local_bitvector_analysis.h:27
local_bitvector_analysist::get_rec
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
Definition: local_bitvector_analysis.cpp:115
locals.h
Local variables whose address is taken.
local_bitvector_analysist::locals
localst locals
Definition: local_bitvector_analysis.h:46
local_bitvector_analysist::flagst::mk_integer_address
static flagst mk_integer_address()
Definition: local_bitvector_analysis.h:157
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:162
local_cfg.h
CFG for One Function.
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:142
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:152
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
local_bitvector_analysist::loc_infost
std::vector< points_tot > loc_infost
Definition: local_bitvector_analysis.h:195
local_bitvector_analysist::flagst::mk_dynamic_heap
static flagst mk_dynamic_heap()
Definition: local_bitvector_analysis.h:127
expanding_vector.h
numbering.h
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:346
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:122
local_bitvector_analysist::work_queuet
std::stack< unsigned > work_queuet
Definition: local_bitvector_analysis.h:185
local_bitvector_analysist::flagst::mk_uninitialized
static flagst mk_uninitialized()
Definition: local_bitvector_analysis.h:97
local_bitvector_analysist::flagst::is_uses_offset
bool is_uses_offset() const
Definition: local_bitvector_analysis.h:112
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
local_bitvector_analysist
Definition: local_bitvector_analysis.h:25
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:92
local_bitvector_analysist::dirty
dirtyt dirty
Definition: local_bitvector_analysis.h:45
local_bitvector_analysist::flagst::mk_uses_offset
static flagst mk_uses_offset()
Definition: local_bitvector_analysis.h:107
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:51
local_bitvector_analysist::flagst::print
void print(std::ostream &) const
Definition: local_bitvector_analysis.cpp:20
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:102
local_bitvector_analysist::flagst::B_integer_address
@ B_integer_address
Definition: local_bitvector_analysis.h:71
local_bitvector_analysist::flagst::B_static_lifetime
@ B_static_lifetime
Definition: local_bitvector_analysis.h:70
local_bitvector_analysist::get
flagst get(const goto_programt::const_targett t, const exprt &src)
Definition: local_bitvector_analysis.cpp:104
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
operator<<
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
Definition: local_bitvector_analysis.h:211
local_bitvector_analysist::merge
static bool merge(points_tot &a, points_tot &b)
Definition: local_bitvector_analysis.cpp:40
local_bitvector_analysist::flagst::mk_static_lifetime
static flagst mk_static_lifetime()
Definition: local_bitvector_analysis.h:147