Allow --verify-function more than once

[kiranandcode]

--verify-function can now be given more than once, and used with several modules.

Semantics

• Each pattern selects functions: exact name, unique substring, or * wildcards at the ends. The run verifies the union of the selections, and each function is checked once.
• Every pattern is resolved before the run fails. The messages for all bad patterns go into one error, separated by a blank line. A repeated pattern is resolved and reported once. With one bad pattern the output is byte-identical to a single flag.
• --verify-function still needs --verify-only-module or --verify-root, and still rejects --verify-module. --verify-only-module can be repeated, and --verify-root can be added alongside. A repeated module counts once.

One rule

Every pattern goes through one matcher, whether one module or several are selected.

• Names: every pattern is matched against each function's name relative to its module (as before). A pattern with :: is also matched against:

  • the function's path from the crate root, with or without crate:: (first::shared, crate::first::shared, crate::beta for the root);
  • its module's path followed by its relative name (with the crate's name dropped), with or without crate::. For impl crate::S<u8> { fn f } written in module ta, that is ta::S::f. So methods of impls of one type in two modules can be told apart.

• Wildcards: a pattern with * at either end selects every function with a name it matches, by any of these names.

• Exact patterns (no * at either end) go through one precedence step, the same with one module or several:

  1. an exact match on the relative name;
  2. if none, an exact match on a qualified name (the crate-root or module-path readings);
  3. if none, the substring fallback: a unique substring match is selected, and several are an error.

  All matches at the first step that finds any are selected if they are in one module (e.g. G::g selects both G<u8>::g and G<u16>::g, and so does ninth::G::g). Matches in more than one module are an ambiguity error. So line::f with module line is the method f of line::line (its relative name), as on main, and not also f in module line (its path). crate::line::f and line::line::f each select one.

• Hints follow the same rule:

  • The ambiguity hint names one matched function by a name that the resolver selects only that function by (the listed name, then the qualified names, in order).
  • If no name selects only one function, the hint names the functions of one module: e.g. eleventh::ninth::G::g when ninth and eleventh each have two methods ninth::G::g.
  • The old fallback {pattern}* is gone, since it also selected other functions starting with the pattern. If no name selects even one module's matches, the error says so and gives no hint.
  • The "more than one match" hint *pat* and the "could not find" hint *clean* match by the same names, so they select exactly the functions listed.

• Listings with several modules show each function's path from the crate root (crate:: plus the name for the root). When several listed functions share a name, each gets its location: - S::f (at src/lib.rs:98:31). With one module, listings are unchanged.

Methods of impls for a type of another crate (e.g. impl Tw for Seq<int> in module twelfth) have no path from the crate root, because their name is the other crate's path (vstd::seq::Seq::tw). They can still be qualified: by the module's path followed by that name, twelfth::vstd::seq::Seq::tw (or crate::twelfth::vstd::seq::Seq::tw). That spelling is not a real Rust path, but it is unique to the module.

Compared with main

Patterns without ::, with one module: byte-identical to main, since they match only the relative name, and with one module there is no ambiguity error and no location in listings.

Patterns with :: that work on main and change, from the comparison below (20 of 318 working inputs). Exact patterns that main matches exactly by relative name are unchanged.:

• An exact pattern that main resolved as an accidental unique substring:
  • a::f in module a: main selects Data::f (its name contains a::f); now selects f, whose path is a::f.
  • :: in first, a and line, and ::f in a and line: main selects the one relative name containing :: (e.g. Data::f). Every path contains ::, so these are now "more than one match" errors.
• A wildcard pattern that now also matches paths, so it selects more: *a::f, *a::f*, *a::*, *a::**, *::f, *::f* in a; *::* in first, a and line; *::f, *::f*, *line::f, line::f*, *line::f* in line.

Changes

• config.rs: help text for PATTERN. The "at most one --verify-only-module or --verify-root" check is gone.
• user_filter.rs:
  • UserFilter::Function(Vec<ModuleId>, HashSet<Fun>).
  • Each selected function is named once. FunName holds the module, the relative name, the qualified names, the listed name and the location. The relative name and the path are cut from the function's full name. Each module's prefixes are computed once, so the friendly-name map's lock is taken once per function (plus once per module).
  • resolve is the single rule. It returns a Resolution, and message words the error.
• driver.rs: is_verifying_entire_crate checks is_empty().
• Not changed: is_verifying_entire_crate ignores --verify-only-module (already so on main), so a run with only --verify-only-module prints no "(partial verification …)" note.

Testing

rust_verify_test/tests/verify_function.rs has 29 tests, all passing. They run through common::run_verus_raw and compare error messages line by line. They cover:

• union, overlap, failing functions, every bad pattern reported, a repeated bad pattern reported once;
• two modules, root plus a module, wildcards across modules, *shar* hints that work;
• qualified patterns with one module (first::shared, first::only_*, crate::beta, crate::alph hinting *crate::alph*, which verifies 2);
• a::f selects f with a alone and with a and first, and so does crate::a::f; a::Data::f selects Data::f;
• cell::f across cell, fifth and sixth is the relative name of the methods in fifth and sixth, so it is ambiguous between those two and hints fifth::cell::f; crate::cell::f selects f in cell;
• line::f selects only the method line::line::f (its relative name wins over the path of f), with line alone and with line and first; crate::line::f and line::line::f each select one;
• with first, second and eighth (struct first with method shared), shared hints crate::first::shared, not first::shared;
• G::g, ninth::G::g and crate::ninth::G::g each verify both methods, with ninth alone and with ninth and first;
• methods of crate::S in ta and tb: S::f is ambiguous, hints ta::S::f, and lists both with their locations; ta::S::f and crate::ta::S::f select one;
• ninth::G::g with ninth and eleventh (two methods each): the hint names one module's functions (eleventh::ninth::G::g), which verifies 2;
• twelfth::vstd::seq::Seq::tw names a method of an impl for vstd's Seq;
• moved (in first, of second::Item) is listed as second::Item::moved and matched by crate::second::Item::moved, second::Item::moved, its full name and first::second::Item::moved, with one or two modules.

Also:

• Other suites: module_order (1), report_json (11) and resident (70) pass with VERUS_CVC5_PATH set to an absolute path. vargo fmt -- --check is clean. I did not run the full rust_verify_test suite.
• Comparison with main: a release binary built from origin/main (3fa79fdb) against this branch, on 4720 single-module, single-pattern invocations of the test fixture: 16 module selections × 295 patterns (exact, substring, ambiguous, no-match, each with * at either or both ends, module- and crate::-qualified, type-qualified, interior *, ::, *). Compared stdout, stderr and the exit code.
  • 318 inputs work on main: 298 are byte-identical, and the 20 that differ are the :: patterns listed above.
  • Of the inputs that fail on main, 266 now give different output, and every one of them contains ::.

Earlier real check (first commit, one module)

On verified-nrkernel impl_u::os_refinement (pristine), with the os-bench flags (-V cvc5 --rlimit 10 --num-threads 4 --multiple-errors 50):

run	result	wall
step_MapEnd_refines	0 verified, 1 error	28 s
lemma_map_soundness_equality	0 verified, 1 error	33 s
both, one process	0 verified, 2 errors, same two error locations	59 s
lemma_protect_soundness_equality	1 verified, 0 errors	9 s
step_MapEnd_refines + lemma_protect_soundness_equality	1 verified, 1 error	39 s
main binary, both flags	Option 'verify-function' given more than once, exit 255	—

The saving per extra function is one front end. The box was shared, so the timings are only indicative. I have not re-run nrkernel with several modules.

Why: the os-bench verus wrapper re-runs fork verus on the changed functions that fail, for --expand-errors. With this change it can do that in one process, even when the functions are in different modules, and it can always pass qualified names.

🤖 Generated with Claude Code