trvon 592a6b4acd

docs: fold runtime performance profile — Z3 is not the bottleneck

- 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

2026-05-29 14:05:03 -04:00

2 KiB

Raw Permalink Blame History

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

# 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

2 KiB Raw Permalink Blame History