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 <cassert>
14 #include <string>
15 #include <vector>
16 
17 #include "irep_ids.h"
18 
19 #define SHARING
20 // #define HASH_CODE
21 #define USE_MOVE
22 // #define SUB_IS_LIST
23 
24 #ifdef SUB_IS_LIST
25 #include <list>
26 #else
27 #include <map>
28 #endif
29 
30 #ifdef USE_DSTRING
33 // NOLINTNEXTLINE(readability/identifiers)
35 #else
36 #include "string_hash.h"
37 typedef std::string irep_idt;
38 typedef std::string irep_namet;
39 // NOLINTNEXTLINE(readability/identifiers)
41 #endif
42 
43 inline const std::string &id2string(const irep_idt &d)
44 {
45  #ifdef USE_DSTRING
46  return as_string(d);
47  #else
48  return d;
49  #endif
50 }
51 
52 inline const std::string &name2string(const irep_namet &n)
53 {
54  #ifdef USE_DSTRING
55  return as_string(n);
56  #else
57  return n;
58  #endif
59 }
60 
61 #define forall_irep(it, irep) \
62  for(irept::subt::const_iterator it=(irep).begin(); \
63  it!=(irep).end(); ++it)
64 
65 #define Forall_irep(it, irep) \
66  for(irept::subt::iterator it=(irep).begin(); \
67  it!=(irep).end(); ++it)
68 
69 #define forall_named_irep(it, irep) \
70  for(irept::named_subt::const_iterator it=(irep).begin(); \
71  it!=(irep).end(); ++it)
72 
73 #define Forall_named_irep(it, irep) \
74  for(irept::named_subt::iterator it=(irep).begin(); \
75  it!=(irep).end(); ++it)
76 
77 #ifdef IREP_DEBUG
78 #include <iostream>
79 #endif
80 
81 class irept;
82 const irept &get_nil_irep();
83 
86 class irept
87 {
88 public:
89  // These are not stable.
90  typedef std::vector<irept> subt;
91 
92  // named_subt has to provide stable references; with C++11 we could
93  // use std::forward_list or std::vector< unique_ptr<T> > to save
94  // memory and increase efficiency.
95 
96  #ifdef SUB_IS_LIST
97  typedef std::list<std::pair<irep_namet, irept> > named_subt;
98  #else
99  typedef std::map<irep_namet, irept> named_subt;
100  #endif
101 
102  bool is_nil() const { return id()==ID_nil; }
103  bool is_not_nil() const { return id()!=ID_nil; }
104 
105  explicit irept(const irep_idt &_id)
106 #ifdef SHARING
107  :data(&empty_d)
108 #endif
109  {
110  id(_id);
111  }
112 
113  #ifdef SHARING
114  // constructor for blank irep
116  {
117  }
118 
119  // copy constructor
120  irept(const irept &irep):data(irep.data)
121  {
122  if(data!=&empty_d)
123  {
124  // NOLINTNEXTLINE(build/deprecated)
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 
276 
280 
281  #ifdef HASH_CODE
282  mutable std::size_t hash_code;
283  #endif
284 
285  void clear()
286  {
287  data.clear();
288  sub.clear();
289  named_sub.clear();
290  comments.clear();
291  #ifdef HASH_CODE
292  hash_code=0;
293  #endif
294  }
295 
296  void swap(dt &d)
297  {
298  d.data.swap(data);
299  d.sub.swap(sub);
300  d.named_sub.swap(named_sub);
301  d.comments.swap(comments);
302  #ifdef HASH_CODE
303  std::swap(d.hash_code, hash_code);
304  #endif
305  }
306 
307  #ifdef SHARING
309  #ifdef HASH_CODE
310  , hash_code(0)
311  #endif
312  {
313  }
314  #else
315  dt()
316  #ifdef HASH_CODE
317  :hash_code(0)
318  #endif
319  {
320  }
321  #endif
322  };
323 
324 protected:
325  #ifdef SHARING
327  static dt empty_d;
328 
329  static void remove_ref(dt *old_data);
330  static void nonrecursive_destructor(dt *old_data);
331  void detach();
332 
333 public:
334  const dt &read() const
335  {
336  return *data;
337  }
338 
340  {
341  detach();
342  #ifdef HASH_CODE
343  data->hash_code=0;
344  #endif
345  return *data;
346  }
347 
348  #else
349  dt data;
350 
351 public:
352  const dt &read() const
353  {
354  return data;
355  }
356 
357  dt &write()
358  {
359  #ifdef HASH_CODE
360  data.hash_code=0;
361  #endif
362  return data;
363  }
364  #endif
365 };
366 
367 // NOLINTNEXTLINE(readability/identifiers)
368 struct irep_hash
369 {
370  std::size_t operator()(const irept &irep) const
371  {
372  return irep.hash();
373  }
374 };
375 
376 // NOLINTNEXTLINE(readability/identifiers)
378 {
379  std::size_t operator()(const irept &irep) const
380  {
381  return irep.full_hash();
382  }
383 };
384 
385 // NOLINTNEXTLINE(readability/identifiers)
387 {
388  bool operator()(const irept &i1, const irept &i2) const
389  {
390  return i1.full_eq(i2);
391  }
392 };
393 
394 #endif // CPROVER_UTIL_IREP_H
irept(const irept &irep)
Definition: irep.h:120
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
subt sub
Definition: irep.h:279
int compare(const irept &i) const
defines ordering on the internal representation
Definition: irep.cpp:498
named_subt comments
Definition: irep.h:278
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< irept > subt
Definition: irep.h:90
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
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
named_subt named_sub
Definition: irep.h:277
subt & get_sub()
Definition: irep.h:245
const dt & read() const
Definition: irep.h:334
void swap(dt &d)
Definition: irep.h:296
bool operator!=(const irept &other) const
Definition: irep.h:226
const irep_idt & id() const
Definition: irep.h:189
dt * data
Definition: irep.h:326
const std::string & name2string(const irep_namet &n)
Definition: irep.h:52
unsigned ref_count
Definition: irep.h:270
std::size_t operator()(const irept &irep) const
Definition: irep.h:370
irept & operator=(const irept &irep)
Definition: irep.h:146
std::size_t operator()(const irept &irep) const
Definition: irep.h:379
dstring_hash irep_id_hash
Definition: irep.h:34
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:86
std::map< irep_namet, irept > named_subt
Definition: irep.h:99
irept()
Definition: irep.h:115
void detach()
Definition: irep.cpp:64
irept & operator=(irept &&irep)
Definition: irep.h:167
dt()
Definition: irep.h:308
const named_subt & get_comments() const
Definition: irep.h:250
static dt empty_d
Definition: irep.h:327
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
static bool is_comment(const irep_namet &name)
Definition: irep.h:260
irep_idt data
This irep_idt is the only place to store data in an irep, other than the mere nesting structure...
Definition: irep.h:275
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:388
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:285
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:32
dstringt irep_idt
Definition: irep.h:31
bool operator==(const irept &other) const
Definition: irep.cpp:355
irept(const irep_idt &_id)
Definition: irep.h:105
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:339