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