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