Add first pass of proof obligation description expressions (#5317)

### Description
Adds a first pass of proof obligation description expressions, towards
resolving #2987. It also adds
a new hidden option, `--show-proof-obligation-expressions`, which adds
to each (supported) failed proof obligation error message an equivalent
Dafny assertion. This option is used to automate tests for the newly
added proof obligation description expressions, but this PR does not
backfill tests for existing PODesc expressions.

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

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>

Source/DafnyCore/DafnyOptions.cs

@@ -380,6 +380,8 @@ public enum IncludesModes {
  [CanBeNull] private TestGenerationOptions testGenOptions = null;
  public bool ExtractCounterexample = false;
 
+ public bool ShowProofObligationExpressions = false;
+
  public bool AuditProgram = false;
 
  public static string DefaultZ3Version = "4.12.1";
@@ -796,6 +798,10 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
  EnhancedErrorMessages = 1;
  return true;
 
+ case "showProofObligationExpressions":
+ ShowProofObligationExpressions = true;
+ return true;
+
  case "testContracts":
  if (ps.ConfirmArgumentCount(1)) {
  if (args[ps.i].Equals("Externs")) {

Source/DafnyCore/Generic/ReporterExtensions.cs

@@ -11,7 +11,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
  var usingSnippets = reporter.Options.Get(Snippets.ShowSnippets);
  var relatedInformation = new List<DafnyRelatedInformation>();
  foreach (var auxiliaryInformation in error.Aux) {
- if (auxiliaryInformation.Category == RelatedMessageCategory) {
+ if (auxiliaryInformation.Category == RelatedMessageCategory || auxiliaryInformation.Category == AssertedExprCategory) {
  error.Msg += "\n" + auxiliaryInformation.FullMsg;
  } else if (auxiliaryInformation.Category == RelatedLocationCategory) {
  relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets));
@@ -46,6 +46,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
  private const string RelatedLocationCategory = "Related location";
  public const string RelatedLocationMessage = RelatedLocationCategory;
  private const string RelatedMessageCategory = "Related message";
+ public const string AssertedExprCategory = "Asserted expression";
  public static readonly string PostConditionFailingMessage = new ProofObligationDescription.EnsuresDescription(null, null).FailureDescription;
  private static string FormatRelated(string related) {
  return $"Could not prove: {related}";

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -359,6 +359,12 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis
 If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) {
  };
 
+ public static readonly Option<bool> ShowProofObligationExpressions = new("--show-proof-obligation-expressions", () => false,
+ @"
+(Experimental) Show Dafny expressions corresponding to unverified proof obligations.".TrimStart()) {
+ IsHidden = true
+ };
+
  static CommonOptionBag() {
  DafnyOptions.RegisterLegacyBinding(WarnAsErrors, (options, value) => {
  if (!options.Get(AllowWarnings) && !options.Get(WarnAsErrors)) {
@@ -571,6 +577,10 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
  options.EnhancedErrorMessages = 1;
  });
 
+ DafnyOptions.RegisterLegacyBinding(ShowProofObligationExpressions, (options, value) => {
+ options.ShowProofObligationExpressions = value;
+ });
+
  DooFile.RegisterLibraryChecks(
  new Dictionary<Option, DooFile.OptionCheck>() {
  { UnicodeCharacters, DooFile.CheckOptionMatches },
@@ -635,7 +645,8 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
  AddCompileSuffix,
  SystemModule,
  ExecutionCoverageReport,
- ExtractCounterexample
+ ExtractCounterexample,
+ ShowProofObligationExpressions
  );
  }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -48,7 +48,8 @@ static DafnyCommands() {
  CommonOptionBag.NoTimeStampForCoverageReport,
  CommonOptionBag.VerificationCoverageReport,
  CommonOptionBag.ExtractCounterexample,
- CommonOptionBag.ManualTriggerOption
+ CommonOptionBag.ManualTriggerOption,
+ CommonOptionBag.ShowProofObligationExpressions
  }.ToList();
 
  public static IReadOnlyList<Option> TranslationOptions = new Option[] {

Source/DafnyCore/Pipeline/Compilation.cs

@@ -14,6 +14,7 @@
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using VC;
+using VCGeneration;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny;
@@ -518,6 +519,9 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
  foreach (var counterExample in result.CounterExamples) //.OrderBy(d => d.GetLocation()))
  {
  var errorInformation = counterExample.CreateErrorInformation(outcome, options.ForceBplErrors);
+ if (options.ShowProofObligationExpressions) {
+ AddAssertedExprToCounterExampleErrorInfo(options, counterExample, errorInformation);
+ }
  var dafnyCounterExampleModel = options.ExtractCounterexample ? new DafnyModel(counterExample.Model, options) : null;
  errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel);
  }
@@ -531,6 +535,40 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
  timeLimit, result.CounterExamples);
  }
 
+ private static void AddAssertedExprToCounterExampleErrorInfo(
+ DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
+ Boogie.ProofObligationDescription? boogieProofObligationDesc = null;
+ switch (errorInformation.Kind) {
+ case ErrorKind.Assertion:
+ boogieProofObligationDesc = ((AssertCounterexample)counterExample).FailingAssert.Description;
+ break;
+ case ErrorKind.Precondition:
+ boogieProofObligationDesc = ((CallCounterexample)counterExample).FailingCall.Description;
+ break;
+ case ErrorKind.Postcondition:
+ boogieProofObligationDesc = ((ReturnCounterexample)counterExample).FailingReturn.Description;
+ break;
+ case ErrorKind.InvariantEntry:
+ case ErrorKind.InvariantMaintainance:
+ AssertCmd failingAssert = ((AssertCounterexample)counterExample).FailingAssert;
+ if (failingAssert is LoopInitAssertCmd loopInitAssertCmd) {
+ boogieProofObligationDesc = loopInitAssertCmd.originalAssert.Description;
+ } else if (failingAssert is LoopInvMaintainedAssertCmd maintainedAssertCmd) {
+ boogieProofObligationDesc = maintainedAssertCmd.originalAssert.Description;
+ }
+ break;
+ default:
+ throw new ArgumentOutOfRangeException($"Unexpected ErrorKind: {errorInformation.Kind}");
+ }
+
+ if (boogieProofObligationDesc is ProofObligationDescription.ProofObligationDescription dafnyProofObligationDesc) {
+ var expr = dafnyProofObligationDesc.GetAssertedExpr(options);
+ if (expr != null) {
+ errorInformation.AddAuxInfo(errorInformation.Tok, expr.ToString(), ErrorReporterExtensions.AssertedExprCategory);
+ }
+ }
+ }
+
  public static VcOutcome GetOutcome(SolverOutcome outcome) {
  switch (outcome) {
  case SolverOutcome.Valid: