diff --git a/src/mir/builder/control_flow/joinir/merge/mod.rs b/src/mir/builder/control_flow/joinir/merge/mod.rs index 94467c0e..43cbf35e 100644 --- a/src/mir/builder/control_flow/joinir/merge/mod.rs +++ b/src/mir/builder/control_flow/joinir/merge/mod.rs @@ -414,6 +414,23 @@ pub(in crate::mir::builder) fn merge_joinir_mir_blocks( ); } + // Phase 200-3: Verify JoinIR contracts (debug only) + #[cfg(debug_assertions)] + { + if let Some(boundary) = boundary { + verify_joinir_contracts( + builder.function(), + entry_block_remapped, + exit_block_id, + &loop_header_phi_info, + boundary, + ); + if debug { + eprintln!("[cf_loop/joinir] Phase 200-3: Contract verification passed"); + } + } + } + Ok(exit_phi_result_id) } @@ -441,3 +458,139 @@ fn remap_values( Ok(()) } + +// ============================================================================ +// Phase 200-3: JoinIR Contract Verification +// ============================================================================ + +/// Verify loop header PHI consistency +/// +/// # Checks +/// +/// 1. If loop_var_name is Some, header block must have corresponding PHI +/// 2. All carriers in LoopHeaderPhiInfo should have PHIs in the header block +/// +/// # Panics +/// +/// Panics in debug mode if contract violations are detected. +#[cfg(debug_assertions)] +fn verify_loop_header_phis( + func: &crate::mir::MirFunction, + header_block: crate::mir::BasicBlockId, + loop_info: &LoopHeaderPhiInfo, + boundary: &JoinInlineBoundary, +) { + // Check 1: Loop variable PHI existence + if let Some(ref loop_var_name) = boundary.loop_var_name { + let header_block_data = &func.blocks[header_block.0]; + let has_loop_var_phi = header_block_data + .instructions + .iter() + .any(|instr| matches!(instr, crate::mir::MirInstruction::Phi { .. })); + + if !has_loop_var_phi && !loop_info.carrier_phis.is_empty() { + panic!( + "[JoinIRVerifier] Loop variable '{}' in boundary but no PHI in header block {} (has {} carrier PHIs)", + loop_var_name, header_block.0, loop_info.carrier_phis.len() + ); + } + } + + // Check 2: Carrier PHI existence + if !loop_info.carrier_phis.is_empty() { + let header_block_data = &func.blocks[header_block.0]; + let phi_count = header_block_data + .instructions + .iter() + .filter(|instr| matches!(instr, crate::mir::MirInstruction::Phi { .. })) + .count(); + + if phi_count == 0 { + panic!( + "[JoinIRVerifier] LoopHeaderPhiInfo has {} PHIs but header block {} has none", + loop_info.carrier_phis.len(), + header_block.0 + ); + } + + // Verify each carrier has a corresponding PHI + for (carrier_name, entry) in &loop_info.carrier_phis { + let phi_exists = header_block_data.instructions.iter().any(|instr| { + if let crate::mir::MirInstruction::Phi { dst, .. } = instr { + *dst == entry.phi_dst + } else { + false + } + }); + + if !phi_exists { + panic!( + "[JoinIRVerifier] Carrier '{}' has PHI dst {:?} but PHI not found in header block {}", + carrier_name, entry.phi_dst, header_block.0 + ); + } + } + } +} + +/// Verify exit line consistency +/// +/// # Checks +/// +/// 1. All exit_bindings in boundary should have corresponding values +/// 2. Exit block should exist and be in range +/// +/// # Panics +/// +/// Panics in debug mode if contract violations are detected. +#[cfg(debug_assertions)] +fn verify_exit_line( + func: &crate::mir::MirFunction, + exit_block: crate::mir::BasicBlockId, + boundary: &JoinInlineBoundary, +) { + // Check 1: Exit block exists + if exit_block.0 >= func.blocks.len() { + panic!( + "[JoinIRVerifier] Exit block {} out of range (func has {} blocks)", + exit_block.0, + func.blocks.len() + ); + } + + // Check 2: Exit bindings reference valid values + if !boundary.exit_bindings.is_empty() { + for binding in &boundary.exit_bindings { + // Verify host_slot is reasonable (basic sanity check) + // We can't verify the exact value since it's from the host's value space, + // but we can check it's not obviously invalid + if binding.host_slot.0 >= 1000000 { + // Arbitrary large number check + panic!( + "[JoinIRVerifier] Exit binding '{}' has suspiciously large host_slot {:?}", + binding.carrier_name, binding.host_slot + ); + } + } + } +} + +/// Verify all loop contracts for a merged JoinIR function +/// +/// This is the main entry point for verification. It runs all checks +/// and panics if any contract violation is found. +/// +/// # Panics +/// +/// Panics in debug mode if any contract violation is detected. +#[cfg(debug_assertions)] +fn verify_joinir_contracts( + func: &crate::mir::MirFunction, + header_block: crate::mir::BasicBlockId, + exit_block: crate::mir::BasicBlockId, + loop_info: &LoopHeaderPhiInfo, + boundary: &JoinInlineBoundary, +) { + verify_loop_header_phis(func, header_block, loop_info, boundary); + verify_exit_line(func, exit_block, boundary); +} diff --git a/src/mir/join_ir/mod.rs b/src/mir/join_ir/mod.rs index 2f871acd..7ef32aca 100644 --- a/src/mir/join_ir/mod.rs +++ b/src/mir/join_ir/mod.rs @@ -46,6 +46,8 @@ pub use lowering::{ // Re-export verification functions pub use verify::verify_progress_for_skip_ws; +// Phase 200-3: Contract verification functions are in merge/mod.rs (private module access) + /// JoinIR 関数ID(MIR 関数とは別 ID でもよい) #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct JoinFuncId(pub u32); diff --git a/src/mir/join_ir/verify.rs b/src/mir/join_ir/verify.rs index 17ba164f..f17e6c01 100644 --- a/src/mir/join_ir/verify.rs +++ b/src/mir/join_ir/verify.rs @@ -384,3 +384,10 @@ mod tests { ); } } + +// ============================================================================ +// Phase 200-3: JoinIR Contract Verification (Loop Header PHI / Exit Line) +// ============================================================================ + +// Note: Verification functions are moved to merge/mod.rs to avoid circular dependencies +// with private control_flow module. This file only contains progress verification.