diff --git a/docs/development/current/main/10-Now.md b/docs/development/current/main/10-Now.md index ce6d493e..b94d9120 100644 --- a/docs/development/current/main/10-Now.md +++ b/docs/development/current/main/10-Now.md @@ -1,6 +1,6 @@ # Self Current Task — Now (main) -## Current Focus: Phase 29aa P5(Multi-predecessor Return join) +## Current Focus: Phase 29aa P6(Multi-predecessor Return join - intersection) **2025-12-28: Phase 29aa P5 完了** ✅ - 目的: Return block が複数 predecessor のとき、incoming state が完全一致する場合のみ ReturnCleanup を成立させる @@ -9,6 +9,10 @@ - Selfcheck: Case 3.7(state一致→cleanup)/ Case 3.8(state不一致→no cleanup)PASS - 検証: quick 154/154 PASS / selfcheck PASS +**2025-12-28: Phase 29aa P6 進行中** +- 目的: multi-predecessor Return で state 不一致でも、共通部分(intersection)だけ ReturnCleanup を成立 +- 入口: `docs/development/current/main/phases/phase-29aa/README.md` + **2025-12-27: Phase 29aa P4 完了** ✅ - 目的: Jump の直列チェーン(単一 predecessor)を通して ReturnCleanup を成立させる(cleanup は Return block のみ) - 入口: `docs/development/current/main/phases/phase-29aa/README.md` diff --git a/docs/development/current/main/30-Backlog.md b/docs/development/current/main/30-Backlog.md index f99d2167..e933564d 100644 --- a/docs/development/current/main/30-Backlog.md +++ b/docs/development/current/main/30-Backlog.md @@ -68,11 +68,12 @@ Related: - 入口: `docs/development/current/main/phases/phase-29z/README.md` - 指示書: `docs/development/current/main/phases/phase-29z/P0-RC_INSERTION_MINIMAL-INSTRUCTIONS.md` -- **Phase 29aa(P4 COMPLETE / P5 planned): RC insertion safety expansion(CFG-aware)** +- **Phase 29aa(P5 COMPLETE / P6 planned): RC insertion safety expansion(CFG-aware)** - 進捗: P2 ✅ 完了(Jump/Branch 終端で cleanup を入れない契約の SSOT 化) - 進捗: P3 ✅ 完了(Jump→Return single-predecessor state 伝播) - 進捗: P4 ✅ 完了(Jump-chain propagation to Return) - - 次: P5(multi-predecessor/PHI/loop/early-exit の安全設計) + - 進捗: P5 ✅ 完了(Multi-predecessor Return join: state完全一致のみ) + - 次: P6(Multi-predecessor Return join: intersection) - 入口: `docs/development/current/main/phases/phase-29aa/README.md` - **Phase 29x(planned, post self-host): De-Rust runtime for LLVM execution** diff --git a/docs/development/current/main/phases/phase-29aa/README.md b/docs/development/current/main/phases/phase-29aa/README.md index ecc01936..db7f25d4 100644 --- a/docs/development/current/main/phases/phase-29aa/README.md +++ b/docs/development/current/main/phases/phase-29aa/README.md @@ -1,6 +1,6 @@ # Phase 29aa: RC insertion safety expansion(CFG-aware design) -Status: P5 Complete (Multi-predecessor Return join) +Status: P6 Ready (Multi-predecessor Return join - intersection) Scope: Phase 29z の単一block限定実装から、誤releaseを起こさない形で CFG-aware に拡張するための設計を固める。 Entry: @@ -25,6 +25,7 @@ Progress: - P3: Jump→Return(単一 predecessor)で state 伝播し ReturnCleanup を成立させる(P2維持) - P4: Jump-chain(単一 predecessor 直列)で state 伝播し ReturnCleanup を成立させる(P2/P3 維持) - P5: Multi-predecessor Return で incoming state が完全一致する場合のみ ReturnCleanup を成立させる(P2/P3/P4 維持) +- P6: Multi-predecessor Return で incoming state の「安全な共通部分(intersection)」のみ cleanup する(P2-P5 維持) P3 SSOT: - Contract: @@ -75,3 +76,17 @@ P5 SSOT: - selfcheck Case 3.7(state一致 → Return block に 1 cleanup)PASS - selfcheck Case 3.8(state不一致 → 全ブロック 0 cleanup)PASS - 既定OFF維持(featureなしは no-op) + +P6 SSOT: +- Objective: + - Return block が multi-predecessor のとき、incoming state が完全一致しない場合でも + 「全経路で必ず保持されている ptr→value」のみを ReturnCleanup で release する。 +- Contract: + - cleanup は Return block の BeforeTerminator のみ(Jump/Branch block には入れない) + - join state は `intersection`(全 predecessor の end_state に同じ ptr が存在し、かつ value が同一のものだけ) + - intersection が empty の場合は cleanup しない + - subset/partial merge は許可するが、PHI 的な “値の合成” はしない(同一値のみ) +- Non-goals: + - PHI/loop/early-exit の cleanup + - value が一致しない ptr を release 対象に含めること + - Jump block への release 挿入(P2維持)