cprover
Loading...
Searching...
No Matches
irep.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Internal Representation
4
5Author: 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?
24 return nil_rep_storage;
25}
26
27void 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
45const 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
58bool irept::get_bool(const irep_idt &name) const
59{
60 return get(name)==ID_1;
61}
62
63int irept::get_int(const irep_idt &name) const
64{
65 return unsafe_string2int(get_string(name));
66}
67
68std::size_t irept::get_size_t(const irep_idt &name) const
69{
70 return unsafe_string2size_t(get_string(name));
71}
72
73long long irept::get_long_long(const irep_idt &name) const
74{
76}
77
78void 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
87void 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
96void irept::remove(const irep_idt &name)
97{
98#if NAMED_SUB_IS_FORWARD_LIST
99 return get_named_sub().remove(name);
100#else
102 s.erase(name);
103#endif
104}
105
106const 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
117{
119 return s[name];
120}
121
122irept &irept::add(const irep_idt &name, irept irep)
123{
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
142unsigned long long irep_cmp_cnt=0;
143unsigned long long irep_cmp_ne_cnt=0;
144#endif
145
146bool 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
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
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
205bool 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
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
245bool 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
314int 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
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
408bool irept::operator<(const irept &other) const
409{
410 return ordering(other);
411}
412
413#ifdef IREP_HASH_STATS
414unsigned long long irep_hash_cnt=0;
415#endif
416
417std::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
428std::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());
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
462#endif
463 return result;
464}
465
466std::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
489static void indent_str(std::string &s, unsigned indent)
490{
491 for(unsigned i=0; i<indent; i++)
492 s+=' ';
493}
494
495std::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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
int compare(const dstringt &b) const
Definition dstring.h:133
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:417
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
bool operator==(const irept &other) const
Definition irep.cpp:146
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
void move_to_named_sub(const irep_idt &name, irept &irep)
Definition irep.cpp:27
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition irep.cpp:245
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void remove(const irep_idt &name)
Definition irep.cpp:96
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:87
std::size_t hash() const
Definition irep.cpp:428
int compare(const irept &i) const
defines ordering on the internal representation comments are ignored
Definition irep.cpp:314
void clear()
Definition irep.h:452
const std::string & id_string() const
Definition irep.h:399
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition irep.cpp:408
bool full_eq(const irept &other) const
Definition irep.cpp:205
long long get_long_long(const irep_idt &name) const
Definition irep.cpp:73
subt & get_sub()
Definition irep.h:456
std::size_t full_hash() const
Definition irep.cpp:466
signed int get_int(const irep_idt &name) const
Definition irep.cpp:63
static bool is_comment(const irep_idt &name)
Definition irep.h:468
void move_to_sub(irept &irep)
Definition irep.cpp:36
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:116
named_subt & get_named_sub()
Definition irep.h:458
const std::string & get_string(const irep_idt &name) const
Definition irep.h:409
dt * data
Definition irep.h:240
std::size_t hash_code
Definition irep.h:117
size_t hash_string(const dstringt &s)
Definition dstring.h:211
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
static void indent_str(std::string &s, unsigned indent)
Definition irep.cpp:489
const irept & get_nil_irep()
Definition irep.cpp:20
irept nil_rep_storage
Definition irep.cpp:18
const irept & get_nil_irep()
Definition irep.cpp:20
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
std::size_t unsafe_string2size_t(const std::string &str, int base)
int unsafe_string2int(const std::string &str, int base)
signed long long int unsafe_string2signedlonglong(const std::string &str, int base)
string hashing
Definition kdev_t.h:24
irep_pretty_diagnosticst(const irept &irep)
Definition irep.cpp:536