planted/build.py now writes §9.3's probe beside the checker corpus: probe.wasm, whose wai_run loads each case's operands from a data segment at run time, runs the twelve operations of the table and stores each result in order (80 bytes), in a memory of one page whose minimum is its maximum; and probe.txt, each case's operands and the result the deterministic profile prescribes, and the probe's bytes. probe-nan-branch.wasm is the probe with a branch after each operation on whether its result is a NaN, writing the canonical NaN itself. Both checkers hold both at the float level and refuse them R3 at the integer level (cases.txt; tests/module_rules.rs). What the planted copy breaks is F1, a property of the probe on engines that no checker decides; the next commit's host shows the probe holds it and the planted copy fails it. Co-Authored-By: Claude Opus 5.5 <[email protected]>
195 lines
7.4 KiB
Rust
195 lines
7.4 KiB
Rust
//! The checker held to the checker corpus of waism §9.1
|
|
//! (`planted/cases.txt`, which `planted/build.py` writes from each module's construction).
|
|
//!
|
|
//! - Every module gets the verdict stated, at every level and under every caps stated.
|
|
//! - Every planted module breaks exactly the rule its row names, at the item it names, and
|
|
//! no other: the checker's full list of findings for it is that one, but for the two rows
|
|
//! §9.1 says break a second rule, and the relaxed instruction that also takes
|
|
//! floating-point lanes at the integer level.
|
|
//! - Every rule from R1 to R12 is broken by a planted module (§11).
|
|
//! - The levels differ only in R3 (§4.3).
|
|
//! - The verdict is one line of ASCII.
|
|
|
|
use std::path::PathBuf;
|
|
|
|
use wai_module_check::{check, findings, level_of, Caps, Finding, Level, Verdict};
|
|
|
|
struct Case {
|
|
name: String,
|
|
level: Level,
|
|
caps: Caps,
|
|
caps_text: String,
|
|
verdict: String,
|
|
derived: bool,
|
|
}
|
|
|
|
fn planted() -> PathBuf {
|
|
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("planted")
|
|
}
|
|
|
|
fn cases() -> Vec<Case> {
|
|
let text = std::fs::read_to_string(planted().join("cases.txt")).expect("planted/cases.txt");
|
|
let mut out = Vec::new();
|
|
for line in text.lines() {
|
|
if line.starts_with('#') || line.trim().is_empty() {
|
|
continue;
|
|
}
|
|
let (body, comment) = match line.split_once(" #") {
|
|
Some((b, c)) => (b, c.trim()),
|
|
None => (line, ""),
|
|
};
|
|
let mut parts = body.splitn(4, ' ');
|
|
let name = parts.next().unwrap().to_string();
|
|
let level = Level::parse(parts.next().unwrap()).expect("a level");
|
|
let caps_text = parts.next().unwrap().to_string();
|
|
let caps = Caps::parse(&caps_text).expect("caps");
|
|
let verdict = parts.next().unwrap().to_string();
|
|
out.push(Case {
|
|
name,
|
|
level,
|
|
caps,
|
|
caps_text,
|
|
verdict,
|
|
derived: comment == "derived",
|
|
});
|
|
}
|
|
assert!(out.len() > 80, "cases.txt holds {} verdicts", out.len());
|
|
out
|
|
}
|
|
|
|
fn module(name: &str) -> Vec<u8> {
|
|
std::fs::read(planted().join(format!("{name}.wasm"))).unwrap_or_else(|e| panic!("{name}.wasm: {e}"))
|
|
}
|
|
|
|
#[test]
|
|
fn every_module_gets_the_verdict_stated() {
|
|
let mut wrong = Vec::new();
|
|
for c in cases() {
|
|
let got = check(&module(&c.name), c.level, &c.caps).to_string();
|
|
if got != c.verdict {
|
|
wrong.push(format!(
|
|
"{} {} {}: {got}, not {}",
|
|
c.name,
|
|
c.level.name(),
|
|
c.caps_text,
|
|
c.verdict
|
|
));
|
|
}
|
|
}
|
|
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
|
|
}
|
|
|
|
/// The rules §9.1 states a planted row breaks besides its own, at the level stated:
|
|
/// `import-memory` defines no memory (R6, at the module's length); `no-memory` lacks the
|
|
/// export `memory` (R10, there too); `f32x4.relaxed_madd` takes `f32x4` lanes (R3, at the
|
|
/// integer level, where it is the row's other rule).
|
|
fn also_broken(name: &str, level: Level) -> &'static [u8] {
|
|
match (name, level) {
|
|
("import-memory", _) => &[6],
|
|
("no-memory", _) => &[10],
|
|
("relaxed-madd", Level::Integer) => &[4],
|
|
_ => &[],
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn every_planted_module_breaks_its_rule_and_no_other() {
|
|
// A module may break its rule at more than one item (`scalar-float` holds three
|
|
// floating-point instructions); it breaks no other rule.
|
|
let mut wrong = Vec::new();
|
|
let mut seen = 0;
|
|
for c in cases() {
|
|
let bytes = module(&c.name);
|
|
let Some(rest) = c.verdict.strip_prefix("refused R") else {
|
|
// A held module breaks nothing.
|
|
assert_eq!(findings(&bytes, c.level, &c.caps), Ok(vec![]), "{}", c.name);
|
|
continue;
|
|
};
|
|
let (rule, offset) = rest.split_once(' ').unwrap();
|
|
let rule: u8 = rule.parse().unwrap();
|
|
if rule <= 2 {
|
|
// R1 and R2 stop the reading; nothing else is decided.
|
|
continue;
|
|
}
|
|
let first = Finding {
|
|
offset: offset.parse().unwrap(),
|
|
rule,
|
|
};
|
|
let got = findings(&bytes, c.level, &c.caps).expect("meets R1 and R2");
|
|
let mut rules: Vec<u8> = got.iter().map(|f| f.rule).collect();
|
|
rules.sort();
|
|
rules.dedup();
|
|
let mut want = vec![rule];
|
|
want.extend_from_slice(also_broken(&c.name, c.level));
|
|
want.sort();
|
|
seen += 1;
|
|
if got.first() != Some(&first) || rules != want {
|
|
wrong.push(format!("{} {}: {got:?}; the rules {want:?}, first {first:?}", c.name, c.level.name()));
|
|
}
|
|
}
|
|
assert!(seen > 60, "{seen} refusals checked");
|
|
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
|
|
}
|
|
|
|
#[test]
|
|
fn every_rule_has_a_planted_module() {
|
|
// §11: every rule of §4.1 that a checker decides is broken by a planted module of §9.1,
|
|
// in a verdict the text states (not one this corpus derives).
|
|
let cases = cases();
|
|
for rule in 1..=12 {
|
|
let prefix = format!("refused R{rule} ");
|
|
assert!(
|
|
cases.iter().any(|c| !c.derived && c.verdict.starts_with(&prefix)),
|
|
"no planted module of §9.1 is refused R{rule}"
|
|
);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn the_levels_differ_only_in_r3() {
|
|
// §4.3: a module refused R3 at the integer level is checked at the float level; every
|
|
// other verdict is the same at both.
|
|
for c in cases() {
|
|
let bytes = module(&c.name);
|
|
let int = check(&bytes, Level::Integer, &c.caps);
|
|
let float = check(&bytes, Level::Float, &c.caps);
|
|
if !matches!(int, Verdict::Refused { rule: 3, .. }) {
|
|
assert_eq!(int, float, "{}", c.name);
|
|
}
|
|
assert!(!matches!(float, Verdict::Refused { rule: 3, .. }), "{}", c.name);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn a_sink_holds_each_module_at_the_level_its_rows_give() {
|
|
// §6, check 9b: the integer level where it is held there, else the float level where
|
|
// the integer level refused it by R3 and the float level holds it.
|
|
let held_int = ["minimal-int", "vector-int", "bulk-and-sign", "fixed-table", "fixed-memory", "custom-section"];
|
|
for name in held_int {
|
|
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Integer), "{name}");
|
|
}
|
|
// The probe of §9.3 meets R1 to R12 at the float level, and so does the probe with a
|
|
// NaN-dependent branch planted: what it breaks is F1, which no checker decides.
|
|
for name in ["minimal-float", "scalar-float", "float-vector", "float-load", "float-unreachable", "probe", "probe-nan-branch"] {
|
|
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Float), "{name}");
|
|
}
|
|
// relaxed-madd: refused R3 at the integer level, then R4 at the float level.
|
|
let (level, verdict) = level_of(&module("relaxed-madd"), &Caps::PROFILE);
|
|
assert_eq!(level, None);
|
|
assert!(matches!(verdict, Verdict::Refused { rule: 4, .. }));
|
|
}
|
|
|
|
#[test]
|
|
fn the_verdict_is_one_line_of_ascii() {
|
|
for c in cases() {
|
|
let v = check(&module(&c.name), c.level, &c.caps).to_string();
|
|
assert!(v.is_ascii() && !v.contains('\n'), "{v:?}");
|
|
let ok = v == "held"
|
|
|| v.strip_prefix("refused R").is_some_and(|rest| {
|
|
let (n, at) = rest.split_once(' ').unwrap_or(("", ""));
|
|
n.parse::<u8>().is_ok_and(|n| (1..=12).contains(&n))
|
|
&& (at == "-" || at.bytes().all(|b| b.is_ascii_digit()))
|
|
});
|
|
assert!(ok, "{v:?}");
|
|
}
|
|
}
|