feat(control_tree): Phase 129-B join_k as-last lowering
This commit is contained in:
@ -13,8 +13,6 @@
|
||||
//! - Focus on "did we extract the same information?"
|
||||
|
||||
use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
|
||||
use std::collections::BTreeSet;
|
||||
|
||||
/// Mismatch classification
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum MismatchKind {
|
||||
@ -143,54 +141,164 @@ pub fn check_full_parity(
|
||||
///
|
||||
/// - Checks function count, continuation count, tail-call form, env args
|
||||
/// - Does NOT check actual execution (RC comparison is optional)
|
||||
/// - Returns mismatch with hint if structure is invalid
|
||||
/// - Returns Err(freeze_with_hint) if structure is invalid
|
||||
pub fn verify_normalized_structure(
|
||||
module: &crate::mir::join_ir::JoinModule,
|
||||
expected_env_fields: usize,
|
||||
) -> ShadowParityResult {
|
||||
use crate::mir::join_ir::JoinIrPhase;
|
||||
) -> Result<(), String> {
|
||||
use crate::mir::join_ir::{JoinFuncId, JoinInst};
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
|
||||
// Check phase
|
||||
if !module.is_normalized() {
|
||||
let hint = format!(
|
||||
"module phase is not Normalized: {:?}",
|
||||
module.phase
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/not_normalized",
|
||||
&format!("module phase is not Normalized: {:?}", module.phase),
|
||||
"ensure the shadow lowering marks module as Normalized",
|
||||
));
|
||||
}
|
||||
|
||||
// Check function count (Phase 122 minimal: 1 main function)
|
||||
if module.functions.is_empty() {
|
||||
let hint = "no functions in module".to_string();
|
||||
return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_functions",
|
||||
"no functions in module",
|
||||
"ensure the shadow lowering emits at least the entry function",
|
||||
));
|
||||
}
|
||||
|
||||
// Check entry point
|
||||
if module.entry.is_none() {
|
||||
let hint = "no entry point in module".to_string();
|
||||
return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
|
||||
let entry_id = module.entry.ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_entry",
|
||||
"no entry point in module",
|
||||
"ensure the shadow lowering sets JoinModule.entry",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Check entry function exists
|
||||
let entry_func = module.functions.get(&entry_id).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/entry_missing",
|
||||
&format!("entry function {:?} not found", entry_id),
|
||||
"ensure the emitted module includes the entry function id",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Env layout: writes + inputs (SSOT)
|
||||
if entry_func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch: expected {}, got {}",
|
||||
expected_env_fields,
|
||||
entry_func.params.len()
|
||||
),
|
||||
"ensure env params are built from (writes + inputs) SSOT",
|
||||
));
|
||||
}
|
||||
|
||||
// Check main function exists
|
||||
let entry_id = module.entry.unwrap();
|
||||
let main_func = module.functions.get(&entry_id);
|
||||
if main_func.is_none() {
|
||||
let hint = format!("entry function {:?} not found", entry_id);
|
||||
return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
|
||||
// All functions in this shadow module must share the same env param arity.
|
||||
for (fid, func) in &module.functions {
|
||||
if func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch in {:?}: expected {}, got {}",
|
||||
fid,
|
||||
expected_env_fields,
|
||||
func.params.len()
|
||||
),
|
||||
"ensure all continuations share the same env layout (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
// Check env args count (Phase 122: writes only)
|
||||
let main_func = main_func.unwrap();
|
||||
if main_func.params.len() != expected_env_fields {
|
||||
let hint = format!(
|
||||
"env args mismatch: expected {}, got {}",
|
||||
expected_env_fields,
|
||||
main_func.params.len()
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
|
||||
// PHI prohibition (Phase 129-B scope): no IfMerge/NestedIfMerge in shadow output.
|
||||
for (fid, func) in &module.functions {
|
||||
for inst in &func.body {
|
||||
if matches!(inst, JoinInst::IfMerge { .. } | JoinInst::NestedIfMerge { .. }) {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/phi_forbidden",
|
||||
&format!("PHI-like merge instruction found in {:?}", fid),
|
||||
"Phase 129-B join_k path forbids IfMerge/NestedIfMerge; use join_k tailcall merge instead",
|
||||
));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
ShadowParityResult::ok()
|
||||
// Detect join_k tailcall form (if present) and validate it.
|
||||
fn tailcall_target(func: &crate::mir::join_ir::JoinFunction) -> Option<(JoinFuncId, usize)> {
|
||||
match func.body.last()? {
|
||||
JoinInst::Call {
|
||||
func,
|
||||
args,
|
||||
k_next: None,
|
||||
dst: None,
|
||||
} => Some((*func, args.len())),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
let mut tailcall_targets: Vec<(JoinFuncId, usize)> = Vec::new();
|
||||
for func in module.functions.values() {
|
||||
if let Some((target, argc)) = tailcall_target(func) {
|
||||
tailcall_targets.push((target, argc));
|
||||
}
|
||||
}
|
||||
|
||||
if tailcall_targets.is_empty() {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
// join_k merge should have at least two branch continuations tailcalling the same target.
|
||||
if tailcall_targets.len() < 2 {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_count",
|
||||
&format!(
|
||||
"join_k tailcall form requires >=2 tailcalls, got {}",
|
||||
tailcall_targets.len()
|
||||
),
|
||||
"ensure both then/else branches tailcall join_k as the last instruction",
|
||||
));
|
||||
}
|
||||
|
||||
let first_target = tailcall_targets[0].0;
|
||||
for (target, argc) in &tailcall_targets {
|
||||
if *target != first_target {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_target_mismatch",
|
||||
"tailcalls do not target a single join_k function",
|
||||
"ensure then/else both tailcall the same join_k function id",
|
||||
));
|
||||
}
|
||||
if *argc != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_arg_arity_mismatch",
|
||||
&format!(
|
||||
"tailcall env arg count mismatch: expected {}, got {}",
|
||||
expected_env_fields, argc
|
||||
),
|
||||
"ensure join_k is called with the full env fields list (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
let join_k_func = module.functions.get(&first_target).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_missing",
|
||||
"tailcall target join_k function not found in module",
|
||||
"ensure join_k is registered in JoinModule.functions",
|
||||
)
|
||||
})?;
|
||||
|
||||
match join_k_func.body.last() {
|
||||
Some(JoinInst::Ret { value: Some(_) }) => Ok(()),
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_not_ret",
|
||||
"join_k must end with Ret(Some(value))",
|
||||
"ensure join_k returns the merged env variable and has no post-if continuation in Phase 129-B",
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
|
||||
Reference in New Issue
Block a user