[Cryptominisat-devel] I need a bit of help debugging CryptoMiniSat

Mate Soos soos.mate at gmail.com
Mer 19 Jan 18:29:02 CET 2011

Hash: SHA1

Dear Vergard,

On 01/19/2011 06:14 PM, Vegard Nossum wrote:
> On 19 January 2011 14:13, Vegard Nossum <vegard.nossum at gmail.com> wrote:
>> On 19 January 2011 12:22, Mate Soos <soos.mate at gmail.com> wrote:
>> Here's my best tip for the moment: Try to find a minimal test-case
>> that exhibits the bad behaviour.
>> So for example, in this case, I would create a new file (with a new
>> main()) and copy some of the relevant classes, for example Clause and
>> Lit. Also copy Solver::propNormalClause() and make it a regular
>> function that you can call from main() with some dummy arguments --
>> make sure you can reproduce the bug in this "controlled" environment
>> (i.e. not using the full solver).
>> From this point you should still be able to remove a lot of things,
>> like unused functions, etc. When you have the minimal test-case it
>> should be pretty easy to tell whether it's a code bug or a gcc bug. At
>> least you have eliminated a lot of things and somebody could finally
>> say: "Ah, but strict aliasing makes GCC cache the value of c[0] in a
>> register because it cannot possibly [...]"
>> I'll give it a try too :-)
> I created a new Main.cpp which defines a new class Solver2, which is
> MUCH smaller than the regular Solver. It uses Var, Lit, vec, and
> ClauseAllocator from the other files, so the next step is to eliminate
> those as well. So you see this new file also demonstrates the same
> problem, but with a much simpler program now. This is the output:
> $ for o in 0 3; do echo -n "-O$o: "; g++ -Wall -O$o -ISolver -Imtl
> -IMTRand -o test Main.cpp Solver/ClauseAllocator.cpp && ./test; done
> -O0: success
> -O3: error

All I can say is: WOW :) I've spent a whole day to isolate the problem
from 13'000 LOC to a couple of lines in a function and all its
dependencies, and you have managed to isolate it down to maybe only
1-200 LOC in just a couple of hours! The way this goes, the bug will be
squashed today :) I am so looking forward to CryptoMS 2.9.0, finally
without bugs ;)

I will work on this right now,



- -- 
Mate Soos
Security Research Labs
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/


More information about the Cryptominisat-devel mailing list