t27c 0.2.0: seven defects, five of them a green exit that is not a result (Refs #2161) - #2728
Merged
Conversation
…or` again (Refs #2161) `parse_for_range` parses its start bound with the full expression grammar, and that grammar carries `..` in the comparison chain (added for slices). So `for i in 0..8` came back as ONE ExprBinary, the `current.kind != DotDot` test below it never fired, and EVERY range loop was built as the collection form. Measured on master: **0** StmtForRange nodes across 746 tracked specs, against 383 StmtFor. `gen_c_for_range_stmt` and `gen_verilog_for_range_stmt` have never run on a single spec. What that cost, per backend: gen-c no loop header at all -- `/* for-each loop */` and a bare block, so the body lowers exactly once. 391 sites, 48 specs gen-verilog the whole range as the bound: `for (i = 0; i < (0 .. 8); ...)` which iverilog rejects. 32 sites, 14 specs gen-rust correct (fixed earlier today) gen (zig) correct The fix is a `no_range` depth counter beside the existing `no_struct_literal`: while a range BOUND is being parsed, `..` is not a binary operator. That makes the DotDot branch reachable, and with it the two dead lowerings. Two consequences handled in the same commit: * `a..=b` moves back here from the comparison chain, where I had put it earlier today. With `no_range` active the chain no longer eats the `..`, so the inclusive `=` arrives in `parse_for_range`. Same lowering: the exclusive range over `b + 1`. * The END bound now uses the full expression grammar too. It has to: `for i in 0..len(s)` is real, `parse_range_bound` is deliberately restricted, and the first version of this fix regressed specs/math/pellis_precision_verify.t27 for exactly that reason. VERIFIED BY RUNNING, not by reading: gen-c for (int k = 0; k < 8; k++) compiles, prints 8 gen-verilog for (k = 0; k < 8; k = k + 1) iverilog -g2005 rc=0 t27c test suite 1622 passed / 13 failed -> 1629 passed / 6 failed the 7 that turned green are exactly the for_range tests, which already encoded this lowering and were red on master specs that parse 615 -> 615, regressions 0 gen-c specs with a dropped loop header 48 -> 37 The 37 remaining are the collection form `for x in xs`, which gen-c does not lower either -- a separate defect, not this one. FROZEN_HASH resealed in the same commit (M5).
`health` -- RED on master, and the broken thing is the compiler's own
embedded self-check spec: its invariant is written
`invariant N { forall a: u32, b: u32 . ... }`, a form the parser rejects,
so `t27c health` reported FAIL at the parse stage and never reached
typecheck or any of the four backends. Rewritten to the braced-assert
form, which parses AND LOWERS -- checked: zero "NOT CHECKED" markers in
the emitted Zig, and the two assertions appear with their failure
messages. HEALTH: OK, all six stages reported.
`ci --repo-root <nonexistent>` -- walked nothing, found nothing, printed
"CI: PASSED" and exited 0. Now two separate refusals: the root holding
neither specs/ nor compiler/ is an error, and a tree that exists but
holds no .t27 is "CI: NO INPUT" with exit 2. A green verdict over an
input that was never read is the failure mode this repository names most
often, and it was in its own CI subcommand.
nonexistent tree exit 0 "CI: PASSED" -> exit 1, names the missing dirs
tree, no .t27 exit 0 "CI: PASSED" -> exit 2 "CI: NO INPUT"
real tree unchanged (exit 1, CI: FAILED)
`battery --dir <nonexistent>` -- ran 13 scripts and reported on them.
`repo_root.join(dir)` REPLACES the base when `dir` is absolute, the
directory read is an `if let Ok(..)` that swallows the failure, and the
fallback then picks up `repo_root/tools` -- so the battery audited THIS
repository while the caller had named another tree. Now it refuses a
`--dir` that is not a directory, prints the oracle and gate counts
separately, and refuses when the oracle count is zero, naming that the
gates come from tools/ and say nothing about the directory asked about.
--dir /tmp/does-not-exist 13 scripts run -> refused, names the path
--dir /etc 13 scripts run -> "0 oracle(s) under /etc,
13 gate(s) from tools/"
--dir docs/reports/upstream unchanged: 1 oracle, 14 scripts, real failures
Neither main.rs nor service.rs is under the M5 freeze; compiler.rs is
untouched by this commit.
…2161) `if (...)` and `while (...)` both accept the parenthesised form. `for` did not, and the diagnostic landed on the `(` as "Expected LBrace, got LParen" -- which reads as a missing body rather than a rejected spelling, and sends the reader to the wrong end of the statement. Checkpointed rather than looked ahead: the parser holds only `current` and `peek`, and Zig's capture form `for (xs) |x| { }` opens with the same `(`. On anything but IDENT + `in` the state is restored and that branch runs unchanged -- verified, `for (xs) |x| { }` still parses. The `paren` flag consumes the matching `)` on BOTH paths out of `parse_for_range`, the collection arm and the range arm. Measured over 746 tracked specs: specs that parse 615 -> 620 regressions 0 The five are specs/numeric/gf{8,12,20,24,32}.t27, and this cluster is unusual: its fix-yield equals its size. Five specs failed on it and all five now fully parse -- no second defect behind the first, which is not what the other clusters in this corpus look like. Lowering checked, not assumed: `for (i in 1..=8)` emits `for (int i = 1; i < (8 + 1); i++)` in C. for_range tests 9/9. FROZEN_HASH resealed in the same commit (M5).
The parenthesised range for unblocked specs/numeric/gf{8,12,20,24,32}.t27.
Each appears on both of the ratchet's lists -- out of `parse`, into
`parse-no-discard` -- because parsing them reveals that the parser
discards their top-level tokens. That is the #2474 population, not new
damage. Ledger 179 -> 179, max_entries untouched: the move is one for one.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
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.
Seven defects in
t27c, five of them a green exit that is not a result, plus the version bump and CHANGELOG for 0.2.0.The anchor:
StmtForRangewas unreachableparse_for_rangeparses its start bound with the full expression grammar, and that grammar carries..as a binary operator (added for slices). Sofor i in 0..8came back as oneExprBinary, thecurrent.kind != DotDottest below it never fired, and every range loop was built as the collection form.Measured on the previous release: 0
StmtForRangenodes across 746 tracked specs, against 383StmtFor.gen_c_for_range_stmtandgen_verilog_for_range_stmthad never run on a single spec.for i in 0..8gen-cgen-verilogfor (i = 0; i < (0 .. 8); …), which iverilog rejects. 32 sites, 14 specsgen-rustgen(Zig)Fixed with a
no_rangedepth counter beside the existingno_struct_literal: while a range bound is parsed,..is not an operator.The oracle was already in the tree, and red. Seven
for_rangeunit tests encode exactly this lowering and were failing on master. They now pass.My first version regressed one spec.
for i in 0..len(s)has a call as its end bound andparse_range_boundis deliberately restricted. The end bound now uses the full grammar under both suppressions.Three more green exits, all in t27c's own CLI
healthforallform its parser rejects, so typecheck and all four backends were never reachedNOT CHECKEDin the emitted Zig)ci --repo-root <nonexistent>CI: PASSED, exit 0CI: NO INPUTexit 2 when the tree exists but holds no.t27battery --dir <anything>batteryis the sharpest:repo_root.join(dir)replaces the base whendiris absolute, the directory read is anif let Ok(..)that swallows the failure, and the fallback then picks uprepo_root/tools. A battery pointed at another tree silently audited this one.Added
for (i in a..b)—if (…)andwhile (…)already accepted the parenthesised form. Checkpointed so Zig'sfor (xs) |x|is unaffected. The only cluster in this corpus whose fix-yield equals its size: 5 specs of 5.--version/-V— theversionsubcommand existed; the flag returned "unexpected argument".Measured, 0.1.0 → 0.2.0
parsefailuresgen-cspecs with a dropped loop headerZero parse regressions at every step, checked individually.
Two numbers got worse and both are mechanical:
parse-no-discard71 → 87 andseal-verify133 → 156. A spec that could not parse at all now parses and reveals that it discards tokens; and changing an emitter's output makes stored seals stop matching. Ledger updated one-for-one,max_entriesuntouched, RATCHET: CLEAN; width baseline 2 known, 0 new.The 37 remaining dropped loops are the collection form
for x in xs, whichgen-cdoes not lower either — a separate defect, not this one.Refs #2161