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