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