mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00
Code Activity

Harden cg-root generation tracking against interrupted merges (#10385)

Browse source 
Fixes state corruption that manifests as a SIGSEGV inside the MBQI model
checker's auxiliary context::check (regression after 4.16.0). The crash
sites vary per run (null enode in a worklist traversal, null enode in
boolean propagation, virtual dispatch through a freed justification) but
all share the pattern 'solver state corrupted, faults wherever it is next
touched'. The corruption originates in the new-in-5.0 machinery that
stores instantiation generations on congruence-class roots and replays
them across merges/unmerges.

Three unguarded spots in that machinery, each capable of producing that
pattern, are hardened:

1. get_cg_root() (smt_context.h): on a cg_table miss find() returns
   nullptr and callers immediately read ->m_generation, segfaulting
   (fault site 1). Fall back to treating n as its own root. Generations
   are a heuristic quantity, so this is sound and merely conservative
   while converting a crash into safe behaviour.

2. reinsert_parents_into_cg_table() (smt_context.cpp): the positional
   generation cache was consumed with unchecked indexing, unlike its
   sibling undo_add_eq() which already bounds-checks. A transiently
   desynced cache could read out of bounds and write a bogus generation.
   Bounds-check the index and fall back to get_generation(parent).

3. add_eq()'s catch(...) rollback (smt_context.cpp): remove_parents /
   reinsert_parents maintain two pieces of transient state not tracked by
   the trail stack -- marks on r1's parents and the m_r1_parent_generations
   scratch vector. If add_eq is interrupted between the two, a still-marked
   parent is silently skipped by the next remove_parents and a leftover
   cache entry desyncs the positional replay, arming the corruption for
   every later merge. Clear both before unwinding.

Also fixes an unrelated MSVC build break in seq_regex.cpp (a lambda
illegally captured the member reference 'ctx' by name instead of 'this').

Validated: seq_monadic unit tests pass; 90 MBQI runs over fstar-ulib
quantified VCs with an rlimit sweep (forcing cancellation mid-MBQI)
show no crashes or regressions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-08-04 20:27:50 -07:00
parent 227238cc0c
commit 07116de4b5
3 changed files with 36 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq_regex.cpp
View file

@ -99,7 +99,7 @@ namespace smt {
}
bool seq_regex::all_true(literal_vector const& lits) const {
return all_of(lits, [&ctx](literal lit) { return l_true == ctx.get_assignment(lit); });
return all_of(lits, [this](literal lit) { return l_true == ctx.get_assignment(lit); });
}
void seq_regex::add_core_literal(void* dep, literal_vector& lits) {

32
src/smt/smt_context.cpp
View file

@ -480,6 +480,7 @@ namespace smt {
*/
void context::add_eq(enode * n1, enode * n2, eq_justification js) {
unsigned old_trail_size = m_trail_stack.size();
enode * r1 = nullptr;
scoped_suspend_rlimit _suspend_cancel(m.limit());
try {
@ -489,7 +490,7 @@ namespace smt {
SASSERT(n1->get_sort() == n2->get_sort());
m_stats.m_num_add_eq++;
enode * r1 = n1->get_root();
r1 = n1->get_root();
enode * r2 = n2->get_root();
if (r1 == r2) {
@ -589,6 +590,19 @@ namespace smt {
// Restore trail size since procedure was interrupted in the middle.
// If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
TRACE(add_eq, tout << "add_eq interrupted. This is unsafe " << m.limit().is_canceled() << "\n";);
// remove_parents_from_cg_table / reinsert_parents_into_cg_table maintain two pieces of
// transient state that are NOT tracked by the trail stack: marks on r1's parents (set in
// remove_parents, cleared in reinsert) and the m_r1_parent_generations scratch vector. If
// add_eq is interrupted between these two calls the marks and the vector are left
// inconsistent; unless cleared they corrupt the *next* add_eq (a still-marked parent is
// silently skipped by remove_parents, and a leftover entry desyncs the positional
// generation replay), which manifests as congruence-table corruption and later crashes
// (issue #10385). Restore both here before unwinding.
if (r1) {
for (enode * parent : enode::parents(r1))
parent->unset_mark();
}
m_r1_parent_generations.reset();
m_trail_stack.shrink(old_trail_size);
throw;
}
@ -692,9 +706,19 @@ namespace smt {
// Look up the generation cache
unsigned parent_generation = 0; // Just use generation 0 for equalities
if (!parent->is_eq()) {
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
SASSERT(p == parent);
parent_generation = g;
// The cache is consumed positionally, in the same order remove_parents_from_cg_table
// populated it. Guard the index (as undo_add_eq already does) so that a transiently
// desynced cache cannot read out of bounds and scribble a bogus generation through a
// stale pointer (see issue #10385). In the healthy case idx is always in range and
// p == parent.
if (generation_cache_idx < m_r1_parent_generations.size()) {
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
SASSERT(p == parent);
parent_generation = g;
}
else {
parent_generation = get_generation(parent);
}
}
auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);

7
src/smt/smt_context.h
View file

@ -1237,6 +1237,13 @@ namespace smt {
return n;
auto r = m_cg_table.find(n);
SASSERT(r != nullptr);
// Defensive: if the "every non-cgr node has a cg_table entry" invariant is transiently
// violated (e.g. after an interrupted merge), find() returns nullptr. Reading
// ->m_generation through it would segfault (see issue #10385, fault site 1). Fall back
// to treating n as its own root; generations are a heuristic quantity, so this is sound
// and merely conservative, while turning a crash into safe behaviour.
if (r == nullptr)
return n;
return r;
}