Skip to content

Commit 268bbd4

Browse files
committed
P-037 A2.2-1: decide argument relevance by value flow, not by syntax
Treatment-only (frontend/roslyn/OwnSharp.Extractor, spec/), under the frozen taxonomy of §10.6 (F0' bb557e1). The instrument is untouched; the after- comparison is still against R with population T. The A2.1 producer decided whether a call was relevant by whether it could represent the argument: a handle under a cast, an `as`, a `!`, a `?:`, a `??` or a switch expression came out `opaque`, and the whole call record vanished. A' (5a0de07) had already broken that coupling for params/ref/out/unstable- owned slots; this extends the same separation to every argument shape the freeze classifies, and does it semantically: - BuildGuardedFacts classifies each argument's VALUE with a small walker over Roslyn IOperation (Classify): a built-in identity or reference conversion that invokes no user-defined operator is transparent (the fact is the unwrapped var/param); `?:`, `??`, a switch expression and an `as` the static type does not guarantee are may-value (relevance kept, slot opaque); a user-defined conversion, implicit or explicit, however spelled, is a hidden call and never relevance; everything else stays opaque and irrelevant. Conversions are read at every IConversionOperation on the path and at the argument's InConversion, because `(Box)r` already has type Box at the call. - The argument operation is matched by span containment: Roslyn attaches it to the innermost expression (`(r)` and `r!` carry the syntax of `r`), so a node-identity match silently dropped exactly the transparent wrappers. - No `mentions`: opaque is opaque (§10.6.5). Pins: - corpus/p037-shapes, 12 new shapes recorded with a2_expect contracts: transparent cast / identity cast / as-upcast / bang captured with `var s`; may-value conditional / coalesce / switch / as-downcast captured with an opaque slot; negatives userconv-implicit, userconv-explicit, cast-nonhandle and mayvalue-userconv-arm carry no guarded_facts at all. The 14 existing shapes, the three A' relevance witnesses included, are byte-identical. - corpus/p037-relevance/probe: a2_2_1_observed measured with this walker; exactly the eight transparent and may-value rows moved to sidecar_call, every other row reads as at A'. tests/test_p037_relevance_freeze.py pins that (indirect rows never captured; direct and call-like rows unmoved; no captured row lost). - scripts/p037_sidecar_inertness.py: 27 documents, 59 sidecars, inert on both engines, python == rust. spec/OwnIR.md §5.2 states the value-flow rule. Refs #304 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb
1 parent bb557e1 commit 268bbd4

29 files changed

Lines changed: 1329 additions & 67 deletions

File tree

‎corpus/p037-relevance/README.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,9 @@ row into a checked `captured` / `excluded_by_rule:<name>` assertion.
4141

4242
## What moves this census
4343

44+
A2.2-1 landed: the eight transparent and may-value rows read `sidecar_call` in
45+
`a2_2_1_observed`, measured with the walker; every other row reads as at A'.
46+
4447
Only an A2.2 step, deliberately, one row at a time: a transparent wrapper
4548
becomes `captured` in A2.2-1, a call-like form in A2.2-2, an orphan record
4649
appears in A2.2-3. A row that moves without a step meaning to move it is a

‎corpus/p037-relevance/probe/expected.json‎

Lines changed: 51 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
"why": "One method per argument shape through which a disposable local can reach a callee, with the conversion edge on the way. Each is classified against the frozen taxonomy; `a2_1_observed` records what the corrected A2.1 extractor (A') emitted for it, measured, not assumed, so the A2.2 steps move a named row, never a number.",
55
"observed_at": "5a0de070af241a2612859153887ad6ae04afcce2",
66
"observed_at_note": "A' = corrected A2.1 treatment (PR #363), landed via main@23e3203; the extractor is byte-identical between A' and that merge. The superseded A (dce26ed) is not a measurement point.",
7+
"a2_2_1_note": "Measured with the A2.2-1 extractor (the IOperation value-flow walker) from the tree this file is committed in, before the commit: the SHA that carries this file is the SHA it was measured at. A2.2-1 promises exactly the transparent and may-value rows move to sidecar_call; every other row must read as it did at A'.",
78
"observed_vocabulary": {
89
"sidecar_call": "a function record with a guarded_facts call fact for the probe call",
910
"record_without_call_fact": "a function record exists but carries no call fact for the probe call",
@@ -27,155 +28,180 @@
2728
"Plain": {
2829
"class": "direct",
2930
"conversion": "reference_upcast",
30-
"a2_1_observed": "sidecar_call"
31+
"a2_1_observed": "sidecar_call",
32+
"a2_2_1_observed": "sidecar_call"
3133
},
3234
"PlainSame": {
3335
"class": "direct",
3436
"conversion": "none",
3537
"note": "identity binding to a NON-consuming callee: the legacy pass reads the pass as an escape, no tracked local remains, no record at all; the orphan carrier's case (\u00a710.6.6), and a direct flow",
36-
"a2_1_observed": "no_record"
38+
"a2_1_observed": "no_record",
39+
"a2_2_1_observed": "no_record"
3740
},
3841
"Parens": {
3942
"class": "transparent",
4043
"wrapper": "parenthesized",
4144
"conversion": "reference_upcast",
42-
"a2_1_observed": "sidecar_call"
45+
"a2_1_observed": "sidecar_call",
46+
"a2_2_1_observed": "sidecar_call"
4347
},
4448
"IdentityCast": {
4549
"class": "transparent",
4650
"wrapper": "cast",
4751
"conversion": "identity",
48-
"a2_1_observed": "record_without_call_fact"
52+
"a2_1_observed": "record_without_call_fact",
53+
"a2_2_1_observed": "sidecar_call"
4954
},
5055
"Cast": {
5156
"class": "transparent",
5257
"wrapper": "cast",
5358
"conversion": "reference_upcast",
54-
"a2_1_observed": "record_without_call_fact"
59+
"a2_1_observed": "record_without_call_fact",
60+
"a2_2_1_observed": "sidecar_call"
5561
},
5662
"AsCast": {
5763
"class": "transparent",
5864
"wrapper": "as",
5965
"conversion": "reference_upcast",
60-
"a2_1_observed": "record_without_call_fact"
66+
"a2_1_observed": "record_without_call_fact",
67+
"a2_2_1_observed": "sidecar_call"
6168
},
6269
"Bang": {
6370
"class": "transparent",
6471
"wrapper": "null_forgiving",
6572
"conversion": "reference_upcast",
66-
"a2_1_observed": "record_without_call_fact"
73+
"a2_1_observed": "record_without_call_fact",
74+
"a2_2_1_observed": "sidecar_call"
6775
},
6876
"Ternary": {
6977
"class": "may_value",
7078
"form": "conditional",
7179
"conversion": "reference_upcast",
72-
"a2_1_observed": "record_without_call_fact"
80+
"a2_1_observed": "record_without_call_fact",
81+
"a2_2_1_observed": "sidecar_call"
7382
},
7483
"Coalesce": {
7584
"class": "may_value",
7685
"form": "null_coalescing",
7786
"conversion": "reference_upcast",
78-
"a2_1_observed": "record_without_call_fact"
87+
"a2_1_observed": "record_without_call_fact",
88+
"a2_2_1_observed": "sidecar_call"
7989
},
8090
"Switch": {
8191
"class": "may_value",
8292
"form": "switch_expression",
8393
"conversion": "reference_upcast",
84-
"a2_1_observed": "record_without_call_fact"
94+
"a2_1_observed": "record_without_call_fact",
95+
"a2_2_1_observed": "sidecar_call"
8596
},
8697
"AsMayFail": {
8798
"class": "may_value",
8899
"form": "as_may_fail",
89100
"conversion": "may_fail_null",
90-
"a2_1_observed": "record_without_call_fact"
101+
"a2_1_observed": "record_without_call_fact",
102+
"a2_2_1_observed": "sidecar_call"
91103
},
92104
"Ctor": {
93105
"class": "call_like",
94106
"form": "object_creation",
95107
"conversion": "reference_upcast",
96-
"a2_1_observed": "record_without_call_fact"
108+
"a2_1_observed": "record_without_call_fact",
109+
"a2_2_1_observed": "record_without_call_fact"
97110
},
98111
"DelegateCall": {
99112
"class": "call_like",
100113
"form": "delegate_invocation",
101114
"conversion": "reference_upcast",
102-
"a2_1_observed": "no_record"
115+
"a2_1_observed": "no_record",
116+
"a2_2_1_observed": "no_record"
103117
},
104118
"Nested": {
105119
"class": "indirect",
106120
"exclusion": "nested_call_result",
107121
"conversion": "not_applicable",
108122
"note": "Wrap(r) itself is direct and is owed its own call fact; Use receives call_result",
109-
"a2_1_observed": "no_record"
123+
"a2_1_observed": "no_record",
124+
"a2_2_1_observed": "no_record"
110125
},
111126
"ArrayInit": {
112127
"class": "indirect",
113128
"exclusion": "container_construction",
114129
"conversion": "not_applicable",
115-
"a2_1_observed": "record_without_call_fact"
130+
"a2_1_observed": "record_without_call_fact",
131+
"a2_2_1_observed": "record_without_call_fact"
116132
},
117133
"CollectionInit": {
118134
"class": "indirect",
119135
"exclusion": "container_construction",
120136
"conversion": "not_applicable",
121-
"a2_1_observed": "record_without_call_fact"
137+
"a2_1_observed": "record_without_call_fact",
138+
"a2_2_1_observed": "record_without_call_fact"
122139
},
123140
"Tuple": {
124141
"class": "indirect",
125142
"exclusion": "tuple_construction",
126143
"conversion": "not_applicable",
127-
"a2_1_observed": "no_record"
144+
"a2_1_observed": "no_record",
145+
"a2_2_1_observed": "no_record"
128146
},
129147
"Closure": {
130148
"class": "indirect",
131149
"exclusion": "closure_capture",
132150
"conversion": "not_applicable",
133151
"note": "the inner Use(r) belongs to the lambda body, which has no record of its own (known gap)",
134-
"a2_1_observed": "no_record"
152+
"a2_1_observed": "no_record",
153+
"a2_2_1_observed": "no_record"
135154
},
136155
"MethodGroup": {
137156
"class": "indirect",
138157
"exclusion": "method_group_conversion",
139158
"conversion": "not_applicable",
140-
"a2_1_observed": "record_without_call_fact"
159+
"a2_1_observed": "record_without_call_fact",
160+
"a2_2_1_observed": "record_without_call_fact"
141161
},
142162
"UserConversion": {
143163
"class": "indirect",
144164
"exclusion": "user_conversion",
145165
"conversion": "user_defined_implicit",
146166
"note": "syntactically a bare identifier; only the semantic model shows the hidden op_Implicit",
147-
"a2_1_observed": "no_record"
167+
"a2_1_observed": "no_record",
168+
"a2_2_1_observed": "no_record"
148169
},
149170
"ExplicitUserConversion": {
150171
"class": "indirect",
151172
"exclusion": "user_conversion",
152173
"conversion": "user_defined_explicit",
153174
"note": "syntactically a cast; the user-defined operator sits inside the cast expression, and (XBox)r already has type XBox at the call",
154-
"a2_1_observed": "record_without_call_fact"
175+
"a2_1_observed": "record_without_call_fact",
176+
"a2_2_1_observed": "record_without_call_fact"
155177
},
156178
"NameOf": {
157179
"class": "indirect",
158180
"exclusion": "nameof_operand",
159181
"conversion": "not_applicable",
160-
"a2_1_observed": "record_without_call_fact"
182+
"a2_1_observed": "record_without_call_fact",
183+
"a2_2_1_observed": "record_without_call_fact"
161184
},
162185
"MemberAccess": {
163186
"class": "indirect",
164187
"exclusion": "member_access_on_handle",
165188
"conversion": "not_applicable",
166-
"a2_1_observed": "record_without_call_fact"
189+
"a2_1_observed": "record_without_call_fact",
190+
"a2_2_1_observed": "record_without_call_fact"
167191
},
168192
"Receiver": {
169193
"class": "indirect",
170194
"exclusion": "receiver_not_summary_parameter",
171195
"conversion": "not_applicable",
172-
"a2_1_observed": "record_without_call_fact"
196+
"a2_1_observed": "record_without_call_fact",
197+
"a2_2_1_observed": "record_without_call_fact"
173198
},
174199
"Indexer": {
175200
"class": "indirect",
176201
"exclusion": "storage_assignment",
177202
"conversion": "not_applicable",
178-
"a2_1_observed": "no_record"
203+
"a2_1_observed": "no_record",
204+
"a2_2_1_observed": "no_record"
179205
}
180206
}
181207
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
using System;
2+
using System.IO;
3+
4+
// A2.2-1 NEGATIVE: a transparent wrapper around a NON-handle creates no relevance. The cast
5+
// unwraps to a static property, which is opaque and not a handle of this method.
6+
static class ShapeCastNonHandle
7+
{
8+
static void Inner(Stream s, bool leaveOpen) { if (!leaveOpen) s.Dispose(); }
9+
static void Caller(string path)
10+
{
11+
var keep = File.OpenRead(path);
12+
Inner((Stream)Stream.Null, true);
13+
keep.Dispose();
14+
}
15+
}
Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "sidecar-cast-nonhandle",
4+
"status": "anchored",
5+
"why": "P-037 A2.2-1 (formal note §10.6.3): negative: a cast around a non-handle is not relevance; no call fact. Recorded with the IOperation value-flow walker; a row that moves without a step meaning to move it is a regression.",
6+
"a2_expect": [
7+
{
8+
"function": "ShapeCastNonHandle.Caller",
9+
"guarded_facts": "absent"
10+
}
11+
],
12+
"facts": {
13+
"ShapeCastNonHandle.Inner": {
14+
"params": [
15+
{
16+
"name": "s",
17+
"line": 8
18+
}
19+
],
20+
"body": [
21+
"if:None@8",
22+
"then:release:s@8"
23+
],
24+
"guarded_facts": {
25+
"version": 1,
26+
"calls": [],
27+
"guards": [
28+
{
29+
"site": {
30+
"line": 8,
31+
"column": 51
32+
},
33+
"param": 1,
34+
"predicate": "truth",
35+
"negated": true
36+
}
37+
]
38+
}
39+
},
40+
"ShapeCastNonHandle.Caller": {
41+
"params": null,
42+
"body": [
43+
"acquire:keep@11",
44+
"release:keep@13"
45+
],
46+
"guarded_facts": null
47+
}
48+
},
49+
"verdict": {
50+
"rust": [],
51+
"python": []
52+
}
53+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
using System;
2+
using System.IO;
3+
4+
// A2.2-1: `s as FileStream` on a Stream-typed handle is NOT guaranteed by the static type: it
5+
// yields the handle or null. May-value: relevant, opaque slot (contrast sidecar-transparent-as-upcast).
6+
static class ShapeMayValueAsDowncast
7+
{
8+
static void InnerF(FileStream f, bool leaveOpen) { if (!leaveOpen) f.Dispose(); }
9+
static void Caller(string path)
10+
{
11+
Stream s = File.OpenRead(path);
12+
InnerF(s as FileStream, true);
13+
}
14+
}

0 commit comments

Comments
 (0)