mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

Fix trail-scope leak in ho_matcher on early exit (#10196)

Browse source 
The higher-order matcher shares the solver's trail stack. On early-exit
paths (resource/rlimit reached via m.inc(), or search budget exhausted)
work items were left on m_backtrack with their pushed scopes never popped,
leaking a trail scope. This desynchronized the trail scope count from the
solver scope level and later tripped SASSERT(ilvl <= m_scope_lvl) /
unsound backtracking in smt::context::reinit_clauses.

Restore the trail before exit on every path using an RAII guard
(scoped_trail_level) and drain the backtrack stack after the main search
loop so m_backtrack is left empty for the next call. This avoids wrapping
large blocks in try/catch (which would mask underlying bugs such as
creating non-well-sorted expressions) while still guaranteeing the trail
is restored on both normal and exceptional exits. The sort-mismatch check
and UNREACHABLE() in refine_ho_match are preserved so ill-sorted terms
remain surfaced rather than silently discarded.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This commit is contained in:
Nikolaj Bjorner 2026-07-23 10:05:28 -07:00
parent e0f978f7cd
commit c9d3dc959d
1 changed files with 29 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/ast/euf/ho_matcher.cpp
View file

@ -49,6 +49,22 @@ Author:
namespace euf {
// RAII guard that restores the shared trail stack to the scope level
// captured at construction. The matcher shares the solver's trail stack, so
// leaking a scope on an early or exceptional exit desynchronizes the trail
// scope count from the solver scope level and later trips an assertion /
// unsound backtracking in smt::context::reinit_clauses. Using a guard
// restores the trail before exit on every path without wrapping large blocks
// of code in exception handlers that would mask underlying bugs.
namespace {
struct scoped_trail_level {
trail_stack& m_trail;
unsigned m_base;
scoped_trail_level(trail_stack& t) : m_trail(t), m_base(t.get_num_scopes()) {}
~scoped_trail_level() { m_trail.pop_scope(m_trail.get_num_scopes() - m_base); }
};
}
expr_ref_vector const &ho_subst::get_binding(quantifier *q) {
ast_manager &m = m_subst.get_manager();
m_binding.reset();
@ -102,13 +118,13 @@ namespace euf {
}
void ho_matcher::operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars) {
scoped_trail_level _restore(m_trail);
m_trail.push_scope();
m_subst.resize(0);
m_subst.resize(num_vars);
m_goals.reset();
m_goals.push(0, num_bound, pat, t);
search();
m_trail.pop_scope(1);
}
void ho_matcher::search() {
@ -119,8 +135,6 @@ namespace euf {
while (m.inc()) {
if (budget-- == 0) {
IF_VERBOSE(2, verbose_stream() << "ho_matcher: search budget exhausted\n");
while (!m_backtrack.empty())
backtrack();
break;
}
// Q, B -> Q', B'. Push work on the backtrack stack and new work items
@ -133,6 +147,17 @@ namespace euf {
break;
}
// Drain any remaining work items so that every backtracking scope pushed
// in consume_work is popped again and m_backtrack is left empty for the
// next call. The loop above can exit early - budget exhausted, or
// m.inc() reporting that the resource limit has been reached - with items
// still on the backtrack stack. Because the matcher shares the solver's
// trail stack, leaking a scope here would desynchronize the trail scope
// count from the solver scope level and later trigger an assertion
// failure / unsound backtracking in smt::context::reinit_clauses.
while (!m_backtrack.empty())
backtrack();
IF_VERBOSE(10, display(verbose_stream() << "ho_matcher: done\n"));
}
@ -947,7 +972,7 @@ namespace euf {
auto& abs = m_pat2abs[fo_pat];
verbose_stream() << " m_pat2abs size: " << abs.size() << "\n";
for (auto [v, pat] : abs) verbose_stream() << " v=" << v << " pat=" << mk_pp(pat, m) << "\n";);
unsigned base_scope = m_trail.get_num_scopes();
scoped_trail_level _restore(m_trail);
m_trail.push_scope();
m_subst.resize(0);
m_subst.resize(s.size());
@ -974,7 +999,6 @@ namespace euf {
// higher-order pattern. Discard this refinement candidate (produce
// no instance) instead of aborting the whole solve.
if (!subst_sorts_match(m, pat, s, true)) {
m_trail.pop_scope(1);
IF_VERBOSE(0, verbose_stream() << "refine_ho_match: sorts do not match for " << mk_pp(pat, m) << " and "
<< s << "\n";);
UNREACHABLE();
@ -988,8 +1012,6 @@ namespace euf {
m_goals.push(level, num_bound, pat_refined, m_subst.get(v));
}
search();
m_trail.pop_scope(1);
}
bool ho_matcher::subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order) {