diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 47daa3c58f..22dc4decac 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,11 +573,11 @@ 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*)", - "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; \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]"); opts.optflag("", OPT_NO_VERIFY, "Do not run verification"); @@ -835,14 +835,8 @@ 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_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..6ad88b56b9 100644 --- a/source/rust_verify/src/user_filter.rs +++ b/source/rust_verify/src/user_filter.rs @@ -2,10 +2,13 @@ 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, parse_path_segments_from_user_str}; +use vir::ast_util::{ + 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 { @@ -13,12 +16,55 @@ pub enum UserFilter { None, /// Verify modules Modules(Vec), - /// Verify function - Function(ModuleId, String, HashSet), + /// Verify the functions matched by any of the patterns, within these modules + Function(Vec, HashSet), } 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 index of the function's module among the selected modules + module: usize, + /// The name relative to the function's module + name: 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 qualified names + fn names(&self, qualified: bool) -> impl Iterator { + 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 { + if several_modules { &self.listed } else { &self.name } + } +} + +/// What a pattern selects, or why it selects nothing +enum Resolution<'a> { + Selected(Vec<&'a FunName>), + /// 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>), + /// 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 { Arc::new(vec![]) } @@ -58,19 +104,39 @@ 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()); - let module = if args.verify_root { - root_module_id() - } else { - 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 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 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(); + let mut seen = HashSet::new(); + for pattern in args.verify_function.iter().filter(|p| seen.insert(p.as_str())) { + 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)), + } + } + if !errors.is_empty() { + return Err(error(errors.join("\n\n"))); + } + return Ok(UserFilter::Function(modules, matches)); } if args.verify_module.is_empty() && args.verify_only_module.is_empty() && !args.verify_root @@ -121,7 +187,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 @@ -162,143 +228,241 @@ 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() - .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) + /// 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 (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); + // 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(), + }; + // 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(); + .collect() + } + + /// Resolve one pattern. + /// + /// 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 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> { + let qualified = pattern.contains("::"); + 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; - // 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 = Self::get_matches_strictly_by_pattern(function_pattern, &module_fun_names); - if matches.len() > 0 { - return Ok(matches.into_iter().map(|(f, _)| f.clone()).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 { + 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. - let substring_matches = - Self::get_all_substring_matches(function_pattern, &module_fun_names); - - let clean = function_pattern.trim_matches('*'); - if clean == function_pattern { + // `*{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.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," + (true, 1) => Resolution::Selected(substring_matches), + (true, _) => Resolution::Substrings(substring_matches), + (false, _) => Resolution::Similar(substring_matches), + } + } + + /// The error message for a pattern that selects nothing + fn message( + funs: &[FunName], + several_modules: bool, + pattern: &str, + failure: Resolution, + ) -> String { + // 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 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 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 (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})," ), - format!( - "or specify a unique substring for the desired function, matched results are:" + (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})," ), - ].into_iter() - .chain(filtered_functions.iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(error(msg)); + (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( + vec![header, format!("matched results are:")], + display_sorted(matches), + ) } - } 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![ + Resolution::Substrings(matches) => Self::listing( + vec![ format!( - "could not find function {function_pattern} specified by --verify-function," + "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:"), - ] - .into_iter() - .chain(filtered_functions.iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(error(msg)); - } + ], + 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()), + ), } + } - // 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!("available functions are:"), - ] - .into_iter() - .chain(all_functions.iter().map(|f| format!(" - {f}"))) - .collect::>() - .join("\n"); - return Err(error(msg)); + /// 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: &String, - funs: &'a Vec<(Fun, String)>, - ) -> Vec<&'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 - } - }) - .collect() - } - - fn get_all_substring_matches<'a>( - function_pattern: &String, - funs: &'a Vec<(Fun, String)>, - ) -> Vec<&'a (Fun, String)> { - let clean = function_pattern.trim_matches('*'); - funs.iter().filter(|(_, name)| name.contains(clean)).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. /// 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 new file mode 100644 index 0000000000..0c0d9e7d53 --- /dev/null +++ b/source/rust_verify_test/tests/verify_function.rs @@ -0,0 +1,583 @@ +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +use std::fs; +use std::process::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); } +pub struct S { t: T } +} +mod first { + use vstd::prelude::*; + 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); } + } +} +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); } } + } +} +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); } } + } +} +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); } } + } +} +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. +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 mut args = vec!["--crate-type=lib", "-V", "no-solver-version-check"]; + for m in modules { + if *m != "--verify-root" { + args.push("--verify-only-module"); + } + args.push(*m); + } + for f in functions { + args.extend(["--verify-function", *f]); + } + 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) +} + +// 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(); + 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 { + 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); +} + +#[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, + // separated by a blank line + let mut expected = error_lines(&delta_stderr); + expected.push(String::new()); + expected.extend(error_lines(&zeta_stderr)); + assert_eq!(error_lines(&stderr), expected); + 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_eq!( + error_lines(&stderr), + [ + "--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", + ] + ); +} + +#[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)); +} + +#[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)); +} + +// 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"]); + 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 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); + let (output, stdout, stderr) = run(&["*crate::alph*"]); + assert!(output.status.success(), "{}", stderr); + assert_eq!(stdout, results(2)); +} + +#[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); +} + +// 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 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_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); +} + +// `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_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. fifth::cell::f),", + "matched results are:", + "- 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`, +// 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"]); + assert!(!output.status.success()); + let lines = error_lines(&stderr); + 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", + "first::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}"); + } + } +} + +// `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_relative_name_wins_over_a_path() { + for modules in [&["line", "first"][..], &["line"][..]] { + // 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"] { + let (output, stdout, stderr) = run_in(modules, &[pattern]); + assert!(output.status.success(), "{pattern}: {}", stderr); + assert_eq!(stdout, results(1), "{pattern}"); + } + } +} + +// 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` 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() { + 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}"); + } + } +} + +// `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 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")), + ] + ); + 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] +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); +}