Skip to content

Commit fd7c02d

Browse files
committed
merge_irept: insert once and then const_cast to edit in place
This avoids multiple lookups in the hash set, each of which requires a number of operator== and hash() calls. The use of const_cast is acceptable, because we do not actually change the object in a way that would affect ordering (objects will continue to have the same hash value and still compare equal). We furthermore ensure 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 2,232,563,047 (generated from 4,326,016,698 invocations). That is, despite ~100M additional invocations (because the performance improvement permits more symbolic execution runs) around 3.6B recursive calls are avoided.
1 parent d5740b3 commit fd7c02d

File tree

1 file changed

+29
-20
lines changed

1 file changed

+29
-20
lines changed

src/util/merge_irep.cpp

Lines changed: 29 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -145,37 +145,46 @@ void merge_irept::operator()(irept &irep)
145145

146146
const irept &merge_irept::merged(const irept &irep)
147147
{
148-
irep_storet::const_iterator entry=irep_store.find(irep);
149-
if(entry!=irep_store.end())
150-
return *entry;
151-
152-
irept new_irep(irep.id());
148+
auto entry = irep_store.insert(irep);
149+
if(!entry.second)
150+
return *entry.first;
153151

154152
const irept::subt &src_sub=irep.get_sub();
155-
irept::subt &dest_sub=new_irep.get_sub();
156-
dest_sub.reserve(src_sub.size());
153+
irept::subt *dest_sub_ptr = nullptr;
157154

155+
std::size_t index = 0;
158156
forall_irep(it, src_sub)
159-
dest_sub.push_back(merged(*it)); // recursive call
157+
{
158+
const irept &op = merged(*it); // recursive call
159+
if(&op.read() != &(it->read()))
160+
{
161+
if(!dest_sub_ptr)
162+
dest_sub_ptr = &(const_cast<irept &>(*entry.first)).get_sub();
163+
(*dest_sub_ptr)[index] = op;
164+
}
165+
++index;
166+
}
160167

161168
const irept::named_subt &src_named_sub=irep.get_named_sub();
162-
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
169+
irept::named_subt *dest_named_sub_ptr = nullptr;
163170

164-
#ifdef NAMED_SUB_IS_FORWARD_LIST
165-
irept::named_subt::iterator before = dest_named_sub.before_begin();
166-
#endif
171+
std::ptrdiff_t advance_by = 0;
167172
forall_named_irep(it, src_named_sub)
168173
{
169-
#ifdef NAMED_SUB_IS_FORWARD_LIST
170-
dest_named_sub.emplace_after(
171-
before, it->first, merged(it->second)); // recursive call
172-
++before;
173-
#else
174-
dest_named_sub[it->first]=merged(it->second); // recursive call
175-
#endif
174+
if(!irept::is_comment(it->first))
175+
{
176+
const irept &op = merged(it->second); // recursive call
177+
if(&op.read() != &(it->second.read()))
178+
{
179+
if(!dest_named_sub_ptr)
180+
dest_named_sub_ptr = &(const_cast<irept &>(*entry.first)).get_named_sub();
181+
std::next(dest_named_sub_ptr->begin(), advance_by)->second = op;
182+
}
183+
}
184+
++advance_by;
176185
}
177186

178-
return *irep_store.insert(std::move(new_irep)).first;
187+
return *entry.first;
179188
}
180189

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

0 commit comments

Comments
 (0)