Enable filtering on a range of assertions (#6077)

### What was changed?
Besides `--filter-position :<line>`, also support `--filter-position
:<start>-<end>`, `--filter-position :<start>-` and `--filter-position
:-<end>`

### How has this been tested?
Extended existing test

<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>

---------

Co-authored-by: Mikaël Mayer <[email protected]>

Source/DafnyDriver/CliCompilation.cs

@@ -242,8 +242,8 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) {
 
     DidVerification = true;
 
-    canVerifies = FilterCanVerifies(canVerifies, out var line);
-    VerifiedAssertions = line != null;
+    canVerifies = FilterCanVerifies(canVerifies, out var filterRange);
+    VerifiedAssertions = filterRange.Filters;
 
     int done = 0;
 
@@ -254,8 +254,8 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) {
       foreach (var canVerify in canVerifiesForModule.OrderBy(v => v.Origin.pos)) {
         var results = new CliCanVerifyState();
         canVerifyResults[canVerify] = results;
-        if (line != null) {
-          results.TaskFilter = t => KeepVerificationTask(t, line.Value);
+        if (VerifiedAssertions) {
+          results.TaskFilter = t => KeepVerificationTask(t, filterRange);
         }
 
         var shouldVerify = await Compilation.VerifyLocation(canVerify.Origin.GetFilePosition(), results.TaskFilter, randomSeed);
@@ -312,8 +312,20 @@ public static string DescribeOutcome(VcOutcome outcome) {
     };
   }
 
-  private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
+  class LineRange(int start, int end) {
+    public int Start { get; } = start;
+    public int End { get; } = end;
+
+    public bool Contains(int value) {
+      return Start <= value && value <= End;
+    }
+    public bool Filters => Start != int.MinValue || End != int.MaxValue;
+  }
+
+  private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out LineRange range) {
     var symbolFilter = Options.Get(VerifyCommand.FilterSymbol);
+    int start = int.MinValue;
+    int end = int.MaxValue;
     if (symbolFilter != null) {
       if (symbolFilter.EndsWith(".")) {
         var withoutDot = new string(symbolFilter.SkipLast(1).ToArray());
@@ -325,33 +337,44 @@ private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int
 
     var filterPosition = Options.Get(VerifyCommand.FilterPosition);
     if (filterPosition == null) {
-      line = null;
+      range = new LineRange(start, end);
       return canVerifies;
     }
 
-    var regex = new Regex(@"(.*)(?::(\d+))?", RegexOptions.RightToLeft);
+    var regex = new Regex(@"(.*)(?::(\d*)(-?)(\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");
-      line = null;
+      range = new LineRange(start, end);
       return new List<ICanVerify>();
     }
     var filePart = result.Groups[1].Value;
-    string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null;
+    string? lineStart = result.Groups[2].Value;
+    bool hasRange = result.Groups[3].Value == "-";
+    string lineEnd = result.Groups[4].Value;
     var fileFiltered = canVerifies.Where(c => c.Origin.Uri.ToString().EndsWith(filePart)).ToList();
-    if (string.IsNullOrEmpty(linePart)) {
-      line = null;
+    if (string.IsNullOrEmpty(lineStart) && string.IsNullOrEmpty(lineEnd)) {
+      range = new LineRange(start, end);
       return fileFiltered;
     }
 
-    var parsedLine = int.Parse(linePart);
-    line = parsedLine;
+    if (!string.IsNullOrEmpty(lineEnd)) {
+      end = int.Parse(lineEnd);
+      if (!hasRange) {
+        start = end;
+      }
+    }
+    if (!string.IsNullOrEmpty(lineStart)) {
+      start = int.Parse(lineStart);
+    }
+
+    range = new LineRange(start, end);
     return fileFiltered.Where(c =>
-        c.Origin.StartToken.line <= parsedLine && parsedLine <= c.Origin.EndToken.line).ToList();
+        c.Origin.StartToken.line <= end && start <= c.Origin.EndToken.line).ToList();
   }
 
-  private bool KeepVerificationTask(IVerificationTask task, int line) {
-    return task.ScopeToken.line == line || task.Token.line == line;
+  private bool KeepVerificationTask(IVerificationTask task, LineRange range) {
+    return range.Contains(task.ScopeToken.line) || range.Contains(task.Token.line);
   }
 }
 

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -33,7 +33,7 @@ static VerifyCommand() {
     @"Filter what gets verified by selecting only symbols whose fully qualified name contains the given argument, for example: ""--filter-symbol=MyNestedModule.MyFooFunction"". Place a dot at the end of the argument to indicate the symbol name must end like this, which can be useful if one symbol name is a prefix of another.");
 
   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, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=: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 or line range. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5-7` will only verify things that between (and including) line 5 and 7 in the file `source1.dfy`. You can also use `:5`, `:5-`, `:-5` to specify individual lines or open ranges. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");
 
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");

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

@@ -5,11 +5,15 @@
 // RUN: %verify --filter-position='e.dfy:2' %S/Inputs/single-file.dfy >> %t
 // RUN: %verify --filter-position='blaergaerga' %S/Inputs/single-file.dfy >> %t
 // RUN: ! %verify --isolate-assertions --filter-position='e.dfy:5' %S/Inputs/single-file.dfy >> %t
+// RUN: ! %verify --isolate-assertions --filter-position='e.dfy:-5' %S/Inputs/single-file.dfy >> %t
 // RUN: %verify --isolate-assertions --filter-position='e.dfy:6' %S/Inputs/single-file.dfy >> %t
 // RUN: %verify --isolate-assertions --filter-position='e.dfy:7' %S/Inputs/single-file.dfy >> %t
 // RUN: ! %verify --isolate-assertions --filter-position='e.dfy:8' %S/Inputs/single-file.dfy >> %t
+// RUN: ! %verify --isolate-assertions --filter-position='e.dfy:8-9' %S/Inputs/single-file.dfy >> %t
 // RUN: %verify --isolate-assertions --filter-position='e.dfy:9' %S/Inputs/single-file.dfy >> %t
+// RUN: %verify --isolate-assertions --filter-position='e.dfy:9-11' %S/Inputs/single-file.dfy >> %t
 // RUN: ! %verify --isolate-assertions --filter-position='e.dfy:16' %S/Inputs/single-file.dfy >> %t
 // RUN: %verify --isolate-assertions --filter-position='y:20' %S/Inputs/single-file.dfy >> %t
 // RUN: ! %verify --isolate-assertions --filter-position=':24' %S/Inputs/single-file.dfy >> %t
+// RUN: ! %verify --isolate-assertions --filter-position=':24-' %S/Inputs/single-file.dfy >> %t
 // RUN: %diff "%s.expect" "%t"

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

@@ -19,13 +19,21 @@ Dafny program verifier finished with 0 verified, 0 errors
 single-file.dfy(8,4): Error: assertion might not hold
 
 Dafny program verifier finished with 3 assertions verified, 1 error
+single-file.dfy(8,4): Error: assertion might not hold
+
+Dafny program verifier finished with 4 assertions verified, 1 error
 
 Dafny program verifier finished with 1 assertions verified, 0 errors
 
 Dafny program verifier finished with 1 assertions verified, 0 errors
 single-file.dfy(8,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 assertions verified, 1 error
+single-file.dfy(8,4): Error: assertion might not hold
+
+Dafny program verifier finished with 1 assertions verified, 1 error
+
+Dafny program verifier finished with 1 assertions verified, 0 errors
 
 Dafny program verifier finished with 1 assertions verified, 0 errors
 single-file.dfy(16,14): Error: loop invariant violation
@@ -37,3 +45,7 @@ single-file.dfy(24,2): Error: assertion might not hold
 single-file.dfy(24,16): Error: assertion might not hold
 
 Dafny program verifier finished with 0 assertions verified, 2 errors
+single-file.dfy(24,2): Error: assertion might not hold
+single-file.dfy(24,16): Error: assertion might not hold
+
+Dafny program verifier finished with 0 assertions verified, 2 errors

docs/dev/news/6077.feat

@@ -0,0 +1 @@
+Besides `--filter-position :<line>`, also support `--filter-position :<start>-<end>`, `--filter-position :<start>-` and `--filter-position :-<end>`