More robust handling of unknown intrinsics

- If an unknown intrinsic appears in the bitcode file,
  it is reported but execution can proceed.

- If an unknown intrinsic is encountered during execution of some path,
  - the intrinsic is reported
  - this path is treated as an error
  - execution of other paths can proceed

To be more precise, there is a list of "known unknown intrinsics".
Intrinsics not on this list will prevent execution.

3 files changed, 129 insertions, 2 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3dbb5a66..ea3fffb7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1511,7 +1511,9 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       // FIXME: It would be nice to check for errors in the usage of this as
       // well.
     default:
-      klee_error("unknown intrinsic: %s", f->getName().data());
+      klee_warning("unimplemented intrinsic: %s", f->getName().data());
+      terminateStateOnError(state, "unimplemented intrinsic", Unhandled);
+      return;
     }
 
     if (InvokeInst *ii = dyn_cast<InvokeInst>(i))
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index a1d4fdda..030a75ca 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -10,6 +10,7 @@
 #include "Passes.h"
 
 #include "klee/Config/Version.h"
+#include "klee/Support/ErrorHandling.h"
 #include "llvm/Analysis/MemoryBuiltins.h"
 #include "llvm/Analysis/ConstantFolding.h"
 #include "llvm/IR/Constants.h"
@@ -20,6 +21,9 @@
 #include "llvm/IR/Instruction.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/IntrinsicInst.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0)
+#include "llvm/IR/IntrinsicsX86.h"
+#endif
 #include "llvm/IR/Module.h"
 #include "llvm/IR/Type.h"
 #include "llvm/Pass.h"
@@ -340,10 +344,69 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
         break;
       }
 #endif
-      default:
+
+      // The following intrinsics are currently handled by LowerIntrinsicCall
+      // (Invoking LowerIntrinsicCall with any intrinsics not on this
+      // list throws an exception.)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
+      case Intrinsic::addressofreturnaddress:
+#endif
+      case Intrinsic::annotation:
+      case Intrinsic::assume:
+      case Intrinsic::bswap:
+      case Intrinsic::ceil:
+      case Intrinsic::copysign:
+      case Intrinsic::cos:
+      case Intrinsic::ctlz:
+      case Intrinsic::ctpop:
+      case Intrinsic::cttz:
+      case Intrinsic::dbg_declare:
+#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
+      case Intrinsic::dbg_label:
+#endif
+      case Intrinsic::eh_typeid_for:
+      case Intrinsic::exp2:
+      case Intrinsic::exp:
+      case Intrinsic::expect:
+      case Intrinsic::floor:
+      case Intrinsic::flt_rounds:
+      case Intrinsic::frameaddress:
+      case Intrinsic::get_dynamic_area_offset:
+      case Intrinsic::invariant_end:
+      case Intrinsic::invariant_start:
+      case Intrinsic::lifetime_end:
+      case Intrinsic::lifetime_start:
+      case Intrinsic::log10:
+      case Intrinsic::log2:
+      case Intrinsic::log:
+      case Intrinsic::memcpy:
+      case Intrinsic::memmove:
+      case Intrinsic::memset:
+      case Intrinsic::not_intrinsic:
+      case Intrinsic::pcmarker:
+      case Intrinsic::pow:
+      case Intrinsic::prefetch:
+      case Intrinsic::ptr_annotation:
+      case Intrinsic::readcyclecounter:
+      case Intrinsic::returnaddress:
+      case Intrinsic::round:
+      case Intrinsic::sin:
+      case Intrinsic::sqrt:
+      case Intrinsic::stackrestore:
+      case Intrinsic::stacksave:
+      case Intrinsic::trunc:
+      case Intrinsic::var_annotation:
         IL->LowerIntrinsicCall(ii);
         dirty = true;
         break;
+
+        // Warn about any unrecognized intrinsics.
+      default: {
+        const Function *Callee = ii->getCalledFunction();
+        llvm::StringRef name = Callee->getName();
+        klee_warning_once((void*)Callee, "unsupported intrinsic %.*s", (int)name.size(), name.data());
+        break;
+      }
       }
     }
   }
diff --git a/test/Intrinsics/Missing.ll b/test/Intrinsics/Missing.ll
new file mode 100644
index 00000000..c628b952
--- /dev/null
+++ b/test/Intrinsics/Missing.ll
@@ -0,0 +1,62 @@
+; RUN: %llvmas %s -o=%t.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out --optimize=false %t.bc 2>&1 | FileCheck %s
+
+; Check that IntrinsicCleaner notices missing intrinsic
+; CHECK: KLEE: WARNING ONCE: unsupported intrinsic llvm.minnum.f32
+
+; Check that Executor notices missing intrinsic
+; CHECK: KLEE: WARNING: unimplemented intrinsic: llvm.minnum.f32
+; CHECK: KLEE: ERROR: (location information missing) unimplemented intrinsic
+; CHECK: KLEE: WARNING: unimplemented intrinsic: llvm.minnum.f32
+
+; Check that Executor explores all paths
+; CHECK: KLEE: done: completed paths = 3
+; CHECK: KLEE: done: generated tests = 2
+
+
+
+; This test checks that KLEE will ignore intrinsics that are not executed
+; It consists of a dead function that is called on one path but not on
+; another path.
+;
+; The choice of which unimplemented intrinsic to use in this test is arbitrary
+; and will need to be updated if the intrinsic is implemented.
+;
+; The dead function is called twice so that we can distinguish between
+; KLEE executing both paths successfully and KLEE aborting on
+; the last path it explores.
+
+declare float @llvm.minnum.f32(float, float)
+
+define void @dead() {
+  %x = call float @llvm.minnum.f32(float 1.0, float 2.0)
+  ret void
+}
+
+declare void @klee_make_symbolic(i8*, i64, i8*)
+
+define i32 @main() {
+  %x1_addr = alloca i8, i8 1
+  call void @klee_make_symbolic(i8* %x1_addr, i64 1, i8* null)
+  %x1 = load i8, i8* %x1_addr
+
+  %x2_addr = alloca i8, i8 1
+  call void @klee_make_symbolic(i8* %x2_addr, i64 1, i8* null)
+  %x2 = load i8, i8* %x2_addr
+
+  %c1 = icmp eq i8 %x1, 0
+  br i1 %c1, label %useDeadIntrinsic1, label %skip1
+useDeadIntrinsic1:
+  call void @dead()
+  ret i32 1
+skip1:
+
+  %c2 = icmp eq i8 %x2, 0
+  br i1 %c2, label %skip2, label %useDeadIntrinsic2
+skip2:
+  ret i32 0
+useDeadIntrinsic2:
+  call void @dead()
+  ret i32 2
+}