Skip to content

fix use-after-free in congruence closure gate table updates #162

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
sfiruch wants to merge 2 commits into from
+35 −12
Closed

fix use-after-free in congruence closure gate table updates #162

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e771a25
fix use-after-free in congruence closure gate table updates
sfiruch Mar 9, 2026
9937740
also fix use-after-free in rewrite_ite_gate and simplify_ite_gate
sfiruch Mar 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 35 additions & 12 deletions src/congruence.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2744,8 +2744,14 @@ void Closure::update_xor_gate (Gate *g, GatesTable::iterator git) {
void Closure::simplify_and_gate (Gate *g) {
if (skip_and_gate (g))
return;
GatesTable::iterator git = (g->indexed ? table.find (g) : end (table));
assert (!g->indexed || git != end (table));
// Remove before modifying rhs: MSVC's unordered_set::erase(iterator)
// recomputes the hash from the current key to fix up bucket pointers,
// so the erase must happen before rhs changes (unlike GCC/Clang STL).
if (g->indexed) {
table.erase (table.find (g));
g->indexed = false;
}
Comment on lines +2750 to +2753
Copy link

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copilot uses AI. Check for mistakes.
GatesTable::iterator git = end (table);
LOG (g, "simplifying");
int falsifies = 0;
std::vector<int>::iterator it = begin (g->rhs);
Expand Down Expand Up @@ -4496,8 +4502,11 @@ void Closure::rewrite_and_gate (Gate *g, int dst, int src, LRAT_ID id1,
assert (dst);
assert (internal->val (src) == internal->val (dst));
LOG (g, "rewriting %d into %d in", src, dst);
GatesTable::iterator git = (g->indexed ? table.find (g) : end (table));
assert (!g->indexed || git != table.end ());
if (g->indexed) {
table.erase (table.find (g));
Copy link

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Suggested change
table.erase (table.find (g));
GatesTable::iterator it = table.find (g);
assert (it != end (table));
table.erase (it);

Copilot uses AI. Check for mistakes.
g->indexed = false;
}
GatesTable::iterator git = end (table);
int clashing = 0, falsifies = 0;
unsigned dst_count = 0, not_dst_count = 0;
auto q = begin (g->rhs);
Expand Down Expand Up @@ -4692,7 +4701,11 @@ void Closure::rewrite_xor_gate (Gate *g, int dst, int src) {
return;
LOG (g, "rewriting (%d -> %d)", src, dst);
check_xor_gate_implied (g);
GatesTable::iterator git = (g->indexed ? table.find (g) : end (table));
if (g->indexed) {
table.erase (table.find (g));
Copy link

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Suggested change
table.erase (table.find (g));
GatesTable::iterator it = table.find (g);
assert (it != table.end ());
table.erase (it);

Copilot uses AI. Check for mistakes.
g->indexed = false;
}
GatesTable::iterator git = end (table);
size_t j = 0, dst_count = 0;
bool original_dst_negated = (dst < 0);
dst = internal->vidx (dst);
Expand Down Expand Up @@ -4766,7 +4779,11 @@ void Closure::simplify_xor_gate (Gate *g) {
return;
check_xor_gate_implied (g);
unsigned negate = 0;
GatesTable::iterator git = (g->indexed ? table.find (g) : end (table));
if (g->indexed) {
table.erase (table.find (g));
Copy link

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Suggested change
table.erase (table.find (g));
GatesTable::iterator it = table.find (g);
assert (it != end (table));
table.erase (it);

Copilot uses AI. Check for mistakes.
g->indexed = false;
}
GatesTable::iterator git = end (table);
const size_t size = g->arity ();
size_t j = 0;
for (size_t i = 0; i < size; ++i) {
Expand Down Expand Up @@ -5677,9 +5694,11 @@ void Closure::rewrite_ite_gate (Gate *g, int dst, int src) {

bool garbage = false;
bool shrink = true;
const auto git = g->indexed ? table.find (g) : end (table);
assert (!g->indexed || git != end (table));
assert (*git == g);
if (g->indexed) {
table.erase (table.find (g));
g->indexed = false;
}
GatesTable::iterator git = end (table);
if (internal->val (cond) && internal->val (then_lit) &&
internal->val (else_lit)) { // propagation has set all value anyway
LOG (g, "all values are set");
Expand Down Expand Up @@ -6620,8 +6639,11 @@ void Closure::simplify_ite_gate (Gate *g) {
}
} else {
assert (!!v_then + !!v_else == 1);
auto git = g->indexed ? table.find (g) : end (table);
assert (!g->indexed || git != end (table));
if (g->indexed) {
table.erase (table.find (g));
g->indexed = false;
}
GatesTable::iterator git = end (table);
if (v_then > 0) {
g->lhs = -lhs;
rhs[0] = -cond;
Expand Down Expand Up @@ -6664,7 +6686,8 @@ void Closure::simplify_ite_gate (Gate *g) {
++internal->stats.congruence.ites;
}
} else {
remove_gate (git);
if (g->indexed)
remove_gate (git);
index_gate (g);
garbage = false;
for (auto lit : rhs)
Expand Down