phase29aa(p5): multi-pred return join when states match
This commit is contained in:
@ -1,11 +1,17 @@
|
||||
# Self Current Task — Now (main)
|
||||
|
||||
## Current Focus: Phase 29aa P4(Jump-chain propagation to Return)
|
||||
## Current Focus: Phase 29aa P5(Multi-predecessor Return join)
|
||||
|
||||
**2025-12-28: Phase 29aa P5 完了** ✅
|
||||
- 目的: Return block が複数 predecessor のとき、incoming state が完全一致する場合のみ ReturnCleanup を成立させる
|
||||
- 入口: `docs/development/current/main/phases/phase-29aa/README.md`
|
||||
- Safety Contract: state 不一致なら join state を作らない(誤 release 防止)
|
||||
- Selfcheck: Case 3.7(state一致→cleanup)/ Case 3.8(state不一致→no cleanup)PASS
|
||||
- 検証: quick 154/154 PASS / selfcheck PASS
|
||||
|
||||
**2025-12-27: Phase 29aa P4 完了** ✅
|
||||
- 目的: Jump の直列チェーン(単一 predecessor)を通して ReturnCleanup を成立させる(cleanup は Return block のみ)
|
||||
- 入口: `docs/development/current/main/phases/phase-29aa/README.md`
|
||||
- 次: Phase 29aa P5(候補: multi-predecessor/PHI/loop/early-exit の安全設計)
|
||||
|
||||
**2025-12-27: Phase 29aa P3 完了** ✅
|
||||
- 目的: Jump→Return(単一 predecessor)で state 伝播し ReturnCleanup を成立
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
# Phase 29aa: RC insertion safety expansion(CFG-aware design)
|
||||
|
||||
Status: P4 Complete (Jump-chain propagation to Return)
|
||||
Status: P5 Complete (Multi-predecessor Return join)
|
||||
Scope: Phase 29z の単一block限定実装から、誤releaseを起こさない形で CFG-aware に拡張するための設計を固める。
|
||||
|
||||
Entry:
|
||||
@ -24,6 +24,7 @@ Progress:
|
||||
- P2: Jump/Branch 終端では cleanup を入れない契約を SSOT 化(Fail-Fast guard)
|
||||
- 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 維持)
|
||||
|
||||
P3 SSOT:
|
||||
- Contract:
|
||||
@ -52,3 +53,25 @@ P4 SSOT:
|
||||
- quick 154/154 PASS 維持
|
||||
- `cargo run --bin rc_insertion_selfcheck --features rc-insertion-minimal` PASS
|
||||
- 既定OFF維持(featureなしは no-op)
|
||||
|
||||
P5 SSOT:
|
||||
- Contract:
|
||||
- cleanup は Return block の BeforeTerminator のみ(Jump/Branch block には入れない)
|
||||
- Return の multi-predecessor 合流は次の条件を全部満たすときだけ許可:
|
||||
1. 対象 block の terminator は Return
|
||||
2. predecessor が 2 以上
|
||||
3. 全 predecessor の end_state が完全一致(同じ ptr→value map)
|
||||
4. 一致した state が非 empty
|
||||
- 条件を満たさない場合は initial_state を作らない(ReturnCleanup なし)
|
||||
- 条件NG時に古い initial_state が残らないよう、毎回再計算して remove する(落とし穴1対策)
|
||||
- initial_state を set/remove したら changed フラグを更新(落とし穴2対策)
|
||||
- Non-goals:
|
||||
- 合流 state の "部分一致" / subset / merge(PHI相当なので禁止)
|
||||
- Branch/PHI/loop/early-exit の cleanup
|
||||
- Jump block への release 挿入(P2維持)
|
||||
- Acceptance:
|
||||
- quick 154/154 PASS 維持
|
||||
- `cargo run --bin rc_insertion_selfcheck --features rc-insertion-minimal` PASS
|
||||
- selfcheck Case 3.7(state一致 → Return block に 1 cleanup)PASS
|
||||
- selfcheck Case 3.8(state不一致 → 全ブロック 0 cleanup)PASS
|
||||
- 既定OFF維持(featureなしは no-op)
|
||||
|
||||
Reference in New Issue
Block a user