An EXEC- or VCC-skipped optional body is accepted when every merge phi's
value from the body equals the skipped value on lanes inactive in the
body. A body value that implies the skip predicate is false on every
inactive lane, so it equals the skipped value when that value is the
predicate itself. inactiveEquals now accepts that case, which covers a
lane's own bit of a ballot of the predicate merged with the predicate.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
MaskReplaySafety counted every use reaching a conditional branch condition as a quad observation, including EXEC/VCC guards that control() itself already proves replay-safe, and every Ballot regardless of how its bits are read. Nested optional regions (a merged phi re-used as the predicate of an inner execz) and ballots consumed only through the own-lane funnel (word extract, lane<32 select, lane&31 shift, &1 isolate) were refused even though neither crosses lane boundaries; the same reasoning exempts explicit-lod samples, which do not compute implicit quad derivatives.
The check now runs conditional branches through a memoized controlProven() with a visiting set, exempts those condition uses in quadObserved, walks past own-bit ballots into the isolated per-lane bools, and treats explicit-lod samples as lane-local in both quadObserved and helperObserved. optionalBody now uses a local region set so nested control proofs do not corrupt the outer walk. Anything not matching these shapes is refused as before.
Generated with [Devin](https://devin.ai)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
IrProgram does not intern values, so titles that evaluate the same
whole-quad ballot twice emit distinct WqmU64 nodes for the low and
high mask words. maskStable and helpers paired those words by object
identity and rejected the split form. Compare the two evaluations
structurally instead: same-block ballots must agree on their source
tree and must not be separated by an execution-mask change, and every
newly accepted node is recorded as restricted. Assassins Creed
Shadows (PPSA20397) hits this in shader 0x407325e400.
Generated with [Devin](https://devin.ai)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
MaskReplaySafety accepted an EXEC- or VCC-skipped body only when it was a
single block branching straight to the merge. Bodies with their own
branches (s_cbranch_execz around nested control flow) were refused.
optionalBody now takes the single-entry region of blocks reached from the
body before the merge: every block is entered only from the branch or
the region, none returns, nothing in it is exported or discarded, its
values leave only through merge phis, and every incoming value of a merge
phi equals the skipped value on inactive lanes. inactiveEquals follows
the region's own phis for that.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Since #6291 a pixel shader's EXEC copy is read as the saved word ANDed
with WQM(Ballot(true)). MaskReplaySafety only accepts a whole-quad
expansion of a ballot it can show excludes helper lanes, and a ballot
of true includes them, so a stencil-exporting shader whose own-lane
masks come from an EXEC copy was refused (own-lane mask not stable).
Every lane of a quad is active (real or helper), so a ballot of true
holds the same quad bits as the all-ones mask the proof already treats
as quad-stable; it is now classified the same way. Helper-dependent
ballots stay uncertain.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
StencilReplaySafe refused every program with usesDma, including pixel
shaders whose only BDA accesses are reads (Onimusha: Way of the Sword,
PPSA27836: one global load, then image and buffer reads). Replaying such
a shader per reference value is idempotent: its only side effect is the
first-fault record, a compare-exchange that keeps the first fault; a
fault is never retried but thrown by CheckFault, and replayed draws with
a BDA table already wait and check faults before publishing. Written-page
tracking exists only in programs with bdaWrites, which stay refused.
Compiled shaders now carry bdaWrites, and ShadersWriteMemory counts a BDA
page table as a memory write only for a program that writes through it.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Without VK_EXT_shader_stencil_export (NVIDIA), stencil reference exports
are emulated by replaying the draw once per value. An export the prover
could not bound to at most 16 values was refused. The replay shader
compares the export's low eight bits, so an unbounded export now
replays all 256 values, and proven values are reduced to their low
eight bits as the comparison sees them.
Refs #4276
Co-Authored-By: Claude Opus 5.5 <[email protected]>
With DB_SHADER_CONTROL.STENCIL_OP_VAL_EXPORT_ENABLE the pixel shader
supplies the value that REPLACE_OP and the add and subtract operations
use in place of DB_STENCILREFMASK.STENCILOPVAL. The bit was refused as a
whole, which stopped Onimusha: Way of the Sword (PPSA27836) at a
DB_SHADER_CONTROL 0x45 draw with DB_STENCIL_CONTROL 0x40040 (REPLACE_OP
on depth pass, both faces), write mask 0xff and compare ALWAYS.
The export is accepted with the 32_GR and 32_ABGR Z formats. When no
reachable operation through a non-zero write mask reads the value, it
cannot change the result and is ignored. Without a test value export, a
reachable REPLACE_OP becomes REPLACE with the exported value as
FragStencilRefEXT (or the bounded replay on devices without the
extension), provided both faces compare without the test value and use
no ONES or REPLACE_TEST; early tests throw. The add and subtract
operations, and REPLACE_OP with a test value export, still throw.
The value is read from bits 8-15 of the second MRTZ channel: the
title's pixel shader shifts it left by 8 right before exp mrtz
(v_lshlrev_b32 v0, 8, v0). That is the only evidence for the layout and
it is listed as technical debt. The pixel stage info carries the new
flag into the cache key, the draw keys and request serialization
version 31.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Preserve instance and triangle order with one dynamic-reference shader pipeline. Require bounded references, complete export coverage, replay-safe mask control and resources; refuse unsupported side effects and feedback.
Co-Authored-By: Codex <[email protected]>
