Proposal: Checkable Precision Diagnostics for Infer Analyses

## Proposal: Checkable imprecision diagnostics for Infer analyses using Error Propagation Logic

Hi Infer maintainers,

Would there be interest in an experimental, disabled-by-default infrastructure/checker for **quantifying precision loss in Infer analyses and, where supported, attributing it to analysis operations**?

The implementation is based on the POPL 2026 paper *A Logic for the Imprecision of Abstract Interpretations*:
https://doi.org/10.1145/3776707

Our intended use case is **analyzer development and precision diagnostics**, rather than introducing another user-facing bug detector.

### Motivation

When an abstract analysis produces an unexpectedly imprecise result, the final issue set does not necessarily show where precision was lost or whether an analysis change improved the underlying invariants without eliminating the final warning.

We have been experimenting with Error Propagation Logic (EPL) as an additional diagnostic layer over existing Infer analysis results. Two cases illustrate the intended use.

#### Connecting precision loss to an existing false positive

Infer currently contains the regression test `call_fromHex2_200_Good_FP` in `prune_constant.c`.

For this call, our checked reference witness yields a return interval of:

```text
[-1,-1]
```

and therefore a downstream array index of:

```text
[0,0]
```

The cached InferBO summary observed by our adapter yields:

```text
[-29,15]
```

which expands the downstream index to:

```text
[-28,16]
```

and corresponds to the existing `BUFFER_OVERRUN_L3` report.

This gives us a concrete example where a quantitative precision difference can be connected to an existing Infer false positive and attributed to summary application.

#### Measuring analysis-policy improvements that do not remove a warning

In an instrumented run on bzip2 `compress.c`, changing the widening schedule tightened the inferred interval for `bt` from:

```text
[-1,+∞]
```

to:

```text
[-1,5]
```

The relevant warning remained because the lower bound was still `-1`.

Thus an issue-based regression test alone would not reveal this improvement, while an explicit precision measurement can distinguish the two analysis results. The more precise configuration also required substantially more abstract interpretation work, making this a useful example of a precision/cost tradeoff.

These experiments suggest three possible uses for such diagnostics:

1. connecting precision loss to downstream false positives;
2. detecting precision changes that are invisible to issue-based regression tests;
3. comparing precision/cost tradeoffs between analysis strategies.

### Current prototype

We currently have a working prototype with:

* an Infer-independent OCaml implementation of the EPL proof rules used by the prototype;
* typed proof objects and a separate fail-closed checker that can replay them independently;
* a read-only Infer adapter comparing checked generator witnesses with cached InferBO interval invariants;
* restricted support for acyclic signed-int32 SIL fragments and a checked counting-loop `Iterate` adapter;
* focused OCaml and C integration tests;
* no modifications to Infer's abstract interpreter, transfer functions, joins, widening schedule, summaries, or ordinary reports.

By "checkable" here, we mean that the diagnostic bound is accompanied by a proof object replayed by a separate checker; we are not claiming that the checker implementation itself is formally verified.

The current Infer integration uses InferBO because its numeric invariants provided a convenient first integration point. InferBO is currently marked deprecated in favor of Pulse, so before investing further in the integration we would like guidance on the appropriate long-term target.

### Questions

1. **Would analyzer-relative precision diagnostics of this kind be useful and in scope for Infer?**

2. **If so, what would be the preferred analysis/integration point today?**

Pulse may be the natural long-term target given InferBO's deprecation, but its analysis state and interface are quite different. Would a read-only InferBO prototype still be useful as an initial demonstration, or would you prefer that any upstream work start directly from another analysis?

3. **If there is interest, what would be the most useful minimal first contribution?**

We would prefer to start with a small end-to-end, read-only integration around one existing Infer regression case rather than proposing the complete prototype as a single change.

The current prototype builds in Infer's development environment and passes its focused tests.

If this direction is of interest, we can publish a clean prototype branch and prepare a small first contribution based on maintainer guidance.

Thanks!