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.

1 files changed, 62 insertions, 0 deletions

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
+}