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.

1 files changed, 36 insertions, 1 deletions

diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 1334b58c..e22b3d24 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -97,7 +97,11 @@ namespace {
                                    "execute switch internally"),
                         clEnumValEnd),
              cl::init(eSwitchTypeInternal));
-  
+
+  cl::opt<bool>
+  SVCOMPRuntime("svcomp-runtime",
+               cl::desc("Add SV-COMP runtime functions"),
+               cl::init(false));
   cl::opt<bool>
   DebugPrintEscapingFunctions("debug-print-escaping-functions", 
                               cl::desc("Print functions whose address is taken."));
@@ -349,6 +353,37 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     );
   module = linkWithLibrary(module, LibPath.str());
 
+  // Add SV-COMP runtime if requested
+  if (SVCOMPRuntime) {
+    LibPath = opts.LibraryDir;
+    SmallString<24> runtimeFileName;
+    llvm::StringRef targetName = module->getTargetTriple();
+    // Different versions of the runtime are required based on target
+    // because the size of some types differ. For example
+    // __VERIFIER_nondet_long() return type is i32 on i386 but i64 on x86_64
+    if (targetName.startswith("x86_64")) {
+        runtimeFileName = "kleeSVCOMPRuntime64";
+    } else if (targetName.startswith("i386")) {
+        runtimeFileName = "kleeSVCOMPRuntime32";
+    } else {
+        klee_error("Cannot determine which SV-COMP runtime to use from target %s",
+                   targetName.data());
+    }
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3,3)
+    runtimeFileName += ".bc";
+#else
+    runtimeFileName += ".bca";
+#endif
+    llvm::sys::path::append(LibPath, runtimeFileName.str());
+    module = linkWithLibrary(module, LibPath.str());
+
+    // Add all error reporting functions as internal functions so we report
+    // failures at the correct location
+    addInternalFunction("__VERIFIER_error");
+    addInternalFunction("__VERIFIER_assert");
+    addInternalFunction("__VERIFIER_assume");
+  }
+
   // Add internal functions which are not used to check if instructions
   // have been already visited
   if (opts.CheckDivZero)