Add profiling tool and run in CI by tautschnig · Pull Request #8859 · diffblue/cbmc

tautschnig · 2026-03-11T09:21:19Z

Add scripts/profile_cbmc.py and scripts/profiling/ package for profiling CBMC's pre-solver stages using perf with flamegraph generation.

Features:

perf-based sampling with DWARF call graphs (16KB stack dumps, empirically validated to capture 91% of full stacks at 25% of the data size vs the default 64KB)
Aggregated results across multiple benchmarks with call chain analysis
Source-level call site resolution via addr2line (--debug-binary)
Built-in benchmarks: --auto (3 quick), --auto-large (10 extended), --auto-csmith (5 CSmith-generated with fixed seeds)
Differential profiling between git refs (--diff REF_A REF_B)
Multi-run mode for statistical significance (--runs N)
Actionable hotspot analysis showing direct callers, call paths, per-benchmark breakdown, and source locations

CI run sthe profiling tool on every PR with 3 runs per benchmark for statistical significance. Posts a text summary to the GitHub step summary and uploads flamegraph SVGs as downloadable artifacts.

Co-authored-by: Kiro kiro-agent@users.noreply.github.com

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copilot

Pull request overview

Adds a new CBMC profiling utility (Python) that runs perf on selected benchmarks, generates per-benchmark + aggregated flamegraphs, and summarizes hotspots; plus a GitHub Actions workflow to run it on PRs.

Changes:

Introduces scripts/profile_cbmc.py and scripts/profiling/* to run perf record/report, generate FlameGraph SVGs, and print/save summaries (including optional multi-run averaging and diff mode).
Adds benchmark generation (built-in suites + optional CSmith seeds) to standardize profiling inputs.
Adds .github/workflows/profiling.yaml to run profiling on PRs and upload outputs as artifacts.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 9 comments.

Show a summary per file

File	Description
scripts/profiling/utils.py	Common helpers, prerequisite checks, CBMC/FlameGraph discovery (with auto-clone).
scripts/profiling/runner.py	Executes perf-recorded benchmark runs; parses perf report; generates flamegraphs; supports multi-run averaging.
scripts/profiling/benchmarks.py	Generates built-in benchmark C sources and optional CSmith-based benchmarks.
scripts/profiling/analysis.py	Aggregates results, derives hotspot/call-chain summaries, writes summary.txt/results.json, optional addr2line mapping.
scripts/profiling/init.py	Declares the profiling package.
scripts/profile_cbmc.py	CLI entrypoint orchestrating builds/benchmarks/profiling, including diff mode via git worktrees.
.github/workflows/profiling.yaml	CI job to build CBMC, run profiling, publish summary and artifacts.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

codecov · 2026-03-11T10:09:48Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.01%. Comparing base (7a4df92) to head (70825b7).
⚠️ Report is 28 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8859   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1703     1703           
  Lines       188396   188396           
  Branches        73       73           
========================================
  Hits        150738   150738           
  Misses       37658    37658

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Add scripts/profile_cbmc.py and scripts/profiling/ package for profiling CBMC's pre-solver stages using perf with flamegraph generation. Features: - perf-based sampling with DWARF call graphs (16KB stack dumps, empirically validated to capture 91% of full stacks at 25% of the data size vs the default 64KB) - Aggregated results across multiple benchmarks with call chain analysis - Source-level call site resolution via addr2line (--debug-binary) - Built-in benchmarks: --auto (3 quick), --auto-large (10 extended), --auto-csmith (5 CSmith-generated with fixed seeds) - Differential profiling between git refs (--diff REF_A REF_B) - Multi-run mode for statistical significance (--runs N) - Actionable hotspot analysis showing direct callers, call paths, per-benchmark breakdown, and source locations Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Run the profiling tool on every PR with 3 runs per benchmark for statistical significance. Posts a text summary to the GitHub step summary and uploads flamegraph SVGs as downloadable artifacts. Uses the --auto benchmarks (linked_list, array_ops, structs) which exercise pointer analysis, array encoding, and struct handling respectively. Solver time is excluded to focus on CBMC's own code. The GitHub step summary now shows both: 1. Differential profile (base → PR) with timing and function changes 2. Full PR branch profile with hotspot analysis Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add documentation for scripts/profile_cbmc.py and the profiling CI workflow to AGENTS.md: - profiling.yaml in the repository structure tree - profile_cbmc.py and profiling/ package in the scripts section - New 'Profiling CBMC' workflow section with usage examples, outputs, and CI integration notes - Profiling command in the Quick Reference Card Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add a 'Profiling with perf (recommended)' subsection to the existing Time profiling section, describing scripts/profile_cbmc.py with usage examples. The existing gprof documentation is preserved as a separate subsection. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

peterschrammel · 2026-03-21T13:40:52Z

Is the intention that this is run on every PR? Or should it rather run on demand (e.g. label-triggered)?
How long does the CI job take?

tautschnig · 2026-03-22T21:01:42Z

Is the intention that this is run on every PR? Or should it rather run on demand (e.g. label-triggered)? How long does the CI job take?

It does run both on PR as well as push to develop (alas there are two jobs profile-PR and profile-develop, where the latter does not run here). The profile-PR job took 3 minutes, see https://github.com/diffblue/cbmc/actions/runs/23057104517?pr=8859 (also check out the job Summary page for consolidated results).

tautschnig requested review from a team and peterschrammel as code owners March 11, 2026 09:21

Copilot AI review requested due to automatic review settings March 11, 2026 09:21

Copilot started reviewing on behalf of tautschnig March 11, 2026 09:21 View session

Copilot AI reviewed Mar 11, 2026

View reviewed changes

tautschnig force-pushed the profiling-tool branch from a18ffa9 to 2e653e4 Compare March 13, 2026 11:40

tautschnig requested review from TGWDB, jimgrundy and kroening as code owners March 13, 2026 11:40

tautschnig force-pushed the profiling-tool branch from a1b7935 to 56eaad6 Compare March 13, 2026 12:33

tautschnig and others added 3 commits March 13, 2026 15:06

tautschnig force-pushed the profiling-tool branch from e19f714 to 70825b7 Compare March 13, 2026 15:08

tautschnig assigned tautschnig, kroening, peterschrammel and TGWDB and unassigned tautschnig and kroening Mar 13, 2026

peterschrammel approved these changes Mar 27, 2026

View reviewed changes

tautschnig merged commit 0170409 into diffblue:develop Mar 27, 2026
43 checks passed

tautschnig deleted the profiling-tool branch March 27, 2026 23:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add profiling tool and run in CI#8859

Add profiling tool and run in CI#8859
tautschnig merged 4 commits intodiffblue:developfrom
tautschnig:profiling-tool

tautschnig commented Mar 11, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Mar 11, 2026 •

edited

Loading

Uh oh!

peterschrammel commented Mar 21, 2026

Uh oh!

tautschnig commented Mar 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

tautschnig commented Mar 11, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Mar 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

peterschrammel commented Mar 21, 2026

Uh oh!

tautschnig commented Mar 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

codecov Bot commented Mar 11, 2026 •

edited

Loading