feat(joinir): Phase 204 PHI Contract Verifier complete
Phase 204-3/5/6/7: PHI inputs verification, integration, testing, docs Implementation: - verify_phi_inputs_defined(): Conservative sanity checks (ValueId < 100000) - Integration: All verifiers in verify_joinir_contracts() - Testing: 821 tests PASS, no regressions Task Status: - ✅ 204-1: Design document (phase204-phi-contract-verifier.md) - ✅ 204-2: PHI dst overwrite detection - ✅ 204-3: PHI inputs sanity checks - ⚠️ 204-4: JoinValueSpace region verification (deferred to Phase 205+) - Rationale: Requires LoopHeaderPhiInfo extension (4+ files) - Alternative: Conservative threshold checks in verify_phi_inputs_defined() - ✅ 204-5: Integration (verify_joinir_contracts) - ✅ 204-6: Tests (821 PASS) - ✅ 204-7: Documentation (phase204 doc + CURRENT_TASK.md) Verification Coverage: - ✅ PHI exists (Phase 200-3) - ✅ PHI dst match (Phase 200-3) - ✅ PHI dst not overwritten (Phase 204-2) ✨ - ✅ PHI inputs sanity (Phase 204-3) ✨ - ⚠️ PHI inputs DFA (Phase 205+) - ⚠️ ValueId regions (Phase 205+) Design Principles: - Debug-only (#[cfg(debug_assertions)]) - Fail-Fast (panic on violation) - Zero cost in release builds Files Modified: - src/mir/builder/control_flow/joinir/merge/mod.rs (+115 lines) - src/mir/builder/control_flow/joinir/merge/exit_line/reconnector.rs (1 line) - docs/development/current/main/phase204-phi-contract-verifier.md (updated) - CURRENT_TASK.md (Phase 204 complete) Success Criteria: 4/5 met (1 deferred with rationale)
This commit is contained in:
nyash-codex
@ -542,6 +542,47 @@
|
||||
- コードベース整理完了
|
||||
- v2 API への完全移行
|
||||
- 保守性向上（デッドコード排除）
|
||||
- [x] **Phase 204: JoinIR PHI Contract Verifier 強化** ✅ (完了: 2025-12-09)
|
||||
- **目的**: Debug build での PHI 契約違反の早期検出
|
||||
- **実装内容**:
|
||||
- 204-1: 設計ドキュメント作成 ✅ (phase204-phi-contract-verifier.md)
|
||||
- 204-2: PHI dst overwrite 検出 ✅
|
||||
- `verify_no_phi_dst_overwrite()` 実装（SSA invariant 保証）
|
||||
- `get_instruction_dst()` ヘルパー（全 MirInstruction 対応）
|
||||
- 204-3: PHI inputs sanity checks ✅
|
||||
- `verify_phi_inputs_defined()` 実装（保守的閾値チェック）
|
||||
- Full DFA verification は Phase 205+ に延期
|
||||
- 204-4: JoinValueSpace 領域検証 ⚠️
|
||||
- **延期理由**: LoopHeaderPhiInfo への JoinValueSpace 追加が必要（4+ ファイル変更）
|
||||
- **代替策**: verify_phi_inputs_defined() で閾値チェック実装済み
|
||||
- 204-5: 統合確認 ✅
|
||||
- `verify_joinir_contracts()` に全チェック統合
|
||||
- 全パターン（P1/P2/P3/P4）で有効化
|
||||
- 204-6: テスト実行 ✅
|
||||
- 821 tests PASS、退行なし
|
||||
- 204-7: ドキュメント更新 ✅
|
||||
- **バグ修正**（Phase 204 作業中に発見）:
|
||||
- `entry_block_remapped` → `entry_block` (line 592)
|
||||
- `HashMap` → `BTreeMap` mismatch (reconnector.rs line 174)
|
||||
- **統計**:
|
||||
- 変更ファイル: 3ファイル (+115 lines in mod.rs)
|
||||
- コミット: `0175e62d` (Phase 204-2), `[pending]` (Phase 204-3/5/7)
|
||||
- テスト: 821 passed, 0 failed
|
||||
- **成果**:
|
||||
- PHI dst 上書き検出完了（手動ミスの早期発見）
|
||||
- PHI inputs sanity check 完了（保守的検証）
|
||||
- Debug-only verification（リリースビルドコストゼロ）
|
||||
- 設計原則遵守（Fail-Fast, 箱化, 最小変更）
|
||||
- **延期項目**:
|
||||
- Task 204-4: JoinValueSpace 領域検証（Phase 205+ で実装予定）
|
||||
- 理由: 高影響チェック優先、Phase 201-202 で衝突既解決
|
||||
- **検証カバレッジ**:
|
||||
- ✅ PHI exists (Phase 200-3)
|
||||
- ✅ PHI dst match (Phase 200-3)
|
||||
- ✅ PHI dst not overwritten (Phase 204-2 ✨)
|
||||
- ✅ PHI inputs sanity (Phase 204-3 ✨)
|
||||
- ⚠️ PHI inputs DFA (Phase 205+ 計画)
|
||||
- ⚠️ ValueId regions (Phase 205+ 計画)
|
||||
|
||||
---
|
||||
|
||||
|
||||
@ -322,9 +322,89 @@ pub struct LoopHeaderPhiInfo {
|
||||
- **Release build verification**: Debug-only for now (zero runtime cost)
|
||||
- **Cross-function verification**: Focus on single-function contracts first
|
||||
|
||||
## 7. References
|
||||
## 7. Implementation Results (2025-12-09)
|
||||
|
||||
### 7.1 Completed Tasks
|
||||
|
||||
| Task | Status | Notes |
|
||||
|------|--------|-------|
|
||||
| 204-1: Design document | ✅ Complete | This document |
|
||||
| 204-2: PHI dst overwrite detection | ✅ Complete | `verify_no_phi_dst_overwrite()` + helper |
|
||||
| 204-3: PHI inputs sanity checks | ✅ Complete | `verify_phi_inputs_defined()` - conservative checks |
|
||||
| 204-4: JoinValueSpace region verification | ⚠️ Deferred | Requires LoopHeaderPhiInfo extension (Phase 205+) |
|
||||
| 204-5: Integration | ✅ Complete | All checks in `verify_joinir_contracts()` |
|
||||
| 204-6: Unit tests | ✅ Complete | 821 tests PASS, no regressions |
|
||||
| 204-7: Documentation | ✅ Complete | This section |
|
||||
|
||||
### 7.2 Implementation Summary
|
||||
|
||||
**Files Modified**:
|
||||
1. `src/mir/builder/control_flow/joinir/merge/mod.rs`: +115 lines
|
||||
- `verify_no_phi_dst_overwrite()` - PHI dst overwrite detection
|
||||
- `get_instruction_dst()` - Helper to extract dst from MirInstruction
|
||||
- `verify_phi_inputs_defined()` - Conservative sanity checks for PHI inputs
|
||||
- `verify_joinir_contracts()` - Updated to call all verifiers
|
||||
2. `src/mir/builder/control_flow/joinir/merge/exit_line/reconnector.rs`: 1 line
|
||||
- Fixed `HashMap` → `BTreeMap` type mismatch
|
||||
|
||||
**Bug Fixes** (discovered during Phase 204):
|
||||
- Fixed `entry_block_remapped` → `entry_block` (line 592, mod.rs)
|
||||
- Fixed HashMap/BTreeMap mismatch (line 174, reconnector.rs)
|
||||
|
||||
**Test Results**:
|
||||
- ✅ 821 tests PASS (all library tests)
|
||||
- ✅ No regressions
|
||||
- ✅ All existing patterns (P1/P2/P3/P4) verified
|
||||
|
||||
**Commit**: `0175e62d` (Phase 204-2), `[pending]` (Phase 204-3/5/7)
|
||||
|
||||
### 7.3 Design Decisions
|
||||
|
||||
**Task 204-4 Deferral Rationale**:
|
||||
|
||||
JoinValueSpace region verification requires passing `JoinValueSpace` from pattern lowerers to merge/mod.rs. This involves:
|
||||
1. Adding `join_value_space: Option<JoinValueSpace>` to `LoopHeaderPhiInfo` (`#[cfg(debug_assertions)]`)
|
||||
2. Updating all pattern lowerers (P1/P2/P3/P4) to pass JoinValueSpace
|
||||
3. Implementing `verify_value_id_regions()` verification function
|
||||
|
||||
**Why deferred to Phase 205+?**:
|
||||
- Phase 204 focus: Immediate value (PHI dst overwrite detection)
|
||||
- JoinValueSpace verification requires coordinated changes across 4+ files
|
||||
- Conservative approach: Implement high-impact checks first
|
||||
- Phase 201-202 already eliminated ValueId collision through region separation
|
||||
- Verification would catch manual errors, but low urgency (no known issues)
|
||||
|
||||
**Alternative approach** (if needed before Phase 205):
|
||||
- Add sanity checks to existing verifiers (e.g., check PHI dst < 100000)
|
||||
- Implemented in `verify_phi_inputs_defined()` as conservative threshold checks
|
||||
|
||||
### 7.4 Verification Coverage
|
||||
|
||||
| Contract | Verified | Checker | Status |
|
||||
|----------|----------|---------|--------|
|
||||
| **PHI exists** | ✅ | `verify_loop_header_phis()` | Phase 200-3 |
|
||||
| **PHI dst match** | ✅ | `verify_loop_header_phis()` | Phase 200-3 |
|
||||
| **PHI dst not overwritten** | ✅ | `verify_no_phi_dst_overwrite()` | Phase 204-2 ✨ |
|
||||
| **PHI inputs sanity** | ✅ | `verify_phi_inputs_defined()` | Phase 204-3 ✨ |
|
||||
| **PHI inputs DFA** | ⚠️ | - | Phase 205+ (future) |
|
||||
| **Exit block exists** | ✅ | `verify_exit_line()` | Phase 200-3 |
|
||||
| **Exit bindings valid** | ✅ | `verify_exit_line()` + `verify_exit_line_contract()` | Phase 200-3 + 190-impl-D |
|
||||
| **ValueId regions** | ⚠️ | - | Phase 205+ (deferred) |
|
||||
|
||||
### 7.5 Success Criteria Review
|
||||
|
||||
1. ✅ All debug assertions enabled in test suite (821 tests pass)
|
||||
2. ✅ PHI dst overwrite detection implemented (`verify_no_phi_dst_overwrite()`)
|
||||
3. ⚠️ JoinValueSpace region verification deferred to Phase 205+
|
||||
4. ✅ No false positives (existing tests still pass)
|
||||
5. ✅ Documentation updated (this document)
|
||||
|
||||
**Overall**: 4/5 success criteria met, 1 deferred with clear rationale.
|
||||
|
||||
## 8. References
|
||||
|
||||
- Phase 200-3: Initial JoinIR verification infrastructure
|
||||
- Phase 201: JoinValueSpace introduction
|
||||
- Phase 190-impl-D-3: ExitLine contract verification
|
||||
- joinir-architecture-overview.md: Section 1.9 (ValueId Space Management)
|
||||
- Commit `0175e62d`: Phase 204-2 implementation
|
||||
|
||||
@ -889,6 +889,54 @@ fn get_instruction_dst(instr: &crate::mir::MirInstruction) -> Option<crate::mir:
|
||||
}
|
||||
}
|
||||
|
||||
/// Verify PHI inputs are defined (Phase 204-3 - Conservative sanity checks)
|
||||
///
|
||||
/// # Checks
|
||||
///
|
||||
/// 1. PHI inputs have reasonable ValueId values (< threshold)
|
||||
/// 2. No obviously undefined values (e.g., suspiciously large IDs)
|
||||
///
|
||||
/// # Note
|
||||
///
|
||||
/// Full data-flow analysis (DFA) verification is deferred to Phase 205+.
|
||||
/// This function only performs conservative sanity checks.
|
||||
///
|
||||
/// # Panics
|
||||
///
|
||||
/// Panics in debug mode if suspicious PHI inputs are detected.
|
||||
#[cfg(debug_assertions)]
|
||||
fn verify_phi_inputs_defined(
|
||||
func: &crate::mir::MirFunction,
|
||||
header_block: crate::mir::BasicBlockId,
|
||||
) {
|
||||
let header_block_data = func.blocks.get(&header_block).unwrap_or_else(|| {
|
||||
panic!(
|
||||
"[JoinIRVerifier] Header block {} not found ({} blocks in func)",
|
||||
header_block,
|
||||
func.blocks.len()
|
||||
)
|
||||
});
|
||||
|
||||
for instr in &header_block_data.instructions {
|
||||
if let crate::mir::MirInstruction::Phi { dst, inputs, type_hint: _ } = instr {
|
||||
for (value_id, pred_block) in inputs {
|
||||
// Conservative sanity check: ValueId should not be suspiciously large
|
||||
// Phase 201 JoinValueSpace uses regions:
|
||||
// - PHI Reserved: 0-99
|
||||
// - Param: 100-999
|
||||
// - Local: 1000+
|
||||
// - Reasonable max: 100000 (arbitrary but catches obvious bugs)
|
||||
if value_id.0 >= 100000 {
|
||||
panic!(
|
||||
"[JoinIRVerifier/Phase204-3] PHI {:?} has suspiciously large input {:?} from predecessor block {:?}",
|
||||
dst, value_id, pred_block
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Verify all loop contracts for a merged JoinIR function
|
||||
///
|
||||
/// This is the main entry point for verification. It runs all checks
|
||||
@ -907,5 +955,6 @@ fn verify_joinir_contracts(
|
||||
) {
|
||||
verify_loop_header_phis(func, header_block, loop_info, boundary);
|
||||
verify_no_phi_dst_overwrite(func, header_block, loop_info); // Phase 204-2
|
||||
verify_phi_inputs_defined(func, header_block); // Phase 204-3
|
||||
verify_exit_line(func, exit_block, boundary);
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user