Skip to content

[fix]

[fix] #76

Workflow file for this run

---
name: CI
on:
pull_request:
branches: [ci]
push:
branches: [ci]
# 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: 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.2.0
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",
"Bitwuzla only",
"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
# 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: 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",
"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:
- 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)$'