You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
gen-verilog: an early return inside a loop does not leave the loop -- 84 guard sites in 34 files, and no corpus file can demonstrate it #2989
An early return inside a loop sets a flag the loop never reads, so the loop keeps going -- and one of them does not terminate
The Verilog backend lowers return inside a loop body as "assign the function's
return variable, set __t27_ret", and guards only the FUNCTION-TAIL return with if (!__t27_ret). Nothing guards the loop. Verbatim from gen-verilog specs/isa/ternary_search.t27:
while ((lo < hi)) begin
mid = (lo + ((hi - lo) /2));
if ((data[mid] == target)) begin
binary_search = $signed(mid);
__t27_ret =1'b1; // <-- flag set, loop NOT exited,endelseif ((data[mid] < target)) begin// lo and hi unchanged
lo = (mid +1);
endelsebegin
hi = mid;
endendif (!__t27_ret) begin
binary_search =-1;
__t27_ret =1'b1;
end
On a hit neither lo nor hi moves, so while ((lo < hi))spins forever.
On a miss it terminates and is correct.
linear_search in the same file has the terminating variant of the same defect:
it runs to the end of the array and returns the LAST match where the source says
the first.
Population
55 sites across 24 of the 581 generated .v files (a scan tracking begin/end
depth from each loop header and counting __t27_ret = 1'b1; inside). Largest: specs_math_property_test_template.v 11, specs_compiler_stdlib.v 8, specs_isa_ternary_hash.v 5, specs_pins_ir.v 4.
55 is the size of the CLASS, not 55 proven-wrong values. An early return in a
loop is only wrong when the loop can iterate again afterwards; the detector
over-counts by construction and this number should not be quoted as defects.
Two functions were read end to end and are demonstrably wrong.
C, Rust and Zig all return the first match on the same source.
Why nothing reported it
All 24 files fail iverilog today for unrelated reasons, and the one deep ruler
that would run them has had zero targets -- #2987. A non-terminating simulation
is also invisible to a compile-only gate by construction.
The repair is the same missing machinery as #2988: a named block per loop, so
the flag can disable it. Filing them separately because the populations differ
and the wrong-value consequence here is silent rather than a no-op.
Correction: the population is 75 sites in 33 files, not 55 in 24
I published 55 sites / 24 files in the issue body. That came from one scanner.
A later sweep ran two structurally independent scanners over the same 581-file
snapshot and both said 75 / 33. Two against one is not a decision, so I wrote
a third reader — begin/end depth tracked from each loop header, counting __t27_ret = 1'b1; that falls inside a loop body:
THIRD READING: 75 sites in 33 files
11 specs_math_property_test_template.v
9 specs_ar_asp_solver.v
8 specs_compiler_stdlib.v
5 specs_isa_ternary_hash.v
4 specs_pins_ir.v
Three readers, 75/33. The original scanner's per-file leaders were exact
where it looked — 11 / 8 / 5 / 4 — and it missed nine whole files, of which ar/asp_solver (9 sites) is the largest. A scanner that is right about every
file it reports and silent about a quarter of them is the harder failure to
notice, because every number you check is correct.
55 / 24 is withdrawn. 75 / 33 is the class size — and it is still the size
of the CLASS, not 75 proven-wrong values: an early return in an effectively-final
iteration is harmless.
Two things the sweep added that change how this should be fixed
The compiler's only test for this construct is loop-free
nested_return_lowers_as_early_exit (compiler.rs:40341) uses a source with no loop and passes. So the shape this issue is about has zero coverage,
and a fix could regress the tested shape without anything saying so. Any patch
here wants two new cases: a loop variant, and a variant whose matching branch
does not advance the induction variable — the binary_search shape.
Fixing the loop guard alone leaves linear_search wrong
In the demo spec, data: []i32 lowers to input [31:0] data — a 32-bit scalar, so data[i] is a bit-select, not an array element. That is a second,
independent defect in the same function. A reader who fixes the loop exit and
re-runs ternary_search will still get a wrong answer and may conclude the loop
fix did not work.
And the non-termination is proven, not inferred from a timeout
Instrumented, binary_search shows lo=0, hi=8, mid=4 unchanged past 2000
iterations — a fixed point, not slowness. Worth recording because "the simulator
timed out" and "the loop cannot terminate" are different claims and only the
second is this defect.
changed the title [-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (75 sites / 33 files)[/+]on Sep 3, 2026
Two corrections, and the first is that this defect has now been run
It reproduces and repairs end to end on THIS spec, not on a probe
An adversarial skeptic took specs/isa/ternary_search.t27, diagnosed the four unrelated emitter defects that keep it from elaborating — try eq(A,B)
emitted verbatim into Verilog, data.len lowered to the unbound identifier data_len, data: []i32 lowered to input [31:0] data so every data[x] is a
bit-select, and call sites passing data[0] — repaired them identically on
both sides with a substitution-count assertion (which fired twice and caught
two of its own errors), and confirmed by diff that the loop guard was the only
remaining difference:
stock : vvp exits 142 at 30s AND at 120s, no output
instrumented: iter=1 lo=0 hi=5 mid=2 ret=0
iter=2..5 lo=0 hi=5 mid=2 ret=1
iter=2000 lo=0 hi=5 mid=2 ret=1
patched : exit 0, [CHECK] got=2 want=2
Identical state at iteration 2000 as at iteration 2 — a measured fixed point,
not slowness. Split per function: linear_search returns 2 on both, so #2989
does not bite it; binary_search is the one that hangs.
A second skeptic repaired the same spec differently (8-element array, input [255:0] data, $signed(data[i*32 +: 32]), localparam integer data_len = 8), got the same hang, and added a negative
control: a miss returns −1 and finishes, rc=0. It also found a second symptom
class — linear_search([-1,-1,0,1,1,0,1,0], 1) returns 6, the last match,
where the language says 3. A third reproduced the wrong-answer form on master's
own emitter (t1(5,2): Verilog 4, C 2).
So this is two defects in one shape: non-termination when the loop cannot
advance, and the last-match-instead-of-first answer when it can. Shown three
times, by three people not looking for the same thing.
The population figure in the title is not confirmed
I corrected 55/24 to 75/33 and put it in the title. Three skeptics counted
independently and landed on 81–82 guarded loops across 32–33 files — but of generated .v, which is a different population from the .t27 source I
counted, over a corpus where 69 of 650 specs never reach .v at all. One
declined to count and said so. One named its own counter broken after it printed
152 sites / 40 files for stock and 99 / 38 for a tree differing in six files,
which cannot both be true.
The file count is corroborated at 32–33. The 75 is not confirmed by anybody,
including me — my third reader agreed with two others on 75/33 over .t27
source, and nothing has since checked that against the generated population.
Leaving the title as it is would be quoting an unconfirmed number, so: the
honest statement is 33 files, and a site count that has been measured two ways
over two populations and reconciled by nobody.
changed the title [-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (75 sites / 33 files)[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (33 files; site count unreconciled)[/+]on Sep 3, 2026
changed the title [-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (33 files; site count unreconciled)[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- 84 guard sites in 34 files, and no corpus file can demonstrate it[/+]on Sep 3, 2026
Three mutually inconsistent numbers on this issue, all reconciled by measurement. A design fan-out built three competing patches, and its judge ran a four-binary census over the carriers.
figure
where it came from
verdict
title 33 files
correct, but specs/ only
the 34th is compiler/runtime/runtime.t27, outside specs/
body 55 sites / 24 files
a while-only count
excluding Verilog for from the detector reproduces 23 files / 54 sites, and that variant's top-4 is this issue's list verbatim. It drops specs/ar/asp_solver.t27 (9 sites), the largest non-while carrier
my later 75 sites / 33 files
closer, still specs/-scoped, and undercounts
—
Measured truth: 34 files, 84 guard sites — 61 while conditions + 22 for body gates + 1 W700 inner if — plus 63 intra-iteration barriers. Say which denominator: 581 is the specs/ generation count, 643 is the whole tree of 745 .t27.
Two corrections to this issue's premise
1. No corpus file hangs. Measured with a hard per-file timeout over all 745 specs: zero timeouts. All 34 carriers exit in 0.02–0.07 s because iverilog refuses to elaborate them, and vvp never starts — 0 of 34 elaborate under any of four binaries, 0 newly broken, 0 newly fixed. specs/isa/ternary_search.t27 in particular is blocked by two unrelated defects: a try keyword leaked into the generated Verilog, and an undeclared data_len.
The spin is real as a mechanism — three independent authors reproduced it with a hand-written testbench (vvp rc 142 / 137 / killed-at-30s unguarded, versus rc 0 returning the right answer with !__t27_ret in the condition). Any commit saying "fixes the binary_search hang under vvp" is false as written. It fixes the mechanism, validated at the seam; the corpus has no oracle for this class today.
2. The better headline needs no hang.ternary_compare in specs/isa/ternary_arithmetic.t27 says "compare from most significant trit" and counts down. The loop runs past the returning trit, so the least significant differing trit's verdict wins: a sign inversion in a comparator, silent, terminating, no alarm.
What the fan-out settled about the repair
The body position is not sufficient, and all three designs measured it independently with one-variable experiments: on an unbounded while a body-position guard turns a wrong answer into a non-termination, because the body is what advances the loop.
And the three designs turned out not to be alternatives: the condition design is the exact disjoint union of the other two (61 + 22 + 1 = 84, union violations: none; byte-identical outputs on the overlaps). The body-only design moves the same 34 files, pays the same 72 seal rewrites, and delivers 25 of 84 guards.
One cost figure that does not exist: the gate-level price of a for body gate on a real carrier. 14 of 34 are yosys-readable and all 14 map to 0 cells in both versions. Every 25→51-cell number in circulation is from a hand-written toy.
The guard's price, measured: zero cells on every corpus instance
This was the open question left after #3021 landed — the dashboard stated it as
unmeasured on purpose, because every "25 → 51 cells" figure ever quoted here came
from a hand-written toy.
It is now settled, and the answer is settled by intersection, not by synthesis.
Intersection zero. None of these functions is instantiated, so both arms
synthesize to 4 cells / 0 LUTs. The 9 files / 20 sites for __t27_ret reproduce
independently by identity; the extra 2 files are __t27_brk gates from #2988, a
different feature.
Class 2 — the while-condition guard
This class was flagged as unpriced and is now priced:
Both were regenerated with the master compiler and with one built from the parent
commit. diff is exactly one line each, the guard term only — while (!__t27_ret && !spi_done) against while (!spi_done). Both fail yosys
elaboration identically in both arms.
What must not be quoted
"+9 cells" and "±10 cells, inside noise" are both prices of a toy with no
corpus instance. The first is worse than imprecise: the unguarded arm of that
toy computes a different function — iverilog returns index 0 guarded and 26
unguarded, last-match-wins, which is the bug #3021 fixes. You cannot buy that
saving.
Not measured, stated as such
No timing. Cells and LUTs only; Fmax was never read, and a guard inside a
loop body is a serialization question as much as an area one.
One toolchain.yosys stat estimates under synth_xilinx, not vendor
place-and-route. PR chore(zenodo): PASS-7 fix invalid ORCID + wrong community slug in .zenodo.json #599 showed every xc7 LUT figure here was 3× overstated
because synth_xilinx printed its own stats before the sampled ones; this repo
ships t27c yostat for exactly that reason. Absolute counts inherit the risk,
deltas taken by one reader on both arms do not.
Nothing on silicon. No board, no bitstream.
The reading that generalises
A construct's price is settled by intersection with what actually elaborates,
not by synthesizing an example of it. Eleven files carry the for-gate and 79
instantiate, and the two sets do not meet. That is a stronger and cheaper result
than any cell count, and it is the measurement that should have been taken first.
Activity
feat(tri): vsim funnel -- how far each spec gets when its Verilog is …
gHashTag commentedon Sep 3, 2026
Correction: the population is 75 sites in 33 files, not 55 in 24
I published 55 sites / 24 files in the issue body. That came from one scanner.
A later sweep ran two structurally independent scanners over the same 581-file
snapshot and both said 75 / 33. Two against one is not a decision, so I wrote
a third reader — begin/end depth tracked from each loop header, counting
__t27_ret = 1'b1;that falls inside a loop body:Three readers, 75/33. The original scanner's per-file leaders were exact
where it looked — 11 / 8 / 5 / 4 — and it missed nine whole files, of which
ar/asp_solver(9 sites) is the largest. A scanner that is right about everyfile it reports and silent about a quarter of them is the harder failure to
notice, because every number you check is correct.
55 / 24is withdrawn. 75 / 33 is the class size — and it is still the sizeof the CLASS, not 75 proven-wrong values: an early return in an effectively-final
iteration is harmless.
Two things the sweep added that change how this should be fixed
The compiler's only test for this construct is loop-free
nested_return_lowers_as_early_exit(compiler.rs:40341) uses a source withno loop and passes. So the shape this issue is about has zero coverage,
and a fix could regress the tested shape without anything saying so. Any patch
here wants two new cases: a loop variant, and a variant whose matching branch
does not advance the induction variable — the
binary_searchshape.Fixing the loop guard alone leaves
linear_searchwrongIn the demo spec,
data: []i32lowers toinput [31:0] data— a 32-bitscalar, so
data[i]is a bit-select, not an array element. That is a second,independent defect in the same function. A reader who fixes the loop exit and
re-runs
ternary_searchwill still get a wrong answer and may conclude the loopfix did not work.
And the non-termination is proven, not inferred from a timeout
Instrumented,
binary_searchshowslo=0, hi=8, mid=4unchanged past 2000iterations — a fixed point, not slowness. Worth recording because "the simulator
timed out" and "the loop cannot terminate" are different claims and only the
second is this defect.
Refs #2987, #2988
[-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (75 sites / 33 files)[/+]gHashTag commentedon Sep 3, 2026
Two corrections, and the first is that this defect has now been run
It reproduces and repairs end to end on THIS spec, not on a probe
An adversarial skeptic took
specs/isa/ternary_search.t27, diagnosed the fourunrelated emitter defects that keep it from elaborating —
try eq(A,B)emitted verbatim into Verilog,
data.lenlowered to the unbound identifierdata_len,data: []i32lowered toinput [31:0] dataso everydata[x]is abit-select, and call sites passing
data[0]— repaired them identically onboth sides with a substitution-count assertion (which fired twice and caught
two of its own errors), and confirmed by diff that the loop guard was the only
remaining difference:
Identical state at iteration 2000 as at iteration 2 — a measured fixed point,
not slowness. Split per function:
linear_searchreturns 2 on both, so #2989does not bite it;
binary_searchis the one that hangs.A second skeptic repaired the same spec differently (8-element array,
input [255:0] data,$signed(data[i*32 +: 32]),localparam integer data_len = 8), got the same hang, and added a negativecontrol: a miss returns −1 and finishes, rc=0. It also found a second symptom
class —
linear_search([-1,-1,0,1,1,0,1,0], 1)returns 6, the last match,where the language says 3. A third reproduced the wrong-answer form on master's
own emitter (
t1(5,2): Verilog 4, C 2).So this is two defects in one shape: non-termination when the loop cannot
advance, and the last-match-instead-of-first answer when it can. Shown three
times, by three people not looking for the same thing.
The population figure in the title is not confirmed
I corrected 55/24 to 75/33 and put it in the title. Three skeptics counted
independently and landed on 81–82 guarded loops across 32–33 files — but of
generated
.v, which is a different population from the.t27source Icounted, over a corpus where 69 of 650 specs never reach
.vat all. Onedeclined to count and said so. One named its own counter broken after it printed
152 sites / 40 files for stock and 99 / 38 for a tree differing in six files,
which cannot both be true.
The file count is corroborated at 32–33. The 75 is not confirmed by anybody,
including me — my third reader agreed with two others on 75/33 over
.t27source, and nothing has since checked that against the generated population.
Leaving the title as it is would be quoting an unconfirmed number, so: the
honest statement is 33 files, and a site count that has been measured two ways
over two populations and reconciled by nobody.
Refs #2988
[-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (75 sites / 33 files)[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (33 files; site count unreconciled)[/+]fix(verilog): break and continue were no-ops; lower them to guard fla…
[-]gen-verilog: an early return inside a loop does not leave the loop -- binary_search never terminates (33 files; site count unreconciled)[/-][+]gen-verilog: an early return inside a loop does not leave the loop -- 84 guard sites in 34 files, and no corpus file can demonstrate it[/+]gHashTag commentedon Sep 3, 2026
Three mutually inconsistent numbers on this issue, all reconciled by measurement. A design fan-out built three competing patches, and its judge ran a four-binary census over the carriers.
specs/onlycompiler/runtime/runtime.t27, outsidespecs/while-only countforfrom the detector reproduces 23 files / 54 sites, and that variant's top-4 is this issue's list verbatim. It dropsspecs/ar/asp_solver.t27(9 sites), the largest non-whilecarrierspecs/-scoped, and undercountsMeasured truth: 34 files, 84 guard sites — 61
whileconditions + 22forbody gates + 1 W700 innerif— plus 63 intra-iteration barriers. Say which denominator: 581 is thespecs/generation count, 643 is the whole tree of 745.t27.Two corrections to this issue's premise
1. No corpus file hangs. Measured with a hard per-file timeout over all 745 specs: zero timeouts. All 34 carriers exit in 0.02–0.07 s because
iverilogrefuses to elaborate them, andvvpnever starts — 0 of 34 elaborate under any of four binaries, 0 newly broken, 0 newly fixed.specs/isa/ternary_search.t27in particular is blocked by two unrelated defects: atrykeyword leaked into the generated Verilog, and an undeclareddata_len.The spin is real as a mechanism — three independent authors reproduced it with a hand-written testbench (
vvprc 142 / 137 / killed-at-30s unguarded, versus rc 0 returning the right answer with!__t27_retin the condition). Any commit saying "fixes thebinary_searchhang undervvp" is false as written. It fixes the mechanism, validated at the seam; the corpus has no oracle for this class today.2. The better headline needs no hang.
ternary_compareinspecs/isa/ternary_arithmetic.t27says "compare from most significant trit" and counts down. The loop runs past the returning trit, so the least significant differing trit's verdict wins: a sign inversion in a comparator, silent, terminating, no alarm.What the fan-out settled about the repair
The body position is not sufficient, and all three designs measured it independently with one-variable experiments: on an unbounded
whilea body-position guard turns a wrong answer into a non-termination, because the body is what advances the loop.And the three designs turned out not to be alternatives: the condition design is the exact disjoint union of the other two (61 + 22 + 1 = 84, union violations: none; byte-identical outputs on the overlaps). The body-only design moves the same 34 files, pays the same 72 seal rewrites, and delivers 25 of 84 guards.
One cost figure that does not exist: the gate-level price of a
forbody gate on a real carrier. 14 of 34 are yosys-readable and all 14 map to 0 cells in both versions. Every 25→51-cell number in circulation is from a hand-written toy.docs(compiler): the referee test's comment named a population that ne…
fix(verilog): a return inside a loop left the function and not the lo…
gHashTag commentedon Sep 3, 2026
The guard's price, measured: zero cells on every corpus instance
This was the open question left after #3021 landed — the dashboard stated it as
unmeasured on purpose, because every "25 → 51 cells" figure ever quoted here came
from a hand-written toy.
It is now settled, and the answer is settled by intersection, not by synthesis.
Class 1 — the
for-body gateOver the 581 generated
.v:Intersection zero. None of these functions is instantiated, so both arms
synthesize to 4 cells / 0 LUTs. The 9 files / 20 sites for
__t27_retreproduceindependently by identity; the extra 2 files are
__t27_brkgates from #2988, adifferent feature.
Class 2 — the
while-condition guardThis class was flagged as unpriced and is now priced:
Both were regenerated with the master compiler and with one built from the parent
commit.
diffis exactly one line each, the guard term only —while (!__t27_ret && !spi_done)againstwhile (!spi_done). Both fail yosyselaboration identically in both arms.
What must not be quoted
"+9 cells" and "±10 cells, inside noise" are both prices of a toy with no
corpus instance. The first is worse than imprecise: the unguarded arm of that
toy computes a different function —
iverilogreturns index 0 guarded and 26unguarded, last-match-wins, which is the bug #3021 fixes. You cannot buy that
saving.
Not measured, stated as such
loop body is a serialization question as much as an area one.
yosys statestimates undersynth_xilinx, not vendorplace-and-route. PR chore(zenodo): PASS-7 fix invalid ORCID + wrong community slug in .zenodo.json #599 showed every xc7 LUT figure here was 3× overstated
because
synth_xilinxprinted its own stats before the sampled ones; this repoships
t27c yostatfor exactly that reason. Absolute counts inherit the risk,deltas taken by one reader on both arms do not.
The reading that generalises
A construct's price is settled by intersection with what actually elaborates,
not by synthesizing an example of it. Eleven files carry the for-gate and 79
instantiate, and the two sets do not meet. That is a stronger and cheaper result
than any cell count, and it is the measurement that should have been taken first.