finalir: a for keeps its iterator call and loop variables - #2528
Merged
Merged
Conversation
`trFor` lowered a `for` to a bare `(loop body)`, skipping the iterator call and the loop variables. That is fine for an analysis that throws its input away and fatal for one whose output is compiled, which is where the Final IR is headed (doc/internals/contracts_elim_rtchecks.md). It now emits `(for <iterCall> <vars> (stmts ...))`, with the body lowered exactly as a `loop`'s is: ending in `(continue .)`, `break` a forward `jmp` to the trailing exit label, which stays forced because the iterator is not inlined until hexer's `elimForLoops`. The prover analyses `(for ...)` directly: `traverseLoop`'s body analysis splits out as `analyseLoopBody` and the exit-label recording as `recordLoopExitLabel`, both shared with the new `traverseFor`. Two things fall out of no longer discarding the operands — the iterator call is analysed like any other call, so a contract its arguments must satisfy is discharged at the `for`; and the loop variables are declared and marked initialized (`declareForVars`) rather than being symbols nothing had ever declared. `trLoopFromBody` loses its now-dead `forBorrow` and `forceExitLabel` parameters. Also: `loop` is documented as the infinite form it has always been emitted as. The Leng-side consumers that still parsed the old before-cond/cond/body/after slots — `genstmts.genLoop`, `llvmgenstmts.genLoopLLVM`, `induction_variables.loopBodyCursor` and `trLoopBody` in `copyprop` and `cse` — read the single body operand now. Nothing produces a Leng `loop` yet; this is about the tag having one meaning when the backend starts consuming Final IR. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…g decls `extractForBorrow`/`addForBorrowDecls` emitted a *second* declaration of each `mut`/`lent` loop binder, with a deliberately fake `(haddr firstArg)` initializer, so contract analysis would treat the binder as a borrower. That was sound only while it *replaced* the real declaration, which `trFor` threw away. Now that `trFor` keeps the loop variables, the same symbol was defined twice — harmless today, fatal once this IR reaches hexer. The fact is derived in `contracts_fir.declareForVars` instead, from the iterator call the `for` node now carries (`forIterFirstArg` resolves the call through an inline temp when xelim hoisted it). Nothing an analysis alone needs is written into an IR that is about to be compiled. Two consequences: - A `for` binder is exempted from the `let`-reassignment check. It is marked initialized at the `for` — the iterator is what initializes it — and the binding protocol (tuple unpacking, a closure iterator's resume) assigns to it, which would otherwise read as reassigning a `let`. Source-level `x = ...` on a `let` binder is already rejected by sem. - The path had no test at all: `tborrow_errors.nim` only *simulates* it with a `var` parameter. `tborrow_lifetime_errors.nim` pins it now with a real `for x in mitems(s): addItem(s, x)`. `callFirstArgs` goes with the fabricators; `callExprs` stays for `forRangeAssumes`. Also records the rest of a lossiness audit of `finalir.nim` in the design doc, and corrects two claims in it: `exprexec`/`expreval` are not Final IR consumers (the first `selfExec`s the compiler, the second has no statement dispatch), and the planned hexer-entry normalizer does not work, because `iterinliner` splices in iterator bodies loaded from other modules' published nifs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`trProcDecl` did `skip n; dest.addDotToken()` for a routine with an
`{.assembler.}` pragma, replacing hand-written machine code with a bodyless
declaration. Like `trFor` before it, that was only ever safe because this
pass's output was thrown away.
The body is passed through verbatim now — deliberately *un*-normalized, since
source order is the contract for such a body and its constructs are outside
the Final IR's vocabulary anyway (a machine flag as an `if` condition is not
an expression). `traverseProc` skips it, alongside the generic and extern
cases it already skipped: not analysed is not the same as not emitted.
Unobservable by any test until the Final IR is what hexer consumes, since the
lowering's output is still discarded. Verified by lowering a module with an
`{.assembler.}` proc through `finalir.nim`'s standalone driver and reading the
result: the body is present and unlowered, where it was a `.` before. There is
no positive test to extend — every test in `tests/nimony/assembler/` is a
negative one, because the C backend refuses such a proc by name and only the
native backend compiles it. `hastur all` (869) and `hastur native` (124) stay
green.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The `else: trExpr` fallback kept a statement's shape and lowered its children as expressions. That is right for some statements and silently wrong for any construct with a *body*, which would keep an un-lowered one — and nothing said which kinds were actually relying on it. Measured, rather than guessed. `-d:firFallbackProbe` prints one line per statement reaching the fallback (spelled like `-d:contractStats` next door); over the `tjson` dependency closure that was `jmp` (163), `lab` (122), `import` (14), `yld` (11), `destroy` (11), `comment` (8), `pragmas` (6) and `incl` (5). Every one of them was handled correctly, by accident. They get their own branches now, stating why each is right: `lab`/`jmp` arrive already lowered (xelim's flat `and`/`or` form is this pass's own vocabulary), module bookkeeping is not code, and the rest are statements whose children are plain expressions. Nothing reaches the fallback any more, so a line from the probe now means something. `corofor` is the construct the fallback would mangle, and it is not reachable here today: its only producer is hexer's `iterinliner`, which runs downstream of every caller of this pass. It becomes reachable when the lowering moves into hexer's pipeline, which is what the probe is for. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two latent traps from the lossiness audit, neither reachable today, both scheduled to become reachable. `trIf` and `genIfViaCx` handle exactly one `elif` and at most one `else`, then resync with `n = ifStart; skip n` — which consumes whatever they did not read. A third branch therefore vanished from the generated code silently, and the `assert n.substructureKind == ElseU` that stood for the invariant compiles out of a `-d:danger` build, after which a second `elif` was lowered *as* an `else` with its condition treated as a statement body. Both procs `bug` on it now, this file's existing idiom for an invariant it relies on. The whole suite passes with the invariant enforced, so `xelim` really does nest every elif chain into elif+else as the precondition claimed. `trAsgn` sent the value through `trExpr` when the destination was not a plain symbol, and `trExpr` rejects a call outright; a symbol destination went through `trBoundExpr`, which binds the call directly to its destination. `a[i] = f(x)` only survived because xelim hoists the call into a temp before this pass sees it — and `final_ir.md`'s remaining work item 2 is about changing when xelim does that. The asymmetry also cost that path its `callIsOver` mutates markers. Both paths use `trBoundExpr` now. The lowered output of 340 modules is byte-identical, so this is a simplification today rather than a fix. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`trCase` and `trTry` dropped an unexpected trailing child the same way `trIf`
did — the `n = xStart; skip n` resync swallows it — and worse, the `addParRi`
has already closed the node, so there is nowhere to put such a child even if
it were noticed. Both `bug` on it now.
Close-paren line info is kept at the six sites that close a node taken from
the input: `trLocal`, both `trAsgn` paths, `trRet`, `trRaise` and `trFor`. A
bare `dest.addParRi()` dropped it there, against the contract `takeInto`
states ("downstream sem phases read close infos"). Each site captures
`n.endInfo` where the cursor provably sits at the node's `)` — checked with
temporary assertions over 436 modules, zero failures, assertions then removed
rather than left in as a guard on an unreachable state. `trAsgn`'s path
destination needed one `skip n` to reach that position. Every remaining bare
`addParRi()` closes a node this pass *synthesizes* (`kill`, `lab`, `ite`,
`loop`, the `for` body's `stmts`), which has no input close to keep.
Two audit entries are closed as intentional rather than fixed: `(scope …)`
normalising to `(stmts …)`, and `block` losing its construct and source name.
Both are the design — scope-ness is re-expressed as the `(kill …)` set, and a
`block` is `body` plus `(lab blockExit)` by definition. Neither is textually
reconstructible, so rendering a `block` back for diagnostics is a `was`
requirement, recorded there.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The lowering emitted zero `scope` tags: `trScopedBody` and the loop and `for`
bodies all opened a scope, emitted `(stmts …)`, and expressed the scope purely
as the trailing `(kill …)` set. That was recorded as an intentional, lossless
normalisation. It is not.
Much of hexer keys off `scope`, not off `kill`. `destroyer` treats `(scope …)`
as a real destructor scope and `(stmts …)` as transparent, and its own comment
says the flat `lab`/`jmp` branch layout *depends* on it: a branch body is a
sibling in the enclosing statement list, not a child of an `(elif …)`, so
`stmts` would let a local declared in a branch live to the end of the enclosing
region. Every site that opens a scope emits one now.
`coro_transform` turns out to be a live consumer of this pass — it runs
`toFinalIr` on a coroutine wrapper and walks the result — and asserted the body
was exactly `StmtsS` in four places. Widened to `{StmtsS, ScopeS}`; all four
re-emit `n.cursorTagId`, so they were shape-agnostic apart from the assert.
The `kill`s stay for the prover, which is what reads them, and should be
dropped rather than published: hexer re-derives destruction from the scope
rules, so carrying both says the same thing twice. That is 11,986 instructions
and 2.0% of the lowered IR. `coro_transform` already drops them, so none reach
generated code today; the general strip belongs in `derefs.nim` at step 4,
when the lowered buffer is what gets published.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The temp was a `cursor`, which the duplifier cannot move out of, so the aggregate received a `=dup` and the call's own result was never destroyed: a leak for a copyable type and a spurious "'=dup' is not available" for a type whose `=dup` is `.error`. The double free the cursor was introduced to avoid does not happen with a `let`: the aggregate is the temp's last read, so the duplifier moves it and `=wasMoved` disarms the scope-end destructor. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`trStmt` lowered every nested `stmts` as a scope, but in statement position
a `stmts` is transparent: `{.keepOverflowFlag.}: let x = ...` and every
declaration xelim hoists land in one and are used after it. The lowering
killed such a local before its uses. Only a branch or loop body opens a scope.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Step 3 of doc/internals/contracts_elim_rtchecks.md. With the switch on,
`toFinalIr` replaces `xelim1` and every later pass reads the Final IR;
tests/nimony is 827/827 that way, and the default build is unchanged.
`cps` already converts the Final IR back for every routine, so only the
passes in between had to learn it: controlflow, destroyer, eraiser and
duplifier. The duplifier treats an `{.inline.}` call temp as its call for
`ensureMove` and for its self-assignment check.
Fixed for the default build as well: a replicated `finally` renames the
labels it declares, and the lowering accepts a lone-statement loop body.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…R_FIR lambdalifting now reads the Final IR: labels are not captures, a closure call's callee temp and env==nil dispatch and a capturing iterator value's frame setup are hoisted in front of the statement, and the corofor trampoline is spelled loop/ite/jmp. The lowering lowers corofor bodies and, for hexer, emits no kill/unknown. Two latent bugs that the move exposed, fixed for the default build too: typenav's crossedProc missed a capture of a local declared in a nested scope, and cps's escape analysis did not pin the first argument of an .establishesBorrow call (tpassive_openarray passed only thanks to a kill). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Under NIMONY_HEXER_FIR, desugar follows the hoisted pattern of the other passes: what an expansion needs first (set operations, runtime set constructors, string-concat chains, the arrat bound check) goes in front of the statement instead of into an (expr ...), its loops, ifs and breaks are spelled loop/ite/jmp, and an and/or whose right operand needs statements is materialized. The lowering now runs right after elimForLoops. xelim keeps a string.& chain nested in TowardsFinalIr mode so desugar can still fold it into one allocation; the concat predicate moved to programs so both passes share it, and the lowering accepts the nested call. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Under NIMONY_HEXER_FIR the module is lowered before elimForLoops. A for arrives with its body ending in (continue .) and its breaks already jumps; each yield gets a copy without the back-edge. Iterator bodies loaded from a nif are lowered on the spot, and every copy declares fresh names. xelim keeps a for's iterator call in place and registers the loop variables. The lowering now spells a source-level continue as a jmp to a label in front of the back-edge, outside a scope of the body's own: a jmp must not skip a declaration whose destructor the scope's end would run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Under NIMONY_HEXER_FIR it is the temp xelim bound it to; trExpr expects a tag. Found by the native self-host boot, which now reaches its fixpoint with the switch on. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The lowering is hexer's first step and every pass reads and writes the Final IR; NIMONY_HEXER_FIR and the Nimony-IR paths it selected against are gone: xelim1, desugar's (expr ...) expansions, lambdalifting's expression dispatch, iterinliner's block/break/continue rewriting, and coro_transform's own lowering run. cps still converts to Nimony IR for lengcgen. Step 3 of doc/internals/contracts_elim_rtchecks.md. tests: 873/873, native 127/127, self-host boot stages 1 = 2 = 3. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
lengcgen spells `ite` as a Leng `if` and `loop` as `while true` (Leng's
own `ite`/`loop` are unknown to the native back end and most optimizer
passes), and its Nimony `if`/`while`/`block`/`break` handlers are gone.
cps passes the Final IR through and its trampoline is always spelled
`loop`/`ite`/`jmp`.
The remaining Nimony producers now speak the Final IR: cps's frame and
wrapper code, vtables (a nil check is `isNil or check`), xelim_final's
`and`/`or` materialization and its walk of `ite`/`loop`, and an
`{.assembler.}` body's `if`. The lifter runs in nimsem too, so it keeps
emitting Nimony IR and hexer lowers its hooks with `toFinalIr`.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
# Conflicts: # src/hexer/coro_transform.nim # src/hexer/desugar.nim # src/hexer/duplifier.nim # src/hexer/lambdalifting.nim # src/nimony/contracts_fir.nim
`lowerExprs` is only ever run for the Final IR or for `LowerCasts`, so the goal is now a required argument and the branches that only the third goal took are gone. `inliner.nim` was added as WIP in January 2025 and never called: the inlining happens on the generated Leng instead (`intramodinliner`, and `shoggoth/intermodinliner` across modules). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Re-ran `-d:firFallbackProbe` now that the lowering runs inside hexer, which is what the probe was left in for. What reaches the fallback is a `.` in statement position, 280 times over the `tjson` closure; it gets its own branch, and the probe itself no longer asserts on a token that is not a tag. `corofor` — the construct the fallback would leave un-lowered — does not reach it: `iterinliner` still runs after this pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`semcheckCore` runs the prover on the tree `derefs` made; the cycle-group path ran it on the tree before that, so the same module was analysed against a different IR depending on whether it happened to be in an import cycle. Both orders are the single-module one now. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
nimsem lowers a module once, right after `derefs`: the prover reads that
buffer and it is what gets written, so hexer no longer lowers anything
at its entry and `iterinliner` no longer lowers an iterator body it
loaded from another module. A body that is re-sem'd elsewhere — a
generic routine, a template — is published unlowered, which the lowering
already did.
The prover's own facts (`kill`, `unknown`) are stripped on the way out;
the backend re-derives destruction from the `scope` tags.
What the switch turned up:
- `discard .` was lowered to a bare `.` in the statement list. It stays
the no-op statement it is.
- The `LowerCasts` run mints its temps in hexer, on a module whose
lowering already minted temps in nimsem. They were both `\`x.N`, so
the second run gave a name away twice; each run has its own prefix.
- The prover could no longer see through an imported accessor: in the
lowered body a call sits in an `{.inline.}` temp first. `matchAccessor`
reads those temps and registers them, which is how the module's own
code was already read (`inlineVars`).
The validator gets the phase for it (`ite`'s `join` slot is Leng's, and
its else-part may be `.`). The sem validator wants branches as written,
so `--keepsemtree` writes the pre-lowering tree as `<mod>.sem.nif` for
it; the compiler never reads that file.
Measured over the `tjson` closure the published nifs grow 11.8%;
`tall` compiles in 4.3 s against 4.4 s, the lowering having run twice
before.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The pass writes its verdict into the node it judged: a proven `(arrat a i hi [lo])` loses the bounds it was stated as, leaving `(arrat a i)` — or `(arrat a i . lo)` for an array that does not start at zero, since NIFC arrays do and the subtraction is still owed. What keeps its bounds is what the backend owes a check for, so `desugar` and `lengcgen` emit one exactly there instead of at every index. The decision travels with the code rather than with whoever compiles it: a body proven here stays check-free wherever it is inlined, and a body from a laxer module keeps its checks. Over `tall` 1158 of 1279 index obligations are discharged and 121 keep a check; `-d:contractStats` now prints that split per index, next to the per-call-site contract verdicts it already printed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`tools/gen_tags` was not run after the `ite` entry changed; the doc comments in the generated enums were stale, which `tools/tester`'s gen_tags check reports. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A routine with a `.requires` is published twice: as itself, keeping the
contract `desugar` turns into the guard, and as `bodyOfRequires` of
itself, carrying it as `(assume …)`. A call the prover discharges goes
to the guard-free copy; anything else — an unproven call, a proc value,
a callback, a vtable slot — can only name the routine and so keeps the
guard. The body's name is derived by rule (`derivedName(stem, "body")`),
so a module proving a call to an imported routine names it without a
lookup; its defining module emitted it.
The guarded copy is the full routine rather than a guard plus a tail
call: forwarding every parameter in its post-`derefs` spelling is its own
source of bugs, and on the unproven path the full copy *is* the old code.
The guard-free copy renames what it declares. Not split: methods (the
call is the dispatch), routines nested in another, and routines with
`{.global.}` storage.
Over `tall` 3851 of 6260 `.requires` call sites are proven. The copies
are 2.1% of the published nifs, while the C shrinks 1.6% (an uncalled
copy is dead code, and proven sites lose their guard); `matmul` and
`nifbench` kernels run 1-6% faster; compile time is unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The routine's body now exists once, under `bodyOfRequires` of its name.
Its own symbol becomes a wrapper: the header as written — so the guard
`desugar` makes of the `.requires` stays there — and a body that
forwards every parameter:
(result :r T .) (asgn r (call f`body p1 … pn)) (ret r)
That is what sem writes for any routine whose body is one call, with a
`var`, `sink` or `openArray` parameter passed as a bare symbol and a
`var T` result as a `result` of that type, so no pass has to learn
anything. Shoggoth's `tailcalls` folds the pair into `(ret (call …))`,
which keeps that spelling confined to Shoggoth's output.
With one body, nothing inside it is renamed any more and a routine with
`{.global.}` storage can be split. Only the body's header declarations
get fresh names; the wrapper keeps the originals because its guard is
rendered into the panic message.
Against the full copy: the same timings on `matmul` and `nifbench`
(within noise), the same executables to a few bytes, and 0.4% smaller
published nifs over `tall`.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`let x = passiveCall()` and `x = passiveCall()` hand `addr x` to the callee as its result slot, and the callee writes it when it completes — after the state proc that made the call has returned. So `x` has to be a frame field whatever states it is read in. Nothing said so. It held by accident while `cps` lowered each coroutine body itself with the prover's facts on: the scope-end `(kill x)` counted as a use in a later state. The Final IR pipeline has no kills, `x` became a stack local, and the callee wrote into a dead frame — harmless on Linux, a clobbered saved register and a crash on Windows (`tests/nimony/cps/tearly_return_in_loop`). `escapingLocalsImpl` pins the destination of a passive call now, registering the locals it walks past so the call's target can be typed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A chain `a & b & c` becomes one `newStringOfCap(len(a) + len(b) + …)` and `add` calls in `derefs`, which already knows the `(haddr s)` spelling a `var string` parameter wants. The lowering then meets ordinary statements, so the three places that only carried a nested chain from `xelim` to `desugar` are gone: `finalir.trCall`'s recursion into nested calls, `xelim.trConcatChain`, and `desugar`'s fold. `needsTemp` moves to `nimony_model`, since `desugar` still uses it for set operations. Also in this commit: comments condensed across the branch's passes and `doc/internals/contracts_elim_rtchecks.md`, and simplifications in `iterinliner`, `contracts_fir`, `lambdalifting`, `controlflow`, `duplifier` and `coro_transform`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
An empty statement slot has its own branch ahead of the fallback, so the probe's non-tag case was dead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`genCallImpl` built the `env == nil` dispatch as a Nimony `(if (elif …) (else …))` — an expression where the call returned a value — inside an `(expr|stmts …)` wrapper for an expression callee's temp, and `genCall` then took that apart again: hoisting the temp, re-parsing the `if` and rebuilding it as an `ite` with a result temp (`emitNilDispatch`). Both shapes only existed to be dismantled. `genClosureValueCall` emits the finished shape: the callee temp, the `llRes` temp and the `ite` go straight into `hoisted`, and the call site gets the result temp — or, for a void call, the `ite` itself. The arguments are translated once and shared by both arms; before, the `else` arm translated them a second time, so an argument that hoists something (a nested closure call) was hoisted twice. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
An imported accessor's `{.inline.}` temps were pushed into `inlineVars`
on every lookup, guarded by `hasKey`. But `inlineVars` is per-routine
state, moved out and restored around each routine, while the accessor
cache is module-wide — so the same module-level facts were re-registered
into whichever routine asked, and the third reader, which keys the
accessor's path in terms of its own parameter with no substitution,
never saw them at all.
The temps are the accessor's own symbols, like its parameter, so they
now go where the parameter goes: into the substitution every reader
already builds to read the accessor's value (`accessorSubst`).
`accessorOf` hands back the whole `AccessorInfo`, and `inlineVars` is
the routine's alone again.
Over `tall`, on the same tree: 3855 `.requires` sites proven against
3845, 2415 unprovable against 2419, 1161 indexes discharged against
1156; no index gained a check.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Araq
added a commit
that referenced
this pull request
Sep 19, 2026
The nativenif side (nim-lang/nativenif araq-arkham-nimony) ports arkham the way #2526 ported shoggoth; `hastur tiers` now builds it too (when the sibling nativenif checkout exists, non-Windows). The pin moves to that commit. Nimony bugs the port hit, each with a test: - `defer` inside a template was lowered at the template, so it fired at the end of the expansion instead of the caller's scope (tdefertemplate). - semDefer left the statement typed `auto`; an empty `(stmts)` (a `when false` template body) was typed `auto` too (twhenvoid). - deferstmts rewrapped if/case EXPRESSION branches as statements, leaving the result temp unassigned. - An implicitly discarded discardable call whose result has a destructor left a bare temp that hexer rejected; sem now wraps it in `(discard …)` (tdiscardablestring). - Runtime set constructors for 3/5/6/7-byte sets used a nonexistent `NU40` (tsetconstr_oddsize). - std/sets: `clear` for HashSet. Also drops tiers' stale `src/hexer/inliner.nim` entry (deleted in #2528).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
trForlowered aforto a bare(loop body), skipping the iterator call and the loop variables. That is fine for an analysis that throws its input away and fatal for one whose output is compiled, which is where the Final IR is headed (doc/internals/contracts_elim_rtchecks.md).It now emits
(for <iterCall> <vars> (stmts ...)), with the body lowered exactly as aloop's is: ending in(continue .),breaka forwardjmpto the trailing exit label, which stays forced because the iterator is not inlined until hexer'selimForLoops.The prover analyses
(for ...)directly:traverseLoop's body analysis splits out asanalyseLoopBodyand the exit-label recording asrecordLoopExitLabel, both shared with the newtraverseFor. Two things fall out of no longer discarding the operands — the iterator call is analysed like any other call, so a contract its arguments must satisfy is discharged at thefor; and the loop variables are declared and marked initialized (declareForVars) rather than being symbols nothing had ever declared.trLoopFromBodyloses its now-deadforBorrowandforceExitLabelparameters.Also:
loopis documented as the infinite form it has always been emitted as. The Leng-side consumers that still parsed the old before-cond/cond/body/after slots —genstmts.genLoop,llvmgenstmts.genLoopLLVM,induction_variables.loopBodyCursorandtrLoopBodyincopypropandcse— read the single body operand now. Nothing produces a Lengloopyet; this is about the tag having one meaning when the backend starts consuming Final IR.