Add CI profiling workflow

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.

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

Author: tautschnig

.github/workflows/profiling.yaml

@@ -0,0 +1,104 @@
+# CBMC Profiling Workflow
+#
+# Runs the CBMC profiling tool on every PR to detect performance changes
+# in the pre-solver pipeline (parsing, type-checking, goto conversion,
+# instrumentation, symbolic execution, and propositional encoding).
+#
+# What it does:
+#   1. Builds CBMC in Release mode (fast, symbols not stripped)
+#   2. Runs 3 built-in benchmarks (linked_list, array_ops, structs) 3 times
+#      each for statistical significance
+#   3. Generates flamegraphs and an aggregated hotspot analysis
+#   4. Posts the text summary to the GitHub step summary
+#   5. Uploads flamegraph SVGs and results as downloadable artifacts
+#
+# 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
+#
+# For more thorough profiling with source locations:
+#   cmake -S . -Bbuild-debug -DCMAKE_BUILD_TYPE=RelWithDebInfo -DWITH_JBMC=OFF
+#   cmake --build build-debug --target cbmc -j$(nproc)
+#   scripts/profile_cbmc.py --auto-large --auto-csmith --runs 3 \
+#     --debug-binary build-debug/bin/cbmc
+
+name: Profiling
+on:
+  pull_request:
+    branches: [ develop ]
+
+jobs:
+  profile:
+    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 \
+            linux-tools-common linux-tools-$(uname -r) || true
+          # perf requires perf_event_paranoid=-1 for call graph recording
+          sudo sysctl kernel.perf_event_paranoid=-1
+
+      - name: Prepare 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)
+
+      # Run each benchmark 3 times for statistical significance.
+      # The summary reports mean ± stddev for timings.
+      - name: Run profiling (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 '```' >> "$GITHUB_STEP_SUMMARY"
+            cat profile-results/summary.txt >> "$GITHUB_STEP_SUMMARY"
+            echo '```' >> "$GITHUB_STEP_SUMMARY"
+          fi
+
+      # Flamegraphs are interactive SVGs — download and open in a browser.
+      - name: Upload artifacts
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: profile-results
+          path: |
+            profile-results/*/flamegraph.svg
+            profile-results/aggregated.svg
+            profile-results/summary.txt
+            profile-results/results.json
+          retention-days: 14