phase29am(p2): verify core loop body effect-only
This commit is contained in:
@ -18,6 +18,7 @@
|
||||
//! - 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
|
||||
//! - V12: Loop.body must be Effect-only (Seq-of-effects allowed)
|
||||
//!
|
||||
//! Phase 273 P3: V1 (Carrier completeness) removed with CoreCarrierInfo
|
||||
|
||||
@ -124,6 +125,7 @@ impl PlanVerifier {
|
||||
}
|
||||
|
||||
// Verify body plans (now in_loop = true)
|
||||
Self::verify_loop_body_effect_only(&loop_plan.body, depth)?;
|
||||
for (i, plan) in loop_plan.body.iter().enumerate() {
|
||||
Self::verify_plan(plan, depth + 1, true).map_err(|e| {
|
||||
format!("[Loop.body[{}]] {}", i, e)
|
||||
@ -278,6 +280,47 @@ impl PlanVerifier {
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn verify_loop_body_effect_only(plans: &[CorePlan], depth: usize) -> Result<(), String> {
|
||||
for (i, plan) in plans.iter().enumerate() {
|
||||
let path = format!("Loop.body[{}]", i);
|
||||
Self::verify_body_plan_effect_only(plan, depth, &path)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn verify_body_plan_effect_only(
|
||||
plan: &CorePlan,
|
||||
depth: usize,
|
||||
path: &str,
|
||||
) -> Result<(), String> {
|
||||
match plan {
|
||||
CorePlan::Effect(_) => Ok(()),
|
||||
CorePlan::Seq(plans) => {
|
||||
for (i, nested) in plans.iter().enumerate() {
|
||||
let nested_path = format!("{}.Seq[{}]", path, i);
|
||||
Self::verify_body_plan_effect_only(nested, depth + 1, &nested_path)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
_ => Err(format!(
|
||||
"[V12] Loop body contains non-effect plan {} at depth {} ({})",
|
||||
Self::plan_kind(plan),
|
||||
depth,
|
||||
path
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
fn plan_kind(plan: &CorePlan) -> &'static str {
|
||||
match plan {
|
||||
CorePlan::Seq(_) => "Seq",
|
||||
CorePlan::Loop(_) => "Loop",
|
||||
CorePlan::If(_) => "If",
|
||||
CorePlan::Effect(_) => "Effect",
|
||||
CorePlan::Exit(_) => "Exit",
|
||||
}
|
||||
}
|
||||
|
||||
/// V6: Basic ValueId validity check
|
||||
///
|
||||
/// Note: This is a basic check. Full validity would require builder context.
|
||||
@ -297,6 +340,40 @@ mod tests {
|
||||
use crate::mir::builder::control_flow::plan::CorePhiInfo;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
fn make_loop_plan(body: Vec<CorePlan>) -> CoreLoopPlan {
|
||||
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);
|
||||
|
||||
CoreLoopPlan {
|
||||
preheader_bb,
|
||||
header_bb,
|
||||
body_bb,
|
||||
step_bb,
|
||||
after_bb,
|
||||
found_bb: after_bb,
|
||||
body,
|
||||
cond_loop: ValueId(100),
|
||||
cond_match: ValueId(101),
|
||||
block_effects: vec![
|
||||
(preheader_bb, vec![]),
|
||||
(header_bb, vec![]),
|
||||
(body_bb, vec![]),
|
||||
(step_bb, vec![]),
|
||||
],
|
||||
phis: vec![CorePhiInfo {
|
||||
block: header_bb,
|
||||
dst: ValueId(102),
|
||||
inputs: vec![(preheader_bb, ValueId(103)), (step_bb, ValueId(104))],
|
||||
tag: "test_phi".to_string(),
|
||||
}],
|
||||
frag: Frag::new(header_bb),
|
||||
final_values: vec![("i".to_string(), ValueId(102))],
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_verify_empty_seq_fails() {
|
||||
let plan = CorePlan::Seq(vec![]);
|
||||
@ -323,6 +400,49 @@ mod tests {
|
||||
assert!(result.is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_verify_loop_body_seq_effects_ok() {
|
||||
let body = vec![CorePlan::Seq(vec![
|
||||
CorePlan::Effect(CoreEffectPlan::Const {
|
||||
dst: ValueId(10),
|
||||
value: ConstValue::Integer(1),
|
||||
}),
|
||||
CorePlan::Seq(vec![CorePlan::Effect(CoreEffectPlan::Const {
|
||||
dst: ValueId(11),
|
||||
value: ConstValue::Integer(2),
|
||||
})]),
|
||||
])];
|
||||
let plan = CorePlan::Loop(make_loop_plan(body));
|
||||
let result = PlanVerifier::verify(&plan);
|
||||
assert!(result.is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_verify_loop_body_if_fails() {
|
||||
let if_plan = CoreIfPlan {
|
||||
condition: ValueId(1),
|
||||
then_plans: vec![CorePlan::Effect(CoreEffectPlan::Const {
|
||||
dst: ValueId(2),
|
||||
value: ConstValue::Integer(1),
|
||||
})],
|
||||
else_plans: None,
|
||||
};
|
||||
let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::If(if_plan)]));
|
||||
let result = PlanVerifier::verify(&plan);
|
||||
assert!(result.is_err());
|
||||
assert!(result.unwrap_err().contains("[V12]"));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_verify_loop_body_exit_fails() {
|
||||
let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::Exit(
|
||||
CoreExitPlan::Return(None),
|
||||
)]));
|
||||
let result = PlanVerifier::verify(&plan);
|
||||
assert!(result.is_err());
|
||||
assert!(result.unwrap_err().contains("[V12]"));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_verify_if_empty_else_fails() {
|
||||
let if_plan = CoreIfPlan {
|
||||
|
||||
Reference in New Issue
Block a user