about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorAlastair Reid <adreid@google.com>2020-06-16 16:57:46 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-06-29 22:22:48 +0100
commit67ea19efc36bbf8885f32e85d11f920342a7949c (patch)
tree17d329f3901bc349d92a4e8ab570b10d6f066ad8 /lib
parent51e28268a927e1e40899ff2df11faa553d3c2e79 (diff)
downloadklee-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.cpp28
-rw-r--r--lib/Module/IntrinsicCleaner.cpp4
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