From 76a7caa5a36b510376e07d99ffa32255c7ac8be5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 24 Jan 2025 16:41:52 +0100 Subject: [PATCH] Enable filtering on a range of assertions (#6077) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### What was changed? Besides `--filter-position :`, also support `--filter-position :-`, `--filter-position :-` and `--filter-position :-` ### How has this been tested? Extended existing test 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). --------- Co-authored-by: Mikaël Mayer --- Source/DafnyDriver/CliCompilation.cs | 55 +++++++++++++------ Source/DafnyDriver/Commands/VerifyCommand.cs | 2 +- .../LitTests/LitTest/verification/filter.dfy | 4 ++ .../LitTest/verification/filter.dfy.expect | 12 ++++ docs/dev/news/6077.feat | 1 + 5 files changed, 57 insertions(+), 17 deletions(-) create mode 100644 docs/dev/news/6077.feat diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 98fba2d30d1..7fa983b15af 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/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 FilterCanVerifies(List 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 FilterCanVerifies(List 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 FilterCanVerifies(List 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(); } 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); } } diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 789db4ee4b9..f2de4002dba 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/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 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."); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index c5cb15cc764..408633c9b96 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/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" \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect index 711d7c90c74..381f316364d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -19,6 +19,9 @@ 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 @@ -26,6 +29,11 @@ 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 diff --git a/docs/dev/news/6077.feat b/docs/dev/news/6077.feat new file mode 100644 index 00000000000..c37bfbef557 --- /dev/null +++ b/docs/dev/news/6077.feat @@ -0,0 +1 @@ +Besides `--filter-position :`, also support `--filter-position :-`, `--filter-position :-` and `--filter-position :-` \ No newline at end of file