From 68f96d0f1b7b9659592c55c4f306d07128324e87 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Feb 2024 00:09:05 +0100 Subject: [PATCH] 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` 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). --- Source/DafnyCore/AST/IHasUsages.cs | 2 ++ Source/DafnyCore/AST/Members/Function.cs | 3 +- .../AST/TypeDeclarations/DatatypeCtor.cs | 1 + Source/DafnyCore/Options/BoogieOptionBag.cs | 3 +- Source/DafnyDriver/CliCompilation.cs | 13 +++++--- Source/DafnyDriver/Commands/VerifyCommand.cs | 7 +++- .../LitTest/verification/filter-symbol.dfy | 27 +++++++++++++++ .../verification/filter-symbol.dfy.expect | 33 +++++++++++++++++++ docs/dev/news/4816.feat | 3 +- 9 files changed, 84 insertions(+), 8 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect diff --git a/Source/DafnyCore/AST/IHasUsages.cs b/Source/DafnyCore/AST/IHasUsages.cs index 090d2d39227..47905ba13a6 100644 --- a/Source/DafnyCore/AST/IHasUsages.cs +++ b/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. /// bool ShouldVerify { get; } + + string FullDafnyName { get; } } public static class AstExtensions { diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 51009797e97..fad27e55094 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/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) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 660350c7749..6721d1ce0ab 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/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; } \ No newline at end of file diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 2e17ba5cfb7..274c2bb4424 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -11,9 +11,10 @@ namespace Microsoft.Dafny; public static class BoogieOptionBag { public static readonly Option> BoogieFilter = new("--boogie-filter", @" -(experimental) Only check proofs whose Boogie name is matched by pattern

. This option may be specified multiple times to match multiple patterns. The pattern

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

. This option may be specified multiple times to match multiple patterns. The pattern

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> BoogieArguments = new("--boogie", diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 2bb07b3c550..ec34f9ff8c8 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/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 FilterCanVerifies(List 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 FilterCanVerifies(List 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; diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 258be4d6a3e..1986fc9f49f 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/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 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 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