Hi, I've been doing some work on KLEE recently and I believe I've found several bugs in the code for the class ConstantExpr (include/klee/Expr.h).
I need to be able to determine whether or not an instance of a ConstantExpr is a boolean true/ boolean false or a integer constant. The ConstantExpr::isTrue() and ConstantExpr::isFalse() methods would seem to provide this however using them can easily cause assertion failures. Consider calling ConstantExpr::isTrue() on a ConstantExpr of width 64 (i.e. it's not an integer constant). This will execute return getZExtValue(1) == 1 Which is turn executes the following assert statement assert(getWidth() <= bits && "Value may be out of range!"); This will fail because it is checking (64 <= 1) which is false! In fact the only case where calling ConstantExpr::isTrue() or ConstantExpr::isFalse() won't result in assertion failure is if the ConstantExpr is width 1. So there is definitely a bug in both ConstantExpr::isTrue() and ConstantExpr::isFalse(). To fix this I present a patch here : https://github.com/delcypher/klee/commit/bcdda366096e6c617a809a58dc8232b8e533c822.patch The other bugs I believe are in the ConstantExpr::getZExtValue(unsigned bits) method.. * It's description is "- Return the constant value for a limited number of bits.". I think this is incredibly mis-leading as I interpret this description to mean return the an integer with bits [0,bits -1] and the remaining bits set to zero. The function actually calls llvm::APInt::getZExtValue() which returns the integer as a uint64_t regardless of what the "bits" parameter is set to. * The assert statement doesn't really make any sense - calling llvm::APInt::getZExtValue() on a llvm::APInt of width greater than 64 will cause an assertion failure according to the documentation ( http://llvm.org/docs/doxygen/html/classllvm_1_1APInt.html#a7dc983ebf0eb2d255fa90a67063c72e2). So an assert really isn't necessary. * The assert itself doesn't make sense surely it should be testing assert(bits <= getWidth() ) instead? Regards, Dan Liew.
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
