From eef6fca8cd3b94a88ee1202ceb27e24c1533a7d5 Mon Sep 17 00:00:00 2001 From: nyash-codex Date: Sat, 1 Nov 2025 16:37:16 +0900 Subject: [PATCH] =?UTF-8?q?docs(loops):=20LoopForm=20SSOT=E8=A8=AD?= =?UTF-8?q?=E8=A8=88=E3=83=8E=E3=83=BC=E3=83=88=E3=82=92=E8=BF=BD=E5=8A=A0?= =?UTF-8?q?=E3=81=97=E3=80=81Bridge=E5=81=B4=E3=83=AB=E3=83=BC=E3=83=97?= =?UTF-8?q?=E9=99=8D=E4=B8=8B=E3=81=ABPHI=E5=88=B0=E9=81=94=E6=A4=9C?= =?UTF-8?q?=E8=A8=BC=E3=82=92=E5=B0=8E=E5=85=A5=EF=BC=88debug=E6=99=82?= =?UTF-8?q?=EF=BC=89=E3=80=82\n\n-=20=E6=96=B0=E8=A6=8F:=20docs/developmen?= =?UTF-8?q?t/architecture/loops/loopform=5Fssot.md\n-=20=E4=BF=AE=E6=AD=A3?= =?UTF-8?q?:=20src/runner/json=5Fv0=5Fbridge/lowering/loop=5F.rs=20?= =?UTF-8?q?=E3=81=AB=20debug=5Fverify=5Fphi=5Finputs=20=E5=91=BC=E3=81=B3?= =?UTF-8?q?=E5=87=BA=E3=81=97=E3=82=92=E8=BF=BD=E5=8A=A0\n-=20=E6=96=B9?= =?UTF-8?q?=E9=87=9D:=20Direct=20MIR=20=E3=81=AF=E6=97=A2=E3=81=AB=20phi?= =?UTF-8?q?=5Fcore=20=E3=82=92=E4=BD=BF=E7=94=A8=E3=80=82Bridge=20?= =?UTF-8?q?=E3=81=AF=E6=AE=B5=E9=9A=8E=E7=9A=84=E3=81=AB=20LoopPhiOps=20?= =?UTF-8?q?=E3=82=A2=E3=83=80=E3=83=97=E3=82=BF=E3=81=A7SSOT=E3=81=AB?= =?UTF-8?q?=E5=AF=84=E3=81=9B=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../architecture/loops/loopform_ssot.md | 33 +++++++++++++++++++ src/runner/json_v0_bridge/lowering/loop_.rs | 20 +++++++++++ 2 files changed, 53 insertions(+) create mode 100644 docs/development/architecture/loops/loopform_ssot.md diff --git a/docs/development/architecture/loops/loopform_ssot.md b/docs/development/architecture/loops/loopform_ssot.md new file mode 100644 index 00000000..b4931696 --- /dev/null +++ b/docs/development/architecture/loops/loopform_ssot.md @@ -0,0 +1,33 @@ +# LoopForm SSOT（単一起点）設計ノート + +目的 +- ループのPHI整形・前処理（preheader Copy、header PHI seed、latch/continue 合流）を単一モジュールに集約してドリフトを防ぐ。 +- ビルダー（Direct MIR）とブリッジ（JSON v0 → MIR）の双方で同一の規約と検証を通す。 + +SSOT（Single Source of Truth） +- 中心: `src/mir/phi_core/loop_phi.rs` + - 型: `IncompletePhi`, `VarSnapshot` + - API: `prepare_loop_variables_with`, `seal_incomplete_phis_with`, `build_exit_phis_with` + - デバッグ: `phi_core::common::debug_verify_phi_inputs`（到達検証・重複検出） +- Direct MIR（既にSSOT使用） + - `src/mir/loop_builder.rs` が `LoopPhiOps` を実装し、`prepare/seal/exit` を phi_core へ委譲。 + - 形状: `preheader → header(φ) → body → latch → header|exit`（LoopForm準拠）。 +- JSON v0 Bridge（段階移行） + - まず同等の順序・検証を導入（Copy→Phi→Latch更新時の検証）。 + - 将来的に `LoopPhiOps` アダプタを追加して SSOT API を直接呼び出す。 + +規約（不変条件） +- header の PHI 入力は「preheader 経由の定義済み値」と「latch/continue からの値」だけ。 +- preheader で Copy を先行挿入し、PHI 入力は Copy の出力を参照する（Use-Before-Def回避）。 +- 1 predecessor なら直接 bind（PHI省略）、2つ以上で PHI を生成。 +- 検証は Fail‑Fast ではなく開発時 WARN（`debug_assert`）だが、将来 Core 側で整形に移管予定。 + +今後の移行 +- Bridge 側に `LoopPhiOps` 実装を追加し、`prepare/seal/exit` を直接呼ぶ。 +- ループ形状の生成をユーティリティ化（builder/bridge 双方から共通呼び出し）。 + +関連 +- `src/mir/loop_builder.rs` +- `src/runner/json_v0_bridge/lowering/loop_.rs` +- `src/mir/phi_core/common.rs` + diff --git a/src/runner/json_v0_bridge/lowering/loop_.rs b/src/runner/json_v0_bridge/lowering/loop_.rs index 719ea316..20306ce7 100644 --- a/src/runner/json_v0_bridge/lowering/loop_.rs +++ b/src/runner/json_v0_bridge/lowering/loop_.rs @@ -54,6 +54,15 @@ pub(super) fn lower_loop_stmt( inputs: vec![(cur_bb, copy_val)], }); } + // 開発時検証（SSOTと同等の不変条件チェック） + #[cfg(debug_assertions)] + { + crate::mir::phi_core::common::debug_verify_phi_inputs( + f, + cond_bb, + &[(cur_bb, copy_val)], + ); + } phi_map.insert(name.clone(), dst); } } @@ -90,6 +99,17 @@ pub(super) fn lower_loop_stmt( for (name, &phi_dst) in &phi_map { if let Some(&latch_val) = body_vars.get(name) { bb.update_phi_input(phi_dst, (bend, latch_val))?; + // 2要素目（preheader copy + latch）の到達検証 + #[cfg(debug_assertions)] + { + if let Some(&pre_copy) = copy_map.get(name) { + crate::mir::phi_core::common::debug_verify_phi_inputs( + f, + cond_bb, + &[(cur_bb, pre_copy), (bend, latch_val)], + ); + } + } } } }