CBMC
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 "invariant.h"
17 #include "irep_ids.h"
18 
19 #define SHARING
20 #ifndef HASH_CODE
21 # define HASH_CODE 1
22 #endif
23 // use forward_list by default, unless _GLIBCXX_DEBUG is set as the debug
24 // overhead is noticeably higher with the regression test suite taking four
25 // times as long.
26 #if !defined(NAMED_SUB_IS_FORWARD_LIST) && !defined(_GLIBCXX_DEBUG)
27 # define NAMED_SUB_IS_FORWARD_LIST 1
28 #endif
29 
30 #if NAMED_SUB_IS_FORWARD_LIST
31 # include "forward_list_as_map.h"
32 #else
33 #include <map>
34 #endif
35 
36 #ifdef USE_DSTRING
38 // NOLINTNEXTLINE(readability/identifiers)
40 #else
41 #include "string_hash.h"
42 typedef std::string irep_idt;
43 // NOLINTNEXTLINE(readability/identifiers)
45 #endif
46 
47 inline const std::string &id2string(const irep_idt &d)
48 {
49  #ifdef USE_DSTRING
50  return as_string(d);
51  #else
52  return d;
53  #endif
54 }
55 
56 #ifdef IREP_DEBUG
57 #include <iostream>
58 #endif
59 
60 class irept;
61 const irept &get_nil_irep();
62 
66 template <bool enabled>
68 {
69 };
70 
71 template <>
72 struct ref_count_ift<true>
73 {
74  unsigned ref_count = 1;
75 };
76 
96 template <typename treet, typename named_subtreest, bool sharing = true>
97 class tree_nodet : public ref_count_ift<sharing>
98 {
99 public:
100  // These are not stable.
101  typedef std::vector<treet> subt;
102 
103  // named_subt has to provide stable references; we can
104  // use std::forward_list or std::vector< unique_ptr<T> > to save
105  // memory and increase efficiency.
106  using named_subt = named_subtreest;
107 
108  friend treet;
109 
112 
115 
116 #if HASH_CODE
117  mutable std::size_t hash_code = 0;
118 #endif
119 
120  void clear()
121  {
122  data.clear();
123  sub.clear();
124  named_sub.clear();
125 #if HASH_CODE
126  hash_code = 0;
127 #endif
128  }
129 
130  void swap(tree_nodet &d)
131  {
132  d.data.swap(data);
133  d.sub.swap(sub);
134  d.named_sub.swap(named_sub);
135 #if HASH_CODE
136  std::swap(d.hash_code, hash_code);
137 #endif
138  }
139 
140  tree_nodet() = default;
141 
142  explicit tree_nodet(irep_idt _data) : data(std::move(_data))
143  {
144  }
145 
146  tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
147  : data(std::move(_data)),
148  named_sub(std::move(_named_sub)),
149  sub(std::move(_sub))
150  {
151  }
152 };
153 
155 template <typename derivedt, typename named_subtreest>
157 {
158 public:
160  using subt = typename dt::subt;
161  using named_subt = typename dt::named_subt;
162 
165 
166  explicit sharing_treet(irep_idt _id) : data(new dt(std::move(_id)))
167  {
168  }
169 
170  sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
171  : data(new dt(std::move(_id), std::move(_named_sub), std::move(_sub)))
172  {
173  }
174 
175  // constructor for blank irep
177  {
178  }
179 
180  // copy constructor
181  sharing_treet(const sharing_treet &irep) : data(irep.data)
182  {
183  if(data!=&empty_d)
184  {
185  PRECONDITION(data->ref_count != 0);
186  data->ref_count++;
187 #ifdef IREP_DEBUG
188  std::cout << "COPY " << data << " " << data->ref_count << '\n';
189 #endif
190  }
191  }
192 
193  // Copy from rvalue reference.
194  // Note that this does avoid a branch compared to the
195  // standard copy constructor above.
197  {
198 #ifdef IREP_DEBUG
199  std::cout << "COPY MOVE\n";
200 #endif
201  irep.data=&empty_d;
202  }
203 
205  {
206 #ifdef IREP_DEBUG
207  std::cout << "ASSIGN\n";
208 #endif
209 
210  // Ordering is very important here!
211  // Consider self-assignment, which may destroy 'irep'
212  dt *irep_data=irep.data;
213  if(irep_data!=&empty_d)
214  irep_data->ref_count++;
215 
216  remove_ref(data); // this may kill 'irep'
217  data=irep_data;
218 
219  return *this;
220  }
221 
222  // Note that the move assignment operator does avoid
223  // three branches compared to standard operator above.
225  {
226 #ifdef IREP_DEBUG
227  std::cout << "ASSIGN MOVE\n";
228 #endif
229  // we simply swap two pointers
230  std::swap(data, irep.data);
231  return *this;
232  }
233 
235  {
236  remove_ref(data);
237  }
238 
239 protected:
241  static dt empty_d;
242 
243  static void remove_ref(dt *old_data);
244  static void nonrecursive_destructor(dt *old_data);
245  void detach();
246 
247 public:
248  const dt &read() const
249  {
250  return *data;
251  }
252 
254  {
255  detach();
256 #if HASH_CODE
257  data->hash_code = 0;
258 #endif
259  return *data;
260  }
261 };
262 
263 // Static field initialization
264 template <typename derivedt, typename named_subtreest>
267 
269 template <typename derivedt, typename named_subtreest>
271 {
272 public:
274  using subt = typename dt::subt;
275  using named_subt = typename dt::named_subt;
276 
279 
280  explicit non_sharing_treet(irep_idt _id) : data(std::move(_id))
281  {
282  }
283 
284  non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
285  : data(std::move(_id), std::move(_named_sub), std::move(_sub))
286  {
287  }
288 
289  non_sharing_treet() = default;
290 
291  const dt &read() const
292  {
293  return data;
294  }
295 
297  {
298 #if HASH_CODE
299  data.hash_code = 0;
300 #endif
301  return data;
302  }
303 
304 protected:
306 };
307 
359 class irept
360 #ifdef SHARING
361  : public sharing_treet<
362  irept,
363 #else
364  : public non_sharing_treet<
365  irept,
366 #endif
367 #if NAMED_SUB_IS_FORWARD_LIST
368  forward_list_as_mapt<irep_idt, irept>>
369 #else
370  std::map<irep_idt, irept>>
371 #endif
372 {
373 public:
375 
376  bool is_nil() const
377  {
378  return id() == ID_nil;
379  }
380  bool is_not_nil() const
381  {
382  return id() != ID_nil;
383  }
384 
385  explicit irept(const irep_idt &_id) : baset(_id)
386  {
387  }
388 
389  irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
390  : baset(_id, _named_sub, _sub)
391  {
392  }
393 
394  irept() = default;
395 
396  const irep_idt &id() const
397  { return read().data; }
398 
399  const std::string &id_string() const
400  { return id2string(read().data); }
401 
402  void id(const irep_idt &_data)
403  { write().data=_data; }
404 
405  const irept &find(const irep_idt &name) const;
406  irept &add(const irep_idt &name);
407  irept &add(const irep_idt &name, irept irep);
408 
409  const std::string &get_string(const irep_idt &name) const
410  {
411  return id2string(get(name));
412  }
413 
414  const irep_idt &get(const irep_idt &name) const;
415  bool get_bool(const irep_idt &name) const;
416  signed int get_int(const irep_idt &name) const;
417  std::size_t get_size_t(const irep_idt &name) const;
418  long long get_long_long(const irep_idt &name) const;
419 
420  void set(const irep_idt &name, const irep_idt &value)
421  {
422  add(name, irept(value));
423  }
424  void set(const irep_idt &name, irept irep)
425  {
426  add(name, std::move(irep));
427  }
428  void set(const irep_idt &name, const long long value);
429  void set_size_t(const irep_idt &name, const std::size_t value);
430 
431  void remove(const irep_idt &name);
432  void move_to_sub(irept &irep);
433  void move_to_named_sub(const irep_idt &name, irept &irep);
434 
435  bool operator==(const irept &other) const;
436 
437  bool operator!=(const irept &other) const
438  {
439  return !(*this==other);
440  }
441 
442  void swap(irept &irep)
443  {
444  std::swap(irep.data, data);
445  }
446 
447  bool operator<(const irept &other) const;
448  bool ordering(const irept &other) const;
449 
450  int compare(const irept &i) const;
451 
452  void clear() { *this=irept(); }
453 
454  void make_nil() { *this=get_nil_irep(); }
455 
456  subt &get_sub() { return write().sub; } // DANGEROUS
457  const subt &get_sub() const { return read().sub; }
458  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
459  const named_subt &get_named_sub() const { return read().named_sub; }
460 
461  std::size_t hash() const;
462  std::size_t full_hash() const;
463 
464  bool full_eq(const irept &other) const;
465 
466  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
467 
468  static bool is_comment(const irep_idt &name)
469  { return !name.empty() && name[0]=='#'; }
470 
472  static std::size_t number_of_non_comments(const named_subt &);
473 };
474 
475 // NOLINTNEXTLINE(readability/identifiers)
476 struct irep_hash
477 {
478  std::size_t operator()(const irept &irep) const
479  {
480  return irep.hash();
481  }
482 };
483 
484 // NOLINTNEXTLINE(readability/identifiers)
486 {
487  std::size_t operator()(const irept &irep) const
488  {
489  return irep.full_hash();
490  }
491 };
492 
493 // NOLINTNEXTLINE(readability/identifiers)
495 {
496  bool operator()(const irept &i1, const irept &i2) const
497  {
498  return i1.full_eq(i2);
499  }
500 };
501 
503 {
504  const irept &irep;
505  explicit irep_pretty_diagnosticst(const irept &irep);
506 };
507 
508 template <>
510 {
511  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
512  {
513  return irep.irep.pretty();
514  }
515 };
516 
517 template <typename derivedt, typename named_subtreest>
519 {
520 #ifdef IREP_DEBUG
521  std::cout << "DETACH1: " << data << '\n';
522 #endif
523 
524  if(data == &empty_d)
525  {
526  data = new dt;
527 
528 #ifdef IREP_DEBUG
529  std::cout << "ALLOCATED " << data << '\n';
530 #endif
531  }
532  else if(data->ref_count > 1)
533  {
534  dt *old_data(data);
535  data = new dt(*old_data);
536 
537 #ifdef IREP_DEBUG
538  std::cout << "ALLOCATED " << data << '\n';
539 #endif
540 
541  data->ref_count = 1;
542  remove_ref(old_data);
543  }
544 
545  POSTCONDITION(data->ref_count == 1);
546 
547 #ifdef IREP_DEBUG
548  std::cout << "DETACH2: " << data << '\n';
549 #endif
550 }
551 
552 template <typename derivedt, typename named_subtreest>
554 {
555  if(old_data == &empty_d)
556  return;
557 
558 #if 0
559  nonrecursive_destructor(old_data);
560 #else
561 
562  PRECONDITION(old_data->ref_count != 0);
563 
564 #ifdef IREP_DEBUG
565  std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
566 #endif
567 
568  old_data->ref_count--;
569  if(old_data->ref_count == 0)
570  {
571 #ifdef IREP_DEBUG
572  std::cout << "D: " << pretty() << '\n';
573  std::cout << "DELETING " << old_data->data << " " << old_data << '\n';
574  old_data->clear();
575  std::cout << "DEALLOCATING " << old_data << "\n";
576 #endif
577 
578  // may cause recursive call
579  delete old_data;
580 
581 #ifdef IREP_DEBUG
582  std::cout << "DONE\n";
583 #endif
584  }
585 #endif
586 }
587 
590 template <typename derivedt, typename named_subtreest>
592  dt *old_data)
593 {
594  std::vector<dt *> stack(1, old_data);
595 
596  while(!stack.empty())
597  {
598  dt *d = stack.back();
599  stack.erase(--stack.end());
600  if(d == &empty_d)
601  continue;
602 
603  INVARIANT(d->ref_count != 0, "All contents of the stack must be in use");
604  d->ref_count--;
605 
606  if(d->ref_count == 0)
607  {
608  stack.reserve(
609  stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
610  d->sub.size());
611 
612  for(typename named_subt::iterator it = d->named_sub.begin();
613  it != d->named_sub.end();
614  it++)
615  {
616  stack.push_back(it->second.data);
617  it->second.data = &empty_d;
618  }
619 
620  for(typename subt::iterator it = d->sub.begin(); it != d->sub.end(); it++)
621  {
622  stack.push_back(it->data);
623  it->data = &empty_d;
624  }
625 
626  // now delete, won't do recursion
627  delete d;
628  }
629  }
630 }
631 
632 #endif // CPROVER_UTIL_IREP_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
void swap(dstringt &b)
Definition: dstring.h:163
bool empty() const
Definition: dstring.h:90
void clear()
Definition: dstring.h:160
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
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:416
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
irept()=default
bool operator==(const irept &other) const
Definition: irep.cpp:145
subt & get_sub()
Definition: irep.h:456
void set(const irep_idt &name, irept irep)
Definition: irep.h:424
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:494
void move_to_named_sub(const irep_idt &name, irept &irep)
Definition: irep.cpp:26
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:67
bool operator!=(const irept &other) const
Definition: irep.h:437
const irept & find(const irep_idt &name) const
Definition: irep.cpp:105
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:244
const subt & get_sub() const
Definition: irep.h:457
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
named_subt & get_named_sub()
Definition: irep.h:458
irept(const irep_idt &_id)
Definition: irep.h:385
const std::string & id_string() const
Definition: irep.h:399
void remove(const irep_idt &name)
Definition: irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const named_subt & get_named_sub() const
Definition: irep.h:459
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:86
irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
Definition: irep.h:389
std::size_t hash() const
Definition: irep.cpp:427
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition: irep.cpp:313
void clear()
Definition: irep.h:452
bool is_not_nil() const
Definition: irep.h:380
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:407
const irep_idt & id() const
Definition: irep.h:396
bool full_eq(const irept &other) const
Definition: irep.cpp:204
long long get_long_long(const irep_idt &name) const
Definition: irep.cpp:72
std::size_t full_hash() const
Definition: irep.cpp:465
void make_nil()
Definition: irep.h:454
signed int get_int(const irep_idt &name) const
Definition: irep.cpp:62
static bool is_comment(const irep_idt &name)
Definition: irep.h:468
void move_to_sub(irept &irep)
Definition: irep.cpp:35
void swap(irept &irep)
Definition: irep.h:442
void id(const irep_idt &_data)
Definition: irep.h:402
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
irept & add(const irep_idt &name)
Definition: irep.cpp:115
bool is_nil() const
Definition: irep.h:376
Base class for tree-like data structures without sharing.
Definition: irep.h:271
non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
Definition: irep.h:284
non_sharing_treet()=default
typename dt::subt subt
Definition: irep.h:274
non_sharing_treet(irep_idt _id)
Definition: irep.h:280
typename dt::named_subt named_subt
Definition: irep.h:275
const dt & read() const
Definition: irep.h:291
dt & write()
Definition: irep.h:296
Base class for tree-like data structures with sharing.
Definition: irep.h:157
sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
Definition: irep.h:170
dt & write()
Definition: irep.h:253
dt * data
Definition: irep.h:240
sharing_treet(irep_idt _id)
Definition: irep.h:166
sharing_treet & operator=(sharing_treet &&irep)
Definition: irep.h:224
static void remove_ref(dt *old_data)
Definition: irep.h:553
typename dt::named_subt named_subt
Definition: irep.h:161
typename dt::subt subt
Definition: irep.h:160
sharing_treet tree_implementationt
Used to refer to this class from derived classes.
Definition: irep.h:164
sharing_treet(const sharing_treet &irep)
Definition: irep.h:181
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition: irep.h:591
static dt empty_d
Definition: irep.h:241
sharing_treet & operator=(const sharing_treet &irep)
Definition: irep.h:204
const dt & read() const
Definition: irep.h:248
sharing_treet()
Definition: irep.h:176
sharing_treet(sharing_treet &&irep)
Definition: irep.h:196
~sharing_treet()
Definition: irep.h:234
void detach()
Definition: irep.h:518
A node with data in a tree, it contains:
Definition: irep.h:98
named_subt named_sub
Definition: irep.h:113
named_subtreest named_subt
Definition: irep.h:106
friend treet
Definition: irep.h:108
tree_nodet()=default
void swap(tree_nodet &d)
Definition: irep.h:130
tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
Definition: irep.h:146
std::vector< treet > subt
Definition: irep.h:101
void clear()
Definition: irep.h:120
tree_nodet(irep_idt _data)
Definition: irep.h:142
std::size_t hash_code
Definition: irep.h:117
subt sub
Definition: irep.h:114
irep_idt data
This irep_idt is the only place to store data in an tree node.
Definition: irep.h:111
dstring_hash irep_id_hash
Definition: irep.h:39
dstringt irep_idt
Definition: irep.h:37
const irept & get_nil_irep()
Definition: irep.cpp:19
#define SHARING
Definition: irep.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
string hashing
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
Definition: irep.h:511
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:299
bool operator()(const irept &i1, const irept &i2) const
Definition: irep.h:496
std::size_t operator()(const irept &irep) const
Definition: irep.h:487
std::size_t operator()(const irept &irep) const
Definition: irep.h:478
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:535
const irept & irep
Definition: irep.h:504
unsigned ref_count
Definition: irep.h:74
Used in tree_nodet for activating or not reference counting.
Definition: irep.h:68