Skip to content

Commit 081b68e

Browse files
PhysShellclaude
PhysShell
and
claude
committed
docs(evidence): N1-F0 oracle frozen before the real-file run; F0-A collector
Oracle (rules 1-3, defect rule) with "disposes r" operationalised in the header; one control-driven fix (a dispose of r inside the catch is not a throwing site, control N6). Controls: N1-N9 silent, P-R/P-B/P-X reported. F0-A collector script (method spans, interprocedural kinds). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TFkNAFFQz9KoTzpPws8vYG
1 parent 66731cc commit 081b68e

4 files changed

Lines changed: 454 additions & 0 deletions

File tree

‎docs/evidence/n1-f0-2026-10/data/f0b_controls.tsv‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
group file type method acq_line acq handover_line kind dispose_evidence throw_line throw_site
2+
controls OwnershipControls.cs Holder P_R 130 Remote.CreateAsync(k) 132 1b _owned[] 154: v.DisposeAsync() 131 await c.PingAsync()
3+
controls OwnershipControls.cs Holder P_B 138 _conn.OpenAsync() 140 1b _owned[] 154: v.DisposeAsync() 139 await ch.PingAsync()
4+
controls OwnershipControls.cs Holder P_X 146 Remote.CreateAsync("x") 148 1c Wrap Wrap._inner disposed at 28: _inner.DisposeAsync() 147 await StepAsync()

‎docs/evidence/n1-f0-2026-10/oracle/F0Oracle.csproj‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
<Project Sdk="Microsoft.NET.Sdk">
2+
<!-- N1-F0 ownership oracle (research only). No PackageReference: Roslyn comes from the e7d33e33 extractor build
3+
(pass -p:RoslynDir=<dir with Microsoft.CodeAnalysis*.dll>), so restore needs no package feed. -->
4+
<PropertyGroup>
5+
<OutputType>Exe</OutputType>
6+
<TargetFramework>net10.0</TargetFramework>
7+
<Nullable>enable</Nullable>
8+
<ImplicitUsings>enable</ImplicitUsings>
9+
<AssemblyName>f0oracle</AssemblyName>
10+
</PropertyGroup>
11+
<ItemGroup>
12+
<Reference Include="Microsoft.CodeAnalysis"><HintPath>$(RoslynDir)/Microsoft.CodeAnalysis.dll</HintPath></Reference>
13+
<Reference Include="Microsoft.CodeAnalysis.CSharp"><HintPath>$(RoslynDir)/Microsoft.CodeAnalysis.CSharp.dll</HintPath></Reference>
14+
</ItemGroup>
15+
</Project>

‎docs/evidence/n1-f0-2026-10/oracle/Program.cs‎

Lines changed: 280 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,280 @@
1+
// N1-F0 part B: ownership oracle (00-preregistration.md, F0-B). Research only, throwaway.
2+
//
3+
// usage: f0oracle --refs <dir> [--refs <dir>] --group <name>=<file>[;<file>...] [--group ...] --out out.tsv
4+
//
5+
// A call result r acquired in method M of type T is OWNED when (rules 1-3 of the pre-registration):
6+
// 1. M hands r over on the success path to (a) a field f of T, (b) an element of a collection field f
7+
// (indexer store, Add, TryAdd), or (c) a constructor argument of an in-source type W whose ctor stores
8+
// it in a field g of W, the W instance being returned or stored as in (a)/(b);
9+
// 2. the same type (T, or W for (c)) disposes that target: Dispose/DisposeAsync/Close/CloseAsync on f/g,
10+
// on a local taken from f (TryRemove/Remove out, indexer read, foreach over f or f.Values), or
11+
// using/await using of one of those;
12+
// 3. the acquisition is not a borrow (IServiceProvider.GetService and friends).
13+
// DEFECT: a throwing site (any invocation or await, except nameof/typeof) lies between the acquisition and
14+
// the hand-over, and no enclosing try disposes r in its catch or finally.
15+
// "Disposes r" is operationalised (fixed before the first run on real files) as any of:
16+
// - Dispose/DisposeAsync/Close/CloseAsync on r (also r?.X);
17+
// - the same call on `new W(r)` where W is an owning wrapper by rules 1c+2;
18+
// - r passed to a method of T whose body disposes the corresponding parameter (one hop).
19+
using Microsoft.CodeAnalysis;
20+
using Microsoft.CodeAnalysis.CSharp;
21+
using Microsoft.CodeAnalysis.CSharp.Syntax;
22+
23+
var refDirs = new List<string>();
24+
var groups = new List<(string Name, string[] Files)>();
25+
string? outPath = null;
26+
for (var i = 0; i < args.Length; i++)
27+
{
28+
switch (args[i])
29+
{
30+
case "--refs": refDirs.Add(args[++i]); break;
31+
case "--group":
32+
var g = args[++i].Split('=', 2);
33+
groups.Add((g[0], g[1].Split(';')));
34+
break;
35+
case "--out": outPath = args[++i]; break;
36+
default: throw new ArgumentException(args[i]);
37+
}
38+
}
39+
var refs = refDirs.SelectMany(d => Directory.EnumerateFiles(d, "*.dll"))
40+
.Select(p => (MetadataReference)MetadataReference.CreateFromFile(p)).ToList();
41+
var rows = new List<string> { "group\tfile\ttype\tmethod\tacq_line\tacq\thandover_line\tkind\tdispose_evidence\tthrow_line\tthrow_site" };
42+
foreach (var (name, files) in groups)
43+
{
44+
var trees = files.Select(f => CSharpSyntaxTree.ParseText(File.ReadAllText(f),
45+
new CSharpParseOptions(LanguageVersion.Preview), Path.GetFileName(f))).ToList();
46+
var comp = CSharpCompilation.Create(name, trees, refs,
47+
new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary));
48+
var o = new Oracle(comp);
49+
foreach (var t in trees) o.Run(t);
50+
foreach (var f in o.Findings) rows.Add(name + "\t" + f);
51+
Console.Error.WriteLine($"{name}: {o.Findings.Count} findings, {o.OwnedAcquisitions} owned acquisitions, {o.Acquisitions} call acquisitions");
52+
}
53+
File.WriteAllLines(outPath ?? "f0b.tsv", rows);
54+
foreach (var r in rows) Console.WriteLine(r);
55+
return 0;
56+
57+
sealed class Oracle(CSharpCompilation comp)
58+
{
59+
public readonly List<string> Findings = new();
60+
public int Acquisitions, OwnedAcquisitions;
61+
62+
static readonly HashSet<string> DisposeNames = new() { "Dispose", "DisposeAsync", "Close", "CloseAsync" };
63+
static readonly HashSet<string> BorrowNames = new()
64+
{ "GetService", "GetRequiredService", "GetServices", "GetKeyedService", "GetRequiredKeyedService", "GetKeyedServices", "GetServiceOrCreateInstance" };
65+
static readonly HashSet<string> StoreNames = new() { "Add", "TryAdd", "AddOrUpdate", "GetOrAdd", "Enqueue", "Push" };
66+
67+
static int Line(SyntaxNode n) => n.GetLocation().GetLineSpan().StartLinePosition.Line + 1;
68+
static string Snip(SyntaxNode n)
69+
{
70+
var s = string.Join(' ', n.ToString().Split((char[])['\r', '\n', '\t'], StringSplitOptions.RemoveEmptyEntries).Select(x => x.Trim()));
71+
return s.Length > 90 ? s[..90] + "…" : s;
72+
}
73+
74+
static ExpressionSyntax Strip(ExpressionSyntax e)
75+
{
76+
while (true)
77+
{
78+
switch (e)
79+
{
80+
case AwaitExpressionSyntax a: e = a.Expression; continue;
81+
case ParenthesizedExpressionSyntax p: e = p.Expression; continue;
82+
case PostfixUnaryExpressionSyntax { RawKind: (int)SyntaxKind.SuppressNullableWarningExpression } pu: e = pu.Operand; continue;
83+
case InvocationExpressionSyntax { Expression: MemberAccessExpressionSyntax { Name.Identifier.Text: "ConfigureAwait" } ma }: e = ma.Expression; continue;
84+
default: return e;
85+
}
86+
}
87+
}
88+
89+
static string? InvokedName(InvocationExpressionSyntax inv) => inv.Expression switch
90+
{
91+
MemberAccessExpressionSyntax ma => ma.Name.Identifier.Text,
92+
SimpleNameSyntax s => s.Identifier.Text,
93+
MemberBindingExpressionSyntax mb => mb.Name.Identifier.Text,
94+
_ => null,
95+
};
96+
97+
// the root identifier of a receiver / expression (x in x.a.b, this.x, x?.y)
98+
static string? RootName(ExpressionSyntax e)
99+
{
100+
while (true)
101+
{
102+
switch (e)
103+
{
104+
case MemberAccessExpressionSyntax { Expression: ThisExpressionSyntax } m: return m.Name.Identifier.Text;
105+
case MemberAccessExpressionSyntax m: e = m.Expression; continue;
106+
case ConditionalAccessExpressionSyntax c: e = c.Expression; continue;
107+
case ElementAccessExpressionSyntax ea: e = ea.Expression; continue;
108+
case ParenthesizedExpressionSyntax p: e = p.Expression; continue;
109+
case PostfixUnaryExpressionSyntax pu: e = pu.Operand; continue;
110+
case IdentifierNameSyntax id: return id.Identifier.Text;
111+
default: return null;
112+
}
113+
}
114+
}
115+
116+
// receiver of a dispose-family call: `x.Dispose()`, `x?.Dispose()`, `(expr).DisposeAsync()`
117+
static ExpressionSyntax? DisposeReceiver(InvocationExpressionSyntax inv)
118+
{
119+
if (inv.Expression is MemberAccessExpressionSyntax ma && DisposeNames.Contains(ma.Name.Identifier.Text)) return ma.Expression;
120+
if (inv.Expression is MemberBindingExpressionSyntax mb && DisposeNames.Contains(mb.Name.Identifier.Text)
121+
&& inv.Parent is ConditionalAccessExpressionSyntax ca) return ca.Expression;
122+
return null;
123+
}
124+
125+
static IEnumerable<InvocationExpressionSyntax> DisposeCalls(SyntaxNode n) =>
126+
n.DescendantNodesAndSelf().OfType<InvocationExpressionSyntax>().Where(i => DisposeReceiver(i) is not null);
127+
128+
// Rule 2: does type `decl` dispose field `field` (directly, via a local taken from it, or via using)?
129+
string? DisposesField(TypeDeclarationSyntax decl, string field)
130+
{
131+
var fromField = new HashSet<string>();
132+
foreach (var arg in decl.DescendantNodes().OfType<ArgumentSyntax>())
133+
{
134+
if (arg.Expression is DeclarationExpressionSyntax { Designation: SingleVariableDesignationSyntax sv }
135+
&& arg.Parent?.Parent is InvocationExpressionSyntax inv && InvokedName(inv) is "TryRemove" or "Remove" or "TryGetValue" or "TryDequeue" or "TryPop" or "TryTake"
136+
&& inv.Expression is MemberAccessExpressionSyntax ma && RootName(ma.Expression) == field)
137+
fromField.Add(sv.Identifier.Text);
138+
}
139+
foreach (var v in decl.DescendantNodes().OfType<VariableDeclaratorSyntax>())
140+
if (v.Initializer?.Value is ElementAccessExpressionSyntax ea && RootName(ea.Expression) == field) fromField.Add(v.Identifier.Text);
141+
foreach (var fe in decl.DescendantNodes().OfType<ForEachStatementSyntax>())
142+
if (RootName(fe.Expression) == field) fromField.Add(fe.Identifier.Text);
143+
foreach (var call in DisposeCalls(decl))
144+
{
145+
var root = RootName(DisposeReceiver(call)!);
146+
if (root == field || (root is not null && fromField.Contains(root))) return $"{Line(call)}: {Snip(call)}";
147+
}
148+
foreach (var u in decl.DescendantNodes().OfType<LocalDeclarationStatementSyntax>().Where(l => l.UsingKeyword != default))
149+
foreach (var v in u.Declaration.Variables)
150+
if (v.Initializer?.Value is { } init && (RootName(init) == field || (RootName(init) is { } r && fromField.Contains(r))))
151+
return $"{Line(u)}: {Snip(u)}";
152+
return null;
153+
}
154+
155+
bool IsField(TypeDeclarationSyntax decl, string name) =>
156+
decl.Members.OfType<FieldDeclarationSyntax>().Any(f => f.Declaration.Variables.Any(v => v.Identifier.Text == name))
157+
|| decl.Members.OfType<PropertyDeclarationSyntax>().Any(p => p.Identifier.Text == name);
158+
159+
// Rule 1c: in-source wrapper type W whose ctor stores parameter #i into a field g that W disposes.
160+
(TypeDeclarationSyntax W, string Evidence)? OwningWrapper(ObjectCreationExpressionSyntax oc, int argIndex)
161+
{
162+
var tn = oc.Type switch { IdentifierNameSyntax i => i.Identifier.Text, QualifiedNameSyntax q => q.Right.Identifier.Text, _ => null };
163+
if (tn is null) return null;
164+
foreach (var tree in comp.SyntaxTrees)
165+
foreach (var w in tree.GetRoot().DescendantNodes().OfType<TypeDeclarationSyntax>().Where(t => t.Identifier.Text == tn))
166+
foreach (var ctor in w.Members.OfType<ConstructorDeclarationSyntax>())
167+
{
168+
if (argIndex >= ctor.ParameterList.Parameters.Count) continue;
169+
var p = ctor.ParameterList.Parameters[argIndex].Identifier.Text;
170+
foreach (var asg in ctor.DescendantNodes().OfType<AssignmentExpressionSyntax>())
171+
if (asg.Right is IdentifierNameSyntax { Identifier.Text: var rp } && rp == p && RootName(asg.Left) is { } g && IsField(w, g)
172+
&& DisposesField(w, g) is { } ev)
173+
return (w, $"{tn}.{g} disposed at {ev}");
174+
}
175+
return null;
176+
}
177+
178+
public void Run(SyntaxTree tree)
179+
{
180+
foreach (var decl in tree.GetRoot().DescendantNodes().OfType<TypeDeclarationSyntax>())
181+
foreach (var m in decl.Members.OfType<MethodDeclarationSyntax>())
182+
if (m.Body is not null) Scan(decl, m);
183+
}
184+
185+
void Scan(TypeDeclarationSyntax T, MethodDeclarationSyntax M)
186+
{
187+
// acquisitions: `var r = <call>` or `r = <call>`, the call possibly awaited
188+
var acqs = new List<(string R, SyntaxNode Stmt, InvocationExpressionSyntax Call)>();
189+
foreach (var v in M.Body!.DescendantNodes().OfType<VariableDeclaratorSyntax>())
190+
if (v.Initializer?.Value is { } init && Strip(init) is InvocationExpressionSyntax inv)
191+
acqs.Add((v.Identifier.Text, v, inv));
192+
foreach (var a in M.Body.DescendantNodes().OfType<AssignmentExpressionSyntax>())
193+
if (a.Left is IdentifierNameSyntax id && Strip(a.Right) is InvocationExpressionSyntax inv2
194+
&& M.Body.DescendantNodes().OfType<VariableDeclaratorSyntax>().Any(v => v.Identifier.Text == id.Identifier.Text))
195+
acqs.Add((id.Identifier.Text, a, inv2));
196+
foreach (var (r, stmt, call) in acqs)
197+
{
198+
if (InvokedName(call) is { } nm && (BorrowNames.Contains(nm) || nm is "nameof")) continue; // rule 3
199+
Acquisitions++;
200+
var after = stmt.Span.End;
201+
// rule 1: hand-over target on the success path, after the acquisition
202+
SyntaxNode? hand = null; string? kind = null; string? ev = null;
203+
foreach (var n in M.Body.DescendantNodes().Where(n => n.SpanStart >= after))
204+
{
205+
if (n is AssignmentExpressionSyntax { Right: var rhs } asg && Strip(rhs) is IdentifierNameSyntax { Identifier.Text: var rr } && rr == r)
206+
{
207+
if (asg.Left is ElementAccessExpressionSyntax ea && RootName(ea.Expression) is { } cf && IsField(T, cf) && DisposesField(T, cf) is { } e1)
208+
{ hand = asg; kind = $"1b {cf}[]"; ev = e1; break; }
209+
if (asg.Left is IdentifierNameSyntax or MemberAccessExpressionSyntax && RootName(asg.Left) is { } ff && ff != r && IsField(T, ff) && DisposesField(T, ff) is { } e2)
210+
{ hand = asg; kind = $"1a {ff}"; ev = e2; break; }
211+
}
212+
if (n is InvocationExpressionSyntax si && InvokedName(si) is { } sn && StoreNames.Contains(sn)
213+
&& si.Expression is MemberAccessExpressionSyntax sma && RootName(sma.Expression) is { } sf && IsField(T, sf)
214+
&& si.ArgumentList.Arguments.Any(x => Strip(x.Expression) is IdentifierNameSyntax { Identifier.Text: var ar } && ar == r)
215+
&& DisposesField(T, sf) is { } e3)
216+
{ hand = si; kind = $"1b {sf}.{sn}"; ev = e3; break; }
217+
if (n is ObjectCreationExpressionSyntax oc && oc.ArgumentList is { } al)
218+
{
219+
var idx = al.Arguments.ToList().FindIndex(x => Strip(x.Expression) is IdentifierNameSyntax { Identifier.Text: var ar } && ar == r);
220+
if (idx >= 0 && OwningWrapper(oc, idx) is { } w
221+
&& (oc.Parent is ReturnStatementSyntax || (oc.Parent is AssignmentExpressionSyntax pa && RootName(pa.Left) is { } wf && IsField(T, wf))))
222+
{ hand = oc; kind = $"1c {w.W.Identifier.Text}"; ev = w.Evidence; break; }
223+
}
224+
}
225+
if (hand is null) continue;
226+
OwnedAcquisitions++;
227+
// defect: a throwing site strictly between the acquisition and the hand-over, not covered by a disposing try
228+
var throwing = M.Body.DescendantNodes()
229+
.Where(n => n.SpanStart >= after && n.Span.End <= hand.SpanStart)
230+
.Where(n => n is InvocationExpressionSyntax inv3 ? InvokedName(inv3) is not ("nameof") : n is AwaitExpressionSyntax)
231+
.Where(n => !n.Ancestors().Any(a => a == hand))
232+
// disposing r cannot leak r (control N6: the dispose inside the catch)
233+
.Where(n => !(Strip(n is AwaitExpressionSyntax aw ? aw.Expression : (ExpressionSyntax)n) is InvocationExpressionSyntax di
234+
&& DisposeReceiver(di) is { } dr && RootName(dr) == r))
235+
.FirstOrDefault(n => !CoveredByDisposingTry(T, n, r, M));
236+
if (throwing is null) continue;
237+
Findings.Add(string.Join('\t', T.SyntaxTree.FilePath, T.Identifier.Text, M.Identifier.Text, Line(stmt), Snip(call),
238+
Line(hand), kind, ev, Line(throwing), Snip(throwing)));
239+
}
240+
}
241+
242+
bool CoveredByDisposingTry(TypeDeclarationSyntax T, SyntaxNode site, string r, MethodDeclarationSyntax M)
243+
{
244+
foreach (var tr in site.Ancestors().OfType<TryStatementSyntax>())
245+
{
246+
if (!tr.Block.Span.Contains(site.Span)) continue;
247+
var cleanup = tr.Catches.Select(c => (SyntaxNode)c.Block).Concat(tr.Finally is { } f ? new SyntaxNode[] { f.Block } : []);
248+
if (cleanup.Any(b => DisposesLocal(T, b, r))) return true;
249+
}
250+
return false;
251+
}
252+
253+
bool DisposesLocal(TypeDeclarationSyntax T, SyntaxNode block, string r)
254+
{
255+
foreach (var call in DisposeCalls(block))
256+
{
257+
var recv = DisposeReceiver(call)!;
258+
if (RootName(recv) == r) return true;
259+
if (recv is ObjectCreationExpressionSyntax oc && oc.ArgumentList is { } al)
260+
{
261+
var idx = al.Arguments.ToList().FindIndex(x => Strip(x.Expression) is IdentifierNameSyntax { Identifier.Text: var ar } && ar == r);
262+
if (idx >= 0 && OwningWrapper(oc, idx) is not null) return true;
263+
}
264+
}
265+
// one hop: r passed to a method of T whose body disposes that parameter
266+
foreach (var inv in block.DescendantNodes().OfType<InvocationExpressionSyntax>())
267+
{
268+
if (inv.Expression is not IdentifierNameSyntax callee) continue;
269+
var idx = inv.ArgumentList.Arguments.ToList().FindIndex(x => Strip(x.Expression) is IdentifierNameSyntax { Identifier.Text: var ar } && ar == r);
270+
if (idx < 0) continue;
271+
foreach (var md in T.Members.OfType<MethodDeclarationSyntax>().Where(x => x.Identifier.Text == callee.Identifier.Text))
272+
{
273+
if (idx >= md.ParameterList.Parameters.Count) continue;
274+
var p = md.ParameterList.Parameters[idx].Identifier.Text;
275+
if (DisposeCalls(md).Any(c => RootName(DisposeReceiver(c)!) == p)) return true;
276+
}
277+
}
278+
return false;
279+
}
280+
}

0 commit comments

Comments
 (0)