cprover
merge_irep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "merge_irep.h"
10 
11 #include "irep_hash.h"
12 
13 std::size_t to_be_merged_irept::hash() const
14 {
15  std::size_t result=hash_string(id());
16 
17  const irept::subt &sub=get_sub();
18  const irept::named_subt &named_sub=get_named_sub();
19 
20  forall_irep(it, sub)
21  result=hash_combine(result, static_cast<const merged_irept &>(*it).hash());
22 
23  forall_named_irep(it, named_sub)
24  {
25  result=hash_combine(result, hash_string(it->first));
26  result=
28  result, static_cast<const merged_irept &>(it->second).hash());
29  }
30 
31  const std::size_t named_sub_size = named_sub.size();
32  result = hash_finalize(result, named_sub_size + sub.size());
33 
34  return result;
35 }
36 
38 {
39  if(id()!=other.id())
40  return false;
41 
42  const irept::subt &sub=get_sub();
43  const irept::subt &o_sub=other.get_sub();
44  const irept::named_subt &named_sub=get_named_sub();
45  const irept::named_subt &o_named_sub=other.get_named_sub();
46 
47  if(sub.size()!=o_sub.size())
48  return false;
49 #ifdef NAMED_SUB_IS_FORWARD_LIST
50  if(
51  std::distance(named_sub.begin(), named_sub.end()) !=
52  std::distance(o_named_sub.begin(), o_named_sub.end()))
53  {
54  return false;
55  }
56 #else
57  if(named_sub.size()!=o_named_sub.size())
58  return false;
59 #endif
60 
61  {
62  irept::subt::const_iterator s_it=sub.begin();
63  irept::subt::const_iterator os_it=o_sub.begin();
64 
65  for(; s_it!=sub.end(); s_it++, os_it++)
66  if(static_cast<const merged_irept &>(*s_it)!=
67  static_cast<const merged_irept &>(*os_it))
68  return false;
69  }
70 
71  {
72  irept::named_subt::const_iterator s_it=named_sub.begin();
73  irept::named_subt::const_iterator os_it=o_named_sub.begin();
74 
75  for(; s_it!=named_sub.end(); s_it++, os_it++)
76  if(s_it->first!=os_it->first ||
77  static_cast<const merged_irept &>(s_it->second)!=
78  static_cast<const merged_irept &>(os_it->second))
79  return false;
80  }
81 
82  return true;
83 }
84 
86 {
87  // first see if it's already a merged_irep
88 
89  merged_irep_storet::const_iterator entry=
90  merged_irep_store.find(merged_irept(irep));
91 
92  if(entry!=merged_irep_store.end())
93  return *entry; // nothing to do
94 
95  // need to build new irep that will be in the container
96  irept new_irep(irep.id());
97 
98  const irept::subt &src_sub=irep.get_sub();
99  irept::subt &dest_sub=new_irep.get_sub();
100  dest_sub.reserve(src_sub.size());
101 
102  forall_irep(it, src_sub)
103  dest_sub.push_back(merged(*it)); // recursive call
104 
105  const irept::named_subt &src_named_sub=irep.get_named_sub();
106  irept::named_subt &dest_named_sub=new_irep.get_named_sub();
107 
108 #ifdef NAMED_SUB_IS_FORWARD_LIST
109  irept::named_subt::iterator before = dest_named_sub.before_begin();
110 #endif
111  forall_named_irep(it, src_named_sub)
112  {
113 #ifdef NAMED_SUB_IS_FORWARD_LIST
114  dest_named_sub.emplace_after(
115  before, it->first, merged(it->second)); // recursive call
116  ++before;
117 #else
118  dest_named_sub[it->first]=merged(it->second); // recursive call
119 #endif
120  }
121 
122  std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
124 
125  if(result.second) // really new, record
126  merged_irep_store.insert(merged_irept(new_irep));
127 
128  return
129  static_cast<const merged_irept &>(
130  static_cast<const irept &>(*result.first));
131 }
132 
134 {
135  // only useful if there is sharing
136  #ifdef SHARING
137  irep=merged(irep);
138  #endif
139 }
140 
141 const irept &merge_irept::merged(const irept &irep)
142 {
143  auto entry = irep_store.insert(irep);
144  if(!entry.second)
145  return *entry.first;
146 
147  const irept::subt &src_sub=irep.get_sub();
148  irept::subt *dest_sub_ptr = nullptr;
149 
150  std::size_t index = 0;
151  forall_irep(it, src_sub)
152  {
153  const irept &op = merged(*it); // recursive call
154  if(&op.read() != &(it->read()))
155  {
156  if(!dest_sub_ptr)
157  dest_sub_ptr = &(const_cast<irept &>(*entry.first)).get_sub();
158  (*dest_sub_ptr)[index] = op;
159  }
160  ++index;
161  }
162 
163  const irept::named_subt &src_named_sub=irep.get_named_sub();
164  irept::named_subt *dest_named_sub_ptr = nullptr;
165 
166  std::ptrdiff_t advance_by = 0;
167  forall_named_irep(it, src_named_sub)
168  {
169  if(!irept::is_comment(it->first))
170  {
171  const irept &op = merged(it->second); // recursive call
172  if(&op.read() != &(it->second.read()))
173  {
174  if(!dest_named_sub_ptr)
175  dest_named_sub_ptr =
176  &(const_cast<irept &>(*entry.first)).get_named_sub();
177  std::next(dest_named_sub_ptr->begin(), advance_by)->second = op;
178  }
179  }
180  ++advance_by;
181  }
182 
183  return *entry.first;
184 }
185 
187 {
188  // only useful if there is sharing
189  #ifdef SHARING
190  irep=merged(irep);
191  #endif
192 }
193 
195 {
196  irep_storet::const_iterator entry=irep_store.find(irep);
197  if(entry!=irep_store.end())
198  return *entry;
199 
200  irept new_irep(irep.id());
201 
202  const irept::subt &src_sub=irep.get_sub();
203  irept::subt &dest_sub=new_irep.get_sub();
204  dest_sub.reserve(src_sub.size());
205 
206  forall_irep(it, src_sub)
207  dest_sub.push_back(merged(*it)); // recursive call
208 
209  const irept::named_subt &src_named_sub=irep.get_named_sub();
210  irept::named_subt &dest_named_sub=new_irep.get_named_sub();
211 
212 #ifdef NAMED_SUB_IS_FORWARD_LIST
213  irept::named_subt::iterator before = dest_named_sub.before_begin();
214 #endif
215  forall_named_irep(it, src_named_sub)
216  {
217 #ifdef NAMED_SUB_IS_FORWARD_LIST
218  dest_named_sub.emplace_after(
219  before, it->first, merged(it->second)); // recursive call
220  ++before;
221 #else
222  dest_named_sub[it->first]=merged(it->second); // recursive call
223 #endif
224  }
225 
226  return *irep_store.insert(std::move(new_irep)).first;
227 }
std::size_t hash() const
Definition: merge_irep.cpp:13
irep_storet irep_store
Definition: merge_irep.h:124
void operator()(irept &)
Definition: merge_irep.cpp:133
#define forall_named_irep(it, irep)
Definition: irep.h:70
subt & get_sub()
Definition: irep.h:477
const irep_idt & id() const
Definition: irep.h:418
const irept & merged(const irept &irep)
Definition: merge_irep.cpp:194
#define hash_finalize(h1, len)
Definition: irep_hash.h:122
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:381
const dt & read() const
Definition: irep.h:270
bool operator==(const to_be_merged_irept &other) const
Definition: merge_irep.cpp:37
named_subt & get_named_sub()
Definition: irep.h:479
void operator()(irept &)
Definition: merge_irep.cpp:186
size_t hash_string(const dstringt &s)
Definition: dstring.h:211
irep hash functions
static bool is_comment(const irep_namet &name)
Definition: irep.h:489
to_be_merged_irep_storet to_be_merged_irep_store
Definition: merge_irep.h:96
const irept & merged(const irept &irep)
Definition: merge_irep.cpp:141
irep_storet irep_store
Definition: merge_irep.h:112
#define hash_combine(h1, h2)
Definition: irep_hash.h:120
const merged_irept & merged(const irept &)
Definition: merge_irep.cpp:85
merged_irep_storet merged_irep_store
Definition: merge_irep.h:92
#define forall_irep(it, irep)
Definition: irep.h:62