feat(analyzer): diagnose modification of for-loop bounds

[tignear]

Status and request for feedback

I started this PR with the expectation that checking the continuation-bound reads against writes in the loop body would be a reasonably local analyzer change.

While implementing and reviewing it, the problem turned out to be substantially larger:

• direct procedural mutation can be checked locally;
• indirect combinational feedback depends on the whole combinational dependency analysis;
• the current DAG analyzer deliberately omits several classes of dependencies;
• opaque and cross-hierarchy effects require an explicit unknown or incomplete result; and
• time-advancing testbench loops require a different event-mediated analysis.

The current patch detects a useful subset of problematic loops, but it does not appear to solve the underlying problem, and extending it further in its current form risks duplicating or further coupling several existing dependency collectors.

I am therefore not attached to merging this implementation, or even to keeping this exact diagnostic design. I opened the PR because the local check initially seemed like a reasonable first step, but the investigation has made it much less clear that this is the right architectural direction.

If anyone has a cleaner language rule, dependency-analysis model, migration strategy, or entirely different approach, please comment. I would be happy for this PR to be replaced or closed if it helps converge on a more complete solution.

Summary

Add the mutable_for_bound warning when the analyzer can establish that a procedural for loop body immediately writes storage read by its continuation bound.

var limit: u32 = 4;

for i in 0..limit {
    limit = 1; // warning: mutable_for_bound
}

Assignments unrelated to the continuation bound remain valid. Writes with true FF/NBA semantics are also permitted because their updated values are not visible until after the current procedural execution completes.

always_ff (clk) {
    for i in 0..limit {
        limit = 1; // permitted: the new FF value is not visible in this loop
    }
}

Procedural locals inside always_ff still use immediate assignment semantics and are diagnosed when modified.

The warning can be suppressed during migration:

#[allow(mutable_for_bound)]
for i in 0..limit {
    limit = 1;
}

This PR intentionally implements only the immediate procedural-write check. It does not claim that every indirect or cross-hierarchy influence is currently diagnosed.

Motivation

Veryl currently does not document when a procedural for loop continuation bound is evaluated.

The native simulator captures the bound before entering the loop, while emitted SystemVerilog evaluates the continuation condition before each iteration. Modifying a bound from the loop body can therefore change the iteration count or termination behavior depending on the backend.

Rather than choosing one evaluation strategy immediately, Veryl can preserve implementation freedom by diagnosing programs that can observe the difference.

For synthesizable code, the intended argument is:

• an immediate procedural write to storage read by the bound must be diagnosed;
• an indirect combinational path from a body write back to the bound forms a combinational cycle, because the bound also controls execution of that body write;
• a path through an FF/NBA boundary is not visible during the current loop execution; and
• a module input cannot be written by the current procedural execution.

Under a sound combinational DAG restriction, rejecting immediate procedural mutation is therefore sufficient to make capture-on-entry and per-iteration evaluation equivalent for ordinary synthesizable code.

This PR addresses the immediate-mutation part of that argument.

Why this is initially a warning

The direct check implemented here is deliberately conservative but incomplete.

It currently handles:

• module and procedural variables;
• statically known array elements and bit ranges;
• conservative whole-object aliasing for dynamic indices and selects;
• writes in nested control flow and nested loops;
• function output arguments;
• reads and writes reached through known Veryl function bodies; and
• the distinction between immediate procedural writes and FF/NBA writes.

It does not construct the complete combinational dependency relation of the elaborated design. In particular, this checker does not independently resolve:

• indirect feedback through other combinational variables or module ports;
• cross-hierarchy aliases and instance connectivity;
• hierarchical testbench storage;
• effects hidden behind opaque or unsupported IR nodes;
• testbench or external component method effects; or
• changes mediated by time advancement or event execution.

Some indirect cases should already be rejected by Veryl's combinational-loop rule. However, the current combinational-loop analyzer also contains deliberate under-detection paths. Among other cases, it may omit dependencies involving SystemVerilog black boxes, inout ports, oversized arrays, or modules whose assignment analysis was suppressed.

Consequently, an indirect feedback path that is invalid according to the language-level DAG rule may still be missed by the current implementation. This PR plus the existing DAG analyzer therefore does not yet guarantee that every warning-free program is independent of the bound-evaluation strategy.

Making the new diagnostic a warning exposes the known immediate cases without presenting the surrounding dependency analysis as complete or immediately rejecting existing programs.

Intended diagnostic model

The eventual analysis should distinguish three outcomes:

Analysis result	Diagnostic
A forbidden immediate mutation or combinational feedback is established	Error
Stability is established	No diagnostic
The relevant dependency or effect analysis is incomplete	Warning

Improving analysis precision may refine a warning into either an error or no diagnostic. An analysis limitation must not be represented by silently dropping dependency edges and treating the result as proof of stability.

This does not require a flat whole-design graph. A future implementation can use total module-local dependency graphs and compositional module summaries which preserve an explicit incomplete or unknown result.

The warning introduced by this PR is a first migration step toward that model.

Testbench code

The warning also applies to known immediate mutation in testbench loops because such code would directly observe the same evaluation-strategy choice.

The synthesizable-code DAG argument does not extend to time-advancing testbench bodies. A testbench may yield, update FF state, or observe changed DUT outputs before the next continuation test without creating a combinational cycle.

This PR does not attempt that event-mediated analysis. Such cases may require a separate conservative warning based on event and write closures.

Alternatives considered

Re-evaluate the bound in the native simulator

The simulator could match emitted SystemVerilog by evaluating the continuation bound before every iteration.

This would define useful behavior for a fragile pattern and would impose repeated evaluation in the common case unless each simulator backend performed loop-invariance analysis.

Capture the bound in emitted SystemVerilog

The emitter could introduce a temporary which captures the continuation bound before entering the loop.

This would match the current native simulator but make emitted SystemVerilog more verbose and commit Veryl to capture-on-entry semantics.

Specify one-time range evaluation

Rust, whose range syntax Veryl resembles, evaluates the range expression before iteration.

Veryl currently has no documented semantics under which mutating a continuation bound is useful. Choosing this model would constrain future backends even though well-formed programs need not observe the choice.

Expand this PR into a complete dependency-analysis rewrite

A complete solution could replace the current overlapping dependency collectors with a total, sound, conservative dependency representation shared by combinational-loop detection and continuation-bound analysis.

That is substantially larger than this diagnostic and should be handled separately. This PR keeps the directly observable procedural case visible while that design is considered.

Compatibility and future work

Programs diagnosed by this PR remain accepted and produce a warning. The warning may be suppressed with #[allow(mutable_for_bound)].

Known immediate mutation can be promoted to an error after the language rule and migration policy are agreed. Analysis-incomplete cases should remain warnings until they can be resolved conservatively.

A warning-free-program guarantee additionally requires the combinational dependency analysis to stop silently omitting relevant edges. That work is not part of this PR.

[codspeed-hq]

Merging this PR will not alter performance

✅ 8 untouched benchmarks

---

_{Comparing tignear:fix/reevaluate-dynamic-for-bound (d3147fe) with master (b22fb96)}