From 89279f9981ea897bc4f32812b81a1f27de94ecee Mon Sep 17 00:00:00 2001 From: "David E. Weekly" Date: Fri, 18 Sep 2026 17:24:32 -0700 Subject: [PATCH] fix(origins): widen loop-carried values instead of exhausting the step budget The origin lattice has unbounded height. A loop-carried `i = i + 1` merges at the loop head to `Alternatives[0, ADD(0, 1)]`; the transfer then yields `ADD(Alternatives[..], 1)`, which the next merge adds as a further option, one nesting level per pass. Every iteration is strictly larger than the last, so `state != out_states[block]` never stops firing and the worklist terminates only by exhausting MAX_TRANSFER_STEPS. `analyze_proto_tree` then reports *every* call in that prototype as `analysis-limit`, including the arguments that converged on the first visit. Widening bounds the iteration: after a block's outgoing state has changed MAX_BLOCK_REVISITS times, the slots still moving are raised to the top of the lattice. Slots that already converged keep their exact expression, so a prototype containing a loop still resolves everything outside it. Measured on a 524-instruction, 116-block prototype from extracted router firmware, where 0.2.0 resolved the arguments and 0.3.0 did not: before proto=0/31 steps=1000001 exhausted=true 117 analysis-limit, 15.85s after proto=0/31 converges 0 analysis-limit, 0.19s and across a 260-file corpus, `analysis-limit` falls from 144 to 17 with no argument losing an expression it previously had. The regression test asserts the mechanism rather than the symptom: a loop-carried accumulator must widen to `ControlFlowConflict`, not grow until `ExpressionDepthLimit` truncates it. A synthetic fixture large enough to exhaust the step budget outright was not reproducible at a reasonable size, and the firmware that does reproduce it is not a public sample. The test fails without this change and passes with it. `tests/fixtures/origins.lua` is untouched so the pinned origin-matrix cardinality gate still holds. --- crates/luad-analysis/src/origins.rs | 37 ++++++++++ .../tests/test_argument_origins_lua51.rs | 71 +++++++++++++++++++ tests/fixtures/origins_loop_widening.lua | 27 +++++++ 3 files changed, 135 insertions(+) create mode 100644 tests/fixtures/origins_loop_widening.lua diff --git a/crates/luad-analysis/src/origins.rs b/crates/luad-analysis/src/origins.rs index 26f502f..16e0062 100644 --- a/crates/luad-analysis/src/origins.rs +++ b/crates/luad-analysis/src/origins.rs @@ -18,6 +18,17 @@ const MAX_TRANSFER_STEPS: usize = 1_000_000; const MAX_TABLE_SCAN_STEPS: usize = 64; const MAX_TABLE_FIELDS: usize = 64; const MAX_ALTERNATIVES: usize = 8; +/// How many times a block's outgoing state may change before its still-moving slots are +/// widened to `Unknown`. +/// +/// The origin lattice has unbounded height: a loop-carried `i = i + 1` merges to +/// `Alternatives[0, ADD(0, 1)]`, whose transfer yields `ADD(Alternatives[..], 1)`, which +/// the next merge adds as a further option. Each pass is strictly larger than the last, so +/// the worklist never reaches a fixpoint and terminates only by exhausting its step budget, +/// which reports every call in the prototype as `analysis-limit`. Widening bounds the +/// iteration instead, so a prototype containing a loop still resolves the expressions that +/// do converge. +const MAX_BLOCK_REVISITS: usize = 8; /// A lossless literal suitable for structural equality in an origin graph. #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, JsonSchema)] @@ -289,6 +300,7 @@ fn run_dataflow( let mut queued: BTreeSet = worklist.iter().copied().collect(); let mut steps = 0usize; let mut exhausted = false; + let mut revisits = vec![0usize; cfg.blocks.len()]; while let Some(block_index) = worklist.pop_front() { queued.remove(&block_index); let block = &cfg.blocks[block_index]; @@ -316,6 +328,31 @@ fn run_dataflow( break; } if state != out_states[block_index] { + revisits[block_index] = revisits[block_index].saturating_add(1); + if revisits[block_index] > MAX_BLOCK_REVISITS { + // Widen: every slot still moving at this point is loop-carried and is not + // going to settle, so raise it to the top of the lattice. Slots that have + // already converged keep their exact expression. + for (slot, previous) in state.iter_mut().zip(out_states[block_index].iter()) { + if slot != previous { + let evidence = match (&slot, previous) { + (FlowValue::Origin(next), FlowValue::Origin(prior)) => next + .evidence + .iter() + .chain(prior.evidence.iter()) + .cloned() + .collect::>(), + (FlowValue::Origin(next), _) => next.evidence.clone(), + (_, FlowValue::Origin(prior)) => prior.evidence.clone(), + _ => Vec::new(), + }; + *slot = FlowValue::Origin(unknown( + OriginUnknownReason::ControlFlowConflict, + evidence, + )); + } + } + } out_states[block_index] = state; for edge in &block.successors { if cfg.blocks[edge.to_block].is_reachable && queued.insert(edge.to_block) { diff --git a/crates/luad-oracle/tests/test_argument_origins_lua51.rs b/crates/luad-oracle/tests/test_argument_origins_lua51.rs index 7f08611..a2203bd 100644 --- a/crates/luad-oracle/tests/test_argument_origins_lua51.rs +++ b/crates/luad-oracle/tests/test_argument_origins_lua51.rs @@ -990,3 +990,74 @@ sink(function() end) assert_eq!(val["prototype"], "0/1"); assert_eq!(val["evidence"], serde_json::json!(["proto:0:pc:2"])); } + +fn loop_widening_chunk() -> luad_core::Chunk { + let _ = luad_oracle::require_luac51(); + let root = luad_oracle::find_workspace_root(); + let source = std::fs::read_to_string(root.join("tests/fixtures/origins_loop_widening.lua")) + .expect("read origins_loop_widening.lua"); + luad_oracle::compile_and_parse_lua51(&source, false).expect("compile loop widening fixture") +} + +#[test] +fn test_loop_carried_values_widen_rather_than_growing_without_bound() { + let analysis = analyze_chunk_origins(&loop_widening_chunk()); + let origins = fixed_origins(&analysis); + assert!(!origins.is_empty(), "fixture must produce fixed arguments"); + + // The loop-carried accumulator cannot be bounded, so it must be widened to the top of + // the lattice at the loop head. Reaching `ExpressionDepthLimit` instead means the + // merge kept nesting `ADD(Alternatives[..], 1)` one level per iteration until the + // expression bounds truncated it, which is the unbounded-height behaviour widening + // exists to prevent; on a prototype with enough blocks that same growth exhausts the + // worklist step budget and reports every call as `analysis-limit`. + let widened = origins.iter().any(|origin| { + matches!( + &origin.kind, + OriginExpressionKind::Unknown { + reason: OriginUnknownReason::ControlFlowConflict + } + ) + }); + let ground_out = origins.iter().any(|origin| { + matches!( + &origin.kind, + OriginExpressionKind::Unknown { + reason: OriginUnknownReason::ExpressionDepthLimit + } + ) + }); + assert!( + widened && !ground_out, + "loop-carried value must widen to control-flow-conflict, not grow to a depth limit" + ); + + // No argument may be reported as `analysis-limit`. + for origin in &origins { + assert!( + !matches!( + &origin.kind, + OriginExpressionKind::Unknown { + reason: OriginUnknownReason::AnalysisLimit + } + ), + "an argument reported analysis-limit; the worklist ran out of steps" + ); + } + + // An argument that is not loop-carried keeps its exact expression. + let concat = origins + .iter() + .find(|origin| matches!(&origin.kind, OriginExpressionKind::Concat { .. })) + .expect("the post-loop sink argument must resolve to a concat"); + let OriginExpressionKind::Concat { parts } = &concat.kind else { + unreachable!("filtered above") + }; + assert_eq!(parts.len(), 3, "expected two literals and one field read"); + assert!( + matches!(&parts[2].kind, OriginExpressionKind::Field { base, .. } + if matches!(&base.kind, OriginExpressionKind::Parameter { .. })), + "the third part must be a field read off the parameter, got {:?}", + parts[2].kind + ); +} diff --git a/tests/fixtures/origins_loop_widening.lua b/tests/fixtures/origins_loop_widening.lua new file mode 100644 index 0000000..fae81b4 --- /dev/null +++ b/tests/fixtures/origins_loop_widening.lua @@ -0,0 +1,27 @@ +-- Loop-carried values make the origin lattice grow without bound. +-- +-- At the loop head the merge of `index` yields Alternatives[0, ADD(0, 1)]. The transfer +-- of `index = index + 1` then yields ADD(Alternatives[..], 1), which the next merge adds +-- as a further option, one nesting level per iteration. Nothing in the expression bounds +-- collapses that, so without widening the worklist never reaches a fixpoint and stops +-- only by exhausting its step budget, which reports every call in the prototype as +-- `analysis-limit` including the ones that converged immediately. +-- +-- The argument to the final sink is deliberately ordinary: two literals and a field read +-- off a parameter, none of it loop-carried. It must resolve. + +local function sink(...) end + +local function loop_counter(params) + local index = 0 + local total = 0 + while index < 10 do + index = index + 1 + total = total + index + end + sink(total) + sink("mkdir -p " .. "/tmp/widen/" .. params.opcode) + return total +end + +loop_counter({ opcode = "x" })