cprover
irep.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_IREP_H
11 #define CPROVER_UTIL_IREP_H
12 
13 #include <vector>
14 #include <string>
15 #include <cassert>
16 #include <iosfwd>
17 
18 #include "irep_ids.h"
19 
20 #define SHARING
21 // #define HASH_CODE
22 #define USE_MOVE
23 // #define SUB_IS_LIST
24 
25 #ifdef SUB_IS_LIST
26 #include <list>
27 #else
28 #include <map>
29 #endif
30 
31 #ifdef USE_DSTRING
34 // NOLINTNEXTLINE(readability/identifiers)
36 #else
37 #include "string_hash.h"
38 typedef std::string irep_idt;
39 typedef std::string irep_namet;
40 // NOLINTNEXTLINE(readability/identifiers)
42 #endif
43 
44 inline const std::string &id2string(const irep_idt &d)
45 {
46  #ifdef USE_DSTRING
47  return as_string(d);
48  #else
49  return d;
50  #endif
51 }
52 
53 inline const std::string &name2string(const irep_namet &n)
54 {
55  #ifdef USE_DSTRING
56  return as_string(n);
57  #else
58  return n;
59  #endif
60 }
61 
62 #define forall_irep(it, irep) \
63  for(irept::subt::const_iterator it=(irep).begin(); \
64  it!=(irep).end(); ++it)
65 
66 #define Forall_irep(it, irep) \
67  for(irept::subt::iterator it=(irep).begin(); \
68  it!=(irep).end(); ++it)
69 
70 #define forall_named_irep(it, irep) \
71  for(irept::named_subt::const_iterator it=(irep).begin(); \
72  it!=(irep).end(); ++it)
73 
74 #define Forall_named_irep(it, irep) \
75  for(irept::named_subt::iterator it=(irep).begin(); \
76  it!=(irep).end(); ++it)
77 
78 #ifdef IREP_DEBUG
79 #include <iostream>
80 #endif
81 
82 class irept;
83 const irept &get_nil_irep();
84 
87 class irept
88 {
89 public:
90  // These are not stable.
91  typedef std::vector<irept> subt;
92 
93  // named_subt has to provide stable references; with C++11 we could
94  // use std::forward_list or std::vector< unique_ptr<T> > to save
95  // memory and increase efficiency.
96 
97  #ifdef SUB_IS_LIST
98  typedef std::list<std::pair<irep_namet, irept> > named_subt;
99  #else
100  typedef std::map<irep_namet, irept> named_subt;
101  #endif
102 
103  bool is_nil() const { return id()==ID_nil; }
104  bool is_not_nil() const { return id()!=ID_nil; }
105 
106  explicit irept(const irep_idt &_id)
107 #ifdef SHARING
108  :data(&empty_d)
109 #endif
110  {
111  id(_id);
112  }
113 
114  #ifdef SHARING
115  // constructor for blank irep
117  {
118  }
119 
120  // copy constructor
121  irept(const irept &irep):data(irep.data)
122  {
123  if(data!=&empty_d)
124  {
125  assert(data->ref_count!=0);
126  data->ref_count++;
127  #ifdef IREP_DEBUG
128  std::cout << "COPY " << data << " " << data->ref_count << '\n';
129  #endif
130  }
131  }
132 
133  #ifdef USE_MOVE
134  // Copy from rvalue reference.
135  // Note that this does avoid a branch compared to the
136  // standard copy constructor above.
137  irept(irept &&irep):data(irep.data)
138  {
139  #ifdef IREP_DEBUG
140  std::cout << "COPY MOVE\n";
141  #endif
142  irep.data=&empty_d;
143  }
144  #endif
145 
146  irept &operator=(const irept &irep)
147  {
148  #ifdef IREP_DEBUG
149  std::cout << "ASSIGN\n";
150  #endif
151 
152  // Ordering is very important here!
153  // Consider self-assignment, which may destroy 'irep'
154  dt *irep_data=irep.data;
155  if(irep_data!=&empty_d)
156  irep_data->ref_count++;
157 
158  remove_ref(data); // this may kill 'irep'
159  data=irep_data;
160 
161  return *this;
162  }
163 
164  #ifdef USE_MOVE
165  // Note that the move assignment operator does avoid
166  // three branches compared to standard operator above.
168  {
169  #ifdef IREP_DEBUG
170  std::cout << "ASSIGN MOVE\n";
171  #endif
172  // we simply swap two pointers
173  std::swap(data, irep.data);
174  return *this;
175  }
176  #endif
177 
179  {
180  remove_ref(data);
181  }
182 
183  #else
184  irept()
185  {
186  }
187  #endif
188 
189  const irep_idt &id() const
190  { return read().data; }
191 
192  const std::string &id_string() const
193  { return id2string(read().data); }
194 
195  void id(const irep_idt &_data)
196  { write().data=_data; }
197 
198  const irept &find(const irep_namet &name) const;
199  irept &add(const irep_namet &name);
200  irept &add(const irep_namet &name, const irept &irep);
201 
202  const std::string &get_string(const irep_namet &name) const
203  {
204  return id2string(get(name));
205  }
206 
207  const irep_idt &get(const irep_namet &name) const;
208  bool get_bool(const irep_namet &name) const;
209  signed int get_int(const irep_namet &name) const;
210  unsigned int get_unsigned_int(const irep_namet &name) const;
211  std::size_t get_size_t(const irep_namet &name) const;
212  long long get_long_long(const irep_namet &name) const;
213 
214  void set(const irep_namet &name, const irep_idt &value)
215  { add(name).id(value); }
216  void set(const irep_namet &name, const irept &irep)
217  { add(name, irep); }
218  void set(const irep_namet &name, const long long value);
219 
220  void remove(const irep_namet &name);
221  void move_to_sub(irept &irep);
222  void move_to_named_sub(const irep_namet &name, irept &irep);
223 
224  bool operator==(const irept &other) const;
225 
226  bool operator!=(const irept &other) const
227  {
228  return !(*this==other);
229  }
230 
231  void swap(irept &irep)
232  {
233  std::swap(irep.data, data);
234  }
235 
236  bool operator<(const irept &other) const;
237  bool ordering(const irept &other) const;
238 
239  int compare(const irept &i) const;
240 
241  void clear() { *this=irept(); }
242 
243  void make_nil() { *this=get_nil_irep(); }
244 
245  subt &get_sub() { return write().sub; } // DANGEROUS
246  const subt &get_sub() const { return read().sub; }
247  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
248  const named_subt &get_named_sub() const { return read().named_sub; }
249  named_subt &get_comments() { return write().comments; } // DANGEROUS
250  const named_subt &get_comments() const { return read().comments; }
251 
252  std::size_t hash() const;
253  std::size_t full_hash() const;
254 
255  bool full_eq(const irept &other) const;
256 
257  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
258 
259 protected:
260  static bool is_comment(const irep_namet &name)
261  { return !name.empty() && name[0]=='#'; }
262 
263 public:
264  class dt
265  {
266  private:
267  friend class irept;
268 
269  #ifdef SHARING
270  unsigned ref_count;
271  #endif
272 
274 
275  named_subt named_sub;
276  named_subt comments;
277  subt sub;
278 
279  #ifdef HASH_CODE
280  mutable std::size_t hash_code;
281  #endif
282 
283  void clear()
284  {
285  data.clear();
286  sub.clear();
287  named_sub.clear();
288  comments.clear();
289  #ifdef HASH_CODE
290  hash_code=0;
291  #endif
292  }
293 
294  void swap(dt &d)
295  {
296  d.data.swap(data);
297  d.sub.swap(sub);
298  d.named_sub.swap(named_sub);
299  d.comments.swap(comments);
300  #ifdef HASH_CODE
301  std::swap(d.hash_code, hash_code);
302  #endif
303  }
304 
305  #ifdef SHARING
306  dt():ref_count(1)
307  #ifdef HASH_CODE
308  , hash_code(0)
309  #endif
310  {
311  }
312  #else
313  dt()
314  #ifdef HASH_CODE
315  :hash_code(0)
316  #endif
317  {
318  }
319  #endif
320  };
321 
322 protected:
323  #ifdef SHARING
325  static dt empty_d;
326 
327  static void remove_ref(dt *old_data);
328  static void nonrecursive_destructor(dt *old_data);
329  void detach();
330 
331 public:
332  const dt &read() const
333  {
334  return *data;
335  }
336 
338  {
339  detach();
340  #ifdef HASH_CODE
341  data->hash_code=0;
342  #endif
343  return *data;
344  }
345 
346  #else
347  dt data;
348 
349 public:
350  const dt &read() const
351  {
352  return data;
353  }
354 
355  dt &write()
356  {
357  #ifdef HASH_CODE
358  data.hash_code=0;
359  #endif
360  return data;
361  }
362  #endif
363 };
364 
365 // NOLINTNEXTLINE(readability/identifiers)
366 struct irep_hash
367 {
368  std::size_t operator()(const irept &irep) const
369  {
370  return irep.hash();
371  }
372 };
373 
374 // NOLINTNEXTLINE(readability/identifiers)
376 {
377  std::size_t operator()(const irept &irep) const
378  {
379  return irep.full_hash();
380  }
381 };
382 
383 // NOLINTNEXTLINE(readability/identifiers)
385 {
386  bool operator()(const irept &i1, const irept &i2) const
387  {
388  return i1.full_eq(i2);
389  }
390 };
391 
392 #endif // CPROVER_UTIL_IREP_H
irept(const irept &irep)
Definition: irep.h:121
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
subt sub
Definition: irep.h:277
int compare(const irept &i) const
defines ordering on the internal representation
Definition: irep.cpp:498
named_subt comments
Definition: irep.h:276
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< irept > subt
Definition: irep.h:91
void move_to_sub(irept &irep)
Definition: irep.cpp:204
std::size_t hash() const
Definition: irep.cpp:575
bool full_eq(const irept &other) const
Definition: irep.cpp:380
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
void id(const irep_idt &_data)
Definition: irep.h:195
irept(irept &&irep)
Definition: irep.h:137
const irept & get_nil_irep()
Definition: irep.cpp:56
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
named_subt named_sub
Definition: irep.h:275
subt & get_sub()
Definition: irep.h:245
const dt & read() const
Definition: irep.h:332
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
void swap(dt &d)
Definition: irep.h:294
bool operator!=(const irept &other) const
Definition: irep.h:226
const irep_idt & id() const
Definition: irep.h:189
dt * data
Definition: irep.h:324
const std::string & name2string(const irep_namet &n)
Definition: irep.h:53
unsigned ref_count
Definition: irep.h:270
std::size_t operator()(const irept &irep) const
Definition: irep.h:368
irept & operator=(const irept &irep)
Definition: irep.h:146
std::size_t operator()(const irept &irep) const
Definition: irep.h:377
dstring_hash irep_id_hash
Definition: irep.h:35
static void nonrecursive_destructor(dt *old_data)
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition: irep.cpp:140
named_subt & get_comments()
Definition: irep.h:249
Base class for tree-like data structures with sharing.
Definition: irep.h:87
std::map< irep_namet, irept > named_subt
Definition: irep.h:100
irept()
Definition: irep.h:116
void detach()
Definition: irep.cpp:64
irept & operator=(irept &&irep)
Definition: irep.h:167
dt()
Definition: irep.h:306
const named_subt & get_comments() const
Definition: irep.h:250
static dt empty_d
Definition: irep.h:325
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:566
static void remove_ref(dt *old_data)
Definition: irep.cpp:100
named_subt & get_named_sub()
Definition: irep.h:247
const named_subt & get_named_sub() const
Definition: irep.h:248
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:430
void swap(dstringt &b)
Definition: dstring.h:118
~irept()
Definition: irep.h:178
void clear()
Definition: dstring.h:115
static bool is_comment(const irep_namet &name)
Definition: irep.h:260
irep_idt data
Definition: irep.h:273
std::size_t full_hash() const
Definition: irep.cpp:606
void clear()
Definition: irep.h:241
bool operator()(const irept &i1, const irept &i2) const
Definition: irep.h:386
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void make_nil()
Definition: irep.h:243
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
void clear()
Definition: irep.h:283
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:260
dstringt irep_namet
Definition: irep.h:33
dstringt irep_idt
Definition: irep.h:32
bool operator==(const irept &other) const
Definition: irep.cpp:355
irept(const irep_idt &_id)
Definition: irep.h:106
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const subt & get_sub() const
Definition: irep.h:246
Definition: kdev_t.h:24
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:195
dt & write()
Definition: irep.h:337