fix: only a definite release makes a call-site handoff (INF-S2, #380) - #381
Merged
Merged
Conversation
ConsumesParam treated a first-party parameter as consumed when the callee contained any immediate Dispose/Close of it, so a release behind a guard was lowered as an unconditional release of the caller's argument. That is the flattened must INF-S2 forbids: on pinned dotnet/runtime code it produced false OWN009 at two callers of VerifyPersistedKey(..., disposeKey: false) and a false must summary for the public Mono.Options GetArguments(TextReader) wrapper. A direct release or a forward to another consumer now counts only when it runs on every normal-return path of the callee: not under a condition, loop or catch, and not behind an earlier return unless a finally covers it. The guard's value is never read and no OwnIR field changes. A declined argument stays an ordinary escape (an untracked local, a used parameter), so no opposite verdict is invented. GuardedConsumeSample + tests/test_guarded_consume.py pin the partial shapes (guard false, guarded early return, guarded forward), the guard-true caller (no fabricated release, no fabricated leak), the definite anchors (plain and finally dispose still give OWN002 on a later use) and the borrowing wrapper (summary no). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp
…hapes No production logic changes. #380 stopped lowering a guarded release as a call-site release, which moves two records the P-037 evidence pins; both are moved on purpose and in view. Conformance controls: `current` pinned the fabricated release and, for the three G-V4 controls, the known-false-positive OWN003 it caused. It is re-measured on both engines and now equals the `post_a1` record those files have carried since afeca38. The superseded record is kept in each control's append-only remeasured[] entry. Fact shapes: nine shapes re-recorded with `p037_fact_shapes.py record`. Seven guarded callers lose their functions[] record and with it the A2 sidecar; two wrappers move release -> use; two verdicts lose OWN003. Each moved shape gains a baseline_transitions[] entry keeping the superseded facts, verdicts and a2_expect verbatim. The vanished records' a2_expect entries are replaced by an asserted absence ({"record": "absent"}), which the checker now enforces by name, so a record that comes back fails the census instead of being re-pinned. Classified as an accepted baseline movement caused by #380: not a P-037 implementation, not a #304 reopen, not evidence that the A2 contract holds. Canonical first-party call transport remains absent; see docs/notes/p037-fact-shape-baseline-transition-380.md. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
…d limitation The comment on IsDefiniteInBody claimed that declining a partial release "never invents the opposite verdict". That holds for owned locals, which become untracked escapes, but not for forwarded parameters: the remaining `use` lets the existing inference derive `no`, which is right for a false guard and wrong for a true or forwarded one. The comment now says what #380 guarantees (no fabricated `must`) and what it does not (INF-S2's `may`). Comment-only change; the algorithm is untouched. GuardedConsumeSample.ForwardDynamic forwards both its parameter and the guard. INF-S3 would summarize it `may`; today it is `no`. tests/test_guarded_consume.py pins `no` as a KNOWN LIMITATION, not as acceptance, and fails with a message naming the direction if it moves: `must` means the fabricated consume is back; `may` means a canonical call fact reached the core, so the pin must be re-recorded and #304's reopen condition 1 re-checked. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что и зачем
ConsumesParamсчитал параметр поглощённым, если в теле вызываемого есть любойDispose/Closeэтого параметра. Поэтому release под guard'ом превращался в безусловныйreleaseаргумента на стороне вызывающего — ровно тот сфабрикованныйmust, который запрещает INF-S2. На закреплённом коде dotnet/runtime это давало ложные OWN009 у двух вызывающихVerifyPersistedKey(..., disposeKey: false)и ложную сводкуmustу публичной обёртки Mono.OptionsGetArguments(TextReader)(#380).Теперь прямой release или форвард в другого потребителя считается поглощением только если он определён — выполняется на каждом нормальном пути вызываемого: не под условием, не в цикле или
catch, не после раннегоreturn(кроме покрытогоfinally). Значение guard'а не читается, OwnIR/schema/lattice/core не меняются. Отказ от handoff предотвращает фабрикацию безусловногоmust, но не даёт INF-S2may: для отслеживаемых локалов это обычно деградирует в escape/молчание; для форвардимых параметров существующий вывод может получитьnoиз оставшегосяuse— это намеренно вне #380 и не полное представлениеmay. Представить частичный форвард какmayможно только через каноничный call-факт.Конкретно: обёртка, форвардящая свой параметр в guarded-потребителя, теперь получает
no, а неmay, которое дал бы INF-S3. Дляfalse(C16) это верно, дляtrue/форварда — нет, но и не фабрикует ownership transfer. Это известное ограничение, а не цель, и оно запинено:GuardedConsumeSample.ForwardDynamic(Stream forwarded, bool dispose)→ сводкаno(KNOWN LIMITATION). Пин громко падает при любом сдвиге:must= сфабрикованный consume вернулся;may= пришли каноничные call-факты, перезаписать пин и перепроверить условие 1 #304.Production-код:
frontend/roslyn/OwnSharp.Extractor/Program.cs— логика только вf164dd3;410431aменяет в нём лишь комментарийIsDefiniteInBody(убрано завышенное «обратный вердикт не изобретается», область гарантии сужена до «нет сфабрикованногоmust»). Остальное — фикстура, тест, CI-шаг и переход записей P-037-evidence.Переход записей P-037 (c662032, без изменения production-логики)
corpus/p036-bakeoff:currentпиннил сфабрикованный release и вызванный имKNOWN_FALSE_POSITIVEOWN003. Перемерено на обоих движках; новоеcurrentсовпадает сpost_a1, который лежит в этих файлах сafeca38. Старая запись сохранена в append-onlyremeasured[].corpus/p037-shapes: 9 форм перезаписаны штатнымrecord. У 7 guarded-вызывающих пропадает записьfunctions[]вместе с A2-сайдкаром; 2 обёрткиrelease→use; у двух форм уходит OWN003. В каждой форме —baseline_transitions[]с дословно сохранёнными старыми фактами, вердиктами иa2_expect. Ожидания для исчезнувших записей заменены утверждённым отсутствием{"record": "absent"}, которое чекер теперь проверяет по имени: если запись вернётся, census упадёт, а не будет молча перезаписан.call-оп до движков не доходит), не доказательство выполнения A2. Подробно:docs/notes/p037-fact-shape-baseline-transition-380.md.Тип изменения
Как проверено
python tests/run_tests.py— сOWN_TIERB_REQUIRED=1,OWEN_STAGE2_REQUIRE=1,OWEN_RUST_CORE: exit 0 (с .NET 8 + .NET 9 SDK;verify-targetTier B 65/65)ruff check .иmypy(strict, включая изменённыеscripts/p037_*.py)python scripts/<...>.py --selftest)Дополнительно:
tests/test_guarded_consume.py(новый, обязательный в CI-джобе wpf-extractor): 0 падений на фиксе, 8 падений на экстракторе23e3203(red → green); якоря безусловного handoff (обычный Dispose и Dispose вfinally) по-прежнему дают OWN002. С410431aтам же пин KNOWN LIMITATIONForwardDynamic.forwarded == ["no"](обе машины согласны).scripts/p037_verdict_snapshot.py(137 файлов, population23e3203, обе машины): сдвинулись 3 файла — все три снятие известного ложного OWN003 в gv4-контролях; новых находок нет.scripts/p037_mos_snapshot.py: собственное дерево (81 файл) UNCHANGED; корпус — 12 сдвигов фактов, все вcorpus/p036-bakeoff, межмашинный паритет 0 расхождений.examples/gallery/cs(включая якорь07_use_after_handoff),examples/flagship,fixtures/marketplace-consumer-demoи всех 103 существующих sample-функций.scripts/p037_controls.py --engine both: all match (и--post-a1: all match);scripts/p037_fact_shapes.py check --engine both: 14/14.mustза C16 сталno(evidence: PhysShell/Own.NET-paperwork,paper-eval/oss-sixcase-fix380-reobservation-v1.json).Связанные issue
Closes #380. Refs #304 — не переоткрывается; reopen condition 1 не выполнено.
Чеклист
feat:,fix:,docs:…) — заголовкиf164dd3иc662032не в этом стиле (410431a— в нём);f164dd3уже цитируется внешними уликами (ConsumesParam flattens guarded release into unconditional handoff, causing false OWN009 and false must summaries #380, paperwork), поэтому история не переписывалась. Заголовок PR — в conventional-стиле.🤖 Generated with Claude Code
https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp