Add --filter-symbol option (#5071)

### Description
- Add an option `--filter-symbol` to the `dafny verify` command, that
filters what gets verified by selecting symbols whose fully qualified
contains the given argument. For example, `dafny verify dfyconfig.toml
--filter-symbol=MyModule` will verify everything inside `MyModule`.
- Deprecate the option `--boogie-filter` by hiding it and updating its
help to say it's deprecated.

### How has this been tested?
Added a littish test `filter-symbol.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/IHasUsages.cs

@@ -24,6 +24,8 @@ public interface ICanVerify : ISymbol {
   /// If true is incorrectly returned, the IDE will allow the user to verify this but it'll pass immediately.
   /// </summary>
   bool ShouldVerify { get; }
+
+  string FullDafnyName { get; }
 }
 
 public static class AstExtensions {

Source/DafnyCore/AST/Members/Function.cs

@@ -9,7 +9,8 @@
 
 namespace Microsoft.Dafny;
 
-public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat, IHasDocstring, ISymbol, ICanAutoRevealDependencies, ICanVerify {
+public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat, IHasDocstring,
+  ICanAutoRevealDependencies, ICanVerify {
   public override string WhatKind => "function";
 
   public string GetFunctionDeclarationKeywords(DafnyOptions options) {

Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs

@@ -58,4 +58,5 @@ public string GetDescription(DafnyOptions options) {
 
   public ModuleDefinition ContainingModule => EnclosingDatatype.EnclosingModuleDefinition;
   public bool ShouldVerify => Formals.Any(f => f.DefaultValue != null);
+  public string FullDafnyName => FullName;
 }

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -11,9 +11,10 @@ namespace Microsoft.Dafny;
 
 public static class BoogieOptionBag {
   public static readonly Option<IEnumerable<string>> BoogieFilter = new("--boogie-filter", @"
-(experimental) Only check proofs whose Boogie name is matched by pattern <p>. This option may be specified multiple times to match multiple patterns. The pattern <p> may contain * wildcards which match any character zero or more times. If you are unsure of how Boogie names are generated, please pre- and postfix your pattern with a wildcard to enable matching on Dafny proof names."
+(obsolete, use --filter-symbol instead) Only check proofs whose Boogie name is matched by pattern <p>. This option may be specified multiple times to match multiple patterns. The pattern <p> may contain * wildcards which match any character zero or more times. If you are unsure of how Boogie names are generated, please pre- and postfix your pattern with a wildcard to enable matching on Dafny proof names."
     .TrimStart()) {
     ArgumentHelpName = "pattern",
+    IsHidden = true,
   };
 
   public static readonly Option<IEnumerable<string>> BoogieArguments = new("--boogie",

Source/DafnyDriver/CliCompilation.cs

@@ -258,11 +258,12 @@ public async Task VerifyAllAndPrintSummary() {
     }
   }
 
-  private bool KeepVerificationTask(IVerificationTask task, int line) {
-    return task.ScopeToken.line == line || task.Token.line == line;
-  }
-
   private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
+    var symbolFilter = options.Get(VerifyCommand.FilterSymbol);
+    if (symbolFilter != null) {
+      canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.Contains(symbolFilter)).ToList();
+    }
+
     var filterPosition = options.Get(VerifyCommand.FilterPosition);
     if (filterPosition == null) {
       line = null;
@@ -290,6 +291,10 @@ private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int
         c.RangeToken.StartToken.line <= parsedLine && parsedLine <= c.RangeToken.EndToken.line).ToList();
   }
 
+  private bool KeepVerificationTask(IVerificationTask task, int line) {
+    return task.ScopeToken.line == line || task.Token.line == line;
+  }
+
   static void WriteTrailer(DafnyOptions options, TextWriter output, bool reportAssertions, VerificationStatistics statistics) {
     if (options.Verbosity <= CoreOptions.VerbosityLevel.Quiet) {
       return;

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -12,11 +12,15 @@ namespace Microsoft.Dafny;
 public static class VerifyCommand {
 
   static VerifyCommand() {
+    DooFile.RegisterNoChecksNeeded(FilterSymbol);
     DooFile.RegisterNoChecksNeeded(FilterPosition);
   }
 
+  public static readonly Option<string> FilterSymbol = new("--filter-symbol",
+    @"Filter what gets verified by selecting only symbols whose fully qualified name contains the given argument. For example: ""--filter-symbol=MyNestedModule.MyFooFunction""");
+
   public static readonly Option<string> FilterPosition = new("--filter-position",
-    @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example: ""--filter=lastFolder/source.dfy:23""");
+    @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example: ""--filter-position=lastFolder/source.dfy:23""");
 
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
@@ -44,6 +48,7 @@ public static Command Create() {
 
   private static IReadOnlyList<Option> Options =>
     new Option[] {
+        FilterSymbol,
         FilterPosition,
         BoogieOptionBag.BoogieFilter,
       }.Concat(DafnyCommands.VerificationOptions).

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy

@@ -0,0 +1,27 @@
+// RUN: %verify --filter-symbol='blaergaerga' %s > %t
+// RUN: ! %verify --filter-symbol='P' %s >> %t
+// RUN: ! %verify --filter-symbol='Q' %s >> %t
+// RUN: ! %verify --filter-symbol='P.Q' %s >> %t
+// RUN: ! %verify --filter-symbol='Q.P' %s >> %t
+// RUN: ! %verify --filter-symbol='DT' %s >> %t
+// RUN: ! %verify --filter-symbol='R1' %s >> %t
+// RUN: %diff "%s.expect" "%t"
+
+module P {
+  module Q {
+    method A() ensures false {}
+  }
+  method B() ensures false {}
+}
+
+module Q {
+  module P {
+    method C() ensures false {}
+  }
+  method D() ensures false {}
+}
+
+method E() ensures false {}
+
+datatype DT = R1(x: nat := -1) | R2(y: nat := -1)
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect

@@ -0,0 +1,33 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(14,27): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(14,21): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 3 errors
+filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(21,27): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(21,21): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 3 errors
+filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+filter-symbol.dfy(26,27): Error: value does not satisfy the subset constraints of 'nat'
+filter-symbol.dfy(26,46): Error: value does not satisfy the subset constraints of 'nat'
+
+Dafny program verifier finished with 0 verified, 2 errors
+filter-symbol.dfy(26,27): Error: value does not satisfy the subset constraints of 'nat'
+
+Dafny program verifier finished with 0 verified, 1 error

docs/dev/news/4816.feat

@@ -1 +1,2 @@
-Add an option `--filter-position` to the `dafny verify` command, that allows verifying a single function or method, based on a file path and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify thing that ranges over line 5 in the file `source1.dfy`.
+- Add an option `--filter-position` to the `dafny verify` command, that allows verifying a single function or method, based on a file path and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify thing that ranges over line 5 in the file `source1.dfy`.
+- Add an option `--filter-symbol` to the `dafny verify` command, that only verifies symbols whose fully qualified contains the given argument. For example, `dafny verify dfyconfig.toml --filter-symbol=MyModule` will verify everything inside `MyModule`.