feat(joinir): add progress carrier verification for skip_ws (Phase 29 L-5.2)
Implement zero-progress backedge detection for JoinIR loops: - Create verify.rs module with ProgressError enum - verify_progress_for_skip_ws() checks BinOp::Add before recursive calls - Hook into joinir_runner_standalone_skip_ws test (NYASH_JOINIR_EXPERIMENT=1) - Currently warning-only, will upgrade to error in Phase 30 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
This commit is contained in:
@ -27,11 +27,17 @@ use crate::mir::ValueId;
|
||||
// Phase 27.9: Lowering submodule
|
||||
pub mod lowering;
|
||||
|
||||
// Phase 29 L-5.2: Progress verification
|
||||
pub mod verify;
|
||||
|
||||
// Re-export lowering functions for backward compatibility
|
||||
pub use lowering::{
|
||||
lower_funcscanner_trim_to_joinir, lower_min_loop_to_joinir, lower_skip_ws_to_joinir,
|
||||
};
|
||||
|
||||
// Re-export verification functions
|
||||
pub use verify::verify_progress_for_skip_ws;
|
||||
|
||||
/// JoinIR 関数ID(MIR 関数とは別 ID でもよい)
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
||||
pub struct JoinFuncId(pub u32);
|
||||
|
||||
274
src/mir/join_ir/verify.rs
Normal file
274
src/mir/join_ir/verify.rs
Normal file
@ -0,0 +1,274 @@
|
||||
//! JoinIR Progress Carrier Verification (Phase 29 L-5.2)
|
||||
//!
|
||||
//! # Purpose
|
||||
//!
|
||||
//! ループの「進捗キャリア」が backedge で必ず更新されていることを検証する。
|
||||
//! ゼロ進捗 backedge(progress carrier が変化しない再帰呼び出し)を検出し、
|
||||
//! 無限ループの可能性を早期に警告する。
|
||||
//!
|
||||
//! # Phase 29 Strategy
|
||||
//!
|
||||
//! - まずは minimal skip_ws JoinIR のみを対象に、dev モードで警告を出す。
|
||||
//! - 将来(Phase 30)では Verifier エラーに格上げする予定。
|
||||
//!
|
||||
//! # Usage
|
||||
//!
|
||||
//! ```ignore
|
||||
//! // NYASH_JOINIR_EXPERIMENT=1 のときのみ有効
|
||||
//! if let Err(e) = verify_progress_for_skip_ws(&join_module) {
|
||||
//! eprintln!("[joinir/progress] warning: {:?}", e);
|
||||
//! }
|
||||
//! ```
|
||||
|
||||
use crate::mir::join_ir::{BinOpKind, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
|
||||
use crate::mir::ValueId;
|
||||
|
||||
/// Progress verification error
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum ProgressError {
|
||||
/// Progress carrier is not updated before backedge (recursive call)
|
||||
ZeroProgressBackedge {
|
||||
/// Progress variable name (for diagnostics)
|
||||
progress_var: String,
|
||||
/// Loop function ID
|
||||
loop_func_id: JoinFuncId,
|
||||
/// The recursive call that doesn't update progress
|
||||
call_index: usize,
|
||||
},
|
||||
/// No recursive call found in loop function
|
||||
NoRecursiveCall {
|
||||
loop_func_id: JoinFuncId,
|
||||
},
|
||||
/// Progress carrier not found
|
||||
ProgressCarrierNotFound {
|
||||
expected_param_index: usize,
|
||||
loop_func_id: JoinFuncId,
|
||||
},
|
||||
}
|
||||
|
||||
/// Verify progress carrier for skip_ws JoinIR (Phase 29 minimal version)
|
||||
///
|
||||
/// This function checks that:
|
||||
/// 1. The loop_step function has a recursive call
|
||||
/// 2. The progress carrier (i, typically the 3rd parameter) is updated via BinOp::Add
|
||||
/// before the recursive call
|
||||
///
|
||||
/// # Arguments
|
||||
///
|
||||
/// * `join_module` - The JoinModule containing skip_ws functions
|
||||
///
|
||||
/// # Returns
|
||||
///
|
||||
/// Ok(()) if progress carrier is properly updated, Err(ProgressError) otherwise.
|
||||
///
|
||||
/// # Skip_ws Structure Expected
|
||||
///
|
||||
/// ```text
|
||||
/// fn loop_step(s: Str, n: Int, i: Int) -> Int {
|
||||
/// if i >= n { return i }
|
||||
/// let ch = s.substring(i, i+1)
|
||||
/// if ch != " " { return i }
|
||||
/// let next_i = i + 1 // ← progress update
|
||||
/// loop_step(s, n, next_i) // ← recursive call with updated progress
|
||||
/// }
|
||||
/// ```
|
||||
pub fn verify_progress_for_skip_ws(join_module: &JoinModule) -> Result<(), ProgressError> {
|
||||
// skip_ws では loop_step が JoinFuncId(1)
|
||||
let loop_func_id = JoinFuncId::new(1);
|
||||
|
||||
let loop_func = match join_module.functions.get(&loop_func_id) {
|
||||
Some(f) => f,
|
||||
None => {
|
||||
// loop_step 関数が無ければ検証スキップ(エラーではない)
|
||||
return Ok(());
|
||||
}
|
||||
};
|
||||
|
||||
// skip_ws の progress carrier は 3番目のパラメータ (i)
|
||||
// params = [s, n, i] → index 2
|
||||
let progress_param_index = 2;
|
||||
let progress_param = match loop_func.params.get(progress_param_index) {
|
||||
Some(&p) => p,
|
||||
None => {
|
||||
return Err(ProgressError::ProgressCarrierNotFound {
|
||||
expected_param_index: progress_param_index,
|
||||
loop_func_id,
|
||||
});
|
||||
}
|
||||
};
|
||||
|
||||
// 1. 再帰呼び出し(loop_step への Call)を探す
|
||||
let mut recursive_call_indices: Vec<usize> = Vec::new();
|
||||
for (idx, inst) in loop_func.body.iter().enumerate() {
|
||||
if let JoinInst::Call { func, .. } = inst {
|
||||
if *func == loop_func_id {
|
||||
recursive_call_indices.push(idx);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if recursive_call_indices.is_empty() {
|
||||
return Err(ProgressError::NoRecursiveCall { loop_func_id });
|
||||
}
|
||||
|
||||
// 2. 再帰呼び出しの前に progress carrier が更新されているか確認
|
||||
// 「BinOp::Add で progress_param を使った演算がある」ことを保守的にチェック
|
||||
for &call_idx in &recursive_call_indices {
|
||||
let has_progress_update =
|
||||
check_progress_update_before(&loop_func.body[..call_idx], progress_param);
|
||||
|
||||
if !has_progress_update {
|
||||
return Err(ProgressError::ZeroProgressBackedge {
|
||||
progress_var: format!("param[{}]", progress_param_index),
|
||||
loop_func_id,
|
||||
call_index: call_idx,
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// Check if there's a BinOp::Add that uses the progress parameter before the call
|
||||
///
|
||||
/// This is a conservative check: we look for any BinOp::Add where progress_param
|
||||
/// is the LHS. The result should be used as an argument to the recursive call.
|
||||
fn check_progress_update_before(instructions: &[JoinInst], progress_param: ValueId) -> bool {
|
||||
for inst in instructions {
|
||||
if let JoinInst::Compute(MirLikeInst::BinOp {
|
||||
op: BinOpKind::Add,
|
||||
lhs,
|
||||
..
|
||||
}) = inst
|
||||
{
|
||||
if *lhs == progress_param {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
/// Verify progress carrier for a generic loop (future extension)
|
||||
///
|
||||
/// This is a placeholder for Phase 30 where we'll support arbitrary loops.
|
||||
#[allow(dead_code)]
|
||||
pub fn verify_progress_generic(
|
||||
_join_module: &JoinModule,
|
||||
_loop_func_id: JoinFuncId,
|
||||
_progress_param_index: usize,
|
||||
) -> Result<(), ProgressError> {
|
||||
// Phase 30: 汎用ループの progress チェック
|
||||
// 現在は未実装(skip_ws 専用版のみ)
|
||||
Ok(())
|
||||
}
|
||||
|
||||
// ============================================================================
|
||||
// Unit Tests
|
||||
// ============================================================================
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::mir::join_ir::{ConstValue, JoinFunction, JoinModule};
|
||||
|
||||
fn build_valid_skip_ws_loop() -> JoinModule {
|
||||
let mut module = JoinModule::new();
|
||||
|
||||
// loop_step(s, n, i) with proper progress update
|
||||
let loop_func_id = JoinFuncId::new(1);
|
||||
let s_param = ValueId(4000);
|
||||
let n_param = ValueId(4001);
|
||||
let i_param = ValueId(4002);
|
||||
let const_1 = ValueId(4010);
|
||||
let next_i = ValueId(4011);
|
||||
|
||||
let mut loop_func = JoinFunction::new(
|
||||
loop_func_id,
|
||||
"loop_step".to_string(),
|
||||
vec![s_param, n_param, i_param],
|
||||
);
|
||||
|
||||
// const 1
|
||||
loop_func.body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: const_1,
|
||||
value: ConstValue::Integer(1),
|
||||
}));
|
||||
|
||||
// next_i = i + 1 (progress update)
|
||||
loop_func.body.push(JoinInst::Compute(MirLikeInst::BinOp {
|
||||
dst: next_i,
|
||||
op: BinOpKind::Add,
|
||||
lhs: i_param, // progress carrier as LHS
|
||||
rhs: const_1,
|
||||
}));
|
||||
|
||||
// recursive call: loop_step(s, n, next_i)
|
||||
loop_func.body.push(JoinInst::Call {
|
||||
func: loop_func_id,
|
||||
args: vec![s_param, n_param, next_i],
|
||||
k_next: None,
|
||||
dst: None,
|
||||
});
|
||||
|
||||
module.add_function(loop_func);
|
||||
module
|
||||
}
|
||||
|
||||
fn build_invalid_skip_ws_loop() -> JoinModule {
|
||||
let mut module = JoinModule::new();
|
||||
|
||||
// loop_step(s, n, i) WITHOUT progress update
|
||||
let loop_func_id = JoinFuncId::new(1);
|
||||
let s_param = ValueId(4000);
|
||||
let n_param = ValueId(4001);
|
||||
let i_param = ValueId(4002);
|
||||
|
||||
let mut loop_func = JoinFunction::new(
|
||||
loop_func_id,
|
||||
"loop_step".to_string(),
|
||||
vec![s_param, n_param, i_param],
|
||||
);
|
||||
|
||||
// recursive call with SAME i (no progress!)
|
||||
loop_func.body.push(JoinInst::Call {
|
||||
func: loop_func_id,
|
||||
args: vec![s_param, n_param, i_param], // i is not updated!
|
||||
k_next: None,
|
||||
dst: None,
|
||||
});
|
||||
|
||||
module.add_function(loop_func);
|
||||
module
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_valid_progress_passes() {
|
||||
let module = build_valid_skip_ws_loop();
|
||||
let result = verify_progress_for_skip_ws(&module);
|
||||
assert!(result.is_ok(), "Valid progress should pass: {:?}", result);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_zero_progress_detected() {
|
||||
let module = build_invalid_skip_ws_loop();
|
||||
let result = verify_progress_for_skip_ws(&module);
|
||||
assert!(result.is_err(), "Zero progress should be detected");
|
||||
match result {
|
||||
Err(ProgressError::ZeroProgressBackedge { .. }) => {
|
||||
// Expected
|
||||
}
|
||||
other => panic!("Expected ZeroProgressBackedge, got {:?}", other),
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_empty_module_ok() {
|
||||
let module = JoinModule::new();
|
||||
let result = verify_progress_for_skip_ws(&module);
|
||||
assert!(
|
||||
result.is_ok(),
|
||||
"Empty module should pass (no loop_step to verify)"
|
||||
);
|
||||
}
|
||||
}
|
||||
@ -11,6 +11,7 @@
|
||||
// - ArrayBox/MapBox は未実装 (joinir_coverage.md A-2.5 参照)
|
||||
|
||||
use crate::mir::join_ir::*;
|
||||
use crate::mir::join_ir::verify::verify_progress_for_skip_ws;
|
||||
use crate::mir::join_ir_runner::{run_joinir_function, JoinValue};
|
||||
|
||||
fn require_experiment_toggle() -> bool {
|
||||
@ -48,7 +49,6 @@ fn require_experiment_toggle() -> bool {
|
||||
/// - Input: "" → Output: 0 (空文字列)
|
||||
/// - Input: "abc" → Output: 0 (空白なし)
|
||||
#[test]
|
||||
#[ignore]
|
||||
fn joinir_runner_standalone_skip_ws() {
|
||||
if !require_experiment_toggle() {
|
||||
return;
|
||||
@ -56,6 +56,18 @@ fn joinir_runner_standalone_skip_ws() {
|
||||
|
||||
let join_module = build_skip_ws_joinir();
|
||||
|
||||
// Phase 29 L-5.2: Progress carrier verification
|
||||
// まずは警告のみ(将来 Phase 30 でエラーに格上げ予定)
|
||||
match verify_progress_for_skip_ws(&join_module) {
|
||||
Ok(()) => {
|
||||
eprintln!("[joinir/progress] ✅ skip_ws progress carrier check passed");
|
||||
}
|
||||
Err(e) => {
|
||||
eprintln!("[joinir/progress] ⚠️ warning: {:?}", e);
|
||||
// Phase 29: 警告のみ、panic しない
|
||||
}
|
||||
}
|
||||
|
||||
// S-5.2-improved: Create MirInterpreter instance for VM integration
|
||||
let mut vm = crate::backend::mir_interpreter::MirInterpreter::new();
|
||||
|
||||
|
||||
Reference in New Issue
Block a user