From 86bb6dac9ae4a747f814a7d38c64373af6f933a78380afdb16d0b1ec45c1d398 Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Fri, 9 Feb 2024 08:00:08 +0000 Subject: [PATCH] up to 3.0+20240208 OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=134 --- ...support-to-build-newer-LLVM-versions.patch | 121 -- ...r-newer-libc-Simplify-path-detection.patch | 148 --- ...nclude-with-libcxx_includes-for-mult.patch | 376 ------ ...-klee-libc-memchr.c-compiler-warning.patch | 47 - 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch | 27 - ...ion-of-old-pass-manager-into-legacy-.patch | 1001 -------------- ...c-v1.4-as-default-to-support-the-com.patch | 28 - ...iler-s-default-standard-is-std-gnu17.patch | 1158 ----------------- ...-KLEE-s-exception-handling-runtime-w.patch | 29 - ...e-opaque-pointer-support-for-LLVM-15.patch | 65 - 0011-Add-support-for-opaque-pointers.patch | 385 ------ ...est-cases-to-support-opaque-pointers.patch | 229 ---- ...ing-unsupported-CHECK_NEXT-instead-o.patch | 33 - ...r-LLVM-versions-instead-of-unsupport.patch | 152 --- ...r-Intrinsic-get_rounding-for-LLVM-16.patch | 32 - ...t-to-aligned_alloc-generated-by-LLVM.patch | 28 - ...orted-passes-for-newer-LLVM-versions.patch | 69 - ...30-llvm-pr39177.ll-for-newer-LLVM-ve.patch | 29 - ...-thrown-libc-exceptions-more-general.patch | 40 - ...-for-expressions-using-udiv-urem-sdi.patch | 242 ---- 0021-Support-newer-LLVM-versions-in-lit.patch | 27 - ...nable-CI-to-test-newer-LLVM-versions.patch | 40 - _servicedata | 2 +- klee-3.0+20231023.obscpio | 3 - klee-3.0+20240208.obscpio | 3 + klee.changes | 48 + klee.obsinfo | 6 +- klee.spec | 35 +- 28 files changed, 59 insertions(+), 4344 deletions(-) delete mode 100644 0001-Add-support-to-build-newer-LLVM-versions.patch delete mode 100644 0002-Add-support-for-newer-libc-Simplify-path-detection.patch delete mode 100644 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch delete mode 100644 0004-Fix-klee-libc-memchr.c-compiler-warning.patch delete mode 100644 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch delete mode 100644 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch delete mode 100644 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch delete mode 100644 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch delete mode 100644 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch delete mode 100644 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch delete mode 100644 0011-Add-support-for-opaque-pointers.patch delete mode 100644 0012-Fix-test-cases-to-support-opaque-pointers.patch delete mode 100644 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch delete mode 100644 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch delete mode 100644 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch delete mode 100644 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch delete mode 100644 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch delete mode 100644 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch delete mode 100644 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch delete mode 100644 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch delete mode 100644 0021-Support-newer-LLVM-versions-in-lit.patch delete mode 100644 0022-Enable-CI-to-test-newer-LLVM-versions.patch delete mode 100644 klee-3.0+20231023.obscpio create mode 100644 klee-3.0+20240208.obscpio diff --git a/0001-Add-support-to-build-newer-LLVM-versions.patch b/0001-Add-support-to-build-newer-LLVM-versions.patch deleted file mode 100644 index f2bc3d9..0000000 --- a/0001-Add-support-to-build-newer-LLVM-versions.patch +++ /dev/null @@ -1,121 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 10:23:34 +0100 -Subject: Add support to build newer LLVM versions -Patch-mainline: no -References: llvm16 - -`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore, -instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition - -Signed-off-by: Jiri Slaby ---- - scripts/build/p-libcxx.inc | 29 ++++++++++++++++++++++------- - scripts/build/p-llvm.inc | 21 +++++++++++++-------- - 2 files changed, 35 insertions(+), 15 deletions(-) - -diff --git a/scripts/build/p-libcxx.inc b/scripts/build/p-libcxx.inc -index 641fad61..b0263c00 100644 ---- a/scripts/build/p-libcxx.inc -+++ b/scripts/build/p-libcxx.inc -@@ -30,7 +30,6 @@ build_libcxx() { - local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" - - local cmake_flags=( -- "-DLLVM_ENABLE_PROJECTS=libcxx;libcxxabi" - "-DLLVM_ENABLE_THREADS:BOOL=OFF" - "-DLIBCXX_ENABLE_THREADS:BOOL=OFF" - "-DLIBCXX_ENABLE_SHARED:BOOL=ON" -@@ -40,6 +39,13 @@ build_libcxx() { - ) - - # Static ABI libraries are not supported under OS X -+ if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then -+ cmake_flags+=("-DLLVM_ENABLE_RUNTIMES=libcxx;libcxxabi") -+ cmake_flags+=("-DLLVM_ENABLE_PROJECTS=") -+ cmake_flags+=("-DLLVM_ENABLE_PROJECTS_USED:BOOL=ON") -+ else -+ cmake_flags+=("-DLLVM_ENABLE_PROJECTS=libcxx;libcxxabi") -+ fi - if [[ "${OS}" == "osx" ]]; then - cmake_flags+=("-DLIBCXX_ENABLE_STATIC_ABI_LIBRARY:BOOL=OFF") - else -@@ -53,7 +59,11 @@ build_libcxx() { - export LLVM_COMPILER_PATH="$(dirname "${BITCODE_CC}")" - - cmake "${cmake_flags[@]}" "${LIBCXX_SRC}/llvm" -- make cxx -j$(nproc) || make cxx -+ if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then -+ make runtimes - j"$(nproc)" || make cxx || return 1 -+ else -+ make cxx - j"$(nproc)" || make cxx || return 1 -+ fi - ) - } - -@@ -65,19 +75,24 @@ install_libcxx() { - export LLVM_COMPILER=clang - export LLVM_COMPILER_PATH="$(dirname "${BITCODE_CC}")" - -- cd "${LIBCXX_BUILD}/projects" -- make install -+ if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then -+ cd "${LIBCXX_BUILD}/runtimes" || return 1 -+ make install || return 1 -+ else -+ cd "${LIBCXX_BUILD}/projects" || return 1 -+ make install || return 1 -+ fi - - local libraries - - if [[ "${OS}" == "osx" ]]; then -- libraries=("${LIBCXX_INSTALL}"/lib/lib*.dylib) -+ libraries=("${LIBCXX_INSTALL}"/lib/*/lib*.dylib) - else -- libraries=("${LIBCXX_INSTALL}"/lib/lib*.so) -+ libraries=("${LIBCXX_INSTALL}"/lib/*/lib*.so) - fi - - local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" -- libraries+=("${LIBCXX_INSTALL}"/lib/lib*.a) -+ libraries+=("${LIBCXX_INSTALL}"/lib/*/lib*.a) - - - for p in "${libraries[@]}" ; do -diff --git a/scripts/build/p-llvm.inc b/scripts/build/p-llvm.inc -index abf895ae..462d69f5 100644 ---- a/scripts/build/p-llvm.inc -+++ b/scripts/build/p-llvm.inc -@@ -174,16 +174,21 @@ configure_llvm() { - ) - - if [[ "${SANITIZER_BUILD:-}" == "memory" ]]; then -- # We have to build without libunwind if RTTI is disables -+ # We have to build without libunwind if RTTI is disabled - CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS}") - else -- CONFIG+=( -- "-DLLVM_BUILD_LLVM_DYLIB:BOOL=ON" -- "-DLLVM_LINK_LLVM_DYLIB:BOOL=ON" -- "-DLLVM_BUILD_STATIC:BOOL=OFF" -- "-DLIBCLANG_BUILD_STATIC:BOOL=OFF" -- ) -- CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS};libcxx;libcxxabi;libunwind") -+ CONFIG+=( -+ "-DLLVM_BUILD_LLVM_DYLIB:BOOL=ON" -+ "-DLLVM_LINK_LLVM_DYLIB:BOOL=ON" -+ "-DLLVM_BUILD_STATIC:BOOL=OFF" -+ "-DLIBCLANG_BUILD_STATIC:BOOL=OFF" -+ ) -+ if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then -+ CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS}") -+ CONFIG+=("-DLLVM_ENABLE_RUNTIMES=libcxx;libcxxabi") -+ else -+ CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS};libcxx;libcxxabi") -+ fi - fi - - if [[ -n ${SANITIZER_BUILD} ]]; then --- -2.43.0 - diff --git a/0002-Add-support-for-newer-libc-Simplify-path-detection.patch b/0002-Add-support-for-newer-libc-Simplify-path-detection.patch deleted file mode 100644 index b792f7c..0000000 --- a/0002-Add-support-for-newer-libc-Simplify-path-detection.patch +++ /dev/null @@ -1,148 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 10:28:42 +0100 -Subject: Add support for newer `libc++`; Simplify path detection -Patch-mainline: no -References: llvm16 - -`libc++` include headers are now split between platform dependent and -platform independent code. - -Before, only include files for the platform independent code were -considered. Add support to automatically find platform dependent -includes as well. - -Simplify the detection of libraries and paths. - -Instead of pointing to the `v1` directory, pointing to the include -directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough. - -Update build script to support this as well. - -Signed-off-by: Jiri Slaby ---- - CMakeLists.txt | 65 +++++++++++++----------------- - runtime/klee-eh-cxx/CMakeLists.txt | 8 +++- - scripts/build/p-klee.inc | 2 +- - 3 files changed, 37 insertions(+), 38 deletions(-) - -diff --git a/CMakeLists.txt b/CMakeLists.txt -index 19e9fc06..6c55eae9 100644 ---- a/CMakeLists.txt -+++ b/CMakeLists.txt -@@ -496,51 +496,44 @@ option(ENABLE_KLEE_LIBCXX "Enable libc++ for klee" OFF) - if (ENABLE_KLEE_LIBCXX) - message(STATUS "klee-libc++ support enabled") - set(SUPPORT_KLEE_LIBCXX 1) # For config.h -- set(KLEE_LIBCXX_DIR "" CACHE PATH "Path to directory containing libc++ shared object (bitcode)") -- if (NOT EXISTS "${KLEE_LIBCXX_DIR}") -- message(FATAL_ERROR -- "KLEE_LIBCXX_DIR (\"${KLEE_LIBCXX_DIR}\") does not exist.\n" -- "Try passing -DKLEE_LIBCXX_DIR= to CMake where is the path" -- "to the directory containing the libc++ shared object file (as bitcode).") -- endif() - -- set(KLEE_LIBCXX_INCLUDE_DIR "" CACHE PATH "Path to libc++ include directory") -- if (NOT EXISTS "${KLEE_LIBCXX_INCLUDE_DIR}") -- message(FATAL_ERROR -- "KLEE_LIBCXX_INCLUDE_DIR (\"${KLEE_LIBCXX_INCLUDE_DIR}\") does not exist.\n" -- "Try passing -DKLEE_LIBCXX_INCLUDE_DIR= to CMake where is the" -- "libc++ include directory.") -- endif() -- message(STATUS "Use libc++ include path: \"${KLEE_LIBCXX_INCLUDE_DIR}\"") -- -- # Find the library bitcode archive -- -- # Check for static first -- set(KLEE_LIBCXX_BC_NAME "libc++.bca") -- set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}") -- if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}") -- # Check for dynamic so lib -- set(KLEE_LIBCXX_BC_NAME "libc++.so.bc") -- set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}") -- if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}") -- set(KLEE_LIBCXX_BC_NAME "libc++.dylib.bc") -- set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}") -- if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}") -- message(FATAL_ERROR -- "libc++ library not found at \"${KLEE_LIBCXX_DIR}\"") -- endif() -- endif() -- endif() -+ find_file(KLEE_LIBCXX_BC_PATH -+ NAMES libc++.bca libc++.so.bc libc++.dylib.bc -+ DOC "Path to directory containing libc++ shared object (bitcode)" -+ PATH_SUFFIXES "lib" "lib/x86_64-unknown-linux-gnu" -+ HINTS ${KLEE_LIBCXX_DIR} -+ REQUIRED -+ ) - message(STATUS "Found libc++ library: \"${KLEE_LIBCXX_BC_PATH}\"") - -+ find_path(KLEE_LIBCXX_PLATFORM_INCLUDE_PATH -+ NAMES __config_site #We are searching for a platform-specific C++ library header called `__config_site` -+ DOC "Path to platform-specific libc++ include directory" -+ PATH_SUFFIXES "x86_64-unknown-linux-gnu/c++/v1" "include/x86_64-unknown-linux-gnu/c++/v1" -+ HINTS ${KLEE_LIBCXX_INCLUDE_DIR} -+ NO_DEFAULT_PATH # Make sure we don't pick-up the standard library's path -+ ) -+ -+ find_path(KLEE_LIBCXX_INCLUDE_PATH -+ NAMES cerrno #We are searching for a C++ library header called `cerrno` -+ DOC "Path to libc++ include directory" -+ PATH_SUFFIXES "c++/v1" "include/c++/v1" -+ HINTS ${KLEE_LIBCXX_INCLUDE_DIR} -+ REQUIRED -+ NO_DEFAULT_PATH # Make sure we don't pick-up the standard library's path -+ ) -+ -+ message(STATUS "Found libc++ include path: ${KLEE_LIBCXX_INCLUDE_PATH} and ${KLEE_LIBCXX_PLATFORM_INCLUDE_PATH} ") -+ -+ - # Copy KLEE_LIBCXX_BC_PATH so KLEE can find it where it is expected. - file(MAKE_DIRECTORY "${KLEE_RUNTIME_DIRECTORY}") - execute_process(COMMAND ${CMAKE_COMMAND} -E copy - "${KLEE_LIBCXX_BC_PATH}" -- "${KLEE_RUNTIME_DIRECTORY}/${KLEE_LIBCXX_BC_NAME}" -+ "${KLEE_RUNTIME_DIRECTORY}/${KLEE_LIBCXX_BC_PATH}" - ) - list(APPEND KLEE_COMPONENT_CXX_DEFINES -- -DKLEE_LIBCXX_BC_NAME=\"${KLEE_LIBCXX_BC_NAME}\") -+ -DKLEE_LIBCXX_BC_NAME=\"${KLEE_LIBCXX_BC_PATH}\") - - else() - message(STATUS "libc++ support disabled") -diff --git a/runtime/klee-eh-cxx/CMakeLists.txt b/runtime/klee-eh-cxx/CMakeLists.txt -index e016757b..470e3f0a 100644 ---- a/runtime/klee-eh-cxx/CMakeLists.txt -+++ b/runtime/klee-eh-cxx/CMakeLists.txt -@@ -16,8 +16,14 @@ set(ADDITIONAL_CXX_FLAGS - -nostdinc++ - -I "${KLEE_LIBCXXABI_SRC_DIR}/src" - -I "${KLEE_LIBCXXABI_SRC_DIR}/include" -- -I "${KLEE_LIBCXX_INCLUDE_DIR}" -+ -I "${KLEE_LIBCXX_INCLUDE_PATH}" -+) -+ -+if (KLEE_LIBCXX_PLATFORM_INCLUDE_PATH) -+ list(APPEND ADDITIONAL_CXX_FLAGS -+ -I "${KLEE_LIBCXX_PLATFORM_INCLUDE_PATH}" - ) -+endif () - # Build it - include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") - prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files) -diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc -index 82dedeaa..b7384b91 100644 ---- a/scripts/build/p-klee.inc -+++ b/scripts/build/p-klee.inc -@@ -49,7 +49,7 @@ if [ "${USE_LIBCXX}" -eq 1 ]; then - CMAKE_ARGUMENTS+=( - "-DENABLE_KLEE_LIBCXX=TRUE" - "-DKLEE_LIBCXX_DIR=${LIBCXX_INSTALL}" -- "-DKLEE_LIBCXX_INCLUDE_DIR=${LIBCXX_INSTALL}/include/c++/v1" -+ "-DKLEE_LIBCXX_INCLUDE_DIR=${LIBCXX_INSTALL}/include/" - "-DENABLE_KLEE_EH_CXX=TRUE" - "-DKLEE_LIBCXXABI_SRC_DIR=${LIBCXX_SRC}/libcxxabi" - ) --- -2.43.0 - diff --git a/0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch b/0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch deleted file mode 100644 index c93d088..0000000 --- a/0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch +++ /dev/null @@ -1,376 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 10:32:32 +0100 -Subject: Replace `%libcxx_include` with `%libcxx_includes` for multi-include - directories -Patch-mainline: no -References: llvm16 - -To support multiple include directories for c++ header files, use -`%libcxx_includes`. This string contains the `-I` compiler directive for -each include path as well. - -Update test cases to use new directive. - -Signed-off-by: Jiri Slaby ---- - test/CXX/symex/libc++/atexit.cpp | 2 +- - test/CXX/symex/libc++/can_catch_test.cpp | 2 +- - test/CXX/symex/libc++/catch_recover.cpp | 2 +- - .../symex/libc++/catch_with_adjusted_exception_pointer.cpp | 2 +- - test/CXX/symex/libc++/cout.cpp | 2 +- - test/CXX/symex/libc++/cout_sym.cpp | 2 +- - test/CXX/symex/libc++/dynamic_cast.cpp | 2 +- - test/CXX/symex/libc++/exception.cpp | 2 +- - test/CXX/symex/libc++/exception_inheritance.cpp | 2 +- - test/CXX/symex/libc++/general_catch.cpp | 2 +- - test/CXX/symex/libc++/landingpad.cpp | 2 +- - test/CXX/symex/libc++/multi_throw.cpp | 2 +- - test/CXX/symex/libc++/multi_unwind.cpp | 2 +- - test/CXX/symex/libc++/nested.cpp | 2 +- - test/CXX/symex/libc++/nested_fail.cpp | 2 +- - test/CXX/symex/libc++/rethrow.cpp | 2 +- - test/CXX/symex/libc++/simple_exception.cpp | 2 +- - test/CXX/symex/libc++/simple_exception_fail.cpp | 2 +- - test/CXX/symex/libc++/symbolic_exception.cpp | 2 +- - test/CXX/symex/libc++/throw_specifiers.cpp | 2 +- - test/CXX/symex/libc++/throwing_exception_destructor.cpp | 2 +- - test/CXX/symex/libc++/uncaught_exception.cpp | 2 +- - test/CXX/symex/libc++/vector.cpp | 2 +- - test/lit.cfg | 5 ++++- - test/lit.site.cfg.in | 4 +++- - 25 files changed, 30 insertions(+), 25 deletions(-) - -diff --git a/test/CXX/symex/libc++/atexit.cpp b/test/CXX/symex/libc++/atexit.cpp -index fa8df475..d084958b 100644 ---- a/test/CXX/symex/libc++/atexit.cpp -+++ b/test/CXX/symex/libc++/atexit.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: uclibc --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/can_catch_test.cpp b/test/CXX/symex/libc++/can_catch_test.cpp -index c70d14a2..4c59c126 100644 ---- a/test/CXX/symex/libc++/can_catch_test.cpp -+++ b/test/CXX/symex/libc++/can_catch_test.cpp -@@ -1,7 +1,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc %t.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/catch_recover.cpp b/test/CXX/symex/libc++/catch_recover.cpp -index c77bea91..8eee326a 100644 ---- a/test/CXX/symex/libc++/catch_recover.cpp -+++ b/test/CXX/symex/libc++/catch_recover.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp b/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp -index e3bf08ad..57751b23 100644 ---- a/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp -+++ b/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp -@@ -1,7 +1,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc %t.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/cout.cpp b/test/CXX/symex/libc++/cout.cpp -index 62cd0406..d845a1ea 100644 ---- a/test/CXX/symex/libc++/cout.cpp -+++ b/test/CXX/symex/libc++/cout.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: uclibc --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/cout_sym.cpp b/test/CXX/symex/libc++/cout_sym.cpp -index 177c3ed7..69420ac9 100644 ---- a/test/CXX/symex/libc++/cout_sym.cpp -+++ b/test/CXX/symex/libc++/cout_sym.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: uclibc --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/dynamic_cast.cpp b/test/CXX/symex/libc++/dynamic_cast.cpp -index a2fc8b82..f8a039ce 100644 ---- a/test/CXX/symex/libc++/dynamic_cast.cpp -+++ b/test/CXX/symex/libc++/dynamic_cast.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: uclibc --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc - -diff --git a/test/CXX/symex/libc++/exception.cpp b/test/CXX/symex/libc++/exception.cpp -index 4d6805f6..c36db2d9 100644 ---- a/test/CXX/symex/libc++/exception.cpp -+++ b/test/CXX/symex/libc++/exception.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/exception_inheritance.cpp b/test/CXX/symex/libc++/exception_inheritance.cpp -index ca207eb4..4551bc18 100644 ---- a/test/CXX/symex/libc++/exception_inheritance.cpp -+++ b/test/CXX/symex/libc++/exception_inheritance.cpp -@@ -1,7 +1,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc %t.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/general_catch.cpp b/test/CXX/symex/libc++/general_catch.cpp -index c544f7a3..eb045d16 100644 ---- a/test/CXX/symex/libc++/general_catch.cpp -+++ b/test/CXX/symex/libc++/general_catch.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/landingpad.cpp b/test/CXX/symex/libc++/landingpad.cpp -index 13dd6bc4..c23b8ee2 100644 ---- a/test/CXX/symex/libc++/landingpad.cpp -+++ b/test/CXX/symex/libc++/landingpad.cpp -@@ -4,7 +4,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc %t.bc | FileCheck %s - // Expect the following output: -diff --git a/test/CXX/symex/libc++/multi_throw.cpp b/test/CXX/symex/libc++/multi_throw.cpp -index 52e8d9b9..626585f4 100644 ---- a/test/CXX/symex/libc++/multi_throw.cpp -+++ b/test/CXX/symex/libc++/multi_throw.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/multi_unwind.cpp b/test/CXX/symex/libc++/multi_unwind.cpp -index cf29422c..ab8d7a5c 100644 ---- a/test/CXX/symex/libc++/multi_unwind.cpp -+++ b/test/CXX/symex/libc++/multi_unwind.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/nested.cpp b/test/CXX/symex/libc++/nested.cpp -index 21222642..1273a3b9 100644 ---- a/test/CXX/symex/libc++/nested.cpp -+++ b/test/CXX/symex/libc++/nested.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/nested_fail.cpp b/test/CXX/symex/libc++/nested_fail.cpp -index d0b8ca09..4dce0279 100644 ---- a/test/CXX/symex/libc++/nested_fail.cpp -+++ b/test/CXX/symex/libc++/nested_fail.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/rethrow.cpp b/test/CXX/symex/libc++/rethrow.cpp -index 149fe693..213cb1af 100644 ---- a/test/CXX/symex/libc++/rethrow.cpp -+++ b/test/CXX/symex/libc++/rethrow.cpp -@@ -1,7 +1,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc %t.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/simple_exception.cpp b/test/CXX/symex/libc++/simple_exception.cpp -index 0196e1eb..0ca8f8ed 100644 ---- a/test/CXX/symex/libc++/simple_exception.cpp -+++ b/test/CXX/symex/libc++/simple_exception.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/simple_exception_fail.cpp b/test/CXX/symex/libc++/simple_exception_fail.cpp -index bda2cd33..793d9201 100644 ---- a/test/CXX/symex/libc++/simple_exception_fail.cpp -+++ b/test/CXX/symex/libc++/simple_exception_fail.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/symbolic_exception.cpp b/test/CXX/symex/libc++/symbolic_exception.cpp -index 3f29fa04..50d682ba 100644 ---- a/test/CXX/symex/libc++/symbolic_exception.cpp -+++ b/test/CXX/symex/libc++/symbolic_exception.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/throw_specifiers.cpp b/test/CXX/symex/libc++/throw_specifiers.cpp -index 96195cd4..efd6a0be 100644 ---- a/test/CXX/symex/libc++/throw_specifiers.cpp -+++ b/test/CXX/symex/libc++/throw_specifiers.cpp -@@ -3,7 +3,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libcxx --libc=uclibc %t.bc | FileCheck %s - -diff --git a/test/CXX/symex/libc++/throwing_exception_destructor.cpp b/test/CXX/symex/libc++/throwing_exception_destructor.cpp -index 02d7cdb9..7505027c 100644 ---- a/test/CXX/symex/libc++/throwing_exception_destructor.cpp -+++ b/test/CXX/symex/libc++/throwing_exception_destructor.cpp -@@ -2,7 +2,7 @@ - // REQUIRES: uclibc - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm -O0 -std=c++11 -c -I "%libcxx_include" -g -nostdinc++ -o %t.bc -+// RUN: %clangxx %s -emit-llvm -O0 -std=c++11 -c %libcxx_includes -g -nostdinc++ -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libcxx --libc=uclibc --exit-on-error %t.bc - -diff --git a/test/CXX/symex/libc++/uncaught_exception.cpp b/test/CXX/symex/libc++/uncaught_exception.cpp -index 848013a0..4f9444a6 100644 ---- a/test/CXX/symex/libc++/uncaught_exception.cpp -+++ b/test/CXX/symex/libc++/uncaught_exception.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: eh-cxx --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/CXX/symex/libc++/vector.cpp b/test/CXX/symex/libc++/vector.cpp -index 6f69ad65..33821b9e 100644 ---- a/test/CXX/symex/libc++/vector.cpp -+++ b/test/CXX/symex/libc++/vector.cpp -@@ -2,7 +2,7 @@ - // Disabling msan because it times out on CI - // REQUIRES: libcxx - // REQUIRES: uclibc --// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc -+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s - -diff --git a/test/lit.cfg b/test/lit.cfg -index cb47d3d4..c442c409 100644 ---- a/test/lit.cfg -+++ b/test/lit.cfg -@@ -156,8 +156,11 @@ config.substitutions.append( - ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh')) - ) - -+# Prepare the full include expression, i.e. for all given paths. For example, ["path1","path2"] -+# becomes "-I path1 -I path2" - config.substitutions.append( -- ('%libcxx_include', getattr(config, 'libcxx_include_dir', None))) -+ ('%libcxx_includes', " ".join( ["-I "+ p for p in getattr(config, 'libcxx_include_dirs', [])] )) -+ ) - - # Add feature for the LLVM version in use, so it can be tested in REQUIRES and - # XFAIL checks. We also add "not-XXX" variants, for the same reason. -diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in -index c7063057..d185982b 100644 ---- a/test/lit.site.cfg.in -+++ b/test/lit.site.cfg.in -@@ -9,7 +9,9 @@ config.klee_obj_root = "@KLEE_BINARY_DIR@" - config.klee_tools_dir = "@KLEE_TOOLS_DIR@" - config.llvm_tools_dir = "@LLVM_TOOLS_DIR@" - --config.libcxx_include_dir = "@KLEE_LIBCXX_INCLUDE_DIR@" -+config.libcxx_include_dirs = ["@KLEE_LIBCXX_INCLUDE_PATH@"] -+if len("@KLEE_LIBCXX_PLATFORM_INCLUDE_PATH@") > 0: -+ config.libcxx_include_dirs.append("@KLEE_LIBCXX_PLATFORM_INCLUDE_PATH@") - - # Needed to check if a hack needs to be applied - config.llvm_version_major = "@LLVM_VERSION_MAJOR@" --- -2.43.0 - diff --git a/0004-Fix-klee-libc-memchr.c-compiler-warning.patch b/0004-Fix-klee-libc-memchr.c-compiler-warning.patch deleted file mode 100644 index 623741e..0000000 --- a/0004-Fix-klee-libc-memchr.c-compiler-warning.patch +++ /dev/null @@ -1,47 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 10:34:01 +0100 -Subject: Fix `klee-libc/memchr.c` compiler warning -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - runtime/klee-libc/memchr.c | 23 +++++++++-------------- - 1 file changed, 9 insertions(+), 14 deletions(-) - -diff --git a/runtime/klee-libc/memchr.c b/runtime/klee-libc/memchr.c -index fe0670a7..3cd47cdf 100644 ---- a/runtime/klee-libc/memchr.c -+++ b/runtime/klee-libc/memchr.c -@@ -36,19 +36,14 @@ - - #include - --void * --memchr(s, c, n) -- const void *s; -- int c; -- size_t n; --{ -- if (n != 0) { -- const unsigned char *p = s; -+void *memchr(const void *s, int c, size_t n) { -+ if (n != 0) { -+ const unsigned char *p = s; - -- do { -- if (*p++ == c) -- return ((void *)(p - 1)); -- } while (--n != 0); -- } -- return (NULL); -+ do { -+ if (*p++ == c) -+ return ((void *)(p - 1)); -+ } while (--n != 0); -+ } -+ return (NULL); - } --- -2.43.0 - diff --git a/0005-Fix-klee_eh_cxx.cpp-compiler-error.patch b/0005-Fix-klee_eh_cxx.cpp-compiler-error.patch deleted file mode 100644 index 8e2d35a..0000000 --- a/0005-Fix-klee_eh_cxx.cpp-compiler-error.patch +++ /dev/null @@ -1,27 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 10:34:33 +0100 -Subject: Fix `klee_eh_cxx.cpp` compiler error -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - runtime/klee-eh-cxx/klee_eh_cxx.cpp | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/runtime/klee-eh-cxx/klee_eh_cxx.cpp b/runtime/klee-eh-cxx/klee_eh_cxx.cpp -index 9d86bef4..cb5e0c7c 100644 ---- a/runtime/klee-eh-cxx/klee_eh_cxx.cpp -+++ b/runtime/klee-eh-cxx/klee_eh_cxx.cpp -@@ -90,7 +90,7 @@ get_thrown_object_ptr(_Unwind_Exception* unwind_exception) - // Our implementation of a personality function for handling - // libcxxabi-exceptions. Follows how libcxxabi's __gxx_personality_v0 handles - // exceptions. --[[gnu::used]] extern "C" std::int32_t -+extern "C" std::int32_t - _klee_eh_cxx_personality(_Unwind_Exception *exceptionPointer, - const std::size_t num_bytes, - const unsigned char *lp_clauses) { --- -2.43.0 - diff --git a/0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch b/0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch deleted file mode 100644 index e9958dc..0000000 --- a/0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch +++ /dev/null @@ -1,1001 +0,0 @@ -From: Martin Nowack -Date: Thu, 12 Oct 2023 11:16:18 +0100 -Subject: Refactor invocation of old pass manager into legacy function -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - lib/Module/CMakeLists.txt | 14 +- - lib/Module/Instrument.cpp | 19 +++ - lib/Module/InstrumentLegacy.cpp | 125 ++++++++++++++++ - lib/Module/KModule.cpp | 139 +++--------------- - lib/Module/ModuleHelper.h | 37 +++++ - lib/Module/Optimize.cpp | 249 +------------------------------- - lib/Module/OptimizeLegacy.cpp | 249 ++++++++++++++++++++++++++++++++ - 7 files changed, 475 insertions(+), 357 deletions(-) - create mode 100644 lib/Module/Instrument.cpp - create mode 100644 lib/Module/InstrumentLegacy.cpp - create mode 100644 lib/Module/ModuleHelper.h - create mode 100644 lib/Module/OptimizeLegacy.cpp - -diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt -index e1f548e8..71e1d40c 100644 ---- a/lib/Module/CMakeLists.txt -+++ b/lib/Module/CMakeLists.txt -@@ -16,12 +16,24 @@ set(KLEE_MODULE_COMPONENT_SRCS - KModule.cpp - LowerSwitch.cpp - ModuleUtil.cpp -- Optimize.cpp - OptNone.cpp - PhiCleaner.cpp - RaiseAsm.cpp - ) - -+if ("${LLVM_VERSION_MAJOR}" LESS 17) -+ LIST(APPEND KLEE_MODULE_COMPONENT_SRCS -+ InstrumentLegacy.cpp -+ OptimizeLegacy.cpp -+ ) -+else () -+ LIST(APPEND KLEE_MODULE_COMPONENT_SRCS -+ Instrument.cpp -+ Optimize.cpp -+ ) -+endif () -+ -+ - add_library(kleeModule - ${KLEE_MODULE_COMPONENT_SRCS} - ) -diff --git a/lib/Module/Instrument.cpp b/lib/Module/Instrument.cpp -new file mode 100644 -index 00000000..bbb5df7c ---- /dev/null -+++ b/lib/Module/Instrument.cpp -@@ -0,0 +1,19 @@ -+//===-- Instrument.cpp ------------------------------------------*- C++ -*-===// -+// -+// The KLEE Symbolic Virtual Machine -+// -+// This file is distributed under the University of Illinois Open Source -+// License. See LICENSE.TXT for details. -+// -+//===----------------------------------------------------------------------===// -+ -+#include "ModuleHelper.h" -+ -+using namespace klee; -+ -+void klee::checkModule(bool DontVerfify, llvm::Module *module) { assert(0); } -+ -+void klee::instrument(bool CheckDivZero, bool CheckOvershift, -+ llvm::Module *module) { -+ assert(0); -+} -\ No newline at end of file -diff --git a/lib/Module/InstrumentLegacy.cpp b/lib/Module/InstrumentLegacy.cpp -new file mode 100644 -index 00000000..daae8043 ---- /dev/null -+++ b/lib/Module/InstrumentLegacy.cpp -@@ -0,0 +1,125 @@ -+//===-- InstrumentLegacy.cpp ------------------------------------*- C++ -*-===// -+// -+// The KLEE Symbolic Virtual Machine -+// -+// This file is distributed under the University of Illinois Open Source -+// License. See LICENSE.TXT for details. -+// -+//===----------------------------------------------------------------------===// -+#include "ModuleHelper.h" -+ -+#include "Passes.h" -+#include "klee/Support/CompilerWarning.h" -+#include "klee/Support/ErrorHandling.h" -+ -+DISABLE_WARNING_PUSH -+DISABLE_WARNING_DEPRECATED_DECLARATIONS -+#include "llvm/Bitcode/BitcodeWriter.h" -+#include "llvm/IR/DataLayout.h" -+#include "llvm/IR/IRBuilder.h" -+#include "llvm/IR/LLVMContext.h" -+#include "llvm/IR/LegacyPassManager.h" -+#include "llvm/IR/Module.h" -+#include "llvm/IR/ValueSymbolTable.h" -+#include "llvm/IR/Verifier.h" -+#include "llvm/Support/CommandLine.h" -+#include "llvm/Transforms/Scalar.h" -+#include "llvm/Transforms/Scalar/Scalarizer.h" -+#include "llvm/Transforms/Utils.h" -+#include "llvm/Transforms/Utils/Cloning.h" -+DISABLE_WARNING_POP -+ -+using namespace llvm; -+using namespace klee; -+ -+void klee::instrument(bool CheckDivZero, bool CheckOvershift, -+ llvm::Module *module) { -+ // Inject checks prior to optimization... we also perform the -+ // invariant transformations that we will end up doing later so that -+ // optimize is seeing what is as close as possible to the final -+ // module. -+ legacy::PassManager pm; -+ pm.add(new RaiseAsmPass()); -+ -+ // This pass will scalarize as much code as possible so that the Executor -+ // does not need to handle operands of vector type for most instructions -+ // other than InsertElementInst and ExtractElementInst. -+ // -+ // NOTE: Must come before division/overshift checks because those passes -+ // don't know how to handle vector instructions. -+ pm.add(createScalarizerPass()); -+ -+ // This pass will replace atomic instructions with non-atomic operations -+ pm.add(createLowerAtomicPass()); -+ if (CheckDivZero) -+ pm.add(new DivCheckPass()); -+ if (CheckOvershift) -+ pm.add(new OvershiftCheckPass()); -+ -+ llvm::DataLayout targetData(module); -+ pm.add(new IntrinsicCleanerPass(targetData)); -+ pm.run(*module); -+} -+ -+void klee::checkModule(bool DontVerify, llvm::Module *module) { -+ InstructionOperandTypeCheckPass *operandTypeCheckPass = -+ new InstructionOperandTypeCheckPass(); -+ -+ legacy::PassManager pm; -+ if (!DontVerify) -+ pm.add(createVerifierPass()); -+ pm.add(operandTypeCheckPass); -+ pm.run(*module); -+ -+ // Enforce the operand type invariants that the Executor expects. This -+ // implicitly depends on the "Scalarizer" pass to be run in order to succeed -+ // in the presence of vector instructions. -+ if (!operandTypeCheckPass->checkPassed()) { -+ klee_error("Unexpected instruction operand types detected"); -+ } -+} -+ -+void klee::optimiseAndPrepare(bool OptimiseKLEECall, bool Optimize, -+ SwitchImplType SwitchType, std::string EntryPoint, -+ llvm::ArrayRef preservedFunctions, -+ llvm::Module *module) { -+ // Preserve all functions containing klee-related function calls from being -+ // optimised around -+ if (!OptimiseKLEECall) { -+ legacy::PassManager pm; -+ pm.add(new OptNonePass()); -+ pm.run(*module); -+ } -+ -+ if (Optimize) -+ optimizeModule(module, preservedFunctions); -+ -+ // Needs to happen after linking (since ctors/dtors can be modified) -+ // and optimization (since global optimization can rewrite lists). -+ injectStaticConstructorsAndDestructors(module, EntryPoint); -+ -+ // Finally, run the passes that maintain invariants we expect during -+ // interpretation. We run the intrinsic cleaner just in case we -+ // linked in something with intrinsics but any external calls are -+ // going to be unresolved. We really need to handle the intrinsics -+ // directly I think? -+ legacy::PassManager pm3; -+ pm3.add(createCFGSimplificationPass()); -+ switch (SwitchType) { -+ case SwitchImplType::eSwitchTypeInternal: -+ break; -+ case SwitchImplType::eSwitchTypeSimple: -+ pm3.add(new LowerSwitchPass()); -+ break; -+ case SwitchImplType::eSwitchTypeLLVM: -+ pm3.add(createLowerSwitchPass()); -+ break; -+ } -+ -+ llvm::DataLayout targetData(module); -+ pm3.add(new IntrinsicCleanerPass(targetData)); -+ pm3.add(createScalarizerPass()); -+ pm3.add(new PhiCleanerPass()); -+ pm3.add(new FunctionAliasPass()); -+ pm3.run(*module); -+} -\ No newline at end of file -diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp -index eed922f8..cb8b4539 100644 ---- a/lib/Module/KModule.cpp -+++ b/lib/Module/KModule.cpp -@@ -9,40 +9,27 @@ - - #define DEBUG_TYPE "KModule" - -+#include "klee/Module/KModule.h" -+ -+#include "ModuleHelper.h" - #include "Passes.h" - - #include "klee/Config/Version.h" - #include "klee/Core/Interpreter.h" --#include "klee/Support/OptionCategories.h" - #include "klee/Module/Cell.h" - #include "klee/Module/InstructionInfoTable.h" - #include "klee/Module/KInstruction.h" --#include "klee/Module/KModule.h" - #include "klee/Support/Debug.h" - #include "klee/Support/ErrorHandling.h" - #include "klee/Support/ModuleUtil.h" -+#include "klee/Support/OptionCategories.h" - - #include "klee/Support/CompilerWarning.h" -+ - DISABLE_WARNING_PUSH - DISABLE_WARNING_DEPRECATED_DECLARATIONS - #include "llvm/Bitcode/BitcodeWriter.h" --#include "llvm/IR/DataLayout.h" - #include "llvm/IR/IRBuilder.h" --#include "llvm/IR/Instructions.h" --#include "llvm/IR/LegacyPassManager.h" --#include "llvm/IR/LLVMContext.h" --#include "llvm/IR/Module.h" --#include "llvm/IR/ValueSymbolTable.h" --#include "llvm/IR/Verifier.h" --#include "llvm/Linker/Linker.h" --#include "llvm/Support/CommandLine.h" --#include "llvm/Support/Path.h" --#include "llvm/Support/raw_ostream.h" --#include "llvm/Support/raw_os_ostream.h" --#include "llvm/Transforms/Scalar.h" --#include "llvm/Transforms/Scalar/Scalarizer.h" --#include "llvm/Transforms/Utils/Cloning.h" --#include "llvm/Transforms/Utils.h" - DISABLE_WARNING_POP - - #include -@@ -57,12 +44,6 @@ cl::OptionCategory - } - - namespace { -- enum SwitchImplType { -- eSwitchTypeSimple, -- eSwitchTypeLLVM, -- eSwitchTypeInternal -- }; -- - cl::opt - OutputSource("output-source", - cl::desc("Write the assembly for the final transformed source (default=true)"), -@@ -75,16 +56,6 @@ namespace { - cl::init(false), - cl::cat(ModuleCat)); - -- cl::opt -- SwitchType("switch-type", cl::desc("Select the implementation of switch (default=internal)"), -- cl::values(clEnumValN(eSwitchTypeSimple, "simple", -- "lower to ordered branches"), -- clEnumValN(eSwitchTypeLLVM, "llvm", -- "lower using LLVM"), -- clEnumValN(eSwitchTypeInternal, "internal", -- "execute switch internally")), -- cl::init(eSwitchTypeInternal), -- cl::cat(ModuleCat)); - - cl::opt - DebugPrintEscapingFunctions("debug-print-escaping-functions", -@@ -102,14 +73,21 @@ namespace { - cl::desc("Allow optimization of functions that " - "contain KLEE calls (default=true)"), - cl::init(true), cl::cat(ModuleCat)); --} -+cl::opt SwitchType( -+ "switch-type", -+ cl::desc("Select the implementation of switch (default=internal)"), -+ cl::values(clEnumValN(SwitchImplType::eSwitchTypeSimple, "simple", -+ "lower to ordered branches"), -+ clEnumValN(SwitchImplType::eSwitchTypeLLVM, "llvm", -+ "lower using LLVM"), -+ clEnumValN(SwitchImplType::eSwitchTypeInternal, "internal", -+ "execute switch internally")), -+ cl::init(SwitchImplType::eSwitchTypeInternal), cl::cat(ModuleCat)); -+ -+} // namespace - - /***/ - --namespace llvm { --extern void Optimize(Module *, llvm::ArrayRef preservedFunctions); --} -- - // what a hack - static Function *getStubFunctionForCtorList(Module *m, - GlobalVariable *gv, -@@ -156,9 +134,8 @@ static Function *getStubFunctionForCtorList(Module *m, - return fn; - } - --static void --injectStaticConstructorsAndDestructors(Module *m, -- llvm::StringRef entryFunction) { -+void klee::injectStaticConstructorsAndDestructors( -+ Module *m, llvm::StringRef entryFunction) { - GlobalVariable *ctors = m->getNamedGlobal("llvm.global_ctors"); - GlobalVariable *dtors = m->getNamedGlobal("llvm.global_dtors"); - -@@ -216,44 +193,12 @@ bool KModule::link(std::vector> &modules, - } - - void KModule::instrument(const Interpreter::ModuleOptions &opts) { -- // Inject checks prior to optimization... we also perform the -- // invariant transformations that we will end up doing later so that -- // optimize is seeing what is as close as possible to the final -- // module. -- legacy::PassManager pm; -- pm.add(new RaiseAsmPass()); -- -- // This pass will scalarize as much code as possible so that the Executor -- // does not need to handle operands of vector type for most instructions -- // other than InsertElementInst and ExtractElementInst. -- // -- // NOTE: Must come before division/overshift checks because those passes -- // don't know how to handle vector instructions. -- pm.add(createScalarizerPass()); -- -- // This pass will replace atomic instructions with non-atomic operations -- pm.add(createLowerAtomicPass()); -- if (opts.CheckDivZero) pm.add(new DivCheckPass()); -- if (opts.CheckOvershift) pm.add(new OvershiftCheckPass()); -- -- pm.add(new IntrinsicCleanerPass(*targetData)); -- pm.run(*module); -+ klee::instrument(opts.CheckDivZero, opts.CheckOvershift, module.get()); - } - - void KModule::optimiseAndPrepare( - const Interpreter::ModuleOptions &opts, - llvm::ArrayRef preservedFunctions) { -- // Preserve all functions containing klee-related function calls from being -- // optimised around -- if (!OptimiseKLEECall) { -- legacy::PassManager pm; -- pm.add(new OptNonePass()); -- pm.run(*module); -- } -- -- if (opts.Optimize) -- Optimize(module.get(), preservedFunctions); -- - // Add internal functions which are not used to check if instructions - // have been already visited - if (opts.CheckDivZero) -@@ -261,28 +206,8 @@ void KModule::optimiseAndPrepare( - if (opts.CheckOvershift) - addInternalFunction("klee_overshift_check"); - -- // Needs to happen after linking (since ctors/dtors can be modified) -- // and optimization (since global optimization can rewrite lists). -- injectStaticConstructorsAndDestructors(module.get(), opts.EntryPoint); -- -- // Finally, run the passes that maintain invariants we expect during -- // interpretation. We run the intrinsic cleaner just in case we -- // linked in something with intrinsics but any external calls are -- // going to be unresolved. We really need to handle the intrinsics -- // directly I think? -- legacy::PassManager pm3; -- pm3.add(createCFGSimplificationPass()); -- switch(SwitchType) { -- case eSwitchTypeInternal: break; -- case eSwitchTypeSimple: pm3.add(new LowerSwitchPass()); break; -- case eSwitchTypeLLVM: pm3.add(createLowerSwitchPass()); break; -- default: klee_error("invalid --switch-type"); -- } -- pm3.add(new IntrinsicCleanerPass(*targetData)); -- pm3.add(createScalarizerPass()); -- pm3.add(new PhiCleanerPass()); -- pm3.add(new FunctionAliasPass()); -- pm3.run(*module); -+ klee::optimiseAndPrepare(OptimiseKLEECall, opts.Optimize, SwitchType, -+ opts.EntryPoint, preservedFunctions, module.get()); - } - - void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) { -@@ -294,7 +219,7 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) { - - if (OutputModule) { - std::unique_ptr f(ih->openOutputFile("final.bc")); -- WriteBitcodeToFile(*module, *f); -+ llvm::WriteBitcodeToFile(*module, *f); - } - - /* Build shadow structures */ -@@ -343,23 +268,7 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) { - } - } - --void KModule::checkModule() { -- InstructionOperandTypeCheckPass *operandTypeCheckPass = -- new InstructionOperandTypeCheckPass(); -- -- legacy::PassManager pm; -- if (!DontVerify) -- pm.add(createVerifierPass()); -- pm.add(operandTypeCheckPass); -- pm.run(*module); -- -- // Enforce the operand type invariants that the Executor expects. This -- // implicitly depends on the "Scalarizer" pass to be run in order to succeed -- // in the presence of vector instructions. -- if (!operandTypeCheckPass->checkPassed()) { -- klee_error("Unexpected instruction operand types detected"); -- } --} -+void KModule::checkModule() { klee::checkModule(DontVerify, module.get()); } - - KConstant* KModule::getKConstant(const Constant *c) { - auto it = constantMap.find(c); -diff --git a/lib/Module/ModuleHelper.h b/lib/Module/ModuleHelper.h -new file mode 100644 -index 00000000..1b279edd ---- /dev/null -+++ b/lib/Module/ModuleHelper.h -@@ -0,0 +1,37 @@ -+//===-- ModuleHelper.h ------------------------------------------*- C++ -*-===// -+// -+// The KLEE Symbolic Virtual Machine -+// -+// This file is distributed under the University of Illinois Open Source -+// License. See LICENSE.TXT for details. -+// -+//===----------------------------------------------------------------------===// -+ -+#ifndef KLEE_MODULEHELPER_H -+#define KLEE_MODULEHELPER_H -+ -+#include "llvm/ADT/ArrayRef.h" -+#include "llvm/IR/Module.h" -+ -+namespace klee { -+enum class SwitchImplType { -+ eSwitchTypeSimple, -+ eSwitchTypeLLVM, -+ eSwitchTypeInternal -+}; -+ -+void optimiseAndPrepare(bool OptimiseKLEECall, bool Optimize, -+ SwitchImplType SwitchType, std::string EntryPoint, -+ llvm::ArrayRef preservedFunctions, -+ llvm::Module *module); -+void checkModule(bool DontVerfify, llvm::Module *module); -+void instrument(bool CheckDivZero, bool CheckOvershift, llvm::Module *module); -+ -+void injectStaticConstructorsAndDestructors(llvm::Module *m, -+ llvm::StringRef entryFunction); -+ -+void optimizeModule(llvm::Module *M, -+ llvm::ArrayRef preservedFunctions); -+} // namespace klee -+ -+#endif // KLEE_MODULEHELPER_H -diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp -index 35b9805a..9475512b 100644 ---- a/lib/Module/Optimize.cpp -+++ b/lib/Module/Optimize.cpp -@@ -15,247 +15,14 @@ - // - //===----------------------------------------------------------------------===// - --#include "klee/Config/Version.h" --#include "klee/Support/OptionCategories.h" -+#include "ModuleHelper.h" - --#include "klee/Support/CompilerWarning.h" --DISABLE_WARNING_PUSH --DISABLE_WARNING_DEPRECATED_DECLARATIONS --#include "llvm/Analysis/GlobalsModRef.h" --#include "llvm/Analysis/Passes.h" --#include "llvm/Analysis/LoopPass.h" - #include "llvm/IR/Module.h" --#include "llvm/IR/DataLayout.h" --#include "llvm/IR/LegacyPassManager.h" --#include "llvm/IR/Verifier.h" --#include "llvm/Support/CommandLine.h" --#include "llvm/Support/DynamicLibrary.h" --#include "llvm/Support/PluginLoader.h" --#include "llvm/Target/TargetMachine.h" --#include "llvm/Transforms/InstCombine/InstCombine.h" --#include "llvm/Transforms/IPO.h" --#include "llvm/Transforms/IPO/FunctionAttrs.h" --#include "llvm/Transforms/Scalar.h" --#include "llvm/Transforms/Scalar/GVN.h" --#include "llvm/Transforms/Utils.h" --DISABLE_WARNING_POP - --using namespace llvm; -- --static cl::opt -- DisableInline("disable-inlining", -- cl::desc("Do not run the inliner pass (default=false)"), -- cl::init(false), cl::cat(klee::ModuleCat)); -- --static cl::opt DisableInternalize( -- "disable-internalize", -- cl::desc("Do not mark all symbols as internal (default=false)"), -- cl::init(false), cl::cat(klee::ModuleCat)); -- --static cl::opt VerifyEach( -- "verify-each", -- cl::desc("Verify intermediate results of all optimization passes (default=false)"), -- cl::init(false), -- cl::cat(klee::ModuleCat)); -- --static cl::alias ExportDynamic("export-dynamic", -- cl::aliasopt(DisableInternalize), -- cl::desc("Alias for -disable-internalize")); -- --static cl::opt -- Strip("strip-all", cl::desc("Strip all symbol information from executable"), -- cl::init(false), cl::cat(klee::ModuleCat)); -- --static cl::alias A0("s", cl::desc("Alias for --strip-all"), -- cl::aliasopt(Strip)); -- --static cl::opt -- StripDebug("strip-debug", -- cl::desc("Strip debugger symbol info from executable"), -- cl::init(false), cl::cat(klee::ModuleCat)); -- --static cl::alias A1("S", cl::desc("Alias for --strip-debug"), -- cl::aliasopt(StripDebug)); -- --// A utility function that adds a pass to the pass manager but will also add --// a verifier pass after if we're supposed to verify. --static inline void addPass(legacy::PassManager &PM, Pass *P) { -- // Add the pass to the pass manager... -- PM.add(P); -- -- // If we are verifying all of the intermediate steps, add the verifier... -- if (VerifyEach) -- PM.add(createVerifierPass()); --} -- --namespace llvm { -- -- --static void AddStandardCompilePasses(legacy::PassManager &PM) { -- PM.add(createVerifierPass()); // Verify that input is correct -- -- // If the -strip-debug command line option was specified, do it. -- if (StripDebug) -- addPass(PM, createStripSymbolsPass(true)); -- -- addPass(PM, createCFGSimplificationPass()); // Clean up disgusting code -- addPass(PM, createPromoteMemoryToRegisterPass());// Kill useless allocas -- addPass(PM, createGlobalOptimizerPass()); // Optimize out global vars -- addPass(PM, createGlobalDCEPass()); // Remove unused fns and globs --#if LLVM_VERSION_CODE >= LLVM_VERSION(11, 0) -- addPass(PM, createSCCPPass()); // Constant prop with SCCP --#else -- addPass(PM, createIPConstantPropagationPass());// IP Constant Propagation --#endif -- addPass(PM, createDeadArgEliminationPass()); // Dead argument elimination -- addPass(PM, createInstructionCombiningPass()); // Clean up after IPCP & DAE -- addPass(PM, createCFGSimplificationPass()); // Clean up after IPCP & DAE -- -- addPass(PM, createPruneEHPass()); // Remove dead EH info -- addPass(PM, createPostOrderFunctionAttrsLegacyPass()); -- addPass(PM, createReversePostOrderFunctionAttrsPass()); // Deduce function attrs -- -- if (!DisableInline) -- addPass(PM, createFunctionInliningPass()); // Inline small functions -- addPass(PM, createArgumentPromotionPass()); // Scalarize uninlined fn args -- -- addPass(PM, createInstructionCombiningPass()); // Cleanup for scalarrepl. -- addPass(PM, createJumpThreadingPass()); // Thread jumps. -- addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -- addPass(PM, createSROAPass()); // Break up aggregate allocas -- addPass(PM, createInstructionCombiningPass()); // Combine silly seq's -- -- addPass(PM, createTailCallEliminationPass()); // Eliminate tail calls -- addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -- addPass(PM, createReassociatePass()); // Reassociate expressions -- addPass(PM, createLoopRotatePass()); -- addPass(PM, createLICMPass()); // Hoist loop invariants -- addPass(PM, createLoopUnswitchPass()); // Unswitch loops. -- // FIXME : Removing instcombine causes nestedloop regression. -- addPass(PM, createInstructionCombiningPass()); -- addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars -- addPass(PM, createLoopDeletionPass()); // Delete dead loops -- addPass(PM, createLoopUnrollPass()); // Unroll small loops -- addPass(PM, createInstructionCombiningPass()); // Clean up after the unroller -- addPass(PM, createGVNPass()); // Remove redundancies -- addPass(PM, createMemCpyOptPass()); // Remove memcpy / form memset -- addPass(PM, createSCCPPass()); // Constant prop with SCCP -- -- // Run instcombine after redundancy elimination to exploit opportunities -- // opened up by them. -- addPass(PM, createInstructionCombiningPass()); -- -- addPass(PM, createDeadStoreEliminationPass()); // Delete dead stores -- addPass(PM, createAggressiveDCEPass()); // Delete dead instructions -- addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -- addPass(PM, createStripDeadPrototypesPass()); // Get rid of dead prototypes -- addPass(PM, createConstantMergePass()); // Merge dup global constants --} -- --/// Optimize - Perform link time optimizations. This will run the scalar --/// optimizations, any loaded plugin-optimization modules, and then the --/// inter-procedural optimizations if applicable. --void Optimize(Module *M, llvm::ArrayRef preservedFunctions) { -- -- // Instantiate the pass manager to organize the passes. -- legacy::PassManager Passes; -- -- // If we're verifying, start off with a verification pass. -- if (VerifyEach) -- Passes.add(createVerifierPass()); -- -- // DWD - Run the opt standard pass list as well. -- AddStandardCompilePasses(Passes); -- -- // Now that composite has been compiled, scan through the module, looking -- // for a main function. If main is defined, mark all other functions -- // internal. -- if (!DisableInternalize) { -- auto PreserveFunctions = [=](const GlobalValue &GV) { -- StringRef GVName = GV.getName(); -- -- for (const char *fun : preservedFunctions) -- if (GVName.equals(fun)) -- return true; -- -- return false; -- }; -- ModulePass *pass = createInternalizePass(PreserveFunctions); -- addPass(Passes, pass); -- } -- -- // Propagate constants at call sites into the functions they call. This -- // opens opportunities for globalopt (and inlining) by substituting function -- // pointers passed as arguments to direct uses of functions. -- addPass(Passes, createIPSCCPPass()); -- -- // Now that we internalized some globals, see if we can hack on them! -- addPass(Passes, createGlobalOptimizerPass()); -- -- // Linking modules together can lead to duplicated global constants, only -- // keep one copy of each constant... -- addPass(Passes, createConstantMergePass()); -- -- // Remove unused arguments from functions... -- addPass(Passes, createDeadArgEliminationPass()); -- -- // Reduce the code after globalopt and ipsccp. Both can open up significant -- // simplification opportunities, and both can propagate functions through -- // function pointers. When this happens, we often have to resolve varargs -- // calls, etc, so let instcombine do this. -- addPass(Passes, createInstructionCombiningPass()); -- -- if (!DisableInline) -- addPass(Passes, createFunctionInliningPass()); // Inline small functions -- -- addPass(Passes, createPruneEHPass()); // Remove dead EH info -- addPass(Passes, createGlobalOptimizerPass()); // Optimize globals again. -- addPass(Passes, createGlobalDCEPass()); // Remove dead functions -- -- // If we didn't decide to inline a function, check to see if we can -- // transform it to pass arguments by value instead of by reference. -- addPass(Passes, createArgumentPromotionPass()); -- -- // The IPO passes may leave cruft around. Clean up after them. -- addPass(Passes, createInstructionCombiningPass()); -- addPass(Passes, createJumpThreadingPass()); // Thread jumps. -- addPass(Passes, createSROAPass()); // Break up allocas -- -- // Run a few AA driven optimizations here and now, to cleanup the code. -- addPass(Passes, createPostOrderFunctionAttrsLegacyPass()); -- addPass(Passes, createReversePostOrderFunctionAttrsPass()); // Add nocapture -- addPass(Passes, createGlobalsAAWrapperPass()); // IP alias analysis -- -- addPass(Passes, createLICMPass()); // Hoist loop invariants -- addPass(Passes, createGVNPass()); // Remove redundancies -- addPass(Passes, createMemCpyOptPass()); // Remove dead memcpy's -- addPass(Passes, createDeadStoreEliminationPass()); // Nuke dead stores -- -- // Cleanup and simplify the code after the scalar optimizations. -- addPass(Passes, createInstructionCombiningPass()); -- -- addPass(Passes, createJumpThreadingPass()); // Thread jumps. -- addPass(Passes, createPromoteMemoryToRegisterPass()); // Cleanup jumpthread. -- -- // Delete basic blocks, which optimization passes may have killed... -- addPass(Passes, createCFGSimplificationPass()); -- -- // Now that we have optimized the program, discard unreachable functions... -- addPass(Passes, createGlobalDCEPass()); -- -- // If the -s or -S command line options were specified, strip the symbols out -- // of the resulting program to make it smaller. -s and -S are GNU ld options -- // that we are supporting; they alias -strip-all and -strip-debug. -- if (Strip || StripDebug) -- addPass(Passes, createStripSymbolsPass(StripDebug && !Strip)); -- -- // The user's passes may leave cruft around; clean up after them. -- addPass(Passes, createInstructionCombiningPass()); -- addPass(Passes, createCFGSimplificationPass()); -- addPass(Passes, createAggressiveDCEPass()); -- addPass(Passes, createGlobalDCEPass()); -- -- // Run our queue of passes all at once now, efficiently. -- Passes.run(*M); --} --} -+using namespace klee; -+void klee::optimiseAndPrepare(bool OptimiseKLEECall, bool Optimize, -+ SwitchImplType SwitchType, std::string EntryPoint, -+ llvm::ArrayRef preservedFunctions, -+ llvm::Module *module) { -+ assert(0); -+} -\ No newline at end of file -diff --git a/lib/Module/OptimizeLegacy.cpp b/lib/Module/OptimizeLegacy.cpp -new file mode 100644 -index 00000000..53488924 ---- /dev/null -+++ b/lib/Module/OptimizeLegacy.cpp -@@ -0,0 +1,249 @@ -+// FIXME: This file is a bastard child of opt.cpp and llvm-ld's -+// Optimize.cpp. This stuff should live in common code. -+ -+//===- Optimize.cpp - Optimize a complete program -------------------------===// -+// -+// The LLVM Compiler Infrastructure -+// -+// This file is distributed under the University of Illinois Open Source -+// License. See LICENSE.TXT for details. -+// -+//===----------------------------------------------------------------------===// -+// -+// This file implements all optimization of the linked module for llvm-ld. -+// -+//===----------------------------------------------------------------------===// -+ -+#include "klee/Config/Version.h" -+#include "klee/Support/OptionCategories.h" -+ -+#include "klee/Support/CompilerWarning.h" -+ -+#include "ModuleHelper.h" -+ -+DISABLE_WARNING_PUSH -+DISABLE_WARNING_DEPRECATED_DECLARATIONS -+#include "llvm/Analysis/GlobalsModRef.h" -+#include "llvm/Analysis/LoopPass.h" -+#include "llvm/IR/LegacyPassManager.h" -+#include "llvm/IR/Module.h" -+#include "llvm/IR/Verifier.h" -+#include "llvm/Support/CommandLine.h" -+#include "llvm/Target/TargetMachine.h" -+#include "llvm/Transforms/IPO.h" -+#include "llvm/Transforms/IPO/FunctionAttrs.h" -+#include "llvm/Transforms/InstCombine/InstCombine.h" -+#include "llvm/Transforms/Scalar.h" -+#include "llvm/Transforms/Scalar/GVN.h" -+#include "llvm/Transforms/Utils.h" -+DISABLE_WARNING_POP -+ -+using namespace llvm; -+using namespace klee; -+ -+namespace { -+static cl::opt -+ DisableInline("disable-inlining", -+ cl::desc("Do not run the inliner pass (default=false)"), -+ cl::init(false), cl::cat(klee::ModuleCat)); -+ -+static cl::opt DisableInternalize( -+ "disable-internalize", -+ cl::desc("Do not mark all symbols as internal (default=false)"), -+ cl::init(false), cl::cat(klee::ModuleCat)); -+ -+static cl::opt VerifyEach("verify-each", -+ cl::desc("Verify intermediate results of all " -+ "optimization passes (default=false)"), -+ cl::init(false), cl::cat(klee::ModuleCat)); -+ -+static cl::opt -+ Strip("strip-all", cl::desc("Strip all symbol information from executable"), -+ cl::init(false), cl::cat(klee::ModuleCat)); -+ -+static cl::opt -+ StripDebug("strip-debug", -+ cl::desc("Strip debugger symbol info from executable"), -+ cl::init(false), cl::cat(klee::ModuleCat)); -+ -+// A utility function that adds a pass to the pass manager but will also add -+// a verifier pass after if we're supposed to verify. -+static inline void addPass(legacy::PassManager &PM, Pass *P) { -+ // Add the pass to the pass manager... -+ PM.add(P); -+ -+ // If we are verifying all of the intermediate steps, add the verifier... -+ if (VerifyEach) -+ PM.add(createVerifierPass()); -+} -+} // namespace -+ -+static void AddStandardCompilePasses(legacy::PassManager &PM) { -+ PM.add(createVerifierPass()); // Verify that input is correct -+ -+ // If the -strip-debug command line option was specified, do it. -+ if (StripDebug) -+ addPass(PM, createStripSymbolsPass(true)); -+ -+ addPass(PM, createCFGSimplificationPass()); // Clean up disgusting code -+ addPass(PM, createPromoteMemoryToRegisterPass()); // Kill useless allocas -+ addPass(PM, createGlobalOptimizerPass()); // Optimize out global vars -+ addPass(PM, createGlobalDCEPass()); // Remove unused fns and globs -+#if LLVM_VERSION_CODE >= LLVM_VERSION(11, 0) -+ addPass(PM, createSCCPPass()); // Constant prop with SCCP -+#else -+ addPass(PM, createIPConstantPropagationPass()); // IP Constant Propagation -+#endif -+ addPass(PM, createDeadArgEliminationPass()); // Dead argument elimination -+ addPass(PM, createInstructionCombiningPass()); // Clean up after IPCP & DAE -+ addPass(PM, createCFGSimplificationPass()); // Clean up after IPCP & DAE -+ -+ addPass(PM, createPruneEHPass()); // Remove dead EH info -+ addPass(PM, createPostOrderFunctionAttrsLegacyPass()); -+ addPass(PM, -+ createReversePostOrderFunctionAttrsPass()); // Deduce function attrs -+ -+ if (!DisableInline) -+ addPass(PM, createFunctionInliningPass()); // Inline small functions -+ addPass(PM, createArgumentPromotionPass()); // Scalarize uninlined fn args -+ -+ addPass(PM, createInstructionCombiningPass()); // Cleanup for scalarrepl. -+ addPass(PM, createJumpThreadingPass()); // Thread jumps. -+ addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -+ addPass(PM, createSROAPass()); // Break up aggregate allocas -+ addPass(PM, createInstructionCombiningPass()); // Combine silly seq's -+ -+ addPass(PM, createTailCallEliminationPass()); // Eliminate tail calls -+ addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -+ addPass(PM, createReassociatePass()); // Reassociate expressions -+ addPass(PM, createLoopRotatePass()); -+ addPass(PM, createLICMPass()); // Hoist loop invariants -+ addPass(PM, createLoopUnswitchPass()); // Unswitch loops. -+ // FIXME : Removing instcombine causes nestedloop regression. -+ addPass(PM, createInstructionCombiningPass()); -+ addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars -+ addPass(PM, createLoopDeletionPass()); // Delete dead loops -+ addPass(PM, createLoopUnrollPass()); // Unroll small loops -+ addPass(PM, createInstructionCombiningPass()); // Clean up after the unroller -+ addPass(PM, createGVNPass()); // Remove redundancies -+ addPass(PM, createMemCpyOptPass()); // Remove memcpy / form memset -+ addPass(PM, createSCCPPass()); // Constant prop with SCCP -+ -+ // Run instcombine after redundancy elimination to exploit opportunities -+ // opened up by them. -+ addPass(PM, createInstructionCombiningPass()); -+ -+ addPass(PM, createDeadStoreEliminationPass()); // Delete dead stores -+ addPass(PM, createAggressiveDCEPass()); // Delete dead instructions -+ addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs -+ addPass(PM, createStripDeadPrototypesPass()); // Get rid of dead prototypes -+ addPass(PM, createConstantMergePass()); // Merge dup global constants -+} -+ -+/// Optimize - Perform link time optimizations. This will run the scalar -+/// optimizations, any loaded plugin-optimization modules, and then the -+/// inter-procedural optimizations if applicable. -+void klee::optimizeModule(llvm::Module *M, -+ llvm::ArrayRef preservedFunctions) { -+ -+ // Instantiate the pass manager to organize the passes. -+ legacy::PassManager Passes; -+ -+ // If we're verifying, start off with a verification pass. -+ if (VerifyEach) -+ Passes.add(createVerifierPass()); -+ -+ // DWD - Run the opt standard pass list as well. -+ AddStandardCompilePasses(Passes); -+ -+ // Now that composite has been compiled, scan through the module, looking -+ // for a main function. If main is defined, mark all other functions -+ // internal. -+ if (!DisableInternalize) { -+ auto PreserveFunctions = [=](const llvm::GlobalValue &GV) { -+ StringRef GVName = GV.getName(); -+ -+ for (const char *fun : preservedFunctions) -+ if (GVName.equals(fun)) -+ return true; -+ -+ return false; -+ }; -+ ModulePass *pass = createInternalizePass(PreserveFunctions); -+ addPass(Passes, pass); -+ } -+ -+ // Propagate constants at call sites into the functions they call. This -+ // opens opportunities for globalopt (and inlining) by substituting function -+ // pointers passed as arguments to direct uses of functions. -+ addPass(Passes, createIPSCCPPass()); -+ -+ // Now that we internalized some globals, see if we can hack on them! -+ addPass(Passes, createGlobalOptimizerPass()); -+ -+ // Linking modules together can lead to duplicated global constants, only -+ // keep one copy of each constant... -+ addPass(Passes, createConstantMergePass()); -+ -+ // Remove unused arguments from functions... -+ addPass(Passes, createDeadArgEliminationPass()); -+ -+ // Reduce the code after globalopt and ipsccp. Both can open up significant -+ // simplification opportunities, and both can propagate functions through -+ // function pointers. When this happens, we often have to resolve varargs -+ // calls, etc, so let instcombine do this. -+ addPass(Passes, createInstructionCombiningPass()); -+ -+ if (!DisableInline) -+ addPass(Passes, createFunctionInliningPass()); // Inline small functions -+ -+ addPass(Passes, createPruneEHPass()); // Remove dead EH info -+ addPass(Passes, createGlobalOptimizerPass()); // Optimize globals again. -+ addPass(Passes, createGlobalDCEPass()); // Remove dead functions -+ -+ // If we didn't decide to inline a function, check to see if we can -+ // transform it to pass arguments by value instead of by reference. -+ addPass(Passes, createArgumentPromotionPass()); -+ -+ // The IPO passes may leave cruft around. Clean up after them. -+ addPass(Passes, createInstructionCombiningPass()); -+ addPass(Passes, createJumpThreadingPass()); // Thread jumps. -+ addPass(Passes, createSROAPass()); // Break up allocas -+ -+ // Run a few AA driven optimizations here and now, to cleanup the code. -+ addPass(Passes, createPostOrderFunctionAttrsLegacyPass()); -+ addPass(Passes, createReversePostOrderFunctionAttrsPass()); // Add nocapture -+ addPass(Passes, createGlobalsAAWrapperPass()); // IP alias analysis -+ -+ addPass(Passes, createLICMPass()); // Hoist loop invariants -+ addPass(Passes, createGVNPass()); // Remove redundancies -+ addPass(Passes, createMemCpyOptPass()); // Remove dead memcpy's -+ addPass(Passes, createDeadStoreEliminationPass()); // Nuke dead stores -+ -+ // Cleanup and simplify the code after the scalar optimizations. -+ addPass(Passes, createInstructionCombiningPass()); -+ -+ addPass(Passes, createJumpThreadingPass()); // Thread jumps. -+ addPass(Passes, createPromoteMemoryToRegisterPass()); // Cleanup jumpthread. -+ -+ // Delete basic blocks, which optimization passes may have killed... -+ addPass(Passes, createCFGSimplificationPass()); -+ -+ // Now that we have optimized the program, discard unreachable functions... -+ addPass(Passes, createGlobalDCEPass()); -+ -+ // If the -s or -S command line options were specified, strip the symbols out -+ // of the resulting program to make it smaller. -s and -S are GNU ld options -+ // that we are supporting; they alias -strip-all and -strip-debug. -+ if (Strip || StripDebug) -+ addPass(Passes, createStripSymbolsPass(StripDebug && !Strip)); -+ -+ // The user's passes may leave cruft around; clean up after them. -+ addPass(Passes, createInstructionCombiningPass()); -+ addPass(Passes, createCFGSimplificationPass()); -+ addPass(Passes, createAggressiveDCEPass()); -+ addPass(Passes, createGlobalDCEPass()); -+ -+ // Run our queue of passes all at once now, efficiently. -+ Passes.run(*M); -+} --- -2.43.0 - diff --git a/0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch b/0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch deleted file mode 100644 index 02e2b8c..0000000 --- a/0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch +++ /dev/null @@ -1,28 +0,0 @@ -From: Martin Nowack -Date: Sun, 29 Oct 2023 20:38:55 +0000 -Subject: Use KLEE's uClibc v1.4 as default to support the compilation with - newer compilers -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - .github/workflows/build.yaml | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml -index 96122bcb..fa924a37 100644 ---- a/.github/workflows/build.yaml -+++ b/.github/workflows/build.yaml -@@ -24,7 +24,7 @@ env: - SOLVERS: STP:Z3 - STP_VERSION: 2.3.3 - TCMALLOC_VERSION: 2.9.1 -- UCLIBC_VERSION: klee_uclibc_v1.3 -+ UCLIBC_VERSION: klee_uclibc_v1.4 - USE_TCMALLOC: 1 - USE_LIBCXX: 1 - Z3_VERSION: 4.8.15 --- -2.43.0 - diff --git a/0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch b/0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch deleted file mode 100644 index f19486b..0000000 --- a/0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch +++ /dev/null @@ -1,1158 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 11:59:29 +0000 -Subject: Assume C compiler's default standard is `-std=gnu17` -Patch-mainline: no -References: llvm16 - -Newer compilers use `-std=gnu17` as the default when compiling C code. -Fix all the test cases that violate this behaviour or explicitly request -older standards `-std=c89` where necessary. - -Signed-off-by: Jiri Slaby ---- - test/ArrayOpt/test_feasible.c | 3 ++- - test/DeterministicAllocation/OneOutOfBounds.c | 2 +- - test/Expr/ReadExprConsistency.c | 10 +++++----- - test/Feature/BFSSearcherAndDFSSearcherInterleaved.c | 2 +- - test/Feature/ByteSwap.c | 2 +- - test/Feature/CheckMemoryAccess.c | 4 ++-- - test/Feature/CompressedExprLogging.c | 2 +- - test/Feature/CopyOnWrite.c | 2 +- - test/Feature/DanglingConcreteReadExpr.c | 2 +- - test/Feature/DefineFixedObject.c | 2 +- - test/Feature/Envp.c | 3 ++- - test/Feature/GetValue.c | 4 ++-- - test/Feature/InAndOutOfBounds.c | 2 ++ - test/Feature/IndirectCallToExternal.c | 2 +- - test/Feature/InlineAsm.c | 2 +- - test/Feature/IsSymbolic.c | 2 +- - test/Feature/KleeReportError.c | 1 + - test/Feature/LowerSwitch.c | 2 +- - test/Feature/MakeSymbolicAPI.c | 3 +-- - test/Feature/MakeSymbolicName.c | 2 +- - test/Feature/Memalign.c | 4 ++-- - test/Feature/MultiMkSym.c | 2 +- - test/Feature/MultipleReadResolution.c | 3 ++- - test/Feature/MultipleReallocResolution.c | 4 ++-- - test/Feature/MultipleWriteResolution.c | 4 ++-- - test/Feature/NamedSeedMatching.c | 4 ++-- - test/Feature/NoExternalCallsAllowed.c | 2 +- - test/Feature/OneOutOfBounds.c | 1 + - test/Feature/Optimize.c | 1 + - test/Feature/OverlappedError.c | 2 +- - test/Feature/PreferCex.c | 5 +---- - test/Feature/RaiseAsm.c | 2 +- - test/Feature/ReplayPath.c | 4 ++-- - test/Feature/Searchers.c | 2 +- - test/Feature/SetForking.c | 2 +- - test/Feature/SilentKleeAssume.c | 4 ++-- - test/Feature/SolverTimeout.c | 2 +- - test/Feature/WriteCov.c | 2 +- - test/Feature/consecutive_divide_by_zero.c | 2 ++ - test/Feature/const_array_opt1.c | 1 + - test/Feature/left-overshift-sym-conc.c | 3 ++- - test/Feature/logical-right-overshift-sym-conc.c | 3 ++- - test/Feature/srem.c | 3 +-- - test/Merging/merge_fail.c | 1 + - .../libkleeruntest/replay_cex_after_assumed_malloc.c | 1 + - test/Runtime/POSIX/FDNumbers.c | 4 ++-- - test/Runtime/POSIX/Fcntl.c | 2 +- - test/Runtime/POSIX/FreeArgv.c | 3 ++- - test/Runtime/POSIX/Getenv.c | 5 +++-- - test/Runtime/POSIX/Openat.c | 3 ++- - test/Runtime/POSIX/Replay.c | 1 + - test/Runtime/POSIX/Stdin.c | 7 ++++--- - test/Runtime/POSIX/Write1.c | 4 +++- - test/Runtime/POSIX/Write2.c | 4 ++-- - .../Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c | 1 + - test/VectorInstructions/insert_element.c | 3 ++- - ...07-07-25-invalid-stp-array-binding-to-objectstate.c | 1 + - test/regression/2007-07-30-unflushed-byte.c | 2 +- - .../2007-08-01-cache-unclear-on-overwrite-flushed.c | 1 + - test/regression/2007-08-06-64bit-shift.c | 1 + - test/regression/2007-08-06-access-after-free.c | 2 ++ - test/regression/2007-08-16-invalid-constant-value.c | 4 +--- - .../2007-08-16-valid-write-to-freed-object.c | 2 ++ - test/regression/2007-10-11-free-of-alloca.c | 2 +- - .../2007-10-12-failed-make-symbolic-after-copy.c | 2 +- - test/regression/2008-03-04-free-of-global.c | 3 ++- - test/regression/2008-03-11-free-of-malloc-zero.c | 2 +- - test/regression/2008-04-10-bad-alloca-free.c | 1 + - test/regression/2014-07-04-unflushed-error-report.c | 1 + - test/regression/2015-08-05-invalid-fork.c | 1 + - test/regression/2015-08-30-empty-constraints.c | 1 + - test/regression/2015-08-30-sdiv-1.c | 1 + - test/regression/2017-02-21-pathOS-id.c | 3 +++ - test/regression/2017-11-01-test-with-empty-varname.c | 2 +- - test/regression/2020-04-27-stp-array-names.c | 2 +- - 75 files changed, 111 insertions(+), 78 deletions(-) - -diff --git a/test/ArrayOpt/test_feasible.c b/test/ArrayOpt/test_feasible.c -index 8e7009b4..8dc3c4e3 100644 ---- a/test/ArrayOpt/test_feasible.c -+++ b/test/ArrayOpt/test_feasible.c -@@ -22,8 +22,9 @@ - // CHECK-OPT_V: KLEE: WARNING: OPT_V: successful - // CHECK-CONST_ARR: const_arr - --#include - #include "klee/klee.h" -+#include -+#include - - char array[5] = {0,1,0,1,0}; - -diff --git a/test/DeterministicAllocation/OneOutOfBounds.c b/test/DeterministicAllocation/OneOutOfBounds.c -index 499ff06b..c3dbc597 100644 ---- a/test/DeterministicAllocation/OneOutOfBounds.c -+++ b/test/DeterministicAllocation/OneOutOfBounds.c -@@ -2,7 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --kdalloc %t.bc 2>&1 | FileCheck %s - // RUN: test -f %t.klee-out/test000001.ptr.err -- -+#include - int main() { - int *x = malloc(sizeof(int)); - // CHECK: OneOutOfBounds.c:[[@LINE+1]]: memory error: out of bound pointer -diff --git a/test/Expr/ReadExprConsistency.c b/test/Expr/ReadExprConsistency.c -index 9b794ee5..6429dc99 100644 ---- a/test/Expr/ReadExprConsistency.c -+++ b/test/Expr/ReadExprConsistency.c -@@ -2,8 +2,9 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc 2>%t.log - // RUN: cat %t.log | FileCheck %s -- -+#include "klee/klee.h" - #include -+#include - - /* - This tests checks ensures that only relevant updates are present when doing -@@ -15,7 +16,6 @@ https://github.com/klee/klee/issues/921 - https://github.com/klee/klee/pull/1061 - */ - --void klee_print_expr(const char*, char); - int main() { - char arr[3]; - char symbolic; -@@ -25,12 +25,12 @@ int main() { - - - char a = arr[2]; // (ReadExpr 2 arr) -- //CHECK: arr[2]:(Read w8 2 arr) -+ // CHECK: arr[2]:(SExt w32 (Read w8 2 arr)) - klee_print_expr("arr[2]", arr[2]); - arr[1] = 0; - char b = arr[symbolic]; // (ReadExpr symbolic [1=0]@arr) -- //CHECK: arr[2]:(Read w8 2 arr) -- //CHECK-NOT: arr[2]:(Read w8 2 [1=0]@arr) -+ // CHECK: arr[2]:(SExt w32 (Read w8 2 arr)) -+ // CHECK-NOT: arr[2]:(SExt w32 (Read w8 2 [1=0]@arr)) - klee_print_expr("arr[2]", arr[2]); - - if(a == b) printf("Equal!\n"); -diff --git a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c -index 88d49548..8e4859a3 100644 ---- a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c -+++ b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c -@@ -13,7 +13,7 @@ - // RUN: FileCheck -input-file=%t-dfs-bfs.out %s - - #include "klee/klee.h" -- -+#include - int main() { - int x, y, z; - klee_make_symbolic(&x, sizeof(x), "x"); -diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c -index 1e4ec190..d862b53d 100644 ---- a/test/Feature/ByteSwap.c -+++ b/test/Feature/ByteSwap.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=klee --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - #include - -diff --git a/test/Feature/CheckMemoryAccess.c b/test/Feature/CheckMemoryAccess.c -index a9e0e6b5..9854f983 100644 ---- a/test/Feature/CheckMemoryAccess.c -+++ b/test/Feature/CheckMemoryAccess.c -@@ -3,10 +3,10 @@ - // RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log - // RUN: grep -q "good" %t.log - // RUN: not grep -q "bad" %t.log -- -+#include "klee/klee.h" - #include --#include - #include -+#include - - int main() { - char buf[4]; -diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c -index 42c42402..1344988b 100644 ---- a/test/Feature/CompressedExprLogging.c -+++ b/test/Feature/CompressedExprLogging.c -@@ -10,7 +10,7 @@ - // RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:kquery %t1.bc - // RUN: gunzip -d %t.klee-out2/all-queries.kquery.gz - // RUN: diff %t.klee-out/all-queries.kquery %t.klee-out/all-queries.kquery -- -+#include "klee/klee.h" - #include - - int constantArr[16] = {1 << 0, 1 << 1, 1 << 2, 1 << 3, 1 << 4, 1 << 5, -diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c -index 9d443bf6..73342642 100644 ---- a/test/Feature/CopyOnWrite.c -+++ b/test/Feature/CopyOnWrite.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm -g -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - - #define N 5 -diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c -index ba7c7bc5..7b0c981d 100644 ---- a/test/Feature/DanglingConcreteReadExpr.c -+++ b/test/Feature/DanglingConcreteReadExpr.c -@@ -2,7 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --optimize=false --output-dir=%t.klee-out %t1.bc - // RUN: grep "total queries = 2" %t.klee-out/info -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/DefineFixedObject.c b/test/Feature/DefineFixedObject.c -index 6e7efb14..102034d0 100644 ---- a/test/Feature/DefineFixedObject.c -+++ b/test/Feature/DefineFixedObject.c -@@ -1,7 +1,7 @@ - // RUN: %clang -emit-llvm -c -o %t1.bc %s - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - - #define ADDRESS ((int*) 0x0080) -diff --git a/test/Feature/Envp.c b/test/Feature/Envp.c -index 62c91325..2b1b6bdc 100644 ---- a/test/Feature/Envp.c -+++ b/test/Feature/Envp.c -@@ -1,8 +1,9 @@ - // RUN: %clang %s -emit-llvm -g -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -- - #include -+#include -+#include - - int main(int argc, char **argv, char **envp) { - unsigned i; -diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c -index d2b046f4..c652658f 100644 ---- a/test/Feature/GetValue.c -+++ b/test/Feature/GetValue.c -@@ -1,9 +1,9 @@ - // RUN: %clang -emit-llvm -c -o %t1.bc %s - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -- --#include -+#include "klee/klee.h" - #include -+#include - - int main() { - int x = klee_int("x"); -diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c -index 39ed8322..37c30e8f 100644 ---- a/test/Feature/InAndOutOfBounds.c -+++ b/test/Feature/InAndOutOfBounds.c -@@ -4,6 +4,8 @@ - // RUN: test -f %t.klee-out/test000001.ptr.err -o -f %t.klee-out/test000002.ptr.err - // RUN: not test -f %t.klee-out/test000001.ptr.err -a -f %t.klee-out/test000002.ptr.err - // RUN: not test -f %t.klee-out/test000003.ktest -+#include "klee/klee.h" -+#include - - unsigned klee_urange(unsigned start, unsigned end) { - unsigned x; -diff --git a/test/Feature/IndirectCallToExternal.c b/test/Feature/IndirectCallToExternal.c -index 03447c7d..2d4943dc 100644 ---- a/test/Feature/IndirectCallToExternal.c -+++ b/test/Feature/IndirectCallToExternal.c -@@ -8,7 +8,7 @@ - #include - - int main() { -- int (*scmp)(char*,char*) = strcmp; -+ int (*scmp)(const char *, const char *) = strcmp; - - assert(scmp("hello","hi") < 0); - -diff --git a/test/Feature/InlineAsm.c b/test/Feature/InlineAsm.c -index 25e0e72e..e6da7bb9 100644 ---- a/test/Feature/InlineAsm.c -+++ b/test/Feature/InlineAsm.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out %t.bc > %t.output.log 2>&1 -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c -index 033d9d6a..266dd23f 100644 ---- a/test/Feature/IsSymbolic.c -+++ b/test/Feature/IsSymbolic.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c -index f406696f..afd447f5 100644 ---- a/test/Feature/KleeReportError.c -+++ b/test/Feature/KleeReportError.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s - // RUN: ls %t.klee-out/ | grep .my.err | wc -l | grep 2 -+#include "klee/klee.h" - #include - #include - -diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c -index a1bd3f38..76b9e63b 100644 ---- a/test/Feature/LowerSwitch.c -+++ b/test/Feature/LowerSwitch.c -@@ -6,7 +6,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --switch-type=simple %t.bc - // RUN: test -f %t.klee-out/test000010.ktest -- -+#include "klee/klee.h" - #include - - int main(int argc, char **argv) { -diff --git a/test/Feature/MakeSymbolicAPI.c b/test/Feature/MakeSymbolicAPI.c -index d5305422..ea115936 100644 ---- a/test/Feature/MakeSymbolicAPI.c -+++ b/test/Feature/MakeSymbolicAPI.c -@@ -1,9 +1,8 @@ --// RUN: %clang %s -emit-llvm -g -c -o %t1.bc -+// RUN: %clang %s -std=c89 -emit-llvm -g -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc 2> %t.stderr.log - // RUN: FileCheck %s -check-prefix=CHECK-WRN --input-file=%t.klee-out/warnings.txt - // RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log -- - int main() { - unsigned a, b, c; - char *p; -diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c -index a57d9a84..332565d7 100644 ---- a/test/Feature/MakeSymbolicName.c -+++ b/test/Feature/MakeSymbolicName.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm -g -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/Memalign.c b/test/Feature/Memalign.c -index e5d09f6c..524e257d 100644 ---- a/test/Feature/Memalign.c -+++ b/test/Feature/Memalign.c -@@ -1,9 +1,9 @@ -+// REQUIRES: not-darwin - // RUN: %clang -emit-llvm -g -c %s -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.log -- -+#include - #include -- - int main(int argc, char *argv[]) { - int *a = (int *)memalign(8, sizeof(int) * 5); - for (int i = 0; i < 5; ++i) { -diff --git a/test/Feature/MultiMkSym.c b/test/Feature/MultiMkSym.c -index 16ac7d1b..e5222a94 100644 ---- a/test/Feature/MultiMkSym.c -+++ b/test/Feature/MultiMkSym.c -@@ -6,7 +6,7 @@ - // RUN: grep "a\[100\]" %t1 | wc -l | grep 2 - - /* Tests that the Array factory correctly distinguishes between arrays created at the same location but with different sizes */ -- -+#include "klee/klee.h" - #include - #include - -diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c -index 8701d068..92f3f92b 100644 ---- a/test/Feature/MultipleReadResolution.c -+++ b/test/Feature/MultipleReadResolution.c -@@ -7,8 +7,9 @@ - // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log - // RUN: diff %t1.res %t1.log - -+#include "klee/klee.h" - #include -- -+#include - unsigned klee_urange(unsigned start, unsigned end) { - unsigned x; - klee_make_symbolic(&x, sizeof x, "x"); -diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c -index 84dd15e2..90570537 100644 ---- a/test/Feature/MultipleReallocResolution.c -+++ b/test/Feature/MultipleReallocResolution.c -@@ -3,10 +3,10 @@ - // RUN: %klee --output-dir=%t.klee-out %t1.bc - // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2 - // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 -- -+#include "klee/klee.h" - #include --#include - #include -+#include - - unsigned klee_urange(unsigned start, unsigned end) { - unsigned x; -diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c -index 89296c11..326767f2 100644 ---- a/test/Feature/MultipleWriteResolution.c -+++ b/test/Feature/MultipleWriteResolution.c -@@ -6,9 +6,9 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log - // RUN: diff %t1.res %t1.log -- -+#include "klee/klee.h" - #include -- -+#include - unsigned klee_urange(unsigned start, unsigned end) { - unsigned x; - klee_make_symbolic(&x, sizeof x, "x"); -diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c -index 6f97e4e7..2cc47340 100644 ---- a/test/Feature/NamedSeedMatching.c -+++ b/test/Feature/NamedSeedMatching.c -@@ -10,9 +10,9 @@ - // RUN: grep -q "b==4" %t.log - // RUN: grep -q "c==5" %t.log - // RUN: grep -q "x==6" %t.log -- --#include -+#include "klee/klee.h" - #include -+#include - - int main(int argc, char **argv) { - int a, b, c, x; -diff --git a/test/Feature/NoExternalCallsAllowed.c b/test/Feature/NoExternalCallsAllowed.c -index 8a8dc54b..62570434 100644 ---- a/test/Feature/NoExternalCallsAllowed.c -+++ b/test/Feature/NoExternalCallsAllowed.c -@@ -2,8 +2,8 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --external-calls=none %t1.bc 2>&1 | FileCheck %s - // RUN: test %t.klee-out/test000001.user.err -- - #include -+#include - - int main(int argc, char** argv) { - // CHECK: Disallowed call to external function: abs -diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c -index a3e6db1f..0dfee6d6 100644 ---- a/test/Feature/OneOutOfBounds.c -+++ b/test/Feature/OneOutOfBounds.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s - // RUN: test -f %t.klee-out/test000001.ptr.err -+#include - - int main() { - int *x = malloc(sizeof(int)); -diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c -index e14be96d..e125eff4 100644 ---- a/test/Feature/Optimize.c -+++ b/test/Feature/Optimize.c -@@ -6,6 +6,7 @@ - // RUN: diff %t3.log %t3.good - - // should complete by 100 instructions if opt is on -+#include - - int main() { - int i, res = 0; -diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c -index e6d36b75..e6595cd1 100644 ---- a/test/Feature/OverlappedError.c -+++ b/test/Feature/OverlappedError.c -@@ -3,7 +3,7 @@ - // RUN: %klee --output-dir=%t.klee-out %t1.bc - // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4 - // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c -index 39337cf5..28a0eb20 100644 ---- a/test/Feature/PreferCex.c -+++ b/test/Feature/PreferCex.c -@@ -2,10 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc - // RUN: %ktest-tool %t.klee-out/test000001.ktest | FileCheck %s -- --#include --#include --#include -+#include "klee/klee.h" - - int main() { - char buf[4]; -diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c -index 842d9f3d..865929ae 100644 ---- a/test/Feature/RaiseAsm.c -+++ b/test/Feature/RaiseAsm.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - - typedef unsigned short uint16; -diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c -index f77656f8..e2eb95af 100644 ---- a/test/Feature/ReplayPath.c -+++ b/test/Feature/ReplayPath.c -@@ -6,9 +6,9 @@ - // RUN: rm -rf %t.klee-out-2 - // RUN: %klee --output-dir=%t.klee-out-2 --replay-path %t.klee-out/test000001.path %t2.bc > %t3.log - // RUN: diff %t3.log %t3.good -- --#include -+#include "klee/klee.h" - #include -+#include - - void cond_exit() { - #ifdef COND_EXIT -diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c -index cd806950..c5260f3d 100644 ---- a/test/Feature/Searchers.c -+++ b/test/Feature/Searchers.c -@@ -30,7 +30,7 @@ - /* this test is basically just for coverage and doesn't really do any - correctness check (aside from testing that the various combinations - don't crash) */ -- -+#include "klee/klee.h" - #include - - int validate(char *buf, int N) { -diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c -index b739910d..a2911743 100644 ---- a/test/Feature/SetForking.c -+++ b/test/Feature/SetForking.c -@@ -5,7 +5,7 @@ - // RUN: grep "1 A" %t.uniq.log - // RUN: grep "1 B" %t.uniq.log - // RUN: grep "1 C" %t.uniq.log -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/SilentKleeAssume.c b/test/Feature/SilentKleeAssume.c -index 06872e9b..24138029 100644 ---- a/test/Feature/SilentKleeAssume.c -+++ b/test/Feature/SilentKleeAssume.c -@@ -5,9 +5,9 @@ - // RUN: rm -rf %t.klee-out - // RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.default-klee-assume.log 2>&1 - // RUN: FileCheck -input-file=%t.default-klee-assume.log -check-prefix=CHECK-DEFAULT-KLEE-ASSUME %s -- --#include -+#include "klee/klee.h" - #include -+#include - - int main() { - int x = klee_int("x"); -diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c -index 98c9ecde..aee7f4da 100644 ---- a/test/Feature/SolverTimeout.c -+++ b/test/Feature/SolverTimeout.c -@@ -3,7 +3,7 @@ - // RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc - // - // Note: This test occasionally fails when using Z3 4.4.1 -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c -index 304198c5..3fd0074c 100644 ---- a/test/Feature/WriteCov.c -+++ b/test/Feature/WriteCov.c -@@ -7,7 +7,7 @@ - // RUN: grep %t.klee-out/test000001.cov:1 %t3.txt - // RUN: grep %t.klee-out/test000002.cov:0 %t3.txt - // RUN: grep %t.klee-out/test000002.cov:1 %t3.txt -- -+#include "klee/klee.h" - #include - #include - -diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c -index 0915bbaa..7a0dc1d9 100644 ---- a/test/Feature/consecutive_divide_by_zero.c -+++ b/test/Feature/consecutive_divide_by_zero.c -@@ -8,6 +8,8 @@ - * only one test case is generated EVEN IF THERE ARE MULTIPLE - * DISTINCT ERRORS! - */ -+ -+#include "klee/klee.h" - int main() { - unsigned int a = 15; - unsigned int b = 15; -diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c -index 1ed3c3ee..f41bdf47 100644 ---- a/test/Feature/const_array_opt1.c -+++ b/test/Feature/const_array_opt1.c -@@ -9,6 +9,7 @@ - this takes under 2 seconds w/ the optimization and almost 6 minutes - w/o. So we kill it in 10 sec and check if it has finished - successfully. */ -+#include "klee/klee.h" - - #include - #include -diff --git a/test/Feature/left-overshift-sym-conc.c b/test/Feature/left-overshift-sym-conc.c -index 0320334f..2aaaf6f1 100644 ---- a/test/Feature/left-overshift-sym-conc.c -+++ b/test/Feature/left-overshift-sym-conc.c -@@ -3,8 +3,9 @@ - // RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc - // RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt - // RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info --#include -+#include "klee/klee.h" - #include -+#include - - typedef enum - { -diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c -index 06bae156..4c4b6f98 100644 ---- a/test/Feature/logical-right-overshift-sym-conc.c -+++ b/test/Feature/logical-right-overshift-sym-conc.c -@@ -3,8 +3,9 @@ - // RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc - // RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt - // RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info --#include -+#include "klee/klee.h" - #include -+#include - - typedef enum - { -diff --git a/test/Feature/srem.c b/test/Feature/srem.c -index 65b324d3..0b542b17 100644 ---- a/test/Feature/srem.c -+++ b/test/Feature/srem.c -@@ -3,8 +3,7 @@ - // RUN: %klee --output-dir=%t.klee-out --klee-call-optimisation=false %t.bc 2>&1 | FileCheck %s - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --klee-call-optimisation=false --optimize %t.bc 2>&1 | FileCheck %s -- --#include -+#include "klee/klee.h" - #include - - int main(int argc, char** argv) -diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c -index 00ea21ef..41ced1aa 100644 ---- a/test/Merging/merge_fail.c -+++ b/test/Merging/merge_fail.c -@@ -14,6 +14,7 @@ - // This test will not merge because we cannot merge states when they allocated memory. - - #include "klee/klee.h" -+#include - - int main(int argc, char **args) { - -diff --git a/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c -index 09d60e79..1ccff177 100644 ---- a/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c -+++ b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c -@@ -3,6 +3,7 @@ - // RUN: %klee --output-dir=%t.klee-out %t.ll - // KLEE just must not fail - #include "klee/klee.h" -+#include - - int main() { - char i; -diff --git a/test/Runtime/POSIX/FDNumbers.c b/test/Runtime/POSIX/FDNumbers.c -index 42f0f5ae..4e0fa79a 100644 ---- a/test/Runtime/POSIX/FDNumbers.c -+++ b/test/Runtime/POSIX/FDNumbers.c -@@ -1,10 +1,10 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 -- - #include --#include - #include -+#include -+#include - - int main(int argc, char **argv) { - int fd = open("A", O_TRUNC); -diff --git a/test/Runtime/POSIX/Fcntl.c b/test/Runtime/POSIX/Fcntl.c -index 53246a15..737d5da5 100644 ---- a/test/Runtime/POSIX/Fcntl.c -+++ b/test/Runtime/POSIX/Fcntl.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 -- -+#include "klee/klee.h" - #include - #include - -diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c -index 93ed697e..cdc5487f 100644 ---- a/test/Runtime/POSIX/FreeArgv.c -+++ b/test/Runtime/POSIX/FreeArgv.c -@@ -4,7 +4,8 @@ - // RUN: test -f %t.klee-out/test000001.free.err - // RUN: test -f %t.klee-out/test000002.free.err - // RUN: test -f %t.klee-out/test000003.free.err -- -+#include "klee/klee.h" -+#include - int main(int argc, char **argv) { - switch (klee_range(0, 3, "range")) { - case 0: -diff --git a/test/Runtime/POSIX/Getenv.c b/test/Runtime/POSIX/Getenv.c -index 6dff3c24..d5db7c39 100644 ---- a/test/Runtime/POSIX/Getenv.c -+++ b/test/Runtime/POSIX/Getenv.c -@@ -1,9 +1,10 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 -- - #include -- -+#include -+#include -+#include - int main(int argc, char **argv) { - char *g = getenv("PWD"); - if (g) { -diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c -index 2341527e..67ff78bd 100644 ---- a/test/Runtime/POSIX/Openat.c -+++ b/test/Runtime/POSIX/Openat.c -@@ -2,9 +2,10 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 - // RUN: test -f %t.klee-out/test000001.ktest -- -+#include "klee/klee.h" - #include - #include -+#include - - int main(int argc, char **argv) { - int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC); -diff --git a/test/Runtime/POSIX/Replay.c b/test/Runtime/POSIX/Replay.c -index 61862c5f..fb1b400c 100644 ---- a/test/Runtime/POSIX/Replay.c -+++ b/test/Runtime/POSIX/Replay.c -@@ -8,6 +8,7 @@ - // REPLAY: Yes - - #ifdef KLEE_EXECUTION -+#include "klee/klee.h" - #define EXIT klee_silent_exit - #else - #include -diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c -index 6d84baff..84caab3a 100644 ---- a/test/Runtime/POSIX/Stdin.c -+++ b/test/Runtime/POSIX/Stdin.c -@@ -9,11 +9,12 @@ - // RUN: grep "mode:lnk" %t.log - // RUN: grep "read:sym:yes" %t.log - // RUN: grep "read:sym:no" %t.log -- --#include -+#include - #include -+#include -+#include - #include --#include -+#include - - int main(int argc, char **argv) { - struct stat stats; -diff --git a/test/Runtime/POSIX/Write1.c b/test/Runtime/POSIX/Write1.c -index 5fc4ff8f..7f1e6f20 100644 ---- a/test/Runtime/POSIX/Write1.c -+++ b/test/Runtime/POSIX/Write1.c -@@ -2,8 +2,10 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log - --#include -+#include "klee/klee.h" - #include -+#include -+#include - - int main(int argc, char** argv) { - char buf[32]; -diff --git a/test/Runtime/POSIX/Write2.c b/test/Runtime/POSIX/Write2.c -index 04698f21..e9eb6f6b 100644 ---- a/test/Runtime/POSIX/Write2.c -+++ b/test/Runtime/POSIX/Write2.c -@@ -1,9 +1,9 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log -- --#include -+#include "klee/klee.h" - #include -+#include - - int main(int argc, char** argv) { - const char* msg = "This will eventually overflow stdout. "; -diff --git a/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c b/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c -index 3b66dd21..26bb1dce 100644 ---- a/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c -+++ b/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c -@@ -3,6 +3,7 @@ - // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc %t1.bc - - // just make sure atexit works ok -+#include - - void boo() { - } -diff --git a/test/VectorInstructions/insert_element.c b/test/VectorInstructions/insert_element.c -index df09819d..35054fd9 100644 ---- a/test/VectorInstructions/insert_element.c -+++ b/test/VectorInstructions/insert_element.c -@@ -5,9 +5,10 @@ - // RUN: %klee --output-dir=%t.klee-out --optimize=false %t1.bc > %t.stdout.log 2> %t.stderr.log - // RUN: FileCheck -check-prefix=CHECK-STDOUT -input-file=%t.stdout.log %s - // RUN: FileCheck -check-prefix=CHECK-STDERR -input-file=%t.stderr.log %s -+#include "klee/klee.h" - #include --#include - #include -+#include - - typedef uint32_t v4ui __attribute__ ((vector_size (16))); - int main() { -diff --git a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c -index 1897266a..ac32063c 100644 ---- a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c -+++ b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - -+#include "klee/klee.h" - #include - - int main(void) { -diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c -index bb480b9a..2d2f1e8c 100644 ---- a/test/regression/2007-07-30-unflushed-byte.c -+++ b/test/regression/2007-07-30-unflushed-byte.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c -index 96115557..73ceec91 100644 ---- a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c -+++ b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - -+#include "klee/klee.h" - #include - #include - -diff --git a/test/regression/2007-08-06-64bit-shift.c b/test/regression/2007-08-06-64bit-shift.c -index f072e453..675211fd 100644 ---- a/test/regression/2007-08-06-64bit-shift.c -+++ b/test/regression/2007-08-06-64bit-shift.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/regression/2007-08-06-access-after-free.c b/test/regression/2007-08-06-access-after-free.c -index 7d1f81db..ef47c868 100644 ---- a/test/regression/2007-08-06-access-after-free.c -+++ b/test/regression/2007-08-06-access-after-free.c -@@ -2,7 +2,9 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - -+#include "klee/klee.h" - #include -+#include - - int main() { - int a; -diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c -index c49357f8..f5474f7a 100644 ---- a/test/regression/2007-08-16-invalid-constant-value.c -+++ b/test/regression/2007-08-16-invalid-constant-value.c -@@ -1,5 +1,5 @@ - // RUN: rm -f %t4.out %t4.err %t4.log --// RUN: %clang %s -emit-llvm -O2 -c -o %t1.bc -+// RUN: %clang %s -std=c89 -emit-llvm -O2 -c -o %t1.bc - // RUN: %llvmas -f %p/../Feature/_utils._ll -o %t2.bc - // RUN: %llvmlink %t1.bc %t2.bc -o %t3.bc - // RUN: rm -rf %t.klee-out -@@ -7,8 +7,6 @@ - - #include - --#include "../Feature/utils.h" -- - int main() { - unsigned char a; - -diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c -index 6b6efecb..2a43a240 100644 ---- a/test/regression/2007-08-16-valid-write-to-freed-object.c -+++ b/test/regression/2007-08-16-valid-write-to-freed-object.c -@@ -2,6 +2,8 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - -+#include "klee/klee.h" -+#include - unsigned sym() { - unsigned x; - klee_make_symbolic(&x, sizeof x, "x"); -diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c -index 6aa6cdb3..cecdeef2 100644 ---- a/test/regression/2007-10-11-free-of-alloca.c -+++ b/test/regression/2007-10-11-free-of-alloca.c -@@ -2,7 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s - // RUN: test -f %t.klee-out/test000001.free.err -- -+#include - int main() { - int buf[4]; - // CHECK: 2007-10-11-free-of-alloca.c:9: free of alloca -diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c -index 64cae9f4..77f9b9f6 100644 ---- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c -+++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c -@@ -2,7 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - // RUN: test -f %t.klee-out/test000001.ktest -- -+#include "klee/klee.h" - int main() { - unsigned x, y[4]; - -diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c -index 995e7173..fb4a2df8 100644 ---- a/test/regression/2008-03-04-free-of-global.c -+++ b/test/regression/2008-03-04-free-of-global.c -@@ -3,10 +3,11 @@ - // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s - // RUN: test -f %t.klee-out/test000001.free.err - -+#include - int buf[4]; - - int main() { -- // CHECK: 2008-03-04-free-of-global.c:10: free of global -+ // CHECK: 2008-03-04-free-of-global.c:[[@LINE+1]]: free of global - free(buf); // this should give runtime error, not crash - return 0; - } -diff --git a/test/regression/2008-03-11-free-of-malloc-zero.c b/test/regression/2008-03-11-free-of-malloc-zero.c -index e90baa2c..cdd2ef35 100644 ---- a/test/regression/2008-03-11-free-of-malloc-zero.c -+++ b/test/regression/2008-03-11-free-of-malloc-zero.c -@@ -1,7 +1,7 @@ - // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -- -+#include "klee/klee.h" - #include - - int main() { -diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c -index 5049f47c..d20d07d2 100644 ---- a/test/regression/2008-04-10-bad-alloca-free.c -+++ b/test/regression/2008-04-10-bad-alloca-free.c -@@ -2,6 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc - -+#include "klee/klee.h" - void f(int *addr) { - klee_make_symbolic(addr, sizeof *addr, "moo"); - } -diff --git a/test/regression/2014-07-04-unflushed-error-report.c b/test/regression/2014-07-04-unflushed-error-report.c -index c929328d..058aef7e 100644 ---- a/test/regression/2014-07-04-unflushed-error-report.c -+++ b/test/regression/2014-07-04-unflushed-error-report.c -@@ -6,6 +6,7 @@ - /* This test checks that the error file isn't empty and contains the - * right content. - */ -+#include "klee/klee.h" - int main() { - unsigned int x = 15; - unsigned int y; -diff --git a/test/regression/2015-08-05-invalid-fork.c b/test/regression/2015-08-05-invalid-fork.c -index a165cab2..5c09cbfc 100644 ---- a/test/regression/2015-08-05-invalid-fork.c -+++ b/test/regression/2015-08-05-invalid-fork.c -@@ -3,6 +3,7 @@ - is printed a single time. - */ - #include "klee/klee.h" -+#include - - // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc - // RUN: rm -rf %t.klee-out -diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c -index f92b6978..8598b6ae 100644 ---- a/test/regression/2015-08-30-empty-constraints.c -+++ b/test/regression/2015-08-30-empty-constraints.c -@@ -10,6 +10,7 @@ - * are generated. - * Make sure we are able to generate an input. - */ -+#include "klee/klee.h" - int main() { - int d; - -diff --git a/test/regression/2015-08-30-sdiv-1.c b/test/regression/2015-08-30-sdiv-1.c -index 7356e74c..2b819aea 100644 ---- a/test/regression/2015-08-30-sdiv-1.c -+++ b/test/regression/2015-08-30-sdiv-1.c -@@ -7,6 +7,7 @@ - /* Division by constant can be optimized.using mul/shift - * For signed division, div by 1 or -1 cannot be optimized like that. - */ -+#include "klee/klee.h" - #include - int main() { - int32_t dividend; -diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c -index b6ee269a..112875de 100644 ---- a/test/regression/2017-02-21-pathOS-id.c -+++ b/test/regression/2017-02-21-pathOS-id.c -@@ -5,6 +5,9 @@ - // RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 - // RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 - // RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 -+ -+#include "klee/klee.h" -+#include "stdlib.h" - int main(){ - int a, b; - klee_make_symbolic (&a, sizeof(int), "a"); -diff --git a/test/regression/2017-11-01-test-with-empty-varname.c b/test/regression/2017-11-01-test-with-empty-varname.c -index 89108d9d..578043ad 100644 ---- a/test/regression/2017-11-01-test-with-empty-varname.c -+++ b/test/regression/2017-11-01-test-with-empty-varname.c -@@ -2,7 +2,7 @@ - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc - // RUN: FileCheck %s --input-file=%t.klee-out/warnings.txt -- -+#include "klee/klee.h" - int main() { - unsigned a; - -diff --git a/test/regression/2020-04-27-stp-array-names.c b/test/regression/2020-04-27-stp-array-names.c -index f06e1b1a..a256441c 100644 ---- a/test/regression/2020-04-27-stp-array-names.c -+++ b/test/regression/2020-04-27-stp-array-names.c -@@ -1,4 +1,4 @@ --// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc -+// RUN: %clang -std=c89 %s -emit-llvm %O0opt -g -c -o %t.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee -output-dir=%t.klee-out --search=bfs --max-instructions=1000 %t.bc - b; --- -2.43.0 - diff --git a/0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch b/0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch deleted file mode 100644 index d76c127..0000000 --- a/0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch +++ /dev/null @@ -1,29 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 12:03:22 +0000 -Subject: Explicitly build KLEE's exception handling runtime with C++11 -Patch-mainline: no -References: llvm16 - -Currently, we assume C++11 support being used to by the tested software. -This needs to change if newer C++ standards should be supported. - -Signed-off-by: Jiri Slaby ---- - runtime/klee-eh-cxx/CMakeLists.txt | 1 + - 1 file changed, 1 insertion(+) - -diff --git a/runtime/klee-eh-cxx/CMakeLists.txt b/runtime/klee-eh-cxx/CMakeLists.txt -index 470e3f0a..b51b8544 100644 ---- a/runtime/klee-eh-cxx/CMakeLists.txt -+++ b/runtime/klee-eh-cxx/CMakeLists.txt -@@ -17,6 +17,7 @@ set(ADDITIONAL_CXX_FLAGS - -I "${KLEE_LIBCXXABI_SRC_DIR}/src" - -I "${KLEE_LIBCXXABI_SRC_DIR}/include" - -I "${KLEE_LIBCXX_INCLUDE_PATH}" -+ -std=c++11 - ) - - if (KLEE_LIBCXX_PLATFORM_INCLUDE_PATH) --- -2.43.0 - diff --git a/0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch b/0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch deleted file mode 100644 index 4bfdc01..0000000 --- a/0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch +++ /dev/null @@ -1,65 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:26:01 +0000 -Subject: Explicitly enable opaque pointer support for LLVM 15 -Patch-mainline: no -References: llvm16 - -This automatically lifts old-style pointers to opaque pointerws. -More recent versions use opaque pointers automatically and do not need -an explicit enabling. - -Signed-off-by: Jiri Slaby ---- - test/Concrete/Makefile.cmake.test.in | 6 ++++-- - tools/klee/main.cpp | 4 ++++ - 2 files changed, 8 insertions(+), 2 deletions(-) - -diff --git a/test/Concrete/Makefile.cmake.test.in b/test/Concrete/Makefile.cmake.test.in -index 2282bb08..765ea690 100644 ---- a/test/Concrete/Makefile.cmake.test.in -+++ b/test/Concrete/Makefile.cmake.test.in -@@ -14,6 +14,8 @@ LLVMCC := @LLVMCC@ - LLVMAS := @LLVM_AS@ - LLVMLINK := @LLVM_LINK@ - LLVMCC.CFlags := @OZERO_OPT@ -Wall -+LLVMAS.Flags := @LLVM_AS_FLAGS@ -+LLVMLINK.Flags := @LLVM_LINK_FLAGS@ - - # Make sure source files can match the pattern rules - VPATH := @CMAKE_CURRENT_SOURCE_DIR@ -@@ -28,7 +30,7 @@ Output/%.bc: %.c Output/.dir - $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@ - - Output/%.bc: %.ll $(LLVMAS) Output/.dir -- $(LLVMAS) -f $< -o $@ -+ $(LLVMAS) $(LLVMAS.Flags) -f $< -o $@ - - # We build a separate testingUtils bitcode for each test, to make sure parallel - # tests don't interact with one another. -@@ -36,7 +38,7 @@ Output/%_testingUtils.bc: _testingUtils.c Output/.dir - $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@ - - Output/linked_%.bc: Output/%.bc Output/%_testingUtils.bc -- $(LLVMLINK) $< Output/$*_testingUtils.bc -o $@ -+ $(LLVMLINK) $(LLVMLINK.Flags) $< Output/$*_testingUtils.bc -o $@ - - .PRECIOUS: Output/.dir - -diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp -index a3062d24..340daf0b 100644 ---- a/tools/klee/main.cpp -+++ b/tools/klee/main.cpp -@@ -1202,6 +1202,10 @@ int main(int argc, char **argv, char **envp) { - // Load the bytecode... - std::string errorMsg; - LLVMContext ctx; -+#if LLVM_VERSION_CODE == LLVM_VERSION(15, 0) -+ // We have to force the upgrade to opaque pointer explicitly for LLVM 15. -+ ctx.setOpaquePointers(true); -+#endif - std::vector> loadedModules; - if (!klee::loadFile(InputFile, ctx, loadedModules, errorMsg)) { - klee_error("error loading program '%s': %s", InputFile.c_str(), --- -2.43.0 - diff --git a/0011-Add-support-for-opaque-pointers.patch b/0011-Add-support-for-opaque-pointers.patch deleted file mode 100644 index 56b57e7..0000000 --- a/0011-Add-support-for-opaque-pointers.patch +++ /dev/null @@ -1,385 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:46:22 +0000 -Subject: Add support for opaque pointers -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - lib/Core/Executor.cpp | 119 ++++++++++++++++++++++----- - lib/Core/ExternalDispatcher.cpp | 20 ++++- - lib/Core/GetElementPtrTypeIterator.h | 8 -- - lib/Module/FunctionAlias.cpp | 8 +- - lib/Module/IntrinsicCleaner.cpp | 11 ++- - 5 files changed, 132 insertions(+), 34 deletions(-) - -diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index b4da6a08..58c15141 100644 ---- a/lib/Core/Executor.cpp -+++ b/lib/Core/Executor.cpp -@@ -14,7 +14,9 @@ - #include "CoreStats.h" - #include "ExecutionState.h" - #include "ExternalDispatcher.h" -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - #include "GetElementPtrTypeIterator.h" -+#endif - #include "ImpliedValue.h" - #include "Memory.h" - #include "MemoryManager.h" -@@ -67,6 +69,9 @@ - #include "llvm/IR/LLVMContext.h" - #include "llvm/IR/Module.h" - #include "llvm/IR/Operator.h" -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+#include "llvm/IR/GetElementPtrTypeIterator.h" -+#endif - #include "llvm/Support/CommandLine.h" - #include "llvm/Support/ErrorHandling.h" - #include "llvm/Support/FileSystem.h" -@@ -1464,24 +1469,25 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, - stateTerminated = false; - - std::vector serialized; -- - for (unsigned current_clause_id = 0; current_clause_id < lpi.getNumClauses(); - ++current_clause_id) { -- llvm::Constant *current_clause = lpi.getClause(current_clause_id); - if (lpi.isCatch(current_clause_id)) { - // catch-clause - serialized.push_back(0); - - std::uint64_t ti_addr = 0; - -- llvm::BitCastOperator *clause_bitcast = -- dyn_cast(current_clause); -- if (clause_bitcast) { -- llvm::GlobalValue *clause_type = -+ llvm::Constant *catchClause = lpi.getClause(current_clause_id); -+ llvm::Constant *typeInfo = catchClause->stripPointerCasts(); -+ if (auto *gv = dyn_cast(typeInfo)) { -+ ti_addr = globalAddresses[gv]->getZExtValue(); -+ } else if (auto *clause_bitcast = -+ dyn_cast(catchClause)) { -+ auto *clause_type = - dyn_cast(clause_bitcast->getOperand(0)); - - ti_addr = globalAddresses[clause_type]->getZExtValue(); -- } else if (current_clause->isNullValue()) { -+ } else if (catchClause->isNullValue()) { - ti_addr = 0; - } else { - terminateStateOnExecError( -@@ -1493,15 +1499,16 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, - serialized.resize(old_size + 8); - memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr)); - } else if (lpi.isFilter(current_clause_id)) { -- if (current_clause->isNullValue()) { -+ llvm::Constant *filter_clause = lpi.getClause(current_clause_id); -+ -+ if (filter_clause->isNullValue()) { - // special handling for a catch-all filter clause, i.e., "[0 x i8*]" - // for this case we serialize 1 element.. - serialized.push_back(1); - // which is a 64bit-wide 0. - serialized.resize(serialized.size() + 8, 0); - } else { -- llvm::ConstantArray const *ca = -- cast(current_clause); -+ const auto *ca = cast(filter_clause); - - // serialize `num_elements+1` as unsigned char - unsigned const num_elements = ca->getNumOperands(); -@@ -1520,18 +1527,16 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, - - // serialize the exception-types occurring in this filter-clause - for (llvm::Value const *v : ca->operands()) { -- llvm::BitCastOperator const *bitcast = -- dyn_cast(v); -- if (!bitcast) { -- terminateStateOnExecError(state, -- "Internal: expected value inside a " -- "filter-clause to be a bitcast"); -- stateTerminated = true; -- return nullptr; -+ llvm::GlobalValue const *clause_value = nullptr; -+ -+ if (auto const *bitcast = dyn_cast(v)) { -+ clause_value = dyn_cast(bitcast->getOperand(0)); -+ } -+ -+ if (auto *gv = dyn_cast(v)) { -+ clause_value = gv; - } - -- llvm::GlobalValue const *clause_value = -- dyn_cast(bitcast->getOperand(0)); - if (!clause_value) { - terminateStateOnExecError(state, - "Internal: expected value inside a " -@@ -2150,7 +2155,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { - unwindToNextLandingpad(state); - } else { - // a clause (or a catch-all clause or filter clause) matches: -- // remember the stack index and switch to cleanup phase -+ // remember the stack index and switch to clean-up phase - state.unwindingInformation = - std::make_unique( - sui->exceptionObject, cast(result), -@@ -2457,8 +2462,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { - - if (f) { - const FunctionType *fType = f->getFunctionType(); -+#if LLVM_VERSION_MAJOR >= 15 -+ const FunctionType *fpType = cb.getFunctionType(); -+#else - const FunctionType *fpType = - dyn_cast(fp->getType()->getPointerElementType()); -+#endif - - // special case the call with a bitcast case - if (fType != fpType) { -@@ -3365,10 +3374,17 @@ template - void Executor::computeOffsetsSeqTy(KGEPInstruction *kgepi, - ref &constantOffset, - uint64_t index, const TypeIt it) { -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - assert(it->getNumContainedTypes() == 1 && - "Sequential type must contain one subtype"); - uint64_t elementSize = - kmodule->targetData->getTypeStoreSize(it->getContainedType(0)); -+#else -+ assert(it.isSequential() && "Called with non-sequential type"); -+ // Get the size of a single element -+ uint64_t elementSize = -+ kmodule->targetData->getTypeStoreSize(it.getIndexedType()); -+#endif - const Value *operand = it.getOperand(); - if (const Constant *c = dyn_cast(operand)) { - ref index = -@@ -3387,13 +3403,21 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) { - ConstantExpr::alloc(0, Context::get().getPointerWidth()); - uint64_t index = 1; - for (TypeIt ii = ib; ii != ie; ++ii) { -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - if (StructType *st = dyn_cast(*ii)) { -+#else -+ if (StructType *st = ii.getStructTypeOrNull()) { -+#endif - const StructLayout *sl = kmodule->targetData->getStructLayout(st); - const ConstantInt *ci = cast(ii.getOperand()); - uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue()); - constantOffset = constantOffset->Add(ConstantExpr::alloc(addend, - Context::get().getPointerWidth())); -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - } else if (ii->isArrayTy() || ii->isVectorTy() || ii->isPointerTy()) { -+#else -+ } else if (ii.isSequential()) { -+#endif - computeOffsetsSeqTy(kgepi, constantOffset, index, ii); - } else - assert("invalid type" && 0); -@@ -3405,15 +3429,66 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) { - void Executor::bindInstructionConstants(KInstruction *KI) { - if (GetElementPtrInst *gepi = dyn_cast(KI->inst)) { - KGEPInstruction *kgepi = static_cast(KI); -- computeOffsets(kgepi, gep_type_begin(gepi), gep_type_end(gepi)); -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) -+ computeOffsets(kgepi, klee::gep_type_begin(gepi), klee::gep_type_end(gepi)); -+#else -+ computeOffsets(kgepi, llvm::gep_type_begin(gepi), llvm::gep_type_end(gepi)); -+#endif - } else if (InsertValueInst *ivi = dyn_cast(KI->inst)) { - KGEPInstruction *kgepi = static_cast(KI); -+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0) - computeOffsets(kgepi, iv_type_begin(ivi), iv_type_end(ivi)); - assert(kgepi->indices.empty() && "InsertValue constant offset expected"); -+#else -+ llvm::Value *agg = ivi->getAggregateOperand(); -+ llvm::Type *current_type = agg->getType(); -+ uint64_t offset = 0; -+ for (auto index : ivi->indices()) { -+ if (StructType *st = dyn_cast(current_type)) { -+ const StructLayout *sl = kmodule->targetData->getStructLayout(st); -+ uint64_t addend = sl->getElementOffset(index); -+ offset = offset + addend; -+ } else if (current_type->isArrayTy() || current_type->isVectorTy() || -+ current_type->isPointerTy()) { -+ uint64_t elementSize = kmodule->targetData->getTypeStoreSize( -+ current_type->getArrayElementType()); -+ offset += elementSize * index; -+ } else { -+ assert(0 && "Unknown type"); -+ } -+ -+ current_type = GetElementPtrInst::getTypeAtIndex(current_type, index); -+ } -+ kgepi->offset = offset; -+#endif - } else if (ExtractValueInst *evi = dyn_cast(KI->inst)) { - KGEPInstruction *kgepi = static_cast(KI); -+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0) - computeOffsets(kgepi, ev_type_begin(evi), ev_type_end(evi)); - assert(kgepi->indices.empty() && "ExtractValue constant offset expected"); -+#else -+ -+ llvm::Value *agg = evi->getAggregateOperand(); -+ llvm::Type *current_type = agg->getType(); -+ uint64_t offset = 0; -+ for (auto index : evi->indices()) { -+ if (StructType *st = dyn_cast(current_type)) { -+ const StructLayout *sl = kmodule->targetData->getStructLayout(st); -+ uint64_t addend = sl->getElementOffset(index); -+ offset = offset + addend; -+ } else if (current_type->isArrayTy() || current_type->isVectorTy() || -+ current_type->isPointerTy()) { -+ uint64_t elementSize = kmodule->targetData->getTypeStoreSize( -+ current_type->getArrayElementType()); -+ offset += elementSize * index; -+ } else { -+ assert(0 && "Unknown type"); -+ } -+ -+ current_type = GetElementPtrInst::getTypeAtIndex(current_type, index); -+ } -+ kgepi->offset = offset; -+#endif - } - } - -diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp -index 718b1c31..7b43218b 100644 ---- a/lib/Core/ExternalDispatcher.cpp -+++ b/lib/Core/ExternalDispatcher.cpp -@@ -250,7 +250,7 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) { - } - - // FIXME: This might have been relevant for the old JIT but the MCJIT --// has a completly different implementation so this comment below is -+// has a completely different implementation so this comment below is - // likely irrelevant and misleading. - // - // For performance purposes we construct the stub in such a way that the -@@ -283,13 +283,20 @@ Function *ExternalDispatcherImpl::createDispatcher(KCallable *target, - - llvm::IRBuilder<> Builder(dBB); - // Get a Value* for &gTheArgsP, as an i64**. -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+ auto argI64sp = Builder.CreateIntToPtr( -+ ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)&gTheArgsP), -+ PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), -+ "argsp"); -+ auto argI64s = Builder.CreateLoad(Builder.getPtrTy(), argI64sp, "args"); -+#else - auto argI64sp = Builder.CreateIntToPtr( - ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)(void *)&gTheArgsP), - PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), - "argsp"); - auto argI64s = Builder.CreateLoad( - argI64sp->getType()->getPointerElementType(), argI64sp, "args"); -- -+#endif - // Get the target function type. - FunctionType *FTy = target->getFunctionType(); - -@@ -306,6 +313,14 @@ Function *ExternalDispatcherImpl::createDispatcher(KCallable *target, - if (argTy->isX86_FP80Ty() && idx & 0x01) - idx++; - -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+ auto argI64p = -+ Builder.CreateGEP(Builder.getPtrTy(), argI64s, -+ ConstantInt::get(Type::getInt32Ty(ctx), idx)); -+ -+ auto argp = Builder.CreateBitCast(argI64p, PointerType::getUnqual(argTy)); -+ args[i] = Builder.CreateLoad(argTy, argp); -+#else - auto argI64p = - Builder.CreateGEP(argI64s->getType()->getPointerElementType(), argI64s, - ConstantInt::get(Type::getInt32Ty(ctx), idx)); -@@ -313,6 +328,7 @@ Function *ExternalDispatcherImpl::createDispatcher(KCallable *target, - auto argp = Builder.CreateBitCast(argI64p, PointerType::getUnqual(argTy)); - args[i] = - Builder.CreateLoad(argp->getType()->getPointerElementType(), argp); -+#endif - - unsigned argSize = argTy->getPrimitiveSizeInBits(); - idx += ((!!argSize ? argSize : 64) + 63) / 64; -diff --git a/lib/Core/GetElementPtrTypeIterator.h b/lib/Core/GetElementPtrTypeIterator.h -index d8b0e097..4e0314cb 100644 ---- a/lib/Core/GetElementPtrTypeIterator.h -+++ b/lib/Core/GetElementPtrTypeIterator.h -@@ -144,14 +144,6 @@ public: - return iv_type_iterator::end(IV->idx_end()); - } - -- inline vce_type_iterator vce_type_begin(const llvm::ConstantExpr *CE) { -- return vce_type_iterator::begin(CE->getOperand(0)->getType(), -- CE->getIndices().begin()); -- } -- inline vce_type_iterator vce_type_end(const llvm::ConstantExpr *CE) { -- return vce_type_iterator::end(CE->getIndices().end()); -- } -- - template - inline generic_gep_type_iterator gep_type_begin(llvm::Type *Op0, ItTy I, - ItTy E) { -diff --git a/lib/Module/FunctionAlias.cpp b/lib/Module/FunctionAlias.cpp -index aa80b35d..c00bde58 100644 ---- a/lib/Module/FunctionAlias.cpp -+++ b/lib/Module/FunctionAlias.cpp -@@ -134,10 +134,16 @@ bool FunctionAliasPass::runOnModule(Module &M) { - } - - const FunctionType *FunctionAliasPass::getFunctionType(const GlobalValue *gv) { -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+ if (auto *ft = dyn_cast(gv->getType())) -+ return ft; -+ return dyn_cast(gv->getValueType()); -+#else - const Type *type = gv->getType(); - while (type->isPointerTy()) - type = type->getPointerElementType(); -- return cast(type); -+ return dyn_cast(type); -+#endif - } - - bool FunctionAliasPass::checkType(const GlobalValue *match, -diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp -index ad7c0631..40ff2874 100644 ---- a/lib/Module/IntrinsicCleaner.cpp -+++ b/lib/Module/IntrinsicCleaner.cpp -@@ -100,9 +100,14 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { - Builder.CreatePointerCast(dst, i8pp, "vacopy.cast.dst"); - auto castedSrc = - Builder.CreatePointerCast(src, i8pp, "vacopy.cast.src"); -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+ auto load = Builder.CreateLoad(Builder.getInt8PtrTy(), castedSrc, -+ "vacopy.read"); -+#else - auto load = - Builder.CreateLoad(castedSrc->getType()->getPointerElementType(), - castedSrc, "vacopy.read"); -+#endif - Builder.CreateStore(load, castedDst, false /* isVolatile */); - } else { - assert(WordSize == 8 && "Invalid word size!"); -@@ -110,9 +115,13 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { - auto pDst = Builder.CreatePointerCast(dst, i64p, "vacopy.cast.dst"); - auto pSrc = Builder.CreatePointerCast(src, i64p, "vacopy.cast.src"); - -+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0) -+ auto pSrcType = Builder.getPtrTy(); -+ auto pDstType = Builder.getPtrTy(); -+#else - auto pSrcType = pSrc->getType()->getPointerElementType(); - auto pDstType = pDst->getType()->getPointerElementType(); -- -+#endif - auto val = Builder.CreateLoad(pSrcType, pSrc); - Builder.CreateStore(val, pDst, ii); - --- -2.43.0 - diff --git a/0012-Fix-test-cases-to-support-opaque-pointers.patch b/0012-Fix-test-cases-to-support-opaque-pointers.patch deleted file mode 100644 index ea1c54d..0000000 --- a/0012-Fix-test-cases-to-support-opaque-pointers.patch +++ /dev/null @@ -1,229 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:48:58 +0000 -Subject: Fix test cases to support opaque pointers -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - test/CXX/LandingPad.cpp | 2 + - test/Concrete/CMakeLists.txt | 4 ++ - test/Feature/KleeStats.c | 2 +- - test/Feature/VarArgByVal.c | 8 +-- - test/Feature/VarArgByValOld.c | 131 ++++++++++++++++++++++++++++++++++ - test/Feature/asm_lifting.ll | 2 +- - 6 files changed, 143 insertions(+), 6 deletions(-) - create mode 100644 test/Feature/VarArgByValOld.c - -diff --git a/test/CXX/LandingPad.cpp b/test/CXX/LandingPad.cpp -index 18cad7c8..6b6e6748 100644 ---- a/test/CXX/LandingPad.cpp -+++ b/test/CXX/LandingPad.cpp -@@ -1,3 +1,5 @@ -+// REQUIRES: lt-llvm-15.0 -+// Different LLVM IR syntax with opaque ptr - it's a nullptr directly, no constant - // RUN: %clangxx %s -emit-llvm -c -o %t1.bc - // RUN: rm -rf %t.klee-out - // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s -diff --git a/test/Concrete/CMakeLists.txt b/test/Concrete/CMakeLists.txt -index e7cf2416..a073482c 100644 ---- a/test/Concrete/CMakeLists.txt -+++ b/test/Concrete/CMakeLists.txt -@@ -8,4 +8,8 @@ - #===------------------------------------------------------------------------===# - - set(OZERO_OPT "-O0 -Xclang -disable-O0-optnone") -+if ("${LLVM_VERSION_MAJOR}" EQUAL 15) -+ set(LLVM_AS_FLAGS "-opaque-pointers") -+ set(LLVM_LINK_FLAGS "-opaque-pointers") -+endif () - configure_file(Makefile.cmake.test.in Makefile.cmake.test @ONLY) -diff --git a/test/Feature/KleeStats.c b/test/Feature/KleeStats.c -index 2a498beb..8045f22e 100644 ---- a/test/Feature/KleeStats.c -+++ b/test/Feature/KleeStats.c -@@ -29,7 +29,7 @@ int main(){ - // First check we find a line with the expected format - // CHECK-STATS: Path,Instrs,Time(s),ICov(%),BCov(%),ICount,TSolver(%),ActiveStates,MaxActiveStates,Mem(MiB),MaxMem(MiB) - // Check there is a line with .klee-out dir, non zero instruction, less than 1 second execution time and 100 ICov. --// CHECK-STATS: {{.*\.klee-out,[1-9]+,[0-9]+\.([0-9]+),100\.00}} -+// CHECK-STATS: {{.*\.klee-out,[1-9][0-9]+,[0-9]+\.([0-9]+),100\.00}} - - // Check other formats - // CHECK-STATS-ABS-TIMES: Path,Time(s),TUser(s),TResolve(s),TCex(s),TSolver(s),TFork(s) -diff --git a/test/Feature/VarArgByVal.c b/test/Feature/VarArgByVal.c -index 551e6c63..7b979f61 100644 ---- a/test/Feature/VarArgByVal.c -+++ b/test/Feature/VarArgByVal.c -@@ -1,4 +1,5 @@ --/* This test checks that KLEE correctly handles variadic arguments with the -+// REQUIRES: geq-llvm-15.0 -+/* This test checks that KLEE correctly handles variadic arguments with the - byval attribute */ - - // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc -@@ -7,9 +8,8 @@ - // RUN: FileCheck %s --input-file=%t.klee-out/assembly.ll - // - // TODO: Make noundef unconditional when LLVM 14 is the oldest supported version. --// CHECK: @test1({{.*}}, i32 {{(noundef )?}}-1, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval --// CHECK: @test2({{.*}}, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval -- -+// CHECK: call void (ptr, i32, ...) @test1(ptr sret(%struct.foo) align 8 {{.*}}, i32 noundef -1, ptr noundef byval(%struct.foo) align 8 {{.*}}, ptr noundef byval(%struct.bar) align 8 {{.*}}) -+// CHECK: call void (ptr, i32, i64, ...) @test2(ptr sret(%struct.foo) align 8 %tmp, i32 noundef {{.*}}, i64 noundef {{.*}}, i32 noundef {{.*}}, ptr noundef byval(%struct.foo) align 8 {{.*}}, i64 noundef {{.*}}, ptr noundef byval(%struct.bar) align 8 {{.*}}, ptr noundef byval(%struct.foo) align 8 {{.*}}, ptr noundef byval(%struct.bar) align 8 {{.*}}) - #include - #include - #include -diff --git a/test/Feature/VarArgByValOld.c b/test/Feature/VarArgByValOld.c -new file mode 100644 -index 00000000..011046d8 ---- /dev/null -+++ b/test/Feature/VarArgByValOld.c -@@ -0,0 +1,131 @@ -+// REQUIRES: lt-llvm-15.0 -+/* This test checks that KLEE correctly handles variadic arguments with the -+ byval attribute */ -+ -+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc -+// RUN: rm -rf %t.klee-out -+// RUN: %klee --exit-on-error --output-dir=%t.klee-out %t1.bc -+// RUN: FileCheck %s --input-file=%t.klee-out/assembly.ll -+// -+// TODO: Make noundef unconditional when LLVM 14 is the oldest supported version. -+// CHECK: @test1({{.*}}, i32 {{(noundef )?}}-1, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval -+// CHECK: @test2({{.*}}, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval -+#include -+#include -+#include -+ -+struct foo { -+ char f1; -+ long long f2; -+ long long f3; -+ char f4; -+ long f5; -+ int f6; -+ char f7; -+}; -+ -+struct bar { -+ long long int f1; -+ char f2; -+ long long f3; -+ char f4; -+ long f5; -+}; -+ -+struct foo test1(int x, ...) { -+ va_list ap; -+ va_start(ap, x); -+ assert(x == -1); -+ -+ struct foo f = va_arg(ap, struct foo); -+ assert(f.f1 == 1); -+ assert(f.f2 == 2); -+ assert(f.f3 == 3); -+ assert(f.f4 == 4); -+ assert(f.f5 == 5); -+ assert(f.f6 == 6); -+ assert(f.f7 == 7); -+ -+ struct bar b = va_arg(ap, struct bar); -+ assert(b.f1 == 11); -+ assert(b.f2 == 12); -+ assert(b.f3 == 13); -+ assert(b.f4 == 14); -+ assert(b.f5 == 15); -+ -+ va_end(ap); -+ -+ f.f1++; -+ return f; -+} -+ -+struct foo test2(int x, long long int l, ...) { -+ va_list ap; -+ va_start(ap, l); -+ assert(x == 10); -+ assert(l == 1000); -+ -+ int i = va_arg(ap, int); -+ assert(i == 10); -+ -+ struct foo f = va_arg(ap, struct foo); -+ assert(f.f1 == 1); -+ assert(f.f2 == 2); -+ assert(f.f3 == 3); -+ assert(f.f4 == 4); -+ assert(f.f5 == 5); -+ assert(f.f6 == 6); -+ assert(f.f7 == 7); -+ -+ l = va_arg(ap, long long int); -+ assert(l == 1000); -+ -+ struct bar b = va_arg(ap, struct bar); -+ assert(b.f1 == 11); -+ assert(b.f2 == 12); -+ assert(b.f3 == 13); -+ assert(b.f4 == 14); -+ assert(b.f5 == 15); -+ -+ f = va_arg(ap, struct foo); -+ assert(f.f1 == 10); -+ assert(f.f2 == 20); -+ assert(f.f3 == 30); -+ assert(f.f4 == 40); -+ assert(f.f5 == 50); -+ assert(f.f6 == 60); -+ assert(f.f7 == 70); -+ -+ b = va_arg(ap, struct bar); -+ assert(b.f1 == 1); -+ assert(b.f2 == 3); -+ assert(b.f3 == 5); -+ assert(b.f4 == 7); -+ assert(b.f5 == 9); -+ -+ va_end(ap); -+ -+ f.f1++; -+ return f; -+} -+ -+int main() { -+ struct foo f = {1, 2, 3, 4, 5, 6, 7}; -+ struct bar b = {11, 12, 13, 14, 15}; -+ struct foo res = test1(-1, f, b); -+ assert(res.f1 == 2); -+ assert(res.f2 == 2); -+ assert(res.f3 == 3); -+ assert(res.f4 == 4); -+ assert(res.f5 == 5); -+ assert(res.f6 == 6); -+ assert(res.f7 == 7); -+ // check that f was not modified, as it's passed by value -+ assert(f.f1 == 1); -+ -+ int i = 10; -+ long long int l = 1000; -+ struct foo f2 = {10, 20, 30, 40, 50, 60, 70}; -+ struct bar b2 = {1, 3, 5, 7, 9}; -+ test2(i, l, i, f, l, b, f2, b2); -+} -diff --git a/test/Feature/asm_lifting.ll b/test/Feature/asm_lifting.ll -index d99db0cf..115bc2f9 100644 ---- a/test/Feature/asm_lifting.ll -+++ b/test/Feature/asm_lifting.ll -@@ -17,7 +17,7 @@ entry: - %1 = getelementptr inbounds [47 x i8], [47 x i8]* %0, i64 0, i64 0 - ; Make sure memory barrier with function arguments is kept - %2 = call i8* asm sideeffect "", "=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1) -- ; CHECK: %2 = call i8* asm sideeffect "", "=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1) -+ ; CHECK: %2 = call {{.*}} asm sideeffect "", "=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"({{.*}} nonnull %1) - ret i32 0 - } - --- -2.43.0 - diff --git a/0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch b/0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch deleted file mode 100644 index 088f583..0000000 --- a/0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch +++ /dev/null @@ -1,33 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:50:51 +0000 -Subject: Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT` -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - test/Concrete/_testingUtils.c | 5 ++--- - 1 file changed, 2 insertions(+), 3 deletions(-) - -diff --git a/test/Concrete/_testingUtils.c b/test/Concrete/_testingUtils.c -index fa395820..d51c6969 100644 ---- a/test/Concrete/_testingUtils.c -+++ b/test/Concrete/_testingUtils.c -@@ -69,12 +69,11 @@ int main(int argc, char *argv[]) - printf("print_i1(0)\n"); - print_i1(0); - // CHECK: i1(0) -- // CHECK_NEXT: 0 -+ // CHECK-NEXT: 0 - - printf("print_i1(1)\n"); - print_i1(1); - // CHECK: i1(1) -- // CHECK_NEXT: 1 -- -+ // CHECK-NEXT: 1 - } - #endif --- -2.43.0 - diff --git a/0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch b/0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch deleted file mode 100644 index e87b451..0000000 --- a/0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch +++ /dev/null @@ -1,152 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:52:37 +0000 -Subject: Use APIs of newer LLVM versions instead of unsupported ones -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - include/klee/Expr/Expr.h | 8 +++++++- - lib/Core/Executor.cpp | 18 ++++++++++++++++++ - lib/Module/LowerSwitch.cpp | 14 ++++++-------- - lib/Module/RaiseAsm.cpp | 6 ++++++ - 4 files changed, 37 insertions(+), 9 deletions(-) - -diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h -index 15075eb8..eb936c3d 100644 ---- a/include/klee/Expr/Expr.h -+++ b/include/klee/Expr/Expr.h -@@ -1117,7 +1117,13 @@ public: - } - - /// isAllOnes - Is this constant all ones. -- bool isAllOnes() const { return getAPValue().isAllOnesValue(); } -+ bool isAllOnes() const { -+#if LLVM_VERSION_CODE <= LLVM_VERSION(13, 0) -+ return getAPValue().isAllOnesValue(); -+#else -+ return getAPValue().isAllOnes(); -+#endif -+ } - - /* Constant Operations */ - -diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp -index 58c15141..792b0c76 100644 ---- a/lib/Core/Executor.cpp -+++ b/lib/Core/Executor.cpp -@@ -2985,7 +2985,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { - llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); - uint64_t value = 0; - bool isExact = true; -+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0) -+ auto valueRef = llvm::MutableArrayRef(value); -+#else - auto valueRef = makeMutableArrayRef(value); -+#endif - Arg.convertToInteger(valueRef, resultType, false, - llvm::APFloat::rmTowardZero, &isExact); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); -@@ -3003,7 +3007,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { - - uint64_t value = 0; - bool isExact = true; -+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0) -+ auto valueRef = llvm::MutableArrayRef(value); -+#else - auto valueRef = makeMutableArrayRef(value); -+#endif - Arg.convertToInteger(valueRef, resultType, true, - llvm::APFloat::rmTowardZero, &isExact); - bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); -@@ -4846,7 +4854,12 @@ size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const { - type = GO->getType(); - } - } else if (const AllocaInst *AI = dyn_cast(allocSite)) { -+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0) - alignment = AI->getAlignment(); -+ -+#else -+ alignment = AI->getAlign().value(); -+#endif - type = AI->getAllocatedType(); - } else if (isa(allocSite) || isa(allocSite)) { - // FIXME: Model the semantics of the call to use the right alignment -@@ -4869,7 +4882,12 @@ size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const { - assert(type != NULL); - // No specified alignment. Get the alignment for the type. - if (type->isSized()) { -+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0) -+ alignment = kmodule->targetData->getPrefTypeAlign(type).value(); -+#else - alignment = kmodule->targetData->getPrefTypeAlignment(type); -+#endif -+ - } else { - klee_warning_once(allocSite, "Cannot determine memory alignment for " - "\"%s\". Using alignment of %zu.", -diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp -index 84b04b24..f8473156 100644 ---- a/lib/Module/LowerSwitch.cpp -+++ b/lib/Module/LowerSwitch.cpp -@@ -70,9 +70,8 @@ void LowerSwitchPass::switchConvert(CaseItr begin, CaseItr end, - - // iterate through all the cases, creating a new BasicBlock for each - for (CaseItr it = begin; it < end; ++it) { -- BasicBlock *newBlock = BasicBlock::Create(F->getContext(), "NodeBlock"); -- Function::iterator FI = origBlock->getIterator(); -- F->getBasicBlockList().insert(++FI, newBlock); -+ BasicBlock *newBlock = BasicBlock::Create(F->getContext(), "NodeBlock", F); -+ - Builder.SetInsertPoint(newBlock); - auto cmpValue = Builder.CreateICmpEQ(value, it->value, "case.cmp"); - Builder.CreateCondBr(cmpValue, it->block, curHead); -@@ -106,10 +105,10 @@ void LowerSwitchPass::processSwitchInst(SwitchInst *SI) { - - // Create a new, empty default block so that the new hierarchy of - // if-then statements go to this and the PHI nodes are happy. -- BasicBlock* newDefault = BasicBlock::Create(F->getContext(), "newDefault"); -+ BasicBlock *newDefault = -+ BasicBlock::Create(F->getContext(), "newDefault", F, defaultBlock); - llvm::IRBuilder<> Builder(newDefault); - -- F->getBasicBlockList().insert(defaultBlock->getIterator(), newDefault); - Builder.CreateBr(defaultBlock); - - // If there is an entry in any PHI nodes for the default edge, make sure -@@ -132,11 +131,10 @@ void LowerSwitchPass::processSwitchInst(SwitchInst *SI) { - // the if comparisons will happen in the same order - // as the cases appear in the switch - std::reverse(cases.begin(), cases.end()); -- -- switchConvert(cases.begin(), cases.end(), switchValue, origBlock, newDefault); - -+ switchConvert(cases.begin(), cases.end(), switchValue, origBlock, newDefault); - // We are now done with the switch instruction, so delete it -- origBlock->getInstList().erase(SI); -+ SI->eraseFromParent(); - } - - } -diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp -index ec447bc4..799218c9 100644 ---- a/lib/Module/RaiseAsm.cpp -+++ b/lib/Module/RaiseAsm.cpp -@@ -91,8 +91,14 @@ bool RaiseAsmPass::runOnModule(Module &M) { - klee_warning("Warning: unable to select target: %s", Err.c_str()); - TLI = 0; - } else { -+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0) -+ TM = Target->createTargetMachine(TargetTriple, "", "", TargetOptions(), -+ std::nullopt); -+#else - TM = Target->createTargetMachine(TargetTriple, "", "", TargetOptions(), - None); -+#endif -+ - TLI = TM->getSubtargetImpl(*(M.begin()))->getTargetLowering(); - - triple = llvm::Triple(TargetTriple); --- -2.43.0 - diff --git a/0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch b/0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch deleted file mode 100644 index a4a8b53..0000000 --- a/0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch +++ /dev/null @@ -1,32 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:53:48 +0000 -Subject: Add support for `Intrinsic::get_rounding` for LLVM 16 -Patch-mainline: no -References: llvm16 - -`Intrinsic::flt_rounds` got removed - -Signed-off-by: Jiri Slaby ---- - lib/Module/IntrinsicCleaner.cpp | 4 ++++ - 1 file changed, 4 insertions(+) - -diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp -index 40ff2874..af77ed70 100644 ---- a/lib/Module/IntrinsicCleaner.cpp -+++ b/lib/Module/IntrinsicCleaner.cpp -@@ -366,7 +366,11 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { - case Intrinsic::experimental_noalias_scope_decl: - #endif - case Intrinsic::floor: -+#if LLVM_VERSION_CODE < LLVM_VERSION(16, 0) - case Intrinsic::flt_rounds: -+#else -+ case Intrinsic::get_rounding: -+#endif - case Intrinsic::frameaddress: - case Intrinsic::get_dynamic_area_offset: - case Intrinsic::invariant_end: --- -2.43.0 - diff --git a/0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch b/0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch deleted file mode 100644 index b714728..0000000 --- a/0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch +++ /dev/null @@ -1,28 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:54:46 +0000 -Subject: Add support to `aligned_alloc` generated by LLVM -Patch-mainline: no -References: llvm16 - -Handle like `memalign` for now. - -Signed-off-by: Jiri Slaby ---- - lib/Core/SpecialFunctionHandler.cpp | 1 + - 1 file changed, 1 insertion(+) - -diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp -index 488fba51..79a86112 100644 ---- a/lib/Core/SpecialFunctionHandler.cpp -+++ b/lib/Core/SpecialFunctionHandler.cpp -@@ -87,6 +87,7 @@ static constexpr std::array handlerInfo = { - addDNR("klee_abort", handleAbort), - addDNR("klee_silent_exit", handleSilentExit), - addDNR("klee_report_error", handleReportError), -+ add("aligned_alloc", handleMemalign, true), - add("calloc", handleCalloc, true), - add("free", handleFree, false), - add("klee_assume", handleAssume, false), --- -2.43.0 - diff --git a/0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch b/0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch deleted file mode 100644 index 9233022..0000000 --- a/0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch +++ /dev/null @@ -1,69 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:56:27 +0000 -Subject: Disable unsupported passes for newer LLVM versions -Patch-mainline: no -References: llvm16 - -Similar functionality needs to be added using a new pass manager - -Signed-off-by: Jiri Slaby ---- - lib/Module/OptimizeLegacy.cpp | 14 ++++++++++++-- - 1 file changed, 12 insertions(+), 2 deletions(-) - -diff --git a/lib/Module/OptimizeLegacy.cpp b/lib/Module/OptimizeLegacy.cpp -index 53488924..20c8ac2a 100644 ---- a/lib/Module/OptimizeLegacy.cpp -+++ b/lib/Module/OptimizeLegacy.cpp -@@ -98,14 +98,18 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) { - addPass(PM, createInstructionCombiningPass()); // Clean up after IPCP & DAE - addPass(PM, createCFGSimplificationPass()); // Clean up after IPCP & DAE - -+#if LLVM_VERSION_CODE <= LLVM_VERSION(15, 0) - addPass(PM, createPruneEHPass()); // Remove dead EH info -+#endif - addPass(PM, createPostOrderFunctionAttrsLegacyPass()); - addPass(PM, - createReversePostOrderFunctionAttrsPass()); // Deduce function attrs - - if (!DisableInline) - addPass(PM, createFunctionInliningPass()); // Inline small functions -- addPass(PM, createArgumentPromotionPass()); // Scalarize uninlined fn args -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) -+ addPass(PM, createArgumentPromotionPass()); // Scalarize uninlined fn args -+#endif - - addPass(PM, createInstructionCombiningPass()); // Cleanup for scalarrepl. - addPass(PM, createJumpThreadingPass()); // Thread jumps. -@@ -118,7 +122,9 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) { - addPass(PM, createReassociatePass()); // Reassociate expressions - addPass(PM, createLoopRotatePass()); - addPass(PM, createLICMPass()); // Hoist loop invariants -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - addPass(PM, createLoopUnswitchPass()); // Unswitch loops. -+#endif - // FIXME : Removing instcombine causes nestedloop regression. - addPass(PM, createInstructionCombiningPass()); - addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars -@@ -197,13 +203,17 @@ void klee::optimizeModule(llvm::Module *M, - if (!DisableInline) - addPass(Passes, createFunctionInliningPass()); // Inline small functions - -- addPass(Passes, createPruneEHPass()); // Remove dead EH info -+#if LLVM_VERSION_CODE <= LLVM_VERSION(15, 0) -+ addPass(Passes, createPruneEHPass()); // Remove dead EH info -+#endif - addPass(Passes, createGlobalOptimizerPass()); // Optimize globals again. - addPass(Passes, createGlobalDCEPass()); // Remove dead functions - -+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0) - // If we didn't decide to inline a function, check to see if we can - // transform it to pass arguments by value instead of by reference. - addPass(Passes, createArgumentPromotionPass()); -+#endif - - // The IPO passes may leave cruft around. Clean up after them. - addPass(Passes, createInstructionCombiningPass()); --- -2.43.0 - diff --git a/0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch b/0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch deleted file mode 100644 index cebe26f..0000000 --- a/0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch +++ /dev/null @@ -1,29 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:57:41 +0000 -Subject: Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions. -Patch-mainline: no -References: llvm16 - -The optimiser generates different code and calls fwrite directly instead. - -Signed-off-by: Jiri Slaby ---- - test/regression/2018-10-30-llvm-pr39177.ll | 4 +++- - 1 file changed, 3 insertions(+), 1 deletion(-) - -diff --git a/test/regression/2018-10-30-llvm-pr39177.ll b/test/regression/2018-10-30-llvm-pr39177.ll -index 027d0d30..b28947ab 100644 ---- a/test/regression/2018-10-30-llvm-pr39177.ll -+++ b/test/regression/2018-10-30-llvm-pr39177.ll -@@ -1,5 +1,7 @@ -+; REQUIRES: lt-llvm-15.0 -+; The optimizer is more efficient and uses fwrite directly in newer LLVM versions - ; RUN: rm -rf %t.klee-out --; RUN: %llvmas -f %s -o - | %klee -optimize -output-dir=%t.klee-out | FileCheck %s -+; RUN: %klee -optimize -output-dir=%t.klee-out %s | FileCheck %s - target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" - target triple = "x86_64-unknown-linux-gnu" - --- -2.43.0 - diff --git a/0019-Handle-check-for-thrown-libc-exceptions-more-general.patch b/0019-Handle-check-for-thrown-libc-exceptions-more-general.patch deleted file mode 100644 index 4b4a232..0000000 --- a/0019-Handle-check-for-thrown-libc-exceptions-more-general.patch +++ /dev/null @@ -1,40 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 14:59:07 +0000 -Subject: Handle check for thrown libc++ exceptions more general -Patch-mainline: no -References: llvm16 - -The wording changed slightly in newer versions. -Update the test case to support this. - -Signed-off-by: Jiri Slaby ---- - test/CXX/symex/libc++/nested_fail.cpp | 2 +- - test/CXX/symex/libc++/simple_exception_fail.cpp | 2 +- - 2 files changed, 2 insertions(+), 2 deletions(-) - -diff --git a/test/CXX/symex/libc++/nested_fail.cpp b/test/CXX/symex/libc++/nested_fail.cpp -index 4dce0279..fe2df4c9 100644 ---- a/test/CXX/symex/libc++/nested_fail.cpp -+++ b/test/CXX/symex/libc++/nested_fail.cpp -@@ -24,4 +24,4 @@ int main(int argc, char **args) { - } - return 0; - } --// CHECK: terminating with uncaught exception of type char* -+// CHECK: terminating {{.*}} uncaught exception of type char* -diff --git a/test/CXX/symex/libc++/simple_exception_fail.cpp b/test/CXX/symex/libc++/simple_exception_fail.cpp -index 793d9201..c3e295c2 100644 ---- a/test/CXX/symex/libc++/simple_exception_fail.cpp -+++ b/test/CXX/symex/libc++/simple_exception_fail.cpp -@@ -11,4 +11,4 @@ - int main(int argc, char **args) { - throw std::runtime_error("foo"); - } --// CHECK: terminating with uncaught exception of type std::runtime_error: foo -\ No newline at end of file -+// CHECK: terminating {{.*}} uncaught exception of type std::runtime_error: foo -\ No newline at end of file --- -2.43.0 - diff --git a/0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch b/0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch deleted file mode 100644 index 644df05..0000000 --- a/0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch +++ /dev/null @@ -1,242 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 15:00:58 +0000 -Subject: Update test case for expressions using `udiv`, `urem`, `sdiv` and - `srem` -Patch-mainline: no -References: llvm16 - -They are not supported anymore for newer LLVM versions. - -Signed-off-by: Jiri Slaby ---- - test/Concrete/ConstantExpr.ll | 29 +----- - test/Concrete/ConstantExprOld.ll | 166 +++++++++++++++++++++++++++++++ - 2 files changed, 167 insertions(+), 28 deletions(-) - create mode 100644 test/Concrete/ConstantExprOld.ll - -diff --git a/test/Concrete/ConstantExpr.ll b/test/Concrete/ConstantExpr.ll -index efe9f141..b85ce36a 100644 ---- a/test/Concrete/ConstantExpr.ll -+++ b/test/Concrete/ConstantExpr.ll -@@ -1,3 +1,4 @@ -+; REQUIRES: geq-llvm-15.0 - ; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s - - ; Most of the test below use the *address* of gInt as part of their computation, -@@ -86,32 +87,6 @@ define void @"test_simple_arith"() { - - ret void - } -- --define void @"test_div_and_mod"() { -- %t1 = add i32 udiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -- %t2 = add i32 urem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -- %t3 = add i32 sdiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -- %t4 = add i32 srem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -- -- %p = ptrtoint i32* @gInt to i32 -- -- %i1 = udiv i32 %p, 13 -- %i2 = urem i32 %p, 13 -- %i3 = sdiv i32 %p, 13 -- %i4 = srem i32 %p, 13 -- -- %x1 = sub i32 %t1, %i1 -- %x2 = sub i32 %t2, %i2 -- %x3 = sub i32 %t3, %i3 -- %x4 = sub i32 %t4, %i4 -- -- call void @print_i32(i32 %x1) -- call void @print_i32(i32 %x2) -- call void @print_i32(i32 %x3) -- call void @print_i32(i32 %x4) -- -- ret void --} - - define void @test_cmp() { - %t1 = add i8 zext(i1 icmp ult (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -@@ -142,8 +117,6 @@ define void @test_cmp() { - define i32 @main() { - call void @test_simple_arith() - -- call void @test_div_and_mod() -- - call void @test_cmp() - - call void @test_int_to_ptr() -diff --git a/test/Concrete/ConstantExprOld.ll b/test/Concrete/ConstantExprOld.ll -new file mode 100644 -index 00000000..2e6438bc ---- /dev/null -+++ b/test/Concrete/ConstantExprOld.ll -@@ -0,0 +1,166 @@ -+; REQUIRES: lt-llvm-15.0 -+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s -+ -+; Most of the test below use the *address* of gInt as part of their computation, -+; and then perform some operation (like x | ~x) which makes the result -+; deterministic. They do, however, assume that the sign bit of the address as a -+; 64-bit value will never be set. -+@gInt = global i32 10 -+@gIntWithConstant = global i32 sub(i32 ptrtoint(i32* @gInt to i32), -+ i32 ptrtoint(i32* @gInt to i32)) -+ -+define void @"test_int_to_ptr"() { -+ %t1 = add i8 ptrtoint(i8* inttoptr(i32 100 to i8*) to i8), 0 -+ %t2 = add i32 ptrtoint(i32* inttoptr(i8 100 to i32*) to i32), 0 -+ %t3 = add i32 ptrtoint(i32* inttoptr(i64 100 to i32*) to i32), 0 -+ %t4 = add i64 ptrtoint(i8* inttoptr(i32 100 to i8*) to i64), 0 -+ -+ call void @print_i8(i8 %t1) -+ call void @print_i32(i32 %t2) -+ call void @print_i32(i32 %t3) -+ call void @print_i64(i64 %t4) -+ -+ ret void -+} -+ -+define void @"test_constant_ops"() { -+ %t1 = add i8 trunc(i64 add(i64 ptrtoint(i32* @gInt to i64), i64 -10) to i8), 10 -+ %t2 = and i64 sub(i64 sext(i32 ptrtoint(i32* @gInt to i32) to i64), i64 ptrtoint(i32* @gInt to i64)), 4294967295 -+ %t3 = and i64 sub(i64 zext(i32 ptrtoint(i32* @gInt to i32) to i64), i64 ptrtoint(i32* @gInt to i64)), 4294967295 -+ -+ %t4 = icmp eq i8 trunc(i64 ptrtoint(i32* @gInt to i64) to i8), %t1 -+ %t5 = zext i1 %t4 to i8 -+ -+ call void @print_i8(i8 %t5) -+ call void @print_i64(i64 %t2) -+ call void @print_i64(i64 %t3) -+ -+ ret void -+} -+ -+define void @"test_logical_ops"() { -+ %t1 = add i32 -10, and(i32 ptrtoint(i32* @gInt to i32), i32 xor(i32 ptrtoint(i32* @gInt to i32), i32 -1)) -+ %t2 = add i32 -10, or(i32 ptrtoint(i32* @gInt to i32), i32 xor(i32 ptrtoint(i32* @gInt to i32), i32 -1)) -+ %t3 = add i32 -10, xor(i32 xor(i32 ptrtoint(i32* @gInt to i32), i32 1024), i32 ptrtoint(i32* @gInt to i32)) -+ -+ call void @print_i32(i32 %t1) -+ call void @print_i32(i32 %t2) -+ call void @print_i32(i32 %t3) -+ -+ ; or the address with 1 to ensure the addresses will differ in 'ne' below -+ %t4 = shl i64 lshr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 -+ %t5 = shl i64 ashr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 -+ %t6 = lshr i64 shl(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 -+ -+ %t7 = icmp eq i64 %t4, %t5 -+ %t8 = icmp ne i64 %t4, %t6 -+ -+ %t9 = zext i1 %t7 to i8 -+ %t10 = zext i1 %t8 to i8 -+ -+ call void @print_i8(i8 %t9) -+ call void @print_i8(i8 %t10) -+ -+ ret void -+} -+ -+%test.struct.type = type { i32, i32 } -+@test_struct = global %test.struct.type { i32 0, i32 10 } -+ -+define void @"test_misc"() { -+ ; probability that @gInt == 100 is very very low -+ %t1 = add i32 select(i1 icmp eq (i32* @gInt, i32* inttoptr(i32 100 to i32*)), i32 10, i32 0), 0 -+ call void @print_i32(i32 %t1) -+ -+ %t2 = load i32, i32* getelementptr(%test.struct.type, %test.struct.type* @test_struct, i32 0, i32 1) -+ call void @print_i32(i32 %t2) -+ -+ ret void -+} -+ -+define void @"test_simple_arith"() { -+ %t1 = add i32 add(i32 ptrtoint(i32* @gInt to i32), i32 0), 0 -+ %t2 = add i32 sub(i32 0, i32 ptrtoint(i32* @gInt to i32)), %t1 -+ %t3 = mul i32 mul(i32 ptrtoint(i32* @gInt to i32), i32 10), %t2 -+ -+ call void @print_i32(i32 %t3) -+ -+ ret void -+} -+ -+define void @"test_div_and_mod"() { -+ %t1 = add i32 udiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -+ %t2 = add i32 urem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -+ %t3 = add i32 sdiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -+ %t4 = add i32 srem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0 -+ -+ %p = ptrtoint i32* @gInt to i32 -+ -+ %i1 = udiv i32 %p, 13 -+ %i2 = urem i32 %p, 13 -+ %i3 = sdiv i32 %p, 13 -+ %i4 = srem i32 %p, 13 -+ -+ %x1 = sub i32 %t1, %i1 -+ %x2 = sub i32 %t2, %i2 -+ %x3 = sub i32 %t3, %i3 -+ %x4 = sub i32 %t4, %i4 -+ -+ call void @print_i32(i32 %x1) -+ call void @print_i32(i32 %x2) -+ call void @print_i32(i32 %x3) -+ call void @print_i32(i32 %x4) -+ -+ ret void -+} -+ -+define void @test_cmp() { -+ %t1 = add i8 zext(i1 icmp ult (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t2 = add i8 zext(i1 icmp ule (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t3 = add i8 zext(i1 icmp uge (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t4 = add i8 zext(i1 icmp ugt (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t5 = add i8 zext(i1 icmp slt (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t6 = add i8 zext(i1 icmp sle (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t7 = add i8 zext(i1 icmp sge (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t8 = add i8 zext(i1 icmp sgt (i64 ptrtoint(i32* @gInt to i64), i64 0) to i8), 1 -+ %t9 = add i8 zext(i1 icmp eq (i64 ptrtoint(i32* @gInt to i64), i64 10) to i8), 1 -+ %t10 = add i8 zext(i1 icmp ne (i64 ptrtoint(i32* @gInt to i64), i64 10) to i8), 1 -+ -+ call void @print_i1(i8 %t1) -+ call void @print_i1(i8 %t2) -+ call void @print_i1(i8 %t3) -+ call void @print_i1(i8 %t4) -+ call void @print_i1(i8 %t5) -+ call void @print_i1(i8 %t6) -+ call void @print_i1(i8 %t7) -+ call void @print_i1(i8 %t8) -+ call void @print_i1(i8 %t9) -+ call void @print_i1(i8 %t10) -+ -+ ret void -+} -+ -+define i32 @main() { -+ call void @test_simple_arith() -+ -+ call void @test_div_and_mod() -+ -+ call void @test_cmp() -+ -+ call void @test_int_to_ptr() -+ -+ call void @test_constant_ops() -+ -+ call void @test_logical_ops() -+ -+ call void @test_misc() -+ -+ ret i32 0 -+} -+ -+; defined in print_int.c -+declare void @print_i1(i8) -+declare void @print_i8(i8) -+declare void @print_i16(i16) -+declare void @print_i32(i32) -+declare void @print_i64(i64) --- -2.43.0 - diff --git a/0021-Support-newer-LLVM-versions-in-lit.patch b/0021-Support-newer-LLVM-versions-in-lit.patch deleted file mode 100644 index 81a9a62..0000000 --- a/0021-Support-newer-LLVM-versions-in-lit.patch +++ /dev/null @@ -1,27 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 15:02:08 +0000 -Subject: Support newer LLVM versions in `lit` -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - test/lit.cfg | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/test/lit.cfg b/test/lit.cfg -index c442c409..ec654a47 100644 ---- a/test/lit.cfg -+++ b/test/lit.cfg -@@ -164,7 +164,7 @@ config.substitutions.append( - - # Add feature for the LLVM version in use, so it can be tested in REQUIRES and - # XFAIL checks. We also add "not-XXX" variants, for the same reason. --known_llvm_versions = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.0" } -+known_llvm_versions = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.0", "15.0", "16.0", "17.0" } - current_llvm_version_tuple = (int(config.llvm_version_major), int(config.llvm_version_minor)) - current_llvm_version = "%s.%s" % current_llvm_version_tuple - --- -2.43.0 - diff --git a/0022-Enable-CI-to-test-newer-LLVM-versions.patch b/0022-Enable-CI-to-test-newer-LLVM-versions.patch deleted file mode 100644 index cb6de8f..0000000 --- a/0022-Enable-CI-to-test-newer-LLVM-versions.patch +++ /dev/null @@ -1,40 +0,0 @@ -From: Martin Nowack -Date: Mon, 30 Oct 2023 15:03:34 +0000 -Subject: Enable CI to test newer LLVM versions -Patch-mainline: no -References: llvm16 - -Signed-off-by: Jiri Slaby ---- - .github/workflows/build.yaml | 8 ++++++++ - 1 file changed, 8 insertions(+) - -diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml -index fa924a37..a329a02c 100644 ---- a/.github/workflows/build.yaml -+++ b/.github/workflows/build.yaml -@@ -36,6 +36,8 @@ jobs: - strategy: - matrix: - name: [ -+ "LLVM 16", -+ "LLVM 15", - "LLVM 14", - "LLVM 13", - "LLVM 12", -@@ -53,6 +55,12 @@ jobs: - "No TCMalloc, optimised runtime", - ] - include: -+ - name: "LLVM 16" -+ env: -+ LLVM_VERSION: 16 -+ - name: "LLVM 15" -+ env: -+ LLVM_VERSION: 15 - - name: "LLVM 14" - env: - LLVM_VERSION: 14 --- -2.43.0 - diff --git a/_servicedata b/_servicedata index c76b766..b2ef906 100644 --- a/_servicedata +++ b/_servicedata @@ -1,4 +1,4 @@ https://github.com/klee/klee - fc83f06b17221bf5ef20e30d9da1ccff927beb17 \ No newline at end of file + 9336cd28f6e58c2f9bc01ec3dbf3930688ad0287 \ No newline at end of file diff --git a/klee-3.0+20231023.obscpio b/klee-3.0+20231023.obscpio deleted file mode 100644 index bb6c8fd..0000000 --- a/klee-3.0+20231023.obscpio +++ /dev/null @@ -1,3 +0,0 @@ -version https://git-lfs.github.com/spec/v1 -oid sha256:5480ed13b30907521bcaf76be6eeba7a2c98e6234bc08b4ee3fa66e97d239b3b -size 19110413 diff --git a/klee-3.0+20240208.obscpio b/klee-3.0+20240208.obscpio new file mode 100644 index 0000000..bc4259f --- /dev/null +++ b/klee-3.0+20240208.obscpio @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:369037b90832d02a041cde740d55d02fa779a8c007d48f3c9667eb419242e142 +size 19196429 diff --git a/klee.changes b/klee.changes index 5e7c8d2..6ddc2a7 100644 --- a/klee.changes +++ b/klee.changes @@ -1,3 +1,51 @@ +------------------------------------------------------------------- +Fri Feb 09 07:40:49 UTC 2024 - jslaby@suse.cz + +- Update to version 3.0+20240208: + * Add space between include and main function for updated test cases + * Mention default value in help text for `--strip-all` and `--strip-debug` + * Use `std::` namespace for `uint64_t` + * Enable CI to test newer LLVM versions + * Support newer LLVM versions in `lit` + * Update test case for expressions using `udiv`, `urem`, `sdiv` and `srem` + * Handle check for thrown libc++ exceptions more general + * Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions. + * Disable unsupported passes for newer LLVM versions + * Add support to `aligned_alloc` generated by LLVM + * Add support for `Intrinsic::get_rounding` for LLVM 16 + * Use APIs of newer LLVM versions instead of unsupported ones + * Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT` + * Fix test cases to support opaque pointers + * Add support for opaque pointers + * Explicitly enable opaque pointer support for LLVM 15 + * Explicitly build KLEE's exception handling runtime with C++11 + * Assume C compiler's default standard is `-std=gnu17` + * Use KLEE's uClibc v1.4 as default to support the compilation with newer compilers + * Refactor invocation of old pass manager into legacy function +- remove (they were upstreamed) + * 0001-Add-support-to-build-newer-LLVM-versions.patch + * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch + * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch + * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch + * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch + * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch + * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch + * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch + * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch + * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch + * 0011-Add-support-for-opaque-pointers.patch + * 0012-Fix-test-cases-to-support-opaque-pointers.patch + * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch + * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch + * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch + * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch + * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch + * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch + * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch + * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch + * 0021-Support-newer-LLVM-versions-in-lit.patch + * 0022-Enable-CI-to-test-newer-LLVM-versions.patch + ------------------------------------------------------------------- Thu Dec 14 07:40:13 UTC 2023 - jslaby@suse.cz diff --git a/klee.obsinfo b/klee.obsinfo index e476ac8..a245b5e 100644 --- a/klee.obsinfo +++ b/klee.obsinfo @@ -1,4 +1,4 @@ name: klee -version: 3.0+20231023 -mtime: 1698093351 -commit: fc83f06b17221bf5ef20e30d9da1ccff927beb17 +version: 3.0+20240208 +mtime: 1707398239 +commit: 9336cd28f6e58c2f9bc01ec3dbf3930688ad0287 diff --git a/klee.spec b/klee.spec index 571508e..da09b4c 100644 --- a/klee.spec +++ b/klee.spec @@ -1,7 +1,7 @@ # # spec file for package klee # -# Copyright (c) 2023 SUSE LLC +# Copyright (c) 2024 SUSE LLC # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -30,35 +30,13 @@ Name: klee Summary: LLVM Execution Engine License: NCSA Group: Development/Languages/Other -Version: 3.0+20231023 +Version: 3.0+20240208 Release: 0 URL: http://klee.github.io/ Source0: %{name}-%{version}.tar.xz Source1: %{name}-rpmlintrc Source2: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/not/not.cpp Source3: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/FileCheck/FileCheck.cpp -Patch1: 0001-Add-support-to-build-newer-LLVM-versions.patch -Patch2: 0002-Add-support-for-newer-libc-Simplify-path-detection.patch -Patch3: 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch -Patch4: 0004-Fix-klee-libc-memchr.c-compiler-warning.patch -Patch5: 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch -Patch6: 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch -Patch7: 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch -Patch8: 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch -Patch9: 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch -Patch10: 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch -Patch11: 0011-Add-support-for-opaque-pointers.patch -Patch12: 0012-Fix-test-cases-to-support-opaque-pointers.patch -Patch13: 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch -Patch14: 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch -Patch15: 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch -Patch16: 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch -Patch17: 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch -Patch18: 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch -Patch19: 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch -Patch20: 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch -Patch21: 0021-Support-newer-LLVM-versions-in-lit.patch -Patch22: 0022-Enable-CI-to-test-newer-LLVM-versions.patch Patch100: 0001-test-disable-failing-tests-with-llvm-15.patch BuildRequires: clang%{llvm_version} @@ -151,13 +129,8 @@ ninja check %doc NEWS README.md %license LICENSE.TXT %{_bindir}/kleaver -%{_bindir}/klee -%{_bindir}/klee-replay -%{_bindir}/klee-stats -%{_bindir}/klee-zesti -%{_bindir}/ktest-gen -%{_bindir}/ktest-randgen -%{_bindir}/ktest-tool +%{_bindir}/klee* +%{_bindir}/ktest-* %{_includedir}/klee/ %{_libdir}/libkleeRuntest.so* %dir %{_libdir}/klee/