[fuzza] More control-flow, call_indirect, spill test cases - #1366
Draft
greenhat wants to merge 9 commits into
Draft
[fuzza] More control-flow, call_indirect, spill test cases#1366greenhat wants to merge 9 commits into
greenhat wants to merge 9 commits into
Conversation
…ore reasons Re-checking the eight ignored differential tests against the current next found three of them fixed: switch_shapes and its pinned twin pass now that the br_table selector wrap (#1235/#1243, PR #1245) is fixed, and spill_edge compiles and passes since the TransformSpills reload panic (i1289) was resolved. All three stay in the suite as regression guards, with their doc comments recording the formerly-blocking bugs. mem_overlap still fails, but as a hash-coded miden-core-lib overlap assert rather than the plainly-worded abort its ignore reason described, so the reason now records the current failure mode and the un-ignore condition. sext_shapes (i1288) and i64_srem reproduce unchanged and keep their ignores.
…ef-table facts call_indirect support (PR #1251 and the signature-tag-check follow-up) landed after the last coverage campaign, leaving the whole funcref-table surface asserted by a single differential case and the knowledge base still calling function pointers untestable. Add six cases that dispatch through the shapes safe Rust can produce: distinct-signature tables (two tags in the one shared table), a user symbol colliding with the generated table name, dyn-trait vtable dispatch, fn pointers as loop-carried values with closure coercion and pointer equality, chained dispatch where an indirect callee dispatches again, and the widest accepted signature (7 u64 parameters, 15 of the 16 operand-stack felts). All six pass differentially; no divergence or panic surfaced, so the corpus now pins this surface as correct. Rewrite the stale CallIndirect facts in KNOWLEDGE.md into a verified funcref-table section (tag interning, single-table toolchain shape, devirtualization conditions, dead-end arms) and refresh the linker closure with the function-table layout. Area coverage moved 1190 to 1198 of 2993 regions with about 125 regions warmed globally; the remaining cold rows are closed by the unreachability arguments recorded there.
…ain scheduler panic A gap-check pass over the control-flow surface (cf/scf canonicalization, cfg-to-scf) probed the remaining cold patterns and closed them with structural arguments now recorded in KNOWLEDGE.md: LLVM emits per-site returns and never result-typed frames, which shuts the br-to-return and passthrough-collapse interiors; constant selectors cannot survive to index_switch folding; the branch-interface constant arms have analysis-only callers. Two cases came out of it. spin_guard covers the one producible passthrough shape the corpus lacked - a bare guarded loop whose header holds only its own back-edge, taking the collapse-into-self-loop bail. unroll_chain is a new compiler-bug reproducer: LLVM 8x runtime-unrolls a %-bounded mul-xor accumulator loop into one block whose interleaved chain defeats every operand-scheduler tactic, and the compiler panics with NoSolution (lowering.rs:109) instead of a diagnostic on three lines of safe Rust. The mul-only and xor-only variants of the same loop compile and pass, bounding the trigger to the interleaved unrolled shape; the finding invalidates the earlier 'NoSolution unreachable' closure, which KNOWLEDGE.md now corrects. Kept #[ignore]d; the test comment carries the full finding.
…tack-motion panic The i1289 fix unblocked the spill transform's edge-split machinery, which no existing case reached: symmetric-pressure shapes spill a value in both arms and never trigger control-flow-edge reconciliation. Two mechanism discoveries make the cluster producible from plain Rust and are recorded in KNOWLEDGE.md: CSE-merged masked rotate-count bands are the only plain-Rust producer of cross-block spill-window traffic (refuting the earlier W-at-most-1-per-boundary corollary), and asymmetric arm pressure over such bands forces reload/spill splits on the diamond edges. spill_split drives split creation, materialization, and branch redirection end-to-end; spill_loop_mix puts 18 felts of shared counts at a loop header for the over-capacity arm plus preheader and backedge splits; spill_switch carries crossing freight through a dense in-loop match. unroll_u32 pins the schedulable side of the unroll-interleave boundary, while unroll_rotmix is a new compiler-bug reproducer: the 4x-unrolled mul-xor-rotate round makes the operand scheduler apply a solution out of range, panicking with 'attempt to subtract with overflow' in Stack::movdn (stack.rs:80) - same trigger family as the known NoSolution panic but a distinct failure site where a found solution is applied unchecked. All differential tests pass aside from the seven documented ignores; the remaining cold spill surface is closed by the arguments promoted to KNOWLEDGE.md.
AGENT-PROMPT.md still told agents to stay away from function pointers, which has been wrong since call_indirect support landed (PR #1251) and the corpus grew a full indirect-dispatch case family. Point at the KNOWLEDGE.md indirect-calls section instead, keeping the still-true breakers (over-limit signatures, recursion). Also apply a rustfmt re-wrap to one ignore attribute.
Root-cause triage of the campaign's two operand-scheduler panics found they are not what they seemed. The unroll-family panics (unroll_chain NoSolution, unroll_rotmix Stack::movdn overflow) share ONE defect that is not in the scheduler: TransformSpills' insert_required_phis seeds every predecessor edge of a dominance-frontier join with the spilled value itself, so a zero-trip loop's bypass edge receives a non-dominating definition; the dead phi is warned about but never removed (open TODO), no verifier checks SSA dominance, and cfg-to-scf threads the dead arguments into a sibling-region scf.yield - the scheduler is then handed an unsatisfiable problem and the crash site is selected purely by yield arity. The defect provably cannot miscompile: a live use of the poisoned arguments would have been invalid SSA before the pass, so they are always dead. Separately, the ten-count rotl trigger is a genuine in-contract solver gap, now pinned by the new rotl_window reproducer: arity-2 problems get only the TwoArgs tactic, whose fixed dup-then-movup solution is rejected by the 16-felt window check with no fallback - although LinearStackWindow's existing machinery solves the same problem in-window. Both older panic tests' doc comments now carry the corrected mechanism story, and KNOWLEDGE.md records the durable facts (arity-2 tactic list, the non-dominated-edge seeding, the cannot-miscompile argument).
… the Local2Reg gaps A gap-check over the memory read/write surface (last worked before the v0.25 rebase and VM 0.29) confirmed the code drift moved no reachability boundaries: every recorded closure held under producer-chain re-verification - the imm-store family still has only the GlobalVariable-initializer producer, the new memcopy_words fast paths are dead because wasm memory.copy stays u8-typed, and the apparent cooling of prepare_addr/enforce_alignment was a report artifact (unit-test and phantom monomorph rows in the untouched table shadowing the warm frontend instantiation - now a recorded report gotcha). The one genuinely producible gap was Local2Reg: case_local_shapes reaches the dead-store-erasure arm through an unused external-linkage parameter (every wasm parameter gets an unconditional entry store_local), the no-locals early return, and the promoted single-use pointer local of a by-value array parameter. KNOWLEDGE.md gains the refreshed memory routing facts, a Local2Reg and data-segment-layout section (including the wasm-ld-bounded segment closure and the frontend-synthesized-debug-info fact that gates the DebugDeclare cluster), and the monomorph-row gotcha.
…bal mop-up The campaign's final global sweep found one producible gap left between the worked areas: the non-strict unsigned u64 comparison arm (gte_u64) had no producer in the corpus, because branch and select position always canonicalize >=/<= into strict compares and the u128 legalization materializes only le_u pairs. case_ucmp_ge reaches i64.ge_u/le_u and i32.ge_u as materialized boolean values through noinline helpers, the same route as the signed twins, and asserts the non-strict boundary semantics differentially at both widths. The u64_ucmp doc comment now says its own comparisons are strict-canonicalized (and drops the stale claim that u64_udiv aborts - that executor gap was fixed in July). Everything else the 711-row sweep surfaced maps onto the standing closure map or new closures now recorded in KNOWLEDGE.md: import/start/dwarf module sections are toolchain-gated, Aggressive-tier region simplification is config-gated, the conversion-driver interiors are invalid-IR backstops, and one apparent cold arm (shr U64) was llvm-cov attribution noise - that verification gotcha is recorded, and the director playbook gains the matching brief-composition caveat. The remaining global cold surface is fully partitioned into out-of-scope, toolchain-unproducible, config-gated, backstop/dead-API, and known-bug-gated groups; no further plain-Rust differential area is warranted.
The workspace format task re-wraps the attribute string added by the triage commit; no content change.
Contributor
Miden examples benchmarkCandidate
SVG flamegraphs and compiled packages are attached to the workflow run. |
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.
No description provided.