From a359f30ad5a15caaf7ce1b571667d6f4ccb9ee2e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 3 Jun 2026 00:40:14 +0100 Subject: [PATCH] feat(verify): human-readable error messages + grouped tw-verify output (refs #126) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rewords every `#[error(...)]` template in OwnershipError / CrossError / VerifyError / CapabilitiesError / AccessSiteError for plain-language readability. All structural fields (func_idx, param_idx, count, …) are preserved — this is a Display-only change, no API breaks. Pattern: "L (): ". Examples: before: "Level 10 violation: function 0, param 0 — Linear (own) param dropped on all paths (must be consumed exactly once)" after: "L10 (linearity): function #0 parameter #0 is a Linear (own) resource but is never used; Linear resources must be consumed exactly once on every path" VerifyError's Vec-wrapper variants previously rendered as raw `{:?}` debug dumps. Now they render as "{count} L7/L10/L13 ownership violation(s) — {first}; … and N more" via a small `display_first_then_ellipsis` helper, so a single-line log is still informative. `tw-verify` binary: replace the raw `{e}`/`{:?}` print with grouped output. OwnershipError variants are sorted into per-function buckets (with a `(module-scope)` bucket for L13 ModuleNotIsolated), and CrossError variants are sorted by caller. Each location prints as a bulleted sub-list under a "in function #N:" header. Output is now scannable top-to-bottom by location rather than a flat debug blob. Source-line resolution ("at .twasm line N") is the natural next step but defers to #129 (source maps): wasm-level indices are still all the verifier has today. 3 new Display unit tests cover OwnershipError, CrossError, and the VerifyError vector-summary path. Refs #126. Source-line resolution defers to #129. Co-Authored-By: Claude Opus 4.7 (1M context) --- crates/typed-wasm-verify/src/bin/tw-verify.rs | 110 ++++++++++++++++-- crates/typed-wasm-verify/src/lib.rs | 107 ++++++++++++++--- 2 files changed, 192 insertions(+), 25 deletions(-) diff --git a/crates/typed-wasm-verify/src/bin/tw-verify.rs b/crates/typed-wasm-verify/src/bin/tw-verify.rs index a1b571e..9ee20e7 100644 --- a/crates/typed-wasm-verify/src/bin/tw-verify.rs +++ b/crates/typed-wasm-verify/src/bin/tw-verify.rs @@ -1,4 +1,5 @@ // SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell // // `tw-verify` — command-line front-end for the typed-wasm verifier. // @@ -10,16 +11,14 @@ // // Exit codes: 0 = verified, 1 = a check failed, 2 = usage / I/O error. // -// This is the executable that makes "verifiable end-to-end by -// `typed-wasm-verify`" a single command rather than a library call. -// The in-tree producer `crates/typed-wasm-codegen` (`tw build`) already -// self-verifies via `verify_from_module`; `tw-verify` is the standalone -// front-end for checking a `.wasm` from any producer (incl. external / -// third-party modules). +// Diagnostic format (#126): violations are printed as a level-prefixed +// bulleted list grouped by function-index, so a regression points at a +// named function rather than a `[…]` debug-dump. Source-line resolution +// ("at .twasm line N") defers to #129 (source maps). use std::process::ExitCode; -use typed_wasm_verify::verify_from_module; +use typed_wasm_verify::{verify_from_module, OwnershipError, VerifyError}; fn main() -> ExitCode { let args: Vec = std::env::args().collect(); @@ -54,8 +53,16 @@ fn main() -> ExitCode { // 2. L7 (aliasing) + L10 (linearity) + L13 (module isolation). match verify_from_module(&bytes) { Ok(()) => println!("ok L7/L10/L13 ownership verification"), + Err(VerifyError::Ownership(errs)) => { + print_ownership_violations(&errs); + return ExitCode::FAILURE; + } + Err(VerifyError::Cross(errs)) => { + print_cross_violations(&errs); + return ExitCode::FAILURE; + } Err(e) => { - eprintln!("tw-verify: ownership verification FAILED: {e}"); + eprintln!("tw-verify: verification error: {e}"); return ExitCode::FAILURE; } } @@ -65,7 +72,13 @@ fn main() -> ExitCode { match typed_wasm_verify::verify_access_sites_from_module(&bytes) { Ok(errs) if errs.is_empty() => println!("ok L2 access-site verification"), Ok(errs) => { - eprintln!("tw-verify: access-site violations: {errs:?}"); + eprintln!( + "FAIL L2 access-site verification ({} violation(s)):", + errs.len() + ); + for e in &errs { + eprintln!(" - {e}"); + } return ExitCode::FAILURE; } Err(e) => { @@ -79,7 +92,13 @@ fn main() -> ExitCode { match typed_wasm_verify::verify_capabilities_from_module(&bytes) { Ok(errs) if errs.is_empty() => println!("ok L15 capability verification"), Ok(errs) => { - eprintln!("tw-verify: capability violations: {errs:?}"); + eprintln!( + "FAIL L15 capability verification ({} violation(s)):", + errs.len() + ); + for e in &errs { + eprintln!(" - {e}"); + } return ExitCode::FAILURE; } Err(e) => { @@ -91,3 +110,74 @@ fn main() -> ExitCode { println!("VERIFIED {path}"); ExitCode::SUCCESS } + +/// Group OwnershipErrors by their func_idx (or by "(module-scope)" for +/// the L13 `ModuleNotIsolated` variant which has no func_idx), and print +/// a bulleted list under each header. Within a function, errors are +/// sorted by param_idx then by Display. +fn print_ownership_violations(errs: &[OwnershipError]) { + use std::collections::BTreeMap; + + let mut by_func: BTreeMap> = BTreeMap::new(); + for e in errs { + let key = match e { + OwnershipError::LinearNotUsed { func_idx, .. } + | OwnershipError::LinearDroppedOnSomePath { func_idx, .. } + | OwnershipError::LinearUsedMultiple { func_idx, .. } + | OwnershipError::ExclBorrowAliased { func_idx, .. } => format!("function #{func_idx}"), + OwnershipError::ModuleNotIsolated { .. } => "(module-scope)".to_string(), + }; + by_func.entry(key).or_default().push(e); + } + + eprintln!( + "FAIL L7/L10/L13 ownership verification ({} violation(s) in {} location(s)):", + errs.len(), + by_func.len() + ); + for (loc, group) in &by_func { + eprintln!(" in {loc}:"); + let mut sorted: Vec<&&OwnershipError> = group.iter().collect(); + sorted.sort_by_key(|e| match e { + OwnershipError::LinearNotUsed { param_idx, .. } + | OwnershipError::LinearDroppedOnSomePath { param_idx, .. } + | OwnershipError::LinearUsedMultiple { param_idx, .. } + | OwnershipError::ExclBorrowAliased { param_idx, .. } => *param_idx, + OwnershipError::ModuleNotIsolated { .. } => 0, + }); + for e in sorted { + eprintln!(" - {e}"); + } + } +} + +/// Group CrossErrors by caller_func_idx. Print bulleted list per caller. +fn print_cross_violations(errs: &[typed_wasm_verify::CrossError]) { + use std::collections::BTreeMap; + use typed_wasm_verify::CrossError; + + let mut by_caller: BTreeMap> = BTreeMap::new(); + for e in errs { + let caller = match e { + CrossError::LinearImportCalledMultiple { + caller_func_idx, .. + } + | CrossError::LinearImportDroppedOnSomePath { + caller_func_idx, .. + } => *caller_func_idx, + }; + by_caller.entry(caller).or_default().push(e); + } + + eprintln!( + "FAIL L10 cross-module boundary verification ({} violation(s) in {} caller(s)):", + errs.len(), + by_caller.len() + ); + for (caller, group) in &by_caller { + eprintln!(" in caller function #{caller}:"); + for e in group { + eprintln!(" - {e}"); + } + } +} diff --git a/crates/typed-wasm-verify/src/lib.rs b/crates/typed-wasm-verify/src/lib.rs index 123d790..67d7c86 100644 --- a/crates/typed-wasm-verify/src/lib.rs +++ b/crates/typed-wasm-verify/src/lib.rs @@ -1,4 +1,5 @@ // SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell // // typed-wasm post-codegen verifier. // @@ -64,20 +65,20 @@ impl OwnershipKind { /// Mirrors OCaml `Tw_verify.ownership_error`. #[derive(Debug, Clone, PartialEq, Eq, Error)] pub enum OwnershipError { - #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on all paths (must be consumed exactly once)")] + #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource but is never used; Linear resources must be consumed exactly once on every path")] LinearNotUsed { func_idx: u32, param_idx: u32 }, - #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on some paths (per-path min uses = 0; must be consumed on every path)")] + #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource that is consumed on some control-flow paths but dropped on others; Linear resources must be consumed exactly once on every path")] LinearDroppedOnSomePath { func_idx: u32, param_idx: u32 }, - #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param loaded {count} times on some path (exactly 1 required; possible duplication)")] + #[error("L10 (linearity): function #{func_idx} parameter #{param_idx} is a Linear (own) resource but is used {count} times on some control-flow path; Linear resources must be consumed exactly once (possible duplication)")] LinearUsedMultiple { func_idx: u32, param_idx: u32, count: u32, }, - #[error("Level 7 violation: function {func_idx}, param {param_idx} — ExclBorrow (mut) param aliased ({count} simultaneous references; at most 1 permitted)")] + #[error("L7 (aliasing): function #{func_idx} parameter #{param_idx} is an ExclBorrow (&mut) reference but {count} simultaneous borrows occur on some control-flow path; at most one is permitted")] ExclBorrowAliased { func_idx: u32, param_idx: u32, @@ -90,7 +91,7 @@ pub enum OwnershipError { /// or table — a cross-module shared-state channel outside the /// declared function-import boundary. Carrier-free (standard /// import/memory sections only; no ownership-section ABI change). - #[error("Level 13 violation: {reason}")] + #[error("L13 (module isolation): {reason}")] ModuleNotIsolated { reason: String }, } @@ -98,7 +99,7 @@ pub enum OwnershipError { /// Mirrors OCaml `Tw_interface.cross_error`. #[derive(Debug, Clone, PartialEq, Eq, Error)] pub enum CrossError { - #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' {count} time(s) on some path (Linear param; must be called at most once)")] + #[error("L10 (linearity, cross-module): caller function #{caller_func_idx} calls Linear import '{import_name}' {count} times on some control-flow path; Linear imports must be called at most once on every path")] LinearImportCalledMultiple { caller_func_idx: u32, import_func_idx: u32, @@ -106,7 +107,7 @@ pub enum CrossError { count: u32, }, - #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' on some paths but not others (Linear param dropped on zero-call path)")] + #[error("L10 (linearity, cross-module): caller function #{caller_func_idx} calls Linear import '{import_name}' on some control-flow paths but not on others; calls must be balanced across all paths")] LinearImportDroppedOnSomePath { caller_func_idx: u32, import_func_idx: u32, @@ -115,18 +116,35 @@ pub enum CrossError { } /// Top-level verification failures (parse + verify). +/// +/// The `Ownership` and `Cross` variants carry vectors of inner errors +/// whose Display impls each emit a full natural-language explanation; the +/// vector wrappers below render as "N L7/L10 violation(s): ; …" +/// so a single-line log line is still informative and the full per-error +/// detail is one `Vec::iter()` away for richer surfaces like `tw-verify`. #[derive(Debug, Error)] pub enum VerifyError { #[error("wasm parse error: {0}")] Parse(#[from] wasmparser::BinaryReaderError), - #[error("ownership violations: {0:?}")] + #[error("{} L7/L10/L13 ownership violation(s) — {}", .0.len(), display_first_then_ellipsis(.0))] Ownership(Vec), - #[error("cross-module boundary violations: {0:?}")] + #[error("{} L10 cross-module boundary violation(s) — {}", .0.len(), display_first_then_ellipsis(.0))] Cross(Vec), } +/// Helper for the vector-variant Display impls: format the first inner +/// error fully, then append "… and N more" if there are more, otherwise +/// just the first. Empty vectors render as "(empty)". +fn display_first_then_ellipsis(errs: &[E]) -> String { + match errs.split_first() { + None => "(empty)".to_string(), + Some((first, [])) => first.to_string(), + Some((first, rest)) => format!("{first}; … and {} more", rest.len()), + } +} + /// Custom-section name carrying ownership annotations. Producer-neutral as /// of the 2026-05-26 rename; both AffineScript (`Codegen.build_ownership_section`) /// and Ephapax (`ephapax-wasm`) emit and read this name. @@ -152,14 +170,14 @@ pub const ACCESS_SITES_SECTION_NAME: &str = "typedwasm.access-sites"; #[cfg(feature = "unstable-l15")] #[derive(Debug, Clone, PartialEq, Eq, Error)] pub enum CapabilitiesError { - #[error("Level 15 violation: function index {func_idx} (entry {entry_idx}) is out of bounds for wasm function section (function_count = {function_count})")] + #[error("L15 (capabilities): typedwasm.capabilities entry #{entry_idx} declares function #{func_idx} but the module only has {function_count} function(s)")] FuncIdxOutOfRange { entry_idx: u32, func_idx: u32, function_count: u32, }, - #[error("Level 15 violation: capability index {cap_idx} in function entry {entry_idx} (func_idx = {func_idx}) is out of bounds for capability table (capability_count = {capability_count})")] + #[error("L15 (capabilities): typedwasm.capabilities entry #{entry_idx} (for function #{func_idx}) requires capability #{cap_idx} but the capability table only has {capability_count} entries")] CapabilityIdxOutOfRange { entry_idx: u32, func_idx: u32, @@ -177,24 +195,24 @@ pub enum AccessSiteError { /// `typedwasm.regions` section — the access-site entries reference /// `region_id` + `field_id` keys with nothing to resolve them /// against otherwise. - #[error("Level 2 violation: typedwasm.access-sites section emitted without companion typedwasm.regions section (MissingDependentCarrier)")] + #[error("L2 (region binding): typedwasm.access-sites section is present but the companion typedwasm.regions section is missing — access-site (region, field) keys have nothing to resolve against")] MissingDependentRegions, - #[error("Level 2 violation: access-site entry {entry_idx}: func_idx {func_idx} is out of bounds for wasm function section (function_count = {function_count})")] + #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} declares function #{func_idx} but the module only has {function_count} function(s)")] FuncIdxOutOfRange { entry_idx: u32, func_idx: u32, function_count: u32, }, - #[error("Level 2 violation: access-site entry {entry_idx}: region_id {region_id} is out of bounds for typedwasm.regions table (region_count = {region_count})")] + #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} references region #{region_id} but typedwasm.regions only declares {region_count} region(s)")] RegionIdOutOfRange { entry_idx: u32, region_id: u32, region_count: u32, }, - #[error("Level 2 violation: access-site entry {entry_idx}: field_id {field_id} is out of bounds for region {region_id}'s field table (field_count = {field_count})")] + #[error("L2 (region binding): typedwasm.access-sites entry #{entry_idx} references field #{field_id} of region #{region_id}, but that region only has {field_count} field(s)")] FieldIdOutOfRange { entry_idx: u32, region_id: u32, @@ -286,4 +304,63 @@ mod tests { } assert_eq!(OwnershipKind::from_byte(99), OwnershipKind::Unrestricted); } + + #[test] + fn ownership_error_display_is_natural_language() { + let e = OwnershipError::LinearUsedMultiple { + func_idx: 3, + param_idx: 1, + count: 5, + }; + let s = e.to_string(); + assert!(s.starts_with("L10 (linearity):"), "got: {s}"); + assert!(s.contains("function #3 parameter #1"), "got: {s}"); + assert!(s.contains("used 5 times"), "got: {s}"); + assert!(s.contains("exactly once"), "got: {s}"); + } + + #[test] + fn verify_error_ownership_summary_renders_count_and_first() { + let e = VerifyError::Ownership(vec![ + OwnershipError::LinearNotUsed { + func_idx: 0, + param_idx: 0, + }, + OwnershipError::ExclBorrowAliased { + func_idx: 1, + param_idx: 0, + count: 2, + }, + OwnershipError::ModuleNotIsolated { + reason: "module owns linear memory yet imports memory 'Host.memory'".to_string(), + }, + ]); + let s = e.to_string(); + // Header: total count + level mix + assert!( + s.starts_with("3 L7/L10/L13 ownership violation(s)"), + "got: {s}" + ); + // First inner error's full Display is included + assert!( + s.contains("L10 (linearity): function #0 parameter #0"), + "got: {s}" + ); + // Tail summarises remainder + assert!(s.contains("… and 2 more"), "got: {s}"); + } + + #[test] + fn cross_error_display_includes_import_name() { + let e = CrossError::LinearImportCalledMultiple { + caller_func_idx: 7, + import_func_idx: 0, + import_name: "consume".to_string(), + count: 2, + }; + let s = e.to_string(); + assert!(s.starts_with("L10 (linearity, cross-module):"), "got: {s}"); + assert!(s.contains("caller function #7"), "got: {s}"); + assert!(s.contains("'consume'"), "got: {s}"); + } }