[feat] Added Bitwuzla solver in list of available solvers.

.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

CMakeLists.txt

@@ -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")

build.sh

@@ -35,7 +35,7 @@ REQUIRES_RTTI=0
 
 ## 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

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()

include/klee/Config/config.h.cmin

@@ -13,6 +13,9 @@
 /* Using Z3 Solver backend */
 #cmakedefine ENABLE_Z3 @ENABLE_Z3@
 
+/* Using Bitwuzla Solver backend */
+#cmakedefine ENABLE_BITWUZLA @ENABLE_BITWUZLA@
+
 /* Enable KLEE floating point extension */
 #cmakedefine ENABLE_FP @ENABLE_FP@
 

include/klee/Expr/Constraints.h

@@ -49,7 +49,11 @@ class ConstraintSet {
   bool isSymcretized(ref<Expr> expr) const;
 
   void rewriteConcretization(const Assignment &a);
-  ConstraintSet withExpr(ref<Expr> e) const;
+  ConstraintSet withExpr(ref<Expr> e) const {
+    ConstraintSet copy = ConstraintSet(*this);
+    copy.addConstraint(e, Assignment());
+    return copy;
+  }
 
   std::vector<const Array *> gatherArrays() const;
   std::vector<const Array *> gatherSymcretizedArrays() const;

include/klee/Solver/SolverCmdLine.h

@@ -65,6 +65,8 @@ enum QueryLoggingSolverType {
 extern llvm::cl::bits<QueryLoggingSolverType> QueryLoggingOptions;
 
 enum CoreSolverType {
+  BITWUZLA_SOLVER,
+  BITWUZLA_TREE_SOLVER,
   STP_SOLVER,
   METASMT_SOLVER,
   DUMMY_SOLVER,