feat: Take commits from KLEE 3.1

.cirrus.yml

@@ -10,7 +10,7 @@ task:
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
+    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg

.github/workflows/build.yaml

@@ -6,6 +6,12 @@ on:
     branches: [main, utbot-main]
   push:
     branches: [main, utbot-main]
+  workflow_dispatch:
+    inputs:
+      warnings_as_errors:
+        description: 'Warnings as errors'
+        required: true
+        default: 1
 
 # Defaults for building KLEE
 env:
@@ -17,7 +23,7 @@ env:
   ENABLE_DOXYGEN: 0
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
-  ENABLE_WARNINGS_AS_ERRORS: 1
+  ENABLE_WARNINGS_AS_ERRORS: ${{ github.event_name == 'workflow_dispatch' && inputs.warnings_as_errors || 1}}
   GTEST_VERSION: 1.11.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
   LLVM_VERSION: 11
@@ -26,7 +32,7 @@ env:
   SOLVERS: BITWUZLA:Z3:STP
   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
@@ -41,12 +47,12 @@ jobs:
     strategy:
       matrix:
         name: [
+          "LLVM 16",
+          "LLVM 15",
           "LLVM 14",
           "LLVM 13",
           "LLVM 12",
           "LLVM 11, Doxygen",
-          "LLVM 10",
-          "LLVM 9",
           "ASan",
           "UBSan",
           "MSan",
@@ -59,6 +65,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
@@ -72,12 +84,6 @@ jobs:
             env:
               LLVM_VERSION: 11
               ENABLE_DOXYGEN: 1
-          - name: "LLVM 10"
-            env:
-              LLVM_VERSION: 10
-          - name: "LLVM 9"
-            env:
-              LLVM_VERSION: 9
           # Sanitizer builds. Do unoptimized build otherwise the optimizer
           # might remove problematic code
           - name: "ASan"

CMakeLists.txt

@@ -17,7 +17,7 @@ project(KLEE CXX C)
 # Project version
 ###############################################################################
 set(KLEE_VERSION_MAJOR 3)
-set(KLEE_VERSION_MINOR 0)
+set(KLEE_VERSION_MINOR 1)
 set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}")
 
 # If a patch is needed, we can add KLEE_VERSION_PATCH
@@ -317,6 +317,16 @@ if (NOT SQLite3_FOUND)
   message( FATAL_ERROR "SQLite3 not found, please install" )
 endif()
 
+find_program(
+  SQLITE_CLI
+  NAMES "sqlite3"
+  DOC "Path to sqlite3 tool"
+)
+
+if (NOT SQLITE_CLI)
+  set(SQLITE_CLI "")
+endif()
+
 ################################################################################
 # Detect libcap
 ################################################################################
@@ -548,51 +558,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=<path> to CMake where <path> 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=<path> to CMake where <path> 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")

DEBT

@@ -0,0 +1,13 @@
+KLEE 3.1, 29 February 2024
+==========================
+
+- New execution tree implementation and klee-exec-tree tool (@251)
+- KDAlloc is now the default allocator in KLEE (KDAlloc was introduced in KLEE 3.0)
+- Resolve memory reads/writes to single objects in more cases (@tkuchta)
+- Concretize values based on seeds when available (@ccadar)
+
+
+KLEE 3.0, 7 June 2023
+=====================
+
+- Added support for the KDAlloc memory allocator, which enables KLEE to more robustly detect use-after-free errors, improves the detection of buffer overflows, and provides deterministic memory allocation (@danielschemmel, based on https://srg.doc.ic.ac.uk/publications/22-kdalloc-ecoop.html)

Dockerfile

@@ -23,7 +23,7 @@ ENV ENABLE_DOXYGEN=1
 ENV ENABLE_OPTIMIZED=1
 ENV ENABLE_DEBUG=1
 ENV DISABLE_ASSERTIONS=0
-ENV ENABLE_WARNINGS_AS_ERRORS=0
+ENV ENABLE_WARNINGS_AS_ERRORS=1
 ENV REQUIRES_RTTI=0
 ENV SOLVERS=STP:Z3
 ENV GTEST_VERSION=1.11.0

NEWS

@@ -1,3 +1,41 @@
+KLEE 3.1, 29 February 2024
+==========================
+
+Incorporating changes from 8 June 2023 to 29 February 2024.
+Maintainers during this time span: @ccadar, @MartinNowack, @251.
+Documentation at http://klee.github.io/releases/docs/v3.1
+
+== Major features and important changes ==
+- New execution tree implementation and klee-exec-tree tool (@251)
+- KDAlloc is now the default allocator in KLEE (KDAlloc was introduced in KLEE 3.0)
+- Resolve memory reads/writes to single objects in more cases (@tkuchta)
+- Concretize values based on seeds when available (@ccadar)
+- Fixed some interactions with external code (@ccadar, @MartinNowack, mishok2503)
+
+== LLVM support ==
+- Current recommended version is still LLVM 13
+- Added support for LLVM 15 and 16 (@MartinNowack)
+- Removed support for LLVM <11 (@danielschemmel)
+- KLEE 3.1 will be the last version with support for LLVM <13
+
+== Options, scripts and KLEE intrinsics added, changed or removed ==
+- New klee-exec-tree tool (@251)
+- New --write-exec-tree and --exec-tree-batch-size options (@251)
+- Renamed --compress-process-tree to --compress-exec-tree (@ccadar)
+- PTree is now called ExecutionTree in the code (@ccadar)
+- KDAlloc (--kdalloc) is now enabled by default (@ccadar)
+- Replaced --suppress-external-warnings and --all-external-warnings with --external-call-warnings=none|once-per-function|all (@ccadar)
+- Keep in the KLEE and Kleaver help menus only the KLEE/Kleaver option categories (@ccadar)
+- Removed --cex-cache-exp, a broken experimental optimisation for validity (@ccadar)
+- Removed --zero-seed-extension, and merge it with --allow-seed-extension (@ccadar)
+
+== Other changes ==
+- Improvements to KDAlloc (@danielschemmel)
+- Avoid generating array names in solver builders that could accidently collide (@MartinNowack)
+- Function has_permission in the POSIX model now returns permission error a single time in symbolic execution mode (@ccadar)
+- Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @ccadar, @dependabot, @danielschemmel, @davidtr1037, @jbuening, @marco6, @MartinNowack, @McSinyx, @sp1ff)
+
+
 KLEE 3.0, 7 June 2023
 =====================
 

build.sh

@@ -26,11 +26,12 @@ USE_LIBCXX=1
 SQLITE_VERSION="3400100"
 
 ## LLVM Required options
-LLVM_VERSION=14
+LLVM_VERSION=16
 ENABLE_OPTIMIZED=1
 ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
 REQUIRES_RTTI=1
+ENABLE_WARNINGS_AS_ERRORS=0
 
 ## Solvers Required options
 # SOLVERS=STP
@@ -46,7 +47,7 @@ JSON_VERSION=v3.11.3
 IMMER_VERSION=v0.8.1
 
 ## UClibC Required options
-UCLIBC_VERSION=klee_uclibc_v1.3
+UCLIBC_VERSION=klee_uclibc_v1.4
 # LLVM_VERSION is also required for UClibC
 
 ## Z3 Required options
@@ -70,6 +71,4 @@ else
 fi
 done
 
-ENABLE_WARNINGS_AS_ERRORS=0
-
-BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ./scripts/build/build.sh klee --install-system-deps
+BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ./scripts/build/build.sh klee --install-system-deps

include/klee/Core/MockBuilder.h

@@ -9,11 +9,14 @@
 #ifndef KLEE_MOCKBUILDER_H
 #define KLEE_MOCKBUILDER_H
 
+#include "klee/Config/Version.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Module/Annotation.h"
 
+#include "llvm/IR/GlobalVariable.h"
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/Module.h"
+#include "llvm/IR/Value.h"
 
 #include <set>
 #include <string>
@@ -58,7 +61,7 @@ class MockBuilder {
       llvm::Function *func, const std::set<Statement::Property> &properties);
 
   std::map<std::string, llvm::FunctionType *> getExternalFunctions();
-  std::map<std::string, llvm::Type *> getExternalGlobals();
+  std::map<std::string, const llvm::GlobalVariable *> getExternalGlobals();
 
   std::pair<llvm::Value *, llvm::Value *>
   goByOffset(llvm::Value *value, const std::vector<std::string> &offset);
@@ -74,12 +77,20 @@ class MockBuilder {
               std::set<std::string> &mainModuleGlobals);
 
   std::unique_ptr<llvm::Module> build();
+  void buildFree(llvm::Value *elem, const Statement::Free *freePtr);
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+  void buildAllocSource(llvm::Value *prev, llvm::Value *elem,
+                        const Statement::Alloc *allocSourcePtr);
+  void processingValue(llvm::Value *prev, llvm::Value *elem,
+                       const Statement::Alloc *allocSourcePtr,
+                       bool initNullPtr);
+#else
   void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,
                         const Statement::Alloc *allocSourcePtr);
-  void buildFree(llvm::Value *elem, const Statement::Free *freePtr);
   void processingValue(llvm::Value *prev, llvm::Type *elemType,
                        const Statement::Alloc *allocSourcePtr,
                        bool initNullPtr);
+#endif
 };
 
 } // namespace klee

include/klee/Expr/Expr.h

@@ -1592,7 +1592,13 @@ class ConstantExpr : public Expr {
   }
 
   /// 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
+  }
 
   bool isFloat() const { return mIsFloat; }