diff options
Diffstat (limited to 'runtime')
26 files changed, 91 insertions, 72 deletions
diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile index 3c6b01b3..49f8f9cc 100644 --- a/runtime/Intrinsic/Makefile +++ b/runtime/Intrinsic/Makefile @@ -9,15 +9,24 @@ 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=kleeRuntimeIntrinsic +else +# KLEE built against older versions of LLVM expects a library archive instead +BYTECODE_LIBRARY=1 LIBRARYNAME=kleeRuntimeIntrinsic +endif + DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 -BYTECODE_LIBRARY=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 -MODULE_NAME=kleeRuntimeIntrinsic C.Flags += -fno-builtin include $(LEVEL)/Makefile.common diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c index 56f0f9dc..6ea1e02e 100644 --- a/runtime/Intrinsic/klee_int.c +++ b/runtime/Intrinsic/klee_int.c @@ -8,7 +8,7 @@ //===----------------------------------------------------------------------===// #include <assert.h> -#include <klee/klee.h> +#include "klee/klee.h" int klee_int(const char *name) { int x; diff --git a/runtime/POSIX/Makefile b/runtime/POSIX/Makefile index 9a42f5c0..1e570098 100644 --- a/runtime/POSIX/Makefile +++ b/runtime/POSIX/Makefile @@ -11,10 +11,10 @@ LEVEL=../.. LIBRARYNAME=kleeRuntimePOSIX DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 BYTECODE_LIBRARY=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index d976b0b4..8b69fd04 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, reasonable. */ klee_assume((s->st_blksize & ~0xFFFF) == 0); - klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); - klee_prefer_cex(s, s->st_dev == defaults->st_dev); - klee_prefer_cex(s, s->st_rdev == defaults->st_rdev); - klee_prefer_cex(s, (s->st_mode&0700) == 0600); - klee_prefer_cex(s, (s->st_mode&0070) == 0020); - klee_prefer_cex(s, (s->st_mode&0007) == 0002); - klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); - klee_prefer_cex(s, s->st_nlink == 1); - klee_prefer_cex(s, s->st_uid == defaults->st_uid); - klee_prefer_cex(s, s->st_gid == defaults->st_gid); - klee_prefer_cex(s, s->st_blksize == 4096); - klee_prefer_cex(s, s->st_atime == defaults->st_atime); - klee_prefer_cex(s, s->st_mtime == defaults->st_mtime); - klee_prefer_cex(s, s->st_ctime == defaults->st_ctime); + klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); + klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev); + klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev); + klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600); + klee_posix_prefer_cex(s, (s->st_mode&0070) == 0020); + klee_posix_prefer_cex(s, (s->st_mode&0007) == 0002); + klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); + klee_posix_prefer_cex(s, s->st_nlink == 1); + klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid); + klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid); + klee_posix_prefer_cex(s, s->st_blksize == 4096); + klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime); + klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime); + klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime); s->st_size = dfile->size; s->st_blocks = 8; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index 2a6b6f68..cbcf31f4 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -67,7 +67,7 @@ static char *__get_sym_str(int numChars, char *name) { klee_make_symbolic(s, numChars+1, name); for (i=0; i<numChars; i++) - klee_prefer_cex(s, __isprint(s[i])); + klee_posix_prefer_cex(s, __isprint(s[i])); s[numChars] = '\0'; return s; diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index eca63169..d059ba8a 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -9,14 +9,23 @@ LEVEL=../.. -LIBRARYNAME=klee-libc +# 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 klee-libc to be a LLVM module rather than an archive MODULE_NAME=klee-libc -#DONT_BUILD_RELINKED=1 +else +# KLEE built against older versions of LLVM expect a library archive instead BYTECODE_LIBRARY=1 -MODULE_NAME=klee-libc +LIBRARYNAME=klee-libc +endif + +#DONT_BUILD_RELINKED=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 #NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some # builtins. diff --git a/runtime/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c index e7982848..990b645d 100644 --- a/runtime/klee-libc/__cxa_atexit.c +++ b/runtime/klee-libc/__cxa_atexit.c @@ -1,11 +1,11 @@ -//===-- __cxa_atexit.c ----------------------------------------------------===// +/*===-- __cxa_atexit.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.h" diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c index 0332d095..741bcf82 100644 --- a/runtime/klee-libc/abort.c +++ b/runtime/klee-libc/abort.c @@ -1,11 +1,11 @@ -//===-- abort.c -----------------------------------------------------------===// +/*===-- abort.c -----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/atexit.c b/runtime/klee-libc/atexit.c index c71b2cd6..7b3b53b5 100644 --- a/runtime/klee-libc/atexit.c +++ b/runtime/klee-libc/atexit.c @@ -1,11 +1,11 @@ -//===-- atexit.c ----------------------------------------------------------===// +/*==-- atexit.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int __cxa_atexit(void (*fn)(void*), void *arg, diff --git a/runtime/klee-libc/calloc.c b/runtime/klee-libc/calloc.c index 30b88b30..1466fc07 100644 --- a/runtime/klee-libc/calloc.c +++ b/runtime/klee-libc/calloc.c @@ -1,16 +1,16 @@ -//===-- calloc.c ----------------------------------------------------------===// +/*===-- calloc.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> #include <string.h> -// DWD - I prefer to be internal +/* DWD - I prefer to be internal */ #if 0 void *calloc(size_t nmemb, size_t size) { unsigned nbytes = nmemb * size; @@ -19,7 +19,8 @@ void *calloc(size_t nmemb, size_t size) { memset(addr, 0, nbytes); return addr; } -// Always reallocate. + +/* Always reallocate. */ void *realloc(void *ptr, size_t nbytes) { if(!ptr) return malloc(nbytes); @@ -30,14 +31,14 @@ void *realloc(void *ptr, size_t nbytes) { } unsigned copy_nbytes = klee_get_obj_size(ptr); - //printf("REALLOC: current object = %d bytes!\n", copy_nbytes); + /* printf("REALLOC: current object = %d bytes!\n", copy_nbytes); */ void *addr = malloc(nbytes); if(addr) { - // shrinking + /* shrinking */ if(copy_nbytes > nbytes) copy_nbytes = nbytes; - //printf("REALLOC: copying = %d bytes!\n", copy_nbytes); + /* printf("REALLOC: copying = %d bytes!\n", copy_nbytes); */ memcpy(addr, ptr, copy_nbytes); free(ptr); } diff --git a/runtime/klee-libc/htonl.c b/runtime/klee-libc/htonl.c index 521ef5d6..777ecf94 100644 --- a/runtime/klee-libc/htonl.c +++ b/runtime/klee-libc/htonl.c @@ -1,11 +1,11 @@ -//===-- htonl.c -----------------------------------------------------------===// +/*===-- htonl.c -----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <sys/types.h> #include <sys/param.h> @@ -16,7 +16,7 @@ #undef ntohs #undef ntohl -// Make sure we can recognize the endianness. +/* Make sure we can recognize the endianness. */ #if (!defined(BYTE_ORDER) || !defined(BIG_ENDIAN) || !defined(LITTLE_ENDIAN)) #error "Unknown platform endianness!" #endif diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c index 181aedaa..44e5cea2 100644 --- a/runtime/klee-libc/klee-choose.c +++ b/runtime/klee-libc/klee-choose.c @@ -1,11 +1,11 @@ -//===-- klee-choose.c -----------------------------------------------------===// +/*===-- klee-choose.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.h" @@ -13,7 +13,7 @@ uintptr_t klee_choose(uintptr_t n) { uintptr_t x; klee_make_symbolic(&x, sizeof x, "klee_choose"); - // NB: this will *not* work if they don't compare to n values. + /* NB: this will *not* work if they don't compare to n values. */ if(x >= n) klee_silent_exit(0); return x; diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c index 7f7f133d..c7c6e6d3 100644 --- a/runtime/klee-libc/memcpy.c +++ b/runtime/klee-libc/memcpy.c @@ -1,11 +1,11 @@ -//===-- memcpy.c ----------------------------------------------------------===// +/*===-- memcpy.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/memmove.c b/runtime/klee-libc/memmove.c index c6e1ada9..3e86de02 100644 --- a/runtime/klee-libc/memmove.c +++ b/runtime/klee-libc/memmove.c @@ -1,11 +1,11 @@ -//===-- memmove.c ---------------------------------------------------------===// +/*===-- memmove.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/mempcpy.c b/runtime/klee-libc/mempcpy.c index 31e142d9..31712251 100644 --- a/runtime/klee-libc/mempcpy.c +++ b/runtime/klee-libc/mempcpy.c @@ -1,11 +1,11 @@ -//===-- mempcpy.c ---------------------------------------------------------===// +/*===-- mempcpy.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c index ee9ecb87..81025d32 100644 --- a/runtime/klee-libc/memset.c +++ b/runtime/klee-libc/memset.c @@ -1,11 +1,11 @@ -//===-- memset.c ----------------------------------------------------------===// +/*===-- memset.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c index 497402a6..bee2d2d7 100644 --- a/runtime/klee-libc/putchar.c +++ b/runtime/klee-libc/putchar.c @@ -1,16 +1,16 @@ -//===-- putchar.c ---------------------------------------------------------===// +/*===-- putchar.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdio.h> #include <unistd.h> -// Some header may #define putchar. +/* Some header may #define putchar. */ #undef putchar int putchar(int c) { diff --git a/runtime/klee-libc/strchr.c b/runtime/klee-libc/strchr.c index 33f97bea..50f1b9f4 100644 --- a/runtime/klee-libc/strchr.c +++ b/runtime/klee-libc/strchr.c @@ -1,11 +1,11 @@ -//===-- strchr.c ----------------------------------------------------------===// +/*===-- strchr.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ char *strchr(const char *p, int ch) { char c; diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c index 6b8c4e85..cdb002c7 100644 --- a/runtime/klee-libc/strcmp.c +++ b/runtime/klee-libc/strcmp.c @@ -1,11 +1,11 @@ -//===-- strcmp.c ----------------------------------------------------------===// +/*===-- strcmp.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int strcmp(const char *a, const char *b) { while (*a && *a == *b) diff --git a/runtime/klee-libc/strcoll.c b/runtime/klee-libc/strcoll.c index 73d59f89..8f78b0b3 100644 --- a/runtime/klee-libc/strcoll.c +++ b/runtime/klee-libc/strcoll.c @@ -1,15 +1,15 @@ -//===-- strcoll.c ---------------------------------------------------------===// +/*===-- strcoll.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> -// according to the manpage, this is equiv in the POSIX/C locale. +/* according to the manpage, this is equiv in the POSIX/C locale. */ int strcoll(const char *s1, const char *s2) { return strcmp(s1,s2); } diff --git a/runtime/klee-libc/strcpy.c b/runtime/klee-libc/strcpy.c index 0fbaf9a7..d1ec67b8 100644 --- a/runtime/klee-libc/strcpy.c +++ b/runtime/klee-libc/strcpy.c @@ -1,11 +1,11 @@ -//===-- strcpy.c ----------------------------------------------------------===// +/*===-- strcpy.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ char *strcpy(char *to, const char *from) { char *start = to; diff --git a/runtime/klee-libc/strlen.c b/runtime/klee-libc/strlen.c index e298410c..33846134 100644 --- a/runtime/klee-libc/strlen.c +++ b/runtime/klee-libc/strlen.c @@ -1,11 +1,11 @@ -//===-- strlen.c ----------------------------------------------------------===// +/*===-- strlen.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> diff --git a/runtime/klee-libc/strrchr.c b/runtime/klee-libc/strrchr.c index 01128b48..4d51769b 100644 --- a/runtime/klee-libc/strrchr.c +++ b/runtime/klee-libc/strrchr.c @@ -1,11 +1,11 @@ -//===-- strrchr.c ---------------------------------------------------------===// +/*===-- strrchr.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> diff --git a/runtime/klee-libc/tolower.c b/runtime/klee-libc/tolower.c index 265f5deb..a311f2010 100644 --- a/runtime/klee-libc/tolower.c +++ b/runtime/klee-libc/tolower.c @@ -1,11 +1,11 @@ -//===-- tolower.c ---------------------------------------------------------===// +/*===-- tolower.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int tolower(int ch) { if ( (unsigned int)(ch - 'A') < 26u ) diff --git a/runtime/klee-libc/toupper.c b/runtime/klee-libc/toupper.c index 37e5f9d6..5030b5cc 100644 --- a/runtime/klee-libc/toupper.c +++ b/runtime/klee-libc/toupper.c @@ -1,11 +1,11 @@ -//===-- toupper.c ---------------------------------------------------------===// +/*===-- toupper.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int toupper(int ch) { if ( (unsigned int)(ch - 'a') < 26u ) diff --git a/runtime/klee-uclibc/Makefile b/runtime/klee-uclibc/Makefile index e166cfbc..1b5ea682 100644 --- a/runtime/klee-uclibc/Makefile +++ b/runtime/klee-uclibc/Makefile @@ -47,8 +47,8 @@ uninstall:: remove_klee_uclibc copy_klee_uclibc: @echo "Installing klee-uclibc archive" - $(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME) + $(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(BYTECODE_DESTINATION)/$(KLEE_UCLIBC_BCA_NAME) remove_klee_uclibc: @echo "Removing klee-uclibc archive" - $(Verb) $(RM) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME) + $(Verb) $(RM) $(BYTECODE_DESTINATION)/$(KLEE_UCLIBC_BCA_NAME) |