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
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:28
localst
Definition: locals.h:20
local_bitvector_analysist::flagst::B_null
@ B_null
Definition: local_bitvector_analysis.h:68
local_bitvector_analysist::flagst::flagst
flagst(const bitst _bits)
Definition: local_bitvector_analysis.h:73
local_bitvector_analysist::ns
const namespacet & ns
Definition: local_bitvector_analysis.h:181
dirty.h
Variables whose address is taken.
local_bitvector_analysist::points_tot
expanding_vectort< flagst > points_tot
Definition: local_bitvector_analysis.h:190
local_bitvector_analysist::flagst::mk_null
static flagst mk_null()
Definition: local_bitvector_analysis.h:136
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:51
local_bitvector_analysist::flagst::mk_dynamic_local
static flagst mk_dynamic_local()
Definition: local_bitvector_analysis.h:116
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:68
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:131
template_numberingt
Definition: numbering.h:22
local_bitvector_analysist::flagst::B_dynamic_local
@ B_dynamic_local
Definition: local_bitvector_analysis.h:66
local_bitvector_analysist::flagst::clear
void clear()
Definition: local_bitvector_analysis.h:55
local_bitvector_analysist::flagst::bits
unsigned bits
Definition: local_bitvector_analysis.h:77
local_bitvector_analysist::build
void build()
Definition: local_bitvector_analysis.cpp:244
exprt
Base class for all expressions.
Definition: expr.h:53
local_bitvector_analysist::flagst::B_uses_offset
@ B_uses_offset
Definition: local_bitvector_analysis.h:65
local_bitvector_analysist::flagst::B_uninitialized
@ B_uninitialized
Definition: local_bitvector_analysis.h:64
local_cfgt
Definition: local_cfg.h:20
local_bitvector_analysist::flagst::merge
bool merge(const flagst &other)
Definition: local_bitvector_analysis.h:79
local_bitvector_analysist::flagst::mk_unknown
static flagst mk_unknown()
Definition: local_bitvector_analysis.h:86
local_bitvector_analysist::is_tracked
bool is_tracked(const irep_idt &identifier)
Definition: local_bitvector_analysis.cpp:61
expanding_vectort
Definition: expanding_vector.h:17
local_bitvector_analysist::loc_infos
loc_infost loc_infos
Definition: local_bitvector_analysis.h:195
local_bitvector_analysist::cfg
local_cfgt cfg
Definition: local_bitvector_analysis.h:46
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
local_bitvector_analysist::flagst::bitst
bitst
Definition: local_bitvector_analysis.h:62
local_bitvector_analysist::flagst::B_unknown
@ B_unknown
Definition: local_bitvector_analysis.h:63
local_bitvector_analysist::flagst::B_dynamic_heap
@ B_dynamic_heap
Definition: local_bitvector_analysis.h:67
local_bitvector_analysist::flagst::operator|
flagst operator|(const flagst other) const
Definition: local_bitvector_analysis.h:168
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:119
locals.h
Local variables whose address is taken.
local_bitvector_analysist::locals
localst locals
Definition: local_bitvector_analysis.h:45
local_bitvector_analysist::flagst::mk_integer_address
static flagst mk_integer_address()
Definition: local_bitvector_analysis.h:156
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:161
local_cfg.h
CFG for One Function.
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:141
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:151
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
local_bitvector_analysist::loc_infost
std::vector< points_tot > loc_infost
Definition: local_bitvector_analysis.h:194
local_bitvector_analysist::flagst::mk_dynamic_heap
static flagst mk_dynamic_heap()
Definition: local_bitvector_analysis.h:126
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:358
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:121
local_bitvector_analysist::work_queuet
std::stack< unsigned > work_queuet
Definition: local_bitvector_analysis.h:184
local_bitvector_analysist::pointers
numbering< irep_idt > pointers
Definition: local_bitvector_analysis.h:186
local_bitvector_analysist::flagst::mk_uninitialized
static flagst mk_uninitialized()
Definition: local_bitvector_analysis.h:96
local_bitvector_analysist::flagst::is_uses_offset
bool is_uses_offset() const
Definition: local_bitvector_analysis.h:111
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
local_bitvector_analysist
Definition: local_bitvector_analysis.h:24
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:91
local_bitvector_analysist::dirty
dirtyt dirty
Definition: local_bitvector_analysis.h:44
local_bitvector_analysist::flagst::mk_uses_offset
static flagst mk_uses_offset()
Definition: local_bitvector_analysis.h:106
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:50
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:101
local_bitvector_analysist::flagst::B_integer_address
@ B_integer_address
Definition: local_bitvector_analysis.h:70
local_bitvector_analysist::flagst::B_static_lifetime
@ B_static_lifetime
Definition: local_bitvector_analysis.h:69
local_bitvector_analysist::get
flagst get(const goto_programt::const_targett t, const exprt &src)
Definition: local_bitvector_analysis.cpp:108
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
operator<<
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
Definition: local_bitvector_analysis.h:210
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:146