Implemented SV-COMP 2016 runtime functions which can be activated with

the --svcomp-runtime flag. This is accompanied with a set of tests
to check all the functions are callable.

Due to the fact that the SV-COMP benchmark suite contains a mixture
of i386 and x86_64 benchmarks it is necessary to compile the runtime
functions twice, once for i386 and once for x86_64 and then link the
right version in at runtime. An example function that is problematic
is ``__VERIFIER_nondet_long()`` which is a different size on i386
and x86_64.

5 files changed, 145 insertions, 0 deletions

diff --git a/test/Runtime/svcomp/verifier_assert.c b/test/Runtime/svcomp/verifier_assert.c
new file mode 100644
index 00000000..1986e8c1
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_assert.c
@@ -0,0 +1,17 @@
+// RUN: %llvmgcc %s -emit-llvm -std=c99 -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --svcomp-runtime %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %t.klee-out/test000001.svcomp.assertfail
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: test -f %t.klee-out/test000002.ktest
+#include "klee/klee.h"
+#include "klee/klee_svcomp.h"
+
+int main() {
+  // FIXME: Use FileCheck's relative line feature
+  // CHECK: verifier_assert.c:15: svcomp assert failed
+  int truth;
+  klee_make_symbolic(&truth, sizeof(int), "truth");
+  __VERIFIER_assert(truth);
+  return 0;
+}
diff --git a/test/Runtime/svcomp/verifier_assume.c b/test/Runtime/svcomp/verifier_assume.c
new file mode 100644
index 00000000..9388edfa
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_assume.c
@@ -0,0 +1,28 @@
+// RUN: %llvmgcc %s -emit-llvm -std=c99 -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --svcomp-runtime %t1.bc
+// RUN: not test -f %t.klee-out/test*.err
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: test -f %t.klee-out/test000002.ktest
+// RUN: not test -f %t.klee-out/test000003.ktest
+#include "klee/klee.h"
+#include "klee/klee_svcomp.h"
+#include "stdio.h"
+
+int main() {
+  // FIXME: Use FileCheck's relative line feature
+  // CHECK: verifier_assert.c:12: svcomp assert failed
+  int x;
+  klee_make_symbolic(&x, sizeof(int), "x");
+  __VERIFIER_assume( x > 10 );
+  if (x == 10) {
+    // should be unreachable
+    printf("Is 10\n");
+    __VERIFIER_error();
+  } else if (x == 11) {
+    printf("Is 11\n");
+  } else {
+    printf("Is something else\n");
+  }
+  return 0;
+}
diff --git a/test/Runtime/svcomp/verifier_atomic.c b/test/Runtime/svcomp/verifier_atomic.c
new file mode 100644
index 00000000..6db889e9
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_atomic.c
@@ -0,0 +1,12 @@
+// RUN: %llvmgcc %s -emit-llvm -g -std=c99 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --svcomp-runtime %t.bc > %t.kleeoutput.log 2>&1
+// RUN: not test -f %t.klee-out/test*.err
+
+// Check that the atomic functions are callable.
+#include "klee/klee_svcomp.h"
+int main() {
+  __VERIFIER_atomic_begin();
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/test/Runtime/svcomp/verifier_error.c b/test/Runtime/svcomp/verifier_error.c
new file mode 100644
index 00000000..ef862f9b
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_error.c
@@ -0,0 +1,13 @@
+// RUN: %llvmgcc %s -emit-llvm -g -std=c99 -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --svcomp-runtime %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %t.klee-out/test000001.svcomp.err
+
+#include "klee/klee_svcomp.h"
+
+int main() {
+  // FIXME: Use FileCheck's relative line feature
+  // CHECK: verifier_error.c:11: svcomp error
+  __VERIFIER_error();
+  return 0;
+}
diff --git a/test/Runtime/svcomp/verifier_nondet.c b/test/Runtime/svcomp/verifier_nondet.c
new file mode 100644
index 00000000..f95e2a52
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_nondet.c
@@ -0,0 +1,75 @@
+// // Test for 32-bit
+// RUN: %llvmgcc %s -emit-llvm -m32 -g -std=c99 -c -o %t_32.bc
+// RUN: rm -rf %t.klee-out_32
+// RUN: %klee --output-dir=%t.klee-out_32 --svcomp-runtime %t_32.bc > %t.kleeoutput.32.log 2>&1
+// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.32.log %s
+// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.32.log %s
+// RUN: not test -f %t.klee-out_32/test*.err
+// Test again for 64-bit
+// RUN: %llvmgcc %s -emit-llvm -m64 -g -std=c99 -c -o %t_64.bc
+// RUN: rm -rf %t.klee-out_64
+// RUN: %klee --output-dir=%t.klee-out_64 --svcomp-runtime %t_64.bc > %t.kleeoutput.64.log 2>&1
+// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.64.log %s
+// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.64.log %s
+// RUN: not test -f %t.klee-out_64/test*.err
+
+// first-CHECK: completed paths = 1
+// second-CHECK-NOT: ERROR
+// second-CHECK-NOT: abort
+#include "klee/klee.h"
+#include "klee/klee_svcomp.h"
+
+#define test_call_D(NAME,T) \
+{ \
+  T initialValue = __VERIFIER_nondet_ ## NAME(); \
+  if (!klee_is_symbolic(initialValue)) { \
+    klee_warning("Failed to get symbolic value for type " # T); \
+    klee_abort(); \
+  } \
+}
+
+#define test_call_ptr_D(NAME,T) \
+{ \
+  T initialValue = __VERIFIER_nondet_ ## NAME(); \
+  if (!klee_is_symbolic((uintptr_t) initialValue)) { \
+    klee_warning("Failed to get symbolic value for type " # T); \
+    klee_abort(); \
+  } \
+}
+
+#define test_call(NAME) test_call_D(NAME,NAME)
+#define test_call_ptr(NAME) test_call_ptr_D(NAME,NAME)
+
+int main() {
+  test_call_D(bool,_Bool);
+  test_call(char);
+  {
+    float initialValue = __VERIFIER_nondet_float();
+    if (klee_is_symbolic(initialValue)) {
+      klee_warning("Did not expect float to be symbolic");
+      klee_abort();
+    }
+  }
+  test_call(int)
+  test_call(long)
+  test_call(loff_t)
+  test_call_ptr_D(pointer,void*)
+  test_call_ptr_D(pchar,char*)
+  {
+    pthread_t initialValue = __VERIFIER_nondet_pthread_t();
+    if (!klee_is_symbolic(initialValue.id)) {
+    klee_warning("Failed to get symbolic value for id field");
+    klee_abort();
+    }
+  }
+  test_call(sector_t)
+  test_call(short)
+  test_call(size_t)
+  test_call_D(u32, uint32_t)
+  test_call_D(uchar,unsigned char)
+  test_call_D(uint, unsigned int)
+  test_call_D(ulong, unsigned long)
+  test_call(unsigned)
+  test_call_D(ushort, unsigned short)
+  return 0;
+}