Add a bunch of features and fixes #1480
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| --- | |
| name: CI | |
| on: | |
| pull_request: | |
| 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: | |
| BASE_IMAGE: ubuntu:jammy-20230126 | |
| REPOSITORY: ghcr.io/unittestbot/klee | |
| BUILD_SUFFIX: "default" | |
| COVERAGE: 0 | |
| DISABLE_ASSERTIONS: 0 | |
| ENABLE_DOXYGEN: 0 | |
| ENABLE_OPTIMIZED: 1 | |
| ENABLE_DEBUG: 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 | |
| MINISAT_VERSION: "master" | |
| REQUIRES_RTTI: 0 | |
| SOLVERS: BITWUZLA:Z3:STP | |
| STP_VERSION: 2.3.3 | |
| TCMALLOC_VERSION: 2.9.1 | |
| UCLIBC_VERSION: klee_uclibc_v1.4 | |
| USE_TCMALLOC: 1 | |
| USE_LIBCXX: 1 | |
| Z3_VERSION: 4.8.15 | |
| SQLITE_VERSION: 3400100 | |
| BITWUZLA_VERSION: 0.6.0 | |
| JSON_VERSION: v3.11.3 | |
| IMMER_VERSION: v0.8.1 | |
| jobs: | |
| Linux: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| name: [ | |
| "LLVM 16", | |
| "LLVM 15", | |
| "LLVM 14", | |
| "LLVM 13", | |
| "LLVM 12", | |
| "LLVM 11, Doxygen", | |
| "ASan", | |
| "UBSan", | |
| "MSan", | |
| "Z3 only", | |
| "metaSMT", | |
| "STP master", | |
| "Bitwuzla only", | |
| "Latest klee-uclibc", | |
| "Asserts disabled", | |
| "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 | |
| - name: "LLVM 13" | |
| env: | |
| LLVM_VERSION: 13 | |
| - name: "LLVM 12" | |
| env: | |
| LLVM_VERSION: 12 | |
| - name: "LLVM 11, Doxygen" | |
| env: | |
| LLVM_VERSION: 11 | |
| ENABLE_DOXYGEN: 1 | |
| # Sanitizer builds. Do unoptimized build otherwise the optimizer | |
| # might remove problematic code | |
| - name: "ASan" | |
| env: | |
| SANITIZER_BUILD: address | |
| ENABLE_OPTIMIZED: 0 | |
| USE_TCMALLOC: 0 | |
| SANITIZER_LLVM_VERSION: 12 | |
| - name: "UBSan" | |
| env: | |
| SANITIZER_BUILD: undefined | |
| ENABLE_OPTIMIZED: 0 | |
| USE_TCMALLOC: 0 | |
| SANITIZER_LLVM_VERSION: 12 | |
| - name: "MSan" | |
| env: | |
| SANITIZER_BUILD: memory | |
| ENABLE_OPTIMIZED: 0 | |
| USE_TCMALLOC: 0 | |
| SOLVERS: STP | |
| SANITIZER_LLVM_VERSION: 14 | |
| # Test just using Z3 only | |
| - name: "Z3 only" | |
| env: | |
| SOLVERS: Z3 | |
| # Test just using metaSMT | |
| - name: "metaSMT" | |
| env: | |
| METASMT_VERSION: qf_abv | |
| SOLVERS: metaSMT | |
| METASMT_DEFAULT: STP | |
| REQUIRES_RTTI: 1 | |
| # Test we can build against STP master | |
| - name: "STP master" | |
| 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: | |
| UCLIBC_VERSION: klee_0_9_29 | |
| # Check at least one build with Asserts disabled. | |
| - name: "Asserts disabled" | |
| env: | |
| DISABLE_ASSERTIONS: 1 | |
| # Check without TCMALLOC and with an optimised runtime library | |
| - name: "No TCMalloc, optimised runtime" | |
| env: | |
| SOLVERS: STP | |
| USE_TCMALLOC: 0 | |
| KLEE_RUNTIME_BUILD: "Release+Debug+Asserts" | |
| steps: | |
| - name: Checkout KLEE source code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Memory layout fix for old clang | |
| run: | | |
| # TODO remove this once upstream fix is available | |
| sudo sysctl -w vm.mmap_rnd_bits=28 | |
| - name: Build KLEE | |
| env: ${{ matrix.env }} | |
| run: scripts/build/build.sh klee --docker --create-final-image | |
| - name: Run tests | |
| env: ${{ matrix.env }} | |
| run: scripts/build/run-tests.sh --run-docker --debug | |
| macOS: | |
| runs-on: macos-latest | |
| env: | |
| LLVM_VERSION: 14 | |
| BASE: /tmp | |
| SOLVERS: STP | |
| UCLIBC_VERSION: 0 | |
| USE_TCMALLOC: 0 | |
| USE_LIBCXX: 0 | |
| steps: | |
| - name: Install newer version of Bash | |
| run: brew install bash | |
| - name: Checkout KLEE source code | |
| uses: actions/checkout@v4 | |
| - name: Create virtualenv for Python3 (PEP 668) | |
| run: python3 -m venv .venv | |
| - name: Build KLEE | |
| run: source .venv/bin/activate && echo "$(which tabulate)" && scripts/build/build.sh klee --debug --install-system-deps | |
| - name: Run tests | |
| run: source .venv/bin/activate && scripts/build/run-tests.sh /tmp/klee_build* --debug | |
| Docker: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout KLEE Code | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Build Docker image | |
| run: docker build . | |
| Coverage: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| name: [ | |
| "STP", | |
| "Z3", | |
| "Bitwuzla", | |
| ] | |
| include: | |
| - name: "STP" | |
| env: | |
| SOLVERS: STP | |
| - name: "Z3" | |
| env: | |
| SOLVERS: Z3:STP | |
| - name: "Bitwuzla" | |
| env: | |
| SOLVERS: BITWUZLA:Z3 | |
| env: | |
| ENABLE_OPTIMIZED: 0 | |
| COVERAGE: 1 | |
| steps: | |
| - name: Checkout KLEE source code | |
| uses: actions/checkout@v3 | |
| with: | |
| # Codecov may run into "Issue detecting commit SHA. Please run | |
| # actions/checkout with fetch-depth > 1 or set to 0" when uploading. | |
| # See also https://github.com/codecov/codecov-action/issues/190 | |
| fetch-depth: 2 | |
| submodules: recursive | |
| - name: Build KLEE | |
| env: ${{ matrix.env }} | |
| run: scripts/build/build.sh klee --docker --create-final-image | |
| - 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: | |
| - uses: actions/checkout@v3 | |
| - uses: actions/setup-python@v4 | |
| with: | |
| python-version: 3.x | |
| - uses: pre-commit/[email protected] |