From b1b96a784632f71928220117624a2c07ab3ca9e6 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 13 Aug 2013 12:22:36 +0200 Subject: Port to LLVM 3.3 Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful --- runtime/Intrinsic/Makefile | 1 + runtime/Intrinsic/memcpy.c | 2 +- runtime/Intrinsic/memmove.c | 2 +- runtime/Intrinsic/mempcpy.c | 3 +-- runtime/Intrinsic/memset.c | 3 +-- runtime/klee-libc/Makefile | 6 ++++-- 6 files changed, 9 insertions(+), 8 deletions(-) (limited to 'runtime') diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile index 849bfeee..3c6b01b3 100644 --- a/runtime/Intrinsic/Makefile +++ b/runtime/Intrinsic/Makefile @@ -17,6 +17,7 @@ BYTECODE_LIBRARY=1 DEBUG_RUNTIME=1 NO_PEDANTIC=1 +MODULE_NAME=kleeRuntimeIntrinsic C.Flags += -fno-builtin include $(LEVEL)/Makefile.common diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c index 7f7f133d..bd9f3e38 100644 --- a/runtime/Intrinsic/memcpy.c +++ b/runtime/Intrinsic/memcpy.c @@ -9,7 +9,7 @@ #include -void *memcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c index c6e1ada9..e89abf7d 100644 --- a/runtime/Intrinsic/memmove.c +++ b/runtime/Intrinsic/memmove.c @@ -9,7 +9,7 @@ #include -void *memmove(void *dst, const void *src, size_t count) { +__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) { char *a = dst; const char *b = src; diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c index 31e142d9..e47a94b1 100644 --- a/runtime/Intrinsic/mempcpy.c +++ b/runtime/Intrinsic/mempcpy.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include - -void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c index bef85e6a..c21f1fa9 100644 --- a/runtime/Intrinsic/memset.c +++ b/runtime/Intrinsic/memset.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include - -void *memset(void * dst, int s, size_t count) { +__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) { volatile char * a = dst; while (count-- > 0) *a++ = s; diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index e6a7ad72..eca63169 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -10,11 +10,13 @@ LEVEL=../.. LIBRARYNAME=klee-libc -DONT_BUILD_RELINKED=1 +MODULE_NAME=klee-libc +#DONT_BUILD_RELINKED=1 BYTECODE_LIBRARY=1 +MODULE_NAME=klee-libc # Don't strip debug info from the module. DEBUG_RUNTIME=1 -NO_PEDANTIC=1 +#NO_PEDANTIC=1 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some # builtins. -- cgit 1.4.1 From 1e63f37178748da804aae3a4735fca73dee5d53a Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 2 Sep 2013 17:15:11 +0200 Subject: Fixed multiple definitions of POSIX file functions Function like stat() were defined for 32bit and 64bit version. Added compile time based selection of appropriate version using GNUC macros __x86_64__ and __ppc64__. --- runtime/POSIX/fd_32.c | 13 +++++++++++++ runtime/POSIX/fd_64.c | 11 +++++++++++ 2 files changed, 24 insertions(+) (limited to 'runtime') diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c index 338d9ba2..20587b42 100644 --- a/runtime/POSIX/fd_32.c +++ b/runtime/POSIX/fd_32.c @@ -6,7 +6,18 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +// Contains 32bit definitions of posix file functions +//===--- +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + +#ifdef ENV32 #define _LARGEFILE64_SOURCE #include "fd.h" @@ -194,3 +205,5 @@ int fstat64(int fd, struct stat64 *buf) __attribute__((weak)); int fstat64(int fd, struct stat64 *buf) { return __fd_fstat(fd, buf); } + +#endif diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index d0710caf..c84599ff 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -7,6 +7,15 @@ // //===----------------------------------------------------------------------===// +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + +#ifdef ENV64 #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" @@ -88,3 +97,5 @@ int getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) { } int __getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) __attribute__((alias("getdents64"))); + +#endif -- cgit 1.4.1 From e9b814eda7a590af35959cd11ceeb7bef7496789 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 18 Sep 2013 12:38:32 +0200 Subject: Compile separate version of fd files only for LLVM 3.3 or higher --- runtime/POSIX/fd_32.c | 3 ++- runtime/POSIX/fd_64.c | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) (limited to 'runtime') diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c index 20587b42..f2f384fb 100644 --- a/runtime/POSIX/fd_32.c +++ b/runtime/POSIX/fd_32.c @@ -17,7 +17,8 @@ #endif #endif -#ifdef ENV32 +#include "klee/Config/Version.h" +#if defined(ENV32) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3)) #define _LARGEFILE64_SOURCE #include "fd.h" diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index c84599ff..268579c0 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -15,7 +15,9 @@ #endif #endif -#ifdef ENV64 + +#include "klee/Config/Version.h" +#if defined(ENV64) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3)) #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" -- cgit 1.4.1