|
| 1 | +name: Clang Sanitizer |
| 2 | +on: |
| 3 | + push: |
| 4 | + branches: [ develop ] |
| 5 | + pull_request: |
| 6 | + branches: [ develop ] |
| 7 | +env: |
| 8 | + cvc5-version: "1.2.1" |
| 9 | + linux-vcpus: 4 |
| 10 | + |
| 11 | +jobs: |
| 12 | + # This job takes approximately X to Y minutes |
| 13 | + clang-asan-ubuntu-24_04-make: |
| 14 | + runs-on: ubuntu-24.04 |
| 15 | + env: |
| 16 | + CC: "ccache /usr/bin/clang" |
| 17 | + CXX: "ccache /usr/bin/clang++" |
| 18 | + # AddressSanitizer configuration for optimal CI performance |
| 19 | + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=1" |
| 20 | + # - `abort_on_error=1`: Terminate immediately on error |
| 21 | + # - `fast_unwind_on_malloc=0`: Use slower but more accurate stack unwinding |
| 22 | + # - `detect_odr_violation=0`: Disable One Definition Rule violation detection to reduce noise |
| 23 | + # - `detect_leaks=1`: Enable leak detection |
| 24 | + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" |
| 25 | + # - `print_stacktrace=1`: Show stack traces for undefined behavior |
| 26 | + # - `halt_on_error=1`: Terminate on undefined behavior |
| 27 | + steps: |
| 28 | + - uses: actions/checkout@v6 |
| 29 | + with: |
| 30 | + submodules: recursive |
| 31 | + - name: Fetch dependencies |
| 32 | + env: |
| 33 | + DEBIAN_FRONTEND: noninteractive |
| 34 | + run: | |
| 35 | + sudo apt-get update |
| 36 | + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils ccache z3 |
| 37 | + make -C src minisat2-download |
| 38 | + - name: Confirm z3 solver is available and log the version installed |
| 39 | + run: z3 --version |
| 40 | + - name: Download cvc-5 from the releases page and make sure it can be deployed |
| 41 | + run: | |
| 42 | + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip |
| 43 | + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 |
| 44 | + rm cvc5-Linux-x86_64-static.zip |
| 45 | + cvc5 --version |
| 46 | + - name: Prepare ccache |
| 47 | + uses: actions/cache@v4 |
| 48 | + with: |
| 49 | + save-always: true |
| 50 | + path: .ccache |
| 51 | + key: ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}-${{ github.sha }}-PR |
| 52 | + restore-keys: | |
| 53 | + ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }} |
| 54 | + ${{ runner.os }}-24.04-make-clang-asan |
| 55 | + - name: ccache environment |
| 56 | + run: | |
| 57 | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV |
| 58 | + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV |
| 59 | + - name: Zero ccache stats and limit in size |
| 60 | + run: ccache -z --max-size=500M |
| 61 | + - name: Build with AddressSanitizer and LeakSanitizer |
| 62 | + run: | |
| 63 | + # Build with sanitizers enabled - using -O1 for reasonable performance |
| 64 | + # -fsanitize=address: detects buffer overflows, use-after-free, etc. |
| 65 | + # -fsanitize=leak: detects memory leaks |
| 66 | + # -fsanitize=undefined: detects undefined behavior |
| 67 | + # -fno-sanitize-recover=all: abort on first error for faster feedback |
| 68 | + # -g: include debug symbols for better error reporting |
| 69 | + export SANITIZER_FLAGS="-fsanitize=address -fsanitize=leak -fsanitize=undefined -fno-sanitize-recover=all -g -O1" |
| 70 | + make -C src -j${{env.linux-vcpus}} \ |
| 71 | + CXXFLAGS="$SANITIZER_FLAGS" \ |
| 72 | + LINKFLAGS="$SANITIZER_FLAGS" \ |
| 73 | + MINISAT2=../../minisat-2.2.1 |
| 74 | + make -C unit -j${{env.linux-vcpus}} \ |
| 75 | + CXXFLAGS="$SANITIZER_FLAGS" \ |
| 76 | + LINKFLAGS="$SANITIZER_FLAGS" |
| 77 | + - name: Print ccache stats |
| 78 | + run: ccache -s |
| 79 | + - name: Run unit tests |
| 80 | + run: | |
| 81 | + make -C unit test |
| 82 | + make -C jbmc/unit test |
| 83 | + echo "Running expected failure tests" |
| 84 | + make TAGS="[!shouldfail]" -C unit test |
| 85 | + make TAGS="[!shouldfail]" -C jbmc/unit test |
| 86 | + - name: Run regression tests |
| 87 | + run: | |
| 88 | + export PATH=$PATH:`pwd`/src/solvers |
| 89 | + make -C regression test-parallel JOBS=${{env.linux-vcpus}} |
| 90 | + make -C regression/cbmc test-paths-lifo |
| 91 | + make -C regression/cbmc test-cprover-smt2 |
| 92 | + make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} |
0 commit comments