Add a --format json option to measure-complexity

Source/DafnyCore/JsonDiagnostics.cs

@@ -11,7 +11,7 @@
 
 namespace Microsoft.Dafny;
 
-record DiagnosticMessageData(MessageSource source, ErrorLevel level, Boogie.IToken tok, string? category, string message, List<ErrorInformation.AuxErrorInfo>? related) {
+public record DiagnosticMessageData(MessageSource source, ErrorLevel level, Boogie.IToken tok, string? category, string message, List<ErrorInformation.AuxErrorInfo>? related) {
   private static JsonObject SerializePosition(Boogie.IToken tok) {
     return new JsonObject {
       ["pos"] = tok.pos,
@@ -20,7 +20,7 @@ private static JsonObject SerializePosition(Boogie.IToken tok) {
     };
   }
 
-  private static JsonObject SerializeRange(Boogie.IToken tok) {
+  public static JsonObject SerializeRange(Boogie.IToken tok) {
     var range = new JsonObject {
       ["start"] = SerializePosition(tok),
     };
@@ -31,7 +31,7 @@ private static JsonObject SerializeRange(Boogie.IToken tok) {
     return range;
   }
 
-  private static JsonObject SerializeToken(Boogie.IToken tok) {
+  public static JsonObject SerializeToken(Boogie.IToken tok) {
     return new JsonObject {
       ["filename"] = tok.filename,
       ["uri"] = ((IOrigin)tok).Uri.AbsoluteUri,

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -14,12 +14,12 @@ public class CommonOptionBag {
 
   public static void EnsureStaticConstructorHasRun() { }
 
-  public enum ProgressLevel { None, Symbol, VerificationJobs }
+  public enum ProgressLevel { None, Iterations, Symbols, Jobs }
   public static readonly Option<ProgressLevel> ProgressOption =
     new("--progress", $"While verifying, output information that helps track progress. " +
-                      $"Use '{ProgressLevel.Symbol}' to show progress across symbols such as methods and functions. " +
+                      $"Use '{ProgressLevel.Symbols}' to show progress across symbols such as methods and functions. " +
                       $"Verification of a symbol is usually split across several jobs. " +
-                      $"Use {ProgressLevel.VerificationJobs} to additionally show progress across jobs.");
+                      $"Use {ProgressLevel.Jobs} to additionally show progress across jobs.");
 
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {

Source/DafnyDriver/CliCompilation.cs

@@ -186,7 +186,7 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed =
         canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
         var completedPartsCount = Interlocked.Increment(ref canVerifyResult.CompletedCount);
 
-        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.VerificationJobs) {
+        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.Jobs) {
           var partOrigin = boogieUpdate.VerificationTask.Split.Token;
 
           var wellFormedness = boogieUpdate.VerificationTask.Split.Implementation.Name.Contains("CheckWellFormed$");
@@ -267,7 +267,7 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) {
       foreach (var canVerify in toAwait) {
         var results = canVerifyResults[canVerify];
         try {
-          if (Options.Get(CommonOptionBag.ProgressOption) > CommonOptionBag.ProgressLevel.None) {
+          if (Options.Get(CommonOptionBag.ProgressOption) >= CommonOptionBag.ProgressLevel.Symbols) {
             await Options.OutputWriter.WriteLineAsync(
               $"Verified {done}/{canVerifies.ToList().Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
           }

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -1,22 +1,24 @@
 using System;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.CommandLine;
 using System.Linq;
 using System.Reactive.Subjects;
+using System.Text.Json;
+using System.Text.Json.Nodes;
 using System.Threading;
 using System.Threading.Tasks;
-using DafnyCore;
 using DafnyDriver.Commands;
 using Microsoft.Boogie;
-using VC;
 
 namespace Microsoft.Dafny;
 
 static class MeasureComplexityCommand {
   public static IEnumerable<Option> Options => new Option[] {
     Iterations,
     RandomSeed,
-    TopX,
+    FormatOption,
+    WorstAmountOption,
     VerifyCommand.FilterSymbol,
     VerifyCommand.FilterPosition,
   }.Concat(DafnyCommands.VerificationOptions).
@@ -29,10 +31,17 @@ static MeasureComplexityCommand() {
 
     OptionRegistry.RegisterOption(Iterations, OptionScope.Cli);
     OptionRegistry.RegisterOption(RandomSeed, OptionScope.Cli);
-    OptionRegistry.RegisterOption(TopX, OptionScope.Cli);
+    OptionRegistry.RegisterOption(FormatOption, OptionScope.Cli);
+    OptionRegistry.RegisterOption(WorstAmountOption, OptionScope.Cli);
   }
 
-  private static readonly Option<uint> TopX = new("--worst-amount", () => 10U,
+  enum ComplexityFormat { Text, Json, LineBased }
+  private static readonly Option<ComplexityFormat> FormatOption = new("--format", 
+    $"Specify the format in which the complexity data is presented") {
+    IsHidden = true
+  };
+
+  private static readonly Option<uint> WorstAmountOption = new("--worst-amount", () => 10U,
     $"Configures the amount of worst performing verification tasks that are reported.");
 
   private static readonly Option<uint> RandomSeed = new("--random-seed", () => 0U,
@@ -54,6 +63,7 @@ public static Command Create() {
   }
 
   private static async Task<int> Execute(DafnyOptions options) {
+    options.Set(DafnyFile.DoNotVerifyDependencies, true);
     if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
       options.TrackVerificationCoverage = true;
     }
@@ -84,14 +94,27 @@ private static async Task<int> Execute(DafnyOptions options) {
     return await compilation.GetAndReportExitCode();
   }
 
+  record TaskIterationStatistics {
+    public ConcurrentBag<int> ResourceCounts = new();
+    public ConcurrentBag<double> VerificationTimes = new();
+    public int Timeouts;
+    public int ResourceOuts;
+    public int Failures;
+    public int Measurements;
+  }
+
   public static async Task ReportResourceSummary(
     CliCompilation cliCompilation,
     IObservable<CanVerifyResult> verificationResults) {
 
+    var allStatistics = new ConcurrentDictionary<string, TaskIterationStatistics>();
     PriorityQueue<VerificationTaskResult, int> worstPerformers = new();
 
-    var totalResources = 0;
-    var worstAmount = cliCompilation.Options.Get(TopX);
+    var totalResources = 0L;
+    var worstAmount = cliCompilation.Options.Get(WorstAmountOption);
+    if (worstAmount == 0) {
+      worstAmount = int.MaxValue;
+    }
     verificationResults.Subscribe(result => {
       foreach (var taskResult in result.Results) {
         var runResult = taskResult.Result;
@@ -100,6 +123,27 @@ public static async Task ReportResourceSummary(
         if (worstPerformers.Count > worstAmount) {
           worstPerformers.Dequeue();
         }
+
+        var key = taskResult.Task.Split.Implementation.Name + taskResult.Task.Split.Token.ShortName;
+        var statistics = allStatistics.GetOrAdd(key, _ => new TaskIterationStatistics());
+        var failed = false;
+        if (runResult.Outcome == SolverOutcome.Valid) {
+          statistics.ResourceCounts.Add(runResult.ResourceCount);
+          statistics.VerificationTimes.Add(runResult.RunTime.TotalSeconds);
+        } else if (runResult.Outcome == SolverOutcome.TimeOut) {
+          Interlocked.Increment(ref statistics.Timeouts);
+          failed = true;
+        } else if (runResult.Outcome == SolverOutcome.OutOfResource) {
+          Interlocked.Increment(ref statistics.ResourceOuts);
+          failed = true;
+        } else if (runResult.Outcome == SolverOutcome.Invalid) {
+          failed = true;
+        }
+
+        if (failed) {
+          Interlocked.Increment(ref statistics.Failures);
+        }
+        Interlocked.Increment(ref statistics.Measurements);
       }
     });
     await verificationResults.WaitForComplete();
@@ -108,23 +152,73 @@ public static async Task ReportResourceSummary(
     while (worstPerformers.Count > 0) {
       decreasingWorst.Push(worstPerformers.Dequeue());
     }
-
-    await output.WriteLineAsync($"The total consumed resources are {totalResources}");
-    await output.WriteLineAsync($"The most demanding {worstAmount} verification tasks consumed these resources:");
-    foreach (var performer in decreasingWorst) {
-      var location = BoogieGenerator.ToDafnyToken(false, performer.Task.Token).TokenToString(cliCompilation.Options);
-      await output.WriteLineAsync($"{location}: {performer.Result.ResourceCount}");
+    if (cliCompilation.Options.Get(FormatOption) == ComplexityFormat.LineBased) {
+      var lines = decreasingWorst.GroupBy(t => t.Task.Token.line).
+        OrderBy(g => g.Key).
+        Select(g => g.Key + ", " + Math.Floor(g.Average(i => i.Result.ResourceCount)));
+
+      await output.WriteLineAsync($"Average resource for each line:\n" + string.Join("\n", lines));
+    } 
+    else if (cliCompilation.Options.Get(FormatOption) == ComplexityFormat.Text)
+    {
+      await output.WriteLineAsync($"The total consumed resources are {totalResources}");
+      await output.WriteLineAsync($"The most demanding {worstAmount} verification tasks consumed these resources:");
+      foreach (var performer in decreasingWorst) {
+        var location = BoogieGenerator.ToDafnyToken(false, performer.Task.Token).TokenToString(cliCompilation.Options);
+        await output.WriteLineAsync($"{location}: {performer.Result.ResourceCount}");
+      }
+    } else if (cliCompilation.Options.Get(FormatOption) == ComplexityFormat.Json) {
+      var json = new JsonObject {
+        ["totalResources"] = totalResources,
+        ["worstPerforming"] = new JsonArray(decreasingWorst.Select(task => new JsonObject {
+          ["location"] = SerializeToken(task.Task.Token),
+          ["resourceCount"] = task.Result.ResourceCount
+        }).ToArray<JsonNode>()),
+        ["taskData"] = new JsonArray(allStatistics.Select(entry => {
+          var (stdDevRc, averageRc) = entry.Value.ResourceCounts.ToList().CalculateStdDev();
+          var (stdDevVt, averageVt) = entry.Value.VerificationTimes.ToList().CalculateStdDev();
+          var failuresAndHighVariations = entry.Value.Failures + entry.Value.ResourceCounts.Count(rc => rc > averageRc * 2);
+          return new JsonObject {
+            ["key"] = entry.Key,
+            ["rcs"] = new JsonArray(entry.Value.ResourceCounts.Select(r => JsonValue.Create(r)).ToArray<JsonNode>()),
+            ["vts"] = new JsonArray(entry.Value.VerificationTimes.Select(r => JsonValue.Create(r)).ToArray<JsonNode>()),
+            ["averageRc"] = averageRc,
+            ["standardDeviationRc"] = stdDevRc,
+            ["relativeStandardDeviationRc"] = stdDevRc / averageRc,
+            ["averageVt"] = averageVt,
+            ["standardDeviationVt"] = stdDevVt,
+            ["relativeStandardDeviationVt"] = stdDevVt / averageVt,
+            ["timeouts"] = entry.Value.Timeouts,
+            ["resourceOuts"] = entry.Value.ResourceOuts,
+            ["failures"] = entry.Value.Failures,
+            ["relFailures"] = (double)entry.Value.Failures / entry.Value.Measurements,
+            ["failuresAndHighVariations"] = failuresAndHighVariations,
+            ["relFailuresAndHighVariations"] = (double)failuresAndHighVariations / entry.Value.Measurements,
+          };
+        }).ToArray<JsonNode>())
+      };
+      var outputString = json.ToJsonString(new JsonSerializerOptions { WriteIndented = false });
+      await output.WriteLineAsync(outputString);
     }
   }
 
+  private static JsonObject SerializeToken(Boogie.IToken tok) {
+    return new JsonObject {
+      ["uri"] = BoogieGenerator.ToDafnyToken(false, tok).Uri.AbsoluteUri,
+      ["range"] = DiagnosticMessageData.SerializeRange(tok)
+    };
+  }
+
   private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation,
     IObserver<CanVerifyResult> verificationResultsObserver) {
     int iterationSeed = (int)options.Get(RandomSeed);
     var random = new Random(iterationSeed);
     var iterations = (int)options.Get(Iterations);
     foreach (var iteration in Enumerable.Range(0, iterations)) {
-      await options.OutputWriter.WriteLineAsync(
-        $"Starting verification of iteration {iteration + 1}/{iterations} with seed {iterationSeed}");
+      if (options.Get(CommonOptionBag.ProgressOption) >= CommonOptionBag.ProgressLevel.Iterations) {
+        await options.OutputWriter.WriteLineAsync(
+          $"{DateTime.Now.ToLocalTime()}: Starting verification of iteration {iteration + 1}/{iterations} with seed {iterationSeed}");
+      }
       try {
         await foreach (var result in compilation.VerifyAllLazily(iterationSeed)) {
           verificationResultsObserver.OnNext(result);
@@ -137,3 +231,45 @@ await options.OutputWriter.WriteLineAsync(
     verificationResultsObserver.OnCompleted();
   }
 }
+public static class ExtensionsClass
+{
+  public static (double StdDev, double Average) CalculateStdDev(this IReadOnlyList<double> values)
+  {
+    if (values.Count == 0) {
+      return (-1, -1);
+    }
+
+    if (values.Count > 1)
+    {
+      // Compute the Average
+      double avg = values.Average();
+
+      // Perform the Sum of (value-avg)^2
+      double sum = values.Sum(d => (d - avg) * (d - avg));
+
+      return (Math.Sqrt(sum / values.Count), avg);
+    }
+
+    return (0, values[0]);
+  }
+
+  public static (double StdDev, double Average) CalculateStdDev(this IReadOnlyList<int> values)
+  {
+    if (values.Count == 0) {
+      return (-1, -1);
+    }
+
+    if (values.Count > 1)
+    {
+      // Compute the Average
+      double avg = values.Average();
+
+      // Perform the Sum of (value-avg)^2
+      double sum = values.Sum(d => (d - avg) * (d - avg));
+
+      return (Math.Sqrt(sum / values.Count), avg);
+    }
+
+    return (0, values[0]);
+  }
+}

Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy

@@ -291,6 +291,7 @@ module Std.JSON.ZeroCopy.Deserializer {
       ensures
         var sp := Core.TryStructural(cs);
         var s0 := sp.t.t.Peek();
+        hide *;
         && ((!cs.BOF? || !cs.EOF?) && (s0 == SEPARATOR as opt_byte) ==> (var sp: Split<Structural<jcomma>> := sp; sp.cs.StrictSuffixOf?(cs)))
         && ((s0 == SEPARATOR as opt_byte) ==> var sp: Split<Structural<jcomma>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
         && ((!cs.BOF? || !cs.EOF?) && (s0 == CLOSE as opt_byte) ==> (var sp: Split<Structural<jclose>> := sp; sp.cs.StrictSuffixOf?(cs)))

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy

@@ -256,7 +256,7 @@ method {:isolate_assertions} SchorrWaite(root: Node, ghost S: set<Node>)
     decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited
   {
     if t.childrenVisited == |t.children| {
-      assert {:focus} true;
+      //assert {:focus} true;
       // pop
       t.childrenVisited := 0;
       if p == null {
@@ -271,12 +271,12 @@ method {:isolate_assertions} SchorrWaite(root: Node, ghost S: set<Node>)
       path := t.pathFromRoot;
 
     } else if t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked {
-      assert {:focus} true;
+      //assert {:focus} true;
       // just advance to next child
       t.childrenVisited := t.childrenVisited + 1;
 
     } else {
-      assert {:focus} true;
+      //assert {:focus} true;
       // push
 
       var newT := t.children[t.childrenVisited];
@@ -289,5 +289,7 @@ method {:isolate_assertions} SchorrWaite(root: Node, ghost S: set<Node>)
       t.pathFromRoot := path;
       unmarkedNodes := unmarkedNodes - {t};
     }
+
+    continue {:isolate "paths"};
   }
 }