diff options
| -rw-r--r-- | include/klee/Expr.h | 9 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 263 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 16 | ||||
| -rw-r--r-- | test/Feature/LongDoubleSupport.c | 33 |
4 files changed, 141 insertions, 180 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index e3a57123..6e55cdd3 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -310,6 +310,12 @@ public: unsigned getNumKids() const { return 0; } ref<Expr> getKid(unsigned i) const { return 0; } + /// getAPValue - Return the arbitrary precision value directly. + /// + /// Clients should generally not use the APInt value directly and instead use + /// native ConstantExpr APIs. + const llvm::APInt &getAPValue() const { return value; } + /// getZExtValue - Return the constant value for a limited number of bits. /// /// This routine should be used in situations where the width of the constant @@ -410,6 +416,9 @@ public: ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); + + // Comparisons return a constant expression of width 1. + ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8f5b3daa..79b2040b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -933,41 +933,7 @@ ref<klee::ConstantExpr> Executor::evalConstant(Constant *c) { if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) { return ConstantExpr::alloc(ci->getValue()); } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) { - switch(cf->getType()->getTypeID()) { - case Type::FloatTyID: { - float f = cf->getValueAPF().convertToFloat(); - return ConstantExpr::create(floats::FloatAsUInt64(f), Expr::Int32); - } - case Type::DoubleTyID: { - double d = cf->getValueAPF().convertToDouble(); - return ConstantExpr::create(floats::DoubleAsUInt64(d), Expr::Int64); - } - case Type::X86_FP80TyID: { - // FIXME: This is really broken, but for now we just convert - // to a double. This isn't going to work at all in general, - // but we need support for wide constants. - APFloat apf = cf->getValueAPF(); - bool ignored; - APFloat::opStatus r = apf.convert(APFloat::IEEEdouble, - APFloat::rmNearestTiesToAway, - &ignored); - (void) r; - //assert(!(r & APFloat::opOverflow) && !(r & APFloat::opUnderflow) && - // "Overflow/underflow while converting from FP80 (x87) to 64-bit double"); - double d = apf.convertToDouble(); - return ConstantExpr::create(floats::DoubleAsUInt64(d), Expr::Int64); - } - default: - llvm::cerr << "Constant of type " << cf->getType()->getDescription() - << " not supported\n"; - llvm::cerr << "Constant used at "; - KConstant *kc = kmodule->getKConstant((Constant*) cf); - if (kc && kc->ki && kc->ki->info) - llvm::cerr << kc->ki->info->file << ":" << kc->ki->info->line << "\n"; - else llvm::cerr << "<unknown>\n"; - - assert(0 && "Arbitrary bit width floating point constants unsupported"); - } + return ConstantExpr::alloc(cf->getValueAPF().bitcastToAPInt()); } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(c)) { return globalAddresses.find(gv)->second; } else if (isa<ConstantPointerNull>(c)) { @@ -1897,66 +1863,62 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { break; } - // Floating point specific instructions - -#define FP_CONSTANT_BINOP(op, type, l, r, target, state) \ - if (type > 64) \ - return terminateStateOnExecError(state, \ - "Unsupported FP operation"); \ - bindLocal(target, state, \ - ConstantExpr::alloc(op(toConstant(state, l, \ - "floating point")->getZExtValue(), \ - toConstant(state, r, \ - "floating point")->getZExtValue(), \ - type), type)) + // Floating point instructions case Instruction::FAdd: { - BinaryOperator *bi = cast<BinaryOperator>(i); - ref<Expr> left = eval(ki, 0, state).value; - ref<Expr> right = eval(ki, 1, state).value; - Expr::Width type = Expr::getWidthForLLVMType(bi->getType()); - FP_CONSTANT_BINOP(floats::add, type, left, right, ki, state); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); + llvm::APFloat Res(left->getAPValue()); + Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } case Instruction::FSub: { - BinaryOperator *bi = cast<BinaryOperator>(i); - ref<Expr> left = eval(ki, 0, state).value; - ref<Expr> right = eval(ki, 1, state).value; - Expr::Width type = Expr::getWidthForLLVMType(bi->getType()); - FP_CONSTANT_BINOP(floats::sub, type, left, right, ki, state); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); + llvm::APFloat Res(left->getAPValue()); + Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } case Instruction::FMul: { - BinaryOperator *bi = cast<BinaryOperator>(i); - ref<Expr> left = eval(ki, 0, state).value; - ref<Expr> right = eval(ki, 1, state).value; - Expr::Width type = Expr::getWidthForLLVMType(bi->getType()); - FP_CONSTANT_BINOP(floats::mul, type, left, right, ki, state); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); + llvm::APFloat Res(left->getAPValue()); + Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } case Instruction::FDiv: { - BinaryOperator *bi = cast<BinaryOperator>(i); - - ref<Expr> dividend = eval(ki, 0, state).value; - ref<Expr> divisor = eval(ki, 1, state).value; - Expr::Width type = Expr::getWidthForLLVMType(bi->getType()); - FP_CONSTANT_BINOP(floats::div, type, dividend, divisor, ki, state); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); + llvm::APFloat Res(left->getAPValue()); + Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } case Instruction::FRem: { - BinaryOperator *bi = cast<BinaryOperator>(i); - - ref<Expr> dividend = eval(ki, 0, state).value; - ref<Expr> divisor = eval(ki, 1, state).value; - Expr::Width type = Expr::getWidthForLLVMType(bi->getType()); - FP_CONSTANT_BINOP(floats::mod, type, dividend, divisor, ki, state); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); + llvm::APFloat Res(left->getAPValue()); + Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } -#undef FP_CONSTANT_BINOP case Instruction::FPTrunc: { FPTruncInst *fi = cast<FPTruncInst>(i); @@ -1964,7 +1926,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); uint64_t value = floats::trunc(arg->getZExtValue(), resultType, arg->getWidth()); @@ -1978,7 +1940,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported FPExt operation"); uint64_t value = floats::ext(arg->getZExtValue(), resultType, arg->getWidth()); @@ -1992,7 +1954,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported FPToUI operation"); uint64_t value = floats::toUnsignedInt(arg->getZExtValue(), resultType, arg->getWidth()); @@ -2006,7 +1968,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported FPToSI operation"); uint64_t value = floats::toSignedInt(arg->getZExtValue(), resultType, arg->getWidth()); @@ -2020,7 +1982,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported UIToFP operation"); uint64_t value = floats::UnsignedIntToFP(arg->getZExtValue(), resultType); bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); @@ -2033,7 +1995,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); if (arg->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); + return terminateStateOnExecError(state, "Unsupported SIToFP operation"); uint64_t value = floats::SignedIntToFP(arg->getZExtValue(), resultType, arg->getWidth()); @@ -2043,111 +2005,90 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { case Instruction::FCmp: { FCmpInst *fi = cast<FCmpInst>(i); - Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); - ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, - "floating point"); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); - if (left->getWidth() > 64) - return terminateStateOnExecError(state, "Unsupported FP operation"); - uint64_t leftVal = left->getZExtValue(); - uint64_t rightVal = right->getZExtValue(); - - //determine whether the operands are NANs - unsigned inWidth = left->getWidth(); - bool leftIsNaN = floats::isNaN( leftVal, inWidth ); - bool rightIsNaN = floats::isNaN( rightVal, inWidth ); - - //handle NAN based on whether the predicate is "ordered" or "unordered" - uint64_t ret = (uint64_t)-1; - bool done = false; + APFloat LHS(left->getAPValue()); + APFloat RHS(right->getAPValue()); + APFloat::cmpResult CmpRes = LHS.compare(RHS); + + bool Result = false; switch( fi->getPredicate() ) { - //predicates which only care about whether or not the operands are NaNs + // Predicates which only care about whether or not the operands are NaNs. case FCmpInst::FCMP_ORD: - done = true; - ret = !leftIsNaN && !rightIsNaN; + Result = CmpRes != APFloat::cmpUnordered; break; case FCmpInst::FCMP_UNO: - done = true; - ret = leftIsNaN || rightIsNaN; + Result = CmpRes == APFloat::cmpUnordered; break; - //ordered comparisons return false if either operand is NaN - case FCmpInst::FCMP_OEQ: - case FCmpInst::FCMP_OGT: - case FCmpInst::FCMP_OGE: - case FCmpInst::FCMP_OLT: - case FCmpInst::FCMP_OLE: - case FCmpInst::FCMP_ONE: - if( !leftIsNaN && !rightIsNaN) //only fall through and return false if there are NaN(s) + // Ordered comparisons return false if either operand is NaN. Unordered + // comparisons return true if either operand is NaN. + case FCmpInst::FCMP_UEQ: + if (CmpRes == APFloat::cmpUnordered) { + Result = true; break; - - case FCmpInst::FCMP_FALSE: { //always return false for this predicate - done = true; - ret = false; + } + case FCmpInst::FCMP_OEQ: + Result = CmpRes == APFloat::cmpEqual; break; - } - //unordered comparisons return true if either operand is NaN - case FCmpInst::FCMP_UEQ: case FCmpInst::FCMP_UGT: - case FCmpInst::FCMP_UGE: - case FCmpInst::FCMP_ULT: - case FCmpInst::FCMP_ULE: - case FCmpInst::FCMP_UNE: - if( !leftIsNaN && !rightIsNaN) //only fall through and return true if there are NaN(s) + if (CmpRes == APFloat::cmpUnordered) { + Result = true; break; - - case FCmpInst::FCMP_TRUE: //always return true for this predicate - done = true; - ret = true; - - default: - case FCmpInst::BAD_FCMP_PREDICATE: /* will fall through and trigger fatal in the next switch */ + } + case FCmpInst::FCMP_OGT: + Result = CmpRes == APFloat::cmpGreaterThan; break; - } - - //if not done, then we need to actually do a comparison to get the result - if( !done ) { - switch( fi->getPredicate() ) { - //ordered comparisons return false if either operand is NaN - case FCmpInst::FCMP_OEQ: - case FCmpInst::FCMP_UEQ: - ret = floats::eq( leftVal, rightVal, inWidth ); - break; - case FCmpInst::FCMP_OGT: - case FCmpInst::FCMP_UGT: - ret = floats::gt( leftVal, rightVal, inWidth ); + case FCmpInst::FCMP_UGE: + if (CmpRes == APFloat::cmpUnordered) { + Result = true; break; + } + case FCmpInst::FCMP_OGE: + Result = CmpRes == APFloat::cmpGreaterThan || CmpRes == APFloat::cmpEqual; + break; - case FCmpInst::FCMP_OGE: - case FCmpInst::FCMP_UGE: - ret = floats::ge( leftVal, rightVal, inWidth ); + case FCmpInst::FCMP_ULT: + if (CmpRes == APFloat::cmpUnordered) { + Result = true; break; + } + case FCmpInst::FCMP_OLT: + Result = CmpRes == APFloat::cmpLessThan; + break; - case FCmpInst::FCMP_OLT: - case FCmpInst::FCMP_ULT: - ret = floats::lt( leftVal, rightVal, inWidth ); + case FCmpInst::FCMP_ULE: + if (CmpRes == APFloat::cmpUnordered) { + Result = true; break; + } + case FCmpInst::FCMP_OLE: + Result = CmpRes == APFloat::cmpLessThan || CmpRes == APFloat::cmpEqual; + break; - case FCmpInst::FCMP_OLE: - case FCmpInst::FCMP_ULE: - ret = floats::le( leftVal, rightVal, inWidth ); - break; + case FCmpInst::FCMP_UNE: + Result = CmpRes == APFloat::cmpUnordered || CmpRes != APFloat::cmpEqual; + break; + case FCmpInst::FCMP_ONE: + Result = CmpRes != APFloat::cmpUnordered && CmpRes != APFloat::cmpEqual; + break; - case FCmpInst::FCMP_ONE: - case FCmpInst::FCMP_UNE: - ret = floats::ne( leftVal, rightVal, inWidth ); - break; - - default: - terminateStateOnExecError(state, "invalid FCmp predicate"); - } + default: + assert(0 && "Invalid FCMP predicate!"); + case FCmpInst::FCMP_FALSE: + Result = false; + break; + case FCmpInst::FCMP_TRUE: + Result = true; + break; } - bindLocal(ki, state, ConstantExpr::alloc(ret, resultType)); + bindLocal(ki, state, ConstantExpr::alloc(Result, Expr::Bool)); break; } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index d4042e3f..fc450d76 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -277,20 +277,10 @@ void Expr::printWidth(std::ostream &os, Width width) { Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) { switch (t->getTypeID()) { - case llvm::Type::IntegerTyID: { - Width w = cast<IntegerType>(t)->getBitWidth(); - - // should remove this limitation soon - if (w == 1 || w == 8 || w == 16 || w == 32 || w == 64) - return w; - else { - assert(0 && "XXX arbitrary bit widths unsupported"); - abort(); - } - } + case llvm::Type::IntegerTyID: return cast<IntegerType>(t)->getBitWidth(); case llvm::Type::FloatTyID: return Expr::Int32; case llvm::Type::DoubleTyID: return Expr::Int64; - case llvm::Type::X86_FP80TyID: return Expr::Int64; // XXX: needs to be fixed + case llvm::Type::X86_FP80TyID: return 80; case llvm::Type::PointerTyID: return kMachinePointerType; default: cerr << "non-primitive type argument to Expr::getTypeForLLVMType()\n"; @@ -332,6 +322,7 @@ ref<Expr> ConstantExpr::fromMemory(void *address, Width width) { case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width); case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width); case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width); + // FIXME: Should support long double, at least. } } @@ -343,6 +334,7 @@ void ConstantExpr::toMemory(void *address) { case Expr::Int16: *((uint16_t*) address) = getZExtValue(16); break; case Expr::Int32: *((uint32_t*) address) = getZExtValue(32); break; case Expr::Int64: *((uint64_t*) address) = getZExtValue(64); break; + // FIXME: Should support long double, at least. } } diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c index b4631832..185a5485 100644 --- a/test/Feature/LongDoubleSupport.c +++ b/test/Feature/LongDoubleSupport.c @@ -1,8 +1,9 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc > %t2.out +// RUN: %klee --optimize=0 --exit-on-error %t1.bc > %t2.out #include <stdio.h> #include <float.h> +#include <assert.h> // FIXME: This doesn't really work at all, it just doesn't // crash. Until we have wide constant support, that is all we care @@ -10,11 +11,29 @@ // constants, we don't actually end up seeing much code which uses long // double. int main() { - long double a = LDBL_MAX; - long double b = -1; - long double c = a + b; - printf("a = %Lg\n", a); - printf("b = %Lg\n", b); - printf("c = %Lg\n", c); + unsigned N0 = 0, N1 = 0, N2 = 0; + + float V0 = .1; + while (V0 != 0) { + V0 *= V0; + N0++; + } + double V1 = .1; + while (V1 != 0) { + V1 *= V1; + N1++; + } + long double V2 = .1; + while (V2 != 0) { + V2 *= V2; + N2++; + } + + printf("counts: %d, %d, %d\n", N0, N1, N2); + + assert(N0 == 6); + assert(N1 == 9); + assert(N2 == 13); + return 0; } |