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 NAMED_SUB_IS_FORWARD_LIST
31 static inline bool named_subt_order(
32  const std::pair<irep_namet, irept> &a,
33  const irep_namet &b)
34 {
35  return a.first<b;
36 }
37 
38 static inline irept::named_subt::const_iterator named_subt_lower_bound(
39  const irept::named_subt &s, const irep_namet &id)
40 {
41  return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
42 }
43 
44 static inline irept::named_subt::iterator named_subt_lower_bound(
45  irept::named_subt &s, const irep_namet &id)
46 {
47  return std::lower_bound(s.begin(), s.end(), id, named_subt_order);
48 }
49 #endif
50 
52 {
53  if(nil_rep_storage.id().empty()) // initialized?
54  nil_rep_storage.id(ID_nil);
55  return nil_rep_storage;
56 }
57 
58 void irept::move_to_named_sub(const irep_namet &name, irept &irep)
59 {
60  #ifdef SHARING
61  detach();
62  #endif
63  add(name).swap(irep);
64  irep.clear();
65 }
66 
68 {
69  #ifdef SHARING
70  detach();
71  #endif
72  get_sub().push_back(get_nil_irep());
73  get_sub().back().swap(irep);
74 }
75 
76 const irep_idt &irept::get(const irep_namet &name) const
77 {
78  const named_subt &s = get_named_sub();
79 
80 #ifdef NAMED_SUB_IS_FORWARD_LIST
81  named_subt::const_iterator it=named_subt_lower_bound(s, name);
82 
83  if(it==s.end() ||
84  it->first!=name)
85  {
86  static const irep_idt empty;
87  return empty;
88  }
89 #else
90  named_subt::const_iterator it=s.find(name);
91 
92  if(it==s.end())
93  {
94  static const irep_idt empty;
95  return empty;
96  }
97 #endif
98 
99  return it->second.id();
100 }
101 
102 bool irept::get_bool(const irep_namet &name) const
103 {
104  return get(name)==ID_1;
105 }
106 
107 int irept::get_int(const irep_namet &name) const
108 {
109  return unsafe_string2int(get_string(name));
110 }
111 
112 std::size_t irept::get_size_t(const irep_namet &name) const
113 {
114  return unsafe_string2size_t(get_string(name));
115 }
116 
117 long long irept::get_long_long(const irep_namet &name) const
118 {
120 }
121 
122 void irept::set(const irep_namet &name, const long long value)
123 {
124 #ifdef USE_DSTRING
125  add(name).id(to_dstring(value));
126 #else
127  add(name).id(std::to_string(value));
128 #endif
129 }
130 
131 void irept::remove(const irep_namet &name)
132 {
133  named_subt &s = get_named_sub();
134 
135 #ifdef NAMED_SUB_IS_FORWARD_LIST
136  named_subt::iterator it=named_subt_lower_bound(s, name);
137 
138  if(it!=s.end() && it->first==name)
139  {
140  named_subt::iterator before = s.before_begin();
141  while(std::next(before) != it)
142  ++before;
143  s.erase_after(before);
144  }
145 #else
146  s.erase(name);
147 #endif
148 }
149 
150 const irept &irept::find(const irep_namet &name) const
151 {
152  const named_subt &s = get_named_sub();
153 
154 #ifdef NAMED_SUB_IS_FORWARD_LIST
155  named_subt::const_iterator it=named_subt_lower_bound(s, name);
156 
157  if(it==s.end() ||
158  it->first!=name)
159  return get_nil_irep();
160 #else
161  named_subt::const_iterator it=s.find(name);
162 
163  if(it==s.end())
164  return get_nil_irep();
165 #endif
166 
167  return it->second;
168 }
169 
171 {
172  named_subt &s = get_named_sub();
173 
174 #ifdef NAMED_SUB_IS_FORWARD_LIST
175  named_subt::iterator it=named_subt_lower_bound(s, name);
176 
177  if(it==s.end() ||
178  it->first!=name)
179  {
180  named_subt::iterator before = s.before_begin();
181  while(std::next(before) != it)
182  ++before;
183  it = s.emplace_after(before, name, irept());
184  }
185 
186  return it->second;
187 #else
188  return s[name];
189 #endif
190 }
191 
192 irept &irept::add(const irep_namet &name, irept irep)
193 {
194  named_subt &s = get_named_sub();
195 
196 #ifdef NAMED_SUB_IS_FORWARD_LIST
197  named_subt::iterator it=named_subt_lower_bound(s, name);
198 
199  if(it==s.end() ||
200  it->first!=name)
201  {
202  named_subt::iterator before = s.before_begin();
203  while(std::next(before) != it)
204  ++before;
205  it = s.emplace_after(before, name, std::move(irep));
206  }
207  else
208  it->second = std::move(irep);
209 
210  return it->second;
211 #else
212  std::pair<named_subt::iterator, bool> entry = s.emplace(
213  std::piecewise_construct,
214  std::forward_as_tuple(name),
215  std::forward_as_tuple(irep));
216 
217  if(!entry.second)
218  entry.first->second = std::move(irep);
219 
220  return entry.first->second;
221 #endif
222 }
223 
224 #ifdef IREP_HASH_STATS
225 unsigned long long irep_cmp_cnt=0;
226 unsigned long long irep_cmp_ne_cnt=0;
227 #endif
228 
229 bool irept::operator==(const irept &other) const
230 {
231  #ifdef IREP_HASH_STATS
232  ++irep_cmp_cnt;
233  #endif
234  #ifdef SHARING
235  if(data==other.data)
236  return true;
237  #endif
238 
239  if(id() != other.id() || get_sub() != other.get_sub()) // recursive call
240  {
241  #ifdef IREP_HASH_STATS
242  ++irep_cmp_ne_cnt;
243  #endif
244  return false;
245  }
246 
247  const auto &this_named_sub = get_named_sub();
248  const auto &other_named_sub = other.get_named_sub();
249 
250  // walk in sync, ignoring comments, until end of both maps
251  named_subt::const_iterator this_it = this_named_sub.begin();
252  named_subt::const_iterator other_it = other_named_sub.begin();
253 
254  while(this_it != this_named_sub.end() || other_it != other_named_sub.end())
255  {
256  if(this_it != this_named_sub.end() && is_comment(this_it->first))
257  {
258  this_it++;
259  continue;
260  }
261 
262  if(other_it != other_named_sub.end() && is_comment(other_it->first))
263  {
264  other_it++;
265  continue;
266  }
267 
268  if(
269  this_it == this_named_sub.end() || // reached end of 'this'
270  other_it == other_named_sub.end() || // reached the end of 'other'
271  this_it->first != other_it->first ||
272  this_it->second != other_it->second) // recursive call
273  {
274 #ifdef IREP_HASH_STATS
275  ++irep_cmp_ne_cnt;
276 #endif
277  return false;
278  }
279 
280  this_it++;
281  other_it++;
282  }
283 
284  // reached the end of both
285  return true;
286 }
287 
288 bool irept::full_eq(const irept &other) const
289 {
290  #ifdef SHARING
291  if(data==other.data)
292  return true;
293  #endif
294 
295  if(id()!=other.id())
296  return false;
297 
298  const irept::subt &i1_sub=get_sub();
299  const irept::subt &i2_sub=other.get_sub();
300 
301  if(i1_sub.size() != i2_sub.size())
302  return false;
303 
304  const irept::named_subt &i1_named_sub=get_named_sub();
305  const irept::named_subt &i2_named_sub=other.get_named_sub();
306 
307 #ifdef NAMED_SUB_IS_FORWARD_LIST
308  if(
309  std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
310  std::distance(i2_named_sub.begin(), i2_named_sub.end()))
311  {
312  return false;
313  }
314 #else
315  if(i1_named_sub.size() != i2_named_sub.size())
316  return false;
317 #endif
318 
319  for(std::size_t i=0; i<i1_sub.size(); i++)
320  if(!i1_sub[i].full_eq(i2_sub[i]))
321  return false;
322 
323  {
324  irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
325  irept::named_subt::const_iterator i2_it=i2_named_sub.begin();
326 
327  for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
328  if(i1_it->first!=i2_it->first ||
329  !i1_it->second.full_eq(i2_it->second))
330  return false;
331  }
332 
333  return true;
334 }
335 
337 bool irept::ordering(const irept &other) const
338 {
339  return compare(other)<0;
340 
341  #if 0
342  if(X.data<Y.data)
343  return true;
344  if(Y.data<X.data)
345  return false;
346 
347  if(X.sub.size()<Y.sub.size())
348  return true;
349  if(Y.sub.size()<X.sub.size())
350  return false;
351 
352  {
353  irept::subt::const_iterator it1, it2;
354 
355  for(it1=X.sub.begin(),
356  it2=Y.sub.begin();
357  it1!=X.sub.end() && it2!=Y.sub.end();
358  it1++,
359  it2++)
360  {
361  if(ordering(*it1, *it2))
362  return true;
363  if(ordering(*it2, *it1))
364  return false;
365  }
366 
367  INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
368  "Unequal lengths will return before this");
369  }
370 
371  if(X.named_sub.size()<Y.named_sub.size())
372  return true;
373  if(Y.named_sub.size()<X.named_sub.size())
374  return false;
375 
376  {
377  irept::named_subt::const_iterator it1, it2;
378 
379  for(it1=X.named_sub.begin(),
380  it2=Y.named_sub.begin();
381  it1!=X.named_sub.end() && it2!=Y.named_sub.end();
382  it1++,
383  it2++)
384  {
385  if(it1->first<it2->first)
386  return true;
387  if(it2->first<it1->first)
388  return false;
389 
390  if(ordering(it1->second, it2->second))
391  return true;
392  if(ordering(it2->second, it1->second))
393  return false;
394  }
395 
396  INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
397  "Unequal lengths will return before this");
398  }
399 
400  return false;
401  #endif
402 }
403 
406 int irept::compare(const irept &i) const
407 {
408  int r;
409 
410  r=id().compare(i.id());
411  if(r!=0)
412  return r;
413 
414  const subt::size_type size=get_sub().size(),
415  i_size=i.get_sub().size();
416 
417  if(size<i_size)
418  return -1;
419  if(size>i_size)
420  return 1;
421 
422  {
423  irept::subt::const_iterator it1, it2;
424 
425  for(it1=get_sub().begin(),
426  it2=i.get_sub().begin();
427  it1!=get_sub().end() && it2!=i.get_sub().end();
428  it1++,
429  it2++)
430  {
431  r=it1->compare(*it2);
432  if(r!=0)
433  return r;
434  }
435 
436  INVARIANT(it1==get_sub().end() && it2==i.get_sub().end(),
437  "Unequal lengths will return before this");
438  }
439 
440  const auto n_size = number_of_non_comments(get_named_sub()),
441  i_n_size = number_of_non_comments(i.get_named_sub());
442 
443  if(n_size<i_n_size)
444  return -1;
445  if(n_size>i_n_size)
446  return 1;
447 
448  {
449  irept::named_subt::const_iterator it1, it2;
450 
451  // clang-format off
452  for(it1 = get_named_sub().begin(),
453  it2 = i.get_named_sub().begin();
454  it1 != get_named_sub().end() ||
455  it2 != i.get_named_sub().end();
456  ) // no iterator increments
457  // clang-format on
458  {
459  if(it1 != get_named_sub().end() && is_comment(it1->first))
460  {
461  it1++;
462  continue;
463  }
464 
465  if(it2 != i.get_named_sub().end() && is_comment(it2->first))
466  {
467  it2++;
468  continue;
469  }
470 
471  // the case that both it1 and it2 are .end() is treated
472  // by the loop guard; furthermore, the number of non-comments
473  // must be the same
474  INVARIANT(it1 != get_named_sub().end(), "not at end of get_named_sub()");
475  INVARIANT(
476  it2 != i.get_named_sub().end(), "not at end of i.get_named_sub()");
477 
478  r=it1->first.compare(it2->first);
479  if(r!=0)
480  return r;
481 
482  r=it1->second.compare(it2->second);
483  if(r!=0)
484  return r;
485 
486  it1++;
487  it2++;
488  }
489 
490  INVARIANT(
491  it1 == get_named_sub().end() && it2 == i.get_named_sub().end(),
492  "Unequal number of non-comments will return before this");
493  }
494 
495  // equal
496  return 0;
497 }
498 
500 bool irept::operator<(const irept &other) const
501 {
502  return ordering(other);
503 }
504 
505 #ifdef IREP_HASH_STATS
506 unsigned long long irep_hash_cnt=0;
507 #endif
508 
509 std::size_t irept::number_of_non_comments(const named_subt &named_sub)
510 {
511  std::size_t result = 0;
512 
513  for(const auto &n : named_sub)
514  if(!is_comment(n.first))
515  result++;
516 
517  return result;
518 }
519 
520 std::size_t irept::hash() const
521 {
522  #ifdef HASH_CODE
523  if(read().hash_code!=0)
524  return read().hash_code;
525  #endif
526 
527  const irept::subt &sub=get_sub();
528  const irept::named_subt &named_sub=get_named_sub();
529 
530  std::size_t result=hash_string(id());
531 
532  forall_irep(it, sub) result=hash_combine(result, it->hash());
533 
534  std::size_t number_of_named_ireps = 0;
535 
536  forall_named_irep(it, named_sub)
537  if(!is_comment(it->first)) // this variant ignores comments
538  {
539  result = hash_combine(result, hash_string(it->first));
540  result = hash_combine(result, it->second.hash());
541  number_of_named_ireps++;
542  }
543 
544  result = hash_finalize(result, sub.size() + number_of_named_ireps);
545 
546 #ifdef HASH_CODE
547  read().hash_code=result;
548 #endif
549 #ifdef IREP_HASH_STATS
550  ++irep_hash_cnt;
551 #endif
552  return result;
553 }
554 
555 std::size_t irept::full_hash() const
556 {
557  const irept::subt &sub=get_sub();
558  const irept::named_subt &named_sub=get_named_sub();
559 
560  std::size_t result=hash_string(id());
561 
562  forall_irep(it, sub) result=hash_combine(result, it->full_hash());
563 
564  // this variant includes all named_sub elements
565  forall_named_irep(it, named_sub)
566  {
567  result=hash_combine(result, hash_string(it->first));
568  result=hash_combine(result, it->second.full_hash());
569  }
570 
571 #ifdef NAMED_SUB_IS_FORWARD_LIST
572  const std::size_t named_sub_size =
573  std::distance(named_sub.begin(), named_sub.end());
574 #else
575  const std::size_t named_sub_size = named_sub.size();
576 #endif
577  result = hash_finalize(result, named_sub_size + sub.size());
578 
579  return result;
580 }
581 
582 static void indent_str(std::string &s, unsigned indent)
583 {
584  for(unsigned i=0; i<indent; i++)
585  s+=' ';
586 }
587 
588 std::string irept::pretty(unsigned indent, unsigned max_indent) const
589 {
590  if(max_indent>0 && indent>max_indent)
591  return "";
592 
593  std::string result;
594 
595  if(!id().empty())
596  {
597  result+=id_string();
598  indent+=2;
599  }
600 
602  {
603  result+="\n";
604  indent_str(result, indent);
605 
606  result+="* ";
607  result+=id2string(it->first);
608  result+=": ";
609 
610  result+=it->second.pretty(indent+2, max_indent);
611  }
612 
613  std::size_t count=0;
614 
615  forall_irep(it, get_sub())
616  {
617  result+="\n";
618  indent_str(result, indent);
619 
620  result+=std::to_string(count++);
621  result+=": ";
622 
623  result+=it->pretty(indent+2, max_indent);
624  }
625 
626  return result;
627 }
628 
630  : irep(irep)
631 {
632 }
const irept & get_nil_irep()
Definition: irep.cpp:51
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:42
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition: irep.cpp:406
dt * data
Definition: irep.h:265
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:588
void move_to_sub(irept &irep)
Definition: irep.cpp:67
std::size_t hash() const
Definition: irep.cpp:520
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool full_eq(const irept &other) const
Definition: irep.cpp:288
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:107
irept()=default
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
Definition: string2int.cpp:48
unsignedbv_typet size_type()
Definition: c_types.cpp:58
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:102
#define forall_named_irep(it, irep)
Definition: irep.h:68
subt & get_sub()
Definition: irep.h:472
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:629
const irep_idt & id() const
Definition: irep.h:413
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:43
static void indent_str(std::string &s, unsigned indent)
Definition: irep.cpp:582
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:76
#define hash_finalize(h1, len)
Definition: irep_hash.h:122
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
const dt & read() const
Definition: irep.h:273
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:500
named_subt & get_named_sub()
Definition: irep.h:474
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:337
irept nil_rep_storage
Definition: irep.cpp:28
size_t hash_string(const dstringt &s)
Definition: dstring.h:211
irep hash functions
static bool is_comment(const irep_namet &name)
Definition: irep.h:484
int compare(const dstringt &b) const
Definition: dstring.h:133
std::size_t full_hash() const
Definition: irep.cpp:555
void clear()
Definition: irep.h:468
typename dt::subt subt
Definition: irep.h:185
irept & add(const irep_namet &name)
Definition: irep.cpp:170
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:426
const std::string & id_string() const
Definition: irep.h:416
void swap(irept &irep)
Definition: irep.h:458
typename dt::named_subt named_subt
Definition: irep.h:186
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:117
#define hash_combine(h1, h2)
Definition: irep_hash.h:120
static std::enable_if< std::is_integral< T >::value, dstringt >::type to_dstring(T value)
equivalent to dstringt(std::to_string(value)), i.e., produces a string from a number ...
Definition: dstring.h:251
bool operator==(const irept &other) const
Definition: irep.cpp:229
void remove(const irep_namet &name)
Definition: irep.cpp:131
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:112
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:33
bool empty() const
Definition: dstring.h:88
const irept & find(const irep_namet &name) const
Definition: irep.cpp:150
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:437
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:58
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:509
#define forall_irep(it, irep)
Definition: irep.h:60