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

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());
+        }
       }
     }
   }