86b2f14a43
- persist TU-owned graphs and guarded configuration evidence - add closed-world production reachability classification - calibrate detector precision and reviewed self-scan policy - terminate poisoned workers instead of longjmp recovery
91 lines
4.4 KiB
Markdown
91 lines
4.4 KiB
Markdown
# Production reachability evidence
|
|
|
|
Fold's whole-program reachability lane is distinct from translation-unit
|
|
`unused-function`, local `dead`, and CFG-only `unreachable` analysis. It uses
|
|
versioned, TU-owned graph contributions and linkage-aware semantic USRs.
|
|
|
|
## Root inventory
|
|
|
|
Each parsed translation unit contributes evidence for:
|
|
|
|
- executable `main` definitions;
|
|
- explicit entrypoints from a versioned configuration profile (USR or qualified
|
|
name; ambiguous qualified names conservatively match every overload);
|
|
- explicitly exported ABI functions (`extern "C"`, default visibility, or
|
|
platform export attributes);
|
|
- functions invoked by static initializers;
|
|
- function addresses passed as callbacks or otherwise escaping;
|
|
- concrete-class virtual methods, retained as conditional candidates until
|
|
reachable construction and target closure are established;
|
|
- test, benchmark, example, and third-party entrypoints, retained separately
|
|
from production roots.
|
|
|
|
Root records preserve the function USR, owning source, evidence location, root
|
|
kind, production/test domain, and whether activation is conditional. They are
|
|
persisted transactionally with the owning TU. Warm graph assembly reuses them;
|
|
source/header/flag/profile/schema changes invalidate them with the rest of the
|
|
contribution.
|
|
|
|
## Proof boundary
|
|
|
|
Root discovery does not itself classify or delete code. The inventory is
|
|
closed-world only when:
|
|
|
|
- every explicit root selector resolves;
|
|
- persisted rows pass schema and enum validation; and
|
|
- no unresolved virtual or indirect callsite remains.
|
|
|
|
Missing selectors and unresolved dynamic calls are coverage failures, never
|
|
proof that a function is dead. Exported ABI functions and escaped callbacks are
|
|
conservative roots. Virtual candidates require the guarded reachability phase
|
|
to establish that a concrete owner is instantiated from a reachable path.
|
|
|
|
Profile telemetry reports bounded counts for production, test, conditional, and
|
|
unresolved explicit roots plus the closed-world flag. It does not emit selectors
|
|
or source expressions.
|
|
|
|
## Guarded classification
|
|
|
|
Enable the project pass with `--detectors production-reachability` (also part of
|
|
`quality` and `dead-code`). Fold forces this detector through one in-process,
|
|
whole-project graph rather than merging unsound per-worker classifications.
|
|
Guarded callsites sharing a caller and target are alternatives: their guards are
|
|
ORed, never ANDed.
|
|
|
|
The classifier uses bounded Z3 reachability constraints with a strictly
|
|
increasing path distance. This prevents a disconnected recursive SCC from
|
|
proving itself reachable. It evaluates paths under profile assumptions and with
|
|
configuration symbols existentially free, then assigns one mutually exclusive
|
|
class:
|
|
|
|
- `production-reachable`: a production-root path is feasible, or conservative
|
|
evidence prevents a stronger conclusion;
|
|
- `test-only`: reachable from test roots but not production roots in a closed
|
|
graph;
|
|
- `default-inactive`: infeasible under the supplied profile but feasible under
|
|
another configuration;
|
|
- `configuration-infeasible`: structurally connected but UNSAT for all modeled
|
|
configurations;
|
|
- `unreachable-production`: disconnected from production and test roots in a
|
|
closed graph;
|
|
- `compile-variant-absent`: reserved for explicit finite variant manifests and
|
|
never inferred from one compile database.
|
|
|
|
Unknown guards are treated as feasible. Solver timeout, budget exhaustion,
|
|
unresolved selectors or dispatch, missing roots, conditional virtual roots, and
|
|
escaped functions produce conservative `production-reachable` records with
|
|
blockers. A reachability-only scan may reuse direct-edge TU contributions when
|
|
unresolved callsites remain, but it preserves `closed_world=false`, performs no
|
|
solver queries, and emits no removal candidate. Other graph consumers retain
|
|
the exhaustive fallback. SAT or UNKNOWN never becomes a removal candidate.
|
|
Only a complete,
|
|
closed-world `unreachable-production` record sets `removal_candidate=true`;
|
|
`test-only`, `default-inactive`, and `configuration-infeasible` remain review
|
|
evidence.
|
|
|
|
The detector emits function-level `production-reachability` findings with a
|
|
stable semantic identity and structured native-JSON/SARIF evidence. It does not
|
|
emit branch/callsite findings and therefore does not duplicate local
|
|
`branch-infeasible`, `dead-statement`, or `always-condition` results. Source
|
|
locations remain absent when the persisted graph has only semantic identity and
|
|
source-file provenance; Fold does not fabricate line numbers.
|