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, 147 insertions, 2 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 7eb02d3f..c0cfd01e 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -14,8 +14,8 @@ LEVEL=..
 
 #
 # List all of the subdirectories that we will compile.
-#
-PARALLEL_DIRS=Intrinsic klee-libc Runtest
+
+PARALLEL_DIRS=Intrinsic klee-libc Runtest svcomp32 svcomp64
 
 include $(LEVEL)/Makefile.config
 
diff --git a/runtime/svcomp32/Makefile b/runtime/svcomp32/Makefile
new file mode 100644
index 00000000..6f877690
--- /dev/null
+++ b/runtime/svcomp32/Makefile
@@ -0,0 +1,36 @@
+#===-- runtime/Intrinsic/Makefile --------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+# FIXME: This doesn't work. So we have to duplicate
+# functions.c via a symlink
+#SOURCES=../svcomp64/functions.c
+
+# Needed for LLVM version
+include $(LEVEL)/Makefile.config
+
+ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True)
+# For these versions of LLVM KLEE expects kleeRuntimeIntrinsic to be a LLVM module rather than an archive
+MODULE_NAME=kleeSVCOMPRuntime32
+else
+# KLEE built against older versions of LLVM expects a library archive instead
+BYTECODE_LIBRARY=1
+LIBRARYNAME=kleeSVCOMPRuntime32
+endif
+
+DONT_BUILD_RELINKED=1
+# Don't strip debug info from the module.
+DEBUG_RUNTIME=1
+NO_PEDANTIC=1
+NO_BUILD_ARCHIVE=1
+
+C.Flags += -fno-builtin -m32
+
+include $(LEVEL)/Makefile.common
diff --git a/runtime/svcomp32/functions.c b/runtime/svcomp32/functions.c
new file mode 120000
index 00000000..5eba0694
--- /dev/null
+++ b/runtime/svcomp32/functions.c
@@ -0,0 +1 @@
+../svcomp64/functions.c
\ No newline at end of file
diff --git a/runtime/svcomp64/Makefile b/runtime/svcomp64/Makefile
new file mode 100644
index 00000000..40d44ec3
--- /dev/null
+++ b/runtime/svcomp64/Makefile
@@ -0,0 +1,32 @@
+#===-- runtime/Intrinsic/Makefile --------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+# Needed for LLVM version
+include $(LEVEL)/Makefile.config
+
+ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True)
+# For these versions of LLVM KLEE expects kleeRuntimeIntrinsic to be a LLVM module rather than an archive
+MODULE_NAME=kleeSVCOMPRuntime64
+else
+# KLEE built against older versions of LLVM expects a library archive instead
+BYTECODE_LIBRARY=1
+LIBRARYNAME=kleeSVCOMPRuntime64
+endif
+
+DONT_BUILD_RELINKED=1
+# Don't strip debug info from the module.
+DEBUG_RUNTIME=1
+NO_PEDANTIC=1
+NO_BUILD_ARCHIVE=1
+
+C.Flags += -fno-builtin -m64
+
+include $(LEVEL)/Makefile.common
diff --git a/runtime/svcomp64/functions.c b/runtime/svcomp64/functions.c
new file mode 100644
index 00000000..0fdae3bd
--- /dev/null
+++ b/runtime/svcomp64/functions.c
@@ -0,0 +1,76 @@
+//===-- functions.c           ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/klee_svcomp.h"
+
+#define SVCOMP_NONDET_DEFN_D(NAME,T) \
+T __VERIFIER_nondet_ ## NAME() { \
+  T initialValue; \
+  klee_make_symbolic(&initialValue,\
+                     sizeof(T),\
+                     "svcomp.sym" # T);\
+  return initialValue; \
+}
+
+#define SVCOMP_NONDET_DEFN(NAME) SVCOMP_NONDET_DEFN_D(NAME, NAME)
+
+#define SVCOMP_NONDET_DEFN_NOT_SUPPORTED(NAME) \
+    SVCOMP_NONDET_DEFN_D_NOT_SUPPORTED(NAME, NAME)
+
+SVCOMP_NONDET_DEFN_D(bool,_Bool)
+SVCOMP_NONDET_DEFN(char)
+SVCOMP_NONDET_DEFN(int)
+SVCOMP_NONDET_DEFN(long)
+SVCOMP_NONDET_DEFN(loff_t)
+SVCOMP_NONDET_DEFN_D(pointer,void*)
+SVCOMP_NONDET_DEFN_D(pchar,char*)
+SVCOMP_NONDET_DEFN(pthread_t)
+SVCOMP_NONDET_DEFN(sector_t)
+SVCOMP_NONDET_DEFN(short)
+SVCOMP_NONDET_DEFN(size_t)
+SVCOMP_NONDET_DEFN_D(u32, uint32_t)
+SVCOMP_NONDET_DEFN_D(uchar,unsigned char)
+SVCOMP_NONDET_DEFN_D(uint, unsigned int)
+SVCOMP_NONDET_DEFN_D(ulong, unsigned long)
+SVCOMP_NONDET_DEFN(unsigned)
+SVCOMP_NONDET_DEFN_D(ushort, unsigned short)
+
+float __VERIFIER_nondet_float() {
+  union {
+    uint32_t asBits;
+    float asFloat;
+  } data;
+  klee_warning("Symbolic data of type float not supported. Returning quiet NaN");
+  data.asBits = 0x7fc00000;
+  return data.asFloat;
+}
+
+void __VERIFIER_assume(int condition) {
+  klee_assume(condition);
+}
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    klee_report_error(__FILE__, __LINE__ ,
+                      "svcomp assert failed",
+                      "svcomp.assertfail");
+  }
+}
+
+__attribute__ ((__noreturn__)) void __VERIFIER_error()  {
+  klee_report_error(__FILE__, __LINE__,"svcomp error", "svcomp.err");
+}
+
+void __VERIFIER_atomic_begin() {
+  klee_warning("__VERIFIER_atomic_begin() is a no-op");
+}
+
+void __VERIFIER_atomic_end() {
+  klee_warning("__VERIFIER_atomic_end() is a no-op");
+}