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