Skip to content

Enable Clang sanitizers in Linux/Clang CI pipeline #8737

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
tautschnig wants to merge 13 commits into
base: develop
Choose a base branch
from
+443 −102
Draft

Enable Clang sanitizers in Linux/Clang CI pipeline #8737

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
45233d2
Fix reference to temporary that has gone out of scope
tautschnig Mar 7, 2026
99642da
Initialise all POD members of goto_symex_statet
tautschnig Dec 1, 2025
f0da068
Do not use value-set supported simplification with multiple threads
tautschnig Nov 30, 2025
dde808b
Remove language_mode from goto_symext
tautschnig Dec 2, 2025
a1e32bc
Avoid invalid shift caused by excessive object bits
tautschnig Dec 2, 2025
d5a73cd
Avoid undefined shift in bv_pointers_wide
tautschnig Mar 7, 2026
92155e1
Initialise message_handler in bv_refinement unit test
tautschnig Mar 7, 2026
fd31137
Add missing quotes around TAGS variable in jbmc unit Makefile
tautschnig Mar 7, 2026
fc0c8a6
Exclude run() error reporting test under sanitizers
tautschnig Mar 7, 2026
c37ae63
Fix out-of-bounds read in MC/DC coverage eval_expr
tautschnig Mar 9, 2026
a0afc81
Enable Clang sanitizers in Linux CI pipeline
tautschnig Mar 7, 2026
a921f4f
Fix Clang Sanitizer CI regression test failures
tautschnig Mar 13, 2026
0e08fa6
Skip JBMC symex-driven-lazy-loading pass under sanitizers
tautschnig Mar 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
311 changes: 311 additions & 0 deletions .github/workflows/clang-sanitizer.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,311 @@
# Clang Sanitizer CI Pipeline
#
# Builds CBMC and JBMC with Clang's AddressSanitizer and
# UndefinedBehaviorSanitizer, then runs the full test suites to detect
# memory errors (buffer overflows, use-after-free, double-free) and
# undefined behavior (invalid shifts, signed integer overflow, etc.).
#
# Pipeline structure (build then parallel test):
#
# ┌── unit-tests (CBMC + JBMC unit tests)
# │
# build-asan ──────┼── cbmc-regression (main regression suite)
# │
# ├── cbmc-special-regression (paths-lifo, cprover-smt2)
# │
# ├── jbmc-regression (JBMC, no lazy loading)
# │
# └── jbmc-regression-symex-lazy-loading (subset)
#
# The build job compiles all binaries with sanitizer flags and uploads
# them as a tarball artifact. The four test jobs download the artifact
# and run their respective test suites in parallel.
#
# Sanitizer configuration:
# - AddressSanitizer: detects buffer overflows, use-after-free,
# use-after-return, double-free, stack-buffer-overflow
# - UndefinedBehaviorSanitizer: detects undefined behavior including
# invalid shifts, signed integer overflow, null pointer dereference
# - LeakSanitizer: disabled (detect_leaks=0) — too many reports to
# address at once
# - Compiled with -O1 for reasonable performance with sanitizers
# - -fno-sanitize-recover=all: abort on first error for clear diagnostics
#
# Unit test configuration:
# - Tests tagged [!shouldfail] (expected failures) are run separately
# - Tests tagged [not_ubsan] are excluded from the main sanitizer run
#
# Dependencies per job:
# - build-asan: clang, flex, bison, ccache
# - unit-tests: clang (runtime libs only), gdb, z3
# - cbmc-regression: clang, gdb, parallel, z3, cvc5, libxml2-utils
# - cbmc-special-regression: clang, gdb, z3, cvc5, libxml2-utils
# - jbmc-regression: clang, gdb, maven, jq, parallel

name: Clang Sanitizer
on:
push:
branches: [ develop ]
pull_request:
branches: [ develop ]
env:
cvc5-version: "1.2.1"
linux-vcpus: 4

jobs:
# Build all CBMC/JBMC binaries and unit test runners with sanitizers.
# Produces a tarball artifact consumed by the parallel test jobs below.
build-asan:
runs-on: ubuntu-24.04
env:
CC: "ccache /usr/bin/clang"
CXX: "ccache /usr/bin/clang++"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 flex bison ccache
make -C src minisat2-download
- name: Prepare ccache
uses: actions/cache@v4
with:
save-always: true
path: .ccache
key: ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: |
${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}
${{ runner.os }}-24.04-make-clang-asan
- name: ccache environment
run: |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Zero ccache stats and limit in size
run: ccache -z --max-size=500M
- name: Build with sanitizers
run: |
export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1"
make -C src -j${{env.linux-vcpus}} \
CXXFLAGS="$SANITIZER_FLAGS" \
LINKFLAGS="$SANITIZER_FLAGS" \
MINISAT2=../../minisat-2.2.1
make -C unit -j${{env.linux-vcpus}} \
CXXFLAGS="$SANITIZER_FLAGS" \
LINKFLAGS="$SANITIZER_FLAGS"
make -C jbmc/src -j${{env.linux-vcpus}} \
CXXFLAGS="$SANITIZER_FLAGS" \
LINKFLAGS="$SANITIZER_FLAGS" \
MINISAT2=../../minisat-2.2.1
make -C jbmc/unit -j${{env.linux-vcpus}} \
CXXFLAGS="$SANITIZER_FLAGS" \
LINKFLAGS="$SANITIZER_FLAGS"
- name: Print ccache stats
run: ccache -s
- name: Package build artifacts
run: |
tar czf build-artifacts.tar.gz \
--exclude='*.d' \
src/ unit/unit_tests jbmc/src/ jbmc/unit/unit_tests \
jbmc/lib/java-models-library/target/ \
minisat-2.2.1/
- name: Upload build artifacts
uses: actions/upload-artifact@v4
with:
name: asan-build
path: build-artifacts.tar.gz
retention-days: 1

# Run CBMC and JBMC unit tests (Catch2-based).
# Excludes [!shouldfail] and [not_ubsan] in the main run, then runs
# expected-failure tests separately.
unit-tests:
runs-on: ubuntu-24.04
needs: build-asan
env:
ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 flex bison gdb z3
- name: Download build artifacts
uses: actions/download-artifact@v4
with:
name: asan-build
- name: Extract build artifacts
run: tar xzf build-artifacts.tar.gz
- name: Run CBMC unit tests
run: |
cd unit
./unit_tests '-d yes' '~[!shouldfail]' '~[not_ubsan]'
echo "Running expected failure tests"
./unit_tests '-d yes' '[!shouldfail]'
- name: Run JBMC unit tests
run: |
cd jbmc/unit
./unit_tests '-d yes'
echo "Running expected failure tests"
./unit_tests '-d yes' '[!shouldfail]'

# Run the main CBMC regression test suite (all directories under regression/).
cbmc-regression:
runs-on: ubuntu-24.04
needs: build-asan
env:
ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb parallel flex bison libxml2-utils z3
- name: Confirm z3 solver is available and log the version installed
run: z3 --version
- name: Download cvc-5 from the releases page and make sure it can be deployed
run: |
wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
rm cvc5-Linux-x86_64-static.zip
cvc5 --version
- name: Download build artifacts
uses: actions/download-artifact@v4
with:
name: asan-build
- name: Extract build artifacts
run: tar xzf build-artifacts.tar.gz
- name: Run CBMC regression tests
env:
TESTPL_TIMEOUT: "1800"
run: |
export PATH=$PATH:$PWD/src/solvers
export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1"
make -C regression test-parallel JOBS=${{env.linux-vcpus}} \
CXXFLAGS="$SANITIZER_FLAGS" \
LINKFLAGS="$SANITIZER_FLAGS"

# Run CBMC's alternative-backend regression tests (paths-lifo, cprover-smt2).
cbmc-special-regression:
runs-on: ubuntu-24.04
needs: build-asan
env:
ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb flex bison libxml2-utils z3
- name: Confirm z3 solver is available and log the version installed
run: z3 --version
- name: Download cvc-5 from the releases page and make sure it can be deployed
run: |
wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
rm cvc5-Linux-x86_64-static.zip
cvc5 --version
- name: Download build artifacts
uses: actions/download-artifact@v4
with:
name: asan-build
- name: Extract build artifacts
run: tar xzf build-artifacts.tar.gz
- name: Run paths-lifo tests
run: |
export PATH=$PATH:$PWD/src/solvers
make -C regression/cbmc test-paths-lifo
- name: Run cprover-smt2 tests
run: |
export PATH=$PATH:$PWD/src/solvers
make -C regression/cbmc test-cprover-smt2

# Run the JBMC regression test suite (all directories under jbmc/regression/).
# The symex-driven-lazy-loading pass is skipped because it roughly doubles
# the runtime, pushing the job past GitHub's 6-hour timeout under sanitizers.
jbmc-regression:
runs-on: ubuntu-24.04
needs: build-asan
timeout-minutes: 360
env:
ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq parallel flex bison
- name: Download build artifacts
uses: actions/download-artifact@v4
with:
name: asan-build
- name: Extract build artifacts
run: tar xzf build-artifacts.tar.gz
- name: Run JBMC regression tests (without lazy loading)
env:
TESTPL_TIMEOUT: "1800"
run: make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} SKIP_SYMEX_DRIVEN_LAZY_LOADING=1

# Run the symex-driven-lazy-loading pass for a subset of JBMC directories.
# The full lazy-loading pass exceeds GitHub's 6-hour timeout under
# sanitizers, so we only run the smaller directories (jbmc-generics,
# book-examples, strings-smoke-tests) to still exercise that code path.
jbmc-regression-symex-lazy-loading:
runs-on: ubuntu-24.04
needs: build-asan
timeout-minutes: 360
env:
ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
steps:
- uses: actions/checkout@v6
with:
submodules: recursive
- name: Fetch dependencies
env:
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq parallel flex bison
- name: Download build artifacts
uses: actions/download-artifact@v4
with:
name: asan-build
- name: Extract build artifacts
run: tar xzf build-artifacts.tar.gz
- name: Run JBMC symex-driven-lazy-loading tests (subset)
env:
TESTPL_TIMEOUT: "1800"
run: |
cd jbmc/regression
mvn --quiet clean package -T1C
parallel \
--halt soon,fail=1 \
--tag --tagstring '{#}:' \
--linebuffer \
--jobs ${{env.linux-vcpus}} \
make -C "{}" test ONLY_SYMEX_DRIVEN_LAZY_LOADING=1 \
::: strings-smoke-tests jbmc-generics book-examples
8 changes: 8 additions & 0 deletions jbmc/regression/book-examples/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,28 @@ default: tests.log
include ../../src/config.inc

test:
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
else
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
endif
endif

tests.log: ../$(CPROVER_DIR)/regression/test.pl
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
else
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
endif
endif

show:
@for dir in *; do \
Expand Down
8 changes: 8 additions & 0 deletions jbmc/regression/jbmc-generics/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,20 @@ default: tests.log
include ../../src/config.inc

test:
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
endif

tests.log: ../$(CPROVER_DIR)/regression/test.pl
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
endif

show:
@for dir in *; do \
Expand Down
12 changes: 12 additions & 0 deletions jbmc/regression/jbmc-strings/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,32 @@ default: tests.log
include ../../src/config.inc

test:
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
endif

testfuture:
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
endif

testall:
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
endif

tests.log: ../$(CPROVER_DIR)/regression/test.pl
ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
endif
ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING
@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
endif

show:
@for dir in *; do \
Expand Down
Loading
Loading