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
16 changes: 16 additions & 0 deletions corpus/ownership-lab/h29/door/README.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
P-OWN053-DOOR: orphaned_awaitables[] bound at both OwnIR strict doors (after the OWN053 promotion;
prereg frozen in Own.NET-paperwork before code). Produced by the PRODUCTION build of this tree, from
the repository root.

promo-u.door.py.txt / promo-u.door.rust.txt
../promotion/promo-u.facts.json through both CLIs, whose path IS the strict door: accepted,
5 advisory OWN053, 0 findings, exit 0, Python == Rust -- the rule and the message did not move.
neg-garbage.facts.json an entry whose local is a list, callee an object, result_type a number
(the exact shape the unbound list rendered as a real OWN053)
neg-line_above.facts.json an entry with line 2147483648 (above the §4.2 domain; the unbound
list degraded it to 0)
neg-family.facts.json an entry with family "C_whatever" (outside the closed set)
neg-*.py.txt / neg-*.rust.txt
both CLIs refuse each document with exit code 2 (ordinary bad input) naming the same rule;
the message text differs by language, as the cp1 ledger allows (verdict + category are the
cross-language contract, tests/fixtures/ownir_validation.json section orphaned_awaitables).
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-family.facts.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"ownir_version": 0, "module": "M", "orphaned_awaitables": [{"local": "tx", "callee": "T.M/0", "file": "Q.cs", "line": 1, "family": "C_whatever"}]}
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-family.py.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-family.facts.json: error: orphaned awaitable 'family' must be one of ['A_owned_result', 'B_protocol_lifecycle'], got 'C_whatever'
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-family.rust.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-family.facts.json: error: orphaned awaitable 'family' must be one of ["A_owned_result", "B_protocol_lifecycle"], got "C_whatever"
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-garbage.facts.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"ownir_version": 0, "module": "M", "orphaned_awaitables": [{"local": ["what", "is", "this"], "callee": {"oops": 1}, "file": "Q.cs", "line": 119, "result_type": 12345}]}
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-garbage.py.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-garbage.facts.json: error: orphaned awaitable 'local' must be a non-empty string, got ['what', 'is', 'this']
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-garbage.rust.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-garbage.facts.json: error: orphaned awaitable: 'local' must be a non-empty string
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-line_above.facts.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"ownir_version": 0, "module": "M", "orphaned_awaitables": [{"local": "tx", "callee": "T.M/0", "file": "Q.cs", "line": 2147483648}]}
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-line_above.py.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-line_above.facts.json: error: orphaned awaitable 'line' must be a source line in [0, 2147483647], got 2147483648 (spec/OwnIR.md §4.2)
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/door/neg-line_above.rust.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
corpus/ownership-lab/h29/door/neg-line_above.facts.json: error: orphaned awaitable 'line' must be a source line in [0, 2147483647], got 2147483648 (spec/OwnIR.md §4.2)
7 changes: 7 additions & 0 deletions corpus/ownership-lab/h29/door/promo-u.door.py.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
corpus/ownership-lab/h29/fx/Orphan.cs:11: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:12: warning: [OWN053] orphaned awaitable: 'r' = Npgsql.NpgsqlCommand.ExecuteReaderAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlDataReader is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:21: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:22: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:23: warning: [OWN053] orphaned awaitable: 'c' = Npgsql.NpgsqlTransaction.CommitAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (there is no result to release), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]

0 findings, 5 advisory (OWN053).
7 changes: 7 additions & 0 deletions corpus/ownership-lab/h29/door/promo-u.door.rust.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
corpus/ownership-lab/h29/fx/Orphan.cs:11: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:12: warning: [OWN053] orphaned awaitable: 'r' = Npgsql.NpgsqlCommand.ExecuteReaderAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlDataReader is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:21: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:22: warning: [OWN053] orphaned awaitable: 'tx' = Npgsql.NpgsqlConnection.BeginTransactionAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (its result Npgsql.NpgsqlTransaction is never released), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]
corpus/ownership-lab/h29/fx/Orphan.cs:23: warning: [OWN053] orphaned awaitable: 'c' = Npgsql.NpgsqlTransaction.CommitAsync/1(...) is obtained and lost -- never awaited, returned, stored or otherwise observed; the operation still runs (there is no result to release), its failure is lost, and a transaction / connection lifecycle call leaves the connection in a state nobody can finish. Await it and keep the result, return or store it where it is observed, or express fire-and-forget explicitly [resource: orphaned awaitable]

0 findings, 5 advisory (OWN053).
27 changes: 27 additions & 0 deletions corpus/ownership-lab/h29/fx/Orphan.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
using System;
using System.Collections.Generic;
using System.Data.Common;
using System.Threading;
using System.Threading.Tasks;
using Npgsql;
// H-29 fixture: orphaned awaitables and their twins; the method name carries the expectation (family / form / later references).
public class Orphan
{
Task _kept; Stream _s = null;
public async Task O01_B_orphan(NpgsqlConnection conn, CancellationToken ct) { var tx = conn.BeginTransactionAsync(ct); await Task.Yield(); } // local, B, refs 0 (PRIMARY)
public async Task O02_A_orphan(NpgsqlCommand cmd) { var r = cmd.ExecuteReaderAsync(); await Task.Yield(); } // local, A, refs 0 (PRIMARY)
public async Task O03_observed_later(NpgsqlConnection conn, CancellationToken ct) { var tx = conn.BeginTransactionAsync(ct); await using var t = await tx; } // refs 1 (not a candidate)
public void O04_stored(NpgsqlCommand cmd) { var t = cmd.ExecuteNonQueryAsync(); _kept = t; } // refs 1
public async Task O05_passed(NpgsqlCommand cmd) { var t = cmd.ExecuteNonQueryAsync(); await Task.WhenAll(t); } // refs 1
public void O06_discard(NpgsqlConnection conn, CancellationToken ct) { _ = conn.BeginTransactionAsync(ct); } // discard, B
public void O07_statement(NpgsqlConnection conn, CancellationToken ct) { conn.BeginTransactionAsync(ct); } // statement, B
public async Task O08_other_delay() { var d = Task.Delay(1); await Task.Yield(); } // local, OTHER, refs 0
public async Task O09_other_nonquery(NpgsqlCommand cmd) { var n = cmd.ExecuteNonQueryAsync(); await Task.Yield(); } // local, OTHER, refs 0
public async Task O10_awaited(NpgsqlCommand cmd) { var r = await cmd.ExecuteReaderAsync(); await r.DisposeAsync(); } // not an awaitable local (awaited)
public async Task O11_B_configureawait(NpgsqlConnection conn, CancellationToken ct) { var tx = conn.BeginTransactionAsync(ct).ConfigureAwait(false); await Task.Yield(); } // local, B via ConfigureAwait, refs 0 (PRIMARY)
public async Task O12_in_try(NpgsqlConnection conn, CancellationToken ct) { try { var tx = conn.BeginTransactionAsync(ct); await Task.Yield(); } finally { await conn.CloseAsync(); } } // local, B, refs 0, in_try (PRIMARY, the real shape)
public void O13_B_sync_commit(NpgsqlTransaction t) { var c = t.CommitAsync(); } // local, B (non-generic Task), refs 0 (PRIMARY)
public async Task O14_lambda(NpgsqlConnection conn, CancellationToken ct) { Func<Task> f = async () => { var tx = conn.BeginTransactionAsync(ct); await Task.Yield(); }; await f(); } // in_lambda flag
public async Task O15_A_stream(Stream s) { var r = s.ReadAsync(new byte[1], 0, 1); await Task.Yield(); } // local, OTHER (int result), refs 0
public async Task O16_using_local(NpgsqlCommand cmd) { await using var r = await cmd.ExecuteReaderAsync(); } // using local: skipped
}
21 changes: 21 additions & 0 deletions corpus/ownership-lab/h29/promotion/README.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
ownership-semantics-lab H-29 -> OWN053 promotion: the fixture run on the PRODUCTION build.

Build: frontend/roslyn/OwnSharp.Extractor of this tree (net8.0, Release), the rule always on under
--flow-locals (the own-check default). Run from the repository root on the committed fixture, with
the H-29 falsifier's Npgsql build output as the reference directory (Npgsql 10.0.3; any directory
holding that Npgsql.dll gives the same facts):
dotnet ownsharp-extract.dll --flow-locals corpus/ownership-lab/h29/fx/Orphan.cs --ref-dir <dir with Npgsql.dll> -o promo-u.facts.json
python -m ownlang ownir promo-u.facts.json > promo-u.py.txt
own-cli ownir promo-u.facts.json > promo-u.rust.txt

promo-u.facts.json the production build's facts (file paths repository-relative)
promo-u.py.txt / promo-u.rust.txt both engines: identical (parity), 5 advisory OWN053 at
Orphan.cs 11 / 12 / 21 / 22 / 23 (O01, O02, O11, O12, O13 --
exactly the five frozen primary sites of the H-29 scan), 0
findings, exit code 0; the eleven twins silent
fixture-diff-prototype-vs-promoted.txt research-branch provenance: the diff between the OWEN_H29=1
prototype build's facts and the promoted research build's
(only the entries' file-path form moved); both builds live on
research/ownership-semantics-lab-v1, whose facts also carry
the research-only params[].ordinal field this tree does not emit
build.txt the extractor's stderr for the run above
1 change: 1 addition & 0 deletions corpus/ownership-lab/h29/promotion/build.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
extractor: +4 references from --ref-dir /tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/falsifier/bin/Release/net8.0 (recursive)
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
106c106
< "file": "/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
---
> "file": "../../../tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
116c116
< "file": "/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
---
> "file": "../../../tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
126c126
< "file": "/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
---
> "file": "../../../tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
136c136
< "file": "/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
---
> "file": "../../../tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
146c146
< "file": "/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
---
> "file": "../../../tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad/lab/h29/fx/Orphan.cs",
153 changes: 153 additions & 0 deletions corpus/ownership-lab/h29/promotion/promo-u.facts.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,153 @@
{
"ownir_version": 0,
"module": "Extracted",
"components": [],
"services": [],
"functions": [
{
"name": "Orphan.O06_discard",
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"sig": "Npgsql.NpgsqlConnection,System.Threading.CancellationToken",
"params": [
{
"name": "conn",
"line": 16
}
],
"body": [
{
"op": "use",
"var": "conn",
"line": 16
}
]
},
{
"name": "Orphan.O07_statement",
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"sig": "Npgsql.NpgsqlConnection,System.Threading.CancellationToken",
"params": [
{
"name": "conn",
"line": 17
}
],
"body": [
{
"op": "use",
"var": "conn",
"line": 17
}
]
},
{
"name": "Orphan.O12_in_try",
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"sig": "Npgsql.NpgsqlConnection,System.Threading.CancellationToken",
"params": [
{
"name": "conn",
"line": 22
}
],
"body": [
{
"op": "if",
"line": 22,
"then": [
{
"op": "use",
"var": "conn",
"line": 22
},
{
"op": "return",
"var": null,
"line": 22
}
],
"else": []
},
{
"op": "if",
"line": 22,
"then": [
{
"op": "use",
"var": "conn",
"line": 22
},
{
"op": "return",
"var": null,
"line": 22
}
],
"else": []
},
{
"op": "use",
"var": "conn",
"line": 22
}
]
}
],
"stats": {
"methods_with_local": 15,
"methods_flow_analysed": 3,
"methods_skipped_unmodelled": 12
},
"orphaned_awaitables": [
{
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"line": 11,
"column": 87,
"method": "Orphan.O01_B_orphan",
"local": "tx",
"callee": "Npgsql.NpgsqlConnection.BeginTransactionAsync/1",
"family": "A_owned_result",
"result_type": "Npgsql.NpgsqlTransaction"
},
{
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"line": 12,
"column": 61,
"method": "Orphan.O02_A_orphan",
"local": "r",
"callee": "Npgsql.NpgsqlCommand.ExecuteReaderAsync/1",
"family": "A_owned_result",
"result_type": "Npgsql.NpgsqlDataReader"
},
{
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"line": 21,
"column": 95,
"method": "Orphan.O11_B_configureawait",
"local": "tx",
"callee": "Npgsql.NpgsqlConnection.BeginTransactionAsync/1",
"family": "A_owned_result",
"result_type": "Npgsql.NpgsqlTransaction"
},
{
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"line": 22,
"column": 91,
"method": "Orphan.O12_in_try",
"local": "tx",
"callee": "Npgsql.NpgsqlConnection.BeginTransactionAsync/1",
"family": "A_owned_result",
"result_type": "Npgsql.NpgsqlTransaction"
},
{
"file": "corpus/ownership-lab/h29/fx/Orphan.cs",
"line": 23,
"column": 62,
"method": "Orphan.O13_B_sync_commit",
"local": "c",
"callee": "Npgsql.NpgsqlTransaction.CommitAsync/1",
"family": "B_protocol_lifecycle",
"result_type": null
}
]
}
Loading
Loading