diff options
| -rw-r--r-- | include/klee/Expr.h | 6 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 130 | ||||
| -rw-r--r-- | lib/Core/ExternalDispatcher.cpp | 7 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 12 | ||||
| -rw-r--r-- | test/Feature/LongDouble.cpp | 56 |
5 files changed, 171 insertions, 40 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index a1a1bc27..0759f953 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -14,6 +14,7 @@ #include "klee/util/Ref.h" #include "llvm/ADT/APInt.h" +#include "llvm/ADT/APFloat.h" #include "llvm/ADT/SmallVector.h" #include <set> @@ -95,6 +96,7 @@ public: static const Width Int16 = 16; static const Width Int32 = 32; static const Width Int64 = 64; + static const Width Fl80 = 80; enum Kind { @@ -361,6 +363,10 @@ public: return r; } + static ref<ConstantExpr> alloc(const llvm::APFloat &f) { + return alloc(f.bitcastToAPInt()); + } + static ref<ConstantExpr> alloc(uint64_t v, Width w) { return alloc(llvm::APInt(w, v)); } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ce80ea37..d0fc43cf 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1303,6 +1303,19 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) { #endif } +static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) { + switch(width) { + case Expr::Int32: + return &llvm::APFloat::IEEEsingle; + case Expr::Int64: + return &llvm::APFloat::IEEEdouble; + case Expr::Fl80: + return &llvm::APFloat::x87DoubleExtended; + default: + return 0; + } +} + void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *i = ki->inst; switch (i->getOpcode()) { @@ -1925,6 +1938,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FAdd operation"); + llvm::APFloat Res(left->getAPValue()); Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); @@ -1936,6 +1953,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FSub operation"); + llvm::APFloat Res(left->getAPValue()); Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); @@ -1947,6 +1968,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FMul operation"); + llvm::APFloat Res(left->getAPValue()); Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); @@ -1958,6 +1983,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FDiv operation"); + llvm::APFloat Res(left->getAPValue()); Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); @@ -1969,6 +1998,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FRem operation"); + llvm::APFloat Res(left->getAPValue()); Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); @@ -1980,12 +2013,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); - if (arg->getWidth() > 64) + if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth()) return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); - uint64_t value = floats::trunc(arg->getZExtValue(), - resultType, - arg->getWidth()); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); + + llvm::APFloat Res(arg->getAPValue()); + bool losesInfo = false; + Res.convert(*fpWidthToSemantics(resultType), + llvm::APFloat::rmNearestTiesToEven, + &losesInfo); + bindLocal(ki, state, ConstantExpr::alloc(Res)); break; } @@ -1993,13 +2029,16 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { FPExtInst *fi = cast<FPExtInst>(i); Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, - "floating point"); - if (arg->getWidth() > 64) + "floating point"); + if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType) return terminateStateOnExecError(state, "Unsupported FPExt operation"); - uint64_t value = floats::ext(arg->getZExtValue(), - resultType, - arg->getWidth()); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); + + llvm::APFloat Res(arg->getAPValue()); + bool losesInfo = false; + Res.convert(*fpWidthToSemantics(resultType), + llvm::APFloat::rmNearestTiesToEven, + &losesInfo); + bindLocal(ki, state, ConstantExpr::alloc(Res)); break; } @@ -2008,11 +2047,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); - if (arg->getWidth() > 64) + if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToUI operation"); - uint64_t value = floats::toUnsignedInt(arg->getZExtValue(), - resultType, - arg->getWidth()); + + llvm::APFloat Arg(arg->getAPValue()); + uint64_t value = 0; + bool isExact = true; + Arg.convertToInteger(&value, resultType, false, + llvm::APFloat::rmTowardZero, &isExact); bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); break; } @@ -2022,11 +2064,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); - if (arg->getWidth() > 64) + if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToSI operation"); - uint64_t value = floats::toSignedInt(arg->getZExtValue(), - resultType, - arg->getWidth()); + + llvm::APFloat Arg(arg->getAPValue()); + uint64_t value = 0; + bool isExact = true; + Arg.convertToInteger(&value, resultType, false, + llvm::APFloat::rmTowardZero, &isExact); bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); break; } @@ -2036,11 +2081,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); - if (arg->getWidth() > 64) + const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType); + if (!semantics) return terminateStateOnExecError(state, "Unsupported UIToFP operation"); - uint64_t value = floats::UnsignedIntToFP(arg->getZExtValue(), - resultType); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); + llvm::APFloat f(*semantics, 0); + f.convertFromAPInt(arg->getAPValue(), false, + llvm::APFloat::rmNearestTiesToEven); + + bindLocal(ki, state, ConstantExpr::alloc(f)); break; } @@ -2049,12 +2097,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType()); ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, "floating point"); - if (arg->getWidth() > 64) + const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType); + if (!semantics) return terminateStateOnExecError(state, "Unsupported SIToFP operation"); - uint64_t value = floats::SignedIntToFP(arg->getZExtValue(), - resultType, - arg->getWidth()); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); + llvm::APFloat f(*semantics, 0); + f.convertFromAPInt(arg->getAPValue(), true, + llvm::APFloat::rmNearestTiesToEven); + + bindLocal(ki, state, ConstantExpr::alloc(f)); break; } @@ -2064,6 +2114,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, "floating point"); + if (!fpWidthToSemantics(left->getWidth()) || + !fpWidthToSemantics(right->getWidth())) + return terminateStateOnExecError(state, "Unsupported FCmp operation"); + APFloat LHS(left->getAPValue()); APFloat RHS(right->getAPValue()); APFloat::cmpResult CmpRes = LHS.compare(RHS); @@ -2561,23 +2615,27 @@ void Executor::callExternalFunction(ExecutionState &state, } // normal external function handling path - uint64_t *args = (uint64_t*) alloca(sizeof(*args) * (arguments.size() + 1)); - memset(args, 0, sizeof(*args) * (arguments.size() + 1)); - - unsigned i = 1; + // allocate 128 bits for each argument (+return value) to support fp80's; + // we could iterate through all the arguments first and determine the exact + // size we need, but this is faster, and the memory usage isn't significant. + uint64_t *args = (uint64_t*) alloca(2*sizeof(*args) * (arguments.size() + 1)); + memset(args, 0, 2 * sizeof(*args) * (arguments.size() + 1)); + unsigned wordIndex = 2; for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), - ae = arguments.end(); ai!=ae; ++ai, ++i) { + ae = arguments.end(); ai!=ae; ++ai) { if (AllowExternalSymCalls) { // don't bother checking uniqueness ref<ConstantExpr> ce; bool success = solver->getValue(state, *ai, ce); assert(success && "FIXME: Unhandled solver failure"); (void) success; - static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]); + ce->toMemory(&args[wordIndex]); + wordIndex += (ce->getWidth()+63)/64; } else { ref<Expr> arg = toUnique(state, *ai); - if (ConstantExpr *CE = dyn_cast<ConstantExpr>(arg)) { + if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) { // XXX kick toMemory functions from here - CE->toMemory((void*) &args[i]); + ce->toMemory(&args[wordIndex]); + wordIndex += (ce->getWidth()+63)/64; } else { terminateStateOnExecError(state, "external call with symbolic argument: " + diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index f746e6fa..665a0461 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -229,7 +229,7 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in cast<FunctionType>(cast<PointerType>(target->getType())->getElementType()); // Each argument will be passed by writing it into gTheArgsP[i]. - unsigned i = 0; + unsigned i = 0, idx = 2; for (CallSite::arg_iterator ai = cs.arg_begin(), ae = cs.arg_end(); ai!=ae; ++ai, ++i) { // Determine the type the argument will be passed as. This accomodates for @@ -240,12 +240,15 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in Instruction *argI64p = GetElementPtrInst::Create(argI64s, ConstantInt::get(Type::getInt32Ty(getGlobalContext()), - i+1), + idx), "", dBB); Instruction *argp = new BitCastInst(argI64p, PointerType::getUnqual(argTy), "", dBB); args[i] = new LoadInst(argp, "", dBB); + + unsigned argSize = argTy->getPrimitiveSizeInBits(); + idx += ((!!argSize ? argSize : 64) + 63)/64; } Constant *dispatchTarget = diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 386d29de..703c689f 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -274,6 +274,7 @@ void Expr::printWidth(std::ostream &os, Width width) { case Expr::Int16: os << "Expr::Int16"; break; case Expr::Int32: os << "Expr::Int32"; break; case Expr::Int64: os << "Expr::Int64"; break; + case Expr::Fl80: os << "Expr::Fl80"; break; default: os << "<invalid type: " << (unsigned) width << ">"; } } @@ -305,7 +306,11 @@ 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. + // FIXME: what about machines without x87 support? + case Expr::Fl80: + return ConstantExpr::alloc(llvm::APInt(width, + (width+llvm::integerPartWidth-1)/llvm::integerPartWidth, + (const uint64_t*)address)); } } @@ -317,7 +322,10 @@ 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. + // FIXME: what about machines without x87 support? + case Expr::Fl80: + *((long double*) address) = *(long double*) value.getRawData(); + break; } } diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.cpp new file mode 100644 index 00000000..ecee43b4 --- /dev/null +++ b/test/Feature/LongDouble.cpp @@ -0,0 +1,56 @@ +// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s +// RUN: %klee --libc=klee --no-output --exit-on-error %t.bc > %t.log +// RUN: grep -q {powl\(-11\\.0,0\)=1\\.0\\+} %t.log +// RUN: grep -q {powl\(-11\\.0,1\)=-11\\.0\\+} %t.log +// RUN: grep -q {powl\(-11\\.0,2\)=121\\.0\\+} %t.log +// RUN: grep -q {1/0=inf} %t.log +// RUN: grep -q {1/-1=-1\\.0\\+} %t.log +// RUN: grep -q {1/-2=-0\\.50\\+} %t.log + +#include <cstdio> +#include <cstdlib> +#include <cmath> +#include <cassert> + +#include "klee/klee.h" + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x, "x"); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int main(int argc, char ** argv) +{ + + int a = klee_urange(0,3); + int b; + + // fork states + switch(a) { + case 0: + b = -0; + break; + case 1: + b = -1; + break; + case 2: + b = -2; + break; + default: + assert(false && "Impossible switch target"); + } + + // test 80-bit external dispatch + long double d = powl((long double)-11.0, (long double)a); + printf("powl(-11.0,%d)=%Lf\n", a, d); + + // test 80-bit fdiv + long double e = (long double) 1 / (long double) b; + printf("1/%d=%Lf\n", b, e); + + return 0; +} + + |