fix use-after-free in congruence closure gate table updates#162
fix use-after-free in congruence closure gate table updates#162sfiruch wants to merge 2 commits into
Conversation
MSVC's unordered_set::erase(iterator) recomputes the hash from the
element's current key to find which bucket's metadata needs updating.
In simplify_and_gate, rewrite_and_gate, rewrite_xor_gate and
simplify_xor_gate the gate's rhs vector was modified before the
iterator was passed to update_{and,xor}_gate, which in turn called
remove_gate (table.erase(git)). Because the key had already changed,
MSVC updated the wrong bucket, leaving a stale pointer to the freed
list node in the original bucket. A subsequent find() on any gate
that hashed to that bucket would then dereference the freed node,
detected as a heap-use-after-free by AddressSanitizer.
GCC and Clang's STL deduce the bucket from the node's position in
the list without recomputing the hash, so the bug did not manifest
there.
Fix: remove the gate from the table before modifying its rhs in all
four affected functions, and pass end(table) to the update helpers
(which already handle the !g->indexed case correctly).
Signed-off-by: Simon Felix <sf@iru.ch>
There was a problem hiding this comment.
Pull request overview
Fixes an MSVC-specific heap-use-after-free caused by mutating a gate’s hash key (rhs) while it is still stored in the congruence-closure unordered_set, then erasing via iterator.
Changes:
- Remove gates from the
GatesTablebefore mutatingrhsinsimplify_and_gate,rewrite_and_gate,rewrite_xor_gate, andsimplify_xor_gate. - Pass
end(table)intoupdate_{and,xor}_gateafter clearingg->indexed, relying on the helpers’ existing!g->indexedhandling. - Add an explanatory comment documenting the MSVC
unordered_set::erase(iterator)behavior and why removal must happen before key mutation.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
You can also share your feedback on Copilot code review. Take the survey.
| if (g->indexed) { | ||
| table.erase (table.find (g)); | ||
| g->indexed = false; | ||
| } |
There was a problem hiding this comment.
table.erase(table.find(g)) will invoke erase with end() if find(g) fails, which is undefined behavior. Previously this was guarded by an assert on the iterator. Consider storing the iterator, asserting it is not end(table) (or calling remove_gate(g) which already enforces the invariant), then erasing it and clearing g->indexed.
| GatesTable::iterator git = (g->indexed ? table.find (g) : end (table)); | ||
| assert (!g->indexed || git != table.end ()); | ||
| if (g->indexed) { | ||
| table.erase (table.find (g)); |
There was a problem hiding this comment.
table.erase(table.find(g)) can pass end() to erase if find(g) unexpectedly fails (UB). Since the earlier code asserted git != end(table) for indexed gates, it would be safer to keep an explicit iterator + assert here (or reuse remove_gate(g)), then erase and clear g->indexed.
| table.erase (table.find (g)); | |
| GatesTable::iterator it = table.find (g); | |
| assert (it != end (table)); | |
| table.erase (it); |
| check_xor_gate_implied (g); | ||
| GatesTable::iterator git = (g->indexed ? table.find (g) : end (table)); | ||
| if (g->indexed) { | ||
| table.erase (table.find (g)); |
There was a problem hiding this comment.
This table.erase(table.find(g)) sequence can call erase(end()) if find(g) fails, which is undefined behavior. Recommend capturing the iterator, asserting it is valid (or calling remove_gate(g)), then erasing and clearing g->indexed.
| table.erase (table.find (g)); | |
| GatesTable::iterator it = table.find (g); | |
| assert (it != table.end ()); | |
| table.erase (it); |
| unsigned negate = 0; | ||
| GatesTable::iterator git = (g->indexed ? table.find (g) : end (table)); | ||
| if (g->indexed) { | ||
| table.erase (table.find (g)); |
There was a problem hiding this comment.
Potential UB: if table.find(g) returns end(table) while g->indexed is true, table.erase(table.find(g)) would erase end(). Suggest storing the iterator and asserting it is valid (or using remove_gate(g)), matching the previous invariant checks.
| table.erase (table.find (g)); | |
| GatesTable::iterator it = table.find (g); | |
| assert (it != end (table)); | |
| table.erase (it); |
|
I replaced the entire hash-table by a custom implementation (62baa32). If this change is not part of the next release, I will merge your code. Thanks for the pull-request! |
Same MSVC-specific bug as fixed for the and/xor gate functions: rewrite_ite_gate and simplify_ite_gate captured a table iterator before modifying the gate, then passed it to remove_gate (table.erase). MSVC recomputes the hash from the current key on erase, so after the gate's lhs/rhs were changed the wrong bucket was updated, leaving a stale pointer in the original bucket. Fix: remove the gate from the table before any modifications, set g->indexed = false, and use end(table) as the sentinel iterator. Also add the missing if (g->indexed) guard before remove_gate in simplify_ite_gate to match the pattern in rewrite_ite_gate.
In
simplify_and_gate,rewrite_and_gate,rewrite_xor_gateandsimplify_xor_gatethe gate'srhsvector is modified before the stored iterator is passed toupdate_{and,xor}_gate, which in turn callsremove_gate(table.erase(git)). Because the key is changed, MSVC updates the wrong bucket, leaving a stale pointer to the freed list node in the original bucket. A subsequentfind()on any gate that hashed to that bucket dereferences the freed node.This is caught as a heap-use-after-free by AddressSanitizer in my Win64 port, which I compile with MSVC. Perhaps only that implementation of
unordered_set::erase(iterator)recomputes the hash from the element's current key to find which bucket's metadata needs updating. I think GCC and Clang's STL deduce the bucket from the node's position in the list without recomputing the hash, so the bug likely does not show up there. But I still think it's better to not rely on that implementation detail. AFAIK the STL does not promise to work.Fix: remove the gate from the table before modifying its
rhsin all four affected functions, and passend(table)to the update helpers (which already handle the!g->indexedcase correctly).