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 SUB_IS_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 SUB_IS_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(stack.size()+
156  d->named_sub.size()+
157  d->comments.size()+
158  d->sub.size());
159 
160  for(named_subt::iterator
161  it=d->named_sub.begin();
162  it!=d->named_sub.end();
163  it++)
164  {
165  stack.push_back(it->second.data);
166  it->second.data=&empty_d;
167  }
168 
169  for(named_subt::iterator
170  it=d->comments.begin();
171  it!=d->comments.end();
172  it++)
173  {
174  stack.push_back(it->second.data);
175  it->second.data=&empty_d;
176  }
177 
178  for(subt::iterator
179  it=d->sub.begin();
180  it!=d->sub.end();
181  it++)
182  {
183  stack.push_back(it->data);
184  it->data=&empty_d;
185  }
186 
187  // now delete, won't do recursion
188  delete d;
189  }
190  }
191 }
192 #endif
193 
194 void irept::move_to_named_sub(const irep_namet &name, irept &irep)
195 {
196  #ifdef SHARING
197  detach();
198  #endif
199  add(name).swap(irep);
200  irep.clear();
201 }
202 
204 {
205  #ifdef SHARING
206  detach();
207  #endif
208  get_sub().push_back(get_nil_irep());
209  get_sub().back().swap(irep);
210 }
211 
212 const irep_idt &irept::get(const irep_namet &name) const
213 {
214  const named_subt &s=
216 
217  #ifdef SUB_IS_LIST
218  named_subt::const_iterator it=named_subt_lower_bound(s, name);
219 
220  if(it==s.end() ||
221  it->first!=name)
222  {
223  static const irep_idt empty;
224  return empty;
225  }
226  #else
227  named_subt::const_iterator it=s.find(name);
228 
229  if(it==s.end())
230  {
231  static const irep_idt empty;
232  return empty;
233  }
234  #endif
235 
236  return it->second.id();
237 }
238 
239 bool irept::get_bool(const irep_namet &name) const
240 {
241  return get(name)==ID_1;
242 }
243 
244 int irept::get_int(const irep_namet &name) const
245 {
246  return unsafe_string2int(get_string(name));
247 }
248 
249 unsigned int irept::get_unsigned_int(const irep_namet &name) const
250 {
251  return unsafe_string2unsigned(get_string(name));
252 }
253 
254 std::size_t irept::get_size_t(const irep_namet &name) const
255 {
256  return unsafe_string2size_t(get_string(name));
257 }
258 
259 long long irept::get_long_long(const irep_namet &name) const
260 {
262 }
263 
264 void irept::set(const irep_namet &name, const long long value)
265 {
266  add(name).id(std::to_string(value));
267 }
268 
269 void irept::remove(const irep_namet &name)
270 {
271  named_subt &s=
273 
274  #ifdef SUB_IS_LIST
275  named_subt::iterator it=named_subt_lower_bound(s, name);
276 
277  if(it!=s.end() && it->first==name)
278  s.erase(it);
279  #else
280  s.erase(name);
281  #endif
282 }
283 
284 const irept &irept::find(const irep_namet &name) const
285 {
286  const named_subt &s=
288 
289  #ifdef SUB_IS_LIST
290  named_subt::const_iterator it=named_subt_lower_bound(s, name);
291 
292  if(it==s.end() ||
293  it->first!=name)
294  return get_nil_irep();
295  #else
296  named_subt::const_iterator it=s.find(name);
297 
298  if(it==s.end())
299  return get_nil_irep();
300  #endif
301 
302  return it->second;
303 }
304 
306 {
307  named_subt &s=
309 
310  #ifdef SUB_IS_LIST
311  named_subt::iterator it=named_subt_lower_bound(s, name);
312 
313  if(it==s.end() ||
314  it->first!=name)
315  it=s.insert(it, std::make_pair(name, irept()));
316 
317  return it->second;
318  #else
319  return s[name];
320  #endif
321 }
322 
323 irept &irept::add(const irep_namet &name, const irept &irep)
324 {
325  named_subt &s=
327 
328  #ifdef SUB_IS_LIST
329  named_subt::iterator it=named_subt_lower_bound(s, name);
330 
331  if(it==s.end() ||
332  it->first!=name)
333  it=s.insert(it, std::make_pair(name, irep));
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() ||
365  get_sub()!=other.get_sub() || // recursive call
366  get_named_sub()!=other.get_named_sub()) // recursive call
367  {
368  #ifdef IREP_HASH_STATS
369  ++irep_cmp_ne_cnt;
370  #endif
371  return false;
372  }
373 
374  // comments are NOT checked
375 
376  return true;
377 }
378 
379 bool irept::full_eq(const irept &other) const
380 {
381  #ifdef SHARING
382  if(data==other.data)
383  return true;
384  #endif
385 
386  if(id()!=other.id())
387  return false;
388 
389  const irept::subt &i1_sub=get_sub();
390  const irept::subt &i2_sub=other.get_sub();
391  const irept::named_subt &i1_named_sub=get_named_sub();
392  const irept::named_subt &i2_named_sub=other.get_named_sub();
393  const irept::named_subt &i1_comments=get_comments();
394  const irept::named_subt &i2_comments=other.get_comments();
395 
396  if(i1_sub.size()!=i2_sub.size() ||
397  i1_named_sub.size()!=i2_named_sub.size() ||
398  i1_comments.size()!=i2_comments.size())
399  return false;
400 
401  for(std::size_t i=0; i<i1_sub.size(); i++)
402  if(!i1_sub[i].full_eq(i2_sub[i]))
403  return false;
404 
405  {
406  irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
407  irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
408 
409  for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
410  if(i1_it->first!=i2_it->first ||
411  !i1_it->second.full_eq(i2_it->second))
412  return false;
413  }
414 
415  {
416  irept::named_subt::const_iterator i1_it=i1_comments.begin();
417  irept::named_subt::const_iterator i2_it=i2_comments.begin();
418 
419  for(; i1_it!=i1_comments.end(); i1_it++, i2_it++)
420  if(i1_it->first!=i2_it->first ||
421  !i1_it->second.full_eq(i2_it->second))
422  return false;
423  }
424 
425  return true;
426 }
427 
429 bool irept::ordering(const irept &other) const
430 {
431  return compare(other)<0;
432 
433  #if 0
434  if(X.data<Y.data)
435  return true;
436  if(Y.data<X.data)
437  return false;
438 
439  if(X.sub.size()<Y.sub.size())
440  return true;
441  if(Y.sub.size()<X.sub.size())
442  return false;
443 
444  {
445  irept::subt::const_iterator it1, it2;
446 
447  for(it1=X.sub.begin(),
448  it2=Y.sub.begin();
449  it1!=X.sub.end() && it2!=Y.sub.end();
450  it1++,
451  it2++)
452  {
453  if(ordering(*it1, *it2))
454  return true;
455  if(ordering(*it2, *it1))
456  return false;
457  }
458 
459  INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
460  "Unequal lengths will return before this");
461  }
462 
463  if(X.named_sub.size()<Y.named_sub.size())
464  return true;
465  if(Y.named_sub.size()<X.named_sub.size())
466  return false;
467 
468  {
469  irept::named_subt::const_iterator it1, it2;
470 
471  for(it1=X.named_sub.begin(),
472  it2=Y.named_sub.begin();
473  it1!=X.named_sub.end() && it2!=Y.named_sub.end();
474  it1++,
475  it2++)
476  {
477  if(it1->first<it2->first)
478  return true;
479  if(it2->first<it1->first)
480  return false;
481 
482  if(ordering(it1->second, it2->second))
483  return true;
484  if(ordering(it2->second, it1->second))
485  return false;
486  }
487 
488  INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
489  "Unequal lengths will return before this");
490  }
491 
492  return false;
493  #endif
494 }
495 
497 int irept::compare(const irept &i) const
498 {
499  int r;
500 
501  r=id().compare(i.id());
502  if(r!=0)
503  return r;
504 
505  const subt::size_type size=get_sub().size(),
506  i_size=i.get_sub().size();
507  if(size<i_size)
508  return -1;
509  if(size>i_size)
510  return 1;
511 
512  {
513  irept::subt::const_iterator it1, it2;
514 
515  for(it1=get_sub().begin(),
516  it2=i.get_sub().begin();
517  it1!=get_sub().end() && it2!=i.get_sub().end();
518  it1++,
519  it2++)
520  {
521  r=it1->compare(*it2);
522  if(r!=0)
523  return r;
524  }
525 
526  INVARIANT(it1==get_sub().end() && it2==i.get_sub().end(),
527  "Unequal lengths will return before this");
528  }
529 
530  const named_subt::size_type n_size=get_named_sub().size(),
531  i_n_size=i.get_named_sub().size();
532  if(n_size<i_n_size)
533  return -1;
534  if(n_size>i_n_size)
535  return 1;
536 
537  {
538  irept::named_subt::const_iterator it1, it2;
539 
540  for(it1=get_named_sub().begin(),
541  it2=i.get_named_sub().begin();
542  it1!=get_named_sub().end() && it2!=i.get_named_sub().end();
543  it1++,
544  it2++)
545  {
546  r=it1->first.compare(it2->first);
547  if(r!=0)
548  return r;
549 
550  r=it1->second.compare(it2->second);
551  if(r!=0)
552  return r;
553  }
554 
555  INVARIANT(it1==get_named_sub().end() &&
556  it2==i.get_named_sub().end(),
557  "Unequal lengths will return before this");
558  }
559 
560  // equal
561  return 0;
562 }
563 
565 bool irept::operator<(const irept &other) const
566 {
567  return ordering(other);
568 }
569 
570 #ifdef IREP_HASH_STATS
571 unsigned long long irep_hash_cnt=0;
572 #endif
573 
574 std::size_t irept::hash() const
575 {
576  #ifdef HASH_CODE
577  if(read().hash_code!=0)
578  return read().hash_code;
579  #endif
580 
581  const irept::subt &sub=get_sub();
582  const irept::named_subt &named_sub=get_named_sub();
583 
584  std::size_t result=hash_string(id());
585 
586  forall_irep(it, sub) result=hash_combine(result, it->hash());
587 
588  forall_named_irep(it, named_sub)
589  {
590  result=hash_combine(result, hash_string(it->first));
591  result=hash_combine(result, it->second.hash());
592  }
593 
594  result=hash_finalize(result, named_sub.size()+sub.size());
595 
596  #ifdef HASH_CODE
597  read().hash_code=result;
598  #endif
599  #ifdef IREP_HASH_STATS
600  ++irep_hash_cnt;
601  #endif
602  return result;
603 }
604 
605 std::size_t irept::full_hash() const
606 {
607  const irept::subt &sub=get_sub();
608  const irept::named_subt &named_sub=get_named_sub();
609  const irept::named_subt &comments=get_comments();
610 
611  std::size_t result=hash_string(id());
612 
613  forall_irep(it, sub) result=hash_combine(result, it->full_hash());
614 
615  forall_named_irep(it, named_sub)
616  {
617  result=hash_combine(result, hash_string(it->first));
618  result=hash_combine(result, it->second.full_hash());
619  }
620 
621  forall_named_irep(it, comments)
622  {
623  result=hash_combine(result, hash_string(it->first));
624  result=hash_combine(result, it->second.full_hash());
625  }
626 
627  result=hash_finalize(
628  result,
629  named_sub.size()+sub.size()+comments.size());
630 
631  return result;
632 }
633 
634 static void indent_str(std::string &s, unsigned indent)
635 {
636  for(unsigned i=0; i<indent; i++)
637  s+=' ';
638 }
639 
640 std::string irept::pretty(unsigned indent, unsigned max_indent) const
641 {
642  if(max_indent>0 && indent>max_indent)
643  return "";
644 
645  std::string result;
646 
647  if(!id().empty())
648  {
649  result+=id_string();
650  indent+=2;
651  }
652 
654  {
655  result+="\n";
656  indent_str(result, indent);
657 
658  result+="* ";
659  result+=id2string(it->first);
660  result+=": ";
661 
662  result+=it->second.pretty(indent+2, max_indent);
663  }
664 
666  {
667  result+="\n";
668  indent_str(result, indent);
669 
670  result+="* ";
671  result+=id2string(it->first);
672  result+=": ";
673 
674  result+=it->second.pretty(indent+2, max_indent);
675  }
676 
677  std::size_t count=0;
678 
679  forall_irep(it, get_sub())
680  {
681  result+="\n";
682  indent_str(result, indent);
683 
684  result+=std::to_string(count++);
685  result+=": ";
686 
687  result+=it->pretty(indent+2, max_indent);
688  }
689 
690  return result;
691 }
692 
694  : irep(irep)
695 {
696 }
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:351
int compare(const irept &i) const
defines ordering on the internal representation
Definition: irep.cpp:497
named_subt comments
Definition: irep.h:350
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
std::vector< irept > subt
Definition: irep.h:160
void move_to_sub(irept &irep)
Definition: irep.cpp:203
std::size_t hash() const
Definition: irep.cpp:574
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool full_eq(const irept &other) const
Definition: irep.cpp:379
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:244
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:239
#define POSTCONDITION(CONDITION)
Definition: invariant.h:443
#define forall_named_irep(it, irep)
Definition: irep.h:70
named_subt named_sub
Definition: irep.h:349
subt & get_sub()
Definition: irep.h:317
const dt & read() const
Definition: irep.h:406
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:693
const irep_idt & id() const
Definition: irep.h:259
dt * data
Definition: irep.h:398
unsigned ref_count
Definition: irep.h:342
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:634
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
#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:427
named_subt & get_comments()
Definition: irep.h:321
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::map< irep_namet, irept > named_subt
Definition: irep.h:169
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:399
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:565
static void remove_ref(dt *old_data)
Definition: irep.cpp:99
named_subt & get_named_sub()
Definition: irep.h:319
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:429
irept nil_rep_storage
Definition: irep.cpp:28
size_t hash_string(const dstringt &s)
Definition: dstring.h:179
irep hash functions
static bool is_comment(const irep_namet &name)
Definition: irep.h:332
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:347
int compare(const dstringt &b) const
Definition: dstring.h:120
std::size_t full_hash() const
Definition: irep.cpp:605
void clear()
Definition: irep.h:313
irept & add(const irep_namet &name)
Definition: irep.cpp:305
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
void clear()
Definition: irep.h:357
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:249
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:259
#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:269
#define stack(x)
Definition: parser.h:144
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
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:284
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:194
#define forall_irep(it, irep)
Definition: irep.h:62