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