From e5363ef4490eec77b59056f5c0654923c6b2c789 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 4 Oct 2023 03:51:39 -0700 Subject: [PATCH] Fix spurious vacuity warnings when assertions converted to assumptions (#4604) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Some assertions are translated into assumptions in specific contexts. Before this change, if those assertions were unused in the proof, Dafny would warn that they may have been proved vacuously. Now it doesn’t. It also skips warning about various internal checks that are proved in a context that the user has no control over. Along the way, this also changes the behavior of proof dependency warnings so that they're produced for any definition that successfully verifies, even if some definitions in the program have errors. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --- Source/DafnyCore/ProofDependencyWarnings.cs | 14 ++++++++++++-- Source/DafnyCore/Verifier/ProofDependency.cs | 14 ++++++++++++++ Source/DafnyCore/Verifier/Translator.cs | 3 ++- Source/DafnyDriver/DafnyDriver.cs | 2 +- Test/logger/ProofDependencyLogging.dfy | 7 +++++++ Test/logger/ProofDependencyWarnings.dfy | 2 +- Test/logger/ProofDependencyWarnings.dfy.expect | 2 +- 7 files changed, 38 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 21058e16554..93a0ac5f0d8 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,6 +1,7 @@ using System.Linq; using DafnyCore.Verifier; using Microsoft.Dafny.ProofObligationDescription; +using VC; namespace Microsoft.Dafny; @@ -16,6 +17,10 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er } public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) { + if (result.Outcome != ConditionGeneration.Outcome.Correct) { + return; + } + var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(logEntry.Name); var usedDependencies = result @@ -81,8 +86,13 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName, return false; } - // Similarly here - if (poDep.ProofObligation is MatchIsComplete or AlternativeIsComplete) { + // Some proof obligations occur in a context that the Dafny programmer + // doesn't have control of, so warning about vacuity isn't helpful. + if (poDep.ProofObligation + is MatchIsComplete + or AlternativeIsComplete + or ValidInRecursion + or TraitDecreases) { return false; } diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index f3a0ebc4b79..b91f08ef1d0 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -66,6 +66,20 @@ public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription p } } +public class AssumedProofObligationDependency : ProofDependency { + public override RangeToken Range { get; } + + public PODesc.ProofObligationDescription ProofObligation { get; } + + public override string Description => + $"assumption that {ProofObligation.SuccessDescription}"; + + public AssumedProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) { + Range = tok as RangeToken ?? new RangeToken(tok, tok); + ProofObligation = proofObligation; + } +} + // Represents the assumption of a requires clause in the process of // proving a Dafny definition. public class RequiresDependency : ProofDependency { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 9d892041e5f..12d8d86f1b4 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -7491,10 +7491,11 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce an assume instead cmd = TrAssumeCmd(tok, condition, kv); + proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, description)); } else { cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv); + proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); } - proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); return cmd; } diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 56010751eea..f052bdd336b 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -468,7 +468,7 @@ private async Task ProcessFilesAsync(IReadOnlyList/*! string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); var (verified, outcome, moduleStats) = await BoogieAsync(options, baseName, boogiePrograms, programId); - if (options.TrackVerificationCoverage && verified) { + if (options.TrackVerificationCoverage) { ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager); } diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy index 637c372b069..522dee90705 100644 --- a/Test/logger/ProofDependencyLogging.dfy +++ b/Test/logger/ProofDependencyLogging.dfy @@ -423,6 +423,13 @@ method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int) return 1; // unreachable } +method CalcStatementWithSideConditions(x: int) { + calc == { + x / 2; + (x*2) / 4; + } +} + method DontWarnAboutVacuousAssertFalse(x: int) { assume x == x + 1; assert false; diff --git a/Test/logger/ProofDependencyWarnings.dfy b/Test/logger/ProofDependencyWarnings.dfy index 7f61c0aac3a..419b325cf41 100644 --- a/Test/logger/ProofDependencyWarnings.dfy +++ b/Test/logger/ProofDependencyWarnings.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t" +// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t" // RUN: %diff "%t" "%s.expect" include "ProofDependencyLogging.dfy" diff --git a/Test/logger/ProofDependencyWarnings.dfy.expect b/Test/logger/ProofDependencyWarnings.dfy.expect index 6fdf6aae938..a433ec699ec 100644 --- a/Test/logger/ProofDependencyWarnings.dfy.expect +++ b/Test/logger/ProofDependencyWarnings.dfy.expect @@ -17,4 +17,4 @@ ProofDependencyLogging.dfy(346,10): Warning: ensures clause proved using contrad ProofDependencyLogging.dfy(354,11): Warning: unnecessary requires clause ProofDependencyLogging.dfy(363,9): Warning: unnecessary assumption -Dafny program verifier finished with 29 verified, 0 errors +Dafny program verifier finished with 30 verified, 0 errors