cprover
irep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Internal Representation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "irep.h"
13 
14 #include <ostream>
15 
16 #include "string2int.h"
17 #include "string_hash.h"
18 #include "irep_hash.h"
19 
20 #ifdef NAMED_SUB_IS_FORWARD_LIST
21 #include <algorithm>
22 #endif
23 
24 #ifdef IREP_DEBUG
25 #include <iostream>
26 #endif
27 
29 
30 #ifdef SHARING
32 #endif
33 
34 #ifdef NAMED_SUB_IS_FORWARD_LIST
35 static inline bool named_subt_order(
36  const std::pair<irep_namet, irept> &a,
37  const irep_namet &b)
38 {
39  return a.first<b;
40 }
41 
42 static inline irept::named_subt::const_iterator named_subt_lower_bound(
43  const irept::named_subt &s, const irep_namet &id)
44 {
45  return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
46 }
47 
48 static inline irept::named_subt::iterator named_subt_lower_bound(
49  irept::named_subt &s, const irep_namet &id)
50 {
51  return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
52 }
53 #endif
54 
56 {
57  if(nil_rep_storage.id().empty()) // initialized?
58  nil_rep_storage.id(ID_nil);
59  return nil_rep_storage;
60 }
61 
62 #ifdef SHARING
64 {
65  #ifdef IREP_DEBUG
66  std::cout << "DETACH1: " << data << '\n';
67  #endif
68 
69  if(data==&empty_d)
70  {
71  data=new dt;
72 
73  #ifdef IREP_DEBUG
74  std::cout << "ALLOCATED " << data << '\n';
75  #endif
76  }
77  else if(data->ref_count>1)
78  {
79  dt *old_data(data);
80  data=new dt(*old_data);
81 
82  #ifdef IREP_DEBUG
83  std::cout << "ALLOCATED " << data << '\n';
84  #endif
85 
86  data->ref_count=1;
87  remove_ref(old_data);
88  }
89 
90  POSTCONDITION(data->ref_count==1);
91 
92  #ifdef IREP_DEBUG
93  std::cout << "DETACH2: " << data << '\n';
94  #endif
95 }
96 #endif
97 
98 #ifdef SHARING
99 void irept::remove_ref(dt *old_data)
100 {
101  if(old_data==&empty_d)
102  return;
103 
104  #if 0
105  nonrecursive_destructor(old_data);
106  #else
107 
108  PRECONDITION(old_data->ref_count!=0);
109 
110  #ifdef IREP_DEBUG
111  std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
112  #endif
113 
114  old_data->ref_count--;
115  if(old_data->ref_count==0)
116  {
117  #ifdef IREP_DEBUG
118  std::cout << "D: " << pretty() << '\n';
119  std::cout << "DELETING " << old_data->data
120  << " " << old_data << '\n';
121  old_data->clear();
122  std::cout << "DEALLOCATING " << old_data << "\n";
123  #endif
124 
125  // may cause recursive call
126  delete old_data;
127 
128  #ifdef IREP_DEBUG
129  std::cout << "DONE\n";
130  #endif
131  }
132  #endif
133 }
134 #endif
135 
138 #ifdef SHARING
140 {
141  std::vector<dt *> stack(1, old_data);
142 
143  while(!stack.empty())
144  {
145  dt *d=stack.back();
146  stack.erase(--stack.end());
147  if(d==&empty_d)
148  continue;
149 
150  INVARIANT(d->ref_count!=0, "All contents of the stack must be in use");
151  d->ref_count--;
152 
153  if(d->ref_count==0)
154  {
155  stack.reserve(
156  stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
157  d->sub.size());
158 
159  for(named_subt::iterator
160  it=d->named_sub.begin();
161  it!=d->named_sub.end();
162  it++)
163  {
164  stack.push_back(it->second.data);
165  it->second.data=&empty_d;
166  }
167 
168  for(subt::iterator
169  it=d->sub.begin();
170  it!=d->sub.end();
171  it++)
172  {
173  stack.push_back(it->data);
174  it->data=&empty_d;
175  }
176 
177  // now delete, won't do recursion
178  delete d;
179  }
180  }
181 }
182 #endif
183 
184 void irept::move_to_named_sub(const irep_namet &name, irept &irep)
185 {
186  #ifdef SHARING
187  detach();
188  #endif
189  add(name).swap(irep);
190  irep.clear();
191 }
192 
194 {
195  #ifdef SHARING
196  detach();
197  #endif
198  get_sub().push_back(get_nil_irep());
199  get_sub().back().swap(irep);
200 }
201 
202 const irep_idt &irept::get(const irep_namet &name) const
203 {
204  const named_subt &s = get_named_sub();
205 
206 #ifdef NAMED_SUB_IS_FORWARD_LIST
207  named_subt::const_iterator it=named_subt_lower_bound(s, name);
208 
209  if(it==s.end() ||
210  it->first!=name)
211  {
212  static const irep_idt empty;
213  return empty;
214  }
215 #else
216  named_subt::const_iterator it=s.find(name);
217 
218  if(it==s.end())
219  {
220  static const irep_idt empty;
221  return empty;
222  }
223 #endif
224 
225  return it->second.id();
226 }
227 
228 bool irept::get_bool(const irep_namet &name) const
229 {
230  return get(name)==ID_1;
231 }
232 
233 int irept::get_int(const irep_namet &name) const
234 {
235  return unsafe_string2int(get_string(name));
236 }
237 
238 unsigned int irept::get_unsigned_int(const irep_namet &name) const
239 {
240  return unsafe_string2unsigned(get_string(name));
241 }
242 
243 std::size_t irept::get_size_t(const irep_namet &name) const
244 {
245  return unsafe_string2size_t(get_string(name));
246 }
247 
248 long long irept::get_long_long(const irep_namet &name) const
249 {
251 }
252 
253 void irept::set(const irep_namet &name, const long long value)
254 {
255  add(name).id(std::to_string(value));
256 }
257 
258 void irept::remove(const irep_namet &name)
259 {
260  named_subt &s = get_named_sub();
261 
262 #ifdef NAMED_SUB_IS_FORWARD_LIST
263  named_subt::iterator it=named_subt_lower_bound(s, name);
264 
265  if(it!=s.end() && it->first==name)
266  {
267  named_subt::iterator before = s.before_begin();
268  while(std::next(before) != it)
269  ++before;
270  s.erase_after(before);
271  }
272 #else
273  s.erase(name);
274 #endif
275 }
276 
277 const irept &irept::find(const irep_namet &name) const
278 {
279  const named_subt &s = get_named_sub();
280 
281 #ifdef NAMED_SUB_IS_FORWARD_LIST
282  named_subt::const_iterator it=named_subt_lower_bound(s, name);
283 
284  if(it==s.end() ||
285  it->first!=name)
286  return get_nil_irep();
287 #else
288  named_subt::const_iterator it=s.find(name);
289 
290  if(it==s.end())
291  return get_nil_irep();
292 #endif
293 
294  return it->second;
295 }
296 
298 {
299  named_subt &s = get_named_sub();
300 
301 #ifdef NAMED_SUB_IS_FORWARD_LIST
302  named_subt::iterator it=named_subt_lower_bound(s, name);
303 
304  if(it==s.end() ||
305  it->first!=name)
306  {
307  named_subt::iterator before = s.before_begin();
308  while(std::next(before) != it)
309  ++before;
310  it = s.emplace_after(before, name, irept());
311  }
312 
313  return it->second;
314 #else
315  return s[name];
316 #endif
317 }
318 
319 irept &irept::add(const irep_namet &name, const irept &irep)
320 {
321  named_subt &s = get_named_sub();
322 
323 #ifdef NAMED_SUB_IS_FORWARD_LIST
324  named_subt::iterator it=named_subt_lower_bound(s, name);
325 
326  if(it==s.end() ||
327  it->first!=name)
328  {
329  named_subt::iterator before = s.before_begin();
330  while(std::next(before) != it)
331  ++before;
332  it = s.emplace_after(before, name, irep);
333  }
334  else
335  it->second=irep;
336 
337  return it->second;
338 #else
339  std::pair<named_subt::iterator, bool> entry=
340  s.insert(std::make_pair(name, irep));
341 
342  if(!entry.second)
343  entry.first->second=irep;
344 
345  return entry.first->second;
346 #endif
347 }
348 
349 #ifdef IREP_HASH_STATS
350 unsigned long long irep_cmp_cnt=0;
351 unsigned long long irep_cmp_ne_cnt=0;
352 #endif
353 
354 bool irept::operator==(const irept &other) const
355 {
356  #ifdef IREP_HASH_STATS
357  ++irep_cmp_cnt;
358  #endif
359  #ifdef SHARING
360  if(data==other.data)
361  return true;
362  #endif
363 
364  if(id() != other.id() || get_sub() != other.get_sub()) // recursive call
365  {
366  #ifdef IREP_HASH_STATS
367  ++irep_cmp_ne_cnt;
368  #endif
369  return false;
370  }
371 
372  const auto &this_named_sub = get_named_sub();
373  const auto &other_named_sub = other.get_named_sub();
374 
375  // walk in sync, ignoring comments, until end of both maps
376  named_subt::const_iterator this_it = this_named_sub.begin();
377  named_subt::const_iterator other_it = other_named_sub.begin();
378 
379  while(this_it != this_named_sub.end() || other_it != other_named_sub.end())
380  {
381  if(this_it != this_named_sub.end() && is_comment(this_it->first))
382  {
383  this_it++;
384  continue;
385  }
386 
387  if(other_it != other_named_sub.end() && is_comment(other_it->first))
388  {
389  other_it++;
390  continue;
391  }
392 
393  if(
394  this_it == this_named_sub.end() || // reached end of 'this'
395  other_it == other_named_sub.end() || // reached the end of 'other'
396  this_it->first != other_it->first ||
397  this_it->second != other_it->second) // recursive call
398  {
399 #ifdef IREP_HASH_STATS
400  ++irep_cmp_ne_cnt;
401 #endif
402  return false;
403  }
404 
405  this_it++;
406  other_it++;
407  }
408 
409  // reached the end of both
410  return true;
411 }
412 
413 bool irept::full_eq(const irept &other) const
414 {
415  #ifdef SHARING
416  if(data==other.data)
417  return true;
418  #endif
419 
420  if(id()!=other.id())
421  return false;
422 
423  const irept::subt &i1_sub=get_sub();
424  const irept::subt &i2_sub=other.get_sub();
425 
426  if(i1_sub.size() != i2_sub.size())
427  return false;
428 
429  const irept::named_subt &i1_named_sub=get_named_sub();
430  const irept::named_subt &i2_named_sub=other.get_named_sub();
431 
432 #ifdef NAMED_SUB_IS_FORWARD_LIST
433  if(
434  std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
435  std::distance(i2_named_sub.begin(), i2_named_sub.end()))
436  {
437  return false;
438  }
439 #else
440  if(i1_named_sub.size() != i2_named_sub.size())
441  return false;
442 #endif
443 
444  for(std::size_t i=0; i<i1_sub.size(); i++)
445  if(!i1_sub[i].full_eq(i2_sub[i]))
446  return false;
447 
448  {
449  irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
450  irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
451 
452  for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
453  if(i1_it->first!=i2_it->first ||
454  !i1_it->second.full_eq(i2_it->second))
455  return false;
456  }
457 
458  return true;
459 }
460 
462 bool irept::ordering(const irept &other) const
463 {
464  return compare(other)<0;
465 
466  #if 0
467  if(X.data<Y.data)
468  return true;
469  if(Y.data<X.data)
470  return false;
471 
472  if(X.sub.size()<Y.sub.size())
473  return true;
474  if(Y.sub.size()<X.sub.size())
475  return false;
476 
477  {
478  irept::subt::const_iterator it1, it2;
479 
480  for(it1=X.sub.begin(),
481  it2=Y.sub.begin();
482  it1!=X.sub.end() && it2!=Y.sub.end();
483  it1++,
484  it2++)
485  {
486  if(ordering(*it1, *it2))
487  return true;
488  if(ordering(*it2, *it1))
489  return false;
490  }
491 
492  INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
493  "Unequal lengths will return before this");
494  }
495 
496  if(X.named_sub.size()<Y.named_sub.size())
497  return true;
498  if(Y.named_sub.size()<X.named_sub.size())
499  return false;
500 
501  {
502  irept::named_subt::const_iterator it1, it2;
503 
504  for(it1=X.named_sub.begin(),
505  it2=Y.named_sub.begin();
506  it1!=X.named_sub.end() && it2!=Y.named_sub.end();
507  it1++,
508  it2++)
509  {
510  if(it1->first<it2->first)
511  return true;
512  if(it2->first<it1->first)
513  return false;
514 
515  if(ordering(it1->second, it2->second))
516  return true;
517  if(ordering(it2->second, it1->second))
518  return false;
519  }
520 
521  INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
522  "Unequal lengths will return before this");
523  }
524 
525  return false;
526  #endif
527 }
528 
531 int irept::compare(const irept &i) const
532 {
533  int r;
534 
535  r=id().compare(i.id());
536  if(r!=0)
537  return r;
538 
539  const subt::size_type size=get_sub().size(),
540  i_size=i.get_sub().size();
541 
542  if(size<i_size)
543  return -1;
544  if(size>i_size)
545  return 1;
546 
547  {
548  irept::subt::const_iterator it1, it2;
549 
550  for(it1=get_sub().begin(),
551  it2=i.get_sub().begin();
552  it1!=get_sub().end() && it2!=i.get_sub().end();
553  it1++,
554  it2++)
555  {
556  r=it1->compare(*it2);
557  if(r!=0)
558  return r;
559  }
560 
561  INVARIANT(it1==get_sub().end() && it2==i.get_sub().end(),
562  "Unequal lengths will return before this");
563  }
564 
565  const auto n_size = number_of_non_comments(get_named_sub()),
566  i_n_size = number_of_non_comments(i.get_named_sub());
567 
568  if(n_size<i_n_size)
569  return -1;
570  if(n_size>i_n_size)
571  return 1;
572 
573  {
574  irept::named_subt::const_iterator it1, it2;
575 
576  // clang-format off
577  for(it1 = get_named_sub().begin(),
578  it2 = i.get_named_sub().begin();
579  it1 != get_named_sub().end() ||
580  it2 != i.get_named_sub().end();
581  ) // no iterator increments
582  // clang-format on
583  {
584  if(it1 != get_named_sub().end() && is_comment(it1->first))
585  {
586  it1++;
587  continue;
588  }
589 
590  if(it2 != i.get_named_sub().end() && is_comment(it2->first))
591  {
592  it2++;
593  continue;
594  }
595 
596  // the case that both it1 and it2 are .end() is treated
597  // by the loop guard; furthermore, the number of non-comments
598  // must be the same
599  INVARIANT(it1 != get_named_sub().end(), "not at end of get_named_sub()");
600  INVARIANT(
601  it2 != i.get_named_sub().end(), "not at end of i.get_named_sub()");
602 
603  r=it1->first.compare(it2->first);
604  if(r!=0)
605  return r;
606 
607  r=it1->second.compare(it2->second);
608  if(r!=0)
609  return r;
610 
611  it1++;
612  it2++;
613  }
614 
615  INVARIANT(
616  it1 == get_named_sub().end() && it2 == i.get_named_sub().end(),
617  "Unequal number of non-comments will return before this");
618  }
619 
620  // equal
621  return 0;
622 }
623 
625 bool irept::operator<(const irept &other) const
626 {
627  return ordering(other);
628 }
629 
630 #ifdef IREP_HASH_STATS
631 unsigned long long irep_hash_cnt=0;
632 #endif
633 
634 std::size_t irept::number_of_non_comments(const named_subt &named_sub)
635 {
636  std::size_t result = 0;
637 
638  for(const auto &n : named_sub)
639  if(!is_comment(n.first))
640  result++;
641 
642  return result;
643 }
644 
645 std::size_t irept::hash() const
646 {
647  #ifdef HASH_CODE
648  if(read().hash_code!=0)
649  return read().hash_code;
650  #endif
651 
652  const irept::subt &sub=get_sub();
653  const irept::named_subt &named_sub=get_named_sub();
654 
655  std::size_t result=hash_string(id());
656 
657  forall_irep(it, sub) result=hash_combine(result, it->hash());
658 
659  std::size_t number_of_named_ireps = 0;
660 
661  forall_named_irep(it, named_sub)
662  if(!is_comment(it->first)) // this variant ignores comments
663  {
664  result = hash_combine(result, hash_string(it->first));
665  result = hash_combine(result, it->second.hash());
666  number_of_named_ireps++;
667  }
668 
669  result = hash_finalize(result, sub.size() + number_of_named_ireps);
670 
671 #ifdef HASH_CODE
672  read().hash_code=result;
673 #endif
674 #ifdef IREP_HASH_STATS
675  ++irep_hash_cnt;
676 #endif
677  return result;
678 }
679 
680 std::size_t irept::full_hash() const
681 {
682  const irept::subt &sub=get_sub();
683  const irept::named_subt &named_sub=get_named_sub();
684 
685  std::size_t result=hash_string(id());
686 
687  forall_irep(it, sub) result=hash_combine(result, it->full_hash());
688 
689  // this variant includes all named_sub elements
690  forall_named_irep(it, named_sub)
691  {
692  result=hash_combine(result, hash_string(it->first));
693  result=hash_combine(result, it->second.full_hash());
694  }
695 
696 #ifdef NAMED_SUB_IS_FORWARD_LIST
697  const std::size_t named_sub_size =
698  std::distance(named_sub.begin(), named_sub.end());
699 #else
700  const std::size_t named_sub_size = named_sub.size();
701 #endif
702  result = hash_finalize(result, named_sub_size + sub.size());
703 
704  return result;
705 }
706 
707 static void indent_str(std::string &s, unsigned indent)
708 {
709  for(unsigned i=0; i<indent; i++)
710  s+=' ';
711 }
712 
713 std::string irept::pretty(unsigned indent, unsigned max_indent) const
714 {
715  if(max_indent>0 && indent>max_indent)
716  return "";
717 
718  std::string result;
719 
720  if(!id().empty())
721  {
722  result+=id_string();
723  indent+=2;
724  }
725 
727  {
728  result+="\n";
729  indent_str(result, indent);
730 
731  result+="* ";
732  result+=id2string(it->first);
733  result+=": ";
734 
735  result+=it->second.pretty(indent+2, max_indent);
736  }
737 
738  std::size_t count=0;
739 
740  forall_irep(it, get_sub())
741  {
742  result+="\n";
743  indent_str(result, indent);
744 
745  result+=std::to_string(count++);
746  result+=": ";
747 
748  result+=it->pretty(indent+2, max_indent);
749  }
750 
751  return result;
752 }
753 
755  : irep(irep)
756 {
757 }
const irept & get_nil_irep()
Definition: irep.cpp:55
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
subt sub
Definition: irep.h:347
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition: irep.cpp:531
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:713
std::vector< irept > subt
Definition: irep.h:157
void move_to_sub(irept &irep)
Definition: irep.cpp:193
std::size_t hash() const
Definition: irep.cpp:645
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool full_eq(const irept &other) const
Definition: irep.cpp:413
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:233
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
Definition: string2int.cpp:79
unsignedbv_typet size_type()
Definition: c_types.cpp:58
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
#define forall_named_irep(it, irep)
Definition: irep.h:70
named_subt named_sub
Definition: irep.h:346
subt & get_sub()
Definition: irep.h:314
const dt & read() const
Definition: irep.h:400
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:754
const irep_idt & id() const
Definition: irep.h:256
dt * data
Definition: irep.h:392
unsigned ref_count
Definition: irep.h:339
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:74
static void indent_str(std::string &s, unsigned indent)
Definition: irep.cpp:707
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:202
#define hash_finalize(h1, len)
Definition: irep_hash.h:122
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition: irep.cpp:139
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Base class for tree-like data structures with sharing.
Definition: irep.h:153
std::map< irep_namet, irept > named_subt
Definition: irep.h:166
irept()
Definition: irep.h:182
void detach()
Definition: irep.cpp:63
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
static dt empty_d
Definition: irep.h:393
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:625
static void remove_ref(dt *old_data)
Definition: irep.cpp:99
named_subt & get_named_sub()
Definition: irep.h:316
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:462
irept nil_rep_storage
Definition: irep.cpp:28
size_t hash_string(const dstringt &s)
Definition: dstring.h:190
irep hash functions
static bool is_comment(const irep_namet &name)
Definition: irep.h:327
irep_idt data
This irep_idt is the only place to store data in an irep, other than the mere nesting structure...
Definition: irep.h:344
int compare(const dstringt &b) const
Definition: dstring.h:120
std::size_t full_hash() const
Definition: irep.cpp:680
void clear()
Definition: irep.h:310
irept & add(const irep_namet &name)
Definition: irep.cpp:297
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:269
const std::string & id_string() const
Definition: irep.h:259
void swap(irept &irep)
Definition: irep.h:300
void clear()
Definition: irep.h:353
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:238
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:248
#define hash_combine(h1, h2)
Definition: irep_hash.h:120
bool operator==(const irept &other) const
Definition: irep.cpp:354
void remove(const irep_namet &name)
Definition: irep.cpp:258
#define stack(x)
Definition: parser.h:144
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:243
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:277
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:283
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:184
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:634
#define forall_irep(it, irep)
Definition: irep.h:62