From a5495b78fa1610bad5484a3d953953d8ea77cd39 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 9 Jun 2026 07:36:05 -0700 Subject: [PATCH] Avoid invalidated column-cell references in LP pivot paths (#9783) MSVC ASan reports showed a container-overflow in LP tableau pivoting, reproducible from both examples and solver tests (issue #9781). The failure came from reading a `column_cell` through a reference after pivoting removed that entry from the backing column. - **Root cause** - `pivot_column_tableau` and the analogous Diophantine elimination loop both held `auto& c = column.back()` across a call (`pivot_row_to_row_given_cell`) that immediately removes that very cell from the column via `remove_element`. - After the mutation, the subsequent read `c.var()` used for bookkeeping observed invalid memory. - **Change** - Record the affected row in the bookkeeping set (`m_touched_rows` / `m_changed_rows`) by reading `c.var()` **before** the pivot call, while the back cell is still valid. - Make `static_matrix::pivot_row_to_row_given_cell` return `void` instead of `bool`. Its result (`!rowii.empty()`) was always `true`: both callers keep the matrix at full row rank (the tableau basis columns form an identity submatrix; the Diophantine `m_l_matrix` stays invertible), so an elementary row operation can never empty a row. The dead `if (!...) return false;` early-exit in `pivot_column_tableau` is removed and replaced with a `SASSERT(!rowii.empty())` documenting the invariant. - **Affected code paths** - `src/math/lp/static_matrix.h`, `src/math/lp/static_matrix.cpp`, `src/math/lp/static_matrix_def.h` - `src/math/lp/lp_core_solver_base_def.h` - `src/math/lp/dioph_eq.cpp` - **Behavioral impact** - No algorithmic change to pivoting. - Removes the stale-reference hazard in the loops that repeatedly eliminate entries from a column. ```c++ while (column.size() > 1) { auto& c = column.back(); SASSERT(c.var() != piv_row_index); if (m_touched_rows != nullptr) m_touched_rows->insert(c.var()); m_A.pivot_row_to_row_given_cell(piv_row_index, c, j); } ``` - **Verification** - Reproduced the exact issue #9781 failure on a local ASan build (`container-overflow` in `pivot_column_tableau`) using the pre-fix code, and confirmed it is gone with this change. - The 4 reported tests pass clean under ASan: `c_example`, `cpp_example`, `test-z3 get_implied_equalities`, `test-z3 quant_solve`. - Full `test-z3 /a` suite: 89 passed, 0 failed, 0 ASan errors. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner Co-authored-by: Lev Nachmanson Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/dioph_eq.cpp | 2 +- src/math/lp/lp_core_solver_base_def.h | 8 +++----- src/math/lp/static_matrix.cpp | 4 ++-- src/math/lp/static_matrix.h | 2 +- src/math/lp/static_matrix_def.h | 4 ++-- 5 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 5058bfaf3..0b3c5166a 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -709,8 +709,8 @@ namespace lp { while (column.size() > 1) { auto& c = column.back(); SASSERT(c.var() != last_row_index); - m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j); m_changed_rows.insert(c.var()); + m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j); } } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index c4c41c26e..21bd48a22 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index; } while (column.size() > 1) { - auto & c = column.back(); + auto& c = column.back(); SASSERT(c.var() != piv_row_index); - if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) { - return false; - } - if (m_touched_rows!= nullptr) + if (m_touched_rows != nullptr) m_touched_rows->insert(c.var()); + m_A.pivot_row_to_row_given_cell(piv_row_index, c, j); } if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs) diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp index 26ce218de..4abf0d88a 100644 --- a/src/math/lp/static_matrix.cpp +++ b/src/math/lp/static_matrix.cpp @@ -51,8 +51,8 @@ namespace lp { template void static_matrix >::set(unsigned int, unsigned int, mpq const&); - template bool static_matrix::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int); - template bool static_matrix >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int); + template void static_matrix::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int); + template void static_matrix >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int); template void static_matrix >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int); template void static_matrix::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell&, unsigned int, int); template void static_matrix >::add_rows(mpq const&, unsigned int, unsigned int); diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 415d3f1a2..08db2245d 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -293,7 +293,7 @@ public: // pivot row i to row ii - bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j); + void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j); void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign); void transpose_rows(unsigned i, unsigned ii) { auto t = m_rows[i]; diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index b28d67740..af07c4482 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -48,7 +48,7 @@ namespace lp { } - template bool static_matrix::pivot_row_to_row_given_cell(unsigned i, + template void static_matrix::pivot_row_to_row_given_cell(unsigned i, column_cell & c, unsigned pivot_col) { unsigned ii = c.var(); SASSERT(i < row_count() && ii < column_count() && i != ii); @@ -82,7 +82,7 @@ namespace lp { if (is_zero(rowii[k].coeff())) remove_element(rowii, rowii[k]); } - return !rowii.empty(); + SASSERT(!rowii.empty()); }