Approximation of tree incrementality for Z3 solver #743
Workflow file for this run
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] | |
| # Defaults for building KLEE | |
| env: | |
| BASE_IMAGE: ubuntu:jammy-20230126 | |
| REPOSITORY: ghcr.io/klee | |
| COVERAGE: 0 | |
| DISABLE_ASSERTIONS: 0 | |
| ENABLE_DOXYGEN: 0 | |
| ENABLE_OPTIMIZED: 1 | |
| ENABLE_DEBUG: 1 | |
| GTEST_VERSION: 1.11.0 | |
| KLEE_RUNTIME_BUILD: "Debug+Asserts" | |
| LLVM_VERSION: 11 | |
| MINISAT_VERSION: "master" | |
| REQUIRES_RTTI: 0 | |
| SOLVERS: 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 | |
| jobs: | |
| Linux: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| name: [ | |
| "LLVM 14", | |
| "LLVM 13", | |
| "LLVM 12", | |
| "LLVM 11, Doxygen", | |
| "LLVM 10", | |
| "LLVM 9", | |
| "ASan", | |
| "UBSan", | |
| "MSan", | |
| "Z3 only", | |
| "metaSMT", | |
| "STP master", | |
| "Latest klee-uclibc", | |
| "Asserts disabled", | |
| "No TCMalloc, optimised runtime", | |
| ] | |
| include: | |
| - 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 | |
| - name: "LLVM 10" | |
| env: | |
| LLVM_VERSION: 10 | |
| - name: "LLVM 9" | |
| env: | |
| LLVM_VERSION: 9 | |
| # 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 | |
| # 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: 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: | |
| 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@v3 | |
| with: | |
| submodules: recursive | |
| - name: Build KLEE | |
| run: scripts/build/build.sh klee --debug --install-system-deps | |
| - name: Run tests | |
| run: 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", | |
| ] | |
| include: | |
| - name: "STP" | |
| env: | |
| SOLVERS: STP | |
| - name: "Z3" | |
| env: | |
| SOLVERS: Z3:STP | |
| 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: | |
| - 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)$' |