search

msoos / cryptominisat

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

sigsegv in CMSat::EGaussian::find_truths2 #558

Closed maxzinkus closed 5 years ago

maxzinkus commented 5 years ago

Attaching CNF file to repro.

c CryptoMiniSat version 5.6.8                                                                                                                                                    
c CMS Copyright Mate Soos (soos.mate@gmail.com)                                                                                                                                  
c CMS SHA revision 517503c0e0c25c33c4f9eb78fd58c8a1d0c7bcb1                                                                                                                      
c CMS is GPL licensed due to M4RI being linked. Build without M4RI to get MIT version                                                                                            
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14                                                                           
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,                                        
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 =  -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-dep
recated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdo
uble-promotion -Wshadow -Wformat=2 -pedantic | COMPILE_DEFINES =  -DUSE_GAUSS -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU -DUSE_M4RI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF 
| Boost_FOUND = 1 | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | NOM4RI = OFF | 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 | MY_TARGETS
 =  | LARGEMEM = OFF | LIMITMEM = OFF | compilation date time = May 26 2019 23:13:23                     
Program received signal SIGSEGV, Segmentation fault.
CMSat::EGaussian::find_truths2 (this=0x0, i=i@entry=0x5555562b21b0, j=@0x7fffffffd200: 0x5555562b21b0, p=p@entry=2057, row_n=0, gqd=...)
    at /home/ubuntu/cryptominisat/src/EGaussian.cpp:518
518         if ((*clauseIt)[row_n]) {
(gdb) list
513         PackedMatrix::iterator rowIt =
514             matrix.matrix.beginMatrix() + row_n; // gaussian watch invoke row
515         PackedMatrix::iterator clauseIt = clause_state.beginMatrix();
516
517         //if this clause is already satisfied
518         if ((*clauseIt)[row_n]) {
519             *j++ = *i; // store watch list
520             return true;
521         }
522
(gdb) bt
#0  CMSat::EGaussian::find_truths2 (this=0x0, i=i@entry=0x5555562b21b0, j=@0x7fffffffd200: 0x5555562b21b0, p=p@entry=2057, row_n=0, gqd=...)
    at /home/ubuntu/cryptominisat/src/EGaussian.cpp:518
#1  0x00007ffff7b2787d in CMSat::Searcher::Gauss_elimination (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/searcher.cpp:2877
#2  0x00007ffff7b27f46 in CMSat::Searcher::search (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/searcher.cpp:1238
#3  0x00007ffff7b2863f in CMSat::Searcher::solve (this=this@entry=0x55555580eb30, _max_confls=<optimized out>) at /home/ubuntu/cryptominisat/src/searcher.cpp:2362
#4  0x00007ffff7b44f24 in CMSat::Solver::iterate_until_solved (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/solver.cpp:1739
#5  0x00007ffff7b4544c in CMSat::Solver::solve_with_assumptions (this=0x55555580eb30, _assumptions=_assumptions@entry=0x7fffffffe310,
    only_sampling_solution=only_sampling_solution@entry=false) at /home/ubuntu/cryptominisat/src/solver.cpp:1510
#6  0x00007ffff7ba194a in calc (assumptions=assumptions@entry=0x7fffffffe310, solve=solve@entry=true, data=<optimized out>, only_sampling_solution=<optimized out>)
    at /home/ubuntu/cryptominisat/src/cryptominisat.cpp:799
#7  0x00007ffff7ba1c53 in CMSat::SATSolver::solve (this=<optimized out>, assumptions=assumptions@entry=0x7fffffffe310, only_sampling_solution=<optimized out>)
    at /home/ubuntu/cryptominisat/src/cryptominisat.cpp:839
#8  0x0000555555571d1a in Main::multi_solutions (this=this@entry=0x7fffffffd920) at /home/ubuntu/cryptominisat/src/main.cpp:1431
#9  0x0000555555573f93 in Main::solve (this=0x7fffffffd920) at /home/ubuntu/cryptominisat/src/main.cpp:1372
#10 0x000055555556f519 in main (argc=2, argv=0x7fffffffe498) at /home/ubuntu/cryptominisat/src/main_exe.cpp:46

Compressed the CNF because of the github limit of 10MB (it's 27MB unpacked). cmserror-11.cnf.txt.gz

msoos commented 5 years ago

Thanks so much! Can you please let me know what command line you used? Or was it just default command line? Thank you so much I'll fix it in 2-3 hours!!

Mate

On Tue, 28 May 2019, 16:51 Max Zinkus, notifications@github.com wrote:

Attaching CNF file to repro.

c CryptoMiniSat version 5.6.8 c CMS Copyright Mate Soos (soos.mate@gmail.com) c CMS SHA revision 517503c0e0c25c33c4f9eb78fd58c8a1d0c7bcb1 c CMS is GPL licensed due to M4RI being linked. Build without M4RI to get MIT version c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14 c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96, 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 = -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-dep recated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdo uble-promotion -Wshadow -Wformat=2 -pedantic | COMPILE_DEFINES = -DUSE_GAUSS -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU -DUSE_M4RI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | STATS = OFF | SQLITE3_FOUND = | ZLIB_FOUND = TRUE | VALGRIND_FOUND = | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | NOM4RI = OFF | SLOWDEBUG = 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 | MY_TARGETS = | LARGEMEM = OFF | LIMITMEM = OFF | compilation date time = May 26 2019 23:13:23

Program received signal SIGSEGV, Segmentation fault. CMSat::EGaussian::find_truths2 (this=0x0, i=i@entry=0x5555562b21b0, j=@0x7fffffffd200: 0x5555562b21b0, p=p@entry=2057, row_n=0, gqd=...) at /home/ubuntu/cryptominisat/src/EGaussian.cpp:518 518 if ((clauseIt)[row_n]) { (gdb) list 513 PackedMatrix::iterator rowIt = 514 matrix.matrix.beginMatrix() + row_n; // gaussian watch invoke row 515 PackedMatrix::iterator clauseIt = clause_state.beginMatrix(); 516 517 //if this clause is already satisfied 518 if ((clauseIt)[row_n]) { 519 j++ = i; // store watch list 520 return true; 521 } 522 (gdb) bt

0 CMSat::EGaussian::find_truths2 (this=0x0, i=i@entry=0x5555562b21b0, j=@0x7fffffffd200: 0x5555562b21b0, p=p@entry=2057, row_n=0, gqd=...)

at /home/ubuntu/cryptominisat/src/EGaussian.cpp:518

1 0x00007ffff7b2787d in CMSat::Searcher::Gauss_elimination (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/searcher.cpp:2877

2 0x00007ffff7b27f46 in CMSat::Searcher::search (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/searcher.cpp:1238

3 0x00007ffff7b2863f in CMSat::Searcher::solve (this=this@entry=0x55555580eb30, _max_confls=) at /home/ubuntu/cryptominisat/src/searcher.cpp:2362

4 0x00007ffff7b44f24 in CMSat::Solver::iterate_until_solved (this=this@entry=0x55555580eb30) at /home/ubuntu/cryptominisat/src/solver.cpp:1739

5 0x00007ffff7b4544c in CMSat::Solver::solve_with_assumptions (this=0x55555580eb30, _assumptions=_assumptions@entry=0x7fffffffe310,

only_sampling_solution=only_sampling_solution@entry=false) at /home/ubuntu/cryptominisat/src/solver.cpp:1510

6 0x00007ffff7ba194a in calc (assumptions=assumptions@entry=0x7fffffffe310, solve=solve@entry=true, data=, only_sampling_solution=)

at /home/ubuntu/cryptominisat/src/cryptominisat.cpp:799

7 0x00007ffff7ba1c53 in CMSat::SATSolver::solve (this=, assumptions=assumptions@entry=0x7fffffffe310, only_sampling_solution=)

at /home/ubuntu/cryptominisat/src/cryptominisat.cpp:839

8 0x0000555555571d1a in Main::multi_solutions (this=this@entry=0x7fffffffd920) at /home/ubuntu/cryptominisat/src/main.cpp:1431

9 0x0000555555573f93 in Main::solve (this=0x7fffffffd920) at /home/ubuntu/cryptominisat/src/main.cpp:1372

10 0x000055555556f519 in main (argc=2, argv=0x7fffffffe498) at /home/ubuntu/cryptominisat/src/main_exe.cpp:46

Compressed the CNF because of the github limit of 10MB (it's 27MB unpacked). cmserror-11.cnf.txt.gz https://github.com/msoos/cryptominisat/files/3228222/cms_error_-11.cnf.txt.gz

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/558?email_source=notifications&email_token=AAKF4OPY6JJV6NIBF6TEJGDPXVBFHA5CNFSM4HQEGXDKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4GWIAQOA, or mute the thread https://github.com/notifications/unsubscribe-auth/AAKF4OPNNOGPQ6HIMQVHBPLPXVBFHANCNFSM4HQEGXDA .

maxzinkus commented 5 years ago

Repros with cryptominisat5 input.cnf and also cryptominisat5 --maxxorsize 8 --maxnummatrixes 100 input.cnf Thanks again!

msoos commented 5 years ago

Sorry, I am really confused, I was an idiot, I wrote a comment yesterday and forgot to send you. Please don't use the devel branch. Please use the master branch. It is probably even faster than the devel. It should have none of these issues. If it still does, please re-open the issue! :) Thanks!

maxzinkus commented 5 years ago

This issue is still an issue in the devel branch and thus should probably stay open, right?

Either way, I can't switch now because I have long-running tests executing.

msoos commented 5 years ago

Oh shit

msoos commented 5 years ago

Oh, okay, I will fix, but I thought you were using the master branch, sorry. I will fix this 517503c0e0c25c33c4f9eb78fd58c8a1d0c7bcb1, create a devel-good and please stick to that and that only. I see that you have been updating to latest because 517503c0e0c25c33c4f9eb78fd58c8a1d0c7bcb1 only came out 1 day ago, so please do not use devel any longer :) I will make a devel-good and please stick to that and that only. Note that master had the fix for the bug you found that blocked you (the segfault, thanks so much for that!) as soon as devel had it :) So master is always the best to use under normal conditions. I will now fix this and push devel-good and close this issue. Please do not switch away from that. Let me now fix this thing.... :)

maxzinkus commented 5 years ago

No need to create a new branch, we'll switch back to master as soon as both your updates are merged and our current tests are done.

msoos commented 5 years ago

Oh... wait, you refer to "both" updates. What do you mean by that? I though that master is now good? I only know of one update, bug #552 That has already been merged to master, so it should be okay -- but you mention two? What is the other one?

maxzinkus commented 5 years ago

Sorry, poor phrasing. The "both" referred to 1) your update and 2) our tests finishing

msoos commented 5 years ago

Damn, I think this affects master too :D Good catch! Thanks, fixing :)

msoos commented 5 years ago

First, an apology is in order. This is indeed a bug and now I will be working very hard to make sure that I can fuzz this kind of issue. The problem is that you have multiple matrices and this has not been fuzzed. So you bumped into 3 separate problems regarding this: #552, #557 and this. I am extremely sorry that you had such a bad experience. All 3 are completely valid and affect every branch. So, it was very valuable that you reported to me, thank you so much! I have now fixed this and #557. I will think about how to fuzz thing thing. To be honest, I would very much welcome your problem generator, because it seems to spit out amazingly good problems that I cannot seem to generate. All my generators have a single matrix, and all 3 bugs you found were about multiple matrices interacting.

As a thank-you, I have put your name and a thank you note into both commits. Thank you so much.

So both this and #557 are now solved.

msoos commented 5 years ago

Please let me know if this or anything like this re-occurs. This should now be solved in both devel and master.

I usually fuzz this thing to hell and it's extremely rare to have any bugs. But I didin't fuzz multi-matrix :( Sorry and thank you again for your patience.