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

409 lines
15 KiB
Rust

//! 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
//! - V10: body_bb effects go in loop_plan.body (block_effects[body_bb] must be empty)
//! - V11: Exit must be last in Seq/If branch
//!
//! 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
));
}
Self::verify_exit_position(plans, depth, "Seq")?;
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
));
}
// V10: body_bb effects must be empty in block_effects (use loop_plan.body instead)
// Phase 286 P2.7: lowerer emits loop_plan.body for body_bb, ignoring block_effects
for (bb, effects) in loop_plan.block_effects.iter() {
if *bb == loop_plan.body_bb && !effects.is_empty() {
return Err(format!(
"[V10] Loop at depth {} has non-empty block_effects for body_bb {:?} ({} effects). \
Body effects must go in loop_plan.body instead.",
depth, loop_plan.body_bb, effects.len()
));
}
}
// 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
));
}
if let Some(else_plans) = &if_plan.else_plans {
if else_plans.is_empty() {
return Err(format!(
"[V5] If at depth {} has empty else_plans",
depth
));
}
}
Self::verify_exit_position(&if_plan.then_plans, depth, "If.then")?;
if let Some(else_plans) = &if_plan.else_plans {
Self::verify_exit_position(else_plans, depth, "If.else")?;
}
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(())
}
fn verify_exit_position(plans: &[CorePlan], depth: usize, scope: &str) -> Result<(), String> {
for (i, plan) in plans.iter().enumerate() {
if matches!(plan, CorePlan::Exit(_)) && i + 1 != plans.len() {
return Err(format!(
"[V11] Exit at depth {} in {} must be last (index {}, len {})",
depth,
scope,
i,
plans.len()
));
}
}
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, ConstValue, ValueId};
use crate::mir::builder::control_flow::edgecfg::api::Frag;
use crate::mir::builder::control_flow::plan::CorePhiInfo;
use std::collections::BTreeMap;
#[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());
}
#[test]
fn test_verify_if_empty_else_fails() {
let if_plan = CoreIfPlan {
condition: ValueId(1),
then_plans: vec![CorePlan::Effect(CoreEffectPlan::Const {
dst: ValueId(2),
value: ConstValue::Integer(1),
})],
else_plans: Some(vec![]),
};
let plan = CorePlan::If(if_plan);
let result = PlanVerifier::verify(&plan);
assert!(result.is_err());
assert!(result.unwrap_err().contains("[V5]"));
}
#[test]
fn test_verify_exit_not_last_fails() {
let plan = CorePlan::Seq(vec![
CorePlan::Exit(CoreExitPlan::Return(None)),
CorePlan::Effect(CoreEffectPlan::Const {
dst: ValueId(1),
value: ConstValue::Integer(0),
}),
]);
let result = PlanVerifier::verify(&plan);
assert!(result.is_err());
assert!(result.unwrap_err().contains("[V11]"));
}
#[test]
fn test_v10_body_bb_effects_in_block_effects_fails() {
// V10: body_bb effects must be empty in block_effects
// This test verifies that having effects in body_bb's block_effects fails validation
let preheader_bb = BasicBlockId(0);
let header_bb = BasicBlockId(1);
let body_bb = BasicBlockId(2);
let step_bb = BasicBlockId(3);
let after_bb = BasicBlockId(4);
let loop_plan = CoreLoopPlan {
preheader_bb,
header_bb,
body_bb,
step_bb,
after_bb,
found_bb: after_bb,
body: vec![],
cond_loop: ValueId(100),
cond_match: ValueId(101),
block_effects: vec![
(preheader_bb, vec![]),
(header_bb, vec![]),
// V10 violation: body_bb has effects in block_effects
(body_bb, vec![CoreEffectPlan::Const {
dst: ValueId(102),
value: ConstValue::Integer(42),
}]),
(step_bb, vec![]),
],
phis: vec![CorePhiInfo {
block: header_bb,
dst: ValueId(103),
inputs: vec![(preheader_bb, ValueId(104)), (step_bb, ValueId(105))],
tag: "test_phi".to_string(),
}],
frag: Frag {
entry: header_bb,
exits: BTreeMap::new(),
wires: vec![],
branches: vec![],
},
final_values: vec![("i".to_string(), ValueId(103))],
};
let plan = CorePlan::Loop(loop_plan);
let result = PlanVerifier::verify(&plan);
assert!(result.is_err());
let err = result.unwrap_err();
assert!(err.contains("[V10]"), "Expected V10 error, got: {}", err);
assert!(err.contains("body_bb"), "Expected body_bb in error, got: {}", err);
}
}