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