Enable Clang sanitizers in Linux/Clang CI pipeline#8737
Draft
tautschnig wants to merge 13 commits intodiffblue:developfrom
Draft
Enable Clang sanitizers in Linux/Clang CI pipeline#8737tautschnig wants to merge 13 commits intodiffblue:developfrom
tautschnig wants to merge 13 commits intodiffblue:developfrom
Conversation
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## develop #8737 +/- ##
========================================
Coverage 80.01% 80.01%
========================================
Files 1703 1703
Lines 188396 188386 -10
Branches 73 73
========================================
- Hits 150738 150731 -7
+ Misses 37658 37655 -3 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
address-sanitizer-ci
branch
from
869c8c6 to
65d8860
Compare
kroening
reviewed
Dec 1, 2025
tautschnig
force-pushed
the
address-sanitizer-ci
branch
2 times, most recently
from
34e4887 to
c71effb
Compare
tautschnig
force-pushed
the
address-sanitizer-ci
branch
8 times, most recently
from
b5055e6 to
ddbc14b
Compare
tautschnig
force-pushed
the
address-sanitizer-ci
branch
6 times, most recently
from
5832b87 to
320733b
Compare
Although the temporary is bound by a const reference, that reference is then just passed on to subobject initialisers. Per https://en.cppreference.com/w/cpp/language/reference_initialization.html#Lifetime_of_a_temporary, "passing on" does not extend the lifetime of a temporary. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The constructor did not take care of them and our unit tests exposed that, at least within unit tests, we were accessing uninitialised members.
Shared pointers may be updated in yet-to-be-executed threads.
`goto_symex_statet` holds a reference to a language mode, which was being initialised to `goto_symext::language_mode` in `goto_symext::initialize_entry_point_state`. That `goto_symext` object, however, may be the one created in `single_path_symex_only_checkert::initialize_worklist`, whereupon the `goto_symex_statet` will outlive it. Fix this problem by getting rid of the `language_mode` member of `goto_symext` and initialise `goto_symex_statet::language_mode` from a mode in the symbol table, which outlives all goto-symex objects.
Use mp_integer to compute the number of permitted objects as the number of object bits is related to the analysis target platform and need not be within the analysis-execution platform's limits.
Use mp_integer to compute the number of permitted objects as the number of object bits is related to the analysis target platform and need not be within the analysis-execution platform's limits. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The message_handler member of bv_refinementt::infot was left uninitialised, which is undefined behaviour when it is later dereferenced. Set it to null_message_handler. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Without quotes, TAGS values containing spaces are split into multiple arguments by the shell, causing incorrect test filtering. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The test invokes a non-existent binary, which does not terminate reliably when running under the address sanitizer. Tag it [not_ubsan] so that the sanitizer CI job can skip it. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The eval_expr function in cover_instrument_mcdc.cpp dereferences the result of std::map::find() without checking for end(). This happens when values_of_atomic_exprs skips inconsistent expressions (where signs.size() != 1), leaving them absent from the map. When eval_expr later encounters such an expression, find() returns end() and the dereference is undefined behavior (stack-buffer-overflow detected by AddressSanitizer). Fix by checking the iterator before dereferencing. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Adds a dedicated CI workflow that compiles with Clang's AddressSanitizer and UndefinedBehaviorSanitizer, then runs the full test suites. Leak detection is disabled for now as there are too many reports to address at once. The workflow is structured as a build job followed by four parallel test jobs: unit tests, CBMC regression, CBMC special regression (paths-lifo, cprover-smt2), and JBMC regression. Build artifacts are shared via a tarball upload. The unit test runner skips tests tagged [!shouldfail] and [not_ubsan] in the main run, then separately runs the expected-failure tests. - [AddressSanitizer](https://clang.llvm.org/docs/AddressSanitizer.html) - [UndefinedBehaviorSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) Fixes: diffblue#832 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
address-sanitizer-ci
branch
4 times, most recently
from
9fc9805 to
e9b5773
Compare
Three issues caused the regression-related sanitizer CI jobs to fail: 1. cbmc-regression: The build creates thin archives (ar rcT) that reference .o files by path. The artifact tarball excludes .o files to save space, breaking the thin archives. The regression/invariants and regression/libcprover-cpp tests link against these archives and fail. Fix: convert thin archives to regular archives before packaging. 2. cbmc-special-regression: The cprover-smt2 tests need the cprover-smt2-solver binary in PATH (from src/solvers/), but the job didn't set this up. All 497 of 1164 cprover-smt2 tests failed with VERIFICATION ERROR because the solver couldn't be found. Fix: add export PATH=$PATH:$PWD/src/solvers before running the tests, matching what pull-request-checks.yaml does. 3. jbmc-regression: The job timed out after 6 hours (GitHub Actions default). Sanitizer overhead on Java bytecode processing is extreme. Fix: add TESTPL_TIMEOUT=600 to kill individual tests that hang, and set an explicit timeout-minutes on the job. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
address-sanitizer-ci
branch
from
e9b5773 to
a921f4f
Compare
Under sanitizers, the JBMC regression suite takes over 6 hours because each test directory runs tests twice: once normally and once with --symex-driven-lazy-loading. Even the lazy-loading pass alone exceeds GitHub Actions' 6-hour timeout for the larger directories. Split into two jobs: - jbmc-regression: all directories, normal pass only (SKIP_SYMEX_DRIVEN_LAZY_LOADING=1) - jbmc-regression-symex-lazy-loading: lazy-loading pass for the smaller directories only (strings-smoke-tests, jbmc-generics, book-examples) to still exercise that code path under sanitizers. The large directories (jbmc, jbmc-strings) are skipped as they alone would exceed the 6-hour timeout. The JBMC regression Makefiles now support two variables: - SKIP_SYMEX_DRIVEN_LAZY_LOADING: skip the --symex-driven-lazy-loading pass - ONLY_SYMEX_DRIVEN_LAZY_LOADING: skip the normal pass (lazy loading only) When neither is set, behavior is unchanged (both passes run). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
address-sanitizer-ci
branch
from
daa4322 to
0e08fa6
Compare
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a dedicated CI job that runs unit and regression tests on Ubuntu 24.04 after compiling with Clang's sanitizers. Enables address sanitizer (buffer overflow, use-after-free, use-after-return, double-free), memory leak sanitizer, and undefined-behavior sanitizer (integer overflow).
Fixes: #832