misonijnik · misonijnik · Aug 20, 2023 · Aug 20, 2023 · Aug 20, 2023 · Aug 20, 2023
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -21,14 +21,16 @@ env:
   LLVM_VERSION: 11
   MINISAT_VERSION: "master"
   REQUIRES_RTTI: 0
-  SOLVERS: Z3:STP
+  SOLVERS: BITWUZLA:Z3:STP
   STP_VERSION: 2.3.3
   TCMALLOC_VERSION: 2.9.1
   UCLIBC_VERSION: klee_uclibc_v1.3
   USE_TCMALLOC: 1
   USE_LIBCXX: 1
   Z3_VERSION: 4.8.15
   SQLITE_VERSION: 3400100
+  BITWUZLA_VERSION: main
+  BITWUZLA_COMMIT: 80ef7cd803e1c71b5939c3eb951f1736388f7090
 
 jobs:
   Linux:
@@ -48,6 +50,7 @@ jobs:
           "Z3 only",
           "metaSMT",
           "STP master",
+          "Bitwuzla only",
           "Latest klee-uclibc",
           "Asserts disabled",
           "No TCMalloc, optimised runtime",
@@ -109,6 +112,10 @@ jobs:
             env:
               SOLVERS: STP
               STP_VERSION: master
+          # Test just using Bitwuzla only
+          - name: "Bitwuzla only"
+            env:
+              SOLVERS: BITWUZLA
           # Check we can build latest klee-uclibc branch
           - name: "Latest klee-uclibc"
             env:
@@ -172,6 +179,7 @@ jobs:
         name: [
           "STP",
           "Z3",
+          "Bitwuzla",
         ]
         include:
           - name: "STP"
@@ -180,6 +188,9 @@ jobs:
           - name: "Z3"
             env:
               SOLVERS: Z3:STP
+          - name: "Bitwuzla"
+            env:
+              SOLVERS: BITWUZLA:Z3
     env:
       ENABLE_OPTIMIZED: 0
       COVERAGE: 1

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -17,16 +17,16 @@ project(KLEE CXX C)
 # Project version
 ###############################################################################
 set(KLEE_VERSION_MAJOR 3)
-set(KLEE_VERSION_MINOR 0-utbot)
+set(KLEE_VERSION_MINOR 0)
 set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}")
 
 # If a patch is needed, we can add KLEE_VERSION_PATCH
 # set(KLEE_VERSION_PATCH 0)
 # set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}.${KLEE_VERSION_PATCH}")
 
-message(STATUS "KLEE version ${KLEE_VERSION}")
-set(PACKAGE_STRING "\"KLEE ${KLEE_VERSION}\"")
-set(PACKAGE_URL "\"https://klee.github.io\"")
+message(STATUS "KLEEF version ${KLEE_VERSION}")
+set(PACKAGE_STRING "\"KLEEF ${KLEE_VERSION}\"")
+set(PACKAGE_URL "\"https://toolchain-labs.com/projects/kleef.html\"")
 
 ################################################################################
 # Sanity check - Disallow building in source.
@@ -204,14 +204,19 @@ include(${CMAKE_SOURCE_DIR}/cmake/find_stp.cmake)
 include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake)
 # metaSMT
 include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake)
+# bitwuzla
+include(${CMAKE_SOURCE_DIR}/cmake/find_bitwuzla.cmake)
 
-if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}))
+
+if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA}))
   message(FATAL_ERROR "No solver was specified. At least one solver is required."
     "You should enable a solver by passing one of more the following options"
     " to cmake:\n"
     "\"-DENABLE_SOLVER_STP=ON\"\n"
     "\"-DENABLE_SOLVER_Z3=ON\"\n"
-    "\"-DENABLE_SOLVER_METASMT=ON\"")
+    "\"-DENABLE_SOLVER_BITWUZLA=ON\"\n"
+    "\"-DENABLE_SOLVER_METASMT=ON\"
+    ")
 endif()
 
 ###############################################################################
@@ -473,10 +478,10 @@ endif()
 ################################################################################
 option(ENABLE_FLOATING_POINT "Enable KLEE's floating point extension" OFF)
 if (ENABLE_FLOATING_POINT)
-  if (NOT ${ENABLE_Z3})
+  if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA}))
     message (FATAL_ERROR "Floating point extension is availible only when using Z3 backend."
-            "You should enable Z3 by passing the following option to cmake:\n"
-            "\"-DENABLE_SOLVER_Z3=ON\"\n")
+            "You should enable either Z3 or Bitwuzla by passing the following options to cmake, respectively:\n"
+            "\"-DENABLE_SOLVER_Z3=ON\" or \"-DENABLE_SOLVER_BITWUZLA=ON\"\n")
   else()
     set(ENABLE_FP 1) # For config.h
     message(STATUS "Floating point extension enabled")
@@ -506,19 +511,29 @@ endif()
 # KLEE uclibc support
 ################################################################################
 set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory")
-set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca")
+
+set(KLEE_UCLIBC_BCA_32_NAME "klee-uclibc-32.bca")
+set(KLEE_UCLIBC_BCA_64_NAME "klee-uclibc-64.bca")
+
 if (NOT KLEE_UCLIBC_PATH STREQUAL "")
   # Find the C library bitcode archive
-  set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a")
-  if (NOT EXISTS "${KLEE_UCLIBC_C_BCA}")
+  set(KLEE_UCLIBC_C_32_BCA "${KLEE_UCLIBC_PATH}-32/lib/libc.a")
+  set(KLEE_UCLIBC_C_64_BCA "${KLEE_UCLIBC_PATH}-64/lib/libc.a")
+
+  if (NOT EXISTS "${KLEE_UCLIBC_C_32_BCA}" OR NOT EXISTS "${KLEE_UCLIBC_C_64_BCA}")
     message(FATAL_ERROR
-      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\". Set KLEE_UCLIBC_PATH to klee-uclibc root directory or empty string.")
+      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_32_BCA}\" or \"${KLEE_UCLIBC_C_64_BCA}\". Set KLEE_UCLIBC_PATH to klee-uclibc root directory or empty string.")
   endif()
-  message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_BCA}\"")
+  message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_32_BCA}\" and \"${KLEE_UCLIBC_C_64_BCA}\"")
   # Copy KLEE_UCLIBC_C_BCA so KLEE can find it where it is expected.
+  # Create 32 and 64 bit versions
   execute_process(COMMAND ${CMAKE_COMMAND} -E copy
-    "${KLEE_UCLIBC_C_BCA}"
-    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_NAME}"
+    "${KLEE_UCLIBC_C_32_BCA}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_32_NAME}"
+  )
+  execute_process(COMMAND ${CMAKE_COMMAND} -E copy
+    "${KLEE_UCLIBC_C_64_BCA}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_64_NAME}"
   )
 else()
   message(STATUS "Skipping copying of klee-uclibc runtime")
@@ -633,6 +648,12 @@ unset(_flags)
 configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/config.h.cmin
   ${CMAKE_BINARY_DIR}/include/klee/Config/config.h)
 
+################################################################################
+# Generate `klee/klee.h` and `klee-test-comp.c`
+################################################################################
+configure_file(${CMAKE_SOURCE_DIR}/include/klee/klee.h ${CMAKE_BINARY_DIR}/include/klee/klee.h COPYONLY)
+configure_file(${CMAKE_SOURCE_DIR}/include/klee-test-comp.c ${CMAKE_BINARY_DIR}/include/klee-test-comp.c COPYONLY)
+
 ################################################################################
 # Generate `CompileTimeInfo.h`
 ################################################################################

diff --git a/README.md b/README.md
@@ -1,27 +1,9 @@
-KLEE Symbolic Virtual Machine
+KLEEF Symbolic Virtual Machine
 =============================
 
-[![Build Status](https://github.com/klee/klee/workflows/CI/badge.svg)](https://github.com/klee/klee/actions?query=workflow%3ACI)
-[![Build Status](https://api.cirrus-ci.com/github/klee/klee.svg)](https://cirrus-ci.com/github/klee/klee)
-[![Coverage](https://codecov.io/gh/klee/klee/branch/master/graph/badge.svg)](https://codecov.io/gh/klee/klee)
+[![Build Status](https://github.com/UnitTestBot/klee/workflows/CI/badge.svg)](https://github.com/UnitTestBot/klee/actions?query=workflow%3ACI)
+[![Coverage](https://codecov.io/gh/UnitTestBot/klee/branch/main/graph/badge.svg)](https://codecov.io/gh/UnitTestBot/klee)
 
-`KLEE` is a symbolic virtual machine built on top of the LLVM compiler
-infrastructure. Currently, there are two primary components:
+`KLEEF` is a complete overhaul of the KLEE symbolic execution engine for LLVM, fine-tuned for a robust analysis of industrial C/C++ code.
 
-  1. The core symbolic virtual machine engine; this is responsible for
-     executing LLVM bitcode modules with support for symbolic
-     values. This is comprised of the code in lib/.
-
-  2. A POSIX/Linux emulation layer oriented towards supporting uClibc,
-     with additional support for making parts of the operating system
-     environment symbolic.
-
-Additionally, there is a simple library for replaying computed inputs
-on native code (for closed programs). There is also a more complicated
-infrastructure for replaying the inputs generated for the POSIX/Linux
-emulation layer, which handles running native programs in an
-environment that matches a computed test input, including setting up
-files, pipes, environment variables, and passing command line
-arguments.
-
-For further information, see the [webpage](http://klee.github.io/).
+For further information, see the [webpage](https://toolchain-labs.com/projects/kleef.html).
diff --git a/build.sh b/build.sh
@@ -29,13 +29,13 @@ SQLITE_VERSION="3400100"
 ## LLVM Required options
 LLVM_VERSION=14
 ENABLE_OPTIMIZED=1
-ENABLE_DEBUG=1
+ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
 REQUIRES_RTTI=1
 
 ## Solvers Required options
 # SOLVERS=STP
-SOLVERS=STP:Z3
+SOLVERS=BITWUZLA:Z3:STP
 
 ## Google Test Required options
 GTEST_VERSION=1.11.0
@@ -46,7 +46,11 @@ UCLIBC_VERSION=klee_uclibc_v1.3
 
 ## Z3 Required options
 Z3_VERSION=4.8.15
+
 STP_VERSION=2.3.3
 MINISAT_VERSION=master
 
-BASE="$BASE" 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 SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps
+BITWUZLA_VERSION=main
+BITWUZLA_COMMIT=80ef7cd803e1c71b5939c3eb951f1736388f7090
+
+BASE="$BASE" 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 BITWUZLA_COMMIT=$BITWUZLA_COMMIT SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps
diff --git a/cmake/find_bitwuzla.cmake b/cmake/find_bitwuzla.cmake
@@ -0,0 +1,46 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+find_package (PkgConfig REQUIRED)
+pkg_check_modules(BITWUZLA IMPORTED_TARGET bitwuzla)
+
+# Set the default so that if the following is true:
+# * Bitwuzla was found
+# * ENABLE_SOLVER_BITWUZLA is not already set as a cache variable
+#
+# then the default is set to `ON`. Otherwise set the default to `OFF`.
+# A consequence of this is if we fail to detect Bitwuzla the first time
+# subsequent calls to CMake will not change the default.
+
+if(BITWUZLA_FOUND)
+  set(ENABLE_SOLVER_BITWUZLA_DEFAULT ON)
+else()
+  set(ENABLE_SOLVER_BITWUZLA_DEFAULT OFF)
+endif()
+
+option(ENABLE_SOLVER_BITWUZLA "Enable Bitwuzla solver support" ${ENABLE_SOLVER_BITWUZLA_DEFAULT})
+
+if (ENABLE_SOLVER_BITWUZLA)
+  message(STATUS "Bitwuzla solver support enabled")
+  if (BITWUZLA_FOUND)
+    message(STATUS "Found Bitwuzla")
+    set(ENABLE_BITWUZLA 1) # For config.h
+
+    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARIES ${BITWUZLA_LINK_LIBRARIES})
+    list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${BITWUZLA_LINK_LIBRARIES})
+
+  else()
+    message(FATAL_ERROR "Bitwuzla not found.")
+  endif()
+else()
+  message(STATUS "Bitwuzla solver support disabled")
+  set(ENABLE_BITWUZLA 0) # For config.h
+endif()
diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c
@@ -7,31 +7,42 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include <stdint.h>
 #ifdef EXTERNAL
 #include "klee.h"
 #include <assert.h>
 #include <stddef.h>
-#include <stdint.h>
 #include <stdlib.h>
 #else
 void klee_make_symbolic(void *addr, unsigned int nbytes, const char *name);
 void klee_assume(_Bool condition);
 __attribute__((noreturn)) void klee_silent_exit(int status);
 void __assert_fail(const char *assertion, const char *file, unsigned int line,
                    const char *function);
+void klee_prefer_cex(void *, uintptr_t);
 #endif
 
 int __VERIFIER_nondet_int(void) {
   int x;
   klee_make_symbolic(&x, sizeof(x), "int");
+  klee_prefer_cex(&x, x < 1024);
   return x;
 }
 
 unsigned int __VERIFIER_nondet_uint(void) {
   unsigned int x;
   klee_make_symbolic(&x, sizeof(x), "unsigned int");
+  klee_prefer_cex(&x, x < 1024);
+  return x;
+}
+
+#ifdef __x86_64__
+unsigned __int128 __VERIFIER_nondet_uint128(void) {
+  unsigned __int128 x;
+  klee_make_symbolic(&x, sizeof(x), "unsigned __int128");
   return x;
 }
+#endif
 
 unsigned __VERIFIER_nondet_unsigned(void) {
   unsigned x;
@@ -82,7 +93,7 @@ unsigned long __VERIFIER_nondet_ulong(void) {
 }
 
 double __VERIFIER_nondet_double(void) {
-  long x;
+  double x;
   klee_make_symbolic(&x, sizeof(x), "double");
   return x;
 }
@@ -96,7 +107,7 @@ void *__VERIFIER_nondet_pointer(void) {
 }
 
 float __VERIFIER_nondet_float(void) {
-  int x;
+  float x;
   klee_make_symbolic(&x, sizeof(x), "float");
   return x;
 }