marijnheule / drat-trim Goto Github PK

on line 1243 of drat_trim.c, should the "(int)" be "(long)", like lines 1218 and 1212? This caused a segfault when verifying a proof for a sat instance.

Parsing the trivially unsat formula (only the empty clause) triggers a buffer overflow in the parser.

On my machine (Ubuntu GLIBC 2.23-0ubuntu5 on x86_64), drat-trim segfaults when trying to dereference NULL, but C-standard also allows other behaviors, depending on the implementation of realloc.

Analysis:
The parser buffer is initialized to 2*nVar, which happens to be 0. Thus, also buffer resizing in l. 931 has no effect. Nevertheless, the terminating zero is written to the zero-sized buffer in l. 941.

See also #5 , which also seems to be caused by illicit parser buffer management.

On my machine, the realloc in l. 932 returns NULL, such that the "pivot=buffer[0]" in l. 940 segfaults. But C standard would also allow realloc to actually return a non-null pointer, such that this bug may never be triggered on some machines, or have different symptoms.

f9.zip

drat-trim full1.cnf full1.drat -C -L full1.lrat
outputs an ASCII(!) lrat proof, though the -C option should have selected binary. In most cases, -C will output a binary proof.

This could be related to the following:
c found complementary unit clauses: -1

which in https://github.com/marijnheule/drat-trim/blob/master/drat-trim.c#L752 takes a shortcut, without respecting
the S->binOutput flag.

full1.cnf
p cnf 1 2
1 0
-1 0

CNF:

p cnf 1 2
c hello world
1 0
-1 0

proof:

3 0 1 2 0

causes lrat-check to produce

c parsed a formula with 1 variables and 2 clauses
c ERROR: using DELECT clause

because the comment is not parsed correctly.

This interferes with most modern IDEs (as they expect the system to build with C++ as well), making it nearly impossible to understand or improve the code.

Not sure if it is important or not.. but a strange warnings issued by drat-trim.
These CNF and PROOF files: https://yurichev.com/tmp/drat-trim-issue/

Running: ./drat-trim SAT_lib.factor.cnf SAT_lib.factor.proof

c turning on binary mode checking
c parsing input formula with 2949 variables and 16465 clauses
c WARNING: detected and deleted duplicate literal -1 at position 2 of line 16466
c WARNING: detected and deleted duplicate literal 1 at position 2 of line 16470
c WARNING: detected and deleted duplicate literal -1 at position 1 of line 16475
c WARNING: detected and deleted duplicate literal 1 at position 2 of line 16478
c finished parsing, read 7896429 bytes from proof file
c detected empty clause; start verification via backward checking
c 8629 of 16465 clauses in core
c 52635 of 294627 lemmas in core using 6846566 resolution steps
c 0 RAT lemmas in core; 33702 redundant literals in core lemmas
s VERIFIED
c verification time: 4.806 seconds

OK, but there are only 16466 lines in the SAT_lib.factor.cnf file.
drat-trim issues warnings about lines >=16470.

The newest version works for me again (internal regression testing with Kissat etc.) but only
for proofs. Forward checking which should be useful for debugging (and testing) of satisfiable
formulas seems to be broken. Here is a delta-debugged example.

$ cat bug.cnf
p cnf 3 3
-2 -3 0
2 -3 0
3 -1 0
$ cat bug.proof
-1 0
-3 0
$ drat-trim bug.cnf bug.proof -S
c parsing input formula with 3 variables and 3 clauses
c WARNING: 5 clauses active if proof succeeds
c [8] -1 0
c [5] -3 2 0
c [10] -3 0
c [3] -3 -2 0
c [7] -1 3 0
c finished parsing
c WARNING: RAT check on proof pivot failed : [11] -3 0
c RAT check failed on all possible pivots
c failed at proof line 5 (modulo deletion errors)

s NOT VERIFIED
c verification time: 0.055 seconds

In most of the instances, there seems to be clauses in the trace check file that are not in the proof ( neither in the lemmas nor in the formula ).

Here is what I did :
I ran glucose 4.1 on an unsat formula (test.txt) and produced a proof (test-proof.txt)
I ran drat trim on the proof and generated the trace check output file (test-traceFile.txt)

I can find clauses like -233 244 -263 in the trace check file whereas I cannot find the clause neither in the proof produced by glucose nor in the cnf file.

However, I can find a clause -233 244 -263 -261 in the proof which is very similar to this one.

test.txt

test-proof.txt

test-traceFile.txt

The formula is from SAT competition 2016. It was originally named modgen-n200-m90860q08c40-12992.cnf
I find that this happens very often in other formulas as well.

BUG. Buffer overflow, may perhaps cause undetected erroneous behaviour of checker.

When drat-trim detects duplicate literals, it prints a warning that it "detected and deleted" the duplicate literal. However, the implementation of doing so is flawed, and seems to cause memory being overwritten.
The attached example coredumps on my linux x86_64 box with "free(): invalid next size (fast): 0x0000000002512890 ***"
f8.zip

The proof generated by CaDiCaL on the instance 'baseballcover15with25' from the SAT Competition 2020 fails to check in the current commit. That same proof is checked correctly with commit #d13f761fbdacd052429f14421f95a7e8cd75deb1

The code contains no tests whatsoever. This system is supposed to give some form of guarantee that the solution is correct. However, it doesn't have any form of checking that it is in fact correct. Note that the entire system contains 4 assert-s.

BUG. Allows SAT formulas being certified as UNSAT

The parser erroneously interprets the last part of a comment line that exceeds 1024 characters as being part of the formula. If one is lucky, this only yields spurious syntax errors, if one is unlucky the comment contains numbers that are then interpreted as clauses!

f7.zip

I have a DIMACS format file that starts

c p cnf 3560 69469
c clauses found (binary, tautologies, nonbinary): 69469 = 668 + 0 + 68801
p cnf 648 668

The initial comment line, however, is treated as the "p cnf 3560 69469" line, leading DRAT-trim to ignore the actual "p cnf" line two lines later, and to complain about not enough clauses being present.

Workaround: Strip out all comment lines from the INPUT file before feeding it to DRAT-trim.

lrat-check seg faults on a LRAT proof generated through drat-trim from MapleLCMDistChronoBT from SAT Comp 18 on the benchmark queen13_13.col.13.cnf. The LRAT file is 8.7 GB. The error is caused by an integer overflow of tableAlloc in line 146.

The quick fix is to change tableAlloc and tableSize to size_t. Also the realloc is not checked.

This system should to be hooked up to a Linux, Mac and Windows build pipeline so that it can surely be compiled under and used in these systems.

For apparently any formula, lrat-check will accept a proof where the empty clause has an empty proof hint. For example,

99999999 0 0

is apparently a universal proof. It also accepts the empty clause with an empty proof at the end of an otherwise valid proof file, not just as the first line.

There are three obstacles to cross platform / older standards compilation:

• Dependency on <sys/time.h>

• Use of getc_unlocked.
  I redefine it:
  #define getc_unlocked _fgetc_nolock

• I use int* sortClause = (int*) malloc(sizeof(int)*S->maxSize);
  instead of int sortClause[S->maxSize];

Tracing back verifier failures to origins could be improved by using line numbers that correspond to lines in the output. Currently the numbers in brackets are indirectly related to clause locations

Hi, I'm wondering if it's possible to validate parts of the DRAT proof, or only 1 of the clause from the proof, to see if it cause conflict.
First I tried deleting one of the clauses inside the DRAT proof for a UNSAT problem. It shows verified without running '-f', and NOT Verified if running with '-f' as option.

Then I tried adding 1.one clause (not deleted) from the proof to a SATISFIABLE problem, 2. The second time I tried adding its negation.
both shows:

c WARNING: RAT check on proof pivot failed : [63593] 869 6198 6718 7658 8954 0
c RAT check failed on all possible pivots
c failed at proof line 7647 (modulo deletion errors)

s NOT VERIFIED

Also I tried adding 1. one clause from the proof to a UNSAT problem. 2. its negation. Both shows the same except one has 15 clauses in core.

c parsing input formula with 13176 variables and 345426 clauses
c finished parsing
c start forward verification
c 16 of 345426 clauses in core
c 1 of 2 lemmas in core using 16 resolution steps
c 0 RAT lemmas in core; 0 redundant literals in core lemmas
c optimized proofs are not supported for forward checking
c VERIFIED derivation: all lemmas preserve satisfiability
c WARNING: no empty clause detected, this is not a refutation
s DERIVATION
c verification time: 0.295 seconds

Am I understanding anywhere incorrectly? Or is the function only available for full refutation check?
Thank you so much!

I think it'd be very convenient if drat-trim could handle both .cnf.gz and .drup.gz files. A possibility would be to try and spawn gunzip -k --stdout the_file.{cnf,drup}.gz and read from the file descriptor, to not even have to depend on zlib at all.

Hi there,

I'm interested in using drat-trim via a C++ API. Is this something you'd be willing to provide in the near future? If not, would you be open to a PR creating such an API?

Cheers,
Alex

Even though all modern SAT solvers open zipped files and most CNFs are stored gzipped due to space constraints.

This is slightly strange, given that the system has a binary mode where the proof is efficiently stored. However, the CNF is still expected to be read in plain.

BUG. Allows SAT formulas being certified as UNSAT.

Although it is documented that variable numbers must be less than 2^31, drat-trim silently overflows on big variable numbers, erroneously identifying different variables.

Suggestion to fix: Terminate with error message, instead of silently overflowing.

f4.zip

Perhaps:

if (tmp == 0 && **!S->binMode**) {
     char ignore[1024];
     if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) printf ("c\n"); }
    ... etc
}

The system contain 4 assert() calls. That is very little. There should be more self-checking. This system is supposed to give guarantees to system builders.

Line

Misses NULL check for return value.

./drat-trim fuzzTest_33.cnf fuzzTest_33.cnf-drat

gives:

c parsing input formula with 53 variables and 116 clauses
c ERROR: comment longer than 1024 characters: a2Rf\Z`bdT

By forcing the binary mode (only possible via hacking the code...):

../../build/tests/drat-trim/drat-trim  out/fuzzTest_33.cnf out/fuzzTest_33.cnf-drat
c parsing input formula with 53 variables and 116 clauses
c finished parsing, read 1203958 bytes from proof file
c detected empty clause; start verification via backward checking
c 116 of 116 clauses in core                            
c 44292 of 55206 lemmas in core using 740218 resolution steps
c 0 RAT lemmas in core; 11329 redundant literals in core lemmas
s VERIFIED
c verification time: 1.386 seconds

This was found using an extensive fuzzer that I built to fuzz CMS. Unfortunately/fortunately, it found a bug in DRAT instead :S

drat.zip

Can we have a force-binary mode please? Also, what is the bug about? I can't seem to wrap my head around it. The detector seems to be wrong. The hexdump seems OK and starts with the right character ("a"):

hexdump -C out/fuzzTest_33.cnf-drat | head
00000000  61 32 52 66 5c 5a 60 62  64 54 02 00 61 08 49 6a  |a2Rf\Z`bdT..a.Ij|
00000010  1a 56 68 62 5a 3d 00 61  49 3d 6a 68 1a 56 5a 62  |.VhbZ=.aI=jh.VZb|
00000020  64 54 02 00 61 10 52 5a  54 62 64 60 02 66 6a 68  |dT..a.RZTbd`.fjh|
00000030  56 0b 58 5c 00 61 52 54  68 5c 6a 56 02 5a 58 62  |V.X\.aRTh\jV.ZXb|
00000040  64 60 66 5e 00 61 30 1a  56 68 49 41 6a 00 61 1a  |d`f^.a0.VhIAj.a.|
00000050  05 41 6a 56 49 62 64 54  68 00 61 05 41 68 6a 56  |.AjVIbdTh.a.AhjV|
00000060  49 62 64 54 02 5e 16 00  61 41 16 68 5e 6a 02 56  |IbdT.^..aA.h^j.V|
00000070  54 49 64 62 5a 53 00 61  18 40 02 54 5a 64 62 00  |[email protected].|
00000080  61 2a 2e 53 5a 16 40 5e  02 54 00 61 3c 54 5e 02  |a*.SZ.@^.T.a<T^.|
00000090  53 5a 62 64 68 6a 56 66  58 5c 00 61 1a 41 68 56  |SZbdhjVfX\.a.AhV|

I'm trying to convert DRAT proof produced by Kissat to LRAT to see if it can be verified in ACL2.
Am I doing this right?

unsat1.cnf:

p cnf 1 2
1 0
-1 0

Running:

% kissat unsat1.cnf unsat1.drat

% xxd -g 1 unsat1.drat
00000000: 61 00 61 00 64 03 00                             a.a.d..

Attempting to generate LRAT proof from DRAT proof.
Am I doing this right?

% ./drat-trim unsat1.cnf unsat1.drat -l unsat1.lrat
c turning on binary mode checking
c parsing input formula with 1 variables and 2 clauses
c WARNING: backward mode ignores deletion of (pseudo) unit clause [0] -1 0
c finished parsing, read 7 bytes from proof file
c found complementary unit clauses: -1
s VERIFIED
c verification time: 0.143 seconds

unsat1.lrat:

0

Running:

% ./lrat-check unsat1.cnf unsat1.lrat
c parsed a formula with 1 variables and 2 clauses
c Added clauses = 2.  Deleted clauses = 0.  Max live clauses = 2
c verification time = 0.00 secs

Trying to verify LRAT proof in ACL2:

% cd /home/i/Downloads/acl2/books/projects/sat/lrat/stobj-based

% ./run.sh ~/Downloads/drat-trim/unsat1.cnf ~/Downloads/drat-trim/unsat1.lrat

Stdout:

s FAILED
  (see /home/i/Downloads/drat-trim/unsat1.out)

unsat1.out:

HARD ACL2 ERROR in VALID-PROOFP$-TOP:  Invalid proof!

The following input causes lrat-check to not terminate:

input:

p cnf 0 1
0

proof: empty

The following input causes lrat-check to terminate with SIGABRT:

input:

p cnf 2 2
1 0
2 -1 0

proof:

3 2 0 1 2 0

I am getting

==10348== Invalid read of size 4
==10348==    at 0x10F085: parse (in /usr/local/bin/drat-trim)
==10348==    by 0x10943A: main (in /usr/local/bin/drat-trim)
==10348==  Address 0xc0af7bc is 4 bytes before a block of size 112 alloc'd
==10348==    at 0x4839D7B: realloc (vg_replace_malloc.c:826)
==10348==    by 0x10E95E: parse (in /usr/local/bin/drat-trim)
==10348==    by 0x10943A: main (in /usr/local/bin/drat-trim)

Input CNF and DRAT attached.
out.zip

Run as:

valgrind drat-trim out/fuzzTest_66.cnf out/fuzzTest-drat_43.cnf

This seems to be because of clause[ID], where ID is -1, which means we are 4 bytes before the malloc boundary (int is 4 bytes on this architecture), as warned by valgrind: Address 0xc0af7bc is 4 bytes before a block of size 112 alloc'd.

I am very confused why ID needs to be -1. Please try to fix before the SAT Race so that valid solvers don't get disqualified :) Thanks!