Support logging verification results in JSON

Source/DafnyCore/DafnyOptions.cs

@@ -722,7 +722,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
 
         case "verificationLogger":
           if (ps.ConfirmArgumentCount(1)) {
-            if (args[ps.i].StartsWith("trx") || args[ps.i].StartsWith("csv") || args[ps.i].StartsWith("text")) {
+            if (args[ps.i].StartsWith("trx") || args[ps.i].StartsWith("csv") || args[ps.i].StartsWith("text") || args[ps.i].StartsWith("json")) {
               VerificationLoggerConfigs.Add(args[ps.i]);
             } else {
               InvalidArgumentError(name, ps);

Source/DafnyCore/Verifier/ProofDependencyManager.cs

@@ -83,5 +83,9 @@ public ProofDependency GetFullIdDependency(TrackedNodeComponent component) {
         throw new ArgumentException($"Malformed dependency ID: {component.SolverLabel}");
       }
     }
+
+    public IEnumerable<ProofDependency> GetOrderedFullDependencies(IEnumerable<TrackedNodeComponent> components) {
+      return components.Select(GetFullIdDependency).OrderBy(dep => (dep.RangeString(), dep.Description));
+    }
   }
 }

Source/DafnyDriver/JsonVerificationLogger.cs

@@ -0,0 +1,106 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Text.Json.Nodes;
+using DafnyCore.Verifier;
+using Microsoft.Boogie;
+using VC;
+
+namespace Microsoft.Dafny;
+
+public class JsonVerificationLogger {
+  private TextWriter tw;
+  private readonly TextWriter outWriter;
+  private readonly ProofDependencyManager depManager;
+
+  public JsonVerificationLogger(ProofDependencyManager depManager, TextWriter outWriter) {
+    this.depManager = depManager;
+    this.outWriter = outWriter;
+  }
+
+  public void Initialize(Dictionary<string, string> parameters) {
+    tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : outWriter;
+  }
+
+  private static JsonNode SerializeAssertion(Microsoft.Boogie.IToken tok, string description) {
+    return new JsonObject {
+      ["filename"] = tok.filename,
+      ["line"] = tok.line,
+      ["col"] = tok.col,
+      ["description"] = description
+    };
+  }
+
+  private JsonNode SerializeProofDependency(ProofDependency dependency) {
+    return new JsonObject {
+      ["startFile"] = dependency.Range.StartToken.Filepath,
+      ["startLine"] = dependency.Range.StartToken.line,
+      ["startCol"] = dependency.Range.StartToken.col,
+      ["endFile"] = dependency.Range.EndToken.Filepath,
+      ["endLine"] = dependency.Range.EndToken.line,
+      ["endCol"] = dependency.Range.EndToken.col,
+      ["description"] = dependency.Description,
+      ["originalText"] = dependency.OriginalString()
+    };
+  }
+
+  private JsonNode SerializeVcResult(IEnumerable<ProofDependency> potentialDependencies, DafnyConsolePrinter.VCResultLogEntry vcResult) {
+    var result = new JsonObject {
+      ["vcNum"] = vcResult.VCNum,
+      ["outcome"] = SerializeOutcome(vcResult.Outcome),
+      ["runTime"] = SerializeTimeSpan(vcResult.RunTime),
+      ["resourceCount"] = vcResult.ResourceCount,
+      ["assertions"] = new JsonArray(vcResult.Asserts.Select(x => SerializeAssertion(x.Tok, x.Description)).ToArray()),
+    };
+    if (potentialDependencies is not null) {
+      var fullDependencies = depManager.GetOrderedFullDependencies(vcResult.CoveredElements);
+      var fullDependencySet = fullDependencies.ToHashSet();
+      var unusedDependencies = potentialDependencies.Where(dep => !fullDependencySet.Contains(dep));
+      result["coveredElements"] = new JsonArray(fullDependencies.Select(SerializeProofDependency).ToArray());
+      result["uncoveredElements"] = new JsonArray(unusedDependencies.Select(SerializeProofDependency).ToArray());
+    }
+    return result;
+  }
+
+  private static JsonNode SerializeTimeSpan(TimeSpan timeSpan) {
+    return timeSpan.ToString();
+  }
+
+  private static JsonNode SerializeOutcome(ProverInterface.Outcome outcome) {
+    return outcome.ToString();
+  }
+  private static JsonNode SerializeOutcome(ConditionGeneration.Outcome outcome) {
+    return outcome.ToString();
+  }
+
+  private JsonNode SerializeVerificationResult(DafnyConsolePrinter.ConsoleLogEntry logEntry) {
+    var (impl, verificationResult) = logEntry;
+    var trackProofDependencies =
+      verificationResult.Outcome == ConditionGeneration.Outcome.Correct &&
+      verificationResult.VCResults.Any(vcResult => vcResult.CoveredElements.Any());
+    var potentialDependencies =
+      trackProofDependencies ? depManager.GetPotentialDependenciesForDefinition(impl.Name) : null;
+    var result = new JsonObject {
+      ["name"] = impl.Name,
+      ["outcome"] = SerializeOutcome(verificationResult.Outcome),
+      ["runTime"] = SerializeTimeSpan(verificationResult.RunTime),
+      ["resourceCount"] = verificationResult.ResourceCount,
+      ["vcResults"] = new JsonArray(verificationResult.VCResults.Select(r => SerializeVcResult(potentialDependencies, r)).ToArray())
+    };
+    if (potentialDependencies is not null) {
+      result["programElements"] = new JsonArray(potentialDependencies.Select(SerializeProofDependency).ToArray());
+    }
+    return result;
+  }
+
+  private JsonObject SerializeVerificationResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verificationResults) {
+    return new JsonObject {
+      ["verificationResults"] = new JsonArray(verificationResults.Select(SerializeVerificationResult).ToArray())
+    };
+  }
+
+  public void LogResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verificationResults) {
+    tw.Write(SerializeVerificationResults(verificationResults).ToJsonString());
+  }
+}

Source/DafnyDriver/TextLogger.cs → Source/DafnyDriver/TextVerificationLogger.cs

@@ -5,12 +5,12 @@
 
 namespace Microsoft.Dafny;
 
-public class TextLogger {
+public class TextVerificationLogger {
   private TextWriter tw;
   private TextWriter outWriter;
   private ProofDependencyManager depManager;
 
-  public TextLogger(ProofDependencyManager depManager, TextWriter outWriter) {
+  public TextVerificationLogger(ProofDependencyManager depManager, TextWriter outWriter) {
     this.depManager = depManager;
     this.outWriter = outWriter;
   }
@@ -47,11 +47,7 @@ public void LogResults(IEnumerable<DafnyConsolePrinter.ConsoleLogEntry> verifica
         if (vcResult.CoveredElements.Any() && vcResult.Outcome == ProverInterface.Outcome.Valid) {
           tw.WriteLine("");
           tw.WriteLine("    Proof dependencies:");
-          var fullDependencies =
-            vcResult
-            .CoveredElements
-            .Select(depManager.GetFullIdDependency)
-            .OrderBy(dep => (dep.RangeString(), dep.Description));
+          var fullDependencies = depManager.GetOrderedFullDependencies(vcResult.CoveredElements);
           foreach (var dep in fullDependencies) {
             tw.WriteLine($"      {dep.RangeString()}: {dep.Description}");
           }

Source/DafnyDriver/VerificationResultLogger.cs

@@ -59,10 +59,16 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
         } else if (loggerName == "csv") {
           var csvLogger = new CSVTestLogger(options.OutputWriter);
           csvLogger.Initialize(events, parameters);
+        } else if (loggerName == "json") {
+          // This logger doesn't implement the ITestLogger interface because
+          // it uses information that's tricky to encode in a TestResult.
+          var jsonLogger = new JsonVerificationLogger(depManager, options.OutputWriter);
+          jsonLogger.Initialize(parameters);
+          jsonLogger.LogResults(verificationResults);
         } else if (loggerName == "text") {
           // This logger doesn't implement the ITestLogger interface because
           // it uses information that's tricky to encode in a TestResult.
-          var textLogger = new TextLogger(depManager, options.OutputWriter);
+          var textLogger = new TextVerificationLogger(depManager, options.OutputWriter);
           textLogger.Initialize(parameters);
           textLogger.LogResults(verificationResults);
         } else {

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

@@ -0,0 +1,10 @@
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:json --isolate-assertions "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid
+method M(x: int, y: int)
+  requires y > 0
+  requires x > 0
+{
+  var d := x / y;
+  assert(d * y == x); // Should fail
+}