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