From 4bdfb598ea5e3352f78af0d2924923ff055ff237 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Fri, 19 Jun 2026 10:03:14 -0700 Subject: [PATCH] Fix stale func_interp entry table after compression (#9906) ## Summary Fix a use-after-free in `func_interp::compress()`. When a function interpretation had previously grown large enough to allocate `m_entry_table`, `compress()` could deallocate entries whose result matched the else-case but leave the hash table intact. Later `get_entry()` lookups could then return freed `func_entry*` values, which showed up during model checking as a corrupted expression result from `model_evaluator`. ## Root cause `func_interp::compress()` compacted `m_entries` and freed removed entries, but it did not rebuild or clear `m_entry_table`. This left stale pointers in the lookup table whenever: - the table had already been allocated on a larger interpretation, and - compression removed some entries. In the reported case, model evaluation rewrote `stack_s!1041` through `BR_REWRITE1`, fetched a freed `func_entry` result from the stale table, and then tripped an assertion in `expr::get_sort()` during quantifier model checking. ## Fix After compression removes entries, rebuild `m_entry_table` from the surviving `m_entries`, or clear it when the surviving interpretation is small. ## Regression coverage Added a unit regression in `src/test/model_evaluator.cpp` that: - creates a `func_interp` large enough to allocate `m_entry_table`, - compresses away almost all entries, - checks that removed keys no longer resolve, and - checks that the surviving key still resolves to the correct result. ## Validation - `../build/z3 ebso-115.smt2` previously hit an assertion in `rewriter_def.h` / `ast.cpp`; after the fix it no longer asserts. - `./test-z3 model_evaluator` passes with the new regression. ## Reproducer I did not produce a smaller SMT2 benchmark in this change. The original reproducer I used was `ebso-115.smt2`, and the new unit regression directly exercises the stale-entry-table path in-process. Co-authored-by: Can Cebeci --- src/model/func_interp.cpp | 10 ++++++++++ src/test/model_evaluator.cpp | 25 +++++++++++++++++++++++++ 2 files changed, 35 insertions(+) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 513c39b10..e42546f72 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -307,6 +307,16 @@ void func_interp::compress() { if (j < m_entries.size()) { reset_interp_cache(); m_entries.shrink(j); + if (m_entry_table) { + dealloc(m_entry_table); + m_entry_table = nullptr; + if (m_entries.size() > 500) { + m_entry_table = alloc(entry_table, 1024, + func_entry_hash(m_arity), func_entry_eq(m_arity)); + for (func_entry* curr : m_entries) + m_entry_table->insert(curr); + } + } } // other compression, if else is a default branch. // or function encode identity. diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index f4a64d4dc..77e13560b 100644 --- a/src/test/model_evaluator.cpp +++ b/src/test/model_evaluator.cpp @@ -1,5 +1,6 @@ #include "model/model.h" #include "model/model_evaluator.h" +#include "model/func_interp.h" #include "model/model_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/reg_decl_plugins.h" @@ -65,5 +66,29 @@ void tst_model_evaluator() { eval(e, v); std::cout << e << " " << v << "\n"; } + + { + func_interp fi2(m, 1); + expr_ref zero(a.mk_int(0), m); + expr_ref one(a.mk_int(1), m); + fi2.set_else(zero); + for (unsigned i = 0; i < 600; ++i) { + expr_ref arg(a.mk_int(rational(i)), m); + expr* args[1] = { arg.get() }; + fi2.insert_entry(args, i == 599 ? one.get() : zero.get()); + } + fi2.compress(); + SASSERT(fi2.num_entries() == 1); + + expr_ref removed_arg(a.mk_int(0), m); + expr* removed_args[1] = { removed_arg.get() }; + SASSERT(fi2.get_entry(removed_args) == nullptr); + + expr_ref kept_arg(a.mk_int(599), m); + expr* kept_args[1] = { kept_arg.get() }; + func_entry* kept = fi2.get_entry(kept_args); + SASSERT(kept != nullptr); + SASSERT(kept->get_result() == one.get()); + } }