z3/.github/workflows/memory-safety.yml

name: Memory Safety Analysis

on:
  schedule:
    - cron: '0 0 * * 1'
  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@v6.0.3

      - name: Setup Python
        uses: actions/setup-python@v6
        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@v7
        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@v6.0.3

      - name: Setup Python
        uses: actions/setup-python@v6
        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 -fsanitize-recover=all" \
            -DCMAKE_CXX_FLAGS="-fsanitize=undefined -fno-omit-frame-pointer -fsanitize-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@v7
        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@v8.0.1
        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