Add --performance-stats option and use this on some tests (#5695)

### Description Add `--performance-stats` option and use this on the SchorrWaite test ### How has this been tested? Updated `SchorrWaite.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>
dafny-lang · Aug 16, 2024 · 7e92b41 · 7e92b41
1 parent f88046b
commit 7e92b41
Show file tree

Hide file tree

Showing 9 changed files with 39 additions and 5 deletions.
diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
@@ -315,4 +315,6 @@ record VerificationStatistics {
   public int OutOfResourceCount;
   public int OutOfMemoryCount;
   public int SolverExceptionCount;
+  public int TotalResourcesUsed;
+  public int MaxVcResourcesUsed;
 }
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -20,8 +20,15 @@ static VerifyCommand() {
     // they can't be specified when building a doo file.
     OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli);
     OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli);
+    OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli);
   }
 
+  public static readonly Option<int> PerformanceStatisticsOption = new("--performance-stats",
+    "Report a summary of the verification performance. " +
+    "The given argument is used to divide all the output with, which can help ignore small differences.") {
+    IsHidden = true
+  };
+
   public static readonly Option<string> 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""");
 
@@ -40,6 +47,7 @@ public static Command Create() {
 
   private static IReadOnlyList<Option> VerifyOptions =>
     new Option[] {
+        PerformanceStatisticsOption,
         FilterSymbol,
         FilterPosition,
         DafnyFile.DoNotVerifyDependencies
@@ -80,6 +88,10 @@ public static async Task ReportVerificationSummary(
     verificationResults.Subscribe(result => {
       foreach (var taskResult in result.Results) {
         var runResult = taskResult.Result;
+        Interlocked.Add(ref statistics.TotalResourcesUsed, runResult.ResourceCount);
+        lock (statistics) {
+          statistics.MaxVcResourcesUsed = Math.Max(statistics.MaxVcResourcesUsed, runResult.ResourceCount);
+        }
 
         switch (runResult.Outcome) {
           case SolverOutcome.Valid:
@@ -114,6 +126,16 @@ public static async Task ReportVerificationSummary(
     });
     await verificationResults.WaitForComplete();
     await WriteTrailer(cliCompilation, statistics);
+    var performanceStatisticsDivisor = cliCompilation.Options.Get(PerformanceStatisticsOption);
+    if (performanceStatisticsDivisor != 0) {
+      int Round(int number) {
+        var numberForUpRounding = number + performanceStatisticsDivisor / 2;
+        return (numberForUpRounding / performanceStatisticsDivisor) * performanceStatisticsDivisor;
+      }
+      var output = cliCompilation.Options.OutputWriter;
+      await output.WriteLineAsync($"Total resources used is {Round(statistics.TotalResourcesUsed)}");
+      await output.WriteLineAsync($"Max resources used by VC is {Round(statistics.MaxVcResourcesUsed)}");
+    }
   }
 
   private static async Task WriteTrailer(CliCompilation cliCompilation,

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1
 
 
 codatatype Stream<T> = Cons(head: T, tail: Stream)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
@@ -31,3 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
+Total resources used is 770731
+Max resources used by VC is 60262
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %build "%s" --relax-definite-assignment --allow-axioms > "%t"
+// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module AssignmentToNat {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
@@ -63,10 +63,10 @@ SubsetTypes.dfy(318,18): Error: value does not satisfy the subset constraints of
 SubsetTypes.dfy(323,20): Error: value does not satisfy the subset constraints of 'nat'
 SubsetTypes.dfy(330,20): Error: result of operation might violate newtype constraint for 'Nat'
 SubsetTypes.dfy(337,20): Error: result of operation might violate newtype constraint for 'Nat'
-SubsetTypes.dfy(343,18): Error: value does not satisfy the subset constraints of 'Nat'
 SubsetTypes.dfy(342,7): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
-SubsetTypes.dfy(348,18): Error: result of operation might violate newtype constraint for 'Nat'
+SubsetTypes.dfy(343,18): Error: value does not satisfy the subset constraints of 'Nat'
 SubsetTypes.dfy(347,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+SubsetTypes.dfy(348,18): Error: result of operation might violate newtype constraint for 'Nat'
 SubsetTypes.dfy(352,7): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 SubsetTypes.dfy(360,21): Error: possible division by zero
 SubsetTypes.dfy(365,23): Error: possible division by zero
@@ -91,3 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
+Total resources used is 738270
+Max resources used by VC is 67520
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --performance-stats=1
 
 
 // Rustan Leino

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect
@@ -1,2 +1,4 @@
 
 Dafny program verifier finished with 15 verified, 0 errors
+Total resources used is 26054893
+Max resources used by VC is 15592113
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect
@@ -0,0 +1,4 @@
+
+Dafny program verifier finished with 15 verified, 0 errors
+Total resources used is 28044428
+Max resources used by VC is 16505967