Issue Description
I was roughly going through some implementation in IC3 and the clear method
|
void ProofGoalQueue::clear() |
|
{ |
|
for (auto p : store_) { |
|
delete p; |
|
} |
|
store_.clear(); |
|
while (!queue_.empty()) { |
|
queue_.pop(); |
|
} |
|
} |
just don't feel right. Since when pop(), priority_queue::pop() calls std::pop_heap, which calls the comparator
|
struct ProofGoalOrder |
|
{ |
|
// comparison for priority queue |
|
// since priority queue returns largest element, we swap the arguments |
|
// -- we want the lowest index to be processed first |
|
bool operator()(const ProofGoal * a, const ProofGoal * b) const |
|
{ |
|
return b->idx < a->idx; |
|
} |
|
}; |
But at this time, what stores in _store has already been deleted (_store and queue_ share ownership of same raw pointers).
Test
So in --debug mode with a manually added -fsanitize=address, run ASAN_OPTIONS=detect_container_overflow=0 make check it indeed shows some errors such as:
==30387==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000144128 at pc 0x0001060d2f60 bp 0x00016ced2e10 sp 0x00016ced2e08
READ of size 8 at 0x607000144128 thread T0
#0 0x0001060d2f5c in pono::ProofGoalOrder::operator()(pono::ProofGoal const*, pono::ProofGoal const*) const ic3base.h:136
#1 0x0001060d27d0 in std::__1::__wrap_iter<pono::ProofGoal**> std::__1::__floyd_sift_down[abi:ne200100]<std::__1::_ClassicAlgPolicy, pono::ProofGoalOrder&, std::__1::__wrap_iter<pono::ProofGoal**>>(std::__1::__wrap_iter<pono::ProofGoal**>, pono::ProofGoalOrder&, std::__1::iterator_traits<std::__1::__wrap_iter<pono::ProofGoal**>>::difference_type) sift_down.h:98
#2 0x0001060d22cc in void std::__1::__pop_heap[abi:ne200100]<std::__1::_ClassicAlgPolicy, pono::ProofGoalOrder, std::__1::__wrap_iter<pono::ProofGoal**>>(std::__1::__wrap_iter<pono::ProofGoal**>, std::__1::__wrap_iter<pono::ProofGoal**>, pono::ProofGoalOrder&, std::__1::iterator_traits<std::__1::__wrap_iter<pono::ProofGoal**>>::difference_type) pop_heap.h:47
#3 0x0001060d1f88 in void std::__1::pop_heap[abi:ne200100]<std::__1::__wrap_iter<pono::ProofGoal**>, pono::ProofGoalOrder>(std::__1::__wrap_iter<pono::ProofGoal**>, std::__1::__wrap_iter<pono::ProofGoal**>, pono::ProofGoalOrder) pop_heap.h:68
#4 0x0001060b4124 in std::__1::priority_queue<pono::ProofGoal*, std::__1::vector<pono::ProofGoal*, std::__1::allocator<pono::ProofGoal*>>, pono::ProofGoalOrder>::pop() queue:922
#5 0x0001060b3d34 in pono::ProofGoalQueue::clear() ic3base.cpp:80
#6 0x0001060c0748 in pono::IC3Base::block_all() ic3base.cpp:646
#7 0x0001060b734c in pono::IC3Base::step(int) ic3base.cpp:441
#8 0x0001060b6bd8 in pono::IC3Base::check_until(int) ic3base.cpp:175
#9 0x000102f325d8 in pono_tests::UtilsEngineUnitTests_MakeProver_Test::TestBody() test_utils.cpp:146
#10 0x00010307bb80 in void testing::internal::HandleSehExceptionsInMethodIfSupported<testing::Test, void>(testing::Test*, void (testing::Test::*)(), char const*) gtest.cc:2686
#11 0x000102fe5b10 in void testing::internal::HandleExceptionsInMethodIfSupported<testing::Test, void>(testing::Test*, void (testing::Test::*)(), char const*) gtest.cc:2722
#12 0x000102fe58a4 in testing::Test::Run() gtest.cc:2761
#13 0x000102fe7d64 in testing::TestInfo::Run() gtest.cc:2907
#14 0x000102fea94c in testing::TestSuite::Run() gtest.cc:3085
#15 0x00010300f17c in testing::internal::UnitTestImpl::RunAllTests() gtest.cc:6077
#16 0x000103095438 in bool testing::internal::HandleSehExceptionsInMethodIfSupported<testing::internal::UnitTestImpl, bool>(testing::internal::UnitTestImpl*, bool (testing::internal::UnitTestImpl::*)(), char const*) gtest.cc:2686
#17 0x00010300dbec in bool testing::internal::HandleExceptionsInMethodIfSupported<testing::internal::UnitTestImpl, bool>(testing::internal::UnitTestImpl*, bool (testing::internal::UnitTestImpl::*)(), char const*) gtest.cc:2722
#18 0x00010300d7e0 in testing::UnitTest::Run() gtest.cc:5617
#19 0x0001030ab9a4 in RUN_ALL_TESTS() gtest.h:2341
#20 0x0001030ab908 in main gtest_main.cc:64
#21 0x000196915d50 (<unknown module>)
on test cases test_utils, others have similar issues:
85% tests passed, 4 tests failed out of 26
Total Test time (real) = 42.12 sec
The following tests FAILED:
5 - test_utils (Subprocess aborted)
12 - test_ic3bits (Subprocess aborted)
14 - test_ic3sa (Subprocess aborted)
16 - test_cegar_ops_uf (Subprocess aborted)
Fix proposed
Simply reorder is fine, since there's no other operation between, delete at the end.
Issue Description
I was roughly going through some implementation in IC3 and the clear method
pono/engines/ic3base.cpp
Lines 73 to 82 in f41dd55
just don't feel right. Since when
pop(),priority_queue::pop()callsstd::pop_heap, which calls the comparatorpono/engines/ic3base.h
Lines 129 to 138 in f41dd55
But at this time, what stores in
_storehas already been deleted (_storeandqueue_share ownership of same raw pointers).Test
So in
--debugmode with a manually added-fsanitize=address, runASAN_OPTIONS=detect_container_overflow=0 make checkit indeed shows some errors such as:on test cases
test_utils, others have similar issues:Fix proposed
Simply reorder is fine, since there's no other operation between, delete at the end.