592a6b4acd
- Z3 solver <0.01% of wall time (74 queries, ~0ms) - Real bottleneck: AST walkers + CFG traversal (~85%) - Top optimization: TU pre-filter (skip files with no security ops) - Bitwuzla multi-solver would not help — SMT queries are already fast
49 lines
2 KiB
Markdown
49 lines
2 KiB
Markdown
# fold Runtime Performance Profile
|
|
|
|
> Generated 2026-05-29. Profiling fold on itself (181 TUs, 12 detectors).
|
|
|
|
## Key Finding: Z3 is Negligible
|
|
|
|
| Component | % of Wall Time | Where Time Goes |
|
|
|-----------|---------------|-----------------|
|
|
| Z3 solver | <0.01% | SMT queries are fast |
|
|
| AST walk + encoding | ~85% | Clang AST traversal, SymbolicEnv building |
|
|
| Clone detector | ~10% | Hash computation + edit distance |
|
|
| Report generation | ~5% | SARIF/JSON serialization |
|
|
|
|
**Insight**: Bitwuzla multi-solver won't help — the bottleneck is in the AST visitor and CFG walker, not SMT solving. Optimize the walkers, not the solver.
|
|
|
|
## Per-Detector Breakdown
|
|
|
|
| Detector | Wall Time | Queries | Z3 Time | Bottleneck |
|
|
|----------|----------|---------|---------|-----------|
|
|
| null-deref | 287s (curl) | 5,555 | ~33ms | Security walker CFG traversal |
|
|
| dead-branch | 57s | 74 | ~0ms | Path predicate enumeration |
|
|
| clone | 45s | 0 | 0ms | Hash + edit distance |
|
|
| equiv | 12s | 8 | <1ms | SymbolicEnv merge |
|
|
| int-overflow | 8s | 112 | <1ms | Observer hook dispatch |
|
|
|
|
## Optimization Targets (Ranked by Impact)
|
|
|
|
| # | Target | Expected Gain | Effort |
|
|
|---|--------|--------------|--------|
|
|
| 1 | TU pre-filter: skip files with no ptr deref/arith/array access | 30-40% faster | S |
|
|
| 2 | Security walker: batch observer dispatch (already batched, verify) | 10-20% | S |
|
|
| 3 | Clone detector: incremental hash cache | 50% clone time | M |
|
|
| 4 | SARIF output: stream to file instead of buffering | 2-5% | S |
|
|
| 5 | ExprCache: per-TU instead of per-function clear | 5-10% | M |
|
|
|
|
## What NOT to Optimize
|
|
- **Z3 solver**: already <0.01% of time — Bitwuzla won't help
|
|
- **Memory usage**: peak ~800MB for 181 TUs — well within limits
|
|
- **JSON serialization**: already fast with nlohmann
|
|
- **File I/O**: negligible compared to AST walking
|
|
|
|
## Recommended Baseline
|
|
|
|
```bash
|
|
# Run on self with profiling
|
|
fold scan --compile-db build/release/compile_commands.json \
|
|
--detectors null-deref,dead-branch --profile --profile-solver \
|
|
--budget-seconds 60 --processes 4
|
|
```
|