Repository navigation
ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380
Description
Summary
Current Roslyn lowering treats a first-party parameter as consumed when the callee contains any immediate Dispose/Close of that parameter. It does not account for a parameter guard that controls that release.
This violates INF-S2 (spec/Inference.md L89). INF-S2 requires a partial release to stay may rather than become a fabricated must, and says that flattening a partial release to must "would charge a caller's defensive dispose a false OWN002/OWN003 — the precision floor forbids it."
This issue is about conformance to the existing INF-S2 precision floor. It does not require or authorize a P-037 implementation (#304 stays FROZEN).
Mechanism (at 23e3203)
In frontend/roslyn/OwnSharp.Extractor/Program.cs:
- L4164:
ConsumeReleaseArgs(expr, model). Every argument it returns is emitted asreleaseat the call site. - L4902
ConsumeReleaseArgscalls L4959ConsumesParam, which calls L4999DisposesLocal. DisposesLocalreturns true on any immediatename.Dispose()/Close()/DisposeAsync()anywhere in the callee body. No guard check is made;IsParamGuardedReleaseis used only for teardown crediting.
The fabricated release is emitted before either engine sees a fact. Rust and Python agree byte-for-byte, so this is a frontend/lowering defect, not an engine divergence.
Reproduced on pinned real code (dotnet/runtime@49e04fa0)
SymmetricCngTestHelpers.VerifyPersistedKey(..., disposeKey: false), called from two real call sites (SymmetricCngTestHelpers.csL51 and L370). The callee disposeskeyonly underif (disposeKey).- The call is lowered as
release cngKey. - The caller's later
cngKey.Delete()then reads as a use after release. - Result: false
OWN009("may be used after disposal on some path") atSymmetricCngTestHelpers.cs:36and:355, on both engines.
- The call is lowered as
ArgumentSource.GetArguments(reader, false)(src/mono/wasm/host/Options.csL675; the callee disposes only underif (close)).- The call is lowered as
release reader. - The public wrapper
GetArguments(TextReader)then exports a falsemusttransfer summary for its caller's reader (summariesdump). This corrupts an interprocedural contract, not just one warning.
- The call is lowered as
In the same extracted facts, the A2.1 guarded sidecar correctly records bool_const false at the guard parameter (param 7 for VerifyPersistedKey, param 1 for GetArguments). The guard information is available; the authoritative lowering path discards it.
Setup: Own.NET 23e3203 unmodified, .NET SDK 8.0.425, ownsharp-extract --flow-locals over the exact pinned files, then own-cli ownir and python -m ownlang ownir (--severity warning --verbosity verbose).
Evidence (Own.NET-paperwork, commit d4e98f2)
- Results:
paper-eval/oss-sixcase-observation-results-v1.json - Manifest:
paper-eval/manifests/oss-sixcase-observation-v1.sha256 - Raw facts and engine output,
VerifyPersistedKey:case4/facts.R0.json,case4/rust.R0.out,case4/py.R0.out - Raw facts and summaries,
GetArguments:case5/facts.R0.json,case5/summaries.R0.json
Relation to what is already on record
The mechanism itself is not new. The A1.1 fact-surface diagnosis on #304 (comment) named ConsumesParam as flattening may to must. The corpus/p036-bakeoff/gv4-control-* controls (scripts/p037_controls.py) pin the fabricated call-site release as the current record.
What this issue adds:
- real-world witnesses on pinned upstream code;
- framing as a violation of the analyzer's own current contract (INF-S2), which stands independently of P-037.
Fix-direction caveat (for whoever picks this up)
Making ConsumesParam answer "not consumed" for a guarded release is not INF-S2-conformant on its own. The argument would then lower to a plain use, i.e. no. That fabricates the opposite verdict: a false OWN001 at callers that rely on the callee's release, such as disposeKey: true or Teardown(false).
INF-S2 conformance means may, which lowers to plain + OWN051 at the call (INF-A1/INF-A5). How the frontend should hand that to the core is a design question. It sits close to #304 reopen condition 1, which is the owner's call, not this issue's.
Activity
Record the #380 baseline transition for the P-037 controls and fact s…
docs(#380): scope the definiteness comment and pin the dynamic-forwar…
Merge pull request #381 from PhysShell/ccr-d1573cc1-g41e75
P-037-X Stage 1: re-record the census, the controls and the #380 pins…
P-037-X Stage 2: replay the frozen P-037 unchanged on canonical calls…
P-037-X Stage 2b: the stage note (EXPLORATORY, research branch)