[klee-dev] Bool vs i1 in STPBuilder

[Cristian Cadar]

Hi Alastair,

Our assumption is that code should not be able to construct such 
expressions in the first place and they are thus invalid at the KQuery 
level.  That expression is also invalid at the SMT level, as Concat 
should take bitvectors and not booleans as arguments.  If for some 
reason Rust code ends up generating such expressions (and the bug is not 
elsewhere), then we need to either reconsider or our assumptions and/or 
fix the expression construction.

You could try --debug-print-instructions=all:stderr to find the part of 
the code that generates this.

You could also instrument the expression creation part in Expr.h/cpp to 
find out where a Concat expression receives a comparison expression as 
one of its subexpressions.  In general, we should add extra checks 
during expression construction to catch invalid expressions early.

Best,
Cristian

On 16/12/2020 15:54, Alastair Reid wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>