CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
value_set_fi.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
15
16#include <list>
17#include <map>
18#include <set>
19#include <unordered_set>
20
21#include <util/mp_arith.h>
23
24#include "object_numbering.h"
25
26class codet;
27class namespacet;
28
30{
31public:
34 // to_function, to_target_index are set by set_to()
35 // from_function, from_target_index are set by set_from()
36 {
37 }
38
43
44 void set_from(const irep_idt &function, unsigned inx)
45 {
46 from_function = function_numbering.number(function);
48 }
49
50 void set_to(const irep_idt &function, unsigned inx)
51 {
52 to_function = function_numbering.number(function);
54 }
55
56 typedef irep_idt idt;
57
60 typedef std::optional<mp_integer> offsett;
61 bool offset_is_zero(const offsett &offset) const
62 {
63 return offset && offset->is_zero();
64 }
65
67 {
68 typedef std::map<object_numberingt::number_type, offsett> data_typet;
70
71 public:
72 // NOLINTNEXTLINE(readability/identifiers)
73 typedef data_typet::iterator iterator;
74 // NOLINTNEXTLINE(readability/identifiers)
75 typedef data_typet::const_iterator const_iterator;
76 // NOLINTNEXTLINE(readability/identifiers)
77 typedef data_typet::value_type value_type;
78
79 iterator begin() { return data.begin(); }
80 const_iterator begin() const { return data.begin(); }
81 const_iterator cbegin() const { return data.cbegin(); }
82
83 iterator end() { return data.end(); }
84 const_iterator end() const { return data.end(); }
85 const_iterator cend() const { return data.cend(); }
86
87 size_t size() const { return data.size(); }
88
93
94 template <typename It>
95 void insert(It b, It e) { data.insert(b, e); }
96
97 template <typename T>
98 const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
99
100 static const object_map_dt blank;
101
102 protected:
103 ~object_map_dt()=default;
104 };
105
106 exprt to_expr(const object_map_dt::value_type &it) const;
107
109
110 void set(object_mapt &dest, const object_map_dt::value_type &it) const
111 {
112 dest.write()[it.first]=it.second;
113 }
114
115 bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
116 {
117 return insert(dest, it.first, it.second);
118 }
119
120 bool insert(object_mapt &dest, const exprt &src) const
121 {
122 return insert(dest, object_numbering.number(src), offsett());
123 }
124
125 bool insert(
126 object_mapt &dest,
127 const exprt &src,
128 const mp_integer &offset_value) const
129 {
130 return insert(dest, object_numbering.number(src), offsett(offset_value));
131 }
132
133 bool insert(
134 object_mapt &dest,
136 const offsett &offset) const
137 {
138 if(dest.read().find(n)==dest.read().end())
139 {
140 // new
141 dest.write()[n] = offset;
142 return true;
143 }
144 else
145 {
146 offsett &old_offset = dest.write()[n];
147
148 if(old_offset && offset)
149 {
150 if(*old_offset == *offset)
151 return false;
152 else
153 {
154 old_offset.reset();
155 return true;
156 }
157 }
158 else if(!old_offset)
159 return false;
160 else
161 {
162 old_offset.reset();
163 return true;
164 }
165 }
166 }
167
168 bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
169 {
170 return insert(dest, object_numbering.number(expr), offset);
171 }
172
173 struct entryt
174 {
177 std::string suffix;
178
180 {
181 }
182
183 entryt(const idt &_identifier, const std::string _suffix):
184 identifier(_identifier),
186 {
187 }
188 };
189
190 typedef std::unordered_set<exprt, irep_hash> expr_sett;
191
192 typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
193
194 typedef std::map<idt, entryt> valuest;
195 typedef std::set<idt> flatten_seent;
196 typedef std::unordered_set<idt> gvs_recursion_sett;
197 typedef std::unordered_set<idt> recfind_recursion_sett;
198 typedef std::unordered_set<idt> assign_recursion_sett;
199
200 std::vector<exprt>
201 get_value_set(const exprt &expr, const namespacet &ns) const;
202
204 const idt &identifier,
205 const std::string &suffix);
206
207 void clear()
208 {
209 values.clear();
210 }
211
212 void add_var(const idt &id)
213 {
214 get_entry(id, "");
215 }
216
217 void add_var(const entryt &e)
218 {
220 }
221
222 entryt &get_entry(const idt &id, const std::string &suffix)
223 {
224 return get_entry(entryt(id, suffix));
225 }
226
228 {
229 std::string index=id2string(e.identifier)+e.suffix;
230
231 std::pair<valuest::iterator, bool> r=
232 values.insert(std::pair<idt, entryt>(index, e));
233
234 return r.first->second;
235 }
236
237 void add_vars(const std::list<entryt> &vars)
238 {
239 for(std::list<entryt>::const_iterator
240 it=vars.begin();
241 it!=vars.end();
242 it++)
243 add_var(*it);
244 }
245
246 void output(
247 const namespacet &ns,
248 std::ostream &out) const;
249
251
253
254 // true = added something new
255 bool make_union(object_mapt &dest, const object_mapt &src) const;
256
257 // true = added something new
258 bool make_union(const valuest &new_values);
259
260 // true = added something new
262 {
263 return make_union(new_values.values);
264 }
265
266 void apply_code(const codet &code, const namespacet &ns);
267
268 void assign(
269 const exprt &lhs,
270 const exprt &rhs,
271 const namespacet &ns);
272
273 void do_function_call(
274 const irep_idt &function,
275 const exprt::operandst &arguments,
276 const namespacet &ns);
277
278 // edge back to call site
279 void do_end_function(
280 const exprt &lhs,
281 const namespacet &ns);
282
284 const exprt &expr,
285 expr_sett &expr_set,
286 const namespacet &ns) const;
287
288protected:
290 const exprt &expr,
291 expr_sett &expr_set,
292 const namespacet &ns) const;
293
295 const exprt &expr,
296 object_mapt &dest,
298 const std::string &suffix,
299 const typet &original_type,
300 const namespacet &ns,
301 gvs_recursion_sett &recursion_set) const;
302
303 void get_value_set(
304 const exprt &expr,
305 object_mapt &dest,
306 const namespacet &ns) const;
307
309 const exprt &expr,
310 object_mapt &dest,
311 const namespacet &ns) const
312 {
313 get_reference_set_sharing_rec(expr, dest, ns);
314 }
315
317 const exprt &expr,
318 object_mapt &dest,
319 const namespacet &ns) const;
320
321 void dereference_rec(
322 const exprt &src,
323 exprt &dest) const;
324
325 void assign_rec(
326 const exprt &lhs,
327 const object_mapt &values_rhs,
328 const std::string &suffix,
329 const namespacet &ns,
330 assign_recursion_sett &recursion_set);
331
332 void flatten(const entryt &e, object_mapt &dest) const;
333
334 void flatten_rec(
335 const entryt&,
337 flatten_seent&) const;
338};
339
340#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const T & read() const
The type of an expression, extends irept.
Definition type.h:29
offsett & operator[](object_numberingt::number_type i)
const_iterator find(T &&t) const
data_typet::value_type value_type
std::map< object_numberingt::number_type, offsett > data_typet
const_iterator cbegin() const
const_iterator begin() const
const_iterator end() const
data_typet::const_iterator const_iterator
const_iterator cend() const
static const object_map_dt blank
data_typet::iterator iterator
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
static numberingt< irep_idt > function_numbering
void add_var(const idt &id)
std::unordered_set< idt > assign_recursion_sett
bool make_union(object_mapt &dest, const object_mapt &src) const
void add_vars(const std::list< entryt > &vars)
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
void set_from(const irep_idt &function, unsigned inx)
void set_to(const irep_idt &function, unsigned inx)
unsigned from_function
bool make_union(const value_set_fit &new_values)
void apply_code(const codet &code, const namespacet &ns)
void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
reference_counting< object_map_dt > object_mapt
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
unsigned to_function
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void dereference_rec(const exprt &src, exprt &dest) const
void output(const namespacet &ns, std::ostream &out) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< idt > recfind_recursion_sett
std::unordered_set< exprt, irep_hash > expr_sett
void do_end_function(const exprt &lhs, const namespacet &ns)
std::set< idt > flatten_seent
std::unordered_set< unsigned int > dynamic_object_id_sett
void flatten(const entryt &e, object_mapt &dest) const
bool offset_is_zero(const offsett &offset) const
entryt & get_entry(const idt &id, const std::string &suffix)
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
void add_var(const entryt &e)
std::unordered_set< idt > gvs_recursion_sett
entryt & get_entry(const entryt &e)
bool insert(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
unsigned to_target_index
std::map< idt, entryt > valuest
exprt to_expr(const object_map_dt::value_type &it) const
void set(object_mapt &dest, const object_map_dt::value_type &it) const
bool insert(object_mapt &dest, const exprt &src) const
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
expr_sett & get(const idt &identifier, const std::string &suffix)
std::unordered_set< exprt, irep_hash > expr_sett
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static int8_t r
Definition irep_hash.h:60
Object Numbering.
Reference Counting.
entryt(const idt &_identifier, const std::string _suffix)