Skip to content

Commit e524972

Browse files
docs(h28): resolve the DbCommand residual — H28-PROVIDER-SPECIFIC
H-28 (research/ownership-semantics-lab-v1 @ 298b305, not on main) settled DataTable.Load(reader) with a runtime falsifier: the reader IS closed, so the presumed BORROW was refuted and the demanding instance (victor-wiki/DatabaseManager DbInterpreter.GetDataTableAsync:699) is not a protocol leak. The same record then wrote one sentence and never classified it: "what remains is the never-disposed DbCommand `cmd` (an object leak without a protocol consequence)" That sentence is a description, not a verdict: it was never falsified, never entered the witnessed-callee table, never reached a gate. This closes it. VERDICT: H28-PROVIDER-SPECIFIC. The absence of DbCommand.Dispose() in this family is not one fact. * Npgsql 10.0.3 (and main, identical): NpgsqlCommand has no finalizer, both ctors GC.SuppressFinalize, and Dispose(bool) only nulls _transaction, sets a managed state flag and optionally recycles the command into the connection's one-slot CachedCommand. Reset() is managed-only. Server-side prepared statements belong to NpgsqlConnector.PreparedStatementManager and are never DEALLOCATEd by the command. => releases nothing. * Microsoft.Data.SqlClient, MySqlConnector: managed-only Dispose, no finalizer. => releases nothing. * Microsoft.Data.Sqlite: SqliteCommand.Dispose -> DisposePreparedStatements finalizes native sqlite3_stmt SafeHandles (ReleaseHandle -> sqlite3_finalize) AND disposes its reader. A plain ExecuteReader() runs PrepareAndEnumerateStatements(), which puts those handles on the COMMAND; SqliteDataReader.Close()/Dispose() does not finalize them. => the command is the only deterministic releaser. REAL defect. So the old residual is true for Npgsql and false for Microsoft.Data.Sqlite; it was written from a two-provider falsifier whose SQLite arm never looked at the command. Sharper witness found on the way (pivot recorded in the report): the ownership relation connection -> command -> reader is not what either side assumes. NpgsqlCommand.CurrentActivity (System.Diagnostics.Activity IS IDisposable in .NET 8 and 10) is stopped by exactly two call sites repo-wide, both in NpgsqlDataReader.Dispose/DisposeAsync -> Command.TraceCommandStop(). Neither NpgsqlDataReader.Close() nor NpgsqlCommand.Dispose() calls it — and DataTable.Load calls Close(). With a tracing listener attached the span never ends. Meanwhile reader Cleanup sets Command.State = Idle, which makes the command reusable: that is not ownership. CURRENT OWN.NET (extractor @ e889f8b, source-derived; engine executed): IsOwningFactory mints an owned local for IDbConnection.CreateCommand() (L4880-4882 -> L7035), IsDisposeOptional does not cover DbCommand (L2593), and the argument-escape rule untracks the reader at table.Load(reader) (L7155-7182). Predicted: OWN001 (error) on `command`, silence on `reader`. The engine half reproduces exactly that (evidence/engine-CommandDispose.txt: 2x command in B/E + 1x reader in E, A/D clean). On Npgsql with tracing on the verdict is inverted — error on the object whose Dispose frees nothing, silence on the one whose disposal is load-bearing. The escape drop is also only accidentally right: DataTable.Load closes the reader IFF !reader.NextResult(), so a multi-result-set reader is left OPEN and the drop is a false negative there. NO PRODUCTION CHANGE. Nothing here touches the extractor, the core, the vocabulary or a diagnostic. corpus/ownership-lab/ is not globbed by tests/test_corpus.py (still 33/33). The model gap is shown to be an instance of #382 — which already names this lowering and this exact loss — with proven_call (OwnIR v2, H1) as the landed transport precedent; section 10 proposes the smallest experiment and explicitly not a lattice, a new code, or provider special-casing. Deliverables: docs/notes/h28-npgsql-command-resolution.md plus corpus/ownership-lab/h28-command/ — fx/CommandDispose.cs (9 variants, abstract ADO.NET types on purpose: that is what IsOwningFactory matches), a runnable falsifier pinned to net8.0/Npgsql 10.0.3/MS.Data.Sqlite 10.0.12 with probes P1-P6 each chosen to separate two hypotheses, and 32 source citations auto-derived from pinned refs (blob sha + sha256 + line range) by scripts/derive_source_evidence.py, which exits non-zero when the note goes stale. Honest limits, stated in the report rather than papered over: there is no .NET SDK and no reachable NuGet feed in the producing sandbox, so the Roslyn extractor and the runtime falsifier were NOT executed. fx/CommandDispose.cs expectations and probes P2/P4/P6 are marked PREDICTED; run.sh runtime prints SKIP-WHY instead of faking it. What WAS executed: the engine half, all 32 source derivations, and a live PostgreSQL 16.2 (pgserver) used to pin that prepared statements and cursors are session-scoped — independently corroborating that no command-level Dispose can be their releaser. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
1 parent e889f8b commit e524972

42 files changed

Lines changed: 2262 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
H-28-CMD: the DbCommand half of the `DataTable.Load(reader)` family.
2+
3+
WHAT THIS IS
4+
The original H-28 (corpus/ownership-lab/h28/, on the research branch
5+
research/ownership-semantics-lab-v1 at 298b305 -- NOT on main) asked about argument
6+
ownership transfer. Its runtime falsifier settled `DataTable.Load(reader)`: the reader IS
7+
closed (RELEASE_IF_LAST_RESULT_SET, not BORROW). The same record then wrote down one
8+
sentence and never classified it:
9+
10+
"what remains is the never-disposed DbCommand `cmd` (an object leak without a
11+
protocol consequence)"
12+
-- h28/scripts/h28_anchors_record.py, consequence_for_the_demanding_instance
13+
14+
This directory closes that sentence. Read docs/notes/h28-npgsql-command-resolution.md.
15+
16+
Verdict: H28-PROVIDER-SPECIFIC. Not disposing the command is a real resource defect on
17+
Microsoft.Data.Sqlite and releases nothing on Npgsql / Microsoft.Data.SqlClient /
18+
MySqlConnector. Details, citations and falsifiers are in the report.
19+
20+
LAYOUT
21+
fx/CommandDispose.cs the fixture, 9 methods (A/B/C/D + 5 controls), written against the
22+
ABSTRACT ADO.NET types on purpose -- that is what the extractor's
23+
IsOwningFactory matches, so one fixture shows the analyzer's verdict
24+
for every provider at once. Expectations are marked PREDICTED: the
25+
Roslyn extractor was not runnable where this was produced.
26+
fx/CommandDispose.own the ENGINE-RUNNABLE reduction of the same family. Needs only
27+
python3. This half WAS executed; see evidence/.
28+
falsifier/Program.cs the runtime falsifier: probes P1-P6 over variants A/B/C/D.
29+
falsifier/h28cmd.csproj net8.0, Npgsql 10.0.3, Microsoft.Data.Sqlite 10.0.12 -- the exact
30+
versions of the original H-28 falsifier, so the two runs compare.
31+
run.sh driver. `engine` always runs; `runtime` prints SKIP-WHY and exits 0
32+
when there is no .NET SDK / NuGet / PostgreSQL, rather than faking it.
33+
scripts/derive_source_evidence.py
34+
re-fetches all 31 pinned source citations and rewrites evidence/.
35+
Non-zero exit = the report's source arm is stale.
36+
evidence/*.txt the artifacts every claim in the report cites. Each carries repo,
37+
ref, path, git blob sha, file sha256 and the extracted line range,
38+
so a quotation is checkable against git rather than against memory.
39+
40+
REPRODUCE
41+
corpus/ownership-lab/h28-command/run.sh engine # python3 only; ~1s
42+
corpus/ownership-lab/h28-command/run.sh runtime # needs .NET 8 SDK + NuGet + PostgreSQL
43+
python3 corpus/ownership-lab/h28-command/scripts/derive_source_evidence.py
44+
45+
The runtime half starts PostgreSQL itself via pgserver (PyPI, self-contained PostgreSQL 16 on
46+
a Unix socket) -- the same harness the original H-28 falsifier used -- or takes H28_PG_DSN.
47+
48+
WHAT WAS AND WAS NOT EXECUTED WHERE THIS WAS PRODUCED
49+
executed : the engine half (evidence/engine-CommandDispose.txt), the source derivation of
50+
all 31 citations (evidence/*.txt + MANIFEST.txt), a live PostgreSQL 16.2 via
51+
pgserver (used only for the server-side lifecycle checks quoted in the report).
52+
NOT executed: the Roslyn extractor (no .NET SDK, no NuGet feed) and the runtime falsifier
53+
(same). fx/CommandDispose.cs expectations and falsifier probes P2/P4/P6 are
54+
therefore PREDICTED from source, and the report says so at each one.
55+
56+
NO PRODUCTION CHANGE
57+
Nothing here alters the extractor, the core, the vocabulary or any diagnostic. corpus/
58+
ownership-lab/ is not globbed by tests/test_corpus.py (only corpus/real-world/ is), so these
59+
fixtures are inert data until someone decides to act on the report's section 10.
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
# H-28-CMD evidence manifest: one line per pinned citation.
2+
# OK = re-derived now; MISSING/MARKER-NOT-FOUND = the report is stale.
3+
OK npgsql-10.0.3-NpgsqlCommand-Dispose.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=1712
4+
OK npgsql-10.0.3-NpgsqlCommand-Reset.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=1728
5+
OK npgsql-10.0.3-NpgsqlCommand-ctor-SuppressFinalize.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=120
6+
OK npgsql-10.0.3-NpgsqlCommand-CreateCachedCommand.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=166
7+
OK npgsql-10.0.3-NpgsqlCommand-TraceCommandStart.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=1748
8+
OK npgsql-10.0.3-NpgsqlCommand-TraceCommandStop.txt npgsql/npgsql@v10.0.3 sha256=6bdde5901d32a633 lines=1792
9+
OK npgsql-10.0.3-NpgsqlConnection-CreateCommand.txt npgsql/npgsql@v10.0.3 sha256=02ed57055a9e1f02 lines=549
10+
OK npgsql-10.0.3-NpgsqlDataReader-Dispose.txt npgsql/npgsql@v10.0.3 sha256=9c109626d6627b55 lines=1008
11+
OK npgsql-10.0.3-NpgsqlDataReader-Close-public.txt npgsql/npgsql@v10.0.3 sha256=9c109626d6627b55 lines=1073
12+
OK npgsql-10.0.3-NpgsqlDataReader-Cleanup.txt npgsql/npgsql@v10.0.3 sha256=9c109626d6627b55 lines=1141
13+
OK npgsql-10.0.3-NpgsqlActivitySource-IsEnabled.txt npgsql/npgsql@v10.0.3 sha256=b7ef8df7f2f66573 lines=17
14+
OK npgsql-10.0.3-NpgsqlActivitySource-SourceName.txt npgsql/npgsql@v10.0.3 sha256=b7ef8df7f2f66573 lines=15
15+
OK npgsql-10.0.3-NpgsqlConnector-PreparedStatementManager.txt npgsql/npgsql@v10.0.3 sha256=7a13d79578e0a087 lines=164
16+
OK npgsql-main-NpgsqlCommand-Dispose.txt npgsql/npgsql@main sha256=fe55e7bb660c4a51 lines=1632
17+
OK npgsql-main-NpgsqlDataReader-Close-public.txt npgsql/npgsql@main sha256=8dfddffefbbb77c7 lines=1096
18+
OK runtime-v8.0.20-DataTable-Load.txt dotnet/runtime@v8.0.20 sha256=469f053f148bd5e4 lines=4969
19+
OK runtime-v10.0.12-DataTable-Load.txt dotnet/runtime@v10.0.12 sha256=dd4002e7407b1b15 lines=4974
20+
OK runtime-v10.0.12-DbCommand-class.txt dotnet/runtime@v10.0.12 sha256=c8f6f56c13b82f05 lines=11
21+
OK runtime-v10.0.12-DbCommand-DisposeAsync.txt dotnet/runtime@v10.0.12 sha256=c8f6f56c13b82f05 lines=245
22+
OK runtime-v10.0.12-DbDataReader-Close-Dispose.txt dotnet/runtime@v10.0.12 sha256=c2f3c2871cbc269f lines=34
23+
OK runtime-v10.0.12-IDbCommand.txt dotnet/runtime@v10.0.12 sha256=5fee96c4567d3894 lines=8
24+
OK runtime-v8.0.20-Activity-Dispose.txt dotnet/runtime@v8.0.20 sha256=2fcfbffca75351dd lines=1006
25+
OK runtime-v8.0.20-Activity-IDisposable.txt dotnet/runtime@v8.0.20 sha256=2fcfbffca75351dd lines=56
26+
OK mssqlite-SqliteCommand-Dispose.txt dotnet/efcore@main sha256=7ac8596c1cd999a3 lines=221
27+
OK mssqlite-SqliteCommand-DisposePreparedStatements.txt dotnet/efcore@main sha256=7ac8596c1cd999a3 lines=604
28+
OK mssqlite-SqliteCommand-PrepareAndEnumerate-head.txt dotnet/efcore@main sha256=7ac8596c1cd999a3 lines=547
29+
OK mssqlite-SqliteCommand-preparedStatements-field.txt dotnet/efcore@main sha256=7ac8596c1cd999a3 lines=31
30+
OK mssqlite-SqliteDataReader-Close-Dispose.txt dotnet/efcore@main sha256=5c3e1c054fceb256 lines=272
31+
OK mssqlite-SqliteConnection-commands-weakrefs.txt dotnet/efcore@main sha256=7ab4e87bd49e75a8 lines=32
32+
OK sqlitepclraw-sqlite3_stmt-SafeHandle.txt ericsink/SQLitePCL.raw@main sha256=0cb6c489786c3acf lines=196
33+
OK sqlclient-SqlCommand-Dispose.txt dotnet/SqlClient@main sha256=fc8200df4b130136 lines=1883
34+
OK mysqlconnector-MySqlCommand-Dispose.txt mysql-net/MySqlConnector@master sha256=4369c492ce1c1fc1 lines=377
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
corpus/ownership-lab/h28-command/fx/CommandDispose.own:42:3: error: [OWN001] 'command' is owned but not released at end of function (leaks on at least one path) [resource: disposable]
2+
42 | release reader; // DataTable.Load(reader) -> reader.Close()
3+
^
4+
note: 'command' acquired here at corpus/ownership-lab/h28-command/fx/CommandDispose.own:40
5+
corpus/ownership-lab/h28-command/fx/CommandDispose.own:69:32: error: [OWN001] 'command' is owned but not released at end of function (leaks on at least one path) [resource: disposable]
6+
69 | let reader = acquire Reader(command);
7+
^
8+
note: 'command' acquired here at corpus/ownership-lab/h28-command/fx/CommandDispose.own:68
9+
corpus/ownership-lab/h28-command/fx/CommandDispose.own:69:7: error: [OWN001] 'reader' is owned but not released at end of function (leaks on at least one path) [resource: disposable]
10+
69 | let reader = acquire Reader(command);
11+
^
12+
note: 'reader' acquired here at corpus/ownership-lab/h28-command/fx/CommandDispose.own:69
13+
14+
3 errors.
15+
# exit code: 1 (OWN001 is error-severity, so non-zero is the expected result)
16+
# command : python3 -m ownlang check corpus/ownership-lab/h28-command/fx/CommandDispose.own
17+
# cwd : repository root
18+
# python : Python 3.11.2
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteCommand.cs
5+
# blob sha : 7436572dcc87189532e757de1717e4972b1c23f3
6+
# file sha256: 7ac8596c1cd999a3967f30890a0e4bbd982b549e716b873106827377bc232588
7+
# file bytes : 26373
8+
# marker : 'protected override void Dispose(bool disposing)'
9+
# region : lines 221..232
10+
# derived by: scripts/derive_source_evidence.py
11+
221| protected override void Dispose(bool disposing)
12+
222| {
13+
223| DisposePreparedStatements(disposing);
14+
224|
15+
225| if (disposing)
16+
226| {
17+
227| _connection?.RemoveCommand(this);
18+
228| }
19+
229|
20+
230| base.Dispose(disposing);
21+
231| }
22+
232|
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteCommand.cs
5+
# blob sha : 7436572dcc87189532e757de1717e4972b1c23f3
6+
# file sha256: 7ac8596c1cd999a3967f30890a0e4bbd982b549e716b873106827377bc232588
7+
# file bytes : 26373
8+
# marker : 'private void DisposePreparedStatements(bool disposing = true)'
9+
# region : lines 604..625
10+
# derived by: scripts/derive_source_evidence.py
11+
604| private void DisposePreparedStatements(bool disposing = true)
12+
605| {
13+
606| if (disposing
14+
607| && DataReader != null)
15+
608| {
16+
609| DataReader.Dispose();
17+
610| DataReader = null;
18+
611| }
19+
612|
20+
613| if (_preparedStatements != null)
21+
614| {
22+
615| foreach (var (stmt, _) in _preparedStatements)
23+
616| {
24+
617| stmt.Dispose();
25+
618| }
26+
619|
27+
620| _preparedStatements.Clear();
28+
621| }
29+
622|
30+
623| _prepared = false;
31+
624| }
32+
625| }
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteCommand.cs
5+
# blob sha : 7436572dcc87189532e757de1717e4972b1c23f3
6+
# file sha256: 7ac8596c1cd999a3967f30890a0e4bbd982b549e716b873106827377bc232588
7+
# file bytes : 26373
8+
# marker : 'private IEnumerable<(sqlite3_stmt Statement, int ParamCount)> PrepareAndEnumerateStatements()'
9+
# region : lines 547..552
10+
# derived by: scripts/derive_source_evidence.py
11+
547| private IEnumerable<(sqlite3_stmt Statement, int ParamCount)> PrepareAndEnumerateStatements()
12+
548| {
13+
549| DisposePreparedStatements(disposing: false);
14+
550|
15+
551| var byteCount = Encoding.UTF8.GetByteCount(_commandText);
16+
552| var sql = new byte[byteCount + 1];
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteCommand.cs
5+
# blob sha : 7436572dcc87189532e757de1717e4972b1c23f3
6+
# file sha256: 7ac8596c1cd999a3967f30890a0e4bbd982b549e716b873106827377bc232588
7+
# file bytes : 26373
8+
# marker : '_preparedStatements ='
9+
# region : lines 31..32
10+
# derived by: scripts/derive_source_evidence.py
11+
31| private readonly List<(sqlite3_stmt Statement, int ParamCount)> _preparedStatements = [with(1)];
12+
32| private SqliteConnection? _connection;
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteConnection.cs
5+
# blob sha : 22e183f1e7be5f329feb2de1ab46b5e722f107ba
6+
# file sha256: 7ab4e87bd49e75a8081f443be91a3b04ba5ca458ca05874f559c54b946ec6a9f
7+
# file bytes : 59980
8+
# marker : 'List<WeakReference<SqliteCommand>> _commands'
9+
# region : lines 32..33
10+
# derived by: scripts/derive_source_evidence.py
11+
32| private readonly List<WeakReference<SqliteCommand>> _commands = [];
12+
33|
Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : dotnet/efcore
3+
# ref : main
4+
# path : src/Microsoft.Data.Sqlite.Core/SqliteDataReader.cs
5+
# blob sha : 105e6e4a2df2206c651fb393564a90fad686686a
6+
# file sha256: 5c3e1c054fceb256fc9b2642db5f16cf870f726aa29e681d36ed4933ef989e9b
7+
# file bytes : 36674
8+
# marker : 'public override void Close()'
9+
# region : lines 272..313
10+
# derived by: scripts/derive_source_evidence.py
11+
272| public override void Close()
12+
273| => Dispose(true);
13+
274|
14+
275| /// <summary>
15+
276| /// Releases any resources used by the data reader and closes it.
16+
277| /// </summary>
17+
278| /// <param name="disposing">
18+
279| /// <see langword="true" /> to release managed and unmanaged resources;
19+
280| /// <see langword="false" /> to release only unmanaged resources.
20+
281| /// </param>
21+
282| protected override void Dispose(bool disposing)
22+
283| {
23+
284| if (!disposing || _closed)
24+
285| {
25+
286| return;
26+
287| }
27+
288|
28+
289| _command.DataReader = null;
29+
290|
30+
291| _record?.Dispose();
31+
292| _record = null;
32+
293|
33+
294| if (_stmtEnumerator != null)
34+
295| {
35+
296| try
36+
297| {
37+
298| while (NextResult())
38+
299| {
39+
300| }
40+
301| }
41+
302| catch
42+
303| {
43+
304| }
44+
305| }
45+
306|
46+
307| _stmtEnumerator?.Dispose();
47+
308|
48+
309| _closed = true;
49+
310|
50+
311| if (_closeConnection)
51+
312| {
52+
313| _command.Connection!.Close();
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
# H-28-CMD source citation (auto-derived, do not edit by hand)
2+
# repo : mysql-net/MySqlConnector
3+
# ref : master
4+
# path : src/MySqlConnector/MySqlCommand.cs
5+
# blob sha : 7712fac730d089d7d725cc1c0078053c88e06e0c
6+
# file sha256: 4369c492ce1c1fc1191b0684be67c6c6dead95b4545ffb7590ec65ab4ecf7d7b
7+
# file bytes : 19512
8+
# marker : 'protected override void Dispose(bool disposing)'
9+
# region : lines 377..382
10+
# derived by: scripts/derive_source_evidence.py
11+
377| protected override void Dispose(bool disposing)
12+
378| {
13+
379| m_isDisposed = true;
14+
380| base.Dispose(disposing);
15+
381| }
16+
382|

0 commit comments

Comments
 (0)