diff options
author | Felix Rath <felix.rath@comsys.rwth-aachen.de> | 2019-05-24 15:44:06 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-05-28 16:59:14 +0100 |
commit | abf654288c2f7f0ee6e1dd3e34b70c1aabe82ea7 (patch) | |
tree | 8f9227364fa0d3bf7792f8eebb0ea57835c2db02 /lib | |
parent | 0cf14d6d70b939ad29a9da42b33a4a5d4697b947 (diff) | |
download | klee-abf654288c2f7f0ee6e1dd3e34b70c1aabe82ea7.tar.gz |
Implement handling of the llvm.fabs intrinsic
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 63 | ||||
-rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 1 |
2 files changed, 39 insertions, 25 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 845fa8ff..05e20f65 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1319,6 +1319,28 @@ void Executor::stepInstruction(ExecutionState &state) { haltExecution = true; } +static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) { + switch (width) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) + case Expr::Int32: + return &llvm::APFloat::IEEEsingle(); + case Expr::Int64: + return &llvm::APFloat::IEEEdouble(); + case Expr::Fl80: + return &llvm::APFloat::x87DoubleExtended(); +#else + case Expr::Int32: + return &llvm::APFloat::IEEEsingle; + case Expr::Int64: + return &llvm::APFloat::IEEEdouble; + case Expr::Fl80: + return &llvm::APFloat::x87DoubleExtended; +#endif + default: + return 0; + } +} + void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, @@ -1332,9 +1354,22 @@ void Executor::executeCall(ExecutionState &state, // state may be destroyed by this call, cannot touch callExternalFunction(state, ki, f, arguments); break; - - // va_arg is handled by caller and intrinsic lowering, see comment for - // ExecutionState::varargs + case Intrinsic::fabs: { + ref<ConstantExpr> arg = + toConstant(state, eval(ki, 0, state).value, "floating point"); + if (!fpWidthToSemantics(arg->getWidth())) + return terminateStateOnExecError( + state, "Unsupported intrinsic llvm.fabs call"); + + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), + arg->getAPValue()); + Res = llvm::abs(Res); + + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); + break; + } + // va_arg is handled by caller and intrinsic lowering, see comment for + // ExecutionState::varargs case Intrinsic::vastart: { StackFrame &sf = state.stack.back(); @@ -1579,28 +1614,6 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { } } -static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) { - switch(width) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) - case Expr::Int32: - return &llvm::APFloat::IEEEsingle(); - case Expr::Int64: - return &llvm::APFloat::IEEEdouble(); - case Expr::Fl80: - return &llvm::APFloat::x87DoubleExtended(); -#else - case Expr::Int32: - return &llvm::APFloat::IEEEsingle; - case Expr::Int64: - return &llvm::APFloat::IEEEdouble; - case Expr::Fl80: - return &llvm::APFloat::x87DoubleExtended; -#endif - default: - return 0; - } -} - void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *i = ki->inst; switch (i->getOpcode()) { diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index dde97036..e2ed3f39 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -59,6 +59,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { switch (ii->getIntrinsicID()) { case Intrinsic::vastart: case Intrinsic::vaend: + case Intrinsic::fabs: break; // Lower vacopy so that object resolution etc is handled by |