Skip to content

Commit d394c49

Browse files
committed
merge_irept: do not store fresh irept::dt unless necessary
This optimisation ensures that operator== can use pointer equality when submitting an already-shared irept to merge_irept. On SV-COMP/ReachSafety-ECA this reduces the number of recursive operator== invocations from 5,814,764,546 (generated by 4,241,423,614 invocations) to 4,673,896,121 (generated from 4,295,188,693 invocations). That is, despite ~50M additional invocations (because the performance improvement permits more symbolic execution runs) around 1.1B recursive calls are avoided.
1 parent 7eb2862 commit d394c49

File tree

1 file changed

+17
-5
lines changed

1 file changed

+17
-5
lines changed

src/util/merge_irep.cpp

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -145,18 +145,26 @@ void merge_irept::operator()(irept &irep)
145145

146146
const irept &merge_irept::merged(const irept &irep)
147147
{
148+
if(irep.get_sub().empty() && irep.get_named_sub().empty())
149+
return *irep_store.insert(irep).first;
150+
148151
irep_storet::const_iterator entry=irep_store.find(irep);
149152
if(entry!=irep_store.end())
150153
return *entry;
151154

155+
bool same_irep = true;
152156
irept new_irep(irep.id());
153157

154158
const irept::subt &src_sub=irep.get_sub();
155159
irept::subt &dest_sub=new_irep.get_sub();
156160
dest_sub.reserve(src_sub.size());
157161

158162
forall_irep(it, src_sub)
159-
dest_sub.push_back(merged(*it)); // recursive call
163+
{
164+
const irept &op = merged(*it); // recursive call
165+
same_irep &= &op.read() == &(it->read());
166+
dest_sub.push_back(op);
167+
}
160168

161169
const irept::named_subt &src_named_sub=irep.get_named_sub();
162170
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
@@ -166,16 +174,20 @@ const irept &merge_irept::merged(const irept &irep)
166174
#endif
167175
forall_named_irep(it, src_named_sub)
168176
{
177+
const irept &op = merged(it->second); // recursive call
178+
same_irep &= &op.read() == &(it->second.read());
169179
#ifdef NAMED_SUB_IS_FORWARD_LIST
170-
dest_named_sub.emplace_after(
171-
before, it->first, merged(it->second)); // recursive call
180+
dest_named_sub.emplace_after(before, it->first, op);
172181
++before;
173182
#else
174-
dest_named_sub[it->first]=merged(it->second); // recursive call
183+
dest_named_sub.emplace(it->first, op);
175184
#endif
176185
}
177186

178-
return *irep_store.insert(std::move(new_irep)).first;
187+
if(same_irep)
188+
return *irep_store.insert(irep).first;
189+
else
190+
return *irep_store.insert(std::move(new_irep)).first;
179191
}
180192

181193
void merge_full_irept::operator()(irept &irep)

0 commit comments

Comments
 (0)