From 42bca7ee2db48b0fc080cdb4af6a05cb666efb8c Mon Sep 17 00:00:00 2001 From: Lukáš Zaoral Date: Wed, 15 Jun 2022 21:17:46 +0200 Subject: Intrinsics: Add support for @llvm.f{ma,muladd}.f* --- lib/Core/Executor.cpp | 35 +++++++++++++++++++++++++++++++++++ lib/Module/IntrinsicCleaner.cpp | 2 ++ 2 files changed, 37 insertions(+) (limited to 'lib') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 1a16d389..a2928864 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1680,6 +1680,41 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, break; } + case Intrinsic::fma: + case Intrinsic::fmuladd: { + // Both fma and fmuladd support float, double and fp80. Note, that fp80 + // is not mentioned in the documentation of fmuladd, nevertheless, it is + // still supported. For details see + // https://github.com/klee/klee/pull/1507/files#r894993332 + + if (isa(i->getOperand(0)->getType())) + return terminateStateOnExecError( + state, f->getName() + " with vectors is not supported"); + + ref op1 = + toConstant(state, eval(ki, 1, state).value, "floating point"); + ref op2 = + toConstant(state, eval(ki, 2, state).value, "floating point"); + ref op3 = + toConstant(state, eval(ki, 3, state).value, "floating point"); + + if (!fpWidthToSemantics(op1->getWidth()) || + !fpWidthToSemantics(op2->getWidth()) || + !fpWidthToSemantics(op3->getWidth())) + return terminateStateOnExecError( + state, "Unsupported " + f->getName() + " call"); + + // (op1 * op2) + op3 + APFloat Res(*fpWidthToSemantics(op1->getWidth()), op1->getAPValue()); + Res.fusedMultiplyAdd( + APFloat(*fpWidthToSemantics(op2->getWidth()), op2->getAPValue()), + APFloat(*fpWidthToSemantics(op3->getWidth()), op3->getAPValue()), + APFloat::rmNearestTiesToEven); + + bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); + break; + } + #if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0) case Intrinsic::abs: { if (isa(i->getOperand(0)->getType())) diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 7836c202..adef513e 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -66,6 +66,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::vastart: case Intrinsic::vaend: case Intrinsic::fabs: + case Intrinsic::fma: + case Intrinsic::fmuladd: #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) case Intrinsic::fshr: case Intrinsic::fshl: -- cgit 1.4.1