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

Vegard Nossum vegard.nossum at gmail.com
Mer 19 Jan 14:13:07 CET 2011

On 19 January 2011 12:22, Mate Soos <soos.mate at gmail.com> wrote:
> Hash: SHA1
> Dear All,
> I need a bit of your help. I have been putting quite some time to find a
> very strange bug in CryptoMiniSat, and I finally have found it, but I am
> not sure what to do with it. The problem was that gcc 4.5.X (4.5.1 for
> sure) seemed to miscompile CryptoMiniSat: the generated executable was
> behaving incorrectly. Through a 32-bit Fedora core 14 virtual machine I
> have traced the problem to this piece of code:
> inline const bool Solver::propNormalClause(Watched* &i, Watched* &j,
> Watched *end, const Lit p, PropBy& confl, const bool update)
> {
>    [..]
>    const uint32_t offset = i->getNormOffset();
>    Clause& c = *clauseAllocator.getPointer(offset);
>    // Make sure the false literal is data[1]:
>    if (c[0] == ~p) {
>        std::swap(c[0], c[1]);
>    }
>    assert(c[1] == ~p);
>    // If 0th watch is true, then clause is already satisfied.
>    if (value(c[0]).getBool()) {
>        printf("Zeroth watch is true\n");
>        j->setNormClause();
>        j->setNormOffset(offset);
>        j->setBlockedLit(c[0]);
>        j++;
>        return true;
>    }
>    // Look for new watch:
>    [..]
> The interesting part here is "std::swap(c[0], c[1])". The 'miscompiled'
> code indeed swaps c[0] and c[1], but then the check for value(c[0]) goes
> wrong: it actually checks c[1]'s value, as if the swap didn't take
> place. If we put in these code pieces:
> // Make sure the false literal is data[1]:
> const Lit lit2 = c.size()>2 ? c[2] : c[0];
> if (c[0] == ~p) {
>    std::swap(c[0], c[1]);
> }
> if (c.size() > 2) assert(lit2 == c[2]);
> then the compiled executable is correct (and, by the way, checks that
> c[2] hasn't been touched). This to me sounds very fishy. Furthermore,
> this "fix" seems to fix CryptoMiniSat for all problems. I.e. this is the
> only piece of 'miscompiled' code.

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).

More information about the Cryptominisat-devel mailing list