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();
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();
180 
181  typedef std::stack<unsigned> work_queuet;
182 
184 
185  // pointers -> flagst
186  // This is a vector, so it's fast.
188 
189  static bool merge(points_tot &a, points_tot &b);
190 
191  typedef std::vector<points_tot> loc_infost;
193 
194  void assign_lhs(
195  const exprt &lhs,
196  const exprt &rhs,
197  points_tot &loc_info_src,
198  points_tot &loc_info_dest);
199 
200  flagst get_rec(
201  const exprt &rhs,
202  points_tot &loc_info_src);
203 
204  bool is_tracked(const irep_idt &identifier);
205 };
206 
207 inline std::ostream &operator<<(
208  std::ostream &out,
210 {
211  flags.print(out);
212  return out;
213 }
214 
215 #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:35
localst
Definition: locals.h:19
local_bitvector_analysist::flagst::B_null
Definition: local_bitvector_analysis.h:66
local_bitvector_analysist::flagst::flagst
flagst(const bitst _bits)
Definition: local_bitvector_analysis.h:71
dirty.h
local_bitvector_analysist::points_tot
expanding_vectort< flagst > points_tot
Definition: local_bitvector_analysis.h:187
local_bitvector_analysist::flagst::mk_null
static flagst mk_null()
Definition: local_bitvector_analysis.h:134
dirtyt
Definition: dirty.h:23
local_bitvector_analysist::flagst::flagst
flagst()
Definition: local_bitvector_analysis.h:49
local_bitvector_analysist::flagst::mk_dynamic_local
static flagst mk_dynamic_local()
Definition: local_bitvector_analysis.h:114
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:72
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:129
template_numberingt
Definition: numbering.h:21
local_bitvector_analysist::flagst::B_dynamic_local
Definition: local_bitvector_analysis.h:64
local_bitvector_analysist::flagst::clear
void clear()
Definition: local_bitvector_analysis.h:53
local_bitvector_analysist::flagst::bits
unsigned bits
Definition: local_bitvector_analysis.h:75
local_bitvector_analysist::build
void build()
Definition: local_bitvector_analysis.cpp:244
exprt
Base class for all expressions.
Definition: expr.h:54
local_bitvector_analysist::flagst::B_uses_offset
Definition: local_bitvector_analysis.h:63
local_bitvector_analysist::flagst::B_uninitialized
Definition: local_bitvector_analysis.h:62
local_cfgt
Definition: local_cfg.h:19
local_bitvector_analysist::flagst::merge
bool merge(const flagst &other)
Definition: local_bitvector_analysis.h:77
local_bitvector_analysist::flagst::mk_unknown
static flagst mk_unknown()
Definition: local_bitvector_analysis.h:84
local_bitvector_analysist::is_tracked
bool is_tracked(const irep_idt &identifier)
Definition: local_bitvector_analysis.cpp:61
expanding_vectort
Definition: expanding_vector.h:16
local_bitvector_analysist::loc_infos
loc_infost loc_infos
Definition: local_bitvector_analysis.h:192
local_bitvector_analysist::cfg
local_cfgt cfg
Definition: local_bitvector_analysis.h:44
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
local_bitvector_analysist::flagst::bitst
bitst
Definition: local_bitvector_analysis.h:59
local_bitvector_analysist::flagst::B_unknown
Definition: local_bitvector_analysis.h:61
local_bitvector_analysist::flagst::B_dynamic_heap
Definition: local_bitvector_analysis.h:65
local_bitvector_analysist::flagst::operator|
flagst operator|(const flagst other) const
Definition: local_bitvector_analysis.h:166
local_bitvector_analysist::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: local_bitvector_analysis.h:26
local_bitvector_analysist::get_rec
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
Definition: local_bitvector_analysis.cpp:123
locals.h
local_bitvector_analysist::locals
localst locals
Definition: local_bitvector_analysis.h:43
local_bitvector_analysist::flagst::mk_integer_address
static flagst mk_integer_address()
Definition: local_bitvector_analysis.h:154
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:159
local_cfg.h
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:139
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:149
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
local_bitvector_analysist::loc_infost
std::vector< points_tot > loc_infost
Definition: local_bitvector_analysis.h:191
local_bitvector_analysist::flagst::mk_dynamic_heap
static flagst mk_dynamic_heap()
Definition: local_bitvector_analysis.h:124
expanding_vector.h
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:327
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:119
local_bitvector_analysist::work_queuet
std::stack< unsigned > work_queuet
Definition: local_bitvector_analysis.h:181
local_bitvector_analysist::pointers
numbering< irep_idt > pointers
Definition: local_bitvector_analysis.h:183
local_bitvector_analysist::flagst::mk_uninitialized
static flagst mk_uninitialized()
Definition: local_bitvector_analysis.h:94
local_bitvector_analysist::flagst::is_uses_offset
bool is_uses_offset() const
Definition: local_bitvector_analysis.h:109
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
local_bitvector_analysist
Definition: local_bitvector_analysis.h:23
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:89
local_bitvector_analysist::dirty
dirtyt dirty
Definition: local_bitvector_analysis.h:42
local_bitvector_analysist::flagst::mk_uses_offset
static flagst mk_uses_offset()
Definition: local_bitvector_analysis.h:104
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:47
local_bitvector_analysist::flagst::print
void print(std::ostream &) const
Definition: local_bitvector_analysis.cpp:24
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:99
local_bitvector_analysist::flagst::B_integer_address
Definition: local_bitvector_analysis.h:68
local_bitvector_analysist::flagst::B_static_lifetime
Definition: local_bitvector_analysis.h:67
local_bitvector_analysist::get
flagst get(const goto_programt::const_targett t, const exprt &src)
Definition: local_bitvector_analysis.cpp:112
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
local_bitvector_analysist::local_bitvector_analysist
local_bitvector_analysist(const goto_functiont &_goto_function)
Definition: local_bitvector_analysis.h:28
operator<<
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
Definition: local_bitvector_analysis.h:207
local_bitvector_analysist::merge
static bool merge(points_tot &a, points_tot &b)
Definition: local_bitvector_analysis.cpp:44
local_bitvector_analysist::flagst::mk_static_lifetime
static flagst mk_static_lifetime()
Definition: local_bitvector_analysis.h:144