cprover
Loading...
Searching...
No Matches
irep.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_IREP_H
11#define CPROVER_UTIL_IREP_H
12
13#include <string>
14#include <vector>
15
16#include "invariant.h"
17#include "irep_ids.h"
18
19#define SHARING
20#ifndef HASH_CODE
21# define HASH_CODE 1
22#endif
23// use forward_list by default, unless _GLIBCXX_DEBUG is set as the debug
24// overhead is noticeably higher with the regression test suite taking four
25// times as long.
26#if !defined(NAMED_SUB_IS_FORWARD_LIST) && !defined(_GLIBCXX_DEBUG)
27# define NAMED_SUB_IS_FORWARD_LIST 1
28#endif
29
30#if NAMED_SUB_IS_FORWARD_LIST
31# include "forward_list_as_map.h"
32#else
33#include <map>
34#endif
35
36#ifdef USE_DSTRING
38// NOLINTNEXTLINE(readability/identifiers)
40#else
41#include "string_hash.h"
42typedef std::string irep_idt;
43// NOLINTNEXTLINE(readability/identifiers)
45#endif
46
47inline const std::string &id2string(const irep_idt &d)
48{
49 #ifdef USE_DSTRING
50 return as_string(d);
51 #else
52 return d;
53 #endif
54}
55
56#ifdef IREP_DEBUG
57#include <iostream>
58#endif
59
60class irept;
61const irept &get_nil_irep();
62
66template <bool enabled>
68{
69};
70
71template <>
72struct ref_count_ift<true>
73{
74 unsigned ref_count = 1;
75};
76
96template <typename treet, typename named_subtreest, bool sharing = true>
97class tree_nodet : public ref_count_ift<sharing>
98{
99public:
100 // These are not stable.
101 typedef std::vector<treet> subt;
102
103 // named_subt has to provide stable references; we can
104 // use std::forward_list or std::vector< unique_ptr<T> > to save
105 // memory and increase efficiency.
107
108 friend treet;
109
112
115
116#if HASH_CODE
117 mutable std::size_t hash_code = 0;
118#endif
119
120 void clear()
121 {
122 data.clear();
123 sub.clear();
125#if HASH_CODE
126 hash_code = 0;
127#endif
128 }
129
131 {
132 d.data.swap(data);
133 d.sub.swap(sub);
134 d.named_sub.swap(named_sub);
135#if HASH_CODE
136 std::swap(d.hash_code, hash_code);
137#endif
138 }
139
140 tree_nodet() = default;
141
142 explicit tree_nodet(irep_idt _data) : data(std::move(_data))
143 {
144 }
145
147 : data(std::move(_data)),
148 named_sub(std::move(_named_sub)),
149 sub(std::move(_sub))
150 {
151 }
152};
153
155template <typename derivedt, typename named_subtreest>
157{
158public:
160 using subt = typename dt::subt;
161 using named_subt = typename dt::named_subt;
162
165
166 explicit sharing_treet(irep_idt _id) : data(new dt(std::move(_id)))
167 {
168 }
169
171 : data(new dt(std::move(_id), std::move(_named_sub), std::move(_sub)))
172 {
173 }
174
175 // constructor for blank irep
177 {
178 }
179
180 // copy constructor
182 {
183 if(data!=&empty_d)
184 {
185 PRECONDITION(data->ref_count != 0);
186 data->ref_count++;
187#ifdef IREP_DEBUG
188 std::cout << "COPY " << data << " " << data->ref_count << '\n';
189#endif
190 }
191 }
192
193 // Copy from rvalue reference.
194 // Note that this does avoid a branch compared to the
195 // standard copy constructor above.
197 {
198#ifdef IREP_DEBUG
199 std::cout << "COPY MOVE\n";
200#endif
201 irep.data=&empty_d;
202 }
203
205 {
206#ifdef IREP_DEBUG
207 std::cout << "ASSIGN\n";
208#endif
209
210 // Ordering is very important here!
211 // Consider self-assignment, which may destroy 'irep'
212 dt *irep_data=irep.data;
213 if(irep_data!=&empty_d)
214 irep_data->ref_count++;
215
216 remove_ref(data); // this may kill 'irep'
218
219 return *this;
220 }
221
222 // Note that the move assignment operator does avoid
223 // three branches compared to standard operator above.
225 {
226#ifdef IREP_DEBUG
227 std::cout << "ASSIGN MOVE\n";
228#endif
229 // we simply swap two pointers
230 std::swap(data, irep.data);
231 return *this;
232 }
233
235 {
237 }
238
239protected:
241 static dt empty_d;
242
243 static void remove_ref(dt *old_data);
245 void detach();
246
247public:
248 const dt &read() const
249 {
250 return *data;
251 }
252
254 {
255 detach();
256#if HASH_CODE
257 data->hash_code = 0;
258#endif
259 return *data;
260 }
261};
262
263// Static field initialization
264template <typename derivedt, typename named_subtreest>
267
269template <typename derivedt, typename named_subtreest>
271{
272public:
274 using subt = typename dt::subt;
275 using named_subt = typename dt::named_subt;
276
279
281 {
282 }
283
285 : data(std::move(_id), std::move(_named_sub), std::move(_sub))
286 {
287 }
288
289 non_sharing_treet() = default;
290
291 const dt &read() const
292 {
293 return data;
294 }
295
297 {
298#if HASH_CODE
299 data.hash_code = 0;
300#endif
301 return data;
302 }
303
304protected:
306};
307
359class irept
361 : public sharing_treet<
362 irept,
363#else
364 : public non_sharing_treet<
365 irept,
366#endif
367#if NAMED_SUB_IS_FORWARD_LIST
368 forward_list_as_mapt<irep_idt, irept>>
369#else
370 std::map<irep_idt, irept>>
371#endif
372{
373public:
375
376 bool is_nil() const
377 {
378 return id() == ID_nil;
379 }
380 bool is_not_nil() const
381 {
382 return id() != ID_nil;
383 }
384
385 explicit irept(const irep_idt &_id) : baset(_id)
386 {
387 }
388
391 {
392 }
393
394 irept() = default;
395
396 const irep_idt &id() const
397 { return read().data; }
398
399 const std::string &id_string() const
400 { return id2string(read().data); }
401
402 void id(const irep_idt &_data)
403 { write().data=_data; }
404
405 const irept &find(const irep_idt &name) const;
406 irept &add(const irep_idt &name);
407 irept &add(const irep_idt &name, irept irep);
408
409 const std::string &get_string(const irep_idt &name) const
410 {
411 return id2string(get(name));
412 }
413
414 const irep_idt &get(const irep_idt &name) const;
415 bool get_bool(const irep_idt &name) const;
416 signed int get_int(const irep_idt &name) const;
417 std::size_t get_size_t(const irep_idt &name) const;
418 long long get_long_long(const irep_idt &name) const;
419
420 void set(const irep_idt &name, const irep_idt &value)
421 {
422 add(name, irept(value));
423 }
424 void set(const irep_idt &name, irept irep)
425 {
426 add(name, std::move(irep));
427 }
428 void set(const irep_idt &name, const long long value);
429 void set_size_t(const irep_idt &name, const std::size_t value);
430
431 void remove(const irep_idt &name);
432 void move_to_sub(irept &irep);
433 void move_to_named_sub(const irep_idt &name, irept &irep);
434
435 bool operator==(const irept &other) const;
436
437 bool operator!=(const irept &other) const
438 {
439 return !(*this==other);
440 }
441
442 void swap(irept &irep)
443 {
444 std::swap(irep.data, data);
445 }
446
447 bool operator<(const irept &other) const;
448 bool ordering(const irept &other) const;
449
450 int compare(const irept &i) const;
451
452 void clear() { *this=irept(); }
453
454 void make_nil() { *this=get_nil_irep(); }
455
456 subt &get_sub() { return write().sub; } // DANGEROUS
457 const subt &get_sub() const { return read().sub; }
458 named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
459 const named_subt &get_named_sub() const { return read().named_sub; }
460
461 std::size_t hash() const;
462 std::size_t full_hash() const;
463
464 bool full_eq(const irept &other) const;
465
466 std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
467
468 static bool is_comment(const irep_idt &name)
469 { return !name.empty() && name[0]=='#'; }
470
472 static std::size_t number_of_non_comments(const named_subt &);
473};
474
475// NOLINTNEXTLINE(readability/identifiers)
477{
478 std::size_t operator()(const irept &irep) const
479 {
480 return irep.hash();
481 }
482};
483
484// NOLINTNEXTLINE(readability/identifiers)
486{
487 std::size_t operator()(const irept &irep) const
488 {
489 return irep.full_hash();
490 }
491};
492
493// NOLINTNEXTLINE(readability/identifiers)
495{
496 bool operator()(const irept &i1, const irept &i2) const
497 {
498 return i1.full_eq(i2);
499 }
500};
501
503{
504 const irept &irep;
505 explicit irep_pretty_diagnosticst(const irept &irep);
506};
507
508template <>
510{
511 static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
512 {
513 return irep.irep.pretty();
514 }
515};
516
517template <typename derivedt, typename named_subtreest>
519{
520#ifdef IREP_DEBUG
521 std::cout << "DETACH1: " << data << '\n';
522#endif
523
524 if(data == &empty_d)
525 {
526 data = new dt;
527
528#ifdef IREP_DEBUG
529 std::cout << "ALLOCATED " << data << '\n';
530#endif
531 }
532 else if(data->ref_count > 1)
533 {
534 dt *old_data(data);
535 data = new dt(*old_data);
536
537#ifdef IREP_DEBUG
538 std::cout << "ALLOCATED " << data << '\n';
539#endif
540
541 data->ref_count = 1;
542 remove_ref(old_data);
543 }
544
545 POSTCONDITION(data->ref_count == 1);
546
547#ifdef IREP_DEBUG
548 std::cout << "DETACH2: " << data << '\n';
549#endif
550}
551
552template <typename derivedt, typename named_subtreest>
554{
555 if(old_data == &empty_d)
556 return;
557
558#if 0
559 nonrecursive_destructor(old_data);
560#else
561
562 PRECONDITION(old_data->ref_count != 0);
563
564#ifdef IREP_DEBUG
565 std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
566#endif
567
568 old_data->ref_count--;
569 if(old_data->ref_count == 0)
570 {
571#ifdef IREP_DEBUG
572 std::cout << "D: " << pretty() << '\n';
573 std::cout << "DELETING " << old_data->data << " " << old_data << '\n';
574 old_data->clear();
575 std::cout << "DEALLOCATING " << old_data << "\n";
576#endif
577
578 // may cause recursive call
579 delete old_data;
580
581#ifdef IREP_DEBUG
582 std::cout << "DONE\n";
583#endif
584 }
585#endif
586}
587
590template <typename derivedt, typename named_subtreest>
592 dt *old_data)
593{
594 std::vector<dt *> stack(1, old_data);
595
596 while(!stack.empty())
597 {
598 dt *d = stack.back();
599 stack.erase(--stack.end());
600 if(d == &empty_d)
601 continue;
602
603 INVARIANT(d->ref_count != 0, "All contents of the stack must be in use");
604 d->ref_count--;
605
606 if(d->ref_count == 0)
607 {
608 stack.reserve(
609 stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
610 d->sub.size());
611
612 for(typename named_subt::iterator it = d->named_sub.begin();
613 it != d->named_sub.end();
614 it++)
615 {
616 stack.push_back(it->second.data);
617 it->second.data = &empty_d;
618 }
619
620 for(typename subt::iterator it = d->sub.begin(); it != d->sub.end(); it++)
621 {
622 stack.push_back(it->data);
623 it->data = &empty_d;
624 }
625
626 // now delete, won't do recursion
627 delete d;
628 }
629 }
630}
631
632#endif // CPROVER_UTIL_IREP_H
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ait()
Definition ai.h:566
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
void swap(dstringt &b)
Definition dstring.h:163
bool empty() const
Definition dstring.h:90
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
irept()=default
bool operator==(const irept &other) const
Definition irep.cpp:141
void set(const irep_idt &name, irept irep)
Definition irep.h:424
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
bool operator!=(const irept &other) const
Definition irep.h:437
const subt & get_sub() const
Definition irep.h:457
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
irept(const irep_idt &_id)
Definition irep.h:385
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
irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
Definition irep.h:389
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
bool is_not_nil() const
Definition irep.h:380
const named_subt & get_named_sub() const
Definition irep.h:459
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
void make_nil()
Definition irep.h:454
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
void id(const irep_idt &_data)
Definition irep.h:402
irept & add(const irep_idt &name)
Definition irep.cpp:111
bool is_nil() const
Definition irep.h:376
named_subt & get_named_sub()
Definition irep.h:458
const std::string & get_string(const irep_idt &name) const
Definition irep.h:409
Base class for tree-like data structures without sharing.
Definition irep.h:271
non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
Definition irep.h:284
const dt & read() const
Definition irep.h:291
non_sharing_treet()=default
typename dt::subt subt
Definition irep.h:274
non_sharing_treet(irep_idt _id)
Definition irep.h:280
typename dt::named_subt named_subt
Definition irep.h:275
dt & write()
Definition irep.h:296
Base class for tree-like data structures with sharing.
Definition irep.h:157
sharing_treet & operator=(sharing_treet &&irep)
Definition irep.h:224
sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
Definition irep.h:170
dt * data
Definition irep.h:240
sharing_treet(irep_idt _id)
Definition irep.h:166
static void remove_ref(dt *old_data)
Definition irep.h:553
typename dt::named_subt named_subt
Definition irep.h:161
typename dt::subt subt
Definition irep.h:160
sharing_treet tree_implementationt
Used to refer to this class from derived classes.
Definition irep.h:164
sharing_treet(const sharing_treet &irep)
Definition irep.h:181
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition irep.h:591
static dt empty_d
Definition irep.h:241
sharing_treet()
Definition irep.h:176
sharing_treet(sharing_treet &&irep)
Definition irep.h:196
const dt & read() const
Definition irep.h:248
dt & write()
Definition irep.h:253
sharing_treet & operator=(const sharing_treet &irep)
Definition irep.h:204
~sharing_treet()
Definition irep.h:234
void detach()
Definition irep.h:518
A node with data in a tree, it contains:
Definition irep.h:98
named_subt named_sub
Definition irep.h:113
named_subtreest named_subt
Definition irep.h:106
friend treet
Definition irep.h:108
tree_nodet()=default
void swap(tree_nodet &d)
Definition irep.h:130
tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
Definition irep.h:146
std::vector< treet > subt
Definition irep.h:101
void clear()
Definition irep.h:120
tree_nodet(irep_idt _data)
Definition irep.h:142
std::size_t hash_code
Definition irep.h:117
subt sub
Definition irep.h:114
irep_idt data
This irep_idt is the only place to store data in an tree node.
Definition irep.h:111
dstring_hash irep_id_hash
Definition irep.h:39
dstringt irep_idt
Definition irep.h:37
const irept & get_nil_irep()
Definition irep.cpp:19
#define SHARING
Definition irep.h:19
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
string hashing
Definition kdev_t.h:24
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
Definition irep.h:511
Helper to give us some diagnostic in a usable form on assertion failure.
Definition invariant.h:299
bool operator()(const irept &i1, const irept &i2) const
Definition irep.h:496
std::size_t operator()(const irept &irep) const
Definition irep.h:487
std::size_t operator()(const irept &irep) const
Definition irep.h:478
const irept & irep
Definition irep.h:504
Used in tree_nodet for activating or not reference counting.
Definition irep.h:68