Repository navigation
t27b: inline a select-shaped callee as cmp + cset/csel (Refs #12871) - #13394
Merged
Merged
Conversation
Law in inline.t27 (select_shape_ok, select_form), glue in codegen.rs, witness inline_select.t27; paid by deleting the unreferenced scripts/audit_discovery.py. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…12871) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…imm is SP (Refs #12871) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
…efs #12871) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-11-09 06:36:27 UTC
Summary
Seal Status
|
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
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.
Refs #12871
What
t27b now lowers a call to a select-shaped callee (
if (x OP y) { return a; } return b;) ascmp+cset/csel, with nobl.specs/tri/t27b/inline.t27:select_shape_ok(shape, 64-bit integer types, operand kinds) andselect_form((1,0) cset, (0,1) cset on the inverted condition, else csel of two materialized constants). 15 new tests including refusals. The existingshould_inline_callverdict is also required.cli/t27b/src/codegen.rs(try_inline, now an executor): each argument is evaluated once, in order; the compare reads those values; the result goes to the destination.specs/tri/shootout/inline_select.t27(17 tests: verdict shape, csel constants, swapped operands, param vs imm, unsigned and signed<, negative constant, expression and call arguments, refused shapes in cold and hot positions).gen/rust/tri/t27b/inline.rsand its seal are the lab gen of the extended spec (supersedes the file gen(t27b): inline.rs from the lab gen of inline.t27, glue reads hot_loop (Refs #12871) #13391 put on master; merged with master, mine wins).Soundness
Refused by the law rather than guessed: floats, i128, narrow types, operands that are not a parameter or an imm12 constant, two constants, any other body shape. A zero first operand is moved into a register first, because register 31 in
cmp_immis SP (found by the lab: 2 FAIL rows, fixed in 785f2e7). Argument single-evaluation holds by construction (oneevalper argument, then values are reused); t27 has no global or side-effecting callee to witness it in a test, so that is by construction only.Lab rows (t27os lab, sha 785f2e7, run 42571382087, seal=true)
Budget
git diff --numstat origin/master: codegen.rs +21/-7 (<= 40). Paid by deleting the unreferencedscripts/audit_discovery.py(-88). Total foreign added 21, deleted 95.Not verified
🤖 Generated with Claude Code