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