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  void set_size_t(const irep_namet &name, const std::size_t value);
441 
442  void remove(const irep_namet &name);
443  void move_to_sub(irept &irep);
444  void move_to_named_sub(const irep_namet &name, irept &irep);
445 
446  bool operator==(const irept &other) const;
447 
448  bool operator!=(const irept &other) const
449  {
450  return !(*this==other);
451  }
452 
453  void swap(irept &irep)
454  {
455  std::swap(irep.data, data);
456  }
457 
458  bool operator<(const irept &other) const;
459  bool ordering(const irept &other) const;
460 
461  int compare(const irept &i) const;
462 
463  void clear() { *this=irept(); }
464 
465  void make_nil() { *this=get_nil_irep(); }
466 
467  subt &get_sub() { return write().sub; } // DANGEROUS
468  const subt &get_sub() const { return read().sub; }
469  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
470  const named_subt &get_named_sub() const { return read().named_sub; }
471 
472  std::size_t hash() const;
473  std::size_t full_hash() const;
474 
475  bool full_eq(const irept &other) const;
476 
477  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
478 
479  static bool is_comment(const irep_namet &name)
480  { return !name.empty() && name[0]=='#'; }
481 
483  static std::size_t number_of_non_comments(const named_subt &);
484 };
485 
486 // NOLINTNEXTLINE(readability/identifiers)
487 struct irep_hash
488 {
489  std::size_t operator()(const irept &irep) const
490  {
491  return irep.hash();
492  }
493 };
494 
495 // NOLINTNEXTLINE(readability/identifiers)
497 {
498  std::size_t operator()(const irept &irep) const
499  {
500  return irep.full_hash();
501  }
502 };
503 
504 // NOLINTNEXTLINE(readability/identifiers)
506 {
507  bool operator()(const irept &i1, const irept &i2) const
508  {
509  return i1.full_eq(i2);
510  }
511 };
512 
514 {
515  const irept &irep;
516  explicit irep_pretty_diagnosticst(const irept &irep);
517 };
518 
519 template <>
521 {
522  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
523  {
524  return irep.irep.pretty();
525  }
526 };
527 
528 template <typename derivedt, typename named_subtreest>
530 {
531 #ifdef IREP_DEBUG
532  std::cout << "DETACH1: " << data << '\n';
533 #endif
534 
535  if(data == &empty_d)
536  {
537  data = new dt;
538 
539 #ifdef IREP_DEBUG
540  std::cout << "ALLOCATED " << data << '\n';
541 #endif
542  }
543  else if(data->ref_count > 1)
544  {
545  dt *old_data(data);
546  data = new dt(*old_data);
547 
548 #ifdef IREP_DEBUG
549  std::cout << "ALLOCATED " << data << '\n';
550 #endif
551 
552  data->ref_count = 1;
553  remove_ref(old_data);
554  }
555 
556  POSTCONDITION(data->ref_count == 1);
557 
558 #ifdef IREP_DEBUG
559  std::cout << "DETACH2: " << data << '\n';
560 #endif
561 }
562 
563 template <typename derivedt, typename named_subtreest>
565 {
566  if(old_data == &empty_d)
567  return;
568 
569 #if 0
570  nonrecursive_destructor(old_data);
571 #else
572 
573  PRECONDITION(old_data->ref_count != 0);
574 
575 #ifdef IREP_DEBUG
576  std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
577 #endif
578 
579  old_data->ref_count--;
580  if(old_data->ref_count == 0)
581  {
582 #ifdef IREP_DEBUG
583  std::cout << "D: " << pretty() << '\n';
584  std::cout << "DELETING " << old_data->data << " " << old_data << '\n';
585  old_data->clear();
586  std::cout << "DEALLOCATING " << old_data << "\n";
587 #endif
588 
589  // may cause recursive call
590  delete old_data;
591 
592 #ifdef IREP_DEBUG
593  std::cout << "DONE\n";
594 #endif
595  }
596 #endif
597 }
598 
601 template <typename derivedt, typename named_subtreest>
603  dt *old_data)
604 {
605  std::vector<dt *> stack(1, old_data);
606 
607  while(!stack.empty())
608  {
609  dt *d = stack.back();
610  stack.erase(--stack.end());
611  if(d == &empty_d)
612  continue;
613 
614  INVARIANT(d->ref_count != 0, "All contents of the stack must be in use");
615  d->ref_count--;
616 
617  if(d->ref_count == 0)
618  {
619  stack.reserve(
620  stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
621  d->sub.size());
622 
623  for(typename named_subt::iterator it = d->named_sub.begin();
624  it != d->named_sub.end();
625  it++)
626  {
627  stack.push_back(it->second.data);
628  it->second.data = &empty_d;
629  }
630 
631  for(typename subt::iterator it = d->sub.begin(); it != d->sub.end(); it++)
632  {
633  stack.push_back(it->data);
634  it->data = &empty_d;
635  }
636 
637  // now delete, won't do recursion
638  delete d;
639  }
640  }
641 }
642 
643 #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:479
sharing_treet::remove_ref
static void remove_ref(dt *old_data)
Definition: irep.h:564
irept::get_int
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:63
irept::clear
void clear()
Definition: irep.h:463
irept::move_to_sub
void move_to_sub(irept &irep)
Definition: irep.cpp:36
irept::make_nil
void make_nil()
Definition: irep.h:465
irep_full_eq::operator()
bool operator()(const irept &i1, const irept &i2) const
Definition: irep.h:507
irept::full_eq
bool full_eq(const irept &other) const
Definition: irep.cpp:205
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
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:428
data
Definition: kdev_t.h:24
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:116
tree_nodet::tree_nodet
tree_nodet()=default
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
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:73
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:522
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:417
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:58
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:27
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:498
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:469
irep_hash::operator()
std::size_t operator()(const irept &irep) const
Definition: irep.h:489
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:602
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:448
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:20
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:453
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:470
sharing_treet::operator=
sharing_treet & operator=(sharing_treet &&irep)
Definition: irep.h:235
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:96
dstringt::empty
bool empty() const
Definition: dstring.h:88
irep_hash
Definition: irep.h:488
irep_pretty_diagnosticst::irep
const irept & irep
Definition: irep.h:515
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:299
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:146
tree_nodet::hash_code
std::size_t hash_code
Definition: irep.h:128
irep_pretty_diagnosticst
Definition: irep.h:514
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:479
irept::ordering
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:245
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:68
irep_ids.h
util
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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:468
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
invariant.h
irept::compare
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition: irep.cpp:314
irept::set_size_t
void set_size_t(const irep_namet &name, const std::size_t value)
Definition: irep.cpp:87
ref_count_ift< true >::ref_count
unsigned ref_count
Definition: irep.h:85
irept::get_sub
subt & get_sub()
Definition: irep.h:467
tree_nodet< derivedt, named_subtreest, false >::named_subt
named_subtreest named_subt
Definition: irep.h:117
SHARING
#define SHARING
Definition: irep.h:19
as_string
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:23
irep_full_eq
Definition: irep.h:506
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:536
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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:408
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:497
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:529
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:466