Support logging verification results in JSON (#4951)

### Description

Implement support for `dafny verify --log-format json` to log the
information provided in the `text` format logger in JSON format.

Fixes #4907

### How has this been tested?

`logger/JsonLogger.dfy`

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

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,12 @@ 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.Range)
+ .ThenBy(dep => 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/CoverageReport.dfy

@@ -2,23 +2,23 @@
 // Verification coverage:
 // RUN: rm -rf "%t"/coverage_verification
 // RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --verification-coverage-report "%t/coverage_verification" %s
-// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_verification/ProofDependencyLogging.dfy_verification.html > "%t"/coverage_verification_actual.html
-// RUN: %diff "%S/ProofDependencyLogging.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_verification/ProofDependencies.dfy_verification.html > "%t"/coverage_verification_actual.html
+// RUN: %diff "%S/ProofDependencies.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
 // Expected test coverage:
 // RUN: rm -rf "%t"/coverage_testing
 // RUN: %baredafny generate-tests Block --no-timestamp-for-coverage-report --coverage-report "%t/coverage_testing" %s
-// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencyLogging.dfy_tests_expected.html > "%t"/coverage_testing_actual.html
-// RUN: %diff "%S/ProofDependencyLogging.dfy_tests_expected.html.expect" "%t/coverage_testing_actual.html"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencies.dfy_tests_expected.html > "%t"/coverage_testing_actual.html
+// RUN: %diff "%S/ProofDependencies.dfy_tests_expected.html.expect" "%t/coverage_testing_actual.html"
 // Combined coverage:
 // RUN: rm -rf "%t"/coverage_combined
 // RUN: %baredafny merge-coverage-reports --no-timestamp-for-coverage-report "%t"/coverage_combined "%t"/coverage_testing "%t"/coverage_verification
-// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined.html
-// RUN: %diff "%S/ProofDependencyLogging.dfy_combined.html.expect" "%t/coverage_combined.html"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined/ProofDependencies.dfy_combined.html > "%t"/coverage_combined.html
+// RUN: %diff "%S/ProofDependencies.dfy_combined.html.expect" "%t/coverage_combined.html"
 // Combined, limited coverage:
 // RUN: rm -rf "%t"/coverage_combined
 // RUN: %baredafny merge-coverage-reports --only-label NotCovered --no-timestamp-for-coverage-report "%t"/coverage_combined_limited "%t"/coverage_testing "%t"/coverage_verification
-// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencyLogging.dfy_combined.html > "%t"/coverage_combined_limited.html
-// RUN: %diff "%S/ProofDependencyLogging.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
+// RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_combined_limited/ProofDependencies.dfy_combined.html > "%t"/coverage_combined_limited.html
+// RUN: %diff "%S/ProofDependencies.dfy_combined_limited.html.expect" "%t/coverage_combined_limited.html"
 
 
-include "ProofDependencyLogging.dfy"
+include "ProofDependencies.dfy"

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