Assertion '__builtin_expect(__n < this->size(), true)' failed.

[jwaldmann]

Hi, with cadical-1.3.0 (as packaged for Fedora 33 GNU/Linux) I am getting

/usr/include/c++/10/bits/stl_vector.h:1045: std::vector<_Tp, _Alloc>::reference std::vector<_Tp, _Alloc>::operator[](std::vector<_Tp, _Alloc>::size_type) [with _Tp = CaDiCaL::Level; _Alloc = std::allocator<CaDiCaL::Level>; std::vector<_Tp, _Alloc>::reference = CaDiCaL::Level&; std::vector<_Tp, _Alloc>::size_type = long unsigned int]: Assertion '__builtin_expect(__n < this->size(), true)' failed.

when called with no arguments (with --sat it's fine)

testcase.log
testcase.cnf.txt

Looks identical to msoos/cryptominisat#643

[arminbiere]

Thanks!

As @msoos figured out in msoos/cryptominisat#643 this is detected by adding the -Wp,-D_GLIBCXX_ASSERTIONS compiler flag.

Then fuzzing with 'mobical' would immediately find small traces like this one:

0 init
1 add -4
2 add 3
3 add 0
4 add -6
5 add -1
6 add 4
7 add 0
8 add -3
9 add 0
10 add -6
11 add -5
12 add 2
13 add 0
14 add -2
15 add 0
16 simplify 5 0

This is also in the latest release (1.4.0) which is used for the SAT competition CaDiCaL Hack track.

0 init
1 add 2
2 add 3
3 add 4
4 add 0
5 add -4
6 add 0
7 add 5
8 add -1
9 add 2
10 add 0
11 simplify 5 0

I can also confirm that the issue is not found by ASAN with other extensive testing I do.

[arminbiere]

In vivification, the code which tries to reuse decisions for a new clause to be vivified assumed that there was at least one decision left from the last try, i.e., the decision level is (still) non-zero. This is not the case in general though, and thus it might happen that the control strack (which has the same size as the number of decisions plus one) shrinks to just the root-level frame, in which case the search starting at decision level one accesses an element of that control stack which was just popped.

So the 'std::vector' shrinks from size 2 to size 1 and then accessing it at position 1 is correctly an out-of-bound access, but apparently the STL implementation of 'std::vector' neither moved the array nor used realloc or something (which is the sane thing to do when shrinking a vector from 2 to 1). So that was (correctly) not detected by ASAN nor 'valgrind', but in principle could lead to a real issue since it violates STL 'std::vector' semantics (as complex they are). The contract checker for STL enabled with -Wp,-D_GLIBCXX_ASSERTIONS catches this.

For now I keep the fix on the development branch (and make it nicer when adding it to the next release). I will add -Wp,-D_GLIBCXX_ASSERTIONS to pedantic mode compilation to make sure such contract violations do not slip through in the future.

[arminbiere]

Merged with sc2021 version.