hakorune/src/mir/builder/control_flow/plan/verifier.rs

//! Phase 273 P3: PlanVerifier - CorePlan 不変条件検証 (fail-fast)
//!
//! # Responsibilities
//!
//! - Validate CorePlan invariants before lowering
//! - Fail fast on close-but-unsupported patterns
//! - Prevent silent miscompilation
//!
//! # Invariants (V2-V9)
//!
//! - V2: Condition validity (valid ValueId)
//! - V3: Exit validity (Return in function, Break/Continue in loop)
//! - V4: Seq non-empty
//! - V5: If completeness (then_plans non-empty)
//! - V6: ValueId validity (all ValueIds pre-generated)
//! - V7: PHI non-empty (loops require at least one carrier)
//! - V8: Frag entry matches header_bb
//! - V9: block_effects contains header_bb
//!
//! Phase 273 P3: V1 (Carrier completeness) removed with CoreCarrierInfo

use super::{CoreEffectPlan, CoreExitPlan, CoreIfPlan, CoreLoopPlan, CorePlan};
use crate::mir::ValueId;

/// Phase 273 P1: PlanVerifier - CorePlan 不変条件検証 (fail-fast)
pub(in crate::mir::builder) struct PlanVerifier;

impl PlanVerifier {
    /// Verify CorePlan invariants
    ///
    /// Returns Ok(()) if all invariants hold, Err with details otherwise.
    pub(in crate::mir::builder) fn verify(plan: &CorePlan) -> Result<(), String> {
        Self::verify_plan(plan, 0, false)
    }

    fn verify_plan(plan: &CorePlan, depth: usize, in_loop: bool) -> Result<(), String> {
        match plan {
            CorePlan::Seq(plans) => Self::verify_seq(plans, depth, in_loop),
            CorePlan::Loop(loop_plan) => Self::verify_loop(loop_plan, depth),
            CorePlan::If(if_plan) => Self::verify_if(if_plan, depth, in_loop),
            CorePlan::Effect(effect) => Self::verify_effect(effect, depth),
            CorePlan::Exit(exit) => Self::verify_exit(exit, depth, in_loop),
        }
    }

    /// V4: Seq non-empty
    fn verify_seq(plans: &[CorePlan], depth: usize, in_loop: bool) -> Result<(), String> {
        if plans.is_empty() {
            return Err(format!(
                "[V4] Empty Seq at depth {} (Seq must have at least one plan)",
                depth
            ));
        }

        for (i, plan) in plans.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                format!("[Seq[{}]] {}", i, e)
            })?;
        }

        Ok(())
    }

    /// Phase 273 P3: Verify loop with generalized fields
    ///
    /// Invariants:
    /// - V2: Condition validity (cond_loop, cond_match)
    /// - V7: PHI non-empty (at least one carrier)
    /// - V8: Frag entry matches header_bb
    /// - V9: block_effects contains header_bb
    fn verify_loop(loop_plan: &CoreLoopPlan, depth: usize) -> Result<(), String> {
        // V2: Condition validity (basic check - ValueId should be non-zero for safety)
        Self::verify_value_id_basic(loop_plan.cond_loop, depth, "cond_loop")?;
        Self::verify_value_id_basic(loop_plan.cond_match, depth, "cond_match")?;

        // V7: PHI non-empty (loops must have at least one carrier)
        if loop_plan.phis.is_empty() {
            return Err(format!(
                "[V7] Loop at depth {} has no PHI nodes (loops require at least one carrier)",
                depth
            ));
        }

        // V8: Frag entry matches header_bb (loop entry SSOT)
        if loop_plan.frag.entry != loop_plan.header_bb {
            return Err(format!(
                "[V8] Loop at depth {} has frag.entry {:?} != header_bb {:?}",
                depth, loop_plan.frag.entry, loop_plan.header_bb
            ));
        }

        // V9: block_effects contains header_bb
        let has_header = loop_plan.block_effects.iter().any(|(bb, _)| *bb == loop_plan.header_bb);
        if !has_header {
            return Err(format!(
                "[V9] Loop at depth {} block_effects missing header_bb {:?}",
                depth, loop_plan.header_bb
            ));
        }

        // Verify block_effects
        for (i, (bb, effects)) in loop_plan.block_effects.iter().enumerate() {
            for (j, effect) in effects.iter().enumerate() {
                Self::verify_effect(effect, depth).map_err(|e| {
                    format!("[Loop.block_effects[{}={:?}][{}]] {}", i, bb, j, e)
                })?;
            }
        }

        // Verify body plans (now in_loop = true)
        for (i, plan) in loop_plan.body.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, true).map_err(|e| {
                format!("[Loop.body[{}]] {}", i, e)
            })?;
        }

        // Verify PHIs
        for (i, phi) in loop_plan.phis.iter().enumerate() {
            Self::verify_value_id_basic(phi.dst, depth, &format!("phi[{}].dst", i))?;
            for (j, (_, val)) in phi.inputs.iter().enumerate() {
                Self::verify_value_id_basic(*val, depth, &format!("phi[{}].inputs[{}]", i, j))?;
            }
        }

        // Verify final_values
        for (i, (name, val)) in loop_plan.final_values.iter().enumerate() {
            if name.is_empty() {
                return Err(format!(
                    "[V6] final_values[{}] at depth {} has empty name",
                    i, depth
                ));
            }
            Self::verify_value_id_basic(*val, depth, &format!("final_values[{}]", i))?;
        }

        Ok(())
    }

    // Phase 273 P3: verify_carrier() removed (CoreCarrierInfo replaced by CorePhiInfo)

    /// V5: If completeness
    fn verify_if(if_plan: &CoreIfPlan, depth: usize, in_loop: bool) -> Result<(), String> {
        // V2: Condition validity
        Self::verify_value_id_basic(if_plan.condition, depth, "if.condition")?;

        // V5: then_plans non-empty
        if if_plan.then_plans.is_empty() {
            return Err(format!(
                "[V5] If at depth {} has empty then_plans",
                depth
            ));
        }

        for (i, plan) in if_plan.then_plans.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                format!("[If.then[{}]] {}", i, e)
            })?;
        }

        if let Some(else_plans) = &if_plan.else_plans {
            for (i, plan) in else_plans.iter().enumerate() {
                Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                    format!("[If.else[{}]] {}", i, e)
                })?;
            }
        }

        Ok(())
    }

    /// V6: Effect ValueId validity
    fn verify_effect(effect: &CoreEffectPlan, depth: usize) -> Result<(), String> {
        match effect {
            CoreEffectPlan::MethodCall { dst, object, method, args, effects: _ } => {
                // P2: dst is now Option<ValueId>
                if let Some(dst_val) = dst {
                    Self::verify_value_id_basic(*dst_val, depth, "MethodCall.dst")?;
                }
                Self::verify_value_id_basic(*object, depth, "MethodCall.object")?;
                if method.is_empty() {
                    return Err(format!(
                        "[V6] MethodCall at depth {} has empty method name",
                        depth
                    ));
                }
                for (i, arg) in args.iter().enumerate() {
                    Self::verify_value_id_basic(*arg, depth, &format!("MethodCall.args[{}]", i))?;
                }
            }
            CoreEffectPlan::BinOp { dst, lhs, op: _, rhs } => {
                Self::verify_value_id_basic(*dst, depth, "BinOp.dst")?;
                Self::verify_value_id_basic(*lhs, depth, "BinOp.lhs")?;
                Self::verify_value_id_basic(*rhs, depth, "BinOp.rhs")?;
            }
            CoreEffectPlan::Compare { dst, lhs, op: _, rhs } => {
                Self::verify_value_id_basic(*dst, depth, "Compare.dst")?;
                Self::verify_value_id_basic(*lhs, depth, "Compare.lhs")?;
                Self::verify_value_id_basic(*rhs, depth, "Compare.rhs")?;
            }
            CoreEffectPlan::Const { dst, value: _ } => {
                Self::verify_value_id_basic(*dst, depth, "Const.dst")?;
            }
        }
        Ok(())
    }

    /// V3: Exit validity
    fn verify_exit(exit: &CoreExitPlan, depth: usize, in_loop: bool) -> Result<(), String> {
        match exit {
            CoreExitPlan::Return(opt_val) => {
                if let Some(val) = opt_val {
                    Self::verify_value_id_basic(*val, depth, "Return.value")?;
                }
                // Return is always valid (in function context)
            }
            CoreExitPlan::Break => {
                if !in_loop {
                    return Err(format!(
                        "[V3] Break at depth {} outside of loop",
                        depth
                    ));
                }
            }
            CoreExitPlan::Continue => {
                if !in_loop {
                    return Err(format!(
                        "[V3] Continue at depth {} outside of loop",
                        depth
                    ));
                }
            }
        }
        Ok(())
    }

    /// V6: Basic ValueId validity check
    ///
    /// Note: This is a basic check. Full validity would require builder context.
    fn verify_value_id_basic(value_id: ValueId, depth: usize, context: &str) -> Result<(), String> {
        // ValueId(0) might be valid in some contexts, so we don't check for zero
        // This is a placeholder for more sophisticated checks if needed
        let _ = (value_id, depth, context);
        Ok(())
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::mir::{BasicBlockId, BinaryOp, CompareOp, ConstValue, ValueId};

    #[test]
    fn test_verify_empty_seq_fails() {
        let plan = CorePlan::Seq(vec![]);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V4]"));
    }

    #[test]
    fn test_verify_break_outside_loop_fails() {
        let plan = CorePlan::Exit(CoreExitPlan::Break);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V3]"));
    }

    #[test]
    fn test_verify_const_effect_succeeds() {
        let plan = CorePlan::Effect(CoreEffectPlan::Const {
            dst: ValueId(1),
            value: ConstValue::Integer(42),
        });
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_ok());
    }
}