[test]

.cirrus.yml

@@ -1,16 +1,16 @@
 task:
   freebsd_instance:
     matrix:
-      - image_family: freebsd-12-3-snap
-      - image_family: freebsd-13-1-snap
+      - image_family: freebsd-13-2-snap
+      - image_family: freebsd-14-0-snap
   deps_script:
     - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
     - env ASSUME_ALWAYS_YES=yes pkg update -f
-    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate
+    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate nlohmann-json bash coreutils
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
+    - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit11\./' test/lit.cfg

.github/workflows/build-in-base-env.yml

@@ -1,14 +1,15 @@
 name: Build in UTBot base_env
 
 on:
-  pull_request:
-    branches: [utbot-main]
-  push:
-    branches: [utbot-main]
+  workflow_run:
+    workflows: ["Clang Format"]
+    types: 
+      - completed
 
 jobs:
   build:
     runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
     container:
       image: ghcr.io/unittestbot/utbotcpp/base_env:02-02-2022
       credentials:

.github/workflows/build.yaml

@@ -2,10 +2,10 @@
 name: CI
 
 on:
-  pull_request:
-    branches: [main, utbot-main]
-  push:
-    branches: [main, utbot-main]
+  workflow_run:
+    workflows: ["Clang Format"]
+    types: 
+      - completed
 
 # Defaults for building KLEE
 env:
@@ -21,18 +21,21 @@ 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: 0.3.1
+  JSON_VERSION: v3.11.3
 
 jobs:
   Linux:
     runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
     strategy:
       matrix:
         name: [
@@ -48,6 +51,7 @@ jobs:
           "Z3 only",
           "metaSMT",
           "STP master",
+          "Bitwuzla only",
           "Latest klee-uclibc",
           "Asserts disabled",
           "No TCMalloc, optimised runtime",
@@ -109,6 +113,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:
@@ -137,6 +145,7 @@ jobs:
 
   macOS:
     runs-on: macos-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
     env:
       BASE: /tmp
       SOLVERS: STP
@@ -157,6 +166,7 @@ jobs:
 
   Docker:
     runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
     steps:
       - name: Checkout KLEE Code
         uses: actions/checkout@v3
@@ -167,11 +177,13 @@ jobs:
 
   Coverage:
     runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
     strategy:
       matrix:
         name: [
           "STP",
           "Z3",
+          "Bitwuzla",
         ]
         include:
           - name: "STP"
@@ -180,6 +192,9 @@ jobs:
           - name: "Z3"
             env:
               SOLVERS: Z3:STP
+          - name: "Bitwuzla"
+            env:
+              SOLVERS: BITWUZLA:Z3
     env:
       ENABLE_OPTIMIZED: 0
       COVERAGE: 1
@@ -198,14 +213,3 @@ jobs:
       - name: Run tests
         env: ${{ matrix.env }}
         run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug
-
-  clang-format:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout KLEE Code
-        uses: actions/checkout@v2
-      - name: Run clang-format on KLEE Code
-        uses: jidicula/[email protected]
-        with:
-          clang-format-version: '13'
-          include-regex: '(^.*\.((((c|C)(c|pp|xx|\+\+)?$)|((h|H)h?(pp|xx|\+\+)?$))|((ino|pde|proto|cu))$)|^(include|lib)\/.*\.inc)$'

.github/workflows/clang-format.yaml

@@ -0,0 +1,20 @@
+---
+name: Clang Format
+
+on:
+  pull_request:
+    branches: [main, utbot-main]
+  push:
+    branches: [main, utbot-main]
+
+jobs:
+  clang-format:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - uses: actions/setup-python@v4
+      with:
+        python-version: 3.x
+    - uses: pre-commit/[email protected]
+    - uses: pre-commit-ci/[email protected]
+      if: always()

.github/workflows/differential-shellcheck.yml

@@ -4,9 +4,9 @@
 name: Differential ShellCheck
 on:
   push:
-    branches: [master]
+    branches: [main]
   pull_request:
-    branches: [master]
+    branches: [main]
 
 permissions:
   contents: read

.pre-commit-config.yaml

@@ -0,0 +1,7 @@
+files: '(^.*\.((((c|C)(c|pp|xx|\+\+)?$)|((h|H)h?(pp|xx|\+\+)?$))|((ino|pde|proto|cu))$)|^(include|lib)\/.*\.inc)$'
+
+repos:
+- repo: https://github.com/pre-commit/mirrors-clang-format
+  rev: v13.0.1
+  hooks:
+  - id: clang-format

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")
@@ -643,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`
 ################################################################################
@@ -667,8 +678,7 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
 ################################################################################
 include_directories("${CMAKE_BINARY_DIR}/include")
 include_directories("${CMAKE_SOURCE_DIR}/include")
-include_directories("${CMAKE_SOURCE_DIR}/json/include")
-include_directories("${CMAKE_SOURCE_DIR}/optional/include")
+include_directories("${JSON_SRC_DIR}/include")
 # set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
 
 ################################################################################

Dockerfile

@@ -34,6 +34,7 @@ ENV Z3_VERSION=4.8.15
 ENV USE_LIBCXX=1
 ENV KLEE_RUNTIME_BUILD="Debug+Asserts"
 ENV SQLITE_VERSION=3400100
+ENV JSON_VERSION=v3.11.3
 LABEL maintainer="KLEE Developers"
 
 # TODO remove adding sudo package

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

build.sh

@@ -29,24 +29,30 @@ 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
 
+## json options
+JSON_VERSION=v3.11.3
+
 ## UClibC Required options
 UCLIBC_VERSION=klee_uclibc_v1.3
 # LLVM_VERSION is also required for UClibC
 
 ## 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=0.3.1
+
+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 SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION ./scripts/build/build.sh klee --install-system-deps