Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 20 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,7 @@ jobs:
frontend/roslyn/samples/CloseReleaseSample.cs \
frontend/roslyn/samples/SemaphoreFieldSample.cs \
frontend/roslyn/samples/VoidSubscribeSample.cs \
frontend/roslyn/samples/ReturnedPublisherSample.cs \
-o "$RUNNER_TEMP/facts.json"
cat "$RUNNER_TEMP/facts.json"
- name: Check facts through the core
Expand Down Expand Up @@ -235,6 +236,25 @@ jobs:
|| { echo "FAIL: expected the lambda-handler subscription leak (warning)"; exit 1; }
echo "$out" | grep -q "inline lambda it has no '-=' handle" \
|| { echo "FAIL: expected the lambda no-handle wording"; exit 1; }
# #146 interprocedural publisher provenance (the Newtonsoft
# Create->ApplySerializerSettings shape): every caller of ApplyBounded
# constructs the publisher and returns it, so the param-publisher
# subscription is bounded -> the extractor stamps
# `source_provenance: "returned_fresh"` and the bridge drops it (SILENT).
grep -q '"source_provenance": "returned_fresh"' "$RUNNER_TEMP/facts.json" \
|| { echo "FAIL: expected the returned_fresh provenance stamp in the facts"; exit 1; }
if echo "$out" | grep -q "publisher.Error"; then
echo "FAIL: the proven returned-fresh publisher subscription must be silent"; exit 1
fi
# ...and every denial case KEEPS the honest OWN001 warning — public
# candidate, mixed callers, field-stored fresh local, the param->param
# DI dual this feature must never silence, and the two local-function
# closure escapes (callee-side capture / caller-side capture, Codex P2).
for ev in "pub.Faulted" "target.Mixed" "stored.Stored" "bus.Changed" \
"deferred.Deferred" "later.Later"; do
echo "$out" | grep -qE "ReturnedPublisherSample\.cs:[0-9]+: warning: \[OWN001\].*'$ev'" \
|| { echo "FAIL: expected the OWN001 warning to survive for '$ev' (provenance must deny)"; exit 1; }
done
# P-004 provenance: a local that ALIASES an injected source (var src =
# _bus) is NOT method-bounded — it must warn, not be silently dropped. A
# local the scope CONSTRUCTS (var owned = new Calc()) IS bounded -> silent.
Expand Down
7 changes: 6 additions & 1 deletion corpus/oracle-fp-baseline.txt
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,12 @@ protobuf-net/protobuf-net | Page.xaml.cs | OWN001 | local 'timer' | non-product
# INSTANCE facts (no ArrayPool set + the sink is a StringWriter), not a type-level no-op, so it stays
# baselined — consistent with excluding writers from IsNoOpDisposeWrapper. See no-op-dispose-wrapper.md.
JamesNK/Newtonsoft.Json | TraceJsonReader.cs | OWN001 | _textWriter | benign-by-instance, NOT a no-op type: JsonTextWriter.Close() returns a (possibly pooled) write buffer and auto-completes JSON tokens; harmless here only because no ArrayPool is set and the sink is a StringWriter — kept baselined (not soundly auto-fixable)
JamesNK/Newtonsoft.Json | JsonSerializer.cs | OWN001 | serializer.Error | intra-call self-subscription: the serializer is freshly created from the same JsonSerializerSettings whose .Error handler it subscribes; source and handler are co-lifetimed
# REMOVED (fixed by #146): `JsonSerializer.cs | OWN001 | serializer.Error` — the
# returned-fresh publisher provenance pass now proves the Create->
# ApplySerializerSettings shape bounded (source_provenance: "returned_fresh") and
# the finding no longer fires. Deliberately NOT left baselined: if the provenance
# pass regresses, the finding must reappear in the triage queue, not be silently
# swallowed by this allowlist. (field-notes #8)

# --- JoshClose/CsvHelper --------------------------------------------------------
JoshClose/CsvHelper | ConsoleHost.cs | OWN014 | AppDomain.CurrentDomain.ProcessExit | non-product (docs-src/ doc-generator) + process-lived subscriber: ConsoleHost itself lives for the whole process, so promoting it to a process-lived event source changes nothing
Expand Down
14 changes: 14 additions & 0 deletions docs/notes/field-notes-patterns.md
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,20 @@ interprocedural (the construct-and-return is in the caller), which is the hard p
The honest interim posture — advisory warning, never a hard error — is already in
place.**

**Status: FIXED (#146).** The extractor now runs a compilation-wide provenance
pass: when a `+=` publisher is a parameter of a private/internal method and
*every* visible caller passes a freshly-constructed local that escapes only into
the call / its own `return` (and the callee never lets the param escape), the
subscription is stamped `source_provenance: "returned_fresh"` and the bridge
drops it (bounded, silent). Any unprovable step — public candidate, method-group
reference, mixed callers, field-stored local, param→param forwarding, or a
local-function closure capture on either side (callee-side `ProvLocalFuncFactory`,
caller-side `ProvCallerLocalFuncFactory` — a stored local function escapes exactly
like a lambda) — denies the proof and the honest warning stands. Pinned by
`frontend/roslyn/samples/ReturnedPublisherSample.cs` (CI `wpf-extractor`) and
the `source_provenance` checks in `tests/test_ownir.py`; spec'd in
`spec/OwnIR.md` §4.

## 9. Owning field whose IDisposable holds no unmanaged resource

**Seen in:** Newtonsoft.Json `Src/Newtonsoft.Json/Serialization/TraceJsonReader.cs:37,38`
Expand Down
31 changes: 20 additions & 11 deletions docs/notes/oracle-known-fps.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ reason: we and the oracles occupy orthogonal niches.

| disposition | count | what happens on re-run |
|---|---:|---|
| **Fixed in the extractor** | 6 | no longer fire (5 NLog `WaitForDispose` timers + protobuf `XsltOptions` self-cycle — see below) |
| **Baselined FP** | 5 | moved to "Known FP (baselined)", out of the triage queue |
| **Fixed in the extractor** | 7 | no longer fire (5 NLog `WaitForDispose` timers + protobuf `XsltOptions` self-cycle + Newtonsoft `serializer.Error` returned-fresh provenance, #146 — see below) |
| **Baselined FP** | 4 | moved to "Known FP (baselined)", out of the triage queue |
| **Non-product (path filter)** | 2 | dropped by `--exclude-tests` (`unittest` rule) |
| **True positive — kept visible** | 4 | stays in "Own.NET only" (real catch, oracle can't express) |
| **True-but-benign — kept, baselined-as-sample** | 3 | (protobuf `assorted/` samples) baselined as non-product |
Expand All @@ -33,21 +33,30 @@ reason: we and the oracles occupy orthogonal niches.
"True-but-benign sample" 2→3 — it is a real leak of a custom `IDisposable`
`Nuxleus.Performance.Stopwatch`, not the BCL non-disposable type first assumed.)

The 5 baselined FPs + the 3 non-product-sample reals = 8 findings, covered by
**7 rules** in `corpus/oracle-fp-baseline.txt` (the two `NetTranscoder` copies
share one basename-keyed rule); the 2 test-base findings are the `--exclude-tests`
drops; the 4 true positives are deliberately **not** suppressed.
The 4 baselined FPs + the 3 non-product-sample reals = 7 findings, covered by
**6 rules** in `corpus/oracle-fp-baseline.txt` (the two `NetTranscoder` copies
share one basename-keyed rule; the Newtonsoft `serializer.Error` rule was removed
when #146 fixed it at the source); the 2 test-base findings are the
`--exclude-tests` drops; the 4 true positives are deliberately **not** suppressed.

**Update (extractor fix landed — protobuf self-cycle).** `CommandLineOptions.XsltOptions.
XsltMessageEncountered` — a `this`-capturing handler subscribed to an event on
`XsltOptions`, a get-only property over a constructed field the class owns — is now
**fixed at the source** by `PropertyReturnsOwnedMember` (the self-owned-source exemption
now covers a property receiver, not just `this`/fields/locals). A live protobuf re-run
confirmed it: own-only **0**, the finding absent from own-only and baselined. See
root-cause #3. Corpus fixture: `subscription-self-owned-property`. Newtonsoft's
`serializer.Error` stays baselined — its source escapes (a returned `Create()` result)
and the handler is a parameter's delegate, so proving non-leak needs lifetime modelling;
the "may outlive" warning is honest, not a clear FP.
root-cause #3. Corpus fixture: `subscription-self-owned-property`.

**Update (#146 landed).** Newtonsoft's `serializer.Error` is now **fixed at the
source** too: the extractor's compilation-wide returned-fresh publisher provenance
pass proves the `Create` → `ApplySerializerSettings` shape bounded
(`source_provenance: "returned_fresh"`) and the bridge drops it. Its baseline
entry is removed (deliberately — a regression must reappear in triage, not be
swallowed by the allowlist). Pinned by
`frontend/roslyn/samples/ReturnedPublisherSample.cs`; denial cases (public
candidate, mixed callers, field-stored local, param→param DI forwarding, and the
two local-function closure captures — callee-side `ProvLocalFuncFactory` and
caller-side `ProvCallerLocalFuncFactory`) keep the honest warning.

**Update (extractor fix landed — all NLog timers).** All 5 of the original NLog
`WaitForDispose` timer FPs are now **fixed at the source**, baseline entries deleted.
Expand Down Expand Up @@ -114,7 +123,7 @@ visible.
| location | verdict | why |
|---|---|---|
| `TraceJsonReader.cs` `_textWriter` | **FP → baseline** | no-op dispose: a `JsonTextWriter` over an in-memory `StringWriter`/`StringBuilder` holds no unmanaged resource |
| `JsonSerializer.cs` `serializer.Error` | **FP → baseline** | intra-call self-subscription: the serializer is freshly built from the same `JsonSerializerSettings` whose `.Error` it subscribes; co-lifetimed |
| `JsonSerializer.cs` `serializer.Error` | **FP → fixed (#146)** | intra-call self-subscription: the serializer is freshly built from the same `JsonSerializerSettings` whose `.Error` it subscribes; co-lifetimed. Now proven bounded by the returned-fresh publisher provenance pass; baseline entry removed |

### JoshClose/CsvHelper — 2 findings

Expand Down
Loading
Loading