Add profiling tool and run in CI

.github/workflows/profiling.yaml

@@ -0,0 +1,283 @@
+# CBMC Profiling Workflow
+#
+# Two modes:
+#
+# 1. On PRs: builds both the base branch and the PR branch, profiles each,
+#    and posts a differential comparison plus the PR's hotspot analysis to
+#    the GitHub step summary.  Flamegraph SVGs are uploaded as artifacts.
+#
+# 2. On pushes to develop: profiles the current develop tip and publishes
+#    the flamegraphs to GitHub Pages at /profiling/ so they are always
+#    available at https://diffblue.github.io/cbmc/profiling/
+#
+# The benchmarks exercise different CBMC subsystems:
+#   - linked_list: pointer analysis + symbolic execution
+#   - array_ops:   array flattening + propositional encoding
+#   - structs:     type checking + goto conversion
+#
+# Solver time is excluded (--dimacs --outfile /dev/null) so that results
+# reflect only CBMC's own code, not the SAT solver.
+#
+# To run locally:
+#   scripts/profile_cbmc.py --auto --runs 3
+
+name: Profiling
+on:
+  pull_request:
+    branches: [ develop ]
+  push:
+    branches: [ develop ]
+
+jobs:
+  # ── PR job: differential profiling (base vs PR) ──────────────────────
+  profile-pr:
+    if: github.event_name == 'pull_request'
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v6
+        with:
+          submodules: recursive
+          fetch-depth: 0
+
+      - name: Install dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq \
+            cmake ninja-build gcc g++ flex bison ccache libgoogle-perftools-dev \
+            linux-tools-common linux-tools-generic
+          PERF_REAL=$(find /usr/lib/linux-tools-*/perf -maxdepth 0 2>/dev/null | head -1)
+          if [ -z "$PERF_REAL" ]; then
+            echo "::error::No perf binary found under /usr/lib/linux-tools-*"
+            exit 1
+          fi
+          echo "$(dirname "$PERF_REAL")" >> "$GITHUB_PATH"
+          "$PERF_REAL" --version
+          sudo sysctl kernel.perf_event_paranoid=-1
+
+      - name: Restore ccache
+        uses: actions/cache/restore@v5
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-24.04-Release-profile
+            ${{ runner.os }}-24.04-Release
+      - run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+
+      # Build the base branch first in a worktree.  Building base before
+      # the PR branch means the PR build gets good ccache hit rates (most
+      # object files are shared).
+      - name: Build and profile base branch
+        run: |
+          BASE_SHA="${{ github.event.pull_request.base.sha }}"
+          git worktree add --detach ../base-worktree "$BASE_SHA"
+          (cd ../base-worktree && git submodule update --init)
+          cmake -S ../base-worktree -B../base-worktree/build -G Ninja \
+            -DWITH_JBMC=OFF -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_C_COMPILER=/usr/bin/gcc \
+            -DCMAKE_CXX_COMPILER=/usr/bin/g++
+          touch ../base-worktree/build/src/{ansi-c,cpp}/library-check.stamp
+          ninja -C ../base-worktree/build cbmc -j$(nproc)
+          python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
+            --build-dir ../base-worktree/build --output-dir base-results
+
+      - name: Build PR branch (Release)
+        run: |
+          cmake -S . -Bbuild -G Ninja -DWITH_JBMC=OFF \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_C_COMPILER=/usr/bin/gcc \
+            -DCMAKE_CXX_COMPILER=/usr/bin/g++
+          touch build/src/{ansi-c,cpp}/library-check.stamp
+          ninja -C build cbmc -j$(nproc)
+
+      - name: Profile PR branch (3 runs per benchmark)
+        run: |
+          python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
+            --output-dir profile-results
+
+      - name: Generate differential summary
+        if: always()
+        run: |
+          if [ -f base-results/results.json ] && [ -f profile-results/results.json ]; then
+            python3 scripts/profile_cbmc.py \
+              --compare base-results profile-results \
+              --compare-labels \
+                "${{ github.event.pull_request.base.ref }}" \
+                "${{ github.event.pull_request.head.ref }}" \
+              --output-dir diff-results
+          fi
+
+      - name: Post summary
+        if: always()
+        run: |
+          if [ -f diff-results/diff_summary.txt ]; then
+            echo '### Differential Profile (base → PR)' >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+            cat diff-results/diff_summary.txt >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+            echo '' >> "$GITHUB_STEP_SUMMARY"
+          fi
+          if [ -f profile-results/summary.txt ]; then
+            echo '### PR Branch Profile' >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+            cat profile-results/summary.txt >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+          fi
+          RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
+          echo '' >> "$GITHUB_STEP_SUMMARY"
+          echo '---' >> "$GITHUB_STEP_SUMMARY"
+          echo "📊 **[Download flamegraph SVGs](${RUN_URL}#artifacts)** — open in a browser for interactive exploration." >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          echo "🔥 **[Latest develop flamegraphs](https://diffblue.github.io/cbmc/profiling/)**" >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Clean up worktree
+        if: always()
+        run: git worktree remove --force ../base-worktree 2>/dev/null || true
+
+      - name: Upload artifacts
+        if: always()
+        uses: actions/upload-artifact@v7
+        with:
+          name: profile-results
+          path: |
+            profile-results/**/flamegraph.svg
+            profile-results/aggregated.svg
+            profile-results/summary.txt
+            profile-results/results.json
+            base-results/results.json
+            diff-results/diff_summary.txt
+          retention-days: 14
+
+      - name: Save ccache
+        if: always()
+        uses: actions/cache/save@v5
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
+
+  # ── Develop job: profile and publish flamegraphs to GitHub Pages ─────
+  profile-develop:
+    if: github.event_name == 'push'
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v6
+        with:
+          submodules: recursive
+
+      - name: Install dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq \
+            cmake ninja-build gcc g++ flex bison ccache libgoogle-perftools-dev \
+            linux-tools-common linux-tools-generic
+          PERF_REAL=$(find /usr/lib/linux-tools-*/perf -maxdepth 0 2>/dev/null | head -1)
+          if [ -z "$PERF_REAL" ]; then
+            echo "::error::No perf binary found under /usr/lib/linux-tools-*"
+            exit 1
+          fi
+          echo "$(dirname "$PERF_REAL")" >> "$GITHUB_PATH"
+          "$PERF_REAL" --version
+          sudo sysctl kernel.perf_event_paranoid=-1
+
+      - name: Restore ccache
+        uses: actions/cache/restore@v5
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-24.04-Release-profile
+            ${{ runner.os }}-24.04-Release
+      - run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+
+      - name: Build CBMC (Release)
+        run: |
+          cmake -S . -Bbuild -G Ninja -DWITH_JBMC=OFF \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_C_COMPILER=/usr/bin/gcc \
+            -DCMAKE_CXX_COMPILER=/usr/bin/g++
+          touch build/src/{ansi-c,cpp}/library-check.stamp
+          ninja -C build cbmc -j$(nproc)
+
+      - name: Profile develop (3 runs per benchmark)
+        run: |
+          python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
+            --output-dir profile-results
+
+      - name: Post summary
+        if: always()
+        run: |
+          if [ -f profile-results/summary.txt ]; then
+            echo '### develop Profile' >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+            cat profile-results/summary.txt >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+            echo '' >> "$GITHUB_STEP_SUMMARY"
+            echo '---' >> "$GITHUB_STEP_SUMMARY"
+            echo '🔥 **[Interactive flamegraphs on GitHub Pages](https://diffblue.github.io/cbmc/profiling/)**' >> "$GITHUB_STEP_SUMMARY"
+          fi
+
+      - name: Prepare pages content
+        if: always()
+        run: |
+          mkdir -p pages-out
+          # Copy all flamegraph SVGs
+          find profile-results -name 'flamegraph.svg' | while read f; do
+            bench=$(basename "$(dirname "$f")")
+            cp "$f" "pages-out/${bench}.svg"
+          done
+          [ -f profile-results/aggregated.svg ] && cp profile-results/aggregated.svg pages-out/
+          [ -f profile-results/summary.txt ] && cp profile-results/summary.txt pages-out/
+          [ -f profile-results/results.json ] && cp profile-results/results.json pages-out/
+          # Generate a simple index page
+          SHORT_SHA=$(echo "${{ github.sha }}" | cut -c1-8)
+          cat > pages-out/index.html <<'HEADER'
+          <!DOCTYPE html>
+          <html><head><meta charset="utf-8">
+          <title>CBMC Profiling — develop</title>
+          <style>
+            body { font-family: system-ui, sans-serif; max-width: 900px; margin: 2em auto; padding: 0 1em; }
+            h1 { border-bottom: 2px solid #333; padding-bottom: 0.3em; }
+            a { color: #0366d6; }
+            .meta { color: #666; font-size: 0.9em; }
+            ul { line-height: 1.8; }
+            pre { background: #f6f8fa; padding: 1em; overflow-x: auto; font-size: 0.85em; }
+          </style>
+          </head><body>
+          HEADER
+          echo "<h1>CBMC Profiling — develop</h1>" >> pages-out/index.html
+          echo "<p class='meta'>Commit: <code>${SHORT_SHA}</code> — $(date -u '+%Y-%m-%d %H:%M UTC')</p>" >> pages-out/index.html
+          echo "<h2>Flamegraphs</h2><p>Click to open interactive SVG (searchable, zoomable):</p><ul>" >> pages-out/index.html
+          for svg in pages-out/*.svg; do
+            name=$(basename "$svg")
+            echo "<li><a href=\"${name}\">${name%.svg}</a></li>" >> pages-out/index.html
+          done
+          echo "</ul>" >> pages-out/index.html
+          if [ -f pages-out/summary.txt ]; then
+            echo "<h2>Summary</h2><pre>" >> pages-out/index.html
+            cat pages-out/summary.txt >> pages-out/index.html
+            echo "</pre>" >> pages-out/index.html
+          fi
+          echo "<p><a href=\"https://github.com/${{ github.repository }}\">← Back to repository</a></p>" >> pages-out/index.html
+          echo "</body></html>" >> pages-out/index.html
+
+      - name: Publish to GitHub Pages
+        if: always()
+        uses: JamesIves/github-pages-deploy-action@v4
+        with:
+          branch: gh-pages
+          folder: pages-out
+          target-folder: profiling
+          clean: true
+
+      - name: Save ccache
+        if: always()
+        uses: actions/cache/save@v5
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}

AGENTS.md

@@ -69,6 +69,7 @@ cbmc/
 │   │   ├── syntax-checks.yaml           # Code style and linting
 │   │   ├── codeql-analysis.yml          # Security analysis
 │   │   ├── performance.yaml             # Performance benchmarking
+│   │   ├── profiling.yaml               # Pre-solver profiling on PRs
 │   │   └── release-packages.yaml        # Release automation
 │   └── dependabot.yml      # Dependency update automation
 ├── CODING_STANDARD.md      # Coding conventions
@@ -214,6 +215,8 @@ Unit tests using the Catch framework:
 
 - Build helpers and utilities
 - `cpplint.py` - Style checker
+- `profile_cbmc.py` - Performance profiling tool (see [Profiling CBMC](#6-profiling-cbmc))
+- `profiling/` - Profiling package (analysis, benchmarks, runner, utils)
 - `test.pl` - Regression test runner (in `regression/`)
 - CI/CD related scripts
 
@@ -764,6 +767,46 @@ cd regression/cbmc
 make test
 ```
 
+### 6. Profiling CBMC
+
+The profiling tool (`scripts/profile_cbmc.py`) profiles CBMC's pre-solver
+stages using `perf` and generates flamegraphs. Solver time is excluded by
+default so results reflect only CBMC's own code.
+
+**Prerequisites:** Linux with `perf` installed.
+
+```bash
+# Profile a single file
+scripts/profile_cbmc.py test.c -- --bounds-check --unwind 100
+
+# Run 3 built-in benchmarks (linked_list, array_ops, structs)
+scripts/profile_cbmc.py --auto
+
+# Extended suite (10 benchmarks) plus CSmith-generated tests
+scripts/profile_cbmc.py --auto-large --auto-csmith
+
+# Multiple runs for statistical significance (reports mean ± stddev)
+scripts/profile_cbmc.py --auto --runs 3
+
+# Source-level call site resolution (build a debug binary first)
+cmake -S . -Bbuild-debug -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF
+cmake --build build-debug --target cbmc -j$(nproc)
+scripts/profile_cbmc.py --auto --debug-binary build-debug/bin/cbmc
+
+# Differential profiling: compare two git refs
+scripts/profile_cbmc.py --diff develop my-optimization-branch
+```
+
+**Outputs** (in `profile-results/` by default):
+- `flamegraph.svg` per benchmark - Interactive flamegraph
+- `aggregated.svg` - Combined flamegraph across all benchmarks
+- `summary.txt` - Text summary with hotspot analysis and optimization suggestions
+- `results.json` - Machine-readable results
+
+**CI integration:** The `profiling.yaml` workflow runs `--auto --runs 3` on
+every PR, posts the summary to the GitHub step summary, and uploads
+flamegraph SVGs as downloadable artifacts.
+
 ---
 
 ## Navigation Tips
@@ -894,6 +937,7 @@ To understand how data flows through CBMC:
 | Create GOTO binary | `goto-cc -o out.gb input.c` |
 | View GOTO program | `goto-instrument --show-goto-functions prog.gb` |
 | Run CBMC | `cbmc program.gb` or `cbmc program.c` |
+| Profile CBMC | `scripts/profile_cbmc.py --auto --runs 3` |
 
 ### Key Files to Know
 

doc/architectural/compilation-and-development.md

@@ -281,6 +281,42 @@ There are also instructions for adding this as a git pre-commit hook in
 
 \section compilation-and-development-section-time-profiling Time profiling
 
+\subsection compilation-and-development-subsection-perf-profiling Profiling with perf (recommended)
+
+The script `scripts/profile_cbmc.py` profiles CBMC's pre-solver stages using
+`perf` and generates interactive flamegraphs. Solver time is excluded by default
+so that results reflect only CBMC's own code. This requires Linux with `perf`
+installed.
+
+Quick start with built-in benchmarks:
+
+    scripts/profile_cbmc.py --auto
+
+For multiple runs (reports mean ± stddev):
+
+    scripts/profile_cbmc.py --auto --runs 3
+
+To profile a specific input file:
+
+    scripts/profile_cbmc.py test.c -- --bounds-check --unwind 100
+
+For source-level call site resolution, build a separate debug binary and pass it
+via `--debug-binary` (profiling still uses the fast Release build):
+
+    cmake -S . -Bbuild-debug -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF
+    cmake --build build-debug --target cbmc -j$(nproc)
+    scripts/profile_cbmc.py --auto --debug-binary build-debug/bin/cbmc
+
+To compare performance between two git refs:
+
+    scripts/profile_cbmc.py --diff develop my-optimization-branch
+
+Results are written to `profile-results/` by default and include flamegraph SVGs,
+a text summary with hotspot analysis, and machine-readable JSON. Run
+`scripts/profile_cbmc.py --help` for the full set of options.
+
+\subsection compilation-and-development-subsection-gprof-profiling Profiling with gprof
+
 To do time profiling with a tool like `gprof`, the flags `-g` (build with debug
 symbols) and `-pg` (enable profiling information) must be
 used when compiling, and `-pg` must be used when linking. If you are building