From 07116de4b5756f8a1974882959c37fd940739f2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Aug 2026 20:27:50 -0700 Subject: [PATCH] Harden cg-root generation tracking against interrupted merges (#10385) 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 --- src/smt/seq_regex.cpp | 2 +- src/smt/smt_context.cpp | 32 ++++++++++++++++++++++++++++---- src/smt/smt_context.h | 7 +++++++ 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 96ce5eac8e..0eec49165c 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -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) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index b8e572513a..cb0474c69e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 0248c75a65..74c1689dea 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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; }