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