[klee-dev] Bool vs i1 in STPBuilder

[Alastair Reid]

I am trying to chase down a bug that occurs while applying KLEE to a
multi-module Rust program (assembly.ll is approx 200k lines).
I'm hoping for suggestions of what might be wrong and/or how to narrow down
the cause of the bug.

What I am seeing in the stack trace is
that klee::STPBuilder::constructActual calls vc_bvConcatExpr (in STP) which
calls stp::checkChildrenAreBV which prints an error message and dies.
The error message involves a very large term but the start of it is as
follows (I have bold-faced the top two levels of the term)

The type is: 0
Fatal Error: BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors

*14808:(BVCONCAT*
*  14806:(BVSGT*
    988:0x00
    14798:(ITE
    ....))

*  14774:(BVSGT*    988:0x00
    14766:(ITE
      14760:(EQ
        14724:(READ
          [14720]
          14386:(BVEXTRACT
            [14380]
            13594:0x0000001F
            60:0x00000000))
        [14758])
      14406:0xFF
      988:0x00)))
0
error: STP Error: BVTypeCheck:ChildNodes of bitvector-terms must be
bitvectors


The first argument of BVCONCAT is the result of BVSGT and STP distinguishes
between booleans and bitvectors.
So I think that the error is in the code in KLEE that constructed this term.

But, after that, I am not sure what is going on - here are my confused
thoughts...

I suspect that the problem is that LLVM represents booleans as bitvectors
of length 1.

So there must be a part of KLEE (in STPBuilder???) that is responsible for
deciding whether a bitvector of length 1 should be represented by an STP
bitvector or by an STP boolean?

And, I see this comment above klee::STPBuilder::constructActual
and klee::STPBuilder::construct

     /** if *width_out!=1 then result is a bitvector,
          otherwise it is a bool */

There are two potential problems with this (but these might be
red-herrings?)

1) The width_out pointer can be null - in which case the width is not
written.
    And the code that converts Expr::Concat to STP passes a null pointer.
    this code (from STPBuilder.cpp) is not distinguishing booleans

571   case Expr::Concat: {
572     ConcatExpr *ce = cast<ConcatExpr>(e);
573     unsigned numKids = ce->getNumKids();
574     ExprHandle res = construct(ce->getKid(numKids-1), 0);
575     for (int i=numKids-2; i>=0; i--) {
576       res = vc_bvConcatExpr(vc, construct(ce->getKid(i), 0), res);
577     }
578     *width_out = ce->getWidth();
579     return res;
580   }

2) This seems to treat all 1-bit bitvectors as booleans - is this always
true?
     In particular, I wonder whether the Rust compiler satisfies this
assumption?



But these could be red-herrings. The expression being converted is a bit
unusual

      concat(sgt(_,_), sgt(_,_))

It's not impossible but it is a bit odd. So maybe something went wrong
elsewhere in KLEE to construct this code?


Any thoughts on how to debug this or on my interpretation of the code above
would be great!

Are there any command line flags that would generate a trace as the Expr is
being constructed? This would let me find the part of assembly.ll that is
triggering the problem and hopefully figure out if the problem is in
STPBuilder or elsewhere.

Thanks,

Alastair
-------------- next part --------------
HTML attachment scrubbed and removed