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:0x001F
60:0x))
[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(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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
