cprover
irep.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_IREP_H
11 #define CPROVER_UTIL_IREP_H
12 
13 #include <string>
14 #include <vector>
15 
16 #include "deprecate.h"
17 #include "invariant.h"
18 #include "irep_ids.h"
19 
20 #define SHARING
21 // #define HASH_CODE
22 #define USE_MOVE
23 // #define NAMED_SUB_IS_FORWARD_LIST
24 
25 #ifdef NAMED_SUB_IS_FORWARD_LIST
26 #include <forward_list>
27 #else
28 #include <map>
29 #endif
30 
31 #ifdef USE_DSTRING
34 // NOLINTNEXTLINE(readability/identifiers)
36 #else
37 #include "string_hash.h"
38 typedef std::string irep_idt;
39 typedef std::string irep_namet;
40 // NOLINTNEXTLINE(readability/identifiers)
42 #endif
43 
44 inline const std::string &id2string(const irep_idt &d)
45 {
46  #ifdef USE_DSTRING
47  return as_string(d);
48  #else
49  return d;
50  #endif
51 }
52 
53 inline const std::string &name2string(const irep_namet &n)
54 {
55  #ifdef USE_DSTRING
56  return as_string(n);
57  #else
58  return n;
59  #endif
60 }
61 
62 #define forall_irep(it, irep) \
63  for(irept::subt::const_iterator it=(irep).begin(); \
64  it!=(irep).end(); ++it)
65 
66 #define Forall_irep(it, irep) \
67  for(irept::subt::iterator it=(irep).begin(); \
68  it!=(irep).end(); ++it)
69 
70 #define forall_named_irep(it, irep) \
71  for(irept::named_subt::const_iterator it=(irep).begin(); \
72  it!=(irep).end(); ++it)
73 
74 #define Forall_named_irep(it, irep) \
75  for(irept::named_subt::iterator it=(irep).begin(); \
76  it!=(irep).end(); ++it)
77 
78 #ifdef IREP_DEBUG
79 #include <iostream>
80 #endif
81 
82 class irept;
83 const irept &get_nil_irep();
84 
153 class irept
154 {
155 public:
156  // These are not stable.
157  typedef std::vector<irept> subt;
158 
159  // named_subt has to provide stable references; with C++11 we could
160  // use std::forward_list or std::vector< unique_ptr<T> > to save
161  // memory and increase efficiency.
162 
163 #ifdef NAMED_SUB_IS_FORWARD_LIST
164  typedef std::forward_list<std::pair<irep_namet, irept>> named_subt;
165 #else
166  typedef std::map<irep_namet, irept> named_subt;
167 #endif
168 
169  bool is_nil() const { return id()==ID_nil; }
170  bool is_not_nil() const { return id()!=ID_nil; }
171 
172  explicit irept(const irep_idt &_id)
173 #ifdef SHARING
174  :data(&empty_d)
175 #endif
176  {
177  id(_id);
178  }
179 
180  #ifdef SHARING
181  // constructor for blank irep
183  {
184  }
185 
186  // copy constructor
187  irept(const irept &irep):data(irep.data)
188  {
189  if(data!=&empty_d)
190  {
191  // NOLINTNEXTLINE(build/deprecated)
192  PRECONDITION(data->ref_count != 0);
193  data->ref_count++;
194  #ifdef IREP_DEBUG
195  std::cout << "COPY " << data << " " << data->ref_count << '\n';
196  #endif
197  }
198  }
199 
200  #ifdef USE_MOVE
201  // Copy from rvalue reference.
202  // Note that this does avoid a branch compared to the
203  // standard copy constructor above.
204  irept(irept &&irep):data(irep.data)
205  {
206  #ifdef IREP_DEBUG
207  std::cout << "COPY MOVE\n";
208  #endif
209  irep.data=&empty_d;
210  }
211  #endif
212 
213  irept &operator=(const irept &irep)
214  {
215  #ifdef IREP_DEBUG
216  std::cout << "ASSIGN\n";
217  #endif
218 
219  // Ordering is very important here!
220  // Consider self-assignment, which may destroy 'irep'
221  dt *irep_data=irep.data;
222  if(irep_data!=&empty_d)
223  irep_data->ref_count++;
224 
225  remove_ref(data); // this may kill 'irep'
226  data=irep_data;
227 
228  return *this;
229  }
230 
231  #ifdef USE_MOVE
232  // Note that the move assignment operator does avoid
233  // three branches compared to standard operator above.
235  {
236  #ifdef IREP_DEBUG
237  std::cout << "ASSIGN MOVE\n";
238  #endif
239  // we simply swap two pointers
240  std::swap(data, irep.data);
241  return *this;
242  }
243  #endif
244 
246  {
247  remove_ref(data);
248  }
249 
250  #else
251  irept()
252  {
253  }
254  #endif
255 
256  const irep_idt &id() const
257  { return read().data; }
258 
259  const std::string &id_string() const
260  { return id2string(read().data); }
261 
262  void id(const irep_idt &_data)
263  { write().data=_data; }
264 
265  const irept &find(const irep_namet &name) const;
266  irept &add(const irep_namet &name);
267  irept &add(const irep_namet &name, const irept &irep);
268 
269  const std::string &get_string(const irep_namet &name) const
270  {
271  return id2string(get(name));
272  }
273 
274  const irep_idt &get(const irep_namet &name) const;
275  bool get_bool(const irep_namet &name) const;
276  signed int get_int(const irep_namet &name) const;
278  DEPRECATED("Use get_size_t instead")
279  unsigned int get_unsigned_int(const irep_namet &name) const;
280  std::size_t get_size_t(const irep_namet &name) const;
281  long long get_long_long(const irep_namet &name) const;
282 
283  void set(const irep_namet &name, const irep_idt &value)
284  { add(name).id(value); }
285  void set(const irep_namet &name, const irept &irep)
286  { add(name, irep); }
287  void set(const irep_namet &name, const long long value);
288 
289  void remove(const irep_namet &name);
290  void move_to_sub(irept &irep);
291  void move_to_named_sub(const irep_namet &name, irept &irep);
292 
293  bool operator==(const irept &other) const;
294 
295  bool operator!=(const irept &other) const
296  {
297  return !(*this==other);
298  }
299 
300  void swap(irept &irep)
301  {
302  std::swap(irep.data, data);
303  }
304 
305  bool operator<(const irept &other) const;
306  bool ordering(const irept &other) const;
307 
308  int compare(const irept &i) const;
309 
310  void clear() { *this=irept(); }
311 
312  void make_nil() { *this=get_nil_irep(); }
313 
314  subt &get_sub() { return write().sub; } // DANGEROUS
315  const subt &get_sub() const { return read().sub; }
316  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
317  const named_subt &get_named_sub() const { return read().named_sub; }
318 
319  std::size_t hash() const;
320  std::size_t full_hash() const;
321 
322  bool full_eq(const irept &other) const;
323 
324  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
325 
326 public:
327  static bool is_comment(const irep_namet &name)
328  { return !name.empty() && name[0]=='#'; }
329 
331  static std::size_t number_of_non_comments(const named_subt &);
332 
333  class dt
334  {
335  private:
336  friend class irept;
337 
338  #ifdef SHARING
339  unsigned ref_count;
340  #endif
341 
345 
348 
349  #ifdef HASH_CODE
350  mutable std::size_t hash_code;
351  #endif
352 
353  void clear()
354  {
355  data.clear();
356  sub.clear();
357  named_sub.clear();
358  #ifdef HASH_CODE
359  hash_code=0;
360  #endif
361  }
362 
363  void swap(dt &d)
364  {
365  d.data.swap(data);
366  d.sub.swap(sub);
367  d.named_sub.swap(named_sub);
368  #ifdef HASH_CODE
369  std::swap(d.hash_code, hash_code);
370  #endif
371  }
372 
373  #ifdef SHARING
375  #ifdef HASH_CODE
376  , hash_code(0)
377  #endif
378  {
379  }
380  #else
381  dt()
382  #ifdef HASH_CODE
383  :hash_code(0)
384  #endif
385  {
386  }
387  #endif
388  };
389 
390 protected:
391  #ifdef SHARING
393  static dt empty_d;
394 
395  static void remove_ref(dt *old_data);
396  static void nonrecursive_destructor(dt *old_data);
397  void detach();
398 
399 public:
400  const dt &read() const
401  {
402  return *data;
403  }
404 
406  {
407  detach();
408  #ifdef HASH_CODE
409  data->hash_code=0;
410  #endif
411  return *data;
412  }
413 
414  #else
415  dt data;
416 
417 public:
418  const dt &read() const
419  {
420  return data;
421  }
422 
423  dt &write()
424  {
425  #ifdef HASH_CODE
426  data.hash_code=0;
427  #endif
428  return data;
429  }
430  #endif
431 };
432 
433 // NOLINTNEXTLINE(readability/identifiers)
434 struct irep_hash
435 {
436  std::size_t operator()(const irept &irep) const
437  {
438  return irep.hash();
439  }
440 };
441 
442 // NOLINTNEXTLINE(readability/identifiers)
444 {
445  std::size_t operator()(const irept &irep) const
446  {
447  return irep.full_hash();
448  }
449 };
450 
451 // NOLINTNEXTLINE(readability/identifiers)
453 {
454  bool operator()(const irept &i1, const irept &i2) const
455  {
456  return i1.full_eq(i2);
457  }
458 };
459 
461 {
462  const irept &irep;
463  explicit irep_pretty_diagnosticst(const irept &irep);
464 };
465 
466 template <>
468 {
469  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
470  {
471  return irep.irep.pretty();
472  }
473 };
474 
475 #endif // CPROVER_UTIL_IREP_H
irept(const irept &irep)
Definition: irep.h:187
bool is_nil() const
Definition: irep.h:169
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:170
subt sub
Definition: irep.h:347
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition: irep.cpp:531
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:713
std::vector< irept > subt
Definition: irep.h:157
void move_to_sub(irept &irep)
Definition: irep.cpp:193
std::size_t hash() const
Definition: irep.cpp:645
bool full_eq(const irept &other) const
Definition: irep.cpp:413
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:233
void id(const irep_idt &_data)
Definition: irep.h:262
irept(irept &&irep)
Definition: irep.h:204
const irept & get_nil_irep()
Definition: irep.cpp:55
STL namespace.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
named_subt named_sub
Definition: irep.h:346
const irept & irep
Definition: irep.h:462
subt & get_sub()
Definition: irep.h:314
const dt & read() const
Definition: irep.h:400
void swap(dt &d)
Definition: irep.h:363
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:754
bool operator!=(const irept &other) const
Definition: irep.h:295
const irep_idt & id() const
Definition: irep.h:256
dt * data
Definition: irep.h:392
const std::string & name2string(const irep_namet &n)
Definition: irep.h:53
unsigned ref_count
Definition: irep.h:339
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:273
std::size_t operator()(const irept &irep) const
Definition: irep.h:436
irept & operator=(const irept &irep)
Definition: irep.h:213
std::size_t operator()(const irept &irep) const
Definition: irep.h:445
dstring_hash irep_id_hash
Definition: irep.h:35
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition: irep.cpp:139
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::string as_string(resultt result)
Definition: properties.cpp:19
Base class for tree-like data structures with sharing.
Definition: irep.h:153
std::map< irep_namet, irept > named_subt
Definition: irep.h:166
irept()
Definition: irep.h:182
void detach()
Definition: irep.cpp:63
irept & operator=(irept &&irep)
Definition: irep.h:234
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
dt()
Definition: irep.h:374
static dt empty_d
Definition: irep.h:393
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:625
static void remove_ref(dt *old_data)
Definition: irep.cpp:99
named_subt & get_named_sub()
Definition: irep.h:316
#define DEPRECATED(msg)
Definition: deprecate.h:23
const named_subt & get_named_sub() const
Definition: irep.h:317
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:462
void swap(dstringt &b)
Definition: dstring.h:132
~irept()
Definition: irep.h:245
static bool is_comment(const irep_namet &name)
Definition: irep.h:327
irep_idt data
This irep_idt is the only place to store data in an irep, other than the mere nesting structure...
Definition: irep.h:344
std::size_t full_hash() const
Definition: irep.cpp:680
void clear()
Definition: irep.h:310
bool operator()(const irept &i1, const irept &i2) const
Definition: irep.h:454
irept & add(const irep_namet &name)
Definition: irep.cpp:297
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:269
void make_nil()
Definition: irep.h:312
const std::string & id_string() const
Definition: irep.h:259
void swap(irept &irep)
Definition: irep.h:300
void clear()
Definition: irep.h:353
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:238
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:248
dstringt irep_namet
Definition: irep.h:33
dstringt irep_idt
Definition: irep.h:32
bool operator==(const irept &other) const
Definition: irep.cpp:354
irept(const irep_idt &_id)
Definition: irep.h:172
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:243
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:277
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
Definition: irep.h:469
const subt & get_sub() const
Definition: irep.h:315
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:283
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:184
static std::size_t number_of_non_comments(const named_subt &)
count the number of named_sub elements that are not comments
Definition: irep.cpp:634
dt & write()
Definition: irep.h:405