diff options
author | Alastair Reid <adreid@google.com> | 2020-06-16 16:57:46 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-06-29 22:22:48 +0100 |
commit | 67ea19efc36bbf8885f32e85d11f920342a7949c (patch) | |
tree | 17d329f3901bc349d92a4e8ab570b10d6f066ad8 /lib | |
parent | 51e28268a927e1e40899ff2df11faa553d3c2e79 (diff) | |
download | klee-67ea19efc36bbf8885f32e85d11f920342a7949c.tar.gz |
Implement fshr/fshl intrinsics
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 28 | ||||
-rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 4 |
2 files changed, 32 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b7041148..af376755 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1424,6 +1424,34 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } + +#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) + case Intrinsic::fshr: + case Intrinsic::fshl: { + ref<Expr> op1 = eval(ki, 1, state).value; + ref<Expr> op2 = eval(ki, 2, state).value; + ref<Expr> op3 = eval(ki, 3, state).value; + unsigned w = op1->getWidth(); + assert(w == op2->getWidth() && "type mismatch"); + assert(w == op3->getWidth() && "type mismatch"); + ref<Expr> c = ConcatExpr::create(op1, op2); + // op3 = zeroExtend(op3 % w) + op3 = URemExpr::create(op3, ConstantExpr::create(w, w)); + op3 = ZExtExpr::create(op3, w+w); + if (f->getIntrinsicID() == Intrinsic::fshl) { + // shift left and take top half + ref<Expr> s = ShlExpr::create(c, op3); + bindLocal(ki, state, ExtractExpr::create(s, w, w)); + } else { + // shift right and take bottom half + // note that LShr and AShr will have same behaviour + ref<Expr> s = LShrExpr::create(c, op3); + bindLocal(ki, state, ExtractExpr::create(s, 0, w)); + } + break; + } +#endif + // va_arg is handled by caller and intrinsic lowering, see comment for // ExecutionState::varargs case Intrinsic::vastart: { diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index f59192c1..a1d4fdda 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -62,6 +62,10 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::vastart: case Intrinsic::vaend: case Intrinsic::fabs: +#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) + case Intrinsic::fshr: + case Intrinsic::fshl: +#endif break; // Lower vacopy so that object resolution etc is handled by |