More random seed logging (dafny-lang#5159)

### Description
- Report non-zero random seeds uniformly across log format

### How has this been tested?
- Manually. `measure-complexity` should get more littish tests

<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>

Source/DafnyDriver/CSVTestLogger.cs

@@ -70,10 +70,11 @@ private void TestResultHandler(object sender, TestResultEventArgs e) {
     }
 
     private void TestRunCompleteHandler(object sender, TestRunCompleteEventArgs e) {
-      writer.WriteLine("TestResult.DisplayName,TestResult.Outcome,TestResult.Duration,TestResult.ResourceCount");
+      writer.WriteLine("TestResult.DisplayName,TestResult.Outcome,TestResult.Duration,TestResult.ResourceCount,RandomSeed");
       foreach (var result in results.OrderByDescending(r => r.Duration)) {
-        var resCount = result.GetPropertyValue(VerificationResultLogger.ResourceCountProperty);
-        writer.WriteLine($"{result.TestCase.DisplayName},{result.Outcome},{result.Duration},{resCount}");
+        var resourceCount = result.GetPropertyValue(VerificationResultLogger.ResourceCountProperty);
+        var randomSeed = result.GetPropertyValue(VerificationResultLogger.RandomSeedProperty) ?? "unknown";
+        writer.WriteLine($"{result.TestCase.DisplayName},{result.Outcome},{result.Duration},{resourceCount},{randomSeed}");
       }
 
       writer.Flush();

Source/DafnyDriver/JsonVerificationLogger.cs

@@ -47,14 +47,18 @@ public static JsonNode SerializeProofDependency(ProofDependency dependency) {
     };
   }
 
-  public static JsonNode SerializeVcResult(ProofDependencyManager dependencyManager, IReadOnlyList<ProofDependency> potentialDependencies, VerificationRunResult vcResult) {
+  public static JsonNode SerializeVcResult(ProofDependencyManager dependencyManager, IReadOnlyList<ProofDependency> potentialDependencies, VerificationTaskResult taskResult) {
+    var vcResult = taskResult.Result;
     var result = new JsonObject {
       ["vcNum"] = vcResult.VcNum,
       ["outcome"] = SerializeOutcome(vcResult.Outcome),
       ["runTime"] = SerializeTimeSpan(vcResult.RunTime),
       ["resourceCount"] = vcResult.ResourceCount,
       ["assertions"] = new JsonArray(vcResult.Asserts.Select(SerializeAssertion).ToArray()),
     };
+    if (taskResult.Task != null && taskResult.Task.Split.RandomSeed != 0) {
+      result["randomSeed"] = taskResult.Task.Split.RandomSeed.ToString();
+    }
     if (potentialDependencies is not null) {
       var fullDependencySet = dependencyManager.GetOrderedFullDependencies(vcResult.CoveredElements).ToHashSet();
       var unusedDependencies = potentialDependencies.Where(dep => !fullDependencySet.Contains(dep));
@@ -75,17 +79,17 @@ private static JsonNode SerializeOutcome(VcOutcome outcome) {
     return outcome.ToString();
   }
 
-  private JsonNode SerializeVerificationResult(VerificationScope scope, IReadOnlyList<VerificationRunResult> results) {
+  private JsonNode SerializeVerificationResult(VerificationScope scope, IReadOnlyList<VerificationTaskResult> results) {
     var trackProofDependencies =
-      results.All(o => o.Outcome == SolverOutcome.Valid) &&
-      results.Any(vcResult => vcResult.CoveredElements.Any());
+      results.All(o => o.Result.Outcome == SolverOutcome.Valid) &&
+      results.Any(vcResult => vcResult.Result.CoveredElements.Any());
     var potentialDependencies =
       trackProofDependencies ? dependencyManager.GetPotentialDependenciesForDefinition(scope.Name).ToList() : null;
     var result = new JsonObject {
       ["name"] = scope.Name,
-      ["outcome"] = SerializeOutcome(results.Aggregate(VcOutcome.Correct, (o, r) => MergeOutcomes(o, r.Outcome))),
-      ["runTime"] = SerializeTimeSpan(TimeSpan.FromSeconds(results.Sum(r => r.RunTime.Seconds))),
-      ["resourceCount"] = results.Sum(r => r.ResourceCount),
+      ["outcome"] = SerializeOutcome(results.Aggregate(VcOutcome.Correct, (o, r) => MergeOutcomes(o, r.Result.Outcome))),
+      ["runTime"] = SerializeTimeSpan(TimeSpan.FromSeconds(results.Sum(r => r.Result.RunTime.Seconds))),
+      ["resourceCount"] = results.Sum(r => r.Result.ResourceCount),
       ["vcResults"] = new JsonArray(results.Select(r => SerializeVcResult(dependencyManager, potentialDependencies, r)).ToArray())
     };
     if (potentialDependencies is not null) {
@@ -134,7 +138,7 @@ public static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome
   }
 
   public void LogScopeResults(VerificationScopeResult scopeResult) {
-    verificationResultNode.Add(SerializeVerificationResult(scopeResult.Scope, scopeResult.Results.Select(r => r.Result).ToList()));
+    verificationResultNode.Add(SerializeVerificationResult(scopeResult.Scope, scopeResult.Results.ToList()));
   }
 
   private readonly IList<JsonNode> verificationResultNode = new List<JsonNode>();

Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs

@@ -40,12 +40,12 @@ private JsonNode SerializeVcResult(IEnumerable<ProofDependency> potentialDepende
     return JsonVerificationLogger.SerializeVcResult(depManager, potentialDependencies?.ToList(), runResult);
   }
 
-  public static VerificationRunResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VCResultLogEntry vcResult) {
+  public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VCResultLogEntry vcResult) {
     var mockNumber = 42;
     var mockAsserts = vcResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description)));
     var runResult = new VerificationRunResult(vcResult.VCNum, mockNumber, vcResult.StartTime, vcResult.Outcome, vcResult.RunTime, mockNumber, null!,
       mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null);
-    return runResult;
+    return new VerificationTaskResult(null, runResult);
   }
 
   private static JsonNode SerializeTimeSpan(TimeSpan timeSpan) {

Source/DafnyDriver/Legacy/LegacyTextVerificationLogger.cs

@@ -21,7 +21,7 @@ public void Initialize(Dictionary<string, string> parameters) {
 
   public void LogResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verificationResults) {
     foreach (var (implementation, result) in verificationResults.OrderBy(vr => (vr.Implementation.Tok.filename, vr.Implementation.Tok.line, vr.Implementation.Tok.col))) {
-      var taskResults = result.VCResults.Select(r => new VerificationTaskResult(null!, LegacyJsonVerificationLogger.VCResultLogEntryToPartialVerificationRunResult(r))).ToList();
+      var taskResults = result.VCResults.Select(LegacyJsonVerificationLogger.VCResultLogEntryToPartialVerificationRunResult).ToList();
       var scopeResult = new VerificationScopeResult(new VerificationScope(implementation.Name, implementation.Tok), taskResults);
       TextVerificationLogger.LogResults(depManager, outWriter, scopeResult);
     }

Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs

@@ -77,7 +77,7 @@ private static IEnumerable<TestResult> VerificationToTestResults(IEnumerable<(Da
 
       foreach (var ((verbName, currentFile), vcResults) in verificationResults) {
         var scopeResult = new VerificationScopeResult(new VerificationScope(verbName, currentFile),
-          vcResults.Select(r => new VerificationTaskResult(null, LegacyJsonVerificationLogger.VCResultLogEntryToPartialVerificationRunResult(r))).ToList());
+          vcResults.Select(LegacyJsonVerificationLogger.VCResultLogEntryToPartialVerificationRunResult).ToList());
         testResults.AddRange(VerificationResultLogger.VerificationToTestResults(scopeResult));
       }
 

Source/DafnyDriver/TextVerificationLogger.cs

@@ -41,10 +41,14 @@ public static void LogResults(ProofDependencyManager proofDependencyManager, Tex
     var maximumResourceCount = results.MaxBy(r => r.ResourceCount).ResourceCount.ToString() ?? "N/A";
     textWriter.WriteLine($"  Maximum assertion batch time: {maximumTime}");
     textWriter.WriteLine($"  Maximum assertion batch resource count: {maximumResourceCount}");
-    foreach (var vcResult in results.OrderBy(r => r.VcNum)) {
+    foreach (var taskResult in scopeResult.Results.OrderBy(r => r.Result.VcNum)) {
+      var vcResult = taskResult.Result;
       textWriter.WriteLine("");
       textWriter.WriteLine($"  Assertion batch {vcResult.VcNum}:");
       textWriter.WriteLine($"    Outcome: {vcResult.Outcome}");
+      if (taskResult.Task != null && taskResult.Task.Split.RandomSeed != 0) {
+        textWriter.WriteLine($"    Random seed: {taskResult.Task.Split.RandomSeed}");
+      }
       textWriter.WriteLine($"    Duration: {vcResult.RunTime}");
       textWriter.WriteLine($"    Resource count: {vcResult.ResourceCount}");
       textWriter.WriteLine("");

Source/DafnyDriver/VerificationResultLogger.cs

@@ -37,6 +37,7 @@ public class VerificationResultLogger {
     private readonly DafnyOptions options;
 
     public static TestProperty ResourceCountProperty = TestProperty.Register("TestResult.ResourceCount", "TestResult.ResourceCount", typeof(int), typeof(TestResult));
+    public static TestProperty RandomSeedProperty = TestProperty.Register("TestResult.RandomSeed", "TestResult.RandomSeed", typeof(int), typeof(TestResult));
 
     private readonly IList<IVerificationResultFormatLogger> formatLoggers = new List<IVerificationResultFormatLogger>();
     private readonly LocalTestLoggerEvents events;
@@ -131,7 +132,7 @@ public static IEnumerable<TestResult> VerificationToTestResults(VerificationScop
                  Select(r => r)) {
         var name = (result.Results.Count > 1
           ? verificationScope.Name + $" (assertion batch {vcResult.VcNum})"
-          : verificationScope.Name) + (task == null ? "" : $" (seed {task.Split.RandomSeed})");
+          : verificationScope.Name);
         var testCase = new TestCase {
           FullyQualifiedName = name,
           ExecutorUri = new Uri("executor://dafnyverifier/v1"),
@@ -142,6 +143,9 @@ public static IEnumerable<TestResult> VerificationToTestResults(VerificationScop
           Duration = vcResult.RunTime
         };
         testResult.SetPropertyValue(ResourceCountProperty, vcResult.ResourceCount);
+        if (task != null && task.Split.RandomSeed != 0) {
+          testResult.SetPropertyValue(RandomSeedProperty, task.Split.RandomSeed);
+        }
         if (vcResult.Outcome == SolverOutcome.Valid) {
           testResult.Outcome = TestOutcome.Passed;
         } else {

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CSVLogger.dfy

@@ -5,9 +5,9 @@
 // The CHECK-NOT directives are a regression test: previously the BoogieXmlConvertor
 // wasn't populating the resource count test result property, and the CSV logger was
 // defaulting to 0 for that column.
-// CHECK-NOT: ExampleWithSplits.*,Passed,.*,0
+// CHECK-NOT: ExampleWithSplits.*,Passed,.*,0,.*
 // CHECK: ExampleWithSplits.*,Passed,.*,.*
-// CHECK-NOT: ExampleWithSplits.*,Passed,.*,0
+// CHECK-NOT: ExampleWithSplits.*,Passed,.*,0,.*
 
 method ExampleWithSplits() returns (y: int)
   ensures y >= 0

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerificationLogger.dfy

@@ -1,9 +1,9 @@
 // RUN: %exits-with 4 %baredafny measure-complexity --iterations=3 --random-seed=1 --log-format:trx";"LogFileName="%t.trx" "%s"
 // RUN: %OutputCheck --file-to-check "%t.trx" "%s"
 
-// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\) .*\>
-// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\) .*\>
-// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\) .*\>
+// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\).*\>
+// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\).*\>
+// CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\).*\>
 
 method ExampleWithSplits() returns (y: int)
   ensures y >= 0