From 6803c37be83f0c97c95870a18cb230e135a131c9 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 15 May 2018 15:10:16 +0100 Subject: Reorganise runtime libraries provided by KLEE Strictly differentiate between the following type of libraries: * FreeStanding: contains minimal amount of methods a compiler would expect * klee-libc: contains a minimal libc implementation * POSIX: contains a POSIX layer that can be used on top of a libc implementation * Intrinsic: contains additional runtime functions which provide KLEE-specific functionalities, (e.g. checks) Builds always archives instead of single modules. This allows to reduce linked-in dependencies of tested applications. --- runtime/CMakeLists.txt | 31 ++++------------- runtime/FreeStanding/Makefile.cmake.bitcode | 15 ++++++++ runtime/FreeStanding/memcmp.c | 53 +++++++++++++++++++++++++++++ runtime/FreeStanding/memcpy.c | 19 +++++++++++ runtime/FreeStanding/memmove.c | 30 ++++++++++++++++ runtime/FreeStanding/memset.c | 17 +++++++++ runtime/Intrinsic/Makefile.cmake.bitcode | 9 +---- runtime/Intrinsic/memcpy.c | 19 ----------- runtime/Intrinsic/memmove.c | 28 --------------- runtime/Intrinsic/mempcpy.c | 18 ---------- runtime/Intrinsic/memset.c | 16 --------- runtime/Makefile.cmake.bitcode | 2 ++ runtime/Makefile.cmake.bitcode.config.in | 3 -- runtime/klee-libc/Makefile.cmake.bitcode | 7 +--- runtime/klee-libc/memcmp.c | 53 ----------------------------- runtime/klee-libc/memcpy.c | 19 ----------- runtime/klee-libc/memmove.c | 28 --------------- runtime/klee-libc/memset.c | 17 --------- 18 files changed, 144 insertions(+), 240 deletions(-) create mode 100644 runtime/FreeStanding/Makefile.cmake.bitcode create mode 100644 runtime/FreeStanding/memcmp.c create mode 100644 runtime/FreeStanding/memcpy.c create mode 100644 runtime/FreeStanding/memmove.c create mode 100644 runtime/FreeStanding/memset.c delete mode 100644 runtime/Intrinsic/memcpy.c delete mode 100644 runtime/Intrinsic/memmove.c delete mode 100644 runtime/Intrinsic/mempcpy.c delete mode 100644 runtime/Intrinsic/memset.c delete mode 100644 runtime/klee-libc/memcmp.c delete mode 100644 runtime/klee-libc/memcpy.c delete mode 100644 runtime/klee-libc/memmove.c delete mode 100644 runtime/klee-libc/memset.c diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index 2a056d9f..53a2f838 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -26,17 +26,6 @@ else() set(RUNTIME_HAS_DEBUG_SYMBOLS 0) endif() - -# FIXME: This is a horrible hack that needs to die. -# Things are very inconsistent. The runtime instrinsic -# is sometimes a LLVM module or a bitcode archive. -if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.3" OR - "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.3") - set(USE_RUNTIME_BINARY_TYPE_HACK 1) -else() - set(USE_RUNTIME_BINARY_TYPE_HACK 0) -endif() - if (ENABLE_POSIX_RUNTIME) set(BUILD_POSIX_RUNTIME 1) else() @@ -55,7 +44,7 @@ configure_file("Makefile.cmake.bitcode.rules" "Makefile.cmake.bitcode.rules" COP # Makefile for root runtime directory # Copy over makefiles for libraries -set(BITCODE_LIBRARIES "Intrinsic" "klee-libc") +set(BITCODE_LIBRARIES "Intrinsic" "klee-libc" "FreeStanding") if (ENABLE_POSIX_RUNTIME) list(APPEND BITCODE_LIBRARIES "POSIX") endif() @@ -130,19 +119,11 @@ add_dependencies(clean_all clean_runtime) ############################################################################### set(RUNTIME_FILES_TO_INSTALL) -# This is quite fragile and depends on knowledge in the bitcode -# build system. Hopefully it won't change very often though. - -# FIXME: This hack needs to die! -if (USE_RUNTIME_BINARY_TYPE_HACK) - list(APPEND RUNTIME_FILES_TO_INSTALL - "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeIntrinsic.bc" - "${KLEE_RUNTIME_DIRECTORY}/klee-libc.bc") -else() - list(APPEND RUNTIME_FILES_TO_INSTALL - "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimeIntrinsic.bca" - "${KLEE_RUNTIME_DIRECTORY}/libklee-libc.bca") -endif() +list(APPEND RUNTIME_FILES_TO_INSTALL + "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeIntrinsic.bc" + "${KLEE_RUNTIME_DIRECTORY}/klee-libc.bc" + "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeFreeStanding.bc" + ) if (ENABLE_POSIX_RUNTIME) list(APPEND RUNTIME_FILES_TO_INSTALL diff --git a/runtime/FreeStanding/Makefile.cmake.bitcode b/runtime/FreeStanding/Makefile.cmake.bitcode new file mode 100644 index 00000000..0ad434d6 --- /dev/null +++ b/runtime/FreeStanding/Makefile.cmake.bitcode @@ -0,0 +1,15 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ../ + +include $(LEVEL)/Makefile.cmake.bitcode.config + +ARCHIVE_NAME=kleeRuntimeFreeStanding + +include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/FreeStanding/memcmp.c b/runtime/FreeStanding/memcmp.c new file mode 100644 index 00000000..566daf48 --- /dev/null +++ b/runtime/FreeStanding/memcmp.c @@ -0,0 +1,53 @@ +/*- + * Copyright (c) 1990, 1993 + * The Regents of the University of California. All rights reserved. + * + * This code is derived from software contributed to Berkeley by + * Chris Torek. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * This product includes software developed by the University of + * California, Berkeley and its contributors. + * 4. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +#include + +/* + * Compare memory regions. + */ +int memcmp(const void *s1, const void *s2, size_t n) { + if (n != 0) { + const unsigned char *p1 = s1, *p2 = s2; + + do { + if (*p1++ != *p2++) { + return (*--p1 - *--p2); + } + } while (--n != 0); + } + return (0); +} diff --git a/runtime/FreeStanding/memcpy.c b/runtime/FreeStanding/memcpy.c new file mode 100644 index 00000000..c7c6e6d3 --- /dev/null +++ b/runtime/FreeStanding/memcpy.c @@ -0,0 +1,19 @@ +/*===-- 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 + +void *memcpy(void *destaddr, void const *srcaddr, size_t len) { + char *dest = destaddr; + char const *src = srcaddr; + + while (len-- > 0) + *dest++ = *src++; + return destaddr; +} diff --git a/runtime/FreeStanding/memmove.c b/runtime/FreeStanding/memmove.c new file mode 100644 index 00000000..ee0e53ae --- /dev/null +++ b/runtime/FreeStanding/memmove.c @@ -0,0 +1,30 @@ +/*===-- 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 + +void *memmove(void *dst, const void *src, size_t count) { + char *a = dst; + const char *b = src; + + if (src == dst) + return dst; + + if (src > dst) { + while (count--) + *a++ = *b++; + } else { + a += count - 1; + b += count - 1; + while (count--) + *a-- = *b--; + } + + return dst; +} diff --git a/runtime/FreeStanding/memset.c b/runtime/FreeStanding/memset.c new file mode 100644 index 00000000..b439001e --- /dev/null +++ b/runtime/FreeStanding/memset.c @@ -0,0 +1,17 @@ +/*===-- 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 + +void *memset(void *dst, int s, size_t count) { + char *a = dst; + while (count-- > 0) + *a++ = s; + return dst; +} diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode index 654ee020..77727fb4 100644 --- a/runtime/Intrinsic/Makefile.cmake.bitcode +++ b/runtime/Intrinsic/Makefile.cmake.bitcode @@ -10,13 +10,6 @@ LEVEL := ../ include $(LEVEL)/Makefile.cmake.bitcode.config -LLVMCC.Flags += -fno-builtin - -# FIXME: This is a horrible hack -ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) - MODULE_NAME=kleeRuntimeIntrinsic -else - ARCHIVE_NAME=kleeRuntimeIntrinsic -endif +ARCHIVE_NAME=kleeRuntimeIntrinsic include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c deleted file mode 100644 index bd9f3e38..00000000 --- a/runtime/Intrinsic/memcpy.c +++ /dev/null @@ -1,19 +0,0 @@ -//===-- 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 - -__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) { - char *dest = destaddr; - char const *src = srcaddr; - - while (len-- > 0) - *dest++ = *src++; - return destaddr; -} diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c deleted file mode 100644 index e89abf7d..00000000 --- a/runtime/Intrinsic/memmove.c +++ /dev/null @@ -1,28 +0,0 @@ -//===-- 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 - -__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) { - char *a = dst; - const char *b = src; - - if (src == dst) - return dst; - - if (src>dst) { - while (count--) *a++ = *b++; - } else { - a+=count-1; - b+=count-1; - while (count--) *a-- = *b--; - } - - return dst; -} diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c deleted file mode 100644 index e47a94b1..00000000 --- a/runtime/Intrinsic/mempcpy.c +++ /dev/null @@ -1,18 +0,0 @@ -//===-- 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 -__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { - char *dest = destaddr; - char const *src = srcaddr; - - while (len-- > 0) - *dest++ = *src++; - return dest; -} diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c deleted file mode 100644 index c21f1fa9..00000000 --- a/runtime/Intrinsic/memset.c +++ /dev/null @@ -1,16 +0,0 @@ -//===-- 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 -__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) { - volatile char * a = dst; - while (count-- > 0) - *a++ = s; - return dst; -} diff --git a/runtime/Makefile.cmake.bitcode b/runtime/Makefile.cmake.bitcode index 94f8a60d..03da435e 100644 --- a/runtime/Makefile.cmake.bitcode +++ b/runtime/Makefile.cmake.bitcode @@ -11,6 +11,8 @@ include $(LEVEL)/Makefile.cmake.bitcode.config DIRS += Intrinsic DIRS += klee-libc +DIRS += FreeStanding + ifneq ($(ENABLE_POSIX_RUNTIME),0) DIRS += POSIX endif diff --git a/runtime/Makefile.cmake.bitcode.config.in b/runtime/Makefile.cmake.bitcode.config.in index 5efa0154..5d1931b8 100644 --- a/runtime/Makefile.cmake.bitcode.config.in +++ b/runtime/Makefile.cmake.bitcode.config.in @@ -33,9 +33,6 @@ RUNTIME_CONFIG_STRING := @KLEE_RUNTIME_BUILD_TYPE@ # Optional features ENABLE_POSIX_RUNTIME := @BUILD_POSIX_RUNTIME@ -# FIXME: Get rid of this! -USE_MODULE_INSTEAD_OF_BCA := @USE_RUNTIME_BINARY_TYPE_HACK@ - # Commands MKDIR := mkdir RM := rm diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode index 6e85952c..9902e558 100644 --- a/runtime/klee-libc/Makefile.cmake.bitcode +++ b/runtime/klee-libc/Makefile.cmake.bitcode @@ -14,11 +14,6 @@ include $(LEVEL)/Makefile.cmake.bitcode.config # of builtins LLVMCC.Flags += -D__NO_INLINE__ -# FIXME: This is a horrible hack -ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) - MODULE_NAME=klee-libc -else - ARCHIVE_NAME=klee-libc -endif +ARCHIVE_NAME=klee-libc include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/klee-libc/memcmp.c b/runtime/klee-libc/memcmp.c deleted file mode 100644 index 7562f4f7..00000000 --- a/runtime/klee-libc/memcmp.c +++ /dev/null @@ -1,53 +0,0 @@ -/*- - * Copyright (c) 1990, 1993 - * The Regents of the University of California. All rights reserved. - * - * This code is derived from software contributed to Berkeley by - * Chris Torek. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions - * are met: - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in the - * documentation and/or other materials provided with the distribution. - * 3. All advertising materials mentioning features or use of this software - * must display the following acknowledgement: - * This product includes software developed by the University of - * California, Berkeley and its contributors. - * 4. Neither the name of the University nor the names of its contributors - * may be used to endorse or promote products derived from this software - * without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND - * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS - * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) - * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT - * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY - * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF - * SUCH DAMAGE. - */ - -#include - -/* - * Compare memory regions. - */ -int memcmp(const void *s1, const void *s2, size_t n) { - if (n != 0) { - const unsigned char *p1 = s1, *p2 = s2; - - do { - if (*p1++ != *p2++) { - return (*--p1 - *--p2); - } - } while (--n != 0); - } - return (0); -} diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c deleted file mode 100644 index c7c6e6d3..00000000 --- a/runtime/klee-libc/memcpy.c +++ /dev/null @@ -1,19 +0,0 @@ -/*===-- 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 - -void *memcpy(void *destaddr, void const *srcaddr, size_t len) { - char *dest = destaddr; - char const *src = srcaddr; - - while (len-- > 0) - *dest++ = *src++; - return destaddr; -} diff --git a/runtime/klee-libc/memmove.c b/runtime/klee-libc/memmove.c deleted file mode 100644 index 3e86de02..00000000 --- a/runtime/klee-libc/memmove.c +++ /dev/null @@ -1,28 +0,0 @@ -/*===-- 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 - -void *memmove(void *dst, const void *src, size_t count) { - char *a = dst; - const char *b = src; - - if (src == dst) - return dst; - - if (src>dst) { - while (count--) *a++ = *b++; - } else { - a+=count-1; - b+=count-1; - while (count--) *a-- = *b--; - } - - return dst; -} diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c deleted file mode 100644 index 81025d32..00000000 --- a/runtime/klee-libc/memset.c +++ /dev/null @@ -1,17 +0,0 @@ -/*===-- 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 - -void *memset(void * dst, int s, size_t count) { - char * a = dst; - while (count-- > 0) - *a++ = s; - return dst; -} -- cgit 1.4.1