From b0020590c549a019437de1e72402472a8a5de5c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Jun 2026 09:16:18 +0000 Subject: [PATCH] =?UTF-8?q?docs(oracle):=20record=20the=20first=20Dapper?= =?UTF-8?q?=20three-way=20=E2=80=94=20Infer#=20trio=20is=20ownership-trans?= =?UTF-8?q?fer?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verified the 3 Infer# leak-class findings from the first real run against Dapper's source: all are `WrappedBasicReader`/`DbWrappedReader` whose ownership is transferred to the caller (`ExecuteReader*` returns `DbWrappedReader.Create(...)`; the `GetRowParser`/`GetDbDataReader` adapter wraps the caller's own reader). The wrapper's `Dispose()` forwards to `_reader.Dispose()` — it's the holder's disposal handle. So Infer# over-reports on the returns-IDisposable pattern, exactly the escape/ ownership-transfer case Own.NET's model treats as not-a-leak: our 0 is correct, Infer#'s 3 are likely false positives (a precision data-point, not a recall gap). CodeQL's 2 (`cs/dispose-not-called-on-throw`) are exception-path disposal, which we don't model by design. `own-only 0` also reflects coverage (async/interprocedural we under-analyse) — motivates the extractor `--stats`. Docs-only. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- docs/notes/oracle.md | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/docs/notes/oracle.md b/docs/notes/oracle.md index 0b03b4c9..75e72c33 100644 --- a/docs/notes/oracle.md +++ b/docs/notes/oracle.md @@ -101,6 +101,42 @@ Pair this with the extractor's planned `--stats` coverage (methods analysed vs skipped) and the picture is complete: how much we looked at, and how our verdicts line up with two independent engines. +## What the first Dapper three-way showed (a worked example) + +Running all three on Dapper's **product code** (commit `72a54c4`; `--exclude-tests` +dropped 165 test/benchmark findings) gave **Own.NET 0 · Infer# 3 · CodeQL 2** +leak-class, `agree 0`, and **`own-only 0`** (no false positives from us). The five +oracle-only findings are both classes we deliberately don't model — and one of them +is arguably a *precision win for us*: + +- **Infer# ×3** — all `WrappedBasicReader` / `DbWrappedReader` in `SqlMapper` + (`SqlMapper.cs:1952`, `:3294`, `SqlMapper.IDataReader.cs:118`): "resource + allocated … is not closed." But that wrapper is Dapper's **caller-owned disposal + handle** — `ExecuteReader*` does `return DbWrappedReader.Create(cmd, reader)` + (ownership handed to the caller), and the `GetRowParser`/`GetDbDataReader` adapter + wraps the *caller's own* reader (disposing it would close the caller's reader). + `WrappedBasicReader.Dispose()` simply forwards to `_reader.Dispose()` — it exists + precisely so the **holder** disposes it. So these are Infer# **over-reports on the + returns-`IDisposable` pattern** — exactly the escape / ownership-transfer case + Own.NET treats as *not a leak*. Our `0` is the right verdict here; Infer#'s `3` + look like false positives. (Verified against `WrappedReader.cs` and the + `ExecuteReader` return; the two `SqlMapper.cs` sites match the same direct-return + and adapter shapes.) +- **CodeQL ×2** — `cs/dispose-not-called-on-throw` at `SqlMapper.cs:1242/1333`: a + disposable local may leak *only if* an exception is thrown mid-method. We don't + model exceptional CFG edges, so this is an honest recall gap **by design**, not a + logic bug. + +Caveat: `own-only 0` also reflects **coverage** — Dapper's core is heavily async and +interprocedural, which we under-analyse, so "found nothing" partly means "didn't +reach it." Telling the two apart needs the extractor's `--stats` (analysed vs +skipped) — the missing signal this run made concrete. + +Net: the oracle did its job. It turned "are we behind?" into a precise map — +precision held (0 FPs; we look *more* correct than Infer# on ownership transfer), +and the recall gap is two named, roadmapped classes (interprocedural escape +tracking, exception-path disposal). + ## Honest gaps (v1) - **No tool versions pinned in the report yet.** `microsoft/infersharpaction@v1.5`