feat: Add Smithril

.github/workflows/build.yaml

@@ -39,6 +39,7 @@ env:
   Z3_VERSION: 4.8.15
   SQLITE_VERSION: 3400100
   BITWUZLA_VERSION: 0.7.0
+  SMITHRIL_VERSION: v0.1.1
   JSON_VERSION: v3.11.3
   IMMER_VERSION: v0.8.1
 
@@ -59,8 +60,9 @@ jobs:
           "MSan",
           "Z3 only",
           "metaSMT",
-          "STP master",
+          # "STP master",
           "Bitwuzla only",
+          "Smithril only",
           "Latest klee-uclibc",
           "Asserts disabled",
           "No TCMalloc, optimised runtime",
@@ -118,14 +120,18 @@ jobs:
               METASMT_DEFAULT: STP
               REQUIRES_RTTI: 1
           # Test we can build against STP master
-          - name: "STP master"
-            env:
-              SOLVERS: STP
-              STP_VERSION: master
+          # - name: "STP master"
+          #   env:
+          #     SOLVERS: STP
+          #     STP_VERSION: master
           # Test just using Bitwuzla only
           - name: "Bitwuzla only"
             env:
               SOLVERS: BITWUZLA
+          # Test just using Smithril only
+          - name: "Smithril only"
+            env:
+              SOLVERS: SMITHRIL
           # Check we can build latest klee-uclibc branch
           - name: "Latest klee-uclibc"
             env:

CMakeLists.txt

@@ -208,15 +208,18 @@ include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake)
 include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake)
 # bitwuzla
 include(${CMAKE_SOURCE_DIR}/cmake/find_bitwuzla.cmake)
+# smithril
+include(${CMAKE_SOURCE_DIR}/cmake/find_smithril.cmake)
 
 
-if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA}))
+if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA}) AND (NOT ${ENABLE_SMITHRIL}))
   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_BITWUZLA=ON\"\n"
+    "\"-DENABLE_SOLVER_SMITHRIL=ON\"\n"
     "\"-DENABLE_SOLVER_METASMT=ON\"
     ")
 endif()
@@ -490,8 +493,8 @@ endif()
 ################################################################################
 option(ENABLE_FLOATING_POINT "Enable KLEE's floating point extension" OFF)
 if (ENABLE_FLOATING_POINT)
-  if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA}))
-    message (FATAL_ERROR "Floating point extension is availible only when using Z3 backend."
+  if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA}) AND (NOT ${ENABLE_SMITHRIL}))
+    message (FATAL_ERROR "Floating point extension is availible only when using Z3, Bitwuzla or Smithril backend."
             "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()

build.sh

@@ -27,7 +27,7 @@ USE_LIBCXX=1
 SQLITE_VERSION="3400100"
 
 ## LLVM Required options
-LLVM_VERSION=16
+LLVM_VERSION=14
 ENABLE_OPTIMIZED=1
 ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
@@ -36,7 +36,7 @@ ENABLE_WARNINGS_AS_ERRORS=0
 
 ## Solvers Required options
 # SOLVERS=STP
-SOLVERS=BITWUZLA:Z3:STP
+SOLVERS=SMITHRIL:BITWUZLA:Z3
 
 ## Google Test Required options
 GTEST_VERSION=1.16.0
@@ -58,6 +58,7 @@ STP_VERSION=2.3.3
 MINISAT_VERSION=master
 
 BITWUZLA_VERSION=0.7.0
+SMITHRIL_VERSION=v0.1.1
 
 KEEP_PARSE="true"
 while [ $KEEP_PARSE = "true" ]; do
@@ -72,4 +73,4 @@ else
 fi
 done
 
-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 ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./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 SMITHRIL_VERSION=$SMITHRIL_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 ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps

cmake/find_smithril.cmake

@@ -0,0 +1,40 @@
+#===------------------------------------------------------------------------===#
+#
+#                     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(SMITHRIL IMPORTED_TARGET smithril)
+
+if (SMITHRIL_FOUND)
+  set(ENABLE_SOLVER_SMITHRIL_DEFAULT ON)
+else()
+  set(ENABLE_SOLVER_SMITHRIL_DEFAULT OFF)
+endif()
+
+option(ENABLE_SOLVER_SMITHRIL "Enable Smithril solver support" ${ENABLE_SOLVER_SMITHRIL_DEFAULT})
+
+if (ENABLE_SOLVER_SMITHRIL)
+  message(STATUS "Smithril solver support enabled")
+  if (SMITHRIL_FOUND)
+    message(STATUS "Found Smithril")
+    set(ENABLE_SMITHRIL 1) # For config.h
+
+    message(STATUS "Found Smithril libraries: \"${SMITHRIL_LIBRARIES}\"")
+    message(STATUS "Found Smithril include path: \"${SMITHRIL_INCLUDE_DIRS}\"")
+    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${SMITHRIL_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARIES ${SMITHRIL_LINK_LIBRARIES})
+    list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${SMITHRIL_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${SMITHRIL_LINK_LIBRARIES})
+
+  else()
+    message(FATAL_ERROR "Smithril not found.")
+  endif()
+else()
+  message(STATUS "Smithril solver support disabled")
+  set(ENABLE_SMITHRIL 0) # For config.h
+endif()

include/klee/Config/config.h.cmin

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

include/klee/Solver/SolverCmdLine.h

@@ -65,6 +65,8 @@ enum CoreSolverType {
   BITWUZLA_SOLVER,
   BITWUZLA_TREE_SOLVER,
   STP_SOLVER,
+  SMITHRIL_SOLVER,
+  SMITHRIL_TREE_SOLVER,
   METASMT_SOLVER,
   DUMMY_SOLVER,
   Z3_SOLVER,

lib/Solver/CMakeLists.txt

@@ -25,6 +25,9 @@ add_library(kleaverSolver
   MetaSMTSolver.cpp
   KQueryLoggingSolver.cpp
   QueryLoggingSolver.cpp
+  SmithrilBuilder.cpp
+  SmithrilHashConfig.cpp
+  SmithrilSolver.cpp
   SMTLIBLoggingSolver.cpp
   Solver.cpp
   SolverCmdLine.cpp

lib/Solver/CoreSolver.cpp

@@ -13,6 +13,10 @@
 #include "BitwuzlaSolver.h"
 #endif
 
+#ifdef ENABLE_SMITHRIL
+#include "SmithrilSolver.h"
+#endif
+
 #ifdef ENABLE_METASMT
 #include "MetaSMTSolver.h"
 #endif
@@ -102,8 +106,20 @@ std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
                    MaxSolversApproxTreeInc.ArgStr.str().c_str());
     }
     return std::make_unique<BitwuzlaSolver>();
+#endif
+  case SMITHRIL_TREE_SOLVER:
+  case SMITHRIL_SOLVER:
+#ifdef ENABLE_SMITHRIL
+    klee_message("Using Smithril solver backend");
+    if (isTreeSolver) {
+      if (MaxSolversApproxTreeInc > 0)
+        return std::make_unique<SmithrilTreeSolver>(MaxSolversApproxTreeInc);
+      klee_warning("--%s is 0, so falling back to non tree-incremental solver",
+                   MaxSolversApproxTreeInc.ArgStr.str().c_str());
+    }
+    return std::make_unique<SmithrilSolver>();
 #else
-    klee_message("Not compiled with Bitwuzla support");
+    klee_message("Not compiled with Smithril support");
     return NULL;
 #endif
   case NO_SOLVER: