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 <string>
14 #include <vector>
15 
16 #include "deprecate.h"
17 #include "invariant.h"
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 
156 class irept
157 {
158 public:
159  // These are not stable.
160  typedef std::vector<irept> subt;
161 
162  // named_subt has to provide stable references; with C++11 we could
163  // use std::forward_list or std::vector< unique_ptr<T> > to save
164  // memory and increase efficiency.
165 
166  #ifdef SUB_IS_LIST
167  typedef std::list<std::pair<irep_namet, irept> > named_subt;
168  #else
169  typedef std::map<irep_namet, irept> named_subt;
170  #endif
171 
172  bool is_nil() const { return id()==ID_nil; }
173  bool is_not_nil() const { return id()!=ID_nil; }
174 
175  explicit irept(const irep_idt &_id)
176 #ifdef SHARING
177  :data(&empty_d)
178 #endif
179  {
180  id(_id);
181  }
182 
183  #ifdef SHARING
184  // constructor for blank irep
186  {
187  }
188 
189  // copy constructor
190  irept(const irept &irep):data(irep.data)
191  {
192  if(data!=&empty_d)
193  {
194  // NOLINTNEXTLINE(build/deprecated)
195  PRECONDITION(data->ref_count != 0);
196  data->ref_count++;
197  #ifdef IREP_DEBUG
198  std::cout << "COPY " << data << " " << data->ref_count << '\n';
199  #endif
200  }
201  }
202 
203  #ifdef USE_MOVE
204  // Copy from rvalue reference.
205  // Note that this does avoid a branch compared to the
206  // standard copy constructor above.
207  irept(irept &&irep):data(irep.data)
208  {
209  #ifdef IREP_DEBUG
210  std::cout << "COPY MOVE\n";
211  #endif
212  irep.data=&empty_d;
213  }
214  #endif
215 
216  irept &operator=(const irept &irep)
217  {
218  #ifdef IREP_DEBUG
219  std::cout << "ASSIGN\n";
220  #endif
221 
222  // Ordering is very important here!
223  // Consider self-assignment, which may destroy 'irep'
224  dt *irep_data=irep.data;
225  if(irep_data!=&empty_d)
226  irep_data->ref_count++;
227 
228  remove_ref(data); // this may kill 'irep'
229  data=irep_data;
230 
231  return *this;
232  }
233 
234  #ifdef USE_MOVE
235  // Note that the move assignment operator does avoid
236  // three branches compared to standard operator above.
238  {
239  #ifdef IREP_DEBUG
240  std::cout << "ASSIGN MOVE\n";
241  #endif
242  // we simply swap two pointers
243  std::swap(data, irep.data);
244  return *this;
245  }
246  #endif
247 
249  {
250  remove_ref(data);
251  }
252 
253  #else
254  irept()
255  {
256  }
257  #endif
258 
259  const irep_idt &id() const
260  { return read().data; }
261 
262  const std::string &id_string() const
263  { return id2string(read().data); }
264 
265  void id(const irep_idt &_data)
266  { write().data=_data; }
267 
268  const irept &find(const irep_namet &name) const;
269  irept &add(const irep_namet &name);
270  irept &add(const irep_namet &name, const irept &irep);
271 
272  const std::string &get_string(const irep_namet &name) const
273  {
274  return id2string(get(name));
275  }
276 
277  const irep_idt &get(const irep_namet &name) const;
278  bool get_bool(const irep_namet &name) const;
279  signed int get_int(const irep_namet &name) const;
281  DEPRECATED("Use get_size_t instead")
282  unsigned int get_unsigned_int(const irep_namet &name) const;
283  std::size_t get_size_t(const irep_namet &name) const;
284  long long get_long_long(const irep_namet &name) const;
285 
286  void set(const irep_namet &name, const irep_idt &value)
287  { add(name).id(value); }
288  void set(const irep_namet &name, const irept &irep)
289  { add(name, irep); }
290  void set(const irep_namet &name, const long long value);
291 
292  void remove(const irep_namet &name);
293  void move_to_sub(irept &irep);
294  void move_to_named_sub(const irep_namet &name, irept &irep);
295 
296  bool operator==(const irept &other) const;
297 
298  bool operator!=(const irept &other) const
299  {
300  return !(*this==other);
301  }
302 
303  void swap(irept &irep)
304  {
305  std::swap(irep.data, data);
306  }
307 
308  bool operator<(const irept &other) const;
309  bool ordering(const irept &other) const;
310 
311  int compare(const irept &i) const;
312 
313  void clear() { *this=irept(); }
314 
315  void make_nil() { *this=get_nil_irep(); }
316 
317  subt &get_sub() { return write().sub; } // DANGEROUS
318  const subt &get_sub() const { return read().sub; }
319  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
320  const named_subt &get_named_sub() const { return read().named_sub; }
321  named_subt &get_comments() { return write().comments; } // DANGEROUS
322  const named_subt &get_comments() const { return read().comments; }
323 
324  std::size_t hash() const;
325  std::size_t full_hash() const;
326 
327  bool full_eq(const irept &other) const;
328 
329  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
330 
331 protected:
332  static bool is_comment(const irep_namet &name)
333  { return !name.empty() && name[0]=='#'; }
334 
335 public:
336  class dt
337  {
338  private:
339  friend class irept;
340 
341  #ifdef SHARING
342  unsigned ref_count;
343  #endif
344 
348 
352 
353  #ifdef HASH_CODE
354  mutable std::size_t hash_code;
355  #endif
356 
357  void clear()
358  {
359  data.clear();
360  sub.clear();
361  named_sub.clear();
362  comments.clear();
363  #ifdef HASH_CODE
364  hash_code=0;
365  #endif
366  }
367 
368  void swap(dt &d)
369  {
370  d.data.swap(data);
371  d.sub.swap(sub);
372  d.named_sub.swap(named_sub);
373  d.comments.swap(comments);
374  #ifdef HASH_CODE
375  std::swap(d.hash_code, hash_code);
376  #endif
377  }
378 
379  #ifdef SHARING
381  #ifdef HASH_CODE
382  , hash_code(0)
383  #endif
384  {
385  }
386  #else
387  dt()
388  #ifdef HASH_CODE
389  :hash_code(0)
390  #endif
391  {
392  }
393  #endif
394  };
395 
396 protected:
397  #ifdef SHARING
399  static dt empty_d;
400 
401  static void remove_ref(dt *old_data);
402  static void nonrecursive_destructor(dt *old_data);
403  void detach();
404 
405 public:
406  const dt &read() const
407  {
408  return *data;
409  }
410 
412  {
413  detach();
414  #ifdef HASH_CODE
415  data->hash_code=0;
416  #endif
417  return *data;
418  }
419 
420  #else
421  dt data;
422 
423 public:
424  const dt &read() const
425  {
426  return data;
427  }
428 
429  dt &write()
430  {
431  #ifdef HASH_CODE
432  data.hash_code=0;
433  #endif
434  return data;
435  }
436  #endif
437 };
438 
439 // NOLINTNEXTLINE(readability/identifiers)
440 struct irep_hash
441 {
442  std::size_t operator()(const irept &irep) const
443  {
444  return irep.hash();
445  }
446 };
447 
448 // NOLINTNEXTLINE(readability/identifiers)
450 {
451  std::size_t operator()(const irept &irep) const
452  {
453  return irep.full_hash();
454  }
455 };
456 
457 // NOLINTNEXTLINE(readability/identifiers)
459 {
460  bool operator()(const irept &i1, const irept &i2) const
461  {
462  return i1.full_eq(i2);
463  }
464 };
465 
467 {
468  const irept &irep;
469  explicit irep_pretty_diagnosticst(const irept &irep);
470 };
471 
472 template <>
474 {
475  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
476  {
477  return irep.irep.pretty();
478  }
479 };
480 
481 #endif // CPROVER_UTIL_IREP_H
irept(const irept &irep)
Definition: irep.h:190
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
subt sub
Definition: irep.h:351
int compare(const irept &i) const
defines ordering on the internal representation
Definition: irep.cpp:497
named_subt comments
Definition: irep.h:350
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
std::vector< irept > subt
Definition: irep.h:160
void move_to_sub(irept &irep)
Definition: irep.cpp:203
std::size_t hash() const
Definition: irep.cpp:574
bool full_eq(const irept &other) const
Definition: irep.cpp:379
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:244
void id(const irep_idt &_data)
Definition: irep.h:265
irept(irept &&irep)
Definition: irep.h:207
const irept & get_nil_irep()
Definition: irep.cpp:55
STL namespace.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
named_subt named_sub
Definition: irep.h:349
const irept & irep
Definition: irep.h:468
subt & get_sub()
Definition: irep.h:317
const dt & read() const
Definition: irep.h:406
void swap(dt &d)
Definition: irep.h:368
irep_pretty_diagnosticst(const irept &irep)
Definition: irep.cpp:693
bool operator!=(const irept &other) const
Definition: irep.h:298
const irep_idt & id() const
Definition: irep.h:259
dt * data
Definition: irep.h:398
const std::string & name2string(const irep_namet &n)
Definition: irep.h:53
unsigned ref_count
Definition: irep.h:342
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:266
std::size_t operator()(const irept &irep) const
Definition: irep.h:442
irept & operator=(const irept &irep)
Definition: irep.h:216
std::size_t operator()(const irept &irep) const
Definition: irep.h:451
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:139
#define PRECONDITION(CONDITION)
Definition: invariant.h:427
named_subt & get_comments()
Definition: irep.h:321
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::map< irep_namet, irept > named_subt
Definition: irep.h:169
irept()
Definition: irep.h:185
void detach()
Definition: irep.cpp:63
irept & operator=(irept &&irep)
Definition: irep.h:237
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
dt()
Definition: irep.h:380
const named_subt & get_comments() const
Definition: irep.h:322
static dt empty_d
Definition: irep.h:399
bool operator<(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:565
static void remove_ref(dt *old_data)
Definition: irep.cpp:99
named_subt & get_named_sub()
Definition: irep.h:319
#define DEPRECATED(msg)
Definition: deprecate.h:23
const named_subt & get_named_sub() const
Definition: irep.h:320
bool ordering(const irept &other) const
defines ordering on the internal representation
Definition: irep.cpp:429
void swap(dstringt &b)
Definition: dstring.h:132
~irept()
Definition: irep.h:248
static bool is_comment(const irep_namet &name)
Definition: irep.h:332
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:347
std::size_t full_hash() const
Definition: irep.cpp:605
void clear()
Definition: irep.h:313
bool operator()(const irept &i1, const irept &i2) const
Definition: irep.h:460
irept & add(const irep_namet &name)
Definition: irep.cpp:305
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
void make_nil()
Definition: irep.h:315
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
void clear()
Definition: irep.h:357
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:249
string hashing
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:259
dstringt irep_namet
Definition: irep.h:33
dstringt irep_idt
Definition: irep.h:32
bool operator==(const irept &other) const
Definition: irep.cpp:354
irept(const irep_idt &_id)
Definition: irep.h:175
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
Definition: irep.h:475
const subt & get_sub() const
Definition: irep.h:318
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:194
dt & write()
Definition: irep.h:411