diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 28 | ||||
| -rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 4 | ||||
| -rw-r--r-- | test/Intrinsics/fshlr.ll | 76 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 14 |
4 files changed, 116 insertions, 6 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 diff --git a/test/Intrinsics/fshlr.ll b/test/Intrinsics/fshlr.ll new file mode 100644 index 00000000..fcdf32ff --- /dev/null +++ b/test/Intrinsics/fshlr.ll @@ -0,0 +1,76 @@ +; Tests for the Funnel Shift intrinsics fshl/fshr(a, b, c) which +; - concatenate 'a' and 'b' +; - shift the result by an amount 'c' (left or right) +; - return the top or bottom half of result (depending on direction) +; +; This file consists of a sequence of tests of the form +; ``` +; T = llvm_fshl(a, b, c); +; C = T != r; +; if C { +; klee_abort(); +; } +; ``` +; where the constants a, b, c and r are copied from the constants +; used in the LLVM testfile llvm/test/Analysis/ConstantFolding/funnel-shift.ll + +; REQUIRES: geq-llvm-7.0 +; RUN: %llvmas %s -o=%t.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %t.bc + +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-pc-linux-gnu" + +declare i32 @llvm.fshl.i32(i32, i32, i32) +declare i32 @llvm.fshr.i32(i32, i32, i32) +declare i7 @llvm.fshl.i7(i7, i7, i7) +declare i7 @llvm.fshr.i7(i7, i7, i7) + +declare void @klee_abort() + +; Function Attrs: noinline nounwind optnone uwtable +define dso_local i32 @main() #0 { + + ; T1: extract(concat(0x12345678, 0xABCDEF01) << 5) = 0x468ACF15 + %T1 = call i32 @llvm.fshl.i32(i32 305419896, i32 2882400001, i32 5) + %C1 = icmp ne i32 %T1, 1183502101 + br i1 %C1, label %FAIL1, label %OK1 +FAIL1: + call void @klee_abort() + unreachable +OK1: + + ; T2: extract(concat(0x12345678, 0xABCDEF01) >> 5) = 0xC55E6F78 + ; Try an oversized shift (37) to test modulo functionality. + %T2 = call i32 @llvm.fshr.i32(i32 305419896, i32 2882400001, i32 37) + %C2 = icmp ne i32 %T2, 3311300472 + br i1 %C2, label %FAIL2, label %OK2 +FAIL2: + call void @klee_abort() + unreachable +OK2: + + ; T3: extract(concat(0b1110000, 0b1111111) << 2) = 0b1000011 + ; Use a weird type. + ; Try an oversized shift (9) to test modulo functionality. + %T3 = call i7 @llvm.fshl.i7(i7 112, i7 127, i7 9) + %C3 = icmp ne i7 %T3, 67 + br i1 %C3, label %FAIL3, label %OK3 +FAIL3: + call void @klee_abort() + unreachable +OK3: + + ; T4: extract(concat(0b1110000, 0b1111111) >> 2) = 0b0011111 + ; Try an oversized shift (16) to test modulo functionality. + %T4 = call i7 @llvm.fshr.i7(i7 112, i7 127, i7 16) + %C4 = icmp ne i7 %T4, 31 + br i1 %C4, label %FAIL4, label %OK4 +FAIL4: + call void @klee_abort() + unreachable +OK4: + + ret i32 0 +} diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index ada08550..87d7ccf9 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -948,12 +948,14 @@ void externalsAndGlobalsCheck(const llvm::Module *m) { const std::string &ext = it->first; if (!modelled.count(ext) && (WarnAllExternals || !dontCare.count(ext))) { - if (unsafe.count(ext)) { - foundUnsafe.insert(*it); - } else { - klee_warning("undefined reference to %s: %s", - it->second ? "variable" : "function", - ext.c_str()); + if (ext.compare(0, 5, "llvm.") != 0) { // not an LLVM reserved name + if (unsafe.count(ext)) { + foundUnsafe.insert(*it); + } else { + klee_warning("undefined reference to %s: %s", + it->second ? "variable" : "function", + ext.c_str()); + } } } } |