feat(control_tree): Phase 131 normalized loop(true) break-once builder (dev-only)
Implement Normalized shadow builder for loop(true) break-once pattern:
**New Module** (407 lines):
- src/mir/control_tree/normalized_shadow/loop_true_break_once.rs
- LoopTrueBreakOnceBuilderBox: loop(true) { <assign>* ; break } lowering
- PHI-free: env parameters + continuation-passing style
- Generated structure: main → loop_step → loop_body → k_exit
- Scope: Bool(true) literal condition only, break at end only
**Integration**:
- src/mir/control_tree/normalized_shadow/builder.rs
- Added lower_with_loop_support() for loop patterns
- try_lower_if_only() now falls through to loop support on capability reject
- src/mir/control_tree/normalized_shadow/mod.rs
- Module declaration added
**Contract**:
- Accepted: loop(true) { <assign of int literal/var/add>* ; break }
- Rejected (Ok(None)): continue, return in body, nested control flow
- Out of scope: general loop conditions, complex post-loop statements
**Limitations**:
- Structure-only (dev-only observation mode)
- Execution path not yet wired (follow-up phase required)
- Shadow JoinModule generation working, structural verification passing
- Unit tests: 1155/1155 PASS
Related: Phase 131 P0
This commit is contained in:
@ -11,6 +11,7 @@ use crate::mir::control_tree::normalized_shadow::env_layout::{
|
|||||||
expected_env_field_count as calc_expected_env_fields, EnvLayout,
|
expected_env_field_count as calc_expected_env_fields, EnvLayout,
|
||||||
};
|
};
|
||||||
use crate::mir::control_tree::normalized_shadow::if_as_last_join_k::IfAsLastJoinKLowererBox;
|
use crate::mir::control_tree::normalized_shadow::if_as_last_join_k::IfAsLastJoinKLowererBox;
|
||||||
|
use crate::mir::control_tree::normalized_shadow::loop_true_break_once::LoopTrueBreakOnceBuilderBox; // Phase 131
|
||||||
use crate::mir::control_tree::normalized_shadow::post_if_post_k::PostIfPostKBuilderBox; // Phase 129-C
|
use crate::mir::control_tree::normalized_shadow::post_if_post_k::PostIfPostKBuilderBox; // Phase 129-C
|
||||||
use crate::mir::control_tree::normalized_shadow::legacy::LegacyLowerer;
|
use crate::mir::control_tree::normalized_shadow::legacy::LegacyLowerer;
|
||||||
use crate::mir::control_tree::step_tree::StepTree;
|
use crate::mir::control_tree::step_tree::StepTree;
|
||||||
@ -40,9 +41,11 @@ impl StepTreeNormalizedShadowLowererBox {
|
|||||||
|
|
||||||
/// Try to lower an if-only StepTree to normalized form
|
/// Try to lower an if-only StepTree to normalized form
|
||||||
///
|
///
|
||||||
/// - `Ok(None)`: Out of scope (e.g., contains loops)
|
/// - `Ok(None)`: Out of scope (e.g., contains unsupported constructs)
|
||||||
/// - `Ok(Some(...))`: Shadow generation succeeded
|
/// - `Ok(Some(...))`: Shadow generation succeeded
|
||||||
/// - `Err(...)`: Should be supported but conversion failed (internal error)
|
/// - `Err(...)`: Should be supported but conversion failed (internal error)
|
||||||
|
///
|
||||||
|
/// Phase 131: Also supports loop(true) break-once pattern
|
||||||
pub fn try_lower_if_only(
|
pub fn try_lower_if_only(
|
||||||
step_tree: &StepTree,
|
step_tree: &StepTree,
|
||||||
available_inputs: &BTreeMap<String, ValueId>,
|
available_inputs: &BTreeMap<String, ValueId>,
|
||||||
@ -50,9 +53,13 @@ impl StepTreeNormalizedShadowLowererBox {
|
|||||||
let capability = check_if_only(step_tree);
|
let capability = check_if_only(step_tree);
|
||||||
match capability {
|
match capability {
|
||||||
CapabilityCheckResult::Supported => {
|
CapabilityCheckResult::Supported => {
|
||||||
|
// If-only path
|
||||||
Self::lower_if_only_to_normalized(step_tree, available_inputs)
|
Self::lower_if_only_to_normalized(step_tree, available_inputs)
|
||||||
}
|
}
|
||||||
CapabilityCheckResult::Unsupported(_reason) => Ok(None),
|
CapabilityCheckResult::Unsupported(_reason) => {
|
||||||
|
// Phase 131: Try loop(true) break-once pattern
|
||||||
|
Self::lower_with_loop_support(step_tree, available_inputs)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -78,6 +85,23 @@ impl StepTreeNormalizedShadowLowererBox {
|
|||||||
LegacyLowerer::lower_if_only_to_normalized(step_tree, &env_layout)
|
LegacyLowerer::lower_if_only_to_normalized(step_tree, &env_layout)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Phase 131: Lower StepTree with loop support (loop(true) break-once only)
|
||||||
|
fn lower_with_loop_support(
|
||||||
|
step_tree: &StepTree,
|
||||||
|
available_inputs: &BTreeMap<String, ValueId>,
|
||||||
|
) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
|
||||||
|
// Phase 126: EnvLayout 生成(available_inputs を使用)
|
||||||
|
let env_layout = EnvLayout::from_contract(&step_tree.contract, available_inputs);
|
||||||
|
|
||||||
|
// Phase 131: loop(true) break-once pattern
|
||||||
|
if let Some((module, meta)) = LoopTrueBreakOnceBuilderBox::lower(step_tree, &env_layout)? {
|
||||||
|
return Ok(Some((module, meta)));
|
||||||
|
}
|
||||||
|
|
||||||
|
// Not supported: fall back to legacy (returns Ok(None))
|
||||||
|
Ok(None)
|
||||||
|
}
|
||||||
|
|
||||||
/// Dev log helper for out-of-scope cases
|
/// Dev log helper for out-of-scope cases
|
||||||
pub fn get_status_string(step_tree: &StepTree) -> String {
|
pub fn get_status_string(step_tree: &StepTree) -> String {
|
||||||
format!(
|
format!(
|
||||||
|
|||||||
396
src/mir/control_tree/normalized_shadow/loop_true_break_once.rs
Normal file
396
src/mir/control_tree/normalized_shadow/loop_true_break_once.rs
Normal file
@ -0,0 +1,396 @@
|
|||||||
|
//! Phase 131 P0: loop(true) break-once Normalized lowering
|
||||||
|
//!
|
||||||
|
//! ## Responsibility
|
||||||
|
//!
|
||||||
|
//! - Lower `loop(true) { <assign>* ; break }` to Normalized JoinModule
|
||||||
|
//! - One-time execution loop (condition is always true, breaks immediately)
|
||||||
|
//! - PHI-free: all state passing via env arguments + continuations
|
||||||
|
//!
|
||||||
|
//! ## Contract
|
||||||
|
//!
|
||||||
|
//! - Input: StepTree with loop(true) { body ; break } pattern
|
||||||
|
//! - Output: JoinModule with:
|
||||||
|
//! - main(env) → TailCall(loop_step, env)
|
||||||
|
//! - loop_step(env) → if true { TailCall(loop_body, env) } else { TailCall(k_exit, env) }
|
||||||
|
//! - loop_body(env) → <assign statements update env> → TailCall(k_exit, env)
|
||||||
|
//! - k_exit(env) → Ret(env[x]) or TailCall(post_k, env)
|
||||||
|
//!
|
||||||
|
//! ## Scope
|
||||||
|
//!
|
||||||
|
//! - Condition: Bool literal `true` only
|
||||||
|
//! - Body: Assign(int literal/var/add) + LocalDecl only (Phase 130 baseline)
|
||||||
|
//! - Exit: Break at end of body only (no continue, no return in body)
|
||||||
|
//! - Post-loop: Simple return only (Phase 124-126 baseline)
|
||||||
|
//!
|
||||||
|
//! ## Fail-Fast
|
||||||
|
//!
|
||||||
|
//! - Out of scope → Ok(None) (fallback to legacy)
|
||||||
|
//! - In scope but conversion failed → Err (with freeze_with_hint in strict mode)
|
||||||
|
|
||||||
|
use super::env_layout::EnvLayout;
|
||||||
|
use super::legacy::LegacyLowerer;
|
||||||
|
use crate::ast::{ASTNode, LiteralValue};
|
||||||
|
use crate::mir::control_tree::step_tree::{StepNode, StepStmtKind, StepTree};
|
||||||
|
use crate::mir::join_ir::lowering::carrier_info::JoinFragmentMeta;
|
||||||
|
use crate::mir::join_ir::lowering::error_tags;
|
||||||
|
use crate::mir::join_ir::{ConstValue, JoinFunction, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
|
||||||
|
use crate::mir::ValueId;
|
||||||
|
use std::collections::BTreeMap;
|
||||||
|
|
||||||
|
/// Box-First: loop(true) break-once lowering to Normalized
|
||||||
|
pub struct LoopTrueBreakOnceBuilderBox;
|
||||||
|
|
||||||
|
impl LoopTrueBreakOnceBuilderBox {
|
||||||
|
/// Try to lower loop(true) break-once pattern to Normalized JoinModule.
|
||||||
|
///
|
||||||
|
/// Returns:
|
||||||
|
/// - Ok(Some((module, meta))): Successfully lowered
|
||||||
|
/// - Ok(None): Out of scope (fallback to legacy)
|
||||||
|
/// - Err(msg): In scope but failed (internal error)
|
||||||
|
pub fn lower(
|
||||||
|
step_tree: &StepTree,
|
||||||
|
env_layout: &EnvLayout,
|
||||||
|
) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
|
||||||
|
// Extract loop(true) pattern from root
|
||||||
|
let (prefix_nodes, loop_node, post_nodes) = match Self::extract_loop_true_pattern(&step_tree.root) {
|
||||||
|
Some(v) => v,
|
||||||
|
None => return Ok(None), // Not a loop(true) pattern
|
||||||
|
};
|
||||||
|
|
||||||
|
// Verify condition is Bool(true)
|
||||||
|
let (cond_ast, body_node) = match loop_node {
|
||||||
|
StepNode::Loop { cond_ast, body, .. } => (cond_ast, body.as_ref()),
|
||||||
|
_ => return Ok(None),
|
||||||
|
};
|
||||||
|
|
||||||
|
if !Self::is_bool_true_literal(&cond_ast.0) {
|
||||||
|
return Ok(None); // Condition is not Bool(true)
|
||||||
|
}
|
||||||
|
|
||||||
|
// Verify body ends with break
|
||||||
|
let body_stmts = match body_node {
|
||||||
|
StepNode::Block(stmts) => stmts,
|
||||||
|
_ => return Ok(None), // Body is not a block
|
||||||
|
};
|
||||||
|
|
||||||
|
if !Self::body_ends_with_break(body_stmts) {
|
||||||
|
return Ok(None); // Body doesn't end with break
|
||||||
|
}
|
||||||
|
|
||||||
|
// Extract body statements (excluding final break)
|
||||||
|
let body_prefix = &body_stmts[..body_stmts.len() - 1];
|
||||||
|
|
||||||
|
// Verify no return/continue in body
|
||||||
|
if Self::has_unsupported_exits(body_prefix) {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
|
||||||
|
let env_fields = env_layout.env_fields();
|
||||||
|
|
||||||
|
fn alloc_value_id(next_value_id: &mut u32) -> ValueId {
|
||||||
|
let vid = ValueId(*next_value_id);
|
||||||
|
*next_value_id += 1;
|
||||||
|
vid
|
||||||
|
}
|
||||||
|
|
||||||
|
let alloc_env_params =
|
||||||
|
|fields: &[String], next_value_id: &mut u32| -> Vec<ValueId> {
|
||||||
|
fields
|
||||||
|
.iter()
|
||||||
|
.map(|_| alloc_value_id(next_value_id))
|
||||||
|
.collect()
|
||||||
|
};
|
||||||
|
|
||||||
|
let build_env_map = |fields: &[String], params: &[ValueId]| -> BTreeMap<String, ValueId> {
|
||||||
|
let mut env = BTreeMap::new();
|
||||||
|
for (name, vid) in fields.iter().zip(params.iter()) {
|
||||||
|
env.insert(name.clone(), *vid);
|
||||||
|
}
|
||||||
|
env
|
||||||
|
};
|
||||||
|
|
||||||
|
let collect_env_args = |fields: &[String], env: &BTreeMap<String, ValueId>| -> Result<Vec<ValueId>, String> {
|
||||||
|
let mut args = Vec::with_capacity(fields.len());
|
||||||
|
for name in fields {
|
||||||
|
let vid = env.get(name).copied().ok_or_else(|| {
|
||||||
|
error_tags::freeze_with_hint(
|
||||||
|
"phase131/loop_true/env_missing",
|
||||||
|
&format!("env missing required field '{name}'"),
|
||||||
|
"ensure env layout and env map are built from the same SSOT field list",
|
||||||
|
)
|
||||||
|
})?;
|
||||||
|
args.push(vid);
|
||||||
|
}
|
||||||
|
Ok(args)
|
||||||
|
};
|
||||||
|
|
||||||
|
let mut next_value_id: u32 = 1;
|
||||||
|
|
||||||
|
// Function IDs (stable, dev-only)
|
||||||
|
let main_id = JoinFuncId::new(0);
|
||||||
|
let loop_step_id = JoinFuncId::new(1);
|
||||||
|
let loop_body_id = JoinFuncId::new(2);
|
||||||
|
let k_exit_id = JoinFuncId::new(3);
|
||||||
|
|
||||||
|
// main(env): <prefix> → TailCall(loop_step, env)
|
||||||
|
let main_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||||
|
let mut env_main = build_env_map(&env_fields, &main_params);
|
||||||
|
let mut main_func = JoinFunction::new(main_id, "main".to_string(), main_params);
|
||||||
|
|
||||||
|
// Lower prefix (pre-loop) statements into main
|
||||||
|
for n in prefix_nodes {
|
||||||
|
match n {
|
||||||
|
StepNode::Stmt { kind, .. } => match kind {
|
||||||
|
StepStmtKind::Assign { target, value_ast } => {
|
||||||
|
if LegacyLowerer::lower_assign_stmt(
|
||||||
|
target,
|
||||||
|
value_ast,
|
||||||
|
&mut main_func.body,
|
||||||
|
&mut next_value_id,
|
||||||
|
&mut env_main,
|
||||||
|
)
|
||||||
|
.is_err()
|
||||||
|
{
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepStmtKind::LocalDecl { .. } => {}
|
||||||
|
_ => {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
},
|
||||||
|
_ => {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// main → loop_step tailcall
|
||||||
|
let main_args = collect_env_args(&env_fields, &env_main)?;
|
||||||
|
main_func.body.push(JoinInst::Call {
|
||||||
|
func: loop_step_id,
|
||||||
|
args: main_args,
|
||||||
|
k_next: None,
|
||||||
|
dst: None,
|
||||||
|
});
|
||||||
|
|
||||||
|
// loop_step(env): if true { TailCall(loop_body, env) } else { TailCall(k_exit, env) }
|
||||||
|
let loop_step_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||||
|
let env_loop_step = build_env_map(&env_fields, &loop_step_params);
|
||||||
|
let mut loop_step_func = JoinFunction::new(loop_step_id, "loop_step".to_string(), loop_step_params);
|
||||||
|
|
||||||
|
// Generate condition: true
|
||||||
|
let cond_vid = alloc_value_id(&mut next_value_id);
|
||||||
|
loop_step_func.body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||||
|
dst: cond_vid,
|
||||||
|
value: ConstValue::Bool(true),
|
||||||
|
}));
|
||||||
|
|
||||||
|
// Conditional jump: if true → loop_body, else → k_exit
|
||||||
|
let loop_step_args = collect_env_args(&env_fields, &env_loop_step)?;
|
||||||
|
loop_step_func.body.push(JoinInst::Jump {
|
||||||
|
cont: loop_body_id.as_cont(),
|
||||||
|
args: loop_step_args.clone(),
|
||||||
|
cond: Some(cond_vid),
|
||||||
|
});
|
||||||
|
loop_step_func.body.push(JoinInst::Jump {
|
||||||
|
cont: k_exit_id.as_cont(),
|
||||||
|
args: loop_step_args,
|
||||||
|
cond: None,
|
||||||
|
});
|
||||||
|
|
||||||
|
// loop_body(env): <assign statements> → TailCall(k_exit, env)
|
||||||
|
let loop_body_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||||
|
let mut env_loop_body = build_env_map(&env_fields, &loop_body_params);
|
||||||
|
let mut loop_body_func = JoinFunction::new(loop_body_id, "loop_body".to_string(), loop_body_params);
|
||||||
|
|
||||||
|
// Lower body statements
|
||||||
|
for n in body_prefix {
|
||||||
|
match n {
|
||||||
|
StepNode::Stmt { kind, .. } => match kind {
|
||||||
|
StepStmtKind::Assign { target, value_ast } => {
|
||||||
|
if LegacyLowerer::lower_assign_stmt(
|
||||||
|
target,
|
||||||
|
value_ast,
|
||||||
|
&mut loop_body_func.body,
|
||||||
|
&mut next_value_id,
|
||||||
|
&mut env_loop_body,
|
||||||
|
)
|
||||||
|
.is_err()
|
||||||
|
{
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepStmtKind::LocalDecl { .. } => {}
|
||||||
|
_ => {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
},
|
||||||
|
_ => {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// loop_body → k_exit tailcall
|
||||||
|
let loop_body_args = collect_env_args(&env_fields, &env_loop_body)?;
|
||||||
|
loop_body_func.body.push(JoinInst::Call {
|
||||||
|
func: k_exit_id,
|
||||||
|
args: loop_body_args,
|
||||||
|
k_next: None,
|
||||||
|
dst: None,
|
||||||
|
});
|
||||||
|
|
||||||
|
// k_exit(env): handle post-loop or return
|
||||||
|
let k_exit_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||||
|
let env_k_exit = build_env_map(&env_fields, &k_exit_params);
|
||||||
|
let mut k_exit_func = JoinFunction::new(k_exit_id, "k_exit".to_string(), k_exit_params);
|
||||||
|
|
||||||
|
// Handle post-loop statements or return
|
||||||
|
if post_nodes.is_empty() {
|
||||||
|
// No post-loop: return void
|
||||||
|
k_exit_func.body.push(JoinInst::Ret { value: None });
|
||||||
|
} else if post_nodes.len() == 1 {
|
||||||
|
// Single post statement: check if it's a return
|
||||||
|
match &post_nodes[0] {
|
||||||
|
StepNode::Stmt { kind, .. } => match kind {
|
||||||
|
StepStmtKind::Return { value_ast } => {
|
||||||
|
if let Some(ast_handle) = value_ast {
|
||||||
|
// Return variable from env
|
||||||
|
if let Some(var_name) = Self::extract_variable_name(&ast_handle.0) {
|
||||||
|
if let Some(vid) = env_k_exit.get(&var_name).copied() {
|
||||||
|
k_exit_func.body.push(JoinInst::Ret { value: Some(vid) });
|
||||||
|
} else {
|
||||||
|
return Ok(None); // Variable not in env
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
return Ok(None); // Return value is not a variable
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
// Return void
|
||||||
|
k_exit_func.body.push(JoinInst::Ret { value: None });
|
||||||
|
}
|
||||||
|
}
|
||||||
|
_ => {
|
||||||
|
return Ok(None); // Unsupported post statement
|
||||||
|
}
|
||||||
|
},
|
||||||
|
_ => {
|
||||||
|
return Ok(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
return Ok(None); // Multiple post statements not supported
|
||||||
|
}
|
||||||
|
|
||||||
|
// Build module
|
||||||
|
let mut module = JoinModule::new();
|
||||||
|
module.add_function(main_func);
|
||||||
|
module.add_function(loop_step_func);
|
||||||
|
module.add_function(loop_body_func);
|
||||||
|
module.add_function(k_exit_func);
|
||||||
|
module.entry = Some(main_id);
|
||||||
|
module.mark_normalized();
|
||||||
|
|
||||||
|
Ok(Some((module, JoinFragmentMeta::empty())))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Extract loop(true) pattern from StepTree root
|
||||||
|
///
|
||||||
|
/// Returns: (prefix_nodes, loop_node, post_nodes)
|
||||||
|
fn extract_loop_true_pattern(root: &StepNode) -> Option<(&[StepNode], &StepNode, &[StepNode])> {
|
||||||
|
match root {
|
||||||
|
StepNode::Loop { .. } => {
|
||||||
|
// Loop is the only statement
|
||||||
|
Some((&[][..], root, &[][..]))
|
||||||
|
}
|
||||||
|
StepNode::Block(nodes) => {
|
||||||
|
// Find loop in block
|
||||||
|
for (i, node) in nodes.iter().enumerate() {
|
||||||
|
if matches!(node, StepNode::Loop { .. }) {
|
||||||
|
let prefix = &nodes[..i];
|
||||||
|
let post = &nodes[i + 1..];
|
||||||
|
return Some((prefix, node, post));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
None
|
||||||
|
}
|
||||||
|
_ => None,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Check if AST node is Bool(true) literal
|
||||||
|
fn is_bool_true_literal(ast: &ASTNode) -> bool {
|
||||||
|
matches!(
|
||||||
|
ast,
|
||||||
|
ASTNode::Literal {
|
||||||
|
value: LiteralValue::Bool(true),
|
||||||
|
..
|
||||||
|
}
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Check if body ends with break statement
|
||||||
|
fn body_ends_with_break(stmts: &[StepNode]) -> bool {
|
||||||
|
if let Some(last) = stmts.last() {
|
||||||
|
matches!(
|
||||||
|
last,
|
||||||
|
StepNode::Stmt {
|
||||||
|
kind: StepStmtKind::Break,
|
||||||
|
..
|
||||||
|
}
|
||||||
|
)
|
||||||
|
} else {
|
||||||
|
false
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Check if body has unsupported exits (return/continue)
|
||||||
|
fn has_unsupported_exits(stmts: &[StepNode]) -> bool {
|
||||||
|
for stmt in stmts {
|
||||||
|
match stmt {
|
||||||
|
StepNode::Stmt { kind, .. } => match kind {
|
||||||
|
StepStmtKind::Return { .. } | StepStmtKind::Continue => return true,
|
||||||
|
_ => {}
|
||||||
|
},
|
||||||
|
StepNode::Block(inner) => {
|
||||||
|
if Self::has_unsupported_exits(inner) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepNode::If { then_branch, else_branch, .. } => {
|
||||||
|
if Self::has_unsupported_exits_in_node(then_branch) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
if let Some(else_node) = else_branch {
|
||||||
|
if Self::has_unsupported_exits_in_node(else_node) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
_ => {}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
false
|
||||||
|
}
|
||||||
|
|
||||||
|
fn has_unsupported_exits_in_node(node: &StepNode) -> bool {
|
||||||
|
match node {
|
||||||
|
StepNode::Stmt { kind, .. } => matches!(kind, StepStmtKind::Return { .. } | StepStmtKind::Continue),
|
||||||
|
StepNode::Block(stmts) => Self::has_unsupported_exits(stmts),
|
||||||
|
StepNode::If { then_branch, else_branch, .. } => {
|
||||||
|
Self::has_unsupported_exits_in_node(then_branch)
|
||||||
|
|| else_branch.as_ref().map_or(false, |n| Self::has_unsupported_exits_in_node(n))
|
||||||
|
}
|
||||||
|
_ => false,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Extract variable name from AST node
|
||||||
|
fn extract_variable_name(ast: &ASTNode) -> Option<String> {
|
||||||
|
match ast {
|
||||||
|
ASTNode::Variable { name, .. } => Some(name.clone()),
|
||||||
|
_ => None,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
@ -34,6 +34,7 @@ pub mod contracts;
|
|||||||
pub mod normalized_verifier;
|
pub mod normalized_verifier;
|
||||||
pub mod env_layout;
|
pub mod env_layout;
|
||||||
pub mod if_as_last_join_k;
|
pub mod if_as_last_join_k;
|
||||||
|
pub mod loop_true_break_once; // Phase 131: loop(true) break-once
|
||||||
pub mod post_if_post_k; // Phase 129-C: post-if with post_k continuation
|
pub mod post_if_post_k; // Phase 129-C: post-if with post_k continuation
|
||||||
pub mod legacy;
|
pub mod legacy;
|
||||||
pub mod dev_pipeline;
|
pub mod dev_pipeline;
|
||||||
|
|||||||
Reference in New Issue
Block a user