docs: Phase 132-P3 verifier note

This commit is contained in:
nyash-codex
2025-12-15 06:08:19 +09:00
parent 771bf6b0d1
commit c8970bd4d4
3 changed files with 23 additions and 0 deletions

View File

@ -23,6 +23,7 @@
- JoinIR/Boundary: exit 値を境界に明示的に渡す - JoinIR/Boundary: exit 値を境界に明示的に渡す
- LLVM Python: PHI を落とす/上書きする経路を除去PHI SSOT を保護) - LLVM Python: PHI を落とす/上書きする経路を除去PHI SSOT を保護)
- JoinIR merge: exit PHI dst の allocator を function-level に統一ValueId 衝突を排除) - JoinIR merge: exit PHI dst の allocator を function-level に統一ValueId 衝突を排除)
- debug-only: Exit PHI collision を早期検出する verifier を追加LLVM 実行時に壊れる前に Fail-Fast
- **Phase 88 完了**: continue + 可変ステップi=i+const 差分)を dev-only fixture で固定、StepCalculator Box 抽出。 - **Phase 88 完了**: continue + 可変ステップi=i+const 差分)を dev-only fixture で固定、StepCalculator Box 抽出。
- **Phase 89 完了**: P0ContinueReturn detector+ P1lowering 実装)完了。 - **Phase 89 完了**: P0ContinueReturn detector+ P1lowering 実装)完了。
- **Phase 90 完了**: ParseStringComposite + `Null` literal + ContinueReturn同一値の複数 return-ifを dev-only fixture で固定。 - **Phase 90 完了**: ParseStringComposite + `Null` literal + ContinueReturn同一値の複数 return-ifを dev-only fixture で固定。

View File

@ -15,6 +15,9 @@
- 結果: `apps/tests/llvm_stage3_loop_only.hako` が LLVM EXE でも `Result: 3`VM 一致) - 結果: `apps/tests/llvm_stage3_loop_only.hako` が LLVM EXE でも `Result: 3`VM 一致)
- 詳細: `investigations/phase132-case-c-llvm-exe.md` - 詳細: `investigations/phase132-case-c-llvm-exe.md`
**追加Phase 132-P3: Exit PHI collision の早期検出debug-only**
- `verify_exit_phi_no_collision()``contract_checks.rs` に追加し、ValueId 衝突を JoinIR merge の段階で Fail-Fast する
## 20251214現状サマリ ## 20251214現状サマリ
補足docs が増えて迷子になったときの「置き場所ルールSSOT」: 補足docs が増えて迷子になったときの「置き場所ルールSSOT」:

View File

@ -91,3 +91,22 @@ Case C`apps/tests/llvm_stage3_loop_only.hako`)の LLVM EXE 検証で、
調査ログ: 調査ログ:
- `docs/development/current/main/investigations/phase132-case-c-llvm-exe.md` - `docs/development/current/main/investigations/phase132-case-c-llvm-exe.md`
---
## 追加: Phase 132-P3debug-onlyExit PHI collision early detection
同種の ValueId 衝突が “LLVM 実行時” にしか露見しないと切り分けコストが高いので、
JoinIR merge の契約検証debug build**早期に Fail-Fast** する検証 Box を追加した。
- 検証: `verify_exit_phi_no_collision()`
- 実装: `src/mir/builder/control_flow/joinir/merge/contract_checks.rs`
- 呼び出し元: `verify_exit_line(...)``#[cfg(debug_assertions)]`
検出例(概念):
- `bb0: %1 = const 0`
- `exit block: %1 = phi ...`(衝突)
期待される振る舞い:
- debug build では compile/run 中に panic で即停止(原因と修正案が出る)
- release build の既定挙動は変えない(検証は `debug_assertions` のみ)