mirror of
https://github.com/Z3Prover/z3
synced 2026-03-09 06:44:53 +00:00
Add ASan/UBSan memory safety CI workflow
Adds a workflow that builds and tests Z3 with AddressSanitizer and UndefinedBehaviorSanitizer on every push to catch runtime memory errors and undefined behavior. Runs unit tests, SMT-LIB2 benchmarks, and regression tests under both sanitizers. Includes a Copilot agentic workflow to generate summary reports as GitHub Discussions. Triggered on push (path-filtered to src/) and manual dispatch.
This commit is contained in:
Angelica Moreira
parent
d40c4721d8
commit
123bb620d4
2 changed files with 457 additions and 0 deletions
252
.github/workflows/memory-safety.yml
vendored
Normal file
252
.github/workflows/memory-safety.yml
vendored
Normal file
|
|
@ -0,0 +1,252 @@
|
|||
name: Memory Safety Analysis
|
||||
|
||||
on:
|
||||
push:
|
||||
branches: ["**"]
|
||||
paths:
|
||||
- 'src/**'
|
||||
- '.github/workflows/memory-safety.yml'
|
||||
workflow_dispatch:
|
||||
inputs:
|
||||
full_scan:
|
||||
description: 'Run full codebase scan (not just changed files)'
|
||||
required: false
|
||||
default: 'false'
|
||||
type: boolean
|
||||
|
||||
permissions:
|
||||
contents: read
|
||||
actions: read
|
||||
|
||||
concurrency:
|
||||
group: memory-safety-${{ github.ref }}
|
||||
cancel-in-progress: true
|
||||
|
||||
jobs:
|
||||
# ============================================================================
|
||||
# Job 1: AddressSanitizer Build and Tests
|
||||
# ============================================================================
|
||||
asan-test:
|
||||
name: "ASan Build & Test"
|
||||
runs-on: ubuntu-latest
|
||||
timeout-minutes: 120
|
||||
env:
|
||||
ASAN_OPTIONS: "detect_leaks=1:halt_on_error=0:print_stats=1:log_path=/tmp/asan"
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
uses: actions/checkout@v4
|
||||
|
||||
- name: Setup Python
|
||||
uses: actions/setup-python@v5
|
||||
with:
|
||||
python-version: '3.x'
|
||||
|
||||
- name: Install dependencies
|
||||
run: sudo apt-get update && sudo apt-get install -y ninja-build clang
|
||||
|
||||
- name: Configure with ASan
|
||||
run: |
|
||||
mkdir -p build-asan
|
||||
cd build-asan
|
||||
CC=clang CXX=clang++ cmake \
|
||||
-DCMAKE_BUILD_TYPE=Debug \
|
||||
-DCMAKE_C_FLAGS="-fsanitize=address -fno-omit-frame-pointer -fno-optimize-sibling-calls" \
|
||||
-DCMAKE_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer -fno-optimize-sibling-calls" \
|
||||
-DCMAKE_EXE_LINKER_FLAGS="-fsanitize=address" \
|
||||
-DCMAKE_SHARED_LINKER_FLAGS="-fsanitize=address" \
|
||||
-G Ninja ../
|
||||
|
||||
- name: Build Z3 with ASan
|
||||
run: |
|
||||
cd build-asan
|
||||
ninja -j$(nproc)
|
||||
ninja test-z3
|
||||
|
||||
- name: Run unit tests under ASan
|
||||
run: |
|
||||
cd build-asan
|
||||
./test-z3 -a 2>&1 | tee /tmp/asan-unit-test.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Run SMT-LIB2 benchmarks under ASan
|
||||
run: |
|
||||
cd build-asan
|
||||
for f in ../examples/SMT-LIB2/bounded\ model\ checking/*.smt2; do
|
||||
echo "=== Testing: $f ==="
|
||||
timeout 60 ./z3 "$f" 2>&1 || true
|
||||
done | tee /tmp/asan-benchmark.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Run regression tests under ASan
|
||||
run: |
|
||||
git clone --depth=1 https://github.com/z3prover/z3test z3test
|
||||
python z3test/scripts/test_benchmarks.py build-asan/z3 z3test/regressions/smt2 2>&1 | tee /tmp/asan-regression.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Collect ASan reports
|
||||
if: always()
|
||||
run: |
|
||||
mkdir -p /tmp/asan-reports
|
||||
cp /tmp/asan* /tmp/asan-reports/ 2>/dev/null || true
|
||||
if ls /tmp/asan.* 1>/dev/null 2>&1; then
|
||||
cp /tmp/asan.* /tmp/asan-reports/
|
||||
fi
|
||||
echo "# ASan Summary" > /tmp/asan-reports/summary.md
|
||||
echo "" >> /tmp/asan-reports/summary.md
|
||||
if ls /tmp/asan-reports/asan.* 1>/dev/null 2>&1; then
|
||||
echo "## Errors Found" >> /tmp/asan-reports/summary.md
|
||||
for f in /tmp/asan-reports/asan.*; do
|
||||
echo '```' >> /tmp/asan-reports/summary.md
|
||||
head -50 "$f" >> /tmp/asan-reports/summary.md
|
||||
echo '```' >> /tmp/asan-reports/summary.md
|
||||
echo "" >> /tmp/asan-reports/summary.md
|
||||
done
|
||||
else
|
||||
echo "No ASan errors detected." >> /tmp/asan-reports/summary.md
|
||||
fi
|
||||
|
||||
- name: Upload ASan reports
|
||||
if: always()
|
||||
uses: actions/upload-artifact@v4
|
||||
with:
|
||||
name: asan-reports
|
||||
path: /tmp/asan-reports/
|
||||
retention-days: 30
|
||||
|
||||
# ============================================================================
|
||||
# Job 2: UndefinedBehaviorSanitizer Build and Tests
|
||||
# ============================================================================
|
||||
ubsan-test:
|
||||
name: "UBSan Build & Test"
|
||||
runs-on: ubuntu-latest
|
||||
timeout-minutes: 120
|
||||
env:
|
||||
UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=0:log_path=/tmp/ubsan"
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
uses: actions/checkout@v4
|
||||
|
||||
- name: Setup Python
|
||||
uses: actions/setup-python@v5
|
||||
with:
|
||||
python-version: '3.x'
|
||||
|
||||
- name: Install dependencies
|
||||
run: sudo apt-get update && sudo apt-get install -y ninja-build clang
|
||||
|
||||
- name: Configure with UBSan
|
||||
run: |
|
||||
mkdir -p build-ubsan
|
||||
cd build-ubsan
|
||||
CC=clang CXX=clang++ cmake \
|
||||
-DCMAKE_BUILD_TYPE=Debug \
|
||||
-DCMAKE_C_FLAGS="-fsanitize=undefined -fno-omit-frame-pointer -fno-sanitize-recover=all" \
|
||||
-DCMAKE_CXX_FLAGS="-fsanitize=undefined -fno-omit-frame-pointer -fno-sanitize-recover=all" \
|
||||
-DCMAKE_EXE_LINKER_FLAGS="-fsanitize=undefined" \
|
||||
-DCMAKE_SHARED_LINKER_FLAGS="-fsanitize=undefined" \
|
||||
-G Ninja ../
|
||||
|
||||
- name: Build Z3 with UBSan
|
||||
run: |
|
||||
cd build-ubsan
|
||||
ninja -j$(nproc)
|
||||
ninja test-z3
|
||||
|
||||
- name: Run unit tests under UBSan
|
||||
run: |
|
||||
cd build-ubsan
|
||||
./test-z3 -a 2>&1 | tee /tmp/ubsan-unit-test.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Run SMT-LIB2 benchmarks under UBSan
|
||||
run: |
|
||||
cd build-ubsan
|
||||
for f in ../examples/SMT-LIB2/bounded\ model\ checking/*.smt2; do
|
||||
echo "=== Testing: $f ==="
|
||||
timeout 60 ./z3 "$f" 2>&1 || true
|
||||
done | tee /tmp/ubsan-benchmark.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Run regression tests under UBSan
|
||||
run: |
|
||||
git clone --depth=1 https://github.com/z3prover/z3test z3test
|
||||
python z3test/scripts/test_benchmarks.py build-ubsan/z3 z3test/regressions/smt2 2>&1 | tee /tmp/ubsan-regression.log
|
||||
continue-on-error: true
|
||||
|
||||
- name: Collect UBSan reports
|
||||
if: always()
|
||||
run: |
|
||||
mkdir -p /tmp/ubsan-reports
|
||||
cp /tmp/ubsan* /tmp/ubsan-reports/ 2>/dev/null || true
|
||||
if ls /tmp/ubsan.* 1>/dev/null 2>&1; then
|
||||
cp /tmp/ubsan.* /tmp/ubsan-reports/
|
||||
fi
|
||||
echo "# UBSan Summary" > /tmp/ubsan-reports/summary.md
|
||||
echo "" >> /tmp/ubsan-reports/summary.md
|
||||
if ls /tmp/ubsan-reports/ubsan.* 1>/dev/null 2>&1; then
|
||||
echo "## Errors Found" >> /tmp/ubsan-reports/summary.md
|
||||
for f in /tmp/ubsan-reports/ubsan.*; do
|
||||
echo '```' >> /tmp/ubsan-reports/summary.md
|
||||
head -50 "$f" >> /tmp/ubsan-reports/summary.md
|
||||
echo '```' >> /tmp/ubsan-reports/summary.md
|
||||
echo "" >> /tmp/ubsan-reports/summary.md
|
||||
done
|
||||
else
|
||||
echo "No UBSan errors detected." >> /tmp/ubsan-reports/summary.md
|
||||
fi
|
||||
|
||||
- name: Upload UBSan reports
|
||||
if: always()
|
||||
uses: actions/upload-artifact@v4
|
||||
with:
|
||||
name: ubsan-reports
|
||||
path: /tmp/ubsan-reports/
|
||||
retention-days: 30
|
||||
|
||||
# ============================================================================
|
||||
# Job 3: Summary Report
|
||||
# ============================================================================
|
||||
summary:
|
||||
name: "Memory Safety Summary"
|
||||
runs-on: ubuntu-latest
|
||||
needs: [asan-test, ubsan-test]
|
||||
if: always()
|
||||
steps:
|
||||
- name: Download all artifacts
|
||||
uses: actions/download-artifact@v4
|
||||
with:
|
||||
path: reports/
|
||||
|
||||
- name: Generate summary
|
||||
run: |
|
||||
echo "# Memory Safety Analysis Report" >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
echo "**Commit**: \`${{ github.sha }}\`" >> $GITHUB_STEP_SUMMARY
|
||||
echo "**Branch**: \`${{ github.ref_name }}\`" >> $GITHUB_STEP_SUMMARY
|
||||
echo "**Trigger**: \`${{ github.event_name }}\`" >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
|
||||
echo "## Job Results" >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
echo "| Analysis | Status |" >> $GITHUB_STEP_SUMMARY
|
||||
echo "|----------|--------|" >> $GITHUB_STEP_SUMMARY
|
||||
echo "| AddressSanitizer | \`${{ needs.asan-test.result }}\` |" >> $GITHUB_STEP_SUMMARY
|
||||
echo "| UndefinedBehaviorSanitizer | \`${{ needs.ubsan-test.result }}\` |" >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
|
||||
if [ -f reports/asan-reports/summary.md ]; then
|
||||
echo "## ASan Results" >> $GITHUB_STEP_SUMMARY
|
||||
cat reports/asan-reports/summary.md >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
fi
|
||||
|
||||
if [ -f reports/ubsan-reports/summary.md ]; then
|
||||
echo "## UBSan Results" >> $GITHUB_STEP_SUMMARY
|
||||
cat reports/ubsan-reports/summary.md >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
fi
|
||||
|
||||
echo "## Artifacts" >> $GITHUB_STEP_SUMMARY
|
||||
echo "" >> $GITHUB_STEP_SUMMARY
|
||||
echo "- Sanitizer logs are available as workflow artifacts" >> $GITHUB_STEP_SUMMARY
|
||||
echo "- Run with \`workflow_dispatch\` and \`full_scan: true\` for complete codebase analysis" >> $GITHUB_STEP_SUMMARY
|
||||
Loading…
Add table
Add a link
Reference in a new issue