msoos / cryptominisat

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

Uninitialised memory warnings with clang 4, valgrind 3.10.1 #393

Closed TrevorHansen closed 7 years ago

TrevorHansen commented 7 years ago

I'm getting some unitialised memory warnings when I run cryptominsat. I'm not getting any memory leaks. For example, on the attached CNF, I get the below warning (plus others). I've looked at the code, but can't see anything wrong. Perhaps these are false alarms because the bitfields?

==25256== Conditional jump or move depends on uninitialised value(s) ==25256== at 0x4E61972: recalc_abst_if_needed (clause.h:321) ==25256== by 0x4E61972: CMSat::OccSimplifier::link_in_clauses(std::vector<unsigned int, std::allocator > const&, bool, unsigned int, long) (occsimplifier.cpp:489) ==25256== by 0x4E66CC5: CMSat::OccSimplifier::fill_occur() (occsimplifier.cpp:1049) ==25256== by 0x4E658CB: CMSat::OccSimplifier::fill_occur_and_print_stats() (occsimplifier.cpp:851) ==25256== by 0x4E67D86: CMSat::OccSimplifier::setup() (occsimplifier.cpp:981) ==25256== by 0x4E67E1C: CMSat::OccSimplifier::simplify(bool, std::string) (occsimplifier.cpp:992) ==25256== by 0x4EA0D8F: CMSat::Solver::execute_inprocess_strategy(bool, std::string const&) (solver.cpp:1645) ==25256== by 0x4E9D206: CMSat::Solver::simplify_problem(bool) (solver.cpp:1801) ==25256== by 0x4E9D6A9: CMSat::Solver::solve() (solver.cpp:1299) ==25256== by 0x4EE6701: solve_with_assumptions (solver.h:431) ==25256== by 0x4EE6701: calc(std::vector<CMSat::Lit, std::allocator > const, bool, CMSat::CMSatPrivateData) (cryptominisat.cpp:637) ==25256== by 0x414F2E: Main::multi_solutions() (main.cpp:1225) ==25256== by 0x4147E7: Main::solve() (main.cpp:1199) ==25256== by 0x42AEEA: main (main_exe.cpp:46)

==25256== Uninitialised value was created by a heap allocation ==25256== at 0x4C2AB80: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==25256== by 0x4C2CF1F: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==25256== by 0x4E770BF: CMSat::ClauseAllocator::allocEnough(unsigned int) (clauseallocator.cpp:109) ==25256== by 0x4E98F45: Clause_new<std::vector<CMSat::Lit, std::allocator > > (clauseallocator.h:67) ==25256== by 0x4E98F45: CMSat::Solver::add_clause_int(std::vector<CMSat::Lit, std::allocator > const&, bool, CMSat::ClauseStats, bool, std::vector<CMSat::Lit, std::allocator >, bool, CMSat::Lit) (solver.cpp:452) ==25256== by 0x4E99F6C: CMSat::Solver::addClause(std::vector<CMSat::Lit, std::allocator > const&, bool) (solver.cpp:671) ==25256== by 0x4EE5EB8: CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator > const&) (cryptominisat.cpp:494) ==25256== by 0x41C20D: DimacsParser<StreamBuffer<gzFile_s, GZ> >::parse_and_add_clause(StreamBuffer<gzFile_s, GZ>&) (dimacsparser.h:379) ==25256== by 0x41B0A0: DimacsParser<StreamBuffer<gzFile_s, GZ> >::parse_DIMACS_main(StreamBuffer<gzFile_s, GZ>&) (dimacsparser.h:451) ==25256== by 0x415BCB: bool DimacsParser<StreamBuffer<gzFile_s, GZ> >::parse_DIMACS<gzFile_s>(gzFile_s) (dimacsparser.h:469) ==25256== by 0x407153: Main::readInAFile(CMSat::SATSolver, std::string const&) (main.cpp:128) ==25256== by 0x4075DE: Main::parseInAllFiles(CMSat::SATSolver) (main.cpp:191) ==25256== by 0x4147DF: Main::solve() (main.cpp:1196) ==25256==

./cryptominisat5 --version c CryptoMiniSat version 5.0.1 c CryptoMiniSat SHA revision f5044d5b24c5a25eec23a8f7f50ad909297f2ed5 c CryptoMiniSat compilation env CMAKE_CXX_COMPILER = /usr/bin/clang++ | CMAKE_CXX_FLAGS = -std=c++11 -g -pthread -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wheader-guard -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 -fPIC | COMPILE_DEFINES = -DUSE_PTHREADS -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DUSE_M4RI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | TBB_FOUND = | STATS = OFF | MYSQL_FOUND = | SQLITE3_FOUND = | ZLIB_FOUND = TRUE | VALGRIND_FOUND = TRUE | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = /usr/bin/python2.7 | PYTHON_LIBRARY = /usr/lib/x86_64-linux-gnu/libpython2.7.so | PYTHON_INCLUDE_DIRS = /usr/include/python2.7;/usr/include/x86_64-linux-gnu/python2.7 | MY_TARGETS = | LIMITMEM = OFF | compilation date time = Apr 27 2017 14:42:32 c compiled with gcc version 4.2.1 Compatible Clang 4.0.0 (branches/release_40)

output_0.cnf.txt

msoos commented 7 years ago

I've checked with gcc+valgrind, it's not there. I'm checking clang+valgrind, it's not there either until now. Are we talking about the current git HEAD? Or is it 5.0.1?

Note: I'm not using STP to do this, I'm using CryptoMiniSat+its fuzzing system I built. The fuzzer extensively checks the library usage, but STP may be using it differently. The issue I had with using valgrind on STP though is that it used to emit so much stuff that was clearly unrelated to CMS that I gave up on that. Have you been fixing STP? I have fixed a bunch of memory leaks in STP and I think we have been improving it over time. I'll check it out, maybe I can find what you are talking about.

So all in all: I'm on this and I'll both try finding it CMS and also in STP+CMS in case STP's valgrind issues don't down out CMS issues.

Thanks again for the report, I'm on it :)

msoos commented 7 years ago

Sorry, I couldn't reproduce it. Can you please give me an example? Like a fuzz example of STP that did that? Thanks!

TrevorHansen commented 7 years ago

Hi Mate,

Thanks for investigating!

I'm running cryptominisat on a CNF, I think it's unrelated to STP. A CNF is hidden down the bottom of my first comment.

I've tried with Valgrind 3.12.0, and Valgrind 3.10.1, both report the warning. So it seems related to clang 4, as mentioned maybe because of the bit-fields.

I'm using Ubuntu 14, and have installed clang 4 via llvm's packages here: deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-4.0 main

When I check the version, it gives:

$ clang --version
clang version 4.0.0-svn297204-1~exp1 (branches/release_40)

I'm not handy with Clang, it seems like a legitimate release version?

I'm building from what I think is the trunk:

$./cryptominisat5 --version
c CryptoMiniSat version 5.0.1
c CryptoMiniSat SHA revision bdcb312cfafece76e5434e95489dc28c0e663ec8
c CryptoMiniSat compilation env CMAKE_CXX_COMPILER = /usr/bin/clang++ | CMAKE_CXX_FLAGS =  -std=c++11 -g -pthread -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wheader-guard -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 -fPIC | COMPILE_DEFINES =  -DUSE_PTHREADS -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DUSE_M4RI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | TBB_FOUND =  | STATS = OFF | MYSQL_FOUND =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND = TRUE | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = /usr/bin/python2.7 | PYTHON_LIBRARY = /usr/lib/x86_64-linux-gnu/libpython2.7.so | PYTHON_INCLUDE_DIRS = /usr/include/python2.7;/usr/include/x86_64-linux-gnu/python2.7 | MY_TARGETS =  | LIMITMEM = OFF | compilation date time = May  2 2017 11:24:39
c compiled with gcc version 4.2.1 Compatible Clang 4.0.0 (branches/release_40)
msoos commented 7 years ago

Ah, I see the CNF, thanks! Sorry, today I spent my whole evening fixing #389 so CMS can run on instances for years instead of days. Some people need it, so I had to do it. I'll be looking at this issue tomorrow. Stay tuned!

Thanks for pointing out the CNF, I was blind. I'll be checking with it. Your suspicion is probably right, I have seen newer clang and newer valgrind both show up new issues. It's possible they are real issues, but probably not, as all my testing in my current environment (valgrind-3.10.0 + clang 3.5.0-10) and other ones (gcc 4.9.2) were OK. I'll look at this tomorrow. Thanks again!

msoos commented 7 years ago

I use Debian, and the clang 4.0 install deb packages are broken for Debian. So I either have to build clang or get e.g. a 16.04 LTS (Xenial Xerus) virtual machine. I think I'll do the latter. It's got "3.11.0-1ubuntu4" valgrind. That should do the trick :) I'll do it this weekend, I'm a bit showered with stuff and I still need to fix the Windows&Linux build for STP.

msoos commented 7 years ago

OK, I'm on to this :) Thanks, seem legit actually, which is a bit shocking. There was no way of getting this with anything else. But once i installed Ubuntu 17.04 in a virtual environment and built the testing system, I could generate an instance that has errors with valgrind really quick. I'm on this :)

msoos commented 7 years ago

I think it's simply wrong. However, I have fixed it, with a memset before placement new. It's a bit slower, zeroing out the memory space, but it's definitely correct, and to me it indicates either of 2 things:

I am willing to say that it could be no. 2 so I'm memsetting before constructing. I could memset the whole memory area after realloc, but that way, we would not pick up some real errors.

TrevorHansen commented 7 years ago

Thanks Mate! I've retested, I'm not getting the warnings any more. It all looks good now.