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 6ef371e..3989376 100644 --- a/crates/typed-wasm-verify/src/lib.rs +++ b/crates/typed-wasm-verify/src/lib.rs @@ -71,20 +71,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, @@ -97,7 +97,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 }, } @@ -105,7 +105,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, @@ -113,7 +113,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, @@ -122,18 +122,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. @@ -167,14 +184,14 @@ pub const REGION_IMPORTS_SECTION_NAME: &str = "typedwasm.region-imports"; #[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, @@ -192,24 +209,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, @@ -387,4 +404,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}"); + } }