From 00b3599a9800b70c0d85bcb9ca867af99cd18e2d Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Wed, 7 Oct 2026 21:12:59 +0000 Subject: [PATCH 1/7] Allow --verify-function more than once Each pattern selects functions as before, with its own no-match and ambiguity errors; the run verifies the union. A single flag behaves as before. Co-Authored-By: Claude Opus 5.5 (1M context) --- source/rust_verify/src/config.rs | 8 +- source/rust_verify/src/driver.rs | 2 +- source/rust_verify/src/user_filter.rs | 13 +-- .../rust_verify_test/tests/verify_function.rs | 89 +++++++++++++++++++ 4 files changed, 102 insertions(+), 10 deletions(-) create mode 100644 source/rust_verify_test/tests/verify_function.rs diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 47daa3c58f..75d03c372e 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -94,7 +94,7 @@ pub struct ArgsX { pub verify_root: bool, pub verify_module: Vec, pub verify_only_module: Vec, - pub verify_function: Option, + pub verify_function: Vec, pub no_external_by_default: bool, pub no_verify: bool, pub no_lifetime: bool, @@ -573,10 +573,10 @@ pub fn parse_args_with_imports( "Verify just one submodule (excluding its descendants) within the crate (e.g. 'foo' or 'foo::bar'), can be repeated to verify only certain modules", "MODULE", ); - opts.optopt( + opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just one function within the one module specified by verify-module or verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*)", + "Verify just one function within the one module specified by verify-module or verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the functions matched by any of the arguments", "MODULE", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); @@ -842,7 +842,7 @@ pub fn parse_args_with_imports( error("Must pass at most one --verify-only-module or --verify-root when using --verify-function".to_string()) } } - matches.opt_str(OPT_VERIFY_FUNCTION) + matches.opt_strs(OPT_VERIFY_FUNCTION) }, no_external_by_default: matches.opt_present(OPT_NO_EXTERNAL_BY_DEFAULT), no_verify: matches.opt_present(OPT_NO_VERIFY), diff --git a/source/rust_verify/src/driver.rs b/source/rust_verify/src/driver.rs index 5b4d93a8b4..a63255d533 100644 --- a/source/rust_verify/src/driver.rs +++ b/source/rust_verify/src/driver.rs @@ -33,7 +33,7 @@ fn run_compiler<'a, 'b>( } pub fn is_verifying_entire_crate(verifier: &Verifier) -> bool { - verifier.args.verify_function.is_none() + verifier.args.verify_function.is_empty() && verifier.args.verify_module.is_empty() && !verifier.args.verify_root } diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index 91cdb7b30a..4a457fba5e 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -13,8 +13,8 @@ pub enum UserFilter { None, /// Verify modules Modules(Vec), - /// Verify function - Function(ModuleId, String, HashSet), + /// Verify the functions matched by any of the patterns + Function(ModuleId, Vec, HashSet), } type ModuleId = vir::ast::Idents; @@ -58,7 +58,7 @@ impl UserFilter { Ok(segments) }; - if let Some(func_name) = &args.verify_function { + if !args.verify_function.is_empty() { assert!(!(args.verify_only_module.is_empty() && !args.verify_root)); assert!(!(args.verify_module.len() + (if args.verify_root { 1 } else { 0 }) > 1)); assert!(args.verify_module.is_empty()); @@ -69,8 +69,11 @@ impl UserFilter { let s = &args.verify_only_module[0]; validate_module_name(s)? }; - let matches = Self::get_matches(&module, func_name, &local_krate.functions)?; - return Ok(UserFilter::Function(module, func_name.clone(), matches)); + let mut matches = HashSet::new(); + for func_name in &args.verify_function { + matches.extend(Self::get_matches(&module, func_name, &local_krate.functions)?); + } + return Ok(UserFilter::Function(module, args.verify_function.clone(), matches)); } if args.verify_module.is_empty() && args.verify_only_module.is_empty() && !args.verify_root diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs new file mode 100644 index 0000000000..2a5e8ecea2 --- /dev/null +++ b/source/rust_verify_test/tests/verify_function.rs @@ -0,0 +1,89 @@ +#![feature(rustc_private)] + +use std::fs; +use std::process::{Command, Output}; + +const CODE: &str = r#" +use vstd::prelude::*; +verus! { +proof fn alpha() { assert(1int + 1 == 2); } +proof fn alpha_two() { assert(2int + 2 == 4); } +proof fn beta() { assert(3int + 3 == 6); } +proof fn gamma() { assert(false); } +} +"#; + +// `gamma` fails, so a run that verifies it reports an error. +fn run(functions: &[&str]) -> (Output, String, String) { + let dir = tempfile::tempdir().unwrap(); + let input = dir.path().join("fixture.rs"); + fs::write(&input, CODE).unwrap(); + let current = std::env::current_exe().unwrap(); + let binary = current.parent().unwrap().parent().unwrap().join("rust_verify"); + let mut command = Command::new(binary); + command.args(["--mcp", "--crate-type=lib", "--verify-root", "-V", "no-solver-version-check"]); + for f in functions { + command.args(["--verify-function", f]); + } + let output = command.arg(&input).output().unwrap(); + let stdout = String::from_utf8_lossy(&output.stdout).into_owned(); + let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + (output, stdout, stderr) +} + +fn results(n: usize) -> String { + format!( + "verification results:: {n} verified, 0 errors (partial verification with `--verify-*`)\n" + ) +} + +#[test] +fn verify_function_once() { + let (output, stdout, stderr) = run(&["beta"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + assert_eq!(stderr.matches("note: verifying root module (selected functions)").count(), 1); +} + +#[test] +fn verify_function_two_exact_names() { + let (output, stdout, stderr) = run(&["alpha", "beta"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +#[test] +fn verify_function_exact_name_and_prefix() { + let (output, stdout, stderr) = run(&["beta", "alpha*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(3)); +} + +#[test] +fn verify_function_overlapping_patterns_check_each_function_once() { + let (output, stdout, stderr) = run(&["alpha*", "alpha_two", "*two"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +#[test] +fn verify_function_includes_a_failing_function() { + let (output, stdout, stderr) = run(&["beta", "gamma"]); + assert!(!output.status.success()); + assert_eq!(stderr.matches("error: assertion failed").count(), 1, "{}", stderr); + assert!( + stdout.contains("1 verified, 1 errors (partial verification with `--verify-*`)"), + "{}", + stdout + ); +} + +#[test] +fn verify_function_pattern_without_match_reports_the_same_error() { + let (single, _, single_stderr) = run(&["delta"]); + let (output, _, stderr) = run(&["alpha", "delta"]); + assert!(!single.status.success() && !output.status.success()); + let message = "could not find function delta specified by --verify-function"; + assert!(single_stderr.contains(message), "{}", single_stderr); + assert_eq!(stderr, single_stderr); +} From e5749e54b897c2781811850d840a66bfd82089ef Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Wed, 7 Oct 2026 23:47:05 +0000 Subject: [PATCH 2/7] --verify-function: report every bad pattern, allow several modules Every pattern is resolved before failing; the no-match and ambiguity messages of all bad patterns go into one error, each worded as before. --verify-function now accepts several --verify-only-module (and --verify-root alongside them). Each pattern is matched across all of them; a pattern that matches in two modules is an error unless it is qualified by its module (foo::bar::f, or crate::f for the root). Qualifiers are only recognised with more than one module, so a single module behaves exactly as before. UserFilter::Function is now (Vec, HashSet), without the unused pattern list, and each module's function names are built once. The help text names the value PATTERN and describes the union. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 10 +- source/rust_verify/src/user_filter.rs | 187 ++++++++++++------ .../rust_verify_test/tests/verify_function.rs | 111 ++++++++++- 3 files changed, 236 insertions(+), 72 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 75d03c372e..916585d617 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,8 +576,8 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just one function within the one module specified by verify-module or verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the functions matched by any of the arguments", - "MODULE", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \nwith several modules, a pattern matching in two of them must be qualified by its module (foo::bar::f, or crate::f for the root)", + "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); opts.optflag("", OPT_NO_VERIFY, "Do not run verification"); @@ -835,12 +835,6 @@ pub fn parse_args_with_imports( .to_owned(), ) } - if matches.opt_count(OPT_VERIFY_ONLY_MODULE) - + (if matches.opt_present(OPT_VERIFY_ROOT) { 1 } else { 0 }) - > 1 - { - error("Must pass at most one --verify-only-module or --verify-root when using --verify-function".to_string()) - } } matches.opt_strs(OPT_VERIFY_FUNCTION) }, diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index 4a457fba5e..d851f5a6a1 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -13,8 +13,8 @@ pub enum UserFilter { None, /// Verify modules Modules(Vec), - /// Verify the functions matched by any of the patterns - Function(ModuleId, Vec, HashSet), + /// Verify the functions matched by any of the patterns, within these modules + Function(Vec, HashSet), } type ModuleId = vir::ast::Idents; @@ -60,20 +60,48 @@ impl UserFilter { if !args.verify_function.is_empty() { assert!(!(args.verify_only_module.is_empty() && !args.verify_root)); - assert!(!(args.verify_module.len() + (if args.verify_root { 1 } else { 0 }) > 1)); assert!(args.verify_module.is_empty()); - let module = if args.verify_root { - root_module_id() - } else { - let s = &args.verify_only_module[0]; - validate_module_name(s)? - }; + let mut modules: Vec = Vec::new(); + for s in &args.verify_only_module { + let module = validate_module_name(s)?; + if !modules.contains(&module) { + modules.push(module); + } + } + if args.verify_root && !modules.contains(&root_module_id()) { + modules.push(root_module_id()); + } + + // Name each module's functions once, rather than once per pattern + let module_fun_names: Vec> = modules + .iter() + .map(|module| Self::module_fun_names(module, &local_krate.functions)) + .collect(); + let qualifiers: Vec = modules + .iter() + .map(|m| { + if m.is_empty() { + "crate".to_string() + } else { + m.iter().map(|s| s.as_str()).collect::>().join("::") + } + }) + .collect(); + + // Resolve every pattern before failing, so that one run reports all the bad ones let mut matches = HashSet::new(); + let mut errors = Vec::new(); for func_name in &args.verify_function { - matches.extend(Self::get_matches(&module, func_name, &local_krate.functions)?); + match Self::get_matches(&qualifiers, &module_fun_names, func_name) { + Ok(m) => matches.extend(m), + Err(msg) => errors.push(msg), + } + } + if !errors.is_empty() { + return Err(error(errors.join("\n\n"))); } - return Ok(UserFilter::Function(module, args.verify_function.clone(), matches)); + return Ok(UserFilter::Function(modules, matches)); } if args.verify_module.is_empty() && args.verify_only_module.is_empty() && !args.verify_root @@ -124,7 +152,7 @@ impl UserFilter { return Ok(modules.clone()); } UserFilter::Modules(m) => m.iter().collect(), - UserFilter::Function(m, _, _) => std::iter::once(m).collect(), + UserFilter::Function(m, _) => m.iter().collect(), }; let module_ids_to_verify = modules @@ -165,22 +193,9 @@ impl UserFilter { } } - /// Get the functions that match the given string. - /// - /// The first part of this process is to - /// infer whether this is an "exact match" filter. - /// (If the user doesn't supply any * in the pattern, then it is usuall - /// exact - however, if there is no exact match, but there is _exactly one_ - /// partial match, then we upgrade to a partial match, i.e., return false) - /// - /// Errors if there is no match. - fn get_matches( - module_id: &ModuleId, - function_pattern: &String, - funs: &Vec, - ) -> Result, VirErr> { - let module_fun_names: Vec<(Fun, String)> = funs - .iter() + /// The functions owned by the module, each with its name relative to the module. + fn module_fun_names(module_id: &ModuleId, funs: &Vec) -> Vec<(Fun, String)> { + funs.iter() .filter(|f| match &f.x.owning_module { None => false, Some(m) => module_id == &m.segments, @@ -192,90 +207,135 @@ impl UserFilter { ); (f.x.name.clone(), name) }) - .collect(); + .collect() + } + + /// Get the functions that match the given string. + /// + /// The first part of this process is to + /// infer whether this is an "exact match" filter. + /// (If the user doesn't supply any * in the pattern, then it is usuall + /// exact - however, if there is no exact match, but there is _exactly one_ + /// partial match, then we upgrade to a partial match, i.e., return false) + /// + /// With more than one module, the pattern is matched in all of them, + /// and must not match in two of them unless it is qualified by its module + /// (`foo::bar::f`, or `crate::f` for the root module). + /// + /// Errors (with the message) if there is no match. + fn get_matches( + qualifiers: &[String], + module_fun_names: &[Vec<(Fun, String)>], + pattern: &String, + ) -> Result, String> { + let several_modules = module_fun_names.len() > 1; + let qualified = qualifiers + .iter() + .enumerate() + .filter(|(_, q)| several_modules && pattern.starts_with(&format!("{q}::"))) + .max_by_key(|(_, q)| q.len()); + let (modules, prefix, function_pattern): (Vec, String, &str) = match qualified { + Some((i, q)) => (vec![i], format!("{q}::"), &pattern[q.len() + 2..]), + None => ((0..module_fun_names.len()).collect(), String::new(), pattern.as_str()), + }; + let funs: Vec<(usize, &(Fun, String))> = + modules.iter().flat_map(|&i| module_fun_names[i].iter().map(move |f| (i, f))).collect(); + // With several modules, show each function qualified by its module + let display = |(i, (_, name)): &(usize, &(Fun, String))| { + if several_modules { format!("{}::{name}", qualifiers[*i]) } else { name.clone() } + }; + let display_sorted = |funs: &Vec<(usize, &(Fun, String))>| { + let mut names = funs.iter().map(display).collect::>(); + names.sort(); + names + }; // First, get the matches without doing anything fancy: // If the user provides a * pattern, then we filter according to the * pattern; // if the user provides an exact match (no *), then filter as an exact match. // If we find anything this way, we're done. - let matches = Self::get_matches_strictly_by_pattern(function_pattern, &module_fun_names); + let matches = Self::get_matches_strictly_by_pattern(function_pattern, &funs); if matches.len() > 0 { - return Ok(matches.into_iter().map(|(f, _)| f.clone()).collect()); + let first_module = matches[0].0; + if matches.iter().any(|(i, _)| *i != first_module) { + let msg = vec![ + format!( + "--verify-function {pattern} matches functions in more than one module, qualify it with the module (e.g. {}::{function_pattern}),", + qualifiers[first_module] + ), + format!("matched results are:"), + ] + .into_iter() + .chain(display_sorted(&matches).iter().map(|f| format!(" - {f}"))) + .collect::>() + .join("\n"); + return Err(msg); + } + return Ok(matches.into_iter().map(|(_, f)| f.0.clone()).collect()); } // Get all substring matches, even if the user didn't use any * in their pattern. // We might use of these automatically, or if not, this list will at least help us // print an informative error message. - let substring_matches = - Self::get_all_substring_matches(function_pattern, &module_fun_names); + let substring_matches = Self::get_all_substring_matches(function_pattern, &funs); let clean = function_pattern.trim_matches('*'); if clean == function_pattern { // If there's no exact match, but there is *exactly one* substring match, // then we go ahead and use that function. if substring_matches.len() == 1 { - return Ok(substring_matches.iter().map(|f| f.0.clone()).collect()); + return Ok(substring_matches.iter().map(|f| f.1.0.clone()).collect()); } else if substring_matches.len() > 1 { - let mut filtered_functions = - substring_matches.iter().map(|f| f.1.clone()).collect::>(); - filtered_functions.sort(); let msg = vec![ format!( - "more than one match found for --verify-function {function_pattern}, consider using wildcard *{function_pattern}* to verify all matched results," + "more than one match found for --verify-function {pattern}, consider using wildcard {prefix}*{function_pattern}* to verify all matched results," ), format!( "or specify a unique substring for the desired function, matched results are:" ), ].into_iter() - .chain(filtered_functions.iter().map(|f| format!(" - {f}"))) + .chain(display_sorted(&substring_matches).iter().map(|f| format!(" - {f}"))) .collect::>() .join("\n"); - return Err(error(msg)); + return Err(msg); } } else { if substring_matches.len() >= 1 { - let mut filtered_functions = - substring_matches.iter().map(|f| f.1.clone()).collect::>(); - filtered_functions.sort(); let msg = vec![ - format!( - "could not find function {function_pattern} specified by --verify-function," - ), - format!("consider *{clean}* if you want to verify similar functions:"), + format!("could not find function {pattern} specified by --verify-function,"), + format!("consider {prefix}*{clean}* if you want to verify similar functions:"), ] .into_iter() - .chain(filtered_functions.iter().map(|f| format!(" - {f}"))) + .chain(display_sorted(&substring_matches).iter().map(|f| format!(" - {f}"))) .collect::>() .join("\n"); - return Err(error(msg)); + return Err(msg); } } // If there were absolutely no substring matches, then we fail by printing // out every possible function in the module. - let mut all_functions = module_fun_names.into_iter().map(|f| f.1).collect::>(); - all_functions.sort(); let msg = vec![ - format!("could not find function {function_pattern} specified by --verify-function"), + format!("could not find function {pattern} specified by --verify-function"), format!("available functions are:"), ] .into_iter() - .chain(all_functions.iter().map(|f| format!(" - {f}"))) + .chain(display_sorted(&funs).iter().map(|f| format!(" - {f}"))) .collect::>() .join("\n"); - return Err(error(msg)); + return Err(msg); } fn get_matches_strictly_by_pattern<'a>( - function_pattern: &String, - funs: &'a Vec<(Fun, String)>, - ) -> Vec<&'a (Fun, String)> { + function_pattern: &str, + funs: &Vec<(usize, &'a (Fun, String))>, + ) -> Vec<(usize, &'a (Fun, String))> { let clean = function_pattern.trim_matches('*'); let left_wildcard = function_pattern.starts_with('*'); let right_wildcard = function_pattern.ends_with('*'); funs.iter() - .filter(|(_, name)| { + .filter(|(_, (_, name))| { if left_wildcard && !right_wildcard { name.ends_with(clean) } else if !left_wildcard && right_wildcard { @@ -286,22 +346,23 @@ impl UserFilter { name == clean } }) + .cloned() .collect() } fn get_all_substring_matches<'a>( - function_pattern: &String, - funs: &'a Vec<(Fun, String)>, - ) -> Vec<&'a (Fun, String)> { + function_pattern: &str, + funs: &Vec<(usize, &'a (Fun, String))>, + ) -> Vec<(usize, &'a (Fun, String))> { let clean = function_pattern.trim_matches('*'); - funs.iter().filter(|(_, name)| name.contains(clean)).collect() + funs.iter().filter(|(_, (_, name))| name.contains(clean)).cloned().collect() } /// Check if the function is included in the filter. /// This assumes the function is already in the correct module /// (i.e., it only checks the function name). pub fn includes_function(&self, function_name: &Fun) -> bool { - if let UserFilter::Function(_module_id, _function, matches) = self { + if let UserFilter::Function(_modules, matches) = self { matches.contains(function_name) } else { true diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index 2a5e8ecea2..33e6ddfdab 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -11,17 +11,43 @@ proof fn alpha_two() { assert(2int + 2 == 4); } proof fn beta() { assert(3int + 3 == 6); } proof fn gamma() { assert(false); } } +mod first { + use vstd::prelude::*; + verus! { + proof fn shared() { assert(4int + 4 == 8); } + proof fn only_first() { assert(5int + 5 == 10); } + } +} +mod second { + use vstd::prelude::*; + verus! { + proof fn shared() { assert(6int + 6 == 12); } + proof fn only_second() { assert(7int + 7 == 14); } + } +} "#; // `gamma` fails, so a run that verifies it reports an error. fn run(functions: &[&str]) -> (Output, String, String) { + run_in(&["--verify-root"], functions) +} + +// `modules` holds `--verify-root` or names for `--verify-only-module`. +fn run_in(modules: &[&str], functions: &[&str]) -> (Output, String, String) { let dir = tempfile::tempdir().unwrap(); let input = dir.path().join("fixture.rs"); fs::write(&input, CODE).unwrap(); let current = std::env::current_exe().unwrap(); let binary = current.parent().unwrap().parent().unwrap().join("rust_verify"); let mut command = Command::new(binary); - command.args(["--mcp", "--crate-type=lib", "--verify-root", "-V", "no-solver-version-check"]); + command.args(["--mcp", "--crate-type=lib", "-V", "no-solver-version-check"]); + for m in modules { + if *m == "--verify-root" { + command.arg(m); + } else { + command.args(["--verify-only-module", m]); + } + } for f in functions { command.args(["--verify-function", f]); } @@ -87,3 +113,86 @@ fn verify_function_pattern_without_match_reports_the_same_error() { assert!(single_stderr.contains(message), "{}", single_stderr); assert_eq!(stderr, single_stderr); } + +#[test] +fn verify_function_bad_pattern_first_reports_the_same_error() { + let (single, _, single_stderr) = run(&["delta"]); + let (output, stdout, stderr) = run(&["delta", "alpha"]); + assert!(!single.status.success() && !output.status.success()); + assert_eq!(stderr, single_stderr); + assert!(!stdout.contains("verified"), "{}", stdout); +} + +#[test] +fn verify_function_reports_every_bad_pattern() { + let (_, _, delta_stderr) = run(&["delta"]); + let (_, _, zeta_stderr) = run(&["zeta"]); + let (output, stdout, stderr) = run(&["delta", "alpha", "zeta"]); + assert!(!output.status.success()); + assert!(!stdout.contains("verified"), "{}", stdout); + // One error, holding each pattern's message as a single flag words it + let message = |s: &str| { + let start = s.find("error: ").unwrap() + "error: ".len(); + let end = s.find("\nerror: aborting").unwrap(); + s[start..end].trim_end().to_string() + }; + assert_eq!( + message(&stderr), + format!("{}\n \n {}", message(&delta_stderr), message(&zeta_stderr)) + ); + assert!(stderr.contains("error: aborting due to 1 previous error"), "{}", stderr); +} + +#[test] +fn verify_function_ambiguous_pattern_among_good_ones() { + let (single, _, single_stderr) = run(&["alph"]); + let (output, stdout, stderr) = run(&["alpha_two", "alph", "beta"]); + assert!(!single.status.success() && !output.status.success()); + assert!(stderr.contains("more than one match found for --verify-function alph,"), "{}", stderr); + assert_eq!(stderr, single_stderr); + assert!(!stdout.contains("verified"), "{}", stdout); +} + +#[test] +fn verify_function_in_two_modules() { + let (output, stdout, stderr) = run_in(&["first", "second"], &["only_first", "only_second"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); + assert_eq!(stderr.matches("note: verifying module first (selected functions)").count(), 1); + assert_eq!(stderr.matches("note: verifying module second (selected functions)").count(), 1); +} + +#[test] +fn verify_function_in_two_modules_requires_qualifying_a_shared_name() { + let (output, stdout, stderr) = run_in(&["first", "second"], &["shared"]); + assert!(!output.status.success()); + assert!(!stdout.contains("verified"), "{}", stdout); + assert!( + stderr.contains( + "error: --verify-function shared matches functions in more than one module, qualify it with the module (e.g. first::shared),\n matched results are:\n - first::shared\n - second::shared\n" + ), + "{}", + stderr + ); +} + +#[test] +fn verify_function_in_two_modules_with_qualified_names() { + let (output, stdout, stderr) = run_in(&["first", "second"], &["first::shared"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + assert_eq!(stderr.matches("note: verifying module second").count(), 0, "{}", stderr); + + let (output, stdout, stderr) = + run_in(&["first", "second"], &["first::shared", "second::shared", "only_first"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(3)); +} + +#[test] +fn verify_function_in_root_and_a_module() { + let (output, stdout, stderr) = + run_in(&["--verify-root", "first"], &["crate::beta", "first::shared", "alpha_two"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(3)); +} From 125db9ae3760e2d1225b7590000561b13f129e39 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Thu, 8 Oct 2026 00:18:09 +0000 Subject: [PATCH 3/7] --verify-function: qualify with any number of modules, union wildcards - A pattern is first matched as written; only if that fails is a leading module name (`m::`, `crate::m::`, or `crate::` for the root) taken as a qualifier, longest first. This works with one selected module too, so a caller can always qualify. Inputs that work on main are unchanged. - An unqualified name such as `T::f` (a method of `T` in another module) is no longer read as `f` in a selected module `T`. - Wildcard matches in several modules are unioned; only an exact name that matches in two modules is an error. The "consider *pat*" hints now work. - Share module-name formatting with `verifier::module_name`. - Tests run through `run_verus_raw` (binary suffix, solver paths) and compare the joined error without depending on rustc's indentation. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 2 +- source/rust_verify/src/user_filter.rs | 91 ++++++++++---- source/rust_verify/src/verifier.rs | 6 +- .../rust_verify_test/tests/verify_function.rs | 117 +++++++++++++++--- 4 files changed, 171 insertions(+), 45 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 916585d617..09f2de6239 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,7 +576,7 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \nwith several modules, a pattern matching in two of them must be qualified by its module (foo::bar::f, or crate::f for the root)", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern can be qualified by its module (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nan exact name found in several modules must be", "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index d851f5a6a1..bf4de1d71a 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -1,7 +1,7 @@ use crate::buckets::{Bucket, BucketId}; use crate::config::Args; use crate::util::error; -use crate::verifier::module_name; +use crate::verifier::{module_name, module_name_of_segments}; use std::collections::HashSet; use std::sync::Arc; use vir::ast::{Fun, Function, Krate, VirErr}; @@ -78,15 +78,12 @@ impl UserFilter { .iter() .map(|module| Self::module_fun_names(module, &local_krate.functions)) .collect(); + // How a pattern names each module: `crate` for the root, else its path let qualifiers: Vec = modules .iter() - .map(|m| { - if m.is_empty() { - "crate".to_string() - } else { - m.iter().map(|s| s.as_str()).collect::>().join("::") - } - }) + .map( + |m| if m.is_empty() { "crate".to_string() } else { module_name_of_segments(m) }, + ) .collect(); // Resolve every pattern before failing, so that one run reports all the bad ones @@ -210,7 +207,58 @@ impl UserFilter { .collect() } - /// Get the functions that match the given string. + /// Get the functions that match the given pattern. + /// + /// The pattern is first matched as written, in all the selected modules. + /// If that fails and the pattern starts with the name of a selected module + /// (`foo::bar::f` or `crate::foo::bar::f`, or `crate::f` for the root module), + /// the rest of the pattern is matched in that module only, + /// trying the longest such module name first. + /// + /// Errors (with the message) if there is no match. + fn get_matches( + qualifiers: &[String], + module_fun_names: &[Vec<(Fun, String)>], + pattern: &String, + ) -> Result, String> { + let all_modules: Vec = (0..module_fun_names.len()).collect(); + let unqualified = + Self::get_matches_in(qualifiers, module_fun_names, &all_modules, "", pattern, pattern); + if unqualified.is_ok() { + return unqualified; + } + let mut prefixes: Vec<(usize, String)> = qualifiers + .iter() + .enumerate() + .flat_map(|(i, q)| { + let absolute = (q != "crate").then(|| format!("crate::{q}::")); + std::iter::once(format!("{q}::")).chain(absolute).map(move |p| (i, p)) + }) + .filter(|(_, p)| pattern.len() > p.len() && pattern.starts_with(p.as_str())) + .collect(); + prefixes.sort_by_key(|(_, p)| std::cmp::Reverse(p.len())); + let mut qualified_err = None; + for (i, prefix) in prefixes { + let function_pattern = &pattern[prefix.len()..]; + match Self::get_matches_in( + qualifiers, + module_fun_names, + &[i], + &prefix, + pattern, + function_pattern, + ) { + Ok(m) => return Ok(m), + Err(msg) => { + qualified_err.get_or_insert(msg); + } + } + } + Err(qualified_err.unwrap_or_else(|| unqualified.unwrap_err())) + } + + /// Get the functions in the given modules that match `function_pattern`, + /// which is `pattern` without the module qualifier `prefix`. /// /// The first part of this process is to /// infer whether this is an "exact match" filter. @@ -218,26 +266,19 @@ impl UserFilter { /// exact - however, if there is no exact match, but there is _exactly one_ /// partial match, then we upgrade to a partial match, i.e., return false) /// - /// With more than one module, the pattern is matched in all of them, - /// and must not match in two of them unless it is qualified by its module - /// (`foo::bar::f`, or `crate::f` for the root module). + /// A wildcard pattern selects its matches in every module, + /// but an exact name must not match in two modules. /// /// Errors (with the message) if there is no match. - fn get_matches( + fn get_matches_in( qualifiers: &[String], module_fun_names: &[Vec<(Fun, String)>], - pattern: &String, + modules: &[usize], + prefix: &str, + pattern: &str, + function_pattern: &str, ) -> Result, String> { let several_modules = module_fun_names.len() > 1; - let qualified = qualifiers - .iter() - .enumerate() - .filter(|(_, q)| several_modules && pattern.starts_with(&format!("{q}::"))) - .max_by_key(|(_, q)| q.len()); - let (modules, prefix, function_pattern): (Vec, String, &str) = match qualified { - Some((i, q)) => (vec![i], format!("{q}::"), &pattern[q.len() + 2..]), - None => ((0..module_fun_names.len()).collect(), String::new(), pattern.as_str()), - }; let funs: Vec<(usize, &(Fun, String))> = modules.iter().flat_map(|&i| module_fun_names[i].iter().map(move |f| (i, f))).collect(); // With several modules, show each function qualified by its module @@ -255,9 +296,10 @@ impl UserFilter { // if the user provides an exact match (no *), then filter as an exact match. // If we find anything this way, we're done. let matches = Self::get_matches_strictly_by_pattern(function_pattern, &funs); + let clean = function_pattern.trim_matches('*'); if matches.len() > 0 { let first_module = matches[0].0; - if matches.iter().any(|(i, _)| *i != first_module) { + if clean == function_pattern && matches.iter().any(|(i, _)| *i != first_module) { let msg = vec![ format!( "--verify-function {pattern} matches functions in more than one module, qualify it with the module (e.g. {}::{function_pattern}),", @@ -279,7 +321,6 @@ impl UserFilter { // print an informative error message. let substring_matches = Self::get_all_substring_matches(function_pattern, &funs); - let clean = function_pattern.trim_matches('*'); if clean == function_pattern { // If there's no exact match, but there is *exactly one* substring match, // then we go ahead and use that function. diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index 379386f278..d8d62a4c88 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -584,7 +584,11 @@ pub(crate) fn io_vir_err(msg: String, err: std::io::Error) -> VirErr { } pub fn module_name(module: &vir::ast::Path) -> String { - module.segments.iter().map(|s| s.to_string()).collect::>().join("::") + module_name_of_segments(&module.segments) +} + +pub fn module_name_of_segments(segments: &vir::ast::Idents) -> String { + segments.iter().map(|s| s.to_string()).collect::>().join("::") } mod util { diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index 33e6ddfdab..ae2823457d 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -1,7 +1,10 @@ #![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; use std::fs; -use std::process::{Command, Output}; +use std::process::Output; const CODE: &str = r#" use vstd::prelude::*; @@ -25,6 +28,20 @@ mod second { proof fn only_second() { assert(7int + 7 == 14); } } } +mod point { + use vstd::prelude::*; + verus! { + proof fn origin() { assert(0int == 0); } + } +} +mod third { + use vstd::prelude::*; + verus! { + #[allow(non_camel_case_types)] + pub struct point {} + impl point { proof fn f() { assert(8int == 8); } } + } +} "#; // `gamma` fails, so a run that verifies it reports an error. @@ -37,21 +54,18 @@ fn run_in(modules: &[&str], functions: &[&str]) -> (Output, String, String) { let dir = tempfile::tempdir().unwrap(); let input = dir.path().join("fixture.rs"); fs::write(&input, CODE).unwrap(); - let current = std::env::current_exe().unwrap(); - let binary = current.parent().unwrap().parent().unwrap().join("rust_verify"); - let mut command = Command::new(binary); - command.args(["--mcp", "--crate-type=lib", "-V", "no-solver-version-check"]); + let mut args = vec!["--crate-type=lib", "-V", "no-solver-version-check"]; for m in modules { - if *m == "--verify-root" { - command.arg(m); - } else { - command.args(["--verify-only-module", m]); + if *m != "--verify-root" { + args.push("--verify-only-module"); } + args.push(*m); } for f in functions { - command.args(["--verify-function", f]); + args.extend(["--verify-function", *f]); } - let output = command.arg(&input).output().unwrap(); + args.push(input.to_str().unwrap()); + let output = run_verus_raw(&args, dir.path()); let stdout = String::from_utf8_lossy(&output.stdout).into_owned(); let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); (output, stdout, stderr) @@ -130,16 +144,17 @@ fn verify_function_reports_every_bad_pattern() { let (output, stdout, stderr) = run(&["delta", "alpha", "zeta"]); assert!(!output.status.success()); assert!(!stdout.contains("verified"), "{}", stdout); - // One error, holding each pattern's message as a single flag words it - let message = |s: &str| { + // One error, holding each pattern's message as a single flag words it, + // separated by a blank line (compared line by line, without the indentation) + let message = |s: &str| -> Vec { let start = s.find("error: ").unwrap() + "error: ".len(); let end = s.find("\nerror: aborting").unwrap(); - s[start..end].trim_end().to_string() + s[start..end].trim_end().lines().map(|line| line.trim().to_string()).collect() }; - assert_eq!( - message(&stderr), - format!("{}\n \n {}", message(&delta_stderr), message(&zeta_stderr)) - ); + let mut expected = message(&delta_stderr); + expected.push(String::new()); + expected.extend(message(&zeta_stderr)); + assert_eq!(message(&stderr), expected); assert!(stderr.contains("error: aborting due to 1 previous error"), "{}", stderr); } @@ -196,3 +211,69 @@ fn verify_function_in_root_and_a_module() { assert!(output.status.success(), "{}", stderr); assert_eq!(stdout, results(3)); } + +#[test] +fn verify_function_wildcard_across_modules() { + let (output, stdout, stderr) = run_in(&["first", "second"], &["*shared"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +#[test] +fn verify_function_ambiguity_across_modules_suggests_a_wildcard_that_works() { + let (output, _, stderr) = run_in(&["first", "second"], &["shar"]); + assert!(!output.status.success()); + assert!( + stderr.contains( + "more than one match found for --verify-function shar, consider using wildcard *shar* to verify all matched results," + ), + "{}", + stderr + ); + let (output, stdout, stderr) = run_in(&["first", "second"], &["*shar*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +// On main, a module-qualified pattern with a single module is "could not find function". +#[test] +fn verify_function_qualified_with_one_module() { + let (output, stdout, stderr) = run_in(&["first"], &["first::shared"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + + let (output, stdout, stderr) = run_in(&["first"], &["first::only_*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + + let (output, stdout, stderr) = run(&["crate::beta"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + + // The hints keep the qualifier + let (output, _, stderr) = run(&["crate::alph"]); + assert!(!output.status.success()); + assert!(stderr.contains("consider using wildcard crate::*alph*"), "{}", stderr); +} + +#[test] +fn verify_function_qualified_by_the_path_from_crate() { + let (output, stdout, stderr) = run_in(&["first"], &["crate::first::shared"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + + let (output, stdout, stderr) = + run_in(&["--verify-root", "first"], &["crate::first::shared", "crate::beta"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +// `point::f` names the method `f` of struct `third::point`; it is not `f` in module `point`. +#[test] +fn verify_function_name_that_starts_with_a_module_name() { + let (output, stdout, stderr) = run_in(&["point", "third"], &["point::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + assert_eq!(stderr.matches("note: verifying module third (selected functions)").count(), 1); + assert_eq!(stderr.matches("note: verifying module point").count(), 0, "{}", stderr); +} From 7971dc6c63f35738f48e3f36b2652b4322158da4 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Thu, 8 Oct 2026 04:28:07 +0000 Subject: [PATCH 4/7] --verify-function: match every reading of a qualified pattern together A qualified pattern was matched as written first, and read as qualified only if that failed. So `a::f` could select `Data::f` (a unique substring match) over `f` in module `a`, and an ambiguity across modules could be resolved silently by the qualified reading. - With several modules, each function is matched by the pattern as written and by the pattern without its own module qualifier, in the same step: exact (or wildcard) matches first, then unique substring matches. An exact name that matches in two modules, by any reading, is an error; its hint names `crate::m::f` when `m::f` is the pattern itself. - With one module, the pattern is first matched only as written, exactly as on main, so every pattern that works on main selects the same functions with byte-identical output; qualified readings apply only when that fails. - Qualifiers come from the module's friendly name (the one names are made relative to), with the crate name written `crate`; a name that is not relative to its module is shown and matched as is, not prefixed. - Wildcard hints list one wildcard per reading that matched. - The four error listings share one helper. - The help text no longer stops mid-sentence. - The two-module ambiguity test compares lines without rustc's indentation. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 2 +- source/rust_verify/src/user_filter.rs | 335 ++++++++++-------- source/rust_verify/src/verifier.rs | 6 +- .../rust_verify_test/tests/verify_function.rs | 129 ++++++- 4 files changed, 294 insertions(+), 178 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 09f2de6239..87dff1e3b0 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,7 +576,7 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern can be qualified by its module (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nan exact name found in several modules must be", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern can be qualified by its module (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nan exact name found in several modules must be qualified", "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index bf4de1d71a..609907044b 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -1,11 +1,14 @@ use crate::buckets::{Bucket, BucketId}; use crate::config::Args; use crate::util::error; -use crate::verifier::{module_name, module_name_of_segments}; +use crate::verifier::module_name; use std::collections::HashSet; use std::sync::Arc; use vir::ast::{Fun, Function, Krate, VirErr}; -use vir::ast_util::{friendly_fun_name_crate_relative, parse_path_segments_from_user_str}; +use vir::ast_util::{ + friendly_fun_name_crate_relative, fun_as_friendly_rust_name, parse_path_segments_from_user_str, + path_as_friendly_rust_name, +}; #[derive(Clone, Debug)] pub enum UserFilter { @@ -19,6 +22,44 @@ pub enum UserFilter { type ModuleId = vir::ast::Idents; +/// A function in one of the selected modules, with the names a pattern can match it by +struct FunName { + fun: Fun, + /// Index of the function's module among the selected modules + module: usize, + /// The name relative to the module, which an unqualified pattern matches + name: String, + /// The module qualifiers that a pattern can put before `name` + /// (`foo::bar::` and `crate::foo::bar::`, or `crate::` for the root module); + /// empty if `name` is not relative to the module + qualifiers: Vec, +} + +impl FunName { + /// The name qualified by its module, shown when several modules are selected + fn qualified(&self) -> String { + format!("{}{}", self.qualifiers.first().map_or("", |q| q.as_str()), self.name) + } + + /// The name qualified by the path of its module from the crate root + fn absolute(&self) -> String { + format!("{}{}", self.qualifiers.last().map_or("", |q| q.as_str()), self.name) + } + + /// The ways to read `pattern` for this function: + /// as written (with qualifier ""), and without each qualifier it starts with. + /// Each reading is (qualifier, pattern without the qualifier). + fn readings<'p>(&self, pattern: &'p str, qualify: bool) -> Vec<(&str, &'p str)> { + let qualified = self + .qualifiers + .iter() + .filter(|q| qualify && pattern.len() > q.len() && pattern.starts_with(q.as_str())); + std::iter::once(("", pattern)) + .chain(qualified.map(|q| (q.as_str(), &pattern[q.len()..]))) + .collect() + } +} + fn root_module_id() -> ModuleId { Arc::new(vec![]) } @@ -74,23 +115,13 @@ impl UserFilter { } // Name each module's functions once, rather than once per pattern - let module_fun_names: Vec> = modules - .iter() - .map(|module| Self::module_fun_names(module, &local_krate.functions)) - .collect(); - // How a pattern names each module: `crate` for the root, else its path - let qualifiers: Vec = modules - .iter() - .map( - |m| if m.is_empty() { "crate".to_string() } else { module_name_of_segments(m) }, - ) - .collect(); + let funs = Self::fun_names(&modules, &local_krate.functions); // Resolve every pattern before failing, so that one run reports all the bad ones let mut matches = HashSet::new(); let mut errors = Vec::new(); for func_name in &args.verify_function { - match Self::get_matches(&qualifiers, &module_fun_names, func_name) { + match Self::get_matches(&funs, modules.len() > 1, func_name) { Ok(m) => matches.extend(m), Err(msg) => errors.push(msg), } @@ -190,75 +221,57 @@ impl UserFilter { } } - /// The functions owned by the module, each with its name relative to the module. - fn module_fun_names(module_id: &ModuleId, funs: &Vec) -> Vec<(Fun, String)> { + /// The functions owned by the modules, each with the names a pattern can match it by. + fn fun_names(modules: &[ModuleId], funs: &Vec) -> Vec { funs.iter() - .filter(|f| match &f.x.owning_module { - None => false, - Some(m) => module_id == &m.segments, - }) - .map(|f| { - let name = friendly_fun_name_crate_relative( - f.x.owning_module.as_ref().unwrap(), - &f.x.name, - ); - (f.x.name.clone(), name) + .filter_map(|f| { + let owning_module = f.x.owning_module.as_ref()?; + let module = modules.iter().position(|m| m == &owning_module.segments)?; + let name = friendly_fun_name_crate_relative(owning_module, &f.x.name); + // Qualify with the module name that `name` was made relative to, + // which starts with the crate's name, written `crate` in a pattern + let qualifiers = if name == fun_as_friendly_rust_name(&f.x.name) { + vec![] + } else { + match path_as_friendly_rust_name(owning_module).split_once("::") { + Some((_, relative)) => { + vec![format!("{relative}::"), format!("crate::{relative}::")] + } + None => vec!["crate::".to_string()], + } + }; + Some(FunName { fun: f.x.name.clone(), module, name, qualifiers }) }) .collect() } /// Get the functions that match the given pattern. /// - /// The pattern is first matched as written, in all the selected modules. - /// If that fails and the pattern starts with the name of a selected module - /// (`foo::bar::f` or `crate::foo::bar::f`, or `crate::f` for the root module), - /// the rest of the pattern is matched in that module only, - /// trying the longest such module name first. + /// A pattern can be qualified by the module of the functions it names + /// (`foo::bar::f` or `crate::foo::bar::f`, or `crate::f` for the root module). + /// A function matches if the pattern, either as written or without its module qualifier, + /// matches the function's name relative to its module; every reading takes part + /// in each step of the search. + /// + /// With one module, the pattern is first matched only as written, + /// as it was before qualifiers existed, so that such a pattern selects the same functions. /// /// Errors (with the message) if there is no match. fn get_matches( - qualifiers: &[String], - module_fun_names: &[Vec<(Fun, String)>], - pattern: &String, + funs: &[FunName], + several_modules: bool, + pattern: &str, ) -> Result, String> { - let all_modules: Vec = (0..module_fun_names.len()).collect(); - let unqualified = - Self::get_matches_in(qualifiers, module_fun_names, &all_modules, "", pattern, pattern); - if unqualified.is_ok() { - return unqualified; - } - let mut prefixes: Vec<(usize, String)> = qualifiers - .iter() - .enumerate() - .flat_map(|(i, q)| { - let absolute = (q != "crate").then(|| format!("crate::{q}::")); - std::iter::once(format!("{q}::")).chain(absolute).map(move |p| (i, p)) - }) - .filter(|(_, p)| pattern.len() > p.len() && pattern.starts_with(p.as_str())) - .collect(); - prefixes.sort_by_key(|(_, p)| std::cmp::Reverse(p.len())); - let mut qualified_err = None; - for (i, prefix) in prefixes { - let function_pattern = &pattern[prefix.len()..]; - match Self::get_matches_in( - qualifiers, - module_fun_names, - &[i], - &prefix, - pattern, - function_pattern, - ) { - Ok(m) => return Ok(m), - Err(msg) => { - qualified_err.get_or_insert(msg); - } + if !several_modules { + if let Ok(matches) = Self::get_matches_in(funs, false, pattern, false) { + return Ok(matches); } } - Err(qualified_err.unwrap_or_else(|| unqualified.unwrap_err())) + Self::get_matches_in(funs, several_modules, pattern, true) } - /// Get the functions in the given modules that match `function_pattern`, - /// which is `pattern` without the module qualifier `prefix`. + /// Get the functions that match `pattern`, read without a module qualifier + /// unless `qualify` is set. /// /// The first part of this process is to /// infer whether this is an "exact match" filter. @@ -271,132 +284,140 @@ impl UserFilter { /// /// Errors (with the message) if there is no match. fn get_matches_in( - qualifiers: &[String], - module_fun_names: &[Vec<(Fun, String)>], - modules: &[usize], - prefix: &str, + funs: &[FunName], + several_modules: bool, pattern: &str, - function_pattern: &str, + qualify: bool, ) -> Result, String> { - let several_modules = module_fun_names.len() > 1; - let funs: Vec<(usize, &(Fun, String))> = - modules.iter().flat_map(|&i| module_fun_names[i].iter().map(move |f| (i, f))).collect(); // With several modules, show each function qualified by its module - let display = |(i, (_, name)): &(usize, &(Fun, String))| { - if several_modules { format!("{}::{name}", qualifiers[*i]) } else { name.clone() } - }; - let display_sorted = |funs: &Vec<(usize, &(Fun, String))>| { - let mut names = funs.iter().map(display).collect::>(); + let display = |f: &FunName| if several_modules { f.qualified() } else { f.name.clone() }; + let display_sorted = |funs: &Vec<&FunName>| { + let mut names = funs.iter().map(|f| display(f)).collect::>(); names.sort(); names }; + let exact = !pattern.contains('*'); // First, get the matches without doing anything fancy: // If the user provides a * pattern, then we filter according to the * pattern; // if the user provides an exact match (no *), then filter as an exact match. // If we find anything this way, we're done. - let matches = Self::get_matches_strictly_by_pattern(function_pattern, &funs); - let clean = function_pattern.trim_matches('*'); + let matches: Vec<&FunName> = funs + .iter() + .filter(|f| { + let readings = f.readings(pattern, qualify); + readings.iter().any(|(_, p)| Self::matches_strictly_by_pattern(p, &f.name)) + }) + .collect(); if matches.len() > 0 { - let first_module = matches[0].0; - if clean == function_pattern && matches.iter().any(|(i, _)| *i != first_module) { - let msg = vec![ - format!( - "--verify-function {pattern} matches functions in more than one module, qualify it with the module (e.g. {}::{function_pattern}),", - qualifiers[first_module] - ), - format!("matched results are:"), - ] - .into_iter() - .chain(display_sorted(&matches).iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(msg); + if exact && matches.iter().any(|f| f.module != matches[0].module) { + let first = matches.iter().min_by_key(|f| display(f)).unwrap(); + let example = + if display(first) == pattern { first.absolute() } else { display(first) }; + return Err(Self::listing( + vec![ + format!( + "--verify-function {pattern} matches functions in more than one module, qualify it with the module (e.g. {example})," + ), + format!("matched results are:"), + ], + display_sorted(&matches), + )); } - return Ok(matches.into_iter().map(|(_, f)| f.0.clone()).collect()); + return Ok(matches.into_iter().map(|f| f.fun.clone()).collect()); } // Get all substring matches, even if the user didn't use any * in their pattern. // We might use of these automatically, or if not, this list will at least help us // print an informative error message. - let substring_matches = Self::get_all_substring_matches(function_pattern, &funs); + // Each reading that matches suggests a wildcard pattern selecting its matches. + let mut substring_matches: Vec<&FunName> = Vec::new(); + let mut wildcards: Vec = Vec::new(); + for f in funs { + let mut matched = false; + for (qualifier, p) in f.readings(pattern, qualify) { + let clean = p.trim_matches('*'); + if f.name.contains(clean) { + matched = true; + let wildcard = format!("{qualifier}*{clean}*"); + if !wildcards.contains(&wildcard) { + wildcards.push(wildcard); + } + } + } + if matched { + substring_matches.push(f); + } + } + let wildcards = wildcards.join(" and "); - if clean == function_pattern { + if exact { // If there's no exact match, but there is *exactly one* substring match, // then we go ahead and use that function. if substring_matches.len() == 1 { - return Ok(substring_matches.iter().map(|f| f.1.0.clone()).collect()); + return Ok(substring_matches.iter().map(|f| f.fun.clone()).collect()); } else if substring_matches.len() > 1 { - let msg = vec![ - format!( - "more than one match found for --verify-function {pattern}, consider using wildcard {prefix}*{function_pattern}* to verify all matched results," - ), - format!( - "or specify a unique substring for the desired function, matched results are:" - ), - ].into_iter() - .chain(display_sorted(&substring_matches).iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(msg); + let wildcard = if wildcards.contains(" and ") { "wildcards" } else { "wildcard" }; + return Err(Self::listing( + vec![ + format!( + "more than one match found for --verify-function {pattern}, consider using {wildcard} {wildcards} to verify all matched results," + ), + format!( + "or specify a unique substring for the desired function, matched results are:" + ), + ], + display_sorted(&substring_matches), + )); } } else { if substring_matches.len() >= 1 { - let msg = vec![ - format!("could not find function {pattern} specified by --verify-function,"), - format!("consider {prefix}*{clean}* if you want to verify similar functions:"), - ] - .into_iter() - .chain(display_sorted(&substring_matches).iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(msg); + return Err(Self::listing( + vec![ + format!( + "could not find function {pattern} specified by --verify-function," + ), + format!("consider {wildcards} if you want to verify similar functions:"), + ], + display_sorted(&substring_matches), + )); } } // If there were absolutely no substring matches, then we fail by printing // out every possible function in the module. - let msg = vec![ - format!("could not find function {pattern} specified by --verify-function"), - format!("available functions are:"), - ] - .into_iter() - .chain(display_sorted(&funs).iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(msg); + Err(Self::listing( + vec![ + format!("could not find function {pattern} specified by --verify-function"), + format!("available functions are:"), + ], + display_sorted(&funs.iter().collect()), + )) + } + + /// An error message: the header lines, then one line per name + fn listing(header: Vec, names: Vec) -> String { + header + .into_iter() + .chain(names.iter().map(|f| format!(" - {f}"))) + .collect::>() + .join("\n") } - fn get_matches_strictly_by_pattern<'a>( - function_pattern: &str, - funs: &Vec<(usize, &'a (Fun, String))>, - ) -> Vec<(usize, &'a (Fun, String))> { + fn matches_strictly_by_pattern(function_pattern: &str, name: &str) -> bool { let clean = function_pattern.trim_matches('*'); let left_wildcard = function_pattern.starts_with('*'); let right_wildcard = function_pattern.ends_with('*'); - funs.iter() - .filter(|(_, (_, name))| { - if left_wildcard && !right_wildcard { - name.ends_with(clean) - } else if !left_wildcard && right_wildcard { - name.starts_with(clean) - } else if left_wildcard && right_wildcard { - name.contains(clean) - } else { - name == clean - } - }) - .cloned() - .collect() - } - - fn get_all_substring_matches<'a>( - function_pattern: &str, - funs: &Vec<(usize, &'a (Fun, String))>, - ) -> Vec<(usize, &'a (Fun, String))> { - let clean = function_pattern.trim_matches('*'); - funs.iter().filter(|(_, (_, name))| name.contains(clean)).cloned().collect() + if left_wildcard && !right_wildcard { + name.ends_with(clean) + } else if !left_wildcard && right_wildcard { + name.starts_with(clean) + } else if left_wildcard && right_wildcard { + name.contains(clean) + } else { + name == clean + } } /// Check if the function is included in the filter. diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index d8d62a4c88..379386f278 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -584,11 +584,7 @@ pub(crate) fn io_vir_err(msg: String, err: std::io::Error) -> VirErr { } pub fn module_name(module: &vir::ast::Path) -> String { - module_name_of_segments(&module.segments) -} - -pub fn module_name_of_segments(segments: &vir::ast::Idents) -> String { - segments.iter().map(|s| s.to_string()).collect::>().join("::") + module.segments.iter().map(|s| s.to_string()).collect::>().join("::") } mod util { diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index ae2823457d..361ffc4f56 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -19,11 +19,13 @@ mod first { verus! { proof fn shared() { assert(4int + 4 == 8); } proof fn only_first() { assert(5int + 5 == 10); } + impl crate::second::Item { proof fn moved() { assert(10int == 10); } } } } mod second { use vstd::prelude::*; verus! { + pub struct Item {} proof fn shared() { assert(6int + 6 == 12); } proof fn only_second() { assert(7int + 7 == 14); } } @@ -42,6 +44,36 @@ mod third { impl point { proof fn f() { assert(8int == 8); } } } } +mod a { + use vstd::prelude::*; + verus! { + proof fn f() { assert(9int == 9); } + pub struct Data {} + impl Data { proof fn f() { assert(false); } } + } +} +mod cell { + use vstd::prelude::*; + verus! { + proof fn f() { assert(11int == 11); } + } +} +mod fifth { + use vstd::prelude::*; + verus! { + #[allow(non_camel_case_types)] + pub struct cell {} + impl cell { proof fn f() { assert(12int == 12); } } + } +} +mod sixth { + use vstd::prelude::*; + verus! { + #[allow(non_camel_case_types)] + pub struct cell {} + impl cell { proof fn f() { assert(13int == 13); } } + } +} "#; // `gamma` fails, so a run that verifies it reports an error. @@ -71,6 +103,13 @@ fn run_in(modules: &[&str], functions: &[&str]) -> (Output, String, String) { (output, stdout, stderr) } +// The lines of the error message, without rustc's indentation +fn error_lines(stderr: &str) -> Vec { + let start = stderr.find("error: ").unwrap() + "error: ".len(); + let end = stderr.find("\nerror: aborting").unwrap(); + stderr[start..end].trim_end().lines().map(|line| line.trim().to_string()).collect() +} + fn results(n: usize) -> String { format!( "verification results:: {n} verified, 0 errors (partial verification with `--verify-*`)\n" @@ -145,16 +184,11 @@ fn verify_function_reports_every_bad_pattern() { assert!(!output.status.success()); assert!(!stdout.contains("verified"), "{}", stdout); // One error, holding each pattern's message as a single flag words it, - // separated by a blank line (compared line by line, without the indentation) - let message = |s: &str| -> Vec { - let start = s.find("error: ").unwrap() + "error: ".len(); - let end = s.find("\nerror: aborting").unwrap(); - s[start..end].trim_end().lines().map(|line| line.trim().to_string()).collect() - }; - let mut expected = message(&delta_stderr); + // separated by a blank line + let mut expected = error_lines(&delta_stderr); expected.push(String::new()); - expected.extend(message(&zeta_stderr)); - assert_eq!(message(&stderr), expected); + expected.extend(error_lines(&zeta_stderr)); + assert_eq!(error_lines(&stderr), expected); assert!(stderr.contains("error: aborting due to 1 previous error"), "{}", stderr); } @@ -182,12 +216,14 @@ fn verify_function_in_two_modules_requires_qualifying_a_shared_name() { let (output, stdout, stderr) = run_in(&["first", "second"], &["shared"]); assert!(!output.status.success()); assert!(!stdout.contains("verified"), "{}", stdout); - assert!( - stderr.contains( - "error: --verify-function shared matches functions in more than one module, qualify it with the module (e.g. first::shared),\n matched results are:\n - first::shared\n - second::shared\n" - ), - "{}", - stderr + assert_eq!( + error_lines(&stderr), + [ + "--verify-function shared matches functions in more than one module, qualify it with the module (e.g. first::shared),", + "matched results are:", + "- first::shared", + "- second::shared", + ] ); } @@ -277,3 +313,66 @@ fn verify_function_name_that_starts_with_a_module_name() { assert_eq!(stderr.matches("note: verifying module third (selected functions)").count(), 1); assert_eq!(stderr.matches("note: verifying module point").count(), 0, "{}", stderr); } + +// The qualified reading `f` in module `a` is an exact match, +// so it wins over `Data::f`, whose name merely contains `a::f`. +#[test] +fn verify_function_qualified_name_is_not_read_as_a_substring() { + let (output, stdout, stderr) = run_in(&["a", "first"], &["a::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); +} + +// With one module, a pattern that works on main selects what it selects on main: +// `a::f` is the unique substring match `Data::f`, which fails. +// The path from `crate` names `f` in module `a`. +#[test] +fn verify_function_qualified_with_one_module_as_on_main() { + let (output, stdout, stderr) = run_in(&["a"], &["a::f"]); + assert!(!output.status.success()); + assert_eq!(stderr.matches("error: assertion failed").count(), 1, "{}", stderr); + assert!(stdout.contains("0 verified, 1 errors"), "{}", stdout); + + let (output, stdout, stderr) = run_in(&["a"], &["crate::a::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); +} + +// `cell::f` names `f` in module `cell` and the methods `cell::f` in `fifth` and `sixth`. +#[test] +fn verify_function_qualified_and_unqualified_readings_are_ambiguous() { + let (output, stdout, stderr) = run_in(&["cell", "fifth", "sixth"], &["cell::f"]); + assert!(!output.status.success()); + assert!(!stdout.contains("verified"), "{}", stdout); + assert_eq!( + error_lines(&stderr), + [ + "--verify-function cell::f matches functions in more than one module, qualify it with the module (e.g. crate::cell::f),", + "matched results are:", + "- cell::f", + "- fifth::cell::f", + "- sixth::cell::f", + ] + ); + + let (output, stdout, stderr) = + run_in(&["cell", "fifth", "sixth"], &["crate::cell::f", "fifth::cell::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); + assert_eq!(stderr.matches("note: verifying module sixth").count(), 0, "{}", stderr); +} + +// `moved` is owned by `first` but named by the path of `second::Item`, from the crate's name, +// so it is listed (and matched) by that name, without `first::` before it. +#[test] +fn verify_function_lists_a_name_from_another_module_as_is() { + let (output, _, stderr) = run_in(&["first", "second"], &["zzz"]); + assert!(!output.status.success()); + let lines = error_lines(&stderr); + assert!(lines.contains(&"- fixture::second::Item::moved".to_string()), "{}", stderr); + assert!(!stderr.contains("first::fixture"), "{}", stderr); + + let (output, stdout, stderr) = run_in(&["first", "second"], &["fixture::second::Item::moved"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); +} From 8ae4c45433180ce80fc3134a90fecbb83f6b6701 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Thu, 8 Oct 2026 07:18:09 +0000 Subject: [PATCH 5/7] --verify-function: one rule for qualified patterns and several modules With one module, every pattern selects what it selects on main. Otherwise (several modules, or a pattern with `::` that main cannot resolve), a pattern with `::` is also matched against each function's path from the crate root, with or without `crate::`, and a pattern without `*` at its ends must select exactly one function, whether or not the matches share a module. The ambiguity hint suggests a name that the same rule resolves to one function, and the wildcard hints match by the same names, so they select what is listed. A function named by a path outside its module (`impl crate::second::Item` inside `first`) can now be named `crate::second::Item::moved`. A pattern is exact when it has no `*` at either end, as on main. A repeated pattern is resolved (and reported) once. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 2 +- source/rust_verify/src/user_filter.rs | 319 +++++++++--------- .../rust_verify_test/tests/verify_function.rs | 136 +++++++- 3 files changed, 285 insertions(+), 172 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 87dff1e3b0..a709cb07fd 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,7 +576,7 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern can be qualified by its module (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nan exact name found in several modules must be qualified", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nwith several modules, or a pattern with :: that matches nothing within one module, \na pattern without * at its ends must match exactly one function", "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index 609907044b..9aa7800094 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -7,8 +7,8 @@ use std::sync::Arc; use vir::ast::{Fun, Function, Krate, VirErr}; use vir::ast_util::{ friendly_fun_name_crate_relative, fun_as_friendly_rust_name, parse_path_segments_from_user_str, - path_as_friendly_rust_name, }; +use vir::def::krate_to_string_ignore_stable_id; #[derive(Clone, Debug)] pub enum UserFilter { @@ -25,39 +25,39 @@ type ModuleId = vir::ast::Idents; /// A function in one of the selected modules, with the names a pattern can match it by struct FunName { fun: Fun, - /// Index of the function's module among the selected modules - module: usize, - /// The name relative to the module, which an unqualified pattern matches + /// The name relative to the function's module, as on main name: String, - /// The module qualifiers that a pattern can put before `name` - /// (`foo::bar::` and `crate::foo::bar::`, or `crate::` for the root module); - /// empty if `name` is not relative to the module - qualifiers: Vec, + /// The path from the crate root and the same path after `crate::`, + /// if the function's name starts with the crate's name + path: Option<(String, String)>, + /// The name shown when several modules are selected + listed: String, } impl FunName { - /// The name qualified by its module, shown when several modules are selected - fn qualified(&self) -> String { - format!("{}{}", self.qualifiers.first().map_or("", |q| q.as_str()), self.name) + /// The names a pattern is matched against: the relative name, + /// and if `qualified`, also the path from the crate root, with and without `crate::` + fn names(&self, qualified: bool) -> impl Iterator { + let paths = self.path.as_ref().filter(|_| qualified); + std::iter::once(self.name.as_str()) + .chain(paths.into_iter().flat_map(|(p, c)| [p.as_str(), c.as_str()])) } - /// The name qualified by the path of its module from the crate root - fn absolute(&self) -> String { - format!("{}{}", self.qualifiers.last().map_or("", |q| q.as_str()), self.name) + fn display(&self, several_modules: bool) -> &str { + if several_modules { &self.listed } else { &self.name } } +} - /// The ways to read `pattern` for this function: - /// as written (with qualifier ""), and without each qualifier it starts with. - /// Each reading is (qualifier, pattern without the qualifier). - fn readings<'p>(&self, pattern: &'p str, qualify: bool) -> Vec<(&str, &'p str)> { - let qualified = self - .qualifiers - .iter() - .filter(|q| qualify && pattern.len() > q.len() && pattern.starts_with(q.as_str())); - std::iter::once(("", pattern)) - .chain(qualified.map(|q| (q.as_str(), &pattern[q.len()..]))) - .collect() - } +/// What a pattern selects, or why it selects nothing +enum Resolution<'a> { + Selected(Vec<&'a FunName>), + /// An exact pattern that matches several functions + Ambiguous(Vec<&'a FunName>), + /// An exact pattern that matches no function, but is a substring of several + Substrings(Vec<&'a FunName>), + /// A wildcard pattern that matches no function, but whose `*`-less text is a substring of some + Similar(Vec<&'a FunName>), + NotFound, } fn root_module_id() -> ModuleId { @@ -116,14 +116,16 @@ impl UserFilter { // Name each module's functions once, rather than once per pattern let funs = Self::fun_names(&modules, &local_krate.functions); + let several_modules = modules.len() > 1; // Resolve every pattern before failing, so that one run reports all the bad ones let mut matches = HashSet::new(); let mut errors = Vec::new(); - for func_name in &args.verify_function { - match Self::get_matches(&funs, modules.len() > 1, func_name) { - Ok(m) => matches.extend(m), - Err(msg) => errors.push(msg), + let mut seen = HashSet::new(); + for pattern in args.verify_function.iter().filter(|p| seen.insert(p.as_str())) { + match Self::resolve(&funs, several_modules, pattern) { + Resolution::Selected(m) => matches.extend(m.iter().map(|f| f.fun.clone())), + failure => errors.push(Self::message(&funs, several_modules, pattern, failure)), } } if !errors.is_empty() { @@ -228,75 +230,60 @@ impl UserFilter { let owning_module = f.x.owning_module.as_ref()?; let module = modules.iter().position(|m| m == &owning_module.segments)?; let name = friendly_fun_name_crate_relative(owning_module, &f.x.name); - // Qualify with the module name that `name` was made relative to, - // which starts with the crate's name, written `crate` in a pattern - let qualifiers = if name == fun_as_friendly_rust_name(&f.x.name) { - vec![] - } else { - match path_as_friendly_rust_name(owning_module).split_once("::") { - Some((_, relative)) => { - vec![format!("{relative}::"), format!("crate::{relative}::")] - } - None => vec!["crate::".to_string()], - } + // The path from the crate root is the full name without the crate's name, + // even for a function named by a path outside its module + let krate = krate_to_string_ignore_stable_id(&owning_module.krate); + let full = fun_as_friendly_rust_name(&f.x.name); + let path = full + .strip_prefix(&format!("{krate}::")) + .map(|p| (p.to_string(), format!("crate::{p}"))); + let listed = match &path { + Some((_, from_crate)) if modules[module].is_empty() => from_crate.clone(), + Some((p, _)) => p.clone(), + None => name.clone(), }; - Some(FunName { fun: f.x.name.clone(), module, name, qualifiers }) + Some(FunName { fun: f.x.name.clone(), name, path, listed }) }) .collect() } - /// Get the functions that match the given pattern. - /// - /// A pattern can be qualified by the module of the functions it names - /// (`foo::bar::f` or `crate::foo::bar::f`, or `crate::f` for the root module). - /// A function matches if the pattern, either as written or without its module qualifier, - /// matches the function's name relative to its module; every reading takes part - /// in each step of the search. + /// Resolve one pattern. /// - /// With one module, the pattern is first matched only as written, - /// as it was before qualifiers existed, so that such a pattern selects the same functions. - /// - /// Errors (with the message) if there is no match. - fn get_matches( - funs: &[FunName], - several_modules: bool, - pattern: &str, - ) -> Result, String> { + /// With one module, a pattern selects what it selects on main + /// (see `resolve_by`, matching the names relative to the module, where + /// an exact name may select several functions). + /// Otherwise (several modules, or a pattern with `::` that selects nothing on main), + /// the general rule applies: a pattern with `::` is also matched against each function's + /// path from the crate root, with or without `crate::`, + /// and a pattern without `*` at its ends must select exactly one function. + fn resolve<'a>(funs: &'a [FunName], several_modules: bool, pattern: &str) -> Resolution<'a> { + let qualified = pattern.contains("::"); if !several_modules { - if let Ok(matches) = Self::get_matches_in(funs, false, pattern, false) { - return Ok(matches); + let on_main = Self::resolve_by(funs, pattern, false, false); + if !qualified || matches!(on_main, Resolution::Selected(_)) { + return on_main; } } - Self::get_matches_in(funs, several_modules, pattern, true) + Self::resolve_by(funs, pattern, qualified, true) } - /// Get the functions that match `pattern`, read without a module qualifier - /// unless `qualify` is set. - /// /// The first part of this process is to /// infer whether this is an "exact match" filter. - /// (If the user doesn't supply any * in the pattern, then it is usuall + /// (If the user doesn't supply any * at the ends of the pattern, then it is usually /// exact - however, if there is no exact match, but there is _exactly one_ - /// partial match, then we upgrade to a partial match, i.e., return false) + /// partial match, then we upgrade to a partial match) /// - /// A wildcard pattern selects its matches in every module, - /// but an exact name must not match in two modules. - /// - /// Errors (with the message) if there is no match. - fn get_matches_in( - funs: &[FunName], - several_modules: bool, + /// Each function is matched by its relative name, and if `qualified`, + /// by its path from the crate root too. + /// If `unique`, an exact pattern that matches several functions is ambiguous. + fn resolve_by<'a>( + funs: &'a [FunName], pattern: &str, - qualify: bool, - ) -> Result, String> { - // With several modules, show each function qualified by its module - let display = |f: &FunName| if several_modules { f.qualified() } else { f.name.clone() }; - let display_sorted = |funs: &Vec<&FunName>| { - let mut names = funs.iter().map(|f| display(f)).collect::>(); - names.sort(); - names - }; - let exact = !pattern.contains('*'); + qualified: bool, + unique: bool, + ) -> Resolution<'a> { + let clean = pattern.trim_matches('*'); + let exact = clean == pattern; // First, get the matches without doing anything fancy: // If the user provides a * pattern, then we filter according to the * pattern; @@ -304,95 +291,103 @@ impl UserFilter { // If we find anything this way, we're done. let matches: Vec<&FunName> = funs .iter() - .filter(|f| { - let readings = f.readings(pattern, qualify); - readings.iter().any(|(_, p)| Self::matches_strictly_by_pattern(p, &f.name)) - }) + .filter(|f| f.names(qualified).any(|n| Self::matches_strictly_by_pattern(pattern, n))) .collect(); - if matches.len() > 0 { - if exact && matches.iter().any(|f| f.module != matches[0].module) { - let first = matches.iter().min_by_key(|f| display(f)).unwrap(); - let example = - if display(first) == pattern { first.absolute() } else { display(first) }; - return Err(Self::listing( - vec![ - format!( - "--verify-function {pattern} matches functions in more than one module, qualify it with the module (e.g. {example})," - ), - format!("matched results are:"), - ], - display_sorted(&matches), - )); - } - return Ok(matches.into_iter().map(|f| f.fun.clone()).collect()); + if matches.len() > 1 && exact && unique { + return Resolution::Ambiguous(matches); + } else if matches.len() > 0 { + return Resolution::Selected(matches); } // Get all substring matches, even if the user didn't use any * in their pattern. // We might use of these automatically, or if not, this list will at least help us // print an informative error message. - // Each reading that matches suggests a wildcard pattern selecting its matches. - let mut substring_matches: Vec<&FunName> = Vec::new(); - let mut wildcards: Vec = Vec::new(); - for f in funs { - let mut matched = false; - for (qualifier, p) in f.readings(pattern, qualify) { - let clean = p.trim_matches('*'); - if f.name.contains(clean) { - matched = true; - let wildcard = format!("{qualifier}*{clean}*"); - if !wildcards.contains(&wildcard) { - wildcards.push(wildcard); - } - } - } - if matched { - substring_matches.push(f); - } - } - let wildcards = wildcards.join(" and "); - - if exact { + // `*{clean}*` selects exactly these, by the same names. + let substring_matches: Vec<&FunName> = + funs.iter().filter(|f| f.names(qualified).any(|n| n.contains(clean))).collect(); + match (exact, substring_matches.len()) { + (_, 0) => Resolution::NotFound, // If there's no exact match, but there is *exactly one* substring match, // then we go ahead and use that function. - if substring_matches.len() == 1 { - return Ok(substring_matches.iter().map(|f| f.fun.clone()).collect()); - } else if substring_matches.len() > 1 { - let wildcard = if wildcards.contains(" and ") { "wildcards" } else { "wildcard" }; - return Err(Self::listing( - vec![ - format!( - "more than one match found for --verify-function {pattern}, consider using {wildcard} {wildcards} to verify all matched results," - ), - format!( - "or specify a unique substring for the desired function, matched results are:" - ), - ], - display_sorted(&substring_matches), - )); - } - } else { - if substring_matches.len() >= 1 { - return Err(Self::listing( - vec![ - format!( - "could not find function {pattern} specified by --verify-function," - ), - format!("consider {wildcards} if you want to verify similar functions:"), - ], - display_sorted(&substring_matches), - )); - } + (true, 1) => Resolution::Selected(substring_matches), + (true, _) => Resolution::Substrings(substring_matches), + (false, _) => Resolution::Similar(substring_matches), } + } - // If there were absolutely no substring matches, then we fail by printing - // out every possible function in the module. - Err(Self::listing( - vec![ - format!("could not find function {pattern} specified by --verify-function"), - format!("available functions are:"), - ], - display_sorted(&funs.iter().collect()), - )) + /// The error message for a pattern that selects nothing + fn message( + funs: &[FunName], + several_modules: bool, + pattern: &str, + failure: Resolution, + ) -> String { + let display_sorted = |funs: Vec<&FunName>| { + let mut names = + funs.iter().map(|f| f.display(several_modules).to_string()).collect::>(); + names.sort(); + names + }; + let clean = pattern.trim_matches('*'); + match failure { + Resolution::Selected(_) => unreachable!(), + Resolution::Ambiguous(matches) => { + // Suggest a name that this resolution selects just one of the matches by + let selects = + |name: &str, f: &FunName| match Self::resolve(funs, several_modules, name) { + Resolution::Selected(m) => m.len() == 1 && m[0].fun == f.fun, + _ => false, + }; + let mut sorted = matches.clone(); + sorted.sort_by(|f, g| f.display(several_modules).cmp(g.display(several_modules))); + let example = sorted.iter().find_map(|f| { + let candidates = [ + Some(f.display(several_modules)), + f.path.as_ref().map(|(_, c)| c.as_str()), + ]; + candidates.into_iter().flatten().find(|name| selects(name, f)) + }); + let header = match example { + Some(example) => format!( + "--verify-function {pattern} matches more than one function, use a name that matches only one (e.g. {example})," + ), + None => format!( + "--verify-function {pattern} matches more than one function and no name matches only one of them, consider using wildcard {pattern}* to verify them all," + ), + }; + Self::listing( + vec![header, format!("matched results are:")], + display_sorted(matches), + ) + } + Resolution::Substrings(matches) => Self::listing( + vec![ + format!( + "more than one match found for --verify-function {pattern}, consider using wildcard *{pattern}* to verify all matched results," + ), + format!( + "or specify a unique substring for the desired function, matched results are:" + ), + ], + display_sorted(matches), + ), + Resolution::Similar(matches) => Self::listing( + vec![ + format!("could not find function {pattern} specified by --verify-function,"), + format!("consider *{clean}* if you want to verify similar functions:"), + ], + display_sorted(matches), + ), + // If there were absolutely no substring matches, then we fail by printing + // out every possible function in the modules. + Resolution::NotFound => Self::listing( + vec![ + format!("could not find function {pattern} specified by --verify-function"), + format!("available functions are:"), + ], + display_sorted(funs.iter().collect()), + ), + } } /// An error message: the header lines, then one line per name diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index 361ffc4f56..41be00c10c 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -74,6 +74,31 @@ mod sixth { impl cell { proof fn f() { assert(13int == 13); } } } } +mod line { + use vstd::prelude::*; + verus! { + proof fn f() { assert(14int == 14); } + #[allow(non_camel_case_types)] + pub struct line {} + impl line { proof fn f() { assert(15int == 15); } } + } +} +mod eighth { + use vstd::prelude::*; + verus! { + #[allow(non_camel_case_types)] + pub struct first {} + impl first { proof fn shared() { assert(16int == 16); } } + } +} +mod ninth { + use vstd::prelude::*; + verus! { + pub struct G { t: T } + impl G { proof fn g() { assert(17int == 17); } } + impl G { proof fn g() { assert(18int == 18); } } + } +} "#; // `gamma` fails, so a run that verifies it reports an error. @@ -219,7 +244,7 @@ fn verify_function_in_two_modules_requires_qualifying_a_shared_name() { assert_eq!( error_lines(&stderr), [ - "--verify-function shared matches functions in more than one module, qualify it with the module (e.g. first::shared),", + "--verify-function shared matches more than one function, use a name that matches only one (e.g. first::shared),", "matched results are:", "- first::shared", "- second::shared", @@ -286,10 +311,13 @@ fn verify_function_qualified_with_one_module() { assert!(output.status.success(), "{}", stderr); assert_eq!(stdout, results(1)); - // The hints keep the qualifier + // The hint's wildcard matches the same names, so it selects the functions listed let (output, _, stderr) = run(&["crate::alph"]); assert!(!output.status.success()); - assert!(stderr.contains("consider using wildcard crate::*alph*"), "{}", stderr); + assert!(stderr.contains("consider using wildcard *crate::alph* "), "{}", stderr); + let (output, stdout, stderr) = run(&["*crate::alph*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); } #[test] @@ -347,7 +375,7 @@ fn verify_function_qualified_and_unqualified_readings_are_ambiguous() { assert_eq!( error_lines(&stderr), [ - "--verify-function cell::f matches functions in more than one module, qualify it with the module (e.g. crate::cell::f),", + "--verify-function cell::f matches more than one function, use a name that matches only one (e.g. crate::cell::f),", "matched results are:", "- cell::f", "- fifth::cell::f", @@ -362,17 +390,107 @@ fn verify_function_qualified_and_unqualified_readings_are_ambiguous() { assert_eq!(stderr.matches("note: verifying module sixth").count(), 0, "{}", stderr); } -// `moved` is owned by `first` but named by the path of `second::Item`, from the crate's name, -// so it is listed (and matched) by that name, without `first::` before it. +// `moved` is owned by `first` but named by the path of `second::Item`, +// so it is listed by that path from the crate root, and matched by it with or without `crate::` +// (or by its full name, as on main). #[test] -fn verify_function_lists_a_name_from_another_module_as_is() { +fn verify_function_names_a_function_by_its_path_from_the_crate_root() { let (output, _, stderr) = run_in(&["first", "second"], &["zzz"]); assert!(!output.status.success()); let lines = error_lines(&stderr); - assert!(lines.contains(&"- fixture::second::Item::moved".to_string()), "{}", stderr); + assert!(lines.contains(&"- second::Item::moved".to_string()), "{}", stderr); assert!(!stderr.contains("first::fixture"), "{}", stderr); - let (output, stdout, stderr) = run_in(&["first", "second"], &["fixture::second::Item::moved"]); + for pattern in + ["crate::second::Item::moved", "second::Item::moved", "fixture::second::Item::moved"] + { + for modules in [&["first", "second"][..], &["first"][..]] { + let (output, stdout, stderr) = run_in(modules, &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } + } +} + +// Two functions of one module that match the same name are ambiguous too, +// unless a single module is selected and the pattern works on main. +#[test] +fn verify_function_ambiguity_within_one_module() { + // `line::f` is the path of `f` in module `line`, and the name of the method `f` of `line::line` + let (output, stdout, stderr) = run_in(&["line", "first"], &["line::f"]); + assert!(!output.status.success()); + assert!(!stdout.contains("verified"), "{}", stdout); + assert_eq!( + error_lines(&stderr), + [ + "--verify-function line::f matches more than one function, use a name that matches only one (e.g. crate::line::f),", + "matched results are:", + "- line::f", + "- line::line::f", + ] + ); + for pattern in ["crate::line::f", "line::line::f"] { + let (output, stdout, stderr) = run_in(&["line", "first"], &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } + + // As on main: with `line` alone, `line::f` is the method's name relative to the module + let (output, stdout, stderr) = run_in(&["line"], &["line::f"]); assert!(output.status.success(), "{}", stderr); assert_eq!(stdout, results(1)); } + +// The example in the hint is a name that the same rule resolves to one function: +// `first::shared` is also the method `shared` of `eighth::first`, so the hint is `crate::first::shared`. +#[test] +fn verify_function_hint_names_just_one_function() { + let modules = ["first", "second", "eighth"]; + let (output, _, stderr) = run_in(&modules, &["shared"]); + assert!(!output.status.success()); + assert_eq!( + error_lines(&stderr), + [ + "--verify-function shared matches more than one function, use a name that matches only one (e.g. crate::first::shared),", + "matched results are:", + "- first::shared", + "- second::shared", + ] + ); + let (output, stdout, stderr) = run_in(&modules, &["crate::first::shared"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + assert_eq!(stderr.matches("note: verifying module eighth").count(), 0, "{}", stderr); +} + +// `G::g` and `G::g` are both named `G::g`: main verifies both with one module, +// and with several modules no name selects just one, so the hint is a wildcard. +#[test] +fn verify_function_functions_with_the_same_name() { + let (output, stdout, stderr) = run_in(&["ninth"], &["G::g"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); + + let (output, _, stderr) = run_in(&["ninth", "first"], &["G::g"]); + assert!(!output.status.success()); + assert_eq!( + error_lines(&stderr), + [ + "--verify-function G::g matches more than one function and no name matches only one of them, consider using wildcard G::g* to verify them all,", + "matched results are:", + "- ninth::G::g", + "- ninth::G::g", + ] + ); + let (output, stdout, stderr) = run_in(&["ninth", "first"], &["G::g*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +#[test] +fn verify_function_repeated_bad_pattern_reports_once() { + let (_, _, single_stderr) = run(&["delta"]); + let (output, _, stderr) = run(&["delta", "alpha", "delta"]); + assert!(!output.status.success()); + assert_eq!(stderr, single_stderr); +} From d0d3624cd3c40dbef81f9b339d4775fdb3fd979f Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Thu, 8 Oct 2026 08:30:21 +0000 Subject: [PATCH 6/7] --verify-function: one matcher for one module and several Every pattern goes through one rule. A pattern is matched against each function's name relative to its module, and, with `::`, also against its path from the crate root and its module's path followed by its relative name, each with or without `crate::`. Exact or wildcard matches come first, then a unique substring. Exact matches in one module are all selected; exact matches in several modules are ambiguous. - Methods of impls of one type in two modules can be told apart by module (`ta::S::f`). - The ambiguity hint names one function, or else the functions of one module, and no longer suggests a wildcard that selects more. - Listings with several modules show where same-named functions are defined. - Comments and tests describe the rule rather than main. - Function names are derived from the full name once, with each module's prefixes computed once. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 2 +- source/rust_verify/src/user_filter.rs | 187 +++++++++-------- .../rust_verify_test/tests/verify_function.rs | 189 +++++++++++++----- 3 files changed, 246 insertions(+), 132 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index a709cb07fd..af4058cc5c 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,7 +576,7 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root); \nwith several modules, or a pattern with :: that matches nothing within one module, \na pattern without * at its ends must match exactly one function", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root) \nand against its module's path followed by its name relative to the module (foo::S::f for a method of an impl of S in module foo); \na pattern without * at its ends that matches functions in more than one module is an error", "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index 9aa7800094..12815a4fee 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -2,11 +2,11 @@ use crate::buckets::{Bucket, BucketId}; use crate::config::Args; use crate::util::error; use crate::verifier::module_name; -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use std::sync::Arc; use vir::ast::{Fun, Function, Krate, VirErr}; use vir::ast_util::{ - friendly_fun_name_crate_relative, fun_as_friendly_rust_name, parse_path_segments_from_user_str, + fun_as_friendly_rust_name, parse_path_segments_from_user_str, path_as_friendly_rust_name, }; use vir::def::krate_to_string_ignore_stable_id; @@ -25,22 +25,27 @@ type ModuleId = vir::ast::Idents; /// A function in one of the selected modules, with the names a pattern can match it by struct FunName { fun: Fun, - /// The name relative to the function's module, as on main + /// The index of the function's module among the selected modules + module: usize, + /// The name relative to the function's module name: String, - /// The path from the crate root and the same path after `crate::`, - /// if the function's name starts with the crate's name - path: Option<(String, String)>, + /// The names that a pattern with `::` is also matched against: + /// the path from the crate root, if the function is named by a path in this crate, + /// and the module's path followed by the relative name (without the crate's name), + /// each with and without `crate::` + qualified: Vec, /// The name shown when several modules are selected listed: String, + /// Where the function is defined, shown to tell apart functions listed by the same name + location: String, } impl FunName { /// The names a pattern is matched against: the relative name, - /// and if `qualified`, also the path from the crate root, with and without `crate::` + /// and if `qualified`, also the qualified names fn names(&self, qualified: bool) -> impl Iterator { - let paths = self.path.as_ref().filter(|_| qualified); - std::iter::once(self.name.as_str()) - .chain(paths.into_iter().flat_map(|(p, c)| [p.as_str(), c.as_str()])) + let qualified = if qualified { &self.qualified[..] } else { &[] }; + std::iter::once(self.name.as_str()).chain(qualified.iter().map(|n| n.as_str())) } fn display(&self, several_modules: bool) -> &str { @@ -51,7 +56,7 @@ impl FunName { /// What a pattern selects, or why it selects nothing enum Resolution<'a> { Selected(Vec<&'a FunName>), - /// An exact pattern that matches several functions + /// An exact pattern that matches functions in several modules Ambiguous(Vec<&'a FunName>), /// An exact pattern that matches no function, but is a substring of several Substrings(Vec<&'a FunName>), @@ -123,7 +128,7 @@ impl UserFilter { let mut errors = Vec::new(); let mut seen = HashSet::new(); for pattern in args.verify_function.iter().filter(|p| seen.insert(p.as_str())) { - match Self::resolve(&funs, several_modules, pattern) { + match Self::resolve(&funs, pattern) { Resolution::Selected(m) => matches.extend(m.iter().map(|f| f.fun.clone())), failure => errors.push(Self::message(&funs, several_modules, pattern, failure)), } @@ -225,63 +230,63 @@ impl UserFilter { /// The functions owned by the modules, each with the names a pattern can match it by. fn fun_names(modules: &[ModuleId], funs: &Vec) -> Vec { + // For each module: the prefix of the names of the functions in it, the prefix of the + // names of the functions in the crate, and the module's path from the crate root + // (empty for the root, otherwise ending with `::`) + let mut prefixes: Vec> = vec![None; modules.len()]; funs.iter() .filter_map(|f| { let owning_module = f.x.owning_module.as_ref()?; let module = modules.iter().position(|m| m == &owning_module.segments)?; - let name = friendly_fun_name_crate_relative(owning_module, &f.x.name); - // The path from the crate root is the full name without the crate's name, - // even for a function named by a path outside its module - let krate = krate_to_string_ignore_stable_id(&owning_module.krate); + let (module_prefix, krate_prefix, module_path) = prefixes[module] + .get_or_insert_with(|| { + let krate = krate_to_string_ignore_stable_id(&owning_module.krate); + let path = module_name(owning_module); + let path = if path.is_empty() { path } else { path + "::" }; + (path_as_friendly_rust_name(owning_module) + "::", krate + "::", path) + }); let full = fun_as_friendly_rust_name(&f.x.name); - let path = full - .strip_prefix(&format!("{krate}::")) - .map(|p| (p.to_string(), format!("crate::{p}"))); - let listed = match &path { - Some((_, from_crate)) if modules[module].is_empty() => from_crate.clone(), - Some((p, _)) => p.clone(), - None => name.clone(), + // A function may be named by a path outside its module + // (e.g. a method of an impl of a type defined elsewhere); + // then its relative name is its full name + let name = full.strip_prefix(module_prefix.as_str()).unwrap_or(&full).to_string(); + let path = full.strip_prefix(krate_prefix.as_str()); + let owned = (!module_path.is_empty()).then(|| { + let rest = name.strip_prefix(krate_prefix.as_str()).unwrap_or(&name); + format!("{module_path}{rest}") + }); + let mut qualified: Vec = Vec::new(); + for n in path.into_iter().chain(owned.as_deref()) { + for n in [n.to_string(), format!("crate::{n}")] { + if !qualified.contains(&n) { + qualified.push(n); + } + } + } + let listed = match (path, &owned) { + (Some(p), _) if module_path.is_empty() => format!("crate::{p}"), + (Some(p), _) => p.to_string(), + (None, Some(owned)) => owned.clone(), + (None, None) => name.clone(), }; - Some(FunName { fun: f.x.name.clone(), name, path, listed }) + // A span prints as `file:line:col: line:col (#ctxt)` + let location = f.span.as_string.split(": ").next().unwrap_or("").to_string(); + Some(FunName { fun: f.x.name.clone(), module, name, qualified, listed, location }) }) .collect() } /// Resolve one pattern. /// - /// With one module, a pattern selects what it selects on main - /// (see `resolve_by`, matching the names relative to the module, where - /// an exact name may select several functions). - /// Otherwise (several modules, or a pattern with `::` that selects nothing on main), - /// the general rule applies: a pattern with `::` is also matched against each function's - /// path from the crate root, with or without `crate::`, - /// and a pattern without `*` at its ends must select exactly one function. - fn resolve<'a>(funs: &'a [FunName], several_modules: bool, pattern: &str) -> Resolution<'a> { + /// A pattern is matched against each function's name relative to its module, + /// and, if the pattern contains `::`, against its qualified names too. + /// A pattern with `*` at either end selects every function with a name that it matches. + /// A pattern without (an exact pattern) selects every function with a name equal to it, + /// as long as these functions are all in one module (otherwise it is ambiguous). + /// An exact pattern that equals no name selects the one function with a name that contains it, + /// and is an error if several do. + fn resolve<'a>(funs: &'a [FunName], pattern: &str) -> Resolution<'a> { let qualified = pattern.contains("::"); - if !several_modules { - let on_main = Self::resolve_by(funs, pattern, false, false); - if !qualified || matches!(on_main, Resolution::Selected(_)) { - return on_main; - } - } - Self::resolve_by(funs, pattern, qualified, true) - } - - /// The first part of this process is to - /// infer whether this is an "exact match" filter. - /// (If the user doesn't supply any * at the ends of the pattern, then it is usually - /// exact - however, if there is no exact match, but there is _exactly one_ - /// partial match, then we upgrade to a partial match) - /// - /// Each function is matched by its relative name, and if `qualified`, - /// by its path from the crate root too. - /// If `unique`, an exact pattern that matches several functions is ambiguous. - fn resolve_by<'a>( - funs: &'a [FunName], - pattern: &str, - qualified: bool, - unique: bool, - ) -> Resolution<'a> { let clean = pattern.trim_matches('*'); let exact = clean == pattern; @@ -293,7 +298,7 @@ impl UserFilter { .iter() .filter(|f| f.names(qualified).any(|n| Self::matches_strictly_by_pattern(pattern, n))) .collect(); - if matches.len() > 1 && exact && unique { + if exact && matches.iter().any(|f| f.module != matches[0].module) { return Resolution::Ambiguous(matches); } else if matches.len() > 0 { return Resolution::Selected(matches); @@ -322,37 +327,63 @@ impl UserFilter { pattern: &str, failure: Resolution, ) -> String { - let display_sorted = |funs: Vec<&FunName>| { - let mut names = - funs.iter().map(|f| f.display(several_modules).to_string()).collect::>(); - names.sort(); - names + // Sorted by name; with several modules, functions listed by the same name + // are told apart by location, in the order they are defined + let display_sorted = |mut funs: Vec<&FunName>| { + let mut counts: HashMap<&str, usize> = HashMap::new(); + for f in &funs { + *counts.entry(f.display(several_modules)).or_default() += 1; + } + funs.sort_by_key(|f| f.display(several_modules)); + funs.iter() + .map(|f| { + let name = f.display(several_modules); + if several_modules && counts[name] > 1 { + format!("{name} (at {})", f.location) + } else { + name.to_string() + } + }) + .collect::>() }; let clean = pattern.trim_matches('*'); match failure { Resolution::Selected(_) => unreachable!(), Resolution::Ambiguous(matches) => { - // Suggest a name that this resolution selects just one of the matches by - let selects = - |name: &str, f: &FunName| match Self::resolve(funs, several_modules, name) { - Resolution::Selected(m) => m.len() == 1 && m[0].fun == f.fun, - _ => false, - }; + // Suggest a name of one of the matches that selects just that function, + // or else one that selects just the matches in its module + let selected = |name: &str| match Self::resolve(funs, name) { + Resolution::Selected(m) => Some(m), + _ => None, + }; let mut sorted = matches.clone(); sorted.sort_by(|f, g| f.display(several_modules).cmp(g.display(several_modules))); - let example = sorted.iter().find_map(|f| { - let candidates = [ - Some(f.display(several_modules)), - f.path.as_ref().map(|(_, c)| c.as_str()), - ]; - candidates.into_iter().flatten().find(|name| selects(name, f)) + let candidates = || { + sorted.iter().flat_map(|f| { + std::iter::once(f.display(several_modules)) + .chain(f.qualified.iter().map(|n| n.as_str())) + .map(move |name| (*f, name)) + }) + }; + let one_function = candidates().find(|(f, name)| { + selected(name).is_some_and(|m| m.len() == 1 && m[0].fun == f.fun) + }); + let one_module = candidates().find(|(f, name)| { + selected(name).is_some_and(|m| { + let in_module = matches.iter().filter(|g| g.module == f.module); + m.len() == in_module.clone().count() + && in_module.zip(&m).all(|(g, h)| g.fun == h.fun) + }) }); - let header = match example { - Some(example) => format!( + let header = match (one_function, one_module) { + (Some((_, example)), _) => format!( "--verify-function {pattern} matches more than one function, use a name that matches only one (e.g. {example})," ), - None => format!( - "--verify-function {pattern} matches more than one function and no name matches only one of them, consider using wildcard {pattern}* to verify them all," + (None, Some((_, example))) => format!( + "--verify-function {pattern} matches functions in more than one module, use a name that matches the functions of only one module (e.g. {example})," + ), + (None, None) => format!( + "--verify-function {pattern} matches functions in more than one module, and no name matches the functions of only one module," ), }; Self::listing( diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index 41be00c10c..645d654499 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -13,6 +13,7 @@ proof fn alpha() { assert(1int + 1 == 2); } proof fn alpha_two() { assert(2int + 2 == 4); } proof fn beta() { assert(3int + 3 == 6); } proof fn gamma() { assert(false); } +pub struct S { t: T } } mod first { use vstd::prelude::*; @@ -99,6 +100,32 @@ mod ninth { impl G { proof fn g() { assert(18int == 18); } } } } +mod ta { + use vstd::prelude::*; + verus! { + impl crate::S { proof fn f() { assert(19int == 19); } } + } +} +mod tb { + use vstd::prelude::*; + verus! { + impl crate::S { proof fn f() { assert(20int == 20); } } + } +} +mod eleventh { + use vstd::prelude::*; + verus! { + impl crate::ninth::G { proof fn g() { assert(21int == 21); } } + impl crate::ninth::G { proof fn g() { assert(22int == 22); } } + } +} +mod twelfth { + use vstd::prelude::*; + verus! { + pub trait Tw { proof fn tw(); } + impl Tw for Seq { proof fn tw() { assert(23int == 23); } } + } +} "#; // `gamma` fails, so a run that verifies it reports an error. @@ -128,11 +155,23 @@ fn run_in(modules: &[&str], functions: &[&str]) -> (Output, String, String) { (output, stdout, stderr) } -// The lines of the error message, without rustc's indentation +// The lines of the error message, without rustc's indentation, +// and with `(at DIR/fixture.rs:...)` shortened to `(at fixture.rs:...)` fn error_lines(stderr: &str) -> Vec { let start = stderr.find("error: ").unwrap() + "error: ".len(); let end = stderr.find("\nerror: aborting").unwrap(); - stderr[start..end].trim_end().lines().map(|line| line.trim().to_string()).collect() + let shorten = |line: &str| match (line.find("(at "), line.find("fixture.rs:")) { + (Some(at), Some(file)) => format!("{}{}", &line[..at + "(at ".len()], &line[file..]), + _ => line.to_string(), + }; + stderr[start..end].trim_end().lines().map(|line| shorten(line.trim())).collect() +} + +// Where `text` starts in the fixture, as `fixture.rs:line:column` +fn location(text: &str) -> String { + let (line, col) = + CODE.lines().enumerate().find_map(|(i, l)| l.find(text).map(|c| (i + 1, c + 1))).unwrap(); + format!("fixture.rs:{line}:{col}") } fn results(n: usize) -> String { @@ -296,7 +335,7 @@ fn verify_function_ambiguity_across_modules_suggests_a_wildcard_that_works() { assert_eq!(stdout, results(2)); } -// On main, a module-qualified pattern with a single module is "could not find function". +// A pattern with `::` is matched against the paths from the crate root with one module, too. #[test] fn verify_function_qualified_with_one_module() { let (output, stdout, stderr) = run_in(&["first"], &["first::shared"]); @@ -351,19 +390,20 @@ fn verify_function_qualified_name_is_not_read_as_a_substring() { assert_eq!(stdout, results(1)); } -// With one module, a pattern that works on main selects what it selects on main: -// `a::f` is the unique substring match `Data::f`, which fails. -// The path from `crate` names `f` in module `a`. +// With one module too, `a::f` is the path of `f` in module `a`, an exact match, +// so it is not read as a substring of `Data::f` (which fails). #[test] -fn verify_function_qualified_with_one_module_as_on_main() { - let (output, stdout, stderr) = run_in(&["a"], &["a::f"]); +fn verify_function_qualified_name_is_not_read_as_a_substring_with_one_module() { + for pattern in ["a::f", "crate::a::f"] { + let (output, stdout, stderr) = run_in(&["a"], &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } + + let (output, stdout, stderr) = run_in(&["a"], &["a::Data::f"]); assert!(!output.status.success()); assert_eq!(stderr.matches("error: assertion failed").count(), 1, "{}", stderr); assert!(stdout.contains("0 verified, 1 errors"), "{}", stdout); - - let (output, stdout, stderr) = run_in(&["a"], &["crate::a::f"]); - assert!(output.status.success(), "{}", stderr); - assert_eq!(stdout, results(1)); } // `cell::f` names `f` in module `cell` and the methods `cell::f` in `fifth` and `sixth`. @@ -391,8 +431,8 @@ fn verify_function_qualified_and_unqualified_readings_are_ambiguous() { } // `moved` is owned by `first` but named by the path of `second::Item`, -// so it is listed by that path from the crate root, and matched by it with or without `crate::` -// (or by its full name, as on main). +// so it is listed by that path from the crate root, and matched by it with or without `crate::`, +// by its full name (its name relative to `first`), and by `first::` followed by that path. #[test] fn verify_function_names_a_function_by_its_path_from_the_crate_root() { let (output, _, stderr) = run_in(&["first", "second"], &["zzz"]); @@ -401,9 +441,12 @@ fn verify_function_names_a_function_by_its_path_from_the_crate_root() { assert!(lines.contains(&"- second::Item::moved".to_string()), "{}", stderr); assert!(!stderr.contains("first::fixture"), "{}", stderr); - for pattern in - ["crate::second::Item::moved", "second::Item::moved", "fixture::second::Item::moved"] - { + for pattern in [ + "crate::second::Item::moved", + "second::Item::moved", + "fixture::second::Item::moved", + "first::second::Item::moved", + ] { for modules in [&["first", "second"][..], &["first"][..]] { let (output, stdout, stderr) = run_in(modules, &[pattern]); assert!(output.status.success(), "{pattern}: {}", stderr); @@ -412,33 +455,20 @@ fn verify_function_names_a_function_by_its_path_from_the_crate_root() { } } -// Two functions of one module that match the same name are ambiguous too, -// unless a single module is selected and the pattern works on main. +// Functions of one module that match a pattern exactly are all selected: +// `line::f` is the path of `f` in module `line`, and the name of the method `f` of `line::line` #[test] -fn verify_function_ambiguity_within_one_module() { - // `line::f` is the path of `f` in module `line`, and the name of the method `f` of `line::line` - let (output, stdout, stderr) = run_in(&["line", "first"], &["line::f"]); - assert!(!output.status.success()); - assert!(!stdout.contains("verified"), "{}", stdout); - assert_eq!( - error_lines(&stderr), - [ - "--verify-function line::f matches more than one function, use a name that matches only one (e.g. crate::line::f),", - "matched results are:", - "- line::f", - "- line::line::f", - ] - ); - for pattern in ["crate::line::f", "line::line::f"] { - let (output, stdout, stderr) = run_in(&["line", "first"], &[pattern]); - assert!(output.status.success(), "{pattern}: {}", stderr); - assert_eq!(stdout, results(1), "{pattern}"); +fn verify_function_exact_matches_within_one_module() { + for modules in [&["line", "first"][..], &["line"][..]] { + let (output, stdout, stderr) = run_in(modules, &["line::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); + for pattern in ["crate::line::f", "line::line::f"] { + let (output, stdout, stderr) = run_in(modules, &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } } - - // As on main: with `line` alone, `line::f` is the method's name relative to the module - let (output, stdout, stderr) = run_in(&["line"], &["line::f"]); - assert!(output.status.success(), "{}", stderr); - assert_eq!(stdout, results(1)); } // The example in the hint is a name that the same rule resolves to one function: @@ -463,28 +493,81 @@ fn verify_function_hint_names_just_one_function() { assert_eq!(stderr.matches("note: verifying module eighth").count(), 0, "{}", stderr); } -// `G::g` and `G::g` are both named `G::g`: main verifies both with one module, -// and with several modules no name selects just one, so the hint is a wildcard. +// `G::g` and `G::g` are both named `G::g` in `ninth`, and both selected by it, +// however the module is written and whichever other modules are selected. #[test] fn verify_function_functions_with_the_same_name() { - let (output, stdout, stderr) = run_in(&["ninth"], &["G::g"]); - assert!(output.status.success(), "{}", stderr); - assert_eq!(stdout, results(2)); + for modules in [&["ninth"][..], &["ninth", "first"][..]] { + for pattern in ["G::g", "ninth::G::g", "crate::ninth::G::g"] { + let (output, stdout, stderr) = run_in(modules, &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(2), "{pattern}"); + } + } +} - let (output, _, stderr) = run_in(&["ninth", "first"], &["G::g"]); +// `ta` and `tb` each have a method `f` of `crate::S`, so `S::f` is ambiguous with both, +// and they are told apart by their modules. The listing shows where each is defined. +#[test] +fn verify_function_impls_of_one_type_in_two_modules() { + let (output, stdout, stderr) = run_in(&["ta", "tb"], &["S::f"]); assert!(!output.status.success()); + assert!(!stdout.contains("verified"), "{}", stdout); assert_eq!( error_lines(&stderr), [ - "--verify-function G::g matches more than one function and no name matches only one of them, consider using wildcard G::g* to verify them all,", - "matched results are:", - "- ninth::G::g", - "- ninth::G::g", + "--verify-function S::f matches more than one function, use a name that matches only one (e.g. ta::S::f),".to_string(), + "matched results are:".to_string(), + format!("- S::f (at {})", location("fn f() { assert(19int")), + format!("- S::f (at {})", location("fn f() { assert(20int")), ] ); - let (output, stdout, stderr) = run_in(&["ninth", "first"], &["G::g*"]); + for pattern in ["ta::S::f", "crate::ta::S::f"] { + let (output, stdout, stderr) = run_in(&["ta", "tb"], &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + assert_eq!(stderr.matches("note: verifying module tb").count(), 0, "{}", stderr); + } +} + +// `eleventh` has two methods `g` of `crate::ninth::G` too, so no name selects one function of +// `ninth::G::g`, and the hint names the functions of one module, which the same rule selects. +#[test] +fn verify_function_same_names_in_two_modules() { + let modules = ["ninth", "eleventh"]; + let (output, _, stderr) = run_in(&modules, &["ninth::G::g"]); + assert!(!output.status.success()); + let listed = ["17int", "18int", "21int", "22int"] + .map(|n| format!("- ninth::G::g (at {})", location(&format!("fn g() {{ assert({n}")))); + let mut expected = vec![ + "--verify-function ninth::G::g matches functions in more than one module, use a name that matches the functions of only one module (e.g. eleventh::ninth::G::g),".to_string(), + "matched results are:".to_string(), + ]; + expected.extend(listed); + assert_eq!(error_lines(&stderr), expected); + + let (output, stdout, stderr) = run_in(&modules, &["eleventh::ninth::G::g"]); assert!(output.status.success(), "{}", stderr); assert_eq!(stdout, results(2)); + assert_eq!(stderr.matches("note: verifying module ninth").count(), 0, "{}", stderr); +} + +// A method of an impl for a type of another crate has no path from the crate root, +// but its module's path followed by its full name names it. +#[test] +fn verify_function_method_of_a_type_of_another_crate() { + let (output, _, stderr) = run_in(&["twelfth", "first"], &["zzz"]); + assert!(!output.status.success()); + let lines = error_lines(&stderr); + assert!(lines.contains(&"- twelfth::vstd::seq::Seq::tw".to_string()), "{}", stderr); + + for modules in [&["twelfth", "first"][..], &["twelfth"][..]] { + for pattern in ["twelfth::vstd::seq::Seq::tw", "crate::twelfth::vstd::seq::Seq::tw"] { + let (output, stdout, stderr) = run_in(modules, &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } + } } #[test] From 59a2974c3709d551aa69a051e34737c304d3fc4f Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Thu, 8 Oct 2026 08:55:19 +0000 Subject: [PATCH 7/7] --verify-function: relative names before paths for exact patterns An exact pattern is matched against relative names first, then against the qualified names (path from the crate root, module path), then by unique substring. So `line::f` with module `line` selects the method `line::line::f`, as on main, rather than also `f` in `line`. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/config.rs | 2 +- source/rust_verify/src/user_filter.rs | 26 ++++++++++++++----- .../rust_verify_test/tests/verify_function.rs | 20 ++++++++------ 3 files changed, 32 insertions(+), 16 deletions(-) diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index af4058cc5c..22dc4decac 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -576,7 +576,7 @@ pub fn parse_args_with_imports( opts.optmulti( "", OPT_VERIFY_FUNCTION, - "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root) \nand against its module's path followed by its name relative to the module (foo::S::f for a method of an impl of S in module foo); \na pattern without * at its ends that matches functions in more than one module is an error", + "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root) \nand against its module's path followed by its name relative to the module (foo::S::f for a method of an impl of S in module foo); \na pattern without * at its ends is matched against names relative to the module first, then against these paths; \nif it matches functions in more than one module, it is an error", "PATTERN", ); opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]"); diff --git a/source/rust_verify/src/user_filter.rs b/source/rust_verify/src/user_filter.rs index 12815a4fee..6ad88b56b9 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -281,8 +281,9 @@ impl UserFilter { /// A pattern is matched against each function's name relative to its module, /// and, if the pattern contains `::`, against its qualified names too. /// A pattern with `*` at either end selects every function with a name that it matches. - /// A pattern without (an exact pattern) selects every function with a name equal to it, - /// as long as these functions are all in one module (otherwise it is ambiguous). + /// A pattern without (an exact pattern) selects the functions whose relative name equals it; + /// if there are none, the functions with a qualified name equal to it. + /// These must all be in one module (otherwise the pattern is ambiguous). /// An exact pattern that equals no name selects the one function with a name that contains it, /// and is an error if several do. fn resolve<'a>(funs: &'a [FunName], pattern: &str) -> Resolution<'a> { @@ -292,12 +293,23 @@ impl UserFilter { // First, get the matches without doing anything fancy: // If the user provides a * pattern, then we filter according to the * pattern; - // if the user provides an exact match (no *), then filter as an exact match. + // if the user provides an exact match (no *), then filter as an exact match, + // by relative name first and then by qualified name. // If we find anything this way, we're done. - let matches: Vec<&FunName> = funs - .iter() - .filter(|f| f.names(qualified).any(|n| Self::matches_strictly_by_pattern(pattern, n))) - .collect(); + let matches: Vec<&FunName> = if exact { + let by_name: Vec<&FunName> = funs.iter().filter(|f| f.name == pattern).collect(); + if by_name.is_empty() && qualified { + funs.iter().filter(|f| f.qualified.iter().any(|n| n == pattern)).collect() + } else { + by_name + } + } else { + funs.iter() + .filter(|f| { + f.names(qualified).any(|n| Self::matches_strictly_by_pattern(pattern, n)) + }) + .collect() + }; if exact && matches.iter().any(|f| f.module != matches[0].module) { return Resolution::Ambiguous(matches); } else if matches.len() > 0 { diff --git a/source/rust_verify_test/tests/verify_function.rs b/source/rust_verify_test/tests/verify_function.rs index 645d654499..0c0d9e7d53 100644 --- a/source/rust_verify_test/tests/verify_function.rs +++ b/source/rust_verify_test/tests/verify_function.rs @@ -406,18 +406,18 @@ fn verify_function_qualified_name_is_not_read_as_a_substring_with_one_module() { assert!(stdout.contains("0 verified, 1 errors"), "{}", stdout); } -// `cell::f` names `f` in module `cell` and the methods `cell::f` in `fifth` and `sixth`. +// `cell::f` is the relative name of the methods `f` of `cell` in `fifth` and `sixth`, +// which wins over the path of `f` in module `cell`, and is ambiguous. #[test] -fn verify_function_qualified_and_unqualified_readings_are_ambiguous() { +fn verify_function_relative_names_win_over_paths_and_are_ambiguous() { let (output, stdout, stderr) = run_in(&["cell", "fifth", "sixth"], &["cell::f"]); assert!(!output.status.success()); assert!(!stdout.contains("verified"), "{}", stdout); assert_eq!( error_lines(&stderr), [ - "--verify-function cell::f matches more than one function, use a name that matches only one (e.g. crate::cell::f),", + "--verify-function cell::f matches more than one function, use a name that matches only one (e.g. fifth::cell::f),", "matched results are:", - "- cell::f", "- fifth::cell::f", "- sixth::cell::f", ] @@ -455,12 +455,16 @@ fn verify_function_names_a_function_by_its_path_from_the_crate_root() { } } -// Functions of one module that match a pattern exactly are all selected: -// `line::f` is the path of `f` in module `line`, and the name of the method `f` of `line::line` +// `line::f` is the name of the method `f` of `line::line` relative to module `line`, +// and the path of `f` in module `line`: the relative name wins, with one module or several. #[test] -fn verify_function_exact_matches_within_one_module() { +fn verify_function_relative_name_wins_over_a_path() { for modules in [&["line", "first"][..], &["line"][..]] { - let (output, stdout, stderr) = run_in(modules, &["line::f"]); + // The method is the one function selected by both patterns + let (output, stdout, stderr) = run_in(modules, &["line::f", "line::line::f"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(1)); + let (output, stdout, stderr) = run_in(modules, &["line::f", "crate::line::f"]); assert!(output.status.success(), "{}", stderr); assert_eq!(stdout, results(2)); for pattern in ["crate::line::f", "line::line::f"] {