Multiple out-of-bounds access in vectors

[volkm]

The latest GCC/Clang versions enable debug assertion by default and as a result, the tests trigger multiple assertions for out-of-bounds access of a vector. See this CI run for an example.

I list the stacktraces for the failing tests in the following.

SparseCtmcCslHelper:

[ RUN      ] StatePermuterTest.ClusterTest
/usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.1.1/../../../../include/c++/15.1.1/bits/stl_vector.h:1263: reference std::vector<double>::operator[](size_type) [_Tp = double, _Alloc = std::allocator<double>]: Assertion '__n < this->size()' failed.

Process terminating with default action of signal 6 (SIGABRT)
   at 0xFFCF74C: __pthread_kill_implementation (pthread_kill.c:44)
   by 0xFF75DBF: raise (raise.c:26)
   by 0xFF5D579: abort (abort.c:73)
   by 0xFC17420: std::__glibcxx_assert_fail(char const*, int, char const*, char const*) (assert_fail.cc:41)
   by 0x413919C: std::vector<double, std::allocator<double> >::operator[](unsigned long) (in /opt/storm/build/bin/test-transformer)
   by 0xB1BAD4F: _ZN5storm12modelchecker6helper19SparseCtmcCslHelper29computeTransientProbabilitiesIdLb1ETnNSt9enable_ifIXsr5storm12NumberTraitsIT_EE19SupportsExponentialEiE4typeELi0EEESt6vectorIS5_SaIS5_EERKNS_11EnvironmentERKNS_7storage12SparseMatrixIS5_EEPKSA_S5_S5_SA_S5_ (src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp:682)
   by 0xB1BA6E4: _ZN5storm12modelchecker6helper19SparseCtmcCslHelper24computeCumulativeRewardsIdNS_6models6sparse19StandardRewardModelIdEETnNSt9enable_ifIXsr5storm12NumberTraitsIT_EE19SupportsExponentialEiE4typeELi0EEESt6vectorIS9_SaIS9_EERKNS_11EnvironmentEONS_6solver9SolveGoalIS9_S9_EERKNS_7storage12SparseMatrixIS9_EERKSE_RKT0_d (src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp:432)
   by 0xB16C1DA: storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> > >::computeCumulativeRewards(storm::Environment const&, storm::modelchecker::CheckTask<storm::logic::CumulativeRewardFormula, double> const&) (src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp:173)
   by 0xAF18DFB: storm::modelchecker::AbstractModelChecker<storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> > >::computeRewards(storm::Environment const&, storm::modelchecker::CheckTask<storm::logic::Formula, double> const&) (src/storm/modelchecker/AbstractModelChecker.cpp:167)
   by 0xAF1E6DF: storm::modelchecker::AbstractModelChecker<storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> > >::checkRewardOperatorFormula(storm::Environment const&, storm::modelchecker::CheckTask<storm::logic::RewardOperatorFormula, double> const&) (src/storm/modelchecker/AbstractModelChecker.cpp:355)
   by 0xAF1C0A5: storm::modelchecker::AbstractModelChecker<storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> > >::checkStateFormula(storm::Environment const&, storm::modelchecker::CheckTask<storm::logic::StateFormula, double> const&) (src/storm/modelchecker/AbstractModelChecker.cpp:262)
   by 0xAF15B24: storm::modelchecker::AbstractModelChecker<storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> > >::check(storm::Environment const&, storm::modelchecker::CheckTask<storm::logic::Formula, double> const&) (src/storm/modelchecker/AbstractModelChecker.cpp:56)

GmmxxLinearEquationSolver:

[ RUN      ] CtmcCslModelCheckerTest/0.simple2
/usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.1.1/../../../../include/c++/15.1.1/bits/stl_vector.h:1263: reference std::vector<double>::operator[](size_type): Assertion '__n < this->size()' failed.

Process terminating with default action of signal 6 (SIGABRT)
   at 0x1018574C: __pthread_kill_implementation (pthread_kill.c:44)
   by 0x1012BDBF: raise (raise.c:26)
   by 0x10113579: abort (abort.c:73)
   by 0xFDCD420: std::__glibcxx_assert_fail(char const*, int, char const*, char const*) (assert_fail.cc:41)
   by 0x41646DC: std::vector<double, std::allocator<double> >::operator[](unsigned long) (stl_vector.h:1263)
   by 0xBD7F4AA: void gmm::ilu_precond<gmm::csr_matrix<double, 0> >::do_ilu<gmm::csr_matrix<double, 0> >(gmm::csr_matrix<double, 0> const&, gmm::row_major) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:210)
   by 0xBD7E442: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::build_with(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:110)
   by 0xBD7E338: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::ilu_precond(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:113)
   by 0xBD727E7: std::__detail::_MakeUniq<gmm::ilu_precond<gmm::csr_matrix<double, 0> > >::__single_object std::make_unique<gmm::ilu_precond<gmm::csr_matrix<double, 0> >, gmm::csr_matrix<double, 0>&>(gmm::csr_matrix<double, 0>&) (unique_ptr.h:1085)
   by 0xBD716F2: storm::solver::GmmxxLinearEquationSolver<double>::internalSolveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/GmmxxLinearEquationSolver.cpp:63)
   by 0xBDBBC8D: storm::solver::LinearEquationSolver<double>::solveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/LinearEquationSolver.cpp:32)
   by 0xB7B348B: storm::modelchecker::helper::SparseDtmcPrctlHelper<double, storm::models::sparse::StandardRewardModel<double> >::computeReachabilityRewards(storm::Environment const&, storm::solver::SolveGoal<double, double>&&, storm::storage::SparseMatrix<double> const&, storm::storage::SparseMatrix<double> const&, std::function<std::vector<double, std::allocator<double> > (unsigned long, storm::storage::SparseMatrix<double> const&, storm::storage::BitVector const&)> const&, storm::storage::BitVector const&, bool, std::function<storm::storage::BitVector ()> const&, storm::modelchecker::ModelCheckerHint const&) (src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp:534)

[ RUN      ] ConditionalDtmcPrctlModelCheckerTest/0.Conditional
/usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.1.1/../../../../include/c++/15.1.1/bits/stl_vector.h:1263: reference std::vector<double>::operator[](size_type): Assertion '__n < this->size()' failed.

Process terminating with default action of signal 6 (SIGABRT)
   at 0x101D574C: __pthread_kill_implementation (pthread_kill.c:44)
   by 0x1017BDBF: raise (raise.c:26)
   by 0x10163579: abort (abort.c:73)
   by 0xFE1D420: std::__glibcxx_assert_fail(char const*, int, char const*, char const*) (assert_fail.cc:41)
   by 0x424945C: std::vector<double, std::allocator<double> >::operator[](unsigned long) (stl_vector.h:1263)
   by 0xBDCF4AA: void gmm::ilu_precond<gmm::csr_matrix<double, 0> >::do_ilu<gmm::csr_matrix<double, 0> >(gmm::csr_matrix<double, 0> const&, gmm::row_major) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:210)
   by 0xBDCE442: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::build_with(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:110)
   by 0xBDCE338: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::ilu_precond(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:113)
   by 0xBDC27E7: std::__detail::_MakeUniq<gmm::ilu_precond<gmm::csr_matrix<double, 0> > >::__single_object std::make_unique<gmm::ilu_precond<gmm::csr_matrix<double, 0> >, gmm::csr_matrix<double, 0>&>(gmm::csr_matrix<double, 0>&) (unique_ptr.h:1085)
   by 0xBDC16F2: storm::solver::GmmxxLinearEquationSolver<double>::internalSolveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/GmmxxLinearEquationSolver.cpp:63)
   by 0xBE0BC8D: storm::solver::LinearEquationSolver<double>::solveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/LinearEquationSolver.cpp:32)
   by 0xB80086E: storm::modelchecker::helper::SparseDtmcPrctlHelper<double, storm::models::sparse::StandardRewardModel<double> >::computeUntilProbabilities(storm::Environment const&, storm::solver::SolveGoal<double, double>&&, storm::storage::SparseMatrix<double> const&, storm::storage::SparseMatrix<double> const&, storm::storage::BitVector const&, storm::storage::BitVector const&, bool, storm::modelchecker::ModelCheckerHint const&) (src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp:237)

[ RUN      ] GradientDescentInstantiationSearcherTest/0.Simple
Trying out a new starting point
Trying initial guess (p->0.5 for every parameter p or set start point)
Starting at {p : 4503608634569751/9007199254740992}
/usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.1.1/../../../../include/c++/15.1.1/bits/stl_vector.h:1263: reference std::vector<double>::operator[](size_type): Assertion '__n < this->size()' failed.

Process terminating with default action of signal 6 (SIGABRT)
   at 0x108B874C: __pthread_kill_implementation (pthread_kill.c:44)
   by 0x1085EDBF: raise (raise.c:26)
   by 0x10846579: abort (abort.c:73)
   by 0x10500420: std::__glibcxx_assert_fail(char const*, int, char const*, char const*) (assert_fail.cc:41)
   by 0x41A44CC: std::vector<double, std::allocator<double> >::operator[](unsigned long) (stl_vector.h:1263)
   by 0xC4B24AA: void gmm::ilu_precond<gmm::csr_matrix<double, 0> >::do_ilu<gmm::csr_matrix<double, 0> >(gmm::csr_matrix<double, 0> const&, gmm::row_major) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:210)
   by 0xC4B1442: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::build_with(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:110)
   by 0xC4B1338: gmm::ilu_precond<gmm::csr_matrix<double, 0> >::ilu_precond(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h:113)
   by 0xC4A57E7: std::__detail::_MakeUniq<gmm::ilu_precond<gmm::csr_matrix<double, 0> > >::__single_object std::make_unique<gmm::ilu_precond<gmm::csr_matrix<double, 0> >, gmm::csr_matrix<double, 0>&>(gmm::csr_matrix<double, 0>&) (unique_ptr.h:1085)
   by 0xC4A46F2: storm::solver::GmmxxLinearEquationSolver<double>::internalSolveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/GmmxxLinearEquationSolver.cpp:63)
   by 0xC4EEC8D: storm::solver::LinearEquationSolver<double>::solveEquations(storm::Environment const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/LinearEquationSolver.cpp:32)
   by 0xBEE386E: storm::modelchecker::helper::SparseDtmcPrctlHelper<double, storm::models::sparse::StandardRewardModel<double> >::computeUntilProbabilities(storm::Environment const&, storm::solver::SolveGoal<double, double>&&, storm::storage::SparseMatrix<double> const&, storm::storage::SparseMatrix<double> const&, storm::storage::BitVector const&, storm::storage::BitVector const&, bool, storm::modelchecker::ModelCheckerHint const&) (src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp:237)

GmmxxMultiplier:

[ RUN      ] SparseMaPcaaMultiObjectiveModelCheckerTest.jobscheduler_pareto_3Obj
/usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/15.1.1/../../../../include/c++/15.1.1/bits/stl_vector.h:1282: const_reference std::vector<double>::operator[](size_type) const: Assertion '__n < this->size()' failed.

Process terminating with default action of signal 6 (SIGABRT)
   at 0x1006C74C: __pthread_kill_implementation (pthread_kill.c:44)
   by 0x10012DBF: raise (raise.c:26)
   by 0xFFFA579: abort (abort.c:73)
   by 0xFCB4420: std::__glibcxx_assert_fail(char const*, int, char const*, char const*) (assert_fail.cc:41)
   by 0x4162F5C: std::vector<double, std::allocator<double> >::operator[](unsigned long) const (stl_vector.h:1282)
   by 0xBC6FB80: gmm::linalg_traits<gmm::csr_matrix<double, 0> >::row_end(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_matrix.h:766)
   by 0xC04188B: gmm::linalg_traits<gmm::csr_matrix<double, 0> >::const_row_iterator gmm::mat_row_const_end<gmm::csr_matrix<double, 0> >(gmm::csr_matrix<double, 0> const&) (resources/3rdparty/gmm-5.2/include/gmm/gmm_def.h:814)
   by 0xC0376BF: void storm::solver::GmmxxMultiplier<double>::multAddReduceHelper<storm::utility::detail::DoubleGreater, true>(std::vector<unsigned long, std::allocator<unsigned long> > const&, std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const*, std::vector<double, std::allocator<double> >&, std::vector<unsigned long, std::allocator<unsigned long> >*) const (src/storm/solver/multiplier/GmmxxMultiplier.cpp:166)
   by 0xC034F83: storm::solver::GmmxxMultiplier<double>::multAddReduceHelper(storm::solver::OptimizationDirection const&, std::vector<unsigned long, std::allocator<unsigned long> > const&, std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const*, std::vector<double, std::allocator<double> >&, std::vector<unsigned long, std::allocator<unsigned long> >*, bool) const (src/storm/solver/multiplier/GmmxxMultiplier.cpp:145)
   by 0xC035019: storm::solver::GmmxxMultiplier<double>::multiplyAndReduceGaussSeidel(storm::Environment const&, storm::solver::OptimizationDirection const&, std::vector<unsigned long, std::allocator<unsigned long> > const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const*, std::vector<unsigned long, std::allocator<unsigned long> >*, bool) const (src/storm/solver/multiplier/GmmxxMultiplier.cpp:110)
   by 0xC0459EE: storm::solver::Multiplier<double>::multiplyAndReduceGaussSeidel(storm::Environment const&, storm::solver::OptimizationDirection const&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const*, std::vector<unsigned long, std::allocator<unsigned long> >*, bool) const (src/storm/solver/multiplier/Multiplier.cpp:43)
   by 0xBA53E8A: storm::solver::AcyclicMinMaxLinearEquationSolver<double>::internalSolveEquations(storm::Environment const&, storm::solver::OptimizationDirection, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> > const&) const (src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp:90)

[volkm]

The issue in GmmxxLinearEquationSolver is triggered in line 210 of gmm_precond_ilu.h. Here, vector L_val is empty.
It seems that this issue is still present in gmm v.5.4.4, see here and is most likely an issue which should be fixed in gmm.

[volkm]

Opened an issue for gmm++.