Add profiling tool and run in CI#8859
Open
tautschnig wants to merge 4 commits intodiffblue:developfrom
Open
Conversation
There was a problem hiding this comment.
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.pyandscripts/profiling/*to runperf 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.yamlto 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 Report✅ All modified and coverable lines are covered by tests. 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. 🚀 New features to boost your workflow:
|
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>
tautschnig
force-pushed
the
profiling-tool
branch
from
a18ffa9 to
2e653e4
Compare
tautschnig
force-pushed
the
profiling-tool
branch
from
a1b7935 to
56eaad6
Compare
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>
tautschnig
force-pushed
the
profiling-tool
branch
from
e19f714 to
70825b7
Compare
tautschnig
assigned
tautschnig,
kroening,
peterschrammel and
TGWDB and unassigned
tautschnig
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add scripts/profile_cbmc.py and scripts/profiling/ package for profiling CBMC's pre-solver stages using perf with flamegraph generation.
Features:
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