//! 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:?}");
    }
}