Test Generation Auditor #4444

Dargones · 2023-08-19T23:25:01Z

This PR (number 4444:) introduces a test generation auditor that scans the program for anything that will cause test generation to fail (errors) or might lead to less helpful results (warnings). These are reported via ConsoleErrorReporter like Dafny would report any other problems. Dafny returns a non-zero exit code and terminates execution if any errors are present or if there are warnings and the --warn-as-errors flag is on. Here is the list of all errors/warnings that can be emitted.

Errors:

Cannot find a method or function annotated with {:testEntry} attribute
Program is not wrapped in a module. Put your code inside "module M {}" or equivalent
{:testInline} attribute on the method [METHOD] can only take one argument, which must be a positive integer specifying the recursion unrolling limit (absence of such an argument or 1 means no unrolling)
Test Generation does not support abstract types, array types, and trait types as inputs. Consider disallowing values of type [TYPE] to be part of the input to {:testEntry}-annotated method [METHOD]
Any error from parser or resolver is propagated up and reported as well

Warnings:

Method [METHOD] will not be inlined because it is not reachable from any of the {:testEntry}-annotated methods or functions
Test Generation does not fully support function types as inputs. Consider disallowing values of type [TYPE] to be part of the input to {:testEntry}-annotated method [METHOD]
Cannot find witness for type [TYPE]. Please consider adding a witness to the declaration
Method [METHOD] is annotated with {:timeLimit 300} but test generation is called with --verification-time-limit:20. Consider increasing the time limit for test generation.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Dargones · 2023-08-19T23:27:43Z

As a side note, I noticed that several tests throughout the project use the Utils.Parse method from DafnyTestGeneration to parse the input. Is there perhaps a better place I should move it to?

Dargones · 2023-08-23T18:56:59Z

Update: I brought the errors reporting mechanism in line with how it works in Dafny more generally - warnings are colored in yellow, errors in red, and -warn-as-errors flag treats warnings like errors

atomb

The implementation looks great, and I mostly had comments about terminology, both in messages and internal names. The key one is that I'm not sure that distinguishing this from the rest of the test generation code with the name "auditor" has a lot of purpose. It's just the first step of test generation, in my mind.

atomb · 2023-08-24T22:34:46Z

Source/DafnyCore/Generic/Reporting.cs

@@ -14,7 +14,7 @@ public enum ErrorLevel {
  }

  public enum MessageSource {
-    Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation
+    Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation, TestGenerationAuditor


I'm not sure that the Auditor term adds much here. I'd just call this TestGeneration. And the checks performed here are just the first phase of test generation.

This makes sense. Have made the change

atomb · 2023-08-24T22:36:53Z

Source/DafnyTestGeneration.Test/AuditorTests.cs

+
+namespace DafnyTestGeneration.Test;
+
+public class AuditorTests : Setup {


I might call this WarningTests or something, to avoid confusion with the separate feature that uses the name "auditor".

It's great to have lots of tests of this, BTW. :)

atomb · 2023-08-24T22:47:25Z

Source/DafnyTestGeneration/Auditor.cs

+  /// </summary>
+  private void PrintWarningsAndErrors(ErrorReporter errorReporter, Program program) {
+    if (Errors.Count() != 0) {
+      errorReporter.Message(MessageSource.TestGenerationAuditor, ErrorLevel.Error, "", program.StartToken,


Is there a reason you can't use the more concise Error method instead of the Message method?

No, I think I just wasn't aware that can use Error/Message - have changed the code to use them now

atomb · 2023-08-24T22:47:41Z

Source/DafnyTestGeneration/Auditor.cs

+      }
+    }
+    if (Warnings.Count() != 0) {
+      errorReporter.Message(MessageSource.TestGenerationAuditor, ErrorLevel.Warning, "", program.StartToken,


Similarly to errors, can you use Warning here?

atomb · 2023-08-24T22:52:29Z

Source/DafnyTestGeneration/Auditor.cs

+    }
+    if (type is UserDefinedType userDefinedType) {
+      var genericMessage =
+        $"Consider disallowing values of type {userDefinedType} to be part of the input to " +


The word "disallowing" seems weird here. Maybe use terminology similar to what you use elsewhere about writing a wrapper to generate types that can't be constructed automatically out of types that can?

I have paraphrased this to "Consider modeling values of type TYPE with a datatype and passing them as input to the {:testEntry} annotated method". I agree that something along these lines should be better than "disallowing" since it tells the user what to do to prevent the error.

Dargones · 2023-08-24T23:58:58Z

Thank you, @atomb! I have made all the changes and have also renamed Auditor to FirstPass to avoid confusion with the top-level Auditor functionality.

atomb

This looks great!

This PR (number 4444:) introduces a test generation auditor that scans the program for anything that will cause test generation to fail (errors) or might lead to less helpful results (warnings). These are reported via `ConsoleErrorReporter` like Dafny would report any other problems. Dafny returns a non-zero exit code and terminates execution if any errors are present or if there are warnings and the `--warn-as-errors` flag is on. Here is the list of all errors/warnings that can be emitted. Errors: - Cannot find a method or function annotated with {:testEntry} attribute - Program is not wrapped in a module. Put your code inside \"module M {}\" or equivalent - {:testInline} attribute on the method [METHOD] can only take one argument, which must be a positive integer specifying the recursion unrolling limit (absence of such an argument or 1 means no unrolling) - Test Generation does not support abstract types, array types, and trait types as inputs. Consider disallowing values of type [TYPE] to be part of the input to {:testEntry}-annotated method [METHOD] - Any error from parser or resolver is propagated up and reported as well Warnings: - Method [METHOD] will not be inlined because it is not reachable from any of the {:testEntry}-annotated methods or functions - Test Generation does not fully support function types as inputs. Consider disallowing values of type [TYPE] to be part of the input to {:testEntry}-annotated method [METHOD] - Cannot find witness for type [TYPE]. Please consider adding a witness to the declaration - Method [METHOD] is annotated with {:timeLimit 300} but test generation is called with --verification-time-limit:20. Consider increasing the time limit for test generation. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com>

Aleksandr Fedchin added 3 commits August 19, 2023 15:49

Auditor for Test Generation

69fe6cd

Undo accidental change

470e562

Update dev news

f59209f

Aleksandr Fedchin added 2 commits August 19, 2023 20:15

Allow testInline attribute with no argument

54cd3c6

Fix tests

bc33f13

Dargones mentioned this pull request Aug 20, 2023

Documenting Test Generation in Reference Manual #4445

Merged

Aleksandr Fedchin added 3 commits August 21, 2023 15:24

Remove LengthLimitWarning

8444c0a

Use Lines as the units of coverage

1d574c4

Rename CallGraph to InlinedBlock

89b5086

Dargones mentioned this pull request Aug 22, 2023

Test Generation Post dafny-lang/blog#9

Merged

Aleksandr Fedchin added 2 commits August 23, 2023 11:28

Use warn-as-errors flag

56596e0

Use ConsoleErrorReporter to color warnings

add26cd

Merge branch 'master' into Auditor

a0e649f

atomb requested changes Aug 24, 2023

View reviewed changes

Remove Auditor to First Pass and paraphrase some messages

05770bf

atomb approved these changes Aug 25, 2023

View reviewed changes

Merge branch 'master' into Auditor

6a82c35

atomb enabled auto-merge (squash) August 25, 2023 15:10

Merge branch 'master' into Auditor

43efe3d

atomb merged commit 95eb74b into dafny-lang:master Aug 25, 2023
18 checks passed

BrewTestBot mentioned this pull request Sep 29, 2023

dafny 4.3.0 Homebrew/homebrew-core#146965

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Test Generation Auditor #4444

Test Generation Auditor #4444

Dargones commented Aug 19, 2023 •

edited

Loading

Dargones commented Aug 19, 2023

Dargones commented Aug 23, 2023 •

edited

Loading

atomb left a comment

atomb Aug 24, 2023

Dargones Aug 24, 2023

atomb Aug 24, 2023

atomb Aug 24, 2023

Dargones Aug 24, 2023

atomb Aug 24, 2023

Dargones Aug 24, 2023

atomb Aug 24, 2023

atomb Aug 24, 2023

Dargones Aug 24, 2023

Dargones commented Aug 24, 2023

atomb left a comment


		namespace DafnyTestGeneration.Test;

		public class AuditorTests : Setup {

Test Generation Auditor #4444

Test Generation Auditor #4444

Conversation

Dargones commented Aug 19, 2023 • edited Loading

Dargones commented Aug 19, 2023

Dargones commented Aug 23, 2023 • edited Loading

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones commented Aug 24, 2023

atomb left a comment

Choose a reason for hiding this comment

Dargones commented Aug 19, 2023 •

edited

Loading

Dargones commented Aug 23, 2023 •

edited

Loading