Skip to content

Commit 0170409

Browse files
tautschnigtautschnig
authored
Merge pull request #8859 from tautschnig/profiling-tool
Add profiling tool and run in CI
2 parents 59d2211 + 70825b7 commit 0170409

9 files changed

Lines changed: 1968 additions & 0 deletions

File tree

‎.github/workflows/profiling.yaml‎

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
# CBMC Profiling Workflow
2+
#
3+
# Two modes:
4+
#
5+
# 1. On PRs: builds both the base branch and the PR branch, profiles each,
6+
# and posts a differential comparison plus the PR's hotspot analysis to
7+
# the GitHub step summary. Flamegraph SVGs are uploaded as artifacts.
8+
#
9+
# 2. On pushes to develop: profiles the current develop tip and publishes
10+
# the flamegraphs to GitHub Pages at /profiling/ so they are always
11+
# available at https://diffblue.github.io/cbmc/profiling/
12+
#
13+
# The benchmarks exercise different CBMC subsystems:
14+
# - linked_list: pointer analysis + symbolic execution
15+
# - array_ops: array flattening + propositional encoding
16+
# - structs: type checking + goto conversion
17+
#
18+
# Solver time is excluded (--dimacs --outfile /dev/null) so that results
19+
# reflect only CBMC's own code, not the SAT solver.
20+
#
21+
# To run locally:
22+
# scripts/profile_cbmc.py --auto --runs 3
23+
24+
name: Profiling
25+
on:
26+
pull_request:
27+
branches: [ develop ]
28+
push:
29+
branches: [ develop ]
30+
31+
jobs:
32+
# ── PR job: differential profiling (base vs PR) ──────────────────────
33+
profile-pr:
34+
if: github.event_name == 'pull_request'
35+
runs-on: ubuntu-24.04
36+
steps:
37+
- name: Check out repository
38+
uses: actions/checkout@v6
39+
with:
40+
submodules: recursive
41+
fetch-depth: 0
42+
43+
- name: Install dependencies
44+
env:
45+
DEBIAN_FRONTEND: noninteractive
46+
run: |
47+
sudo apt-get update
48+
sudo apt-get install --no-install-recommends -yq \
49+
cmake ninja-build gcc g++ flex bison ccache libgoogle-perftools-dev \
50+
linux-tools-common linux-tools-generic
51+
PERF_REAL=$(find /usr/lib/linux-tools-*/perf -maxdepth 0 2>/dev/null | head -1)
52+
if [ -z "$PERF_REAL" ]; then
53+
echo "::error::No perf binary found under /usr/lib/linux-tools-*"
54+
exit 1
55+
fi
56+
echo "$(dirname "$PERF_REAL")" >> "$GITHUB_PATH"
57+
"$PERF_REAL" --version
58+
sudo sysctl kernel.perf_event_paranoid=-1
59+
60+
- name: Restore ccache
61+
uses: actions/cache/restore@v5
62+
with:
63+
path: .ccache
64+
key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
65+
restore-keys: |
66+
${{ runner.os }}-24.04-Release-profile
67+
${{ runner.os }}-24.04-Release
68+
- run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
69+
70+
# Build the base branch first in a worktree. Building base before
71+
# the PR branch means the PR build gets good ccache hit rates (most
72+
# object files are shared).
73+
- name: Build and profile base branch
74+
run: |
75+
BASE_SHA="${{ github.event.pull_request.base.sha }}"
76+
git worktree add --detach ../base-worktree "$BASE_SHA"
77+
(cd ../base-worktree && git submodule update --init)
78+
cmake -S ../base-worktree -B../base-worktree/build -G Ninja \
79+
-DWITH_JBMC=OFF -DCMAKE_BUILD_TYPE=Release \
80+
-DCMAKE_C_COMPILER=/usr/bin/gcc \
81+
-DCMAKE_CXX_COMPILER=/usr/bin/g++
82+
touch ../base-worktree/build/src/{ansi-c,cpp}/library-check.stamp
83+
ninja -C ../base-worktree/build cbmc -j$(nproc)
84+
python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
85+
--build-dir ../base-worktree/build --output-dir base-results
86+
87+
- name: Build PR branch (Release)
88+
run: |
89+
cmake -S . -Bbuild -G Ninja -DWITH_JBMC=OFF \
90+
-DCMAKE_BUILD_TYPE=Release \
91+
-DCMAKE_C_COMPILER=/usr/bin/gcc \
92+
-DCMAKE_CXX_COMPILER=/usr/bin/g++
93+
touch build/src/{ansi-c,cpp}/library-check.stamp
94+
ninja -C build cbmc -j$(nproc)
95+
96+
- name: Profile PR branch (3 runs per benchmark)
97+
run: |
98+
python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
99+
--output-dir profile-results
100+
101+
- name: Generate differential summary
102+
if: always()
103+
run: |
104+
if [ -f base-results/results.json ] && [ -f profile-results/results.json ]; then
105+
python3 scripts/profile_cbmc.py \
106+
--compare base-results profile-results \
107+
--compare-labels \
108+
"${{ github.event.pull_request.base.ref }}" \
109+
"${{ github.event.pull_request.head.ref }}" \
110+
--output-dir diff-results
111+
fi
112+
113+
- name: Post summary
114+
if: always()
115+
run: |
116+
if [ -f diff-results/diff_summary.txt ]; then
117+
echo '### Differential Profile (base → PR)' >> "$GITHUB_STEP_SUMMARY"
118+
echo '```' >> "$GITHUB_STEP_SUMMARY"
119+
cat diff-results/diff_summary.txt >> "$GITHUB_STEP_SUMMARY"
120+
echo '```' >> "$GITHUB_STEP_SUMMARY"
121+
echo '' >> "$GITHUB_STEP_SUMMARY"
122+
fi
123+
if [ -f profile-results/summary.txt ]; then
124+
echo '### PR Branch Profile' >> "$GITHUB_STEP_SUMMARY"
125+
echo '```' >> "$GITHUB_STEP_SUMMARY"
126+
cat profile-results/summary.txt >> "$GITHUB_STEP_SUMMARY"
127+
echo '```' >> "$GITHUB_STEP_SUMMARY"
128+
fi
129+
RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
130+
echo '' >> "$GITHUB_STEP_SUMMARY"
131+
echo '---' >> "$GITHUB_STEP_SUMMARY"
132+
echo "📊 **[Download flamegraph SVGs](${RUN_URL}#artifacts)** — open in a browser for interactive exploration." >> "$GITHUB_STEP_SUMMARY"
133+
echo "" >> "$GITHUB_STEP_SUMMARY"
134+
echo "🔥 **[Latest develop flamegraphs](https://diffblue.github.io/cbmc/profiling/)**" >> "$GITHUB_STEP_SUMMARY"
135+
136+
- name: Clean up worktree
137+
if: always()
138+
run: git worktree remove --force ../base-worktree 2>/dev/null || true
139+
140+
- name: Upload artifacts
141+
if: always()
142+
uses: actions/upload-artifact@v7
143+
with:
144+
name: profile-results
145+
path: |
146+
profile-results/**/flamegraph.svg
147+
profile-results/aggregated.svg
148+
profile-results/summary.txt
149+
profile-results/results.json
150+
base-results/results.json
151+
diff-results/diff_summary.txt
152+
retention-days: 14
153+
154+
- name: Save ccache
155+
if: always()
156+
uses: actions/cache/save@v5
157+
with:
158+
path: .ccache
159+
key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
160+
161+
# ── Develop job: profile and publish flamegraphs to GitHub Pages ─────
162+
profile-develop:
163+
if: github.event_name == 'push'
164+
runs-on: ubuntu-24.04
165+
steps:
166+
- name: Check out repository
167+
uses: actions/checkout@v6
168+
with:
169+
submodules: recursive
170+
171+
- name: Install dependencies
172+
env:
173+
DEBIAN_FRONTEND: noninteractive
174+
run: |
175+
sudo apt-get update
176+
sudo apt-get install --no-install-recommends -yq \
177+
cmake ninja-build gcc g++ flex bison ccache libgoogle-perftools-dev \
178+
linux-tools-common linux-tools-generic
179+
PERF_REAL=$(find /usr/lib/linux-tools-*/perf -maxdepth 0 2>/dev/null | head -1)
180+
if [ -z "$PERF_REAL" ]; then
181+
echo "::error::No perf binary found under /usr/lib/linux-tools-*"
182+
exit 1
183+
fi
184+
echo "$(dirname "$PERF_REAL")" >> "$GITHUB_PATH"
185+
"$PERF_REAL" --version
186+
sudo sysctl kernel.perf_event_paranoid=-1
187+
188+
- name: Restore ccache
189+
uses: actions/cache/restore@v5
190+
with:
191+
path: .ccache
192+
key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}
193+
restore-keys: |
194+
${{ runner.os }}-24.04-Release-profile
195+
${{ runner.os }}-24.04-Release
196+
- run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
197+
198+
- name: Build CBMC (Release)
199+
run: |
200+
cmake -S . -Bbuild -G Ninja -DWITH_JBMC=OFF \
201+
-DCMAKE_BUILD_TYPE=Release \
202+
-DCMAKE_C_COMPILER=/usr/bin/gcc \
203+
-DCMAKE_CXX_COMPILER=/usr/bin/g++
204+
touch build/src/{ansi-c,cpp}/library-check.stamp
205+
ninja -C build cbmc -j$(nproc)
206+
207+
- name: Profile develop (3 runs per benchmark)
208+
run: |
209+
python3 scripts/profile_cbmc.py --auto --runs 3 --timeout 120 \
210+
--output-dir profile-results
211+
212+
- name: Post summary
213+
if: always()
214+
run: |
215+
if [ -f profile-results/summary.txt ]; then
216+
echo '### develop Profile' >> "$GITHUB_STEP_SUMMARY"
217+
echo '```' >> "$GITHUB_STEP_SUMMARY"
218+
cat profile-results/summary.txt >> "$GITHUB_STEP_SUMMARY"
219+
echo '```' >> "$GITHUB_STEP_SUMMARY"
220+
echo '' >> "$GITHUB_STEP_SUMMARY"
221+
echo '---' >> "$GITHUB_STEP_SUMMARY"
222+
echo '🔥 **[Interactive flamegraphs on GitHub Pages](https://diffblue.github.io/cbmc/profiling/)**' >> "$GITHUB_STEP_SUMMARY"
223+
fi
224+
225+
- name: Prepare pages content
226+
if: always()
227+
run: |
228+
mkdir -p pages-out
229+
# Copy all flamegraph SVGs
230+
find profile-results -name 'flamegraph.svg' | while read f; do
231+
bench=$(basename "$(dirname "$f")")
232+
cp "$f" "pages-out/${bench}.svg"
233+
done
234+
[ -f profile-results/aggregated.svg ] && cp profile-results/aggregated.svg pages-out/
235+
[ -f profile-results/summary.txt ] && cp profile-results/summary.txt pages-out/
236+
[ -f profile-results/results.json ] && cp profile-results/results.json pages-out/
237+
# Generate a simple index page
238+
SHORT_SHA=$(echo "${{ github.sha }}" | cut -c1-8)
239+
cat > pages-out/index.html <<'HEADER'
240+
<!DOCTYPE html>
241+
<html><head><meta charset="utf-8">
242+
<title>CBMC Profiling — develop</title>
243+
<style>
244+
body { font-family: system-ui, sans-serif; max-width: 900px; margin: 2em auto; padding: 0 1em; }
245+
h1 { border-bottom: 2px solid #333; padding-bottom: 0.3em; }
246+
a { color: #0366d6; }
247+
.meta { color: #666; font-size: 0.9em; }
248+
ul { line-height: 1.8; }
249+
pre { background: #f6f8fa; padding: 1em; overflow-x: auto; font-size: 0.85em; }
250+
</style>
251+
</head><body>
252+
HEADER
253+
echo "<h1>CBMC Profiling — develop</h1>" >> pages-out/index.html
254+
echo "<p class='meta'>Commit: <code>${SHORT_SHA}</code> — $(date -u '+%Y-%m-%d %H:%M UTC')</p>" >> pages-out/index.html
255+
echo "<h2>Flamegraphs</h2><p>Click to open interactive SVG (searchable, zoomable):</p><ul>" >> pages-out/index.html
256+
for svg in pages-out/*.svg; do
257+
name=$(basename "$svg")
258+
echo "<li><a href=\"${name}\">${name%.svg}</a></li>" >> pages-out/index.html
259+
done
260+
echo "</ul>" >> pages-out/index.html
261+
if [ -f pages-out/summary.txt ]; then
262+
echo "<h2>Summary</h2><pre>" >> pages-out/index.html
263+
cat pages-out/summary.txt >> pages-out/index.html
264+
echo "</pre>" >> pages-out/index.html
265+
fi
266+
echo "<p><a href=\"https://github.com/${{ github.repository }}\">← Back to repository</a></p>" >> pages-out/index.html
267+
echo "</body></html>" >> pages-out/index.html
268+
269+
- name: Publish to GitHub Pages
270+
if: always()
271+
uses: JamesIves/github-pages-deploy-action@v4
272+
with:
273+
branch: gh-pages
274+
folder: pages-out
275+
target-folder: profiling
276+
clean: true
277+
278+
- name: Save ccache
279+
if: always()
280+
uses: actions/cache/save@v5
281+
with:
282+
path: .ccache
283+
key: ${{ runner.os }}-24.04-Release-profile-${{ github.sha }}

‎AGENTS.md‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ cbmc/
6969
│ │ ├── syntax-checks.yaml # Code style and linting
7070
│ │ ├── codeql-analysis.yml # Security analysis
7171
│ │ ├── performance.yaml # Performance benchmarking
72+
│ │ ├── profiling.yaml # Pre-solver profiling on PRs
7273
│ │ └── release-packages.yaml # Release automation
7374
│ └── dependabot.yml # Dependency update automation
7475
├── CODING_STANDARD.md # Coding conventions
@@ -214,6 +215,8 @@ Unit tests using the Catch framework:
214215

215216
- Build helpers and utilities
216217
- `cpplint.py` - Style checker
218+
- `profile_cbmc.py` - Performance profiling tool (see [Profiling CBMC](#6-profiling-cbmc))
219+
- `profiling/` - Profiling package (analysis, benchmarks, runner, utils)
217220
- `test.pl` - Regression test runner (in `regression/`)
218221
- CI/CD related scripts
219222

@@ -764,6 +767,46 @@ cd regression/cbmc
764767
make test
765768
```
766769

770+
### 6. Profiling CBMC
771+
772+
The profiling tool (`scripts/profile_cbmc.py`) profiles CBMC's pre-solver
773+
stages using `perf` and generates flamegraphs. Solver time is excluded by
774+
default so results reflect only CBMC's own code.
775+
776+
**Prerequisites:** Linux with `perf` installed.
777+
778+
```bash
779+
# Profile a single file
780+
scripts/profile_cbmc.py test.c -- --bounds-check --unwind 100
781+
782+
# Run 3 built-in benchmarks (linked_list, array_ops, structs)
783+
scripts/profile_cbmc.py --auto
784+
785+
# Extended suite (10 benchmarks) plus CSmith-generated tests
786+
scripts/profile_cbmc.py --auto-large --auto-csmith
787+
788+
# Multiple runs for statistical significance (reports mean ± stddev)
789+
scripts/profile_cbmc.py --auto --runs 3
790+
791+
# Source-level call site resolution (build a debug binary first)
792+
cmake -S . -Bbuild-debug -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF
793+
cmake --build build-debug --target cbmc -j$(nproc)
794+
scripts/profile_cbmc.py --auto --debug-binary build-debug/bin/cbmc
795+
796+
# Differential profiling: compare two git refs
797+
scripts/profile_cbmc.py --diff develop my-optimization-branch
798+
```
799+
800+
**Outputs** (in `profile-results/` by default):
801+
- `flamegraph.svg` per benchmark - Interactive flamegraph
802+
- `aggregated.svg` - Combined flamegraph across all benchmarks
803+
- `summary.txt` - Text summary with hotspot analysis and optimization suggestions
804+
- `results.json` - Machine-readable results
805+
806+
**CI integration:** The `profiling.yaml` workflow runs `--auto --runs 3` on
807+
every PR, posts the summary to the GitHub step summary, and uploads
808+
flamegraph SVGs as downloadable artifacts.
809+
767810
---
768811

769812
## Navigation Tips
@@ -894,6 +937,7 @@ To understand how data flows through CBMC:
894937
| Create GOTO binary | `goto-cc -o out.gb input.c` |
895938
| View GOTO program | `goto-instrument --show-goto-functions prog.gb` |
896939
| Run CBMC | `cbmc program.gb` or `cbmc program.c` |
940+
| Profile CBMC | `scripts/profile_cbmc.py --auto --runs 3` |
897941

898942
### Key Files to Know
899943

‎doc/architectural/compilation-and-development.md‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,6 +281,42 @@ There are also instructions for adding this as a git pre-commit hook in
281281

282282
\section compilation-and-development-section-time-profiling Time profiling
283283

284+
\subsection compilation-and-development-subsection-perf-profiling Profiling with perf (recommended)
285+
286+
The script `scripts/profile_cbmc.py` profiles CBMC's pre-solver stages using
287+
`perf` and generates interactive flamegraphs. Solver time is excluded by default
288+
so that results reflect only CBMC's own code. This requires Linux with `perf`
289+
installed.
290+
291+
Quick start with built-in benchmarks:
292+
293+
scripts/profile_cbmc.py --auto
294+
295+
For multiple runs (reports mean ± stddev):
296+
297+
scripts/profile_cbmc.py --auto --runs 3
298+
299+
To profile a specific input file:
300+
301+
scripts/profile_cbmc.py test.c -- --bounds-check --unwind 100
302+
303+
For source-level call site resolution, build a separate debug binary and pass it
304+
via `--debug-binary` (profiling still uses the fast Release build):
305+
306+
cmake -S . -Bbuild-debug -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF
307+
cmake --build build-debug --target cbmc -j$(nproc)
308+
scripts/profile_cbmc.py --auto --debug-binary build-debug/bin/cbmc
309+
310+
To compare performance between two git refs:
311+
312+
scripts/profile_cbmc.py --diff develop my-optimization-branch
313+
314+
Results are written to `profile-results/` by default and include flamegraph SVGs,
315+
a text summary with hotspot analysis, and machine-readable JSON. Run
316+
`scripts/profile_cbmc.py --help` for the full set of options.
317+
318+
\subsection compilation-and-development-subsection-gprof-profiling Profiling with gprof
319+
284320
To do time profiling with a tool like `gprof`, the flags `-g` (build with debug
285321
symbols) and `-pg` (enable profiling information) must be
286322
used when compiling, and `-pg` must be used when linking. If you are building

0 commit comments

Comments
 (0)