search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
817 stars 181 forks source link

solverconf invalid bool value #534

Closed Geremia closed 5 years ago

Geremia commented 5 years ago

I'm not sure if this is a Boost 1.69.0 issue, as I get:

/usr/include/boost/any.hpp:249:17: runtime error: downcast of address 0x604000000c50 which does not point to an object of type 'holder'
0x604000000c50: note: object is of type 'boost::any::holder<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >'
 07 00 00 57  d0 0b 79 d6 fa 7f 00 00  68 0c 00 00 40 60 00 00  06 00 00 00 00 00 00 00  69 6e 2e 63
              ^~~~~~~~~~~~~~~~~~~~~~~
              vptr for 'boost::any::holder<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >'

but there does seem to be some issue in solverconf:

/tmp/cryptominisat-master/src/solverconf.h:134:18: runtime error: load of value 89, which is not a valid value for type 'bool'

when it is reading in a large CNF of about 18million clauses. (The "89" is garbage, which changes between runs.)

GDB reports it gets stuck here:

#0  0x00007ffad56b35ed in __pthread_timedjoin_ex () from /lib64/libpthread.so.0
#1  0x00007ffad6648d43 in std::thread::join() () from /usr/lib64/libstdc++.so.6
#2  0x00007ffad895ce31 in ?? () from /usr/lib64/libcryptominisat5.so.5.6
#3  0x00007ffad895f4d0 in CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&) ()
   from /usr/lib64/libcryptominisat5.so.5.6
#4  0x000000000052aaf9 in DimacsParser<StreamBuffer<gzFile_s*, GZ> >::parse_DIMACS_main(StreamBuffer<gzFile_s*, GZ>&) ()
#5  0x000000000052e151 in bool DimacsParser<StreamBuffer<gzFile_s*, GZ> >::parse_DIMACS<gzFile_s*>(gzFile_s*, bool) ()
#6  0x000000000043949a in Main::readInAFile(CMSat::SATSolver*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) ()
#7  0x000000000043e92a in Main::parseInAllFiles(CMSat::SATSolver*) ()
#8  0x0000000000452363 in Main::solve() ()
#9  0x000000000042a814 in main ()

Memory usage keeps going up indefinitely the longer it runs, so it seems to be a leak.

Geremia commented 5 years ago

As of 065a0ce, leaks are detected:

$ /usr/include/boost/any.hpp:249:17: runtime error: downcast of address 0x604000000c10 which does not point to an object of type 'holder'
0x604000000c10: note: object is of type 'boost::any::holder<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >'
 01 00 80 3f  d0 db 6f 67 9b 7f 00 00  f0 79 00 00 30 60 00 00  14 00 00 00 00 00 00 00  14 00 00 00
              ^~~~~~~~~~~~~~~~~~~~~~~
              vptr for 'boost::any::holder<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >'
ERROR! Variable requested is far too large

=================================================================
==98904==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x7f9b6b1c6320 in __interceptor_realloc (/usr/lib64/libasan.so.5+0xe9320)
    #1 0x7f9b6758f2a2  (/usr/lib64/libstdc++.so.6+0x952a2)

Indirect leak of 32768 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b6770b145  (/lib64/libz.so.1+0x8145)

Indirect leak of 16384 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b67710be2  (/lib64/libz.so.1+0xdbe2)

Indirect leak of 8192 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b67710bd2  (/lib64/libz.so.1+0xdbd2)

Indirect leak of 7160 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b6770b4b5 in inflateInit2_ (/lib64/libz.so.1+0x84b5)

Indirect leak of 232 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b67710418  (/lib64/libz.so.1+0xd418)

Indirect leak of 21 byte(s) in 1 object(s) allocated from:
    #0 0x7f9b6b1c5f30 in malloc (/usr/lib64/libasan.so.5+0xe8f30)
    #1 0x7f9b67710502  (/lib64/libz.so.1+0xd502)

SUMMARY: AddressSanitizer: 65013 byte(s) leaked in 8 allocation(s).

Output:

c Outputting solution to console
c CryptoMiniSat version 5.6.6
c CMS Copyright Mate Soos (soos.mate@gmail.com)
c CMS SHA revision GIT-notfound
c CMS is MIT licensed
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -O2 -fPIC -g -fsanitize=address -fsanitize=undefined -fsanitize=leak -fno-stack-protector -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic -Wno-class-memaccess | COMPILE_DEFINES =  -DUSE_GAUSS -DNDEBUG -D_FORTIFY_SOURCE=0 -DLIMITMEM -DBOOST_TEST_DYN_LINK -DUSE_ZLIB | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND = TRUE | ENABLE_TESTING = OFF | M4RI_FOUND = FALSE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = OFF | PYTHON_EXECUTABLE = /usr/bin/python3 | PYTHON_LIBRARY = /usr/lib64/libpython3.6m.so | PYTHON_INCLUDE_DIRS = /usr/include/python3.6m | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = ON | compilation date time = Jan 19 2019 10:22:28
c CMS compiled with gcc version 8.2.0
c Executed with command line: cryptominisat5 -t 64 in_simplified.cnf.gz
c Reading file 'in_simplified.cnf.gz'
c -- header says num vars:         961856
c -- header says num clauses:     6355738
msoos commented 5 years ago

Hi,

First of all, thanks for the bug reports and I hope you are enjoying using CMS.

Unfortunately, Boost is known to be buggy with respect to address sanitizer. There are plenty of issues with it. They still haven't fix them. I have removed that particular option from CMS, but another option will probably show up. It's the way it is. Please talk to the Boost developers to fix the option parser :(

As for the memory leak -- I can't find it. Maybe it's an outdated/old/new/weird libz your are using? For my libz, there are no issues and I seem to be using libz correctly, i.e. according to the doc. So something may be off on your end? Please check again and if it still persists, maybe you can send me the input file that generated this? I cannot recreate the bug :(

Geremia commented 5 years ago

@msoos Yes, I think it did have to do with libz.