Filter option (#5008)

Fixes #4816 

### Description
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 something if it ranges
over line 5 in the file `source1.dfy`.

### How has this been tested?
Add a littish test `filter.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/DafnyDriver/CliCompilation.cs

@@ -1,18 +1,22 @@
+#nullable enable
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
+using System.Text.RegularExpressions;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.FileSystemGlobbing;
 using Microsoft.Extensions.Logging;
 using VC;
 using IToken = Microsoft.Dafny.IToken;
+using Token = Microsoft.Dafny.Token;
 
 namespace DafnyDriver.Commands;
 
@@ -189,6 +193,8 @@ public async Task VerifyAllAndPrintSummary() {
       var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList();
 
       if (canVerifies != null) {
+        canVerifies = FilterCanVerifies(canVerifies);
+
         var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
         foreach (var canVerify in orderedCanVerifies) {
           canVerifyResults[canVerify] = new CliCanVerifyResults();
@@ -228,4 +234,28 @@ public async Task VerifyAllAndPrintSummary() {
       // Failed to resolve the program due to a user error.
     }
   }
+
+  private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies) {
+    var filterPosition = options.Get(VerifyCommand.FilterPosition);
+    if (filterPosition == null) {
+      return canVerifies;
+    }
+
+    var regex = new Regex(@"(.+)(?::(\d+))?", RegexOptions.RightToLeft);
+    var result = regex.Match(filterPosition);
+    if (result.Length != filterPosition.Length || !result.Success) {
+      Compilation.Reporter.Error(MessageSource.Project, Token.Cli, "Could not parse value passed to --filter-position");
+      return new List<ICanVerify>();
+    }
+    var filePart = result.Groups[1].Value;
+    string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null;
+    var fileFiltered = canVerifies.Where(c => c.Tok.Uri.ToString().EndsWith(filePart)).ToList();
+    if (string.IsNullOrEmpty(linePart)) {
+      return fileFiltered;
+    }
+
+    var line = int.Parse(linePart);
+    return fileFiltered.Where(c =>
+        c.RangeToken.StartToken.line <= line && line <= c.RangeToken.EndToken.line).ToList();
+  }
 }

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -3,13 +3,21 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore;
 using DafnyDriver.Commands;
 using JetBrains.Annotations;
 
 namespace Microsoft.Dafny;
 
 public static class VerifyCommand {
 
+  static VerifyCommand() {
+    DooFile.RegisterNoChecksNeeded(FilterPosition);
+  }
+
+  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""");
+
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
     result.AddArgument(DafnyCommands.FilesArgument);
@@ -36,6 +44,7 @@ public static Command Create() {
 
   private static IReadOnlyList<Option> Options =>
     new Option[] {
+        FilterPosition,
         BoogieOptionBag.BoogieFilter,
       }.Concat(DafnyCommands.VerificationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source1.dfy

@@ -0,0 +1,7 @@
+method Succeeds()
+  ensures true {
+}
+
+method Fails() 
+  ensures false {
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/src/source2.dfy

@@ -0,0 +1,7 @@
+method Succeeds2()
+  ensures true {
+}
+
+method Fails2() 
+  ensures false {
+}

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

@@ -0,0 +1,11 @@
+// RUN: %verify --boogie-filter='*Succeeds*' --bprint:"%t.bpl" %s > %t
+// RUN: ! %verify %s >> %t
+// RUN: %diff "%s.expect" "%t"
+
+method Succeeds()
+  ensures true {
+}
+
+method Fails() 
+  ensures false {
+}

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

@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+boogie-filter.dfy(10,16): Error: a postcondition could not be proved on this return path
+boogie-filter.dfy(10,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 1 verified, 1 error

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

@@ -1,5 +1,9 @@
-// RUN: %verify --boogie-filter='*Succeeds*' --bprint:"%t.bpl" %s > %t
-// RUN: ! %verify %s >> %t
+// RUN: %verify --filter-position='blaergaerga' %s > %t
+// RUN: %verify --filter-position='C:\windows\path.dfy' %s >> %t
+// RUN: ! %verify --filter-position='filter.dfy' %s >> %t
+// RUN: ! %verify --filter-position='filter.dfy:14' %s >> %t
+// RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Inputs/dfyconfig.toml >> %t
+// RUN: %verify --filter-position='src/source1.dfy:2' %S/Inputs/dfyconfig.toml >> %t
 // RUN: %diff "%s.expect" "%t"
 
 method Succeeds()

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

@@ -1,6 +1,18 @@
 
-Dafny program verifier finished with 1 verified, 0 errors
-filter.dfy(10,16): Error: a postcondition could not be proved on this return path
-filter.dfy(10,10): Related location: this is the postcondition that could not be proved
+Dafny program verifier finished with 0 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+filter.dfy(14,16): Error: a postcondition could not be proved on this return path
+filter.dfy(14,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
+filter.dfy(14,16): Error: a postcondition could not be proved on this return path
+filter.dfy(14,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+source1.dfy(6,16): Error: a postcondition could not be proved on this return path
+source1.dfy(6,10): Related location: this is the postcondition that could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/4816.feat

@@ -0,0 +1 @@
+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`.