Skip to content

Re-ground Infer's tool-native decline on an enumerated-and-executed activation surface (A28) - #124

Merged
DavidBakerEffendi merged 3 commits into
mainfrom
dave/infer-native-a27
Sep 2, 2026
Merged

Re-ground Infer's tool-native decline on an enumerated-and-executed activation surface (A28)#124
DavidBakerEffendi merged 3 commits into
mainfrom
dave/infer-native-a27

Conversation

@DavidBakerEffendi

@DavidBakerEffendi DavidBakerEffendi commented Sep 2, 2026

Copy link
Copy Markdown
Collaborator

What this is

A maintainer challenge sent Amendment A14's central phrase — "Pulse taint is off absent a configuration" — into the field, the same movement A25 (OpenTaint) and A26 (Joern) made for their native declines. Part of the phrase failed. The decline survives on stronger evidence, recorded as Amendment A28. No cell moves: all six Infer native cells stay unsupported, 0 / 6, Java alone.

What was measured (all three arms executed on the pinned v1.3.0 binary, evidence retained under reports/raw/amendment-a28-infer-native-activation/)

  1. The distribution bundles default taint data — enumerated. Exactly one shipped taint surface exists: lib/infer/infer/config/taint/, four Objective-C NSLib files (NSString, NSArray, NSDictionary, NSSet) plus a README stating they "are always included when running infer". Every file's single top-level key is pulse-taint-propagators. No sources, no sinks, no sanitizers, no policies, no .inferconfig anywhere in the distribution, no Java identity.
  2. A zero-configuration invocation activates it — proven, not quoted. Corrupting one bundled file in a byte copy of the distribution kills a zero-config Java capture with exit 3, the error naming the file from Config.pulse_taint_config's directory fold (engagement-proof-transcript.txt). This matters because the pinned release's signature failure mode is silent config loss: here the opposite is established — A14's silence is an engaged silence. The loader runs, loads the shipped taint data, and that data binds no endpoint to any policy.
  3. The full default surface decides nothing the split invocation missed. infer run --sarif — the release's whole default checker set, not the adapter's capture + analyze --pulse-only arms — produced zero findings of any rule over all twelve Java native fixtures (verbatim SARIF retained per fixture). No non-taint Pulse finding exists to reconcile against any anchor, so no cell becomes a live activation deciding not-reached.

Why the cells stay declined

The shipped model set expresses no flow question over any probe endpoint — the one taint artifact it ships is propagator-only and Objective-C-only. The twelve zero-finding full-default runs are the decline's evidence, not scored runs; not-reached would assert an asked question that found no flow, and no question is asked. (A7's / A26's distinction.)

What changes where

  • docs/native-profile.md — A28 amendment entry; the Infer activation section gains the engaged-silence paragraph (A14's imprecise sentence stays quoted, per the retired-sentence discipline); table rows 1–2 restated.
  • src/main.rs — the six NATIVE_PARTITION Infer rationales re-grounded (Amendments A14, A28). The retained 0 / 6 report predates the amendment and keeps A14's wording, exactly as A26 left Joern's; the corrected strings land with the next evidence re-run.
  • docs/java-native.md, adapters/infer/README.md — mirrored.
  • scripts/probe-infer-native-activation.sh — the three-arm probe (works on a scratch copy; the pinned distribution is never mutated).

Battery

cargo fmt --check ✓ · cargo test 207 ✓ · validate 852 cases ✓ · validate-reports 82 ✓ · validate-freeze reports/freeze.json (v0.6.1) ✓ · generate-results --check current ✓ · astro build 45 pages ✓

Amendment number: drafted as A27, renumbered to A28 before merge — the concurrent #123 claims A27 for Semgrep's native re-grounding (race note recorded in the entry). Rebased on main past A25 (#121) and A26 (#122).

🤖 Generated with Claude Code

…ctivation surface (A28)

A maintainer challenge sent A14's phrase "Pulse taint is off absent a
configuration" into the field, where half of it failed: the pinned v1.3.0
distribution DOES bundle default taint data (lib/infer/infer/config/taint/,
four Objective-C NSLib files), and a zero-configuration invocation DOES load
it — proven by corrupting one bundled file in a byte copy of the
distribution and watching a zero-config Java capture die (exit 3) from
Config.pulse_taint_config's directory fold. The decline survives on stronger
evidence: the loaded bundle declares pulse-taint-propagators only — no
source, sink, sanitizer, or policy in any language, no .inferconfig, no Java
identity — and the release's full default checker set (infer run --sarif,
not the adapter's --pulse-only arm) fires zero findings of any rule over all
twelve Java native fixtures, so no live activation decides not-reached and
all six cells stay unsupported.

Evidence retained under reports/raw/amendment-a28-infer-native-activation/
(scripts/probe-infer-native-activation.sh). NATIVE_PARTITION rationales,
the profile's Infer activation section, docs/java-native.md, and the adapter
README are re-grounded; the retained 0/6 report predates the amendment and
keeps A14's wording, exactly as A26 left Joern's. Drafted as A27, renumbered
to A28: the concurrent #123 claims A27 for Semgrep.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@DavidBakerEffendi DavidBakerEffendi changed the title Re-ground Infer's tool-native decline on an enumerated-and-executed activation surface (A27) Re-ground Infer's tool-native decline on an enumerated-and-executed activation surface (A28) Sep 2, 2026
@DavidBakerEffendi
DavidBakerEffendi merged commit ffd5b99 into main Sep 2, 2026
2 checks passed
@DavidBakerEffendi
DavidBakerEffendi deleted the dave/infer-native-a27 branch September 2, 2026 07:48
DavidBakerEffendi added a commit that referenced this pull request Sep 2, 2026
Fixes #131.

## What

`sarif_anchor_outcome` returns `not-reached` as soon as a SARIF document
has zero results, and the kernel queries select flows only — nothing
verified that the `dfb_source`/`dfb_sink` endpoints were actually
extracted into the database. A *recoverable* per-file parse error in an
interpreted-language extractor (JS/TS/Python/Ruby) that drops the sink
expression would therefore yield a vacuous clean true-negative with no
diagnostic.

This PR adds an endpoint-observation guard on the same terms as
`JoernEndpointRule::BothMustBeObserved`:

- **Eleven companion probe queries**, one per kernel population, living
beside each kernel query in its own pack
(`<Language>KernelEndpointProbe.ql`, rule id
`dataflowbench/<language>-kernel-endpoint-probe`). Each probe mirrors
its kernel's own endpoint recognizers exactly — the
`dfb_source()`/`dfb_sink(value)` contract, the Java kernel's extra
endpoint names, and the file-extension guards where C/C++, Kotlin, and
the two ECMA populations share an extractor — and reports one row per
endpoint the extracted database resolves.
- **One `database analyze` invocation** evaluates the kernel query and
the probe together, so the retained SARIF is the raw evidence for both
(the probe output is retained as-is on disk).
- **Normalization** splits the probe's rows back out before any finding
is reconciled (`split_codeql_endpoint_probe`), so kernel result sets and
retained diagnostics are unchanged by the probe running alongside. A run
whose probe never observed both benchmark-controlled endpoints is
normalized to `inconclusive` (`unobserved_codeql_endpoint_outcome`),
never `not-reached`; a document with no analysis run stays
`runner-error`. The gate sits before flow reconciliation, exactly where
Joern applies its endpoint rule.
- **The modeling matrix runs no probe** — an absent *declared* endpoint
is frequently the assertion a modeling negative makes (the
`AbsenceIsTheAssertion` analogue) — and the tool-native profile is
untouched.
- Each population's `configuration_hash` now binds the probe query, and
each runner fails fast when the probe file is missing.

## Tests

Mirrors the existing anti-vacuous tests
(`sarif_execution_errors_prevent_clean_negative_interpretation`, the
Joern endpoint tests):

- `codeql_endpoint_probe_rows_are_split_from_kernel_findings`
- `an_unobserved_codeql_endpoint_prevents_clean_negative_interpretation`
- `every_codeql_kernel_evaluates_an_endpoint_probe_beside_its_query`
(all eleven populations: probe exists in the kernel query's pack,
declares `@kind problem` and the expected rule id, and is recognized by
the runner's split predicate)

## Verification

- `cargo fmt --check`, `cargo test` (210 passed), `cargo run --
validate` (852 cases), `cargo run -- validate-reports` (82 reports) all
pass.
- All eleven probe queries compile cleanly with `codeql query compile`
under the pinned CLI 2.26.4 (build
`6b1e4dee94adb20f90a671f3fc9e04be32eecf65`) against the committed pack
locks.
- End-to-end shape check on a scratch JavaScript database (no committed
evidence touched): analyzing kernel + probe in one invocation yields
probe rows with rule id `dataflowbench/javascript-kernel-endpoint-probe`
and messages `Benchmark source/sink endpoint observed.`, which is
exactly what the splitter keys on.

## Committed reports need a re-run

The changed normalization semantics and configuration hashes supersede
the committed CodeQL kernel evidence. **No reports were hand-edited.**
The eleven CodeQL kernel populations (Java, JavaScript, TypeScript,
Python, Kotlin, C#, Go, C, C++, Rust, Ruby) need a re-run under a new
amendment before the next freeze, per docs/freeze.md and the amendment
conventions in docs/adapters.md. Note the repo-wide amendment sequence
currently tops out at A29 with A27–A29 still open (#123, #124, #125) —
refetch main before claiming a number.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant