mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

Fix use-after-free in polymorphism substitution over sorts

Browse source 
In polymorphism::substitution::operator()(sort*), each substituted
sub-sort was held only in a local sort_ref that was destroyed at the end
of the loop iteration, while its raw pointer was retained in the
parameter vector passed to mk_sort. When the sub-sort's refcount dropped
to zero, its memory was freed and then reused by the next allocation,
producing a self-referential sort. Structural sort traversals such as
has_type_var (which has no cycle detection) then recursed infinitely,
manifesting as a stack overflow.

Pin each intermediate sub-sort in a sort_ref_vector so it stays alive
until after mk_sort has taken its own references.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 09:06:54 -07:00
parent c8e5dd0ca5
commit 6b7725dcb8
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/polymorphism_util.cpp
View file

@ -39,11 +39,13 @@ namespace polymorphism {
}
unsigned n = s->get_num_parameters();
vector<parameter> ps;
sort_ref_vector pin(m); // keep substituted sub-sorts alive until mk_sort below
for (unsigned i = 0; i < n; ++i) {
auto &p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
sort_ref s = (*this)(to_sort(p.get_ast()));
ps.push_back(parameter(s.get()));
sort_ref ss = (*this)(to_sort(p.get_ast()));
pin.push_back(ss);
ps.push_back(parameter(ss.get()));
}
else
ps.push_back(p);