Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…

…ardDrummer/dafny into supportAllOptionTypesInProjectFile

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -6,6 +6,7 @@
 using System.Linq;
 using DafnyCore;
 using Microsoft.Boogie;
+using VC;
 
 namespace Microsoft.Dafny;
 
@@ -20,7 +21,24 @@ public class DafnyConsolePrinter : ConsolePrinter {
 
  private readonly ConcurrentDictionary<string, List<string>> fsCache = new();
  private DafnyOptions options;
- public ConcurrentBag<(Implementation, VerificationResult)> VerificationResults { get; } = new();
+
+ public record ImplementationLogEntry(string Name, Boogie.IToken Tok);
+ public record VCResultLogEntry(
+ int VCNum,
+ DateTime StartTime,
+ TimeSpan RunTime,
+ ProverInterface.Outcome Outcome,
+ List<(Boogie.IToken Tok, string Description)> Asserts,
+ IEnumerable<TrackedNodeComponent> CoveredElements,
+ int ResourceCount);
+ public record VerificationResultLogEntry(
+ ConditionGeneration.Outcome Outcome,
+ TimeSpan RunTime,
+ int ResourceCount,
+ List<VCResultLogEntry> VCResults);
+ public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);
+
+ public ConcurrentBag<ConsoleLogEntry> VerificationResults { get; } = new();
 
  public override void AdvisoryWriteLine(TextWriter output, string format, params object[] args) {
  if (output == Console.Out) {
@@ -115,7 +133,12 @@ public class DafnyConsolePrinter : ConsolePrinter {
  }
  }
 
- public override void ReportEndVerifyImplementation(Implementation implementation, Boogie.VerificationResult result) {
- VerificationResults.Add((implementation, result));
+ public override void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
+ var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok);
+ var vcResults = result.VCResults.Select(r =>
+ new VCResultLogEntry(r.vcNum, r.startTime, r.runTime, r.outcome, r.asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.coveredElements, r.resourceCount)
+ ).ToList();
+ var res = new VerificationResultLogEntry(result.Outcome, result.End - result.Start, result.ResourceCount, vcResults);
+ VerificationResults.Add(new ConsoleLogEntry(impl, res));
  }
 }

Source/DafnyDriver/TextLogger.cs

@@ -1,8 +1,6 @@
-using System;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 
@@ -20,40 +18,36 @@ public class TextLogger {
  tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : outWriter;
  }
 
- public void LogResults(List<(Implementation, VerificationResult)> verificationResults) {
- var orderedResults =
- verificationResults.OrderBy(vr =>
- (vr.Item1.tok.filename, vr.Item1.tok.line, vr.Item1.tok.col));
- foreach (var (implementation, result) in orderedResults) {
+ 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))) {
  tw.WriteLine("");
- tw.WriteLine($"Results for {implementation.VerboseName}");
+ tw.WriteLine($"Results for {implementation.Name}");
  tw.WriteLine($" Overall outcome: {result.Outcome}");
- tw.WriteLine($" Overall time: {result.End - result.Start}");
+ tw.WriteLine($" Overall time: {result.RunTime}");
  tw.WriteLine($" Overall resource count: {result.ResourceCount}");
  // It doesn't seem possible to get a result with zero VCResults, but being careful with nulls just in case :)
- var maximumTime = result.VCResults.MaxBy(r => r.runTime)?.runTime.ToString() ?? "N/A";
- var maximumRC = result.VCResults.MaxBy(r => r.resourceCount)?.resourceCount.ToString() ?? "N/A";
+ var maximumTime = result.VCResults.MaxBy(r => r.RunTime).RunTime.ToString() ?? "N/A";
+ var maximumRC = result.VCResults.MaxBy(r => r.ResourceCount).ResourceCount.ToString() ?? "N/A";
  tw.WriteLine($" Maximum assertion batch time: {maximumTime}");
  tw.WriteLine($" Maximum assertion batch resource count: {maximumRC}");
- foreach (var vcResult in result.VCResults.OrderBy(r => r.vcNum)) {
+ foreach (var vcResult in result.VCResults.OrderBy(r => r.VCNum)) {
  tw.WriteLine("");
- tw.WriteLine($" Assertion batch {vcResult.vcNum}:");
- tw.WriteLine($" Outcome: {vcResult.outcome}");
- tw.WriteLine($" Duration: {vcResult.runTime}");
- tw.WriteLine($" Resource count: {vcResult.resourceCount}");
+ tw.WriteLine($" Assertion batch {vcResult.VCNum}:");
+ tw.WriteLine($" Outcome: {vcResult.Outcome}");
+ tw.WriteLine($" Duration: {vcResult.RunTime}");
+ tw.WriteLine($" Resource count: {vcResult.ResourceCount}");
  tw.WriteLine("");
  tw.WriteLine(" Assertions:");
- foreach (var cmd in vcResult.asserts) {
+ foreach (var cmd in vcResult.Asserts) {
  tw.WriteLine(
- $" {((IToken)cmd.tok).filename}({cmd.tok.line},{cmd.tok.col}): {cmd.Description.SuccessDescription}");
+ $" {cmd.Tok.filename}({cmd.Tok.line},{cmd.Tok.col}): {cmd.Description}");
  }
-
- if (vcResult.coveredElements.Any()) {
+ if (vcResult.CoveredElements.Any()) {
  tw.WriteLine("");
  tw.WriteLine(" Proof dependencies:");
  var fullDependencies =
  vcResult
- .coveredElements
+ .CoveredElements
  .Select(depManager.GetFullIdDependency)
  .OrderBy(dep => (dep.RangeString(), dep.Description));
  foreach (var dep in fullDependencies) {

Source/DafnyDriver/VerificationResultLogger.cs

@@ -13,7 +13,6 @@
 using Microsoft.VisualStudio.TestPlatform.ObjectModel;
 using Microsoft.VisualStudio.TestPlatform.ObjectModel.Client;
 using Microsoft.VisualStudio.TestPlatform.ObjectModel.Logging;
-using VC;
 
 namespace Microsoft.Dafny {
 
@@ -75,7 +74,7 @@ public static class VerificationResultLogger {
 
  // Sort failures to the top, and then slower procedures first.
  // Loggers may not maintain this ordering unfortunately.
- var results = VerificationToTestResults(verificationResults)
+ var results = VerificationToTestResults(verificationResults.Select(e => (e.Implementation, e.Result.VCResults)))
  .OrderBy(r => r.Outcome == TestOutcome.Passed)
  .ThenByDescending(r => r.Duration);
  foreach (var result in results) {
@@ -88,32 +87,29 @@ public static class VerificationResultLogger {
  ));
  }
 
- private static IEnumerable<TestResult> VerificationToTestResults(List<(Implementation, VerificationResult)> verificationResults) {
+ private static IEnumerable<TestResult> VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List<DafnyConsolePrinter.VCResultLogEntry>)> verificationResults) {
  var testResults = new List<TestResult>();
 
- foreach (var (implementation, result) in verificationResults) {
- var vcResults = result.VCResults.OrderBy(r => r.vcNum);
- var currentFile = ((IToken)implementation.tok).Uri;
- foreach (var vcResult in vcResults) {
- var verbName = implementation.VerboseName;
+ foreach (var ((verbName, currentFile), vcResults) in verificationResults) {
+ foreach (var vcResult in vcResults.OrderBy(r => r.VCNum)) {
  var name = vcResults.Count() > 1
- ? verbName + $" (assertion batch {vcResult.vcNum})"
+ ? verbName + $" (assertion batch {vcResult.VCNum})"
  : verbName;
  var testCase = new TestCase {
  FullyQualifiedName = name,
  ExecutorUri = new Uri("executor:https://dafnyverifier/v1"),
- Source = currentFile.LocalPath
+ Source = ((IToken)currentFile).Uri.LocalPath
  };
  var testResult = new TestResult(testCase) {
- StartTime = vcResult.startTime,
- Duration = vcResult.runTime
+ StartTime = vcResult.StartTime,
+ Duration = vcResult.RunTime
  };
- testResult.SetPropertyValue(ResourceCountProperty, vcResult.resourceCount);
- if (vcResult.outcome == ProverInterface.Outcome.Valid) {
+ testResult.SetPropertyValue(ResourceCountProperty, vcResult.ResourceCount);
+ if (vcResult.Outcome == ProverInterface.Outcome.Valid) {
  testResult.Outcome = TestOutcome.Passed;
  } else {
  testResult.Outcome = TestOutcome.Failed;
- testResult.ErrorMessage = vcResult.outcome.ToString();
+ testResult.ErrorMessage = vcResult.Outcome.ToString();
  }
  testResults.Add(testResult);
  }