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