about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/klee_svcomp.h62
-rw-r--r--lib/Module/KModule.cpp37
-rw-r--r--runtime/Makefile4
-rw-r--r--runtime/svcomp32/Makefile36
l---------runtime/svcomp32/functions.c1
-rw-r--r--runtime/svcomp64/Makefile32
-rw-r--r--runtime/svcomp64/functions.c76
-rw-r--r--test/Runtime/svcomp/verifier_assert.c17
-rw-r--r--test/Runtime/svcomp/verifier_assume.c28
-rw-r--r--test/Runtime/svcomp/verifier_atomic.c12
-rw-r--r--test/Runtime/svcomp/verifier_error.c13
-rw-r--r--test/Runtime/svcomp/verifier_nondet.c75
12 files changed, 390 insertions, 3 deletions
diff --git a/include/klee/klee_svcomp.h b/include/klee/klee_svcomp.h
new file mode 100644
index 00000000..27ca1404
--- /dev/null
+++ b/include/klee/klee_svcomp.h
@@ -0,0 +1,62 @@
+//===-- klee_svomp.h           ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+// This file declares the SV-COMP 2016 functions
+// as defined in http://sv-comp.sosy-lab.org/2016/rules.php
+
+#include "klee/klee.h"
+#include "stdint.h"
+
+/* Start SV-COMP specific type declarations
+ *
+ * Taken from ``ddv-machzwd/ddv_machzwd_all_false-unreach-call.i``. Not really
+ * sure if it's applicable everywhere.
+ */
+typedef long long loff_t;
+typedef unsigned long sector_t;
+struct __pthread_t_struct
+{
+      int id;
+};
+typedef struct __pthread_t_struct pthread_t;
+
+/* End SV-COMP specific type declarations */
+
+#define SVCOMP_NONDET_DECL_D(NAME,T) \
+  T __VERIFIER_nondet_ ## NAME();
+
+#define SVCOMP_NONDET_DECL(NAME) SVCOMP_NONDET_DECL_D(NAME,NAME)
+
+SVCOMP_NONDET_DECL_D(bool,_Bool)
+SVCOMP_NONDET_DECL(char)
+SVCOMP_NONDET_DECL(float)
+SVCOMP_NONDET_DECL(int)
+SVCOMP_NONDET_DECL(long)
+SVCOMP_NONDET_DECL(loff_t)
+SVCOMP_NONDET_DECL_D(pointer,void*)
+SVCOMP_NONDET_DECL_D(pchar,char*)
+SVCOMP_NONDET_DECL(pthread_t)
+SVCOMP_NONDET_DECL(sector_t)
+SVCOMP_NONDET_DECL(short)
+SVCOMP_NONDET_DECL(size_t)
+SVCOMP_NONDET_DECL_D(u32, uint32_t)
+SVCOMP_NONDET_DECL_D(uchar,unsigned char)
+SVCOMP_NONDET_DECL_D(uint, unsigned int)
+SVCOMP_NONDET_DECL_D(ulong, unsigned long)
+SVCOMP_NONDET_DECL(unsigned)
+SVCOMP_NONDET_DECL_D(ushort, unsigned short)
+
+#undef SVCOMP_NONDET_D_DECL
+#undef SVCOMP_NONDET_DECL
+
+void __VERIFIER_assume(int condition);
+void __VERIFIER_assert(int cond);
+__attribute__ ((__noreturn__)) void __VERIFIER_error();
+void __VERIFIER_atomic_begin();
+void __VERIFIER_atomic_end();
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)
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");
+}
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;
+}
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-21 21:36:49 +0000