aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-27 00:55:57 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-27 00:55:57 +0000
commit7ea8afa20439c579c4a1ccb251a78770ef873787 (patch)
tree59d4455f6e3f078aa093d3b95c394050b96d43dd /lib
parent648aa4261c5d2ac2c69dd08bf7a727bf6929c185 (diff)
downloadklee-7ea8afa20439c579c4a1ccb251a78770ef873787.tar.gz
Start move to using APFloat (support long double).
- Incomplete, still have to move some conversion operations. - Also, there isn't support yet for copying long double values to native memory. - Still, should be a monotonic improvement and we are no longer faking long double support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp263
-rw-r--r--lib/Expr/Expr.cpp16
2 files changed, 106 insertions, 173 deletions
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.
}
}