4b5f73c1dc
#452 review S1. Rule 8 checked signed add, subtract and multiply by looking for `as_type<uint>(` in the MSL and `asuint(` in the HLSL, which every `bitcast<u32>(i32)` also writes: modules with no signed arithmetic carried both, and ops32 passed for a reason the check did not test. It now requires naga's nesting, `as_type<int>(as_type<uint>(` (and its two-component form) in MSL and `asint(asuint(` in HLSL. A new test takes the wrapping out of ops32's translations, leaving its bitcasts, and shows each refused; wai-ops-gpu.yml counts 17 tests. Co-Authored-By: Claude Opus 5.5 <[email protected]>
563 lines
30 KiB
Rust
563 lines
30 KiB
Rust
//! The shipped WGSL modules held, on naga 30.0.1's IR (the translator wgpu runs them
|
||
//! through), to the rules the `decode-equivalence` tier on a GPU rests on
|
||
//! (determinism-tiers §5, *Claiming the tier on a GPU*). No adapter is needed: these run
|
||
//! on every leg.
|
||
//!
|
||
//! 1. Each module parses, and validates with every validation flag and no capability:
|
||
//! so no `f16`, no 64-bit type, no subgroup or quad operation, no extension.
|
||
//! 2. Every entry point is a compute entry point; the globals are exactly the six
|
||
//! bindings of `wgsl/common.wgsl`, and there is no workgroup or private memory.
|
||
//! 3. Every scalar, in the type arena and in the type of every expression, is `bool`,
|
||
//! `i32` or `u32`; every literal is one of those. No floating-point value exists.
|
||
//! 4. Every expression is one of a closed list: no derivative, image, ray-query,
|
||
//! subgroup or cooperative-matrix expression; every built-in function is one of the
|
||
//! integer functions the semantics suite tests; every conversion is between `bool`,
|
||
//! `i32` and `u32`.
|
||
//! 5. In the kernels (every module but `semantics`, which exists to evaluate them), every
|
||
//! shift amount is a literal in 0..=31 or masked to 0..=31 (`e & 31u`), and every
|
||
//! `clamp` has literal bounds in order: the two integer operations whose WGSL result
|
||
//! naga 30.0.1 does not produce itself in MSL, HLSL and SPIR-V
|
||
//! (`semantics::UNGUARDED`) are reached only where every backend defines them. No
|
||
//! kernel shifts a signed value left: MSL leaves a left shift of a negative or
|
||
//! overflowing signed value undefined, and naga writes the shift as it is, so a kernel
|
||
//! shifts the `u32` and bitcasts.
|
||
//! 6. The only atomic operation is `atomicOr`, its result unused, and no `atomicLoad` or
|
||
//! `atomicStore` reaches an atomic word (naga lowers both to a plain load and store
|
||
//! through a pointer to it, which this rule reads): so every atomic operation on a word
|
||
//! is of one kind, and no result depends on the order in which invocations reach it;
|
||
//! there is no barrier.
|
||
//! 7. Every integer operation the kernels use (by operator and by signedness) is one the
|
||
//! semantics suite runs on every adapter (`src/semantics.rs`).
|
||
//! 8. Each module translates to MSL 2.4, HLSL shader model 5.1 and SPIR-V; the MSL and
|
||
//! HLSL carry naga's guards for every guarded operation the module uses (signed
|
||
//! arithmetic through unsigned, found by its nesting, `as_type<int>(as_type<uint>(`
|
||
//! and `asint(asuint(`, not by a bitcast; `naga_div`, `naga_mod`, `naga_neg`,
|
||
//! `naga_abs`), and
|
||
//! the MSL guards for division vanish when `emit_int_div_checks` is turned off,
|
||
//! which is what the crate must never do.
|
||
//!
|
||
//! Then each planted violation (a floating-point value, `f16`, a subgroup operation, an
|
||
//! `atomicAdd`, an atomic's result read, an `atomicLoad`, an `atomicStore`, `atomicOr`
|
||
//! and `atomicStore` on one word, a workgroup variable and barrier, a storage barrier
|
||
//! alone, an unmasked shift, a signed left shift, a run-time `clamp`) is shown to be refused, by the rule it
|
||
//! breaks.
|
||
|
||
use std::collections::BTreeSet;
|
||
|
||
use naga::back::{hlsl, msl, spv};
|
||
use naga::valid::{Capabilities, ModuleInfo, ValidationFlags, Validator};
|
||
use naga::{AddressSpace, AtomicFunction, BinaryOperator, Block, Expression, Literal, MathFunction, Module, Scalar, ScalarKind, ShaderStage, Statement, StorageAccess, TypeInner, UnaryOperator};
|
||
use wai_ops_gpu::kernels::Sources;
|
||
use wai_ops_gpu::semantics::Op;
|
||
|
||
type Check<T = ()> = Result<T, String>;
|
||
|
||
/// Step 1.
|
||
fn compile(text: &str) -> Check<(Module, ModuleInfo)> {
|
||
let module = naga::front::wgsl::parse_str(text).map_err(|e| format!("rule 1: parse: {}", e.emit_to_string(text)))?;
|
||
let info = Validator::new(ValidationFlags::all(), Capabilities::empty()).validate(&module).map_err(|e| format!("rule 1: validation: {}", e.emit_to_string(text)))?;
|
||
Ok((module, info))
|
||
}
|
||
|
||
/// The functions and entry points, with their expression-info tables.
|
||
fn functions<'a>(m: &'a Module, info: &'a ModuleInfo) -> Vec<(String, &'a naga::Function, &'a naga::valid::FunctionInfo)> {
|
||
let mut v: Vec<(String, &naga::Function, &naga::valid::FunctionInfo)> = m.functions.iter().map(|(h, f)| (f.name.clone().unwrap_or_default(), f, &info[h])).collect();
|
||
for (i, e) in m.entry_points.iter().enumerate() {
|
||
v.push((e.name.clone(), &e.function, info.get_entry_point(i)));
|
||
}
|
||
v
|
||
}
|
||
|
||
/// Step 2.
|
||
fn interface(m: &Module) -> Check {
|
||
for e in &m.entry_points {
|
||
if e.stage != ShaderStage::Compute {
|
||
return Err(format!("rule 2: entry point `{}` is a {:?} stage", e.name, e.stage));
|
||
}
|
||
if e.workgroup_size_overrides.is_some() || e.workgroup_size[1] != 1 || e.workgroup_size[2] != 1 {
|
||
return Err(format!("rule 2: entry point `{}` has workgroup size {:?}", e.name, e.workgroup_size));
|
||
}
|
||
}
|
||
let mut found = Vec::new();
|
||
for (_, v) in m.global_variables.iter() {
|
||
let name = v.name.clone().unwrap_or_default();
|
||
let space = match v.space {
|
||
AddressSpace::Uniform => "uniform",
|
||
AddressSpace::Storage { access } if access == StorageAccess::LOAD => "read",
|
||
AddressSpace::Storage { access } if access.contains(StorageAccess::LOAD | StorageAccess::STORE) => "read_write",
|
||
other => return Err(format!("rule 2: global `{name}` is in address space {other:?}")),
|
||
};
|
||
let b = v.binding.ok_or(format!("rule 2: global `{name}` has no binding"))?;
|
||
found.push((b.group, b.binding, space));
|
||
}
|
||
found.sort();
|
||
let want = vec![(0, 0, "uniform"), (0, 1, "read"), (0, 2, "read"), (0, 3, "read"), (0, 4, "read_write"), (0, 5, "read_write")];
|
||
if found != want {
|
||
return Err(format!("rule 2: the globals are {found:?}, not the six bindings of common.wgsl"));
|
||
}
|
||
Ok(())
|
||
}
|
||
|
||
fn scalar_ok(s: Scalar) -> bool {
|
||
s.kind == ScalarKind::Bool || (matches!(s.kind, ScalarKind::Sint | ScalarKind::Uint) && s.width == 4)
|
||
}
|
||
|
||
fn type_ok(t: &TypeInner) -> Check {
|
||
match *t {
|
||
TypeInner::Scalar(s) | TypeInner::Vector { scalar: s, .. } | TypeInner::Atomic(s) | TypeInner::ValuePointer { scalar: s, .. } => {
|
||
if scalar_ok(s) { Ok(()) } else { Err(format!("{:?} of width {}", s.kind, s.width)) }
|
||
}
|
||
TypeInner::Pointer { .. } | TypeInner::Array { .. } | TypeInner::Struct { .. } => Ok(()),
|
||
ref other => Err(format!("{other:?}")),
|
||
}
|
||
}
|
||
|
||
/// Step 3.
|
||
fn types(m: &Module, info: &ModuleInfo) -> Check {
|
||
for (_, t) in m.types.iter() {
|
||
type_ok(&t.inner).map_err(|e| format!("rule 3: the type {} is not made of bool, i32 and u32: {e}", t.name.clone().unwrap_or_default()))?;
|
||
}
|
||
for (name, f, fi) in functions(m, info) {
|
||
for (h, e) in f.expressions.iter() {
|
||
type_ok(fi[h].ty.inner_with(&m.types)).map_err(|err| format!("rule 3: in `{name}`, {e:?} has a type that is not bool, i32 or u32: {err}"))?;
|
||
if let Expression::Literal(l) = e {
|
||
literal_ok(l).map_err(|err| format!("rule 3: in `{name}`: {err}"))?;
|
||
}
|
||
}
|
||
}
|
||
for (_, e) in m.global_expressions.iter() {
|
||
if let Expression::Literal(l) = e {
|
||
literal_ok(l).map_err(|err| format!("rule 3: at module scope: {err}"))?;
|
||
}
|
||
}
|
||
Ok(())
|
||
}
|
||
|
||
fn literal_ok(l: &Literal) -> Check {
|
||
match l {
|
||
Literal::U32(_) | Literal::I32(_) | Literal::Bool(_) => Ok(()),
|
||
other => Err(format!("the literal {other:?}")),
|
||
}
|
||
}
|
||
|
||
/// The integer functions the semantics suite tests.
|
||
fn math_ok(f: MathFunction) -> bool {
|
||
use MathFunction::*;
|
||
matches!(f, Min | Max | Clamp | Abs | Sign | CountLeadingZeros | CountTrailingZeros | CountOneBits | ReverseBits | FirstLeadingBit | FirstTrailingBit | ExtractBits | InsertBits)
|
||
}
|
||
|
||
/// The integer value of a literal, or of a constant initialised with one.
|
||
fn literal_value(m: &Module, arena: &naga::Arena<Expression>, h: naga::Handle<Expression>) -> Option<i64> {
|
||
let lit = |l: &Literal| match *l {
|
||
Literal::U32(v) => Some(i64::from(v)),
|
||
Literal::I32(v) => Some(i64::from(v)),
|
||
_ => None,
|
||
};
|
||
match &arena[h] {
|
||
Expression::Literal(l) => lit(l),
|
||
Expression::Constant(c) => match &m.global_expressions[m.constants[*c].init] {
|
||
Expression::Literal(l) => lit(l),
|
||
_ => None,
|
||
},
|
||
_ => None,
|
||
}
|
||
}
|
||
|
||
/// A shift amount the kernels may use: a literal in 0..=31, or `e & k` with `k` a literal
|
||
/// in 0..=31 (either side).
|
||
fn amount_bounded(m: &Module, arena: &naga::Arena<Expression>, h: naga::Handle<Expression>) -> bool {
|
||
if let Some(v) = literal_value(m, arena, h) {
|
||
return (0..=31).contains(&v);
|
||
}
|
||
match arena[h] {
|
||
Expression::Binary { op: BinaryOperator::And, left, right } => [left, right].iter().any(|&x| literal_value(m, arena, x).is_some_and(|v| (0..=31).contains(&v))),
|
||
_ => false,
|
||
}
|
||
}
|
||
|
||
/// The scalar kind of an expression and whether it is a vector.
|
||
fn kind_of(m: &Module, fi: &naga::valid::FunctionInfo, h: naga::Handle<Expression>) -> (Option<ScalarKind>, bool) {
|
||
let t = fi[h].ty.inner_with(&m.types);
|
||
(t.scalar_kind(), matches!(t, TypeInner::Vector { .. }))
|
||
}
|
||
|
||
/// Whether a pointer expression points at an atomic: naga lowers `atomicLoad` to a plain
|
||
/// `Load` and `atomicStore` to a plain `Store` through such a pointer.
|
||
fn points_at_atomic(m: &Module, fi: &naga::valid::FunctionInfo, p: naga::Handle<Expression>) -> bool {
|
||
match *fi[p].ty.inner_with(&m.types) {
|
||
TypeInner::Pointer { base, .. } => matches!(m.types[base].inner, TypeInner::Atomic(_)),
|
||
_ => false,
|
||
}
|
||
}
|
||
|
||
/// Steps 4, 5 and 7: the closed list of expressions, the kernel rules on shifts and
|
||
/// `clamp`, and the semantics operation each integer operation is. Returns the
|
||
/// operations used.
|
||
fn expressions(m: &Module, info: &ModuleInfo, kernel: bool) -> Check<BTreeSet<Op>> {
|
||
let mut used = BTreeSet::new();
|
||
for (name, f, fi) in functions(m, info) {
|
||
let arena = &f.expressions;
|
||
for (h, e) in arena.iter() {
|
||
let at = |what: String| format!("in `{name}`, {what}");
|
||
match *e {
|
||
Expression::Literal(_) | Expression::Constant(_) | Expression::ZeroValue(_) | Expression::Compose { .. } | Expression::Access { .. } | Expression::AccessIndex { .. } | Expression::Splat { .. } | Expression::Swizzle { .. } | Expression::FunctionArgument(_) | Expression::GlobalVariable(_) | Expression::LocalVariable(_) | Expression::CallResult(_) | Expression::ArrayLength(_) => {}
|
||
// An `atomicLoad`: its value depends on which invocations reached the word first.
|
||
Expression::Load { pointer } => {
|
||
if points_at_atomic(m, fi, pointer) {
|
||
return Err(format!("rule 6: {}", at("an atomic word is loaded (atomicLoad)".into())));
|
||
}
|
||
}
|
||
Expression::Relational { fun, .. } => {
|
||
if !matches!(fun, naga::RelationalFunction::All | naga::RelationalFunction::Any) {
|
||
return Err(format!("rule 4: {}", at(format!("the relational function {fun:?}"))));
|
||
}
|
||
}
|
||
// naga gives every atomic call a result; the call statement does not count
|
||
// as a reference to it, so a count above zero is a read.
|
||
Expression::AtomicResult { .. } => {
|
||
if fi[h].ref_count > 0 {
|
||
return Err(format!("rule 6: {}", at("an atomic operation's result is read".into())));
|
||
}
|
||
}
|
||
Expression::Unary { op, expr } => {
|
||
let (k, _) = kind_of(m, fi, expr);
|
||
match (op, k) {
|
||
(UnaryOperator::Negate, Some(ScalarKind::Sint)) => {
|
||
used.insert(Op::NegI32);
|
||
}
|
||
(UnaryOperator::BitwiseNot, Some(ScalarKind::Sint | ScalarKind::Uint)) => {
|
||
used.insert(Op::Not);
|
||
}
|
||
(UnaryOperator::LogicalNot, Some(ScalarKind::Bool)) | (UnaryOperator::BitwiseNot, Some(ScalarKind::Bool)) => {}
|
||
(op, k) => return Err(format!("rule 4: {}", at(format!("the unary {op:?} on {k:?}")))),
|
||
}
|
||
}
|
||
Expression::Binary { op, left, right } => {
|
||
let (k, vector) = kind_of(m, fi, left);
|
||
use BinaryOperator as B;
|
||
let s = k == Some(ScalarKind::Sint);
|
||
let int = matches!(k, Some(ScalarKind::Sint | ScalarKind::Uint));
|
||
let v = vector;
|
||
let op_used = match op {
|
||
B::Add if int && v && !s => Some(Op::AddVec2U32),
|
||
B::Multiply if int && v => Some(if s { Op::MulVec2I32 } else { Op::MulVec2U32 }),
|
||
B::ShiftRight if v => Some(if s { Op::ShrVec2I32 } else { Op::ShrVec2U32 }),
|
||
B::Add if int && !v => Some(if s { Op::AddI32 } else { Op::AddU32 }),
|
||
B::Subtract if int && !v => Some(if s { Op::SubI32 } else { Op::SubU32 }),
|
||
B::Multiply if int && !v => Some(if s { Op::MulI32 } else { Op::MulU32 }),
|
||
B::Divide if int && !v => Some(if s { Op::DivI32 } else { Op::DivU32 }),
|
||
B::Modulo if int && !v => Some(if s { Op::RemI32 } else { Op::RemU32 }),
|
||
B::ShiftLeft if int && !v => Some(if s { Op::ShlI32 } else { Op::ShlU32 }),
|
||
B::ShiftRight if int && !v => Some(if s { Op::ShrI32 } else { Op::ShrU32 }),
|
||
B::And if int && !v => Some(Op::And),
|
||
B::InclusiveOr if int && !v => Some(Op::Or),
|
||
B::ExclusiveOr if int && !v => Some(Op::Xor),
|
||
B::Less | B::Greater if int && !v => Some(if s { Op::LtI32 } else { Op::LtU32 }),
|
||
B::LessEqual | B::GreaterEqual if int && !v => Some(if s { Op::LeI32 } else { Op::LeU32 }),
|
||
B::Equal if int && !v => Some(Op::Eq),
|
||
B::NotEqual if int && !v => Some(Op::Ne),
|
||
B::LogicalAnd | B::LogicalOr | B::And | B::InclusiveOr | B::Equal | B::NotEqual if k == Some(ScalarKind::Bool) => None,
|
||
_ => return Err(format!("rule 7: {}", at(format!("{op:?} on {k:?} (vector {vector}), which the semantics suite does not test")))),
|
||
};
|
||
// MSL leaves a left shift of a negative or overflowing signed value undefined,
|
||
// and naga passes it through: a kernel shifts a u32 and bitcasts.
|
||
if kernel && op == B::ShiftLeft && s {
|
||
return Err(format!("rule 5: {}", at("a left shift of a signed value: shift the u32 and bitcast".into())));
|
||
}
|
||
if kernel && matches!(op, B::ShiftLeft | B::ShiftRight) && !amount_bounded(m, arena, right) {
|
||
return Err(format!("rule 5: {}", at(format!("{op:?} by an amount that is neither a literal in 0..=31 nor masked to it: {:?}", arena[right]))));
|
||
}
|
||
used.extend(op_used);
|
||
}
|
||
Expression::Select { accept, .. } => {
|
||
let (k, vector) = kind_of(m, fi, accept);
|
||
used.insert(match (k, vector) {
|
||
(_, true) => Op::SelectVec2U32,
|
||
(Some(ScalarKind::Sint), false) => Op::SelectI32,
|
||
_ => Op::SelectU32,
|
||
});
|
||
}
|
||
Expression::Math { fun, arg, arg1, arg2, .. } => {
|
||
if !math_ok(fun) {
|
||
return Err(format!("rule 4: {}", at(format!("the built-in function {fun:?}, not an integer function the suite tests"))));
|
||
}
|
||
let (k, _) = kind_of(m, fi, arg);
|
||
let s = k == Some(ScalarKind::Sint);
|
||
use MathFunction as F;
|
||
if kernel && fun == F::Clamp {
|
||
let lo = arg1.and_then(|x| literal_value(m, arena, x));
|
||
let hi = arg2.and_then(|x| literal_value(m, arena, x));
|
||
match (lo, hi) {
|
||
(Some(lo), Some(hi)) if lo <= hi => {}
|
||
_ => return Err(format!("rule 5: {}", at("a clamp whose bounds are not literals in order: write min(max(e, low), high)".into()))),
|
||
}
|
||
}
|
||
used.insert(match fun {
|
||
F::Min => if s { Op::MinI32 } else { Op::MinU32 },
|
||
F::Max => if s { Op::MaxI32 } else { Op::MaxU32 },
|
||
F::Clamp => if s { Op::ClampI32 } else { Op::ClampU32 },
|
||
F::Abs => Op::AbsI32,
|
||
F::Sign => Op::SignI32,
|
||
F::CountLeadingZeros => if s { Op::CountLeadingZerosI32 } else { Op::CountLeadingZerosU32 },
|
||
F::CountTrailingZeros => Op::CountTrailingZerosU32,
|
||
F::CountOneBits => Op::CountOneBitsU32,
|
||
F::ReverseBits => Op::ReverseBitsU32,
|
||
F::FirstLeadingBit => if s { Op::FirstLeadingBitI32 } else { Op::FirstLeadingBitU32 },
|
||
F::FirstTrailingBit => Op::FirstTrailingBitU32,
|
||
F::ExtractBits => if s { Op::ExtractBitsI32 } else { Op::ExtractBitsU32 },
|
||
F::InsertBits => if s { Op::InsertBitsI32 } else { Op::InsertBitsU32 },
|
||
_ => unreachable!(),
|
||
});
|
||
}
|
||
Expression::As { expr, kind, convert } => {
|
||
let (from, _) = kind_of(m, fi, expr);
|
||
let ok = |k: Option<ScalarKind>| matches!(k, Some(ScalarKind::Sint | ScalarKind::Uint | ScalarKind::Bool));
|
||
if !ok(Some(kind)) || !ok(from) || convert.is_some_and(|w| w != 4) {
|
||
return Err(format!("rule 4: {}", at(format!("a conversion from {from:?} to {kind:?} ({convert:?})"))));
|
||
}
|
||
if convert.is_some() {
|
||
used.insert(match (from, kind) {
|
||
(Some(ScalarKind::Bool), _) => Op::U32OfBool,
|
||
(Some(ScalarKind::Sint), ScalarKind::Uint) => Op::U32OfI32,
|
||
(Some(ScalarKind::Uint), ScalarKind::Sint) => Op::I32OfU32,
|
||
_ => continue,
|
||
});
|
||
}
|
||
}
|
||
ref other => return Err(format!("rule 4: {}", at(format!("the expression {other:?}")))),
|
||
}
|
||
}
|
||
}
|
||
Ok(used)
|
||
}
|
||
|
||
/// Step 6, recursively.
|
||
fn statements(m: &Module, fi: &naga::valid::FunctionInfo, block: &Block, name: &str) -> Check {
|
||
for s in block.iter() {
|
||
match s {
|
||
// An `atomicStore`: on a word an atomic also reaches, the result is order-dependent.
|
||
Statement::Store { pointer, .. } if points_at_atomic(m, fi, *pointer) => {
|
||
return Err(format!("rule 6: in `{name}`, an atomic word is stored to (atomicStore)"));
|
||
}
|
||
// Whether its result is read is the expression rule's (rule 6 there).
|
||
Statement::Atomic { fun, .. } => {
|
||
if !matches!(fun, AtomicFunction::InclusiveOr) {
|
||
return Err(format!("rule 6: in `{name}`, the atomic operation {fun:?}"));
|
||
}
|
||
}
|
||
Statement::ControlBarrier(_) | Statement::MemoryBarrier(_) | Statement::WorkGroupUniformLoad { .. } => return Err(format!("rule 6: in `{name}`, a barrier")),
|
||
Statement::Block(b) => statements(m, fi, b, name)?,
|
||
Statement::If { accept, reject, .. } => {
|
||
statements(m, fi, accept, name)?;
|
||
statements(m, fi, reject, name)?;
|
||
}
|
||
Statement::Switch { cases, .. } => {
|
||
for c in cases {
|
||
statements(m, fi, &c.body, name)?;
|
||
}
|
||
}
|
||
Statement::Loop { body, continuing, .. } => {
|
||
statements(m, fi, body, name)?;
|
||
statements(m, fi, continuing, name)?;
|
||
}
|
||
Statement::Emit(_) | Statement::Break | Statement::Continue | Statement::Return { .. } | Statement::Store { .. } | Statement::Call { .. } => {}
|
||
other => return Err(format!("rule 4: in `{name}`, the statement {other:?}")),
|
||
}
|
||
}
|
||
Ok(())
|
||
}
|
||
|
||
/// What one module was found to use.
|
||
struct Found {
|
||
module: Module,
|
||
info: ModuleInfo,
|
||
used: BTreeSet<Op>,
|
||
}
|
||
|
||
/// Rules 1–7 on one module's text; `kernel` is false only for the semantics module.
|
||
fn check(text: &str, kernel: bool) -> Check<Found> {
|
||
let (module, info) = compile(text)?;
|
||
interface(&module)?;
|
||
types(&module, &info)?;
|
||
let used = expressions(&module, &info, kernel)?;
|
||
for (name, f, fi) in functions(&module, &info) {
|
||
statements(&module, fi, &f.body, &name)?;
|
||
}
|
||
Ok(Found { module, info, used })
|
||
}
|
||
|
||
fn msl_text(f: &Found, int_div_checks: bool) -> Check<String> {
|
||
let options = msl::Options { lang_version: (2, 4), emit_int_div_checks: int_div_checks, ..Default::default() };
|
||
msl::write_string(&f.module, &f.info, &options, &msl::PipelineOptions::default()).map(|(s, _)| s).map_err(|e| format!("rule 8: MSL: {e}"))
|
||
}
|
||
|
||
fn hlsl_text(f: &Found) -> Check<String> {
|
||
let mut s = String::new();
|
||
hlsl::Writer::new(&mut s, &hlsl::Options::default(), &hlsl::PipelineOptions::default()).write(&f.module, &f.info, None).map_err(|e| format!("rule 8: HLSL: {e}"))?;
|
||
Ok(s)
|
||
}
|
||
|
||
/// Rule 8's signed arithmetic: naga writes a signed add, subtract or multiply through
|
||
/// unsigned, `as_type<int>(as_type<uint>(a) + ...)` in MSL and `asint(asuint(a) + ...)` in
|
||
/// HLSL. The nesting is what is looked for: a bare bitcast (`bitcast<u32>(i32)`) gives the
|
||
/// inner form alone, and is no evidence of the wrapping.
|
||
fn signed_guards(name: &str, u: &BTreeSet<Op>, m: &str, h: &str) -> Check {
|
||
let scalar = [Op::AddI32, Op::SubI32, Op::MulI32].iter().any(|o| u.contains(o));
|
||
let vector = u.contains(&Op::MulVec2I32);
|
||
let fail = |lang: &str, what: &str| Err(format!("rule 8: {name}: the {lang} lacks naga's wrapping of {what} signed arithmetic through unsigned"));
|
||
if scalar && !m.contains("as_type<int>(as_type<uint>(") {
|
||
return fail("MSL", "scalar");
|
||
}
|
||
if vector && !["as_type<metal::int2>(as_type<metal::uint2>(", "as_type<int2>(as_type<uint2>("].iter().any(|p| m.contains(p)) {
|
||
return fail("MSL", "vector");
|
||
}
|
||
if (scalar || vector) && !h.contains("asint(asuint(") {
|
||
return fail("HLSL", "");
|
||
}
|
||
Ok(())
|
||
}
|
||
|
||
/// Rule 8 on one module: the translations, and the guards each must carry.
|
||
fn translations(name: &str, f: &Found) -> Check {
|
||
let m = msl_text(f, true)?;
|
||
let h = hlsl_text(f)?;
|
||
spv::write_vec(&f.module, &f.info, &spv::Options::default(), None).map_err(|e| format!("rule 8: {name}: SPIR-V: {e}"))?;
|
||
let u = &f.used;
|
||
let need = |cond: bool, text: &str, pat: &str, lang: &str| -> Check {
|
||
if cond && !text.contains(pat) {
|
||
return Err(format!("rule 8: {name}: the {lang} lacks `{pat}`, the guard for an operation the module uses"));
|
||
}
|
||
Ok(())
|
||
};
|
||
signed_guards(name, u, &m, &h)?;
|
||
let div = [Op::DivU32, Op::DivI32].iter().any(|o| u.contains(o));
|
||
let rem = [Op::RemU32, Op::RemI32].iter().any(|o| u.contains(o));
|
||
for (text, lang) in [(&m, "MSL"), (&h, "HLSL")] {
|
||
need(div, text, "naga_div(", lang)?;
|
||
need(rem, text, "naga_mod(", lang)?;
|
||
need(u.contains(&Op::NegI32), text, "naga_neg(", lang)?;
|
||
need(u.contains(&Op::AbsI32), text, "naga_abs(", lang)?;
|
||
}
|
||
if div || rem {
|
||
let raw = msl_text(f, false)?;
|
||
if raw.contains("naga_div(") || raw.contains("naga_mod(") {
|
||
return Err(format!("rule 8: {name}: the MSL keeps its division guards with emit_int_div_checks off, so this check does not see the switch"));
|
||
}
|
||
}
|
||
Ok(())
|
||
}
|
||
|
||
#[test]
|
||
fn every_shipped_module_meets_the_rules() {
|
||
let src = Sources::shipped();
|
||
let mut all = BTreeSet::new();
|
||
for (name, text) in src.named() {
|
||
let kernel = name != "semantics";
|
||
let f = check(text, kernel).unwrap_or_else(|e| panic!("{name}: {e}"));
|
||
translations(name, &f).unwrap_or_else(|e| panic!("{e}"));
|
||
let ops: Vec<&str> = f.used.iter().map(|o| o.name()).collect();
|
||
println!("ops-gpu wgsl rules: {name}: rules 1-8 hold; integer operations used: {}", ops.join(" "));
|
||
if kernel {
|
||
all.extend(f.used);
|
||
}
|
||
}
|
||
let ops: Vec<&str> = all.iter().map(|o| o.name()).collect();
|
||
println!("ops-gpu wgsl rules: the kernels use {} of the suite's operations: {}", all.len(), ops.join(" "));
|
||
}
|
||
|
||
/// Rule 7 the other way: the semantics module evaluates every operation of the suite,
|
||
/// so a kernel operation the suite names is one the device is held to.
|
||
#[test]
|
||
fn the_semantics_module_evaluates_every_operation_of_the_suite() {
|
||
let src = Sources::shipped();
|
||
let f = check(&src.semantics, false).unwrap();
|
||
for op in wai_ops_gpu::semantics::ALL {
|
||
// The conversions u32(i32) and i32(u32) are bit-preserving, as bitcast is; the
|
||
// comparisons with > and >= are those with < and <= on swapped operands.
|
||
assert!(f.used.contains(&op), "the semantics module does not evaluate {op:?}");
|
||
}
|
||
}
|
||
|
||
/// The crate creates every module through `create_shader_module`, which keeps wgpu's
|
||
/// run-time checks, the division guards among them, on; never through the unchecked
|
||
/// form or with checks of its own choosing.
|
||
#[test]
|
||
fn the_crate_never_turns_the_translators_checks_off() {
|
||
let dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("src");
|
||
let mut seen = 0;
|
||
for entry in std::fs::read_dir(&dir).unwrap() {
|
||
let p = entry.unwrap().path();
|
||
if p.extension().is_some_and(|e| e == "rs") {
|
||
let text = std::fs::read_to_string(&p).unwrap();
|
||
for (n, line) in text.lines().enumerate() {
|
||
let code = line.split("//").next().unwrap_or("");
|
||
for bad in ["create_shader_module_trusted", "ShaderRuntimeChecks", "create_shader_module_passthrough", "create_shader_module_spirv"] {
|
||
assert!(!code.contains(bad), "{}:{}: {bad}", p.display(), n + 1);
|
||
}
|
||
seen += code.matches("create_shader_module(").count();
|
||
}
|
||
}
|
||
}
|
||
assert!(seen >= 1, "no module is created through create_shader_module");
|
||
}
|
||
|
||
/// Rule 8 sees naga's wrapping of signed arithmetic, not a bitcast: a translation of
|
||
/// `ops32` (which adds signed values) with the wrapping taken out, its bitcasts left, is
|
||
/// refused, in MSL and in HLSL.
|
||
#[test]
|
||
fn rule_8_finds_the_wrapping_of_signed_arithmetic() {
|
||
let src = Sources::shipped();
|
||
let f = check(&src.ops32, true).unwrap();
|
||
assert!(f.used.contains(&Op::AddI32), "ops32 adds signed values");
|
||
let (m, h) = (msl_text(&f, true).unwrap(), hlsl_text(&f).unwrap());
|
||
signed_guards("ops32", &f.used, &m, &h).unwrap();
|
||
let unwrapped = m.replace("as_type<int>(as_type<uint>(", "as_type<int>((");
|
||
assert_ne!(unwrapped, m);
|
||
assert!(unwrapped.contains("as_type<uint>("), "the bitcasts alone remain, which the old check took for the wrapping");
|
||
assert!(signed_guards("ops32", &f.used, &unwrapped, &h).unwrap_err().starts_with("rule 8"));
|
||
let unwrapped = h.replace("asint(asuint(", "asint((");
|
||
assert_ne!(unwrapped, h);
|
||
assert!(signed_guards("ops32", &f.used, &m, &unwrapped).unwrap_err().starts_with("rule 8"));
|
||
println!("ops-gpu wgsl rules: rule 8 found the signed wrapping in ops32's MSL and HLSL, and refused each with it taken out");
|
||
}
|
||
|
||
/// Each violation, planted in a shipped module, is refused by the rule it breaks.
|
||
#[test]
|
||
fn each_planted_violation_is_refused() {
|
||
let src = Sources::shipped();
|
||
let ops32 = &src.ops32;
|
||
let anchor = " let v = A[t];\n switch P.mode {";
|
||
assert_eq!(ops32.matches(anchor).count(), 1);
|
||
let plant = |code: &str| ops32.replacen(anchor, &format!("{code}\n{anchor}"), 1);
|
||
let cases: Vec<(&str, String, &str)> = vec![
|
||
("a floating-point value", plant(" let fl = f32(P.n) * 0.5;\n O[t] = u32(fl);"), "rule 3"),
|
||
("an f16 value", format!("enable f16;\n{}", plant(" let h = f16(A[t]);\n O[t] = u32(h);")), "rule 1"),
|
||
("a subgroup reduction", format!("enable subgroups;\n{}", plant(" O[t] = subgroupAdd(A[t]);")), "rule 1"),
|
||
("an atomicAdd", plant(" atomicAdd(&F[P.flag], 1u);"), "rule 6"),
|
||
("an atomic's result read", plant(" let old = atomicOr(&F[P.flag], 1u);\n O[t] = old;"), "rule 6"),
|
||
("an atomicLoad read into the output", plant(" O[t] = atomicLoad(&F[P.flag]);"), "rule 6"),
|
||
("an atomicStore", plant(" atomicStore(&F[P.flag], 0u);"), "rule 6"),
|
||
("atomicOr and atomicStore on one word", plant(" atomicOr(&F[P.flag], 1u);\n atomicStore(&F[P.flag], 0u);"), "rule 6"),
|
||
("a storage barrier alone", plant(" storageBarrier();"), "rule 6"),
|
||
("a workgroup variable and a barrier", format!("var<workgroup> wg: array<u32, 64>;\n{}", plant(" wg[t & 63u] = A[t];\n workgroupBarrier();")), "rule 2"),
|
||
("an unmasked shift", plant(" O[t] = A[t] << P.f;"), "rule 5"),
|
||
("a left shift of a signed value", plant(" O[t] = bitcast<u32>(bitcast<i32>(A[t]) << 31u);"), "rule 5"),
|
||
("a clamp with run-time bounds", plant(" O[t] = clamp(A[t], P.lo_x, P.hi_x);"), "rule 5"),
|
||
("a floating-point built-in", plant(" O[t] = u32(sqrt(f32(A[t])));"), "rule 3"),
|
||
];
|
||
for (what, text, rule) in &cases {
|
||
assert_ne!(text, ops32, "{what}: the plant did not change the text");
|
||
match check(text, true) {
|
||
Ok(_) => panic!("{what}: the rules accepted it"),
|
||
Err(e) => {
|
||
assert!(e.starts_with(rule), "{what}: refused, but by `{e}`, not {rule}");
|
||
println!("ops-gpu wgsl rules: planted {what}: refused: {}", e.lines().next().unwrap_or(""));
|
||
}
|
||
}
|
||
}
|
||
// And the shift rule reads the masks the kernels carry: unmask one of arith.wgsl's.
|
||
let unmasked = ops32.replacen("(a.y << ((32u - s) & 31u))", "(a.y << (32u - s))", 1);
|
||
assert_ne!(&unmasked, ops32);
|
||
let e = check(&unmasked, true).err().expect("an unmasked shift in arith.wgsl was accepted");
|
||
assert!(e.starts_with("rule 5"), "{e}");
|
||
}
|