feat(joinir): Task 200-3 - JoinIRVerifier for LoopHeader PHI and ExitLine contracts
Debug-only verification module to catch JoinIR contract violations early: - verify_loop_header_phis: Checks loop_var_name → PHI exists in header block - verify_exit_line: Checks exit_bindings → values exist, exit block in range - verify_joinir_contracts: Main entry point, runs all checks Implementation: - Added verification functions to merge/mod.rs (private module has type access) - Called from merge_joinir_mir_blocks after exit block setup - Only active in debug builds (#[cfg(debug_assertions)]) Benefits: - Catches "动くけど header PHI 無い" bugs immediately - Validates exit_bindings before variable_map reconnection - Prevents silent contract violations during development
This commit is contained in:
@ -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)
|
Ok(exit_phi_result_id)
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -441,3 +458,139 @@ fn remap_values(
|
|||||||
|
|
||||||
Ok(())
|
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);
|
||||||
|
}
|
||||||
|
|||||||
@ -46,6 +46,8 @@ pub use lowering::{
|
|||||||
// Re-export verification functions
|
// Re-export verification functions
|
||||||
pub use verify::verify_progress_for_skip_ws;
|
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 でもよい)
|
/// JoinIR 関数ID(MIR 関数とは別 ID でもよい)
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
||||||
pub struct JoinFuncId(pub u32);
|
pub struct JoinFuncId(pub u32);
|
||||||
|
|||||||
@ -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.
|
||||||
|
|||||||
Reference in New Issue
Block a user