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