Repository navigation
t27b: a write through an array literal printed @constCast(&[_]E{ ... }) is refused by name, not encoded, from a t27 plan (Closes #7765) - #7786
Merged
Conversation
…}) is refused by name, not encoded (Closes #7765) #7694 let a write through such a slice succeed and be read back by the next evaluation of an equal literal, as zig 0.16's x86_64 Debug backend does. Writing that comptime constant is undefined behaviour in Zig: on the native aarch64 job (LLVM) four tests of static_slice_literal.t27 fail (run 37758574293, master 209ab18: REFFAIL, 4 REFDISAGREE, STALE). specs/tri/t27b/slice_lit_plan.t27 now decides a write check: the glue logs each STATIC literal whose destination is a mutable slice, and each WRITE, a store through an element of a mutable slice or its address taken (`lvalue` sets `writing`; `slice_index` reports), in code the reference analyzes. After every body, a WRITE whose element type a STATIC backs is refused as StmtAssign(write through an array literal), at the write. Reads keep their static storage. The conformance spec keeps its read-only tests (5, 22 runtime asserts, 0 vacuous under t27c test-report on the t27c lab) and drops the four that wrote; cli/t27b/tests/arraylit.rs checks the refusal through a callee, a struct element, an address and a derived slice, and that a write through another element type's slice still runs. Plan: 13/13 pass, 0 vacuous; 14 of 14 new plan mutants killed, 11 of 11 conformance assert mutants, 6 of 6 glue mutants (cargo test). gen-rust regenerated; both specs resealed (seal --save, --verify: all MATCH). cargo test --release -p t27b: all pass (t27c lab). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
) `wc -l` of cli/t27b/src/*.rs 14905 -> 14922 (+17, lower.rs) and cli/t27b/tests/*.rs 7942 -> 7964 (+22, arraylit.rs) on master 01de65c. The write check's decisions are specs/tri/t27b/slice_lit_plan.t27. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
October 8, 2026 11:44
This was referenced Oct 8, 2026
Contributor
This was referenced Oct 8, 2026
policy: owner-approved exception for the AX7203 Ethernet beacon wrapper and XDC (Closes #7792)
#7794
Merged
Merged
Contributor
PR DashboardGenerated at: 2026-10-08 13:17:44 UTC
Summary
Seal Status
|
This was referenced Oct 8, 2026
This was referenced Oct 8, 2026
Merged
Contributor
PR DashboardGenerated at: 2026-10-08 14:21:49 UTC
Summary
Seal Status
|
This was referenced Oct 8, 2026
Merged
gHashTag
pushed a commit
that referenced
this pull request
Oct 8, 2026
From master's side; the only conflict is the AGENTS.md remainder. AGENTS.md: master's remainder plus this branch's clause after #7765's, re-measured with `wc -l` over master 7f7bf2c: src/*.rs 15043 -> 15081, src/*/*.rs 1202, tests/*.rs 8027 -> 8038. The ledger merged without a conflict; its counts match its rows (pass 906, pass_vacuous 151, not_pass 39). Merged-tree checks on the t27c lab: cargo test --release -p t27b passes with 0 failed. Corpus, master 7f7bf2c's t27b against this merge's over the same tree (qemu-aarch64): gen_assertion.t27 and opaque_pointer.t27 move to pass, gen_hazard_pointers.t27 moves to ExprBinary(?T); nothing else. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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.
Closes #7765. Part of #6063 (t27b coverage). Follows #7680 / #7694.
The UB
t27c prints an array literal as
@constCast(&[_]E{ ... })in two places: a slice field of a named struct literal, and the value of a fn that returns a slice. #7694 (20d20c9) lowered such a literal of compile-time elements into one t27b global per (array type, bytes). It also let a write through the slice succeed, so that a later evaluation of an equal literal reads the write back.That is what zig 0.16's default x86_64 self-hosted Debug backend happens to do on the t27c lab. But the array is a comptime constant, and writing it through
@constCastis undefined behaviour in Zig. #7694's own notes say-fllvmfaults on the write and ReleaseSafe folds the read away.The evidence
On aarch64, Zig uses LLVM. The native arm64 job
t27b-native-ratchetruns the reference there. On master 209ab18 (run 37758574293) it reports:So the reference's verdict on such a write depends on the backend. t27b must not encode either backend's result.
The decision
t27b refuses the write by name:
StmtAssign(write through an array literal), reported at the write. Reads stay as they were.The decision is
specs/tri/t27b/slice_lit_plan.t27(logs,refuses_write,what/whyofREFUSE_WRITE), reaching cli/t27b throught27c gen-rust. It works in three steps.[]E;xs[i] = v,xs[i].f op= v,&xs[i], and the same through a slice derived from one.[]const Eor astris never written, because Zig refuses that at compile time. An EMPTY literal has no element to write.Known limit: the check goes by element type, not by where the slice points. A write through an unrelated slice of the same element type is refused too. That gives more refusals, never a missed one. t27b's types do not tell
usizefromu64, which only widens it.The glue stays thin:
lvaluesetswritingwhile it builds a place to store to or take the address of.slice_indexreports the element throughslice_write.slice_litlogs STATIC.literal_writesruns once, before the error check.The literal's storage is unchanged.
The conformance spec is now read-only.
static_slice_literal.t27drops the four tests that wrote. It keeps its read-only tests with real asserts, and adds one that reads another value, another element type and equal bytes of two types:t27c test-reporton the t27c lab (x86_64);The refusal is checked in
cli/t27b/tests/arraylit.rs(a_write_through_a_static_literal_is_refused):Files refused on purpose
No ledger spec moves. I ran branch t27b
test --blockersover every one of the 1769 tracked.t27files on the t27c lab, including the 1084 ledger paths. Ledger specs that gain the new refusal: none. graph.t27, bellman_ford.t27 and topological_sort.t27 only read their literals. bench_proxy.t27 is not in the ledger, and it stops first atExprArrayLiteral(string slice return).Three files outside the ledger (the reference does not pass them) do write through such slices. Each gains this refusal as a further blocker. Each one's first blocker and verdict are unchanged:
specs/ml/layers/batchnorm_layer.t27: 4 writes;specs/ml/recurrent/gru_cell.t27: 1 write;specs/ml/recurrent/lstm_single.t27: 2 writes.docs/reports/t27b_expectations.jsontherefore has no row that changes;static_slice_literal.t27stayspass. The STALE finding clears once the native reference passes the spec.Checks
cargo test --release -p t27bpasses (t27c lab).t27c test-report: 13/13 pass, 0 vacuous.logsandrefuses_writeinputs, the refusal's name and words, the constants);cargo test(no WRITE logged, no STATIC logged, the check never run,writingnever set, every index a write, the key ignored).seal --save, then--verify: all hashes MATCH).gen/c/policy/own_language.c:check_budgetovergit diff --numstat --no-renames origin/master...HEADexits 0, andcheck_allwithorigin/master:tools/policy/foreign-exceptions.txtexits 0.Lines by file (hand-written foreign)
cli/t27b/src/lower.rscli/t27b/src/lower/arraylit.rscli/t27b/tests/arraylit.rsThe rest is t27, generated, seals and prose:
specs/tri/t27b/slice_lit_plan.t27+81 -17,specs/tri/t27b/conformance/static_slice_literal.t27+18 -47,gen/rust/tri/t27b/slice_lit_plan.rs+22 -2, two seals, AGENTS.md.Receipt verdict
Verdict: NEUTRAL (exit 4), which may merge. No spec regressed, so there is no REGRESSED (
left-pass) file to list.The receipts are signed corpus receipts (#7686 / #7672):
/runs/579bc55aab76deabadc6f3e4a359a089f47cc6bb.receipt.json. This is the merge-base of the requested head./work/t27:What changed. Only this PR's two specs, and both still pass. The conformance spec has 8 tests down to 5; the plan has 11 up to 13. No corpus verdict moved.
The head moved after the request. Three merge commits bring master in from master's side:
lower.rs..lencalls). It conflicted in AGENTS.md..{}, frame-address stores). It conflicted in AGENTS.md;lower.rsandtests/arraylit.rsmerged cleanly.Both carry only master's changes. The lane's diff against master is the same nine files and the same lines. After each merge,
cargo test --release -p t27bpassed again on the t27c lab. After the last one, a rescan of all 1809 tracked specs found the same three ml files and no ledger spec. To keep the queued request admitted while its sha was no longer the branch head, I pinned 679dd41 under a temporary branch,fix/t27b-arraylit-ub-receipt. I deleted that branch once the receipt was published.Native aarch64
t27b-native-ratcheton this PR's head 679dd41 (run 37772376293, ubuntu-24.04-arm, reference built natively with LLVM):The results for this spec:
static_slice_literal.t27. Reference disagree is 0 over the whole corpus, against 4 on master 209ab18.passrow for the spec is backed by the native reference again.The job stays red for findings that master has too. Its run 37758574293 has the same 2 UNEXPECTED PASS (
weight_bram.t27,fuzz.t27), the same UNLISTED rows and the same MOVED rows (zig_field_syntax,sigmoid_activation,weber_tuning). None of them is in this PR.The final head ac6f434 gives the same result (run 37786018561):
UNLISTED grew because master gained specs the ledger does not name yet (#7799's lessons, among others), not because of this PR.
Generated with Claude Code