CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
merge_irep.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "merge_irep.h"
10
11#include "irep_hash.h"
12
13std::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();
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=
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
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
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
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
144const 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
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 {
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
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
226 merged(irep_entry.second); // recursive call
227#endif
228 }
229
230 return *irep_store.insert(std::move(new_irep)).first;
231}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
static bool is_comment(const irep_idt &name)
Definition irep.h:460
const irep_idt & id() const
Definition irep.h:388
named_subt & get_named_sub()
Definition irep.h:450
irep_storet irep_store
Definition merge_irep.h:124
const irept & merged(const irept &irep)
void operator()(irept &)
const irept & merged(const irept &irep)
void operator()(irept &)
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 &)
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
bool operator==(const to_be_merged_irept &other) const
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