From 21b942f55ba6e39eebdf543d2c6d6055ae7ed027 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 08:59:18 +0200 Subject: [PATCH 01/27] bump boogie --- Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Pipeline/Compilation.cs | 3 +-- Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs | 2 +- Source/DafnyTestGeneration/PathBasedModifier.cs | 4 ++-- customBoogie.patch | 2 +- 5 files changed, 6 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index e4bf8fe0ea7..3acc56618f8 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 266c5ee30f8..35a7d58f625 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -3,7 +3,6 @@ using System; using System.Collections.Concurrent; using System.Collections.Generic; -using System.Collections.Immutable; using System.IO; using System.Linq; using System.Reactive; @@ -575,7 +574,7 @@ public static VcOutcome GetOutcome(SolverOutcome outcome) { case SolverOutcome.Undetermined: return VcOutcome.Inconclusive; case SolverOutcome.Bounded: - return VcOutcome.ReachedBound; + return VcOutcome.Inconclusive; default: throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null); } diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 7ae1caf539d..8f46023b75a 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -62,7 +62,7 @@ public async Task> GetVerificationTasksAsync(Ex ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); } - return engine.GetVerificationTasks(boogieProgram); + return await engine.GetVerificationTasks(boogieProgram); } finally { mutex.Release(); diff --git a/Source/DafnyTestGeneration/PathBasedModifier.cs b/Source/DafnyTestGeneration/PathBasedModifier.cs index c8efff85896..84537f894cd 100644 --- a/Source/DafnyTestGeneration/PathBasedModifier.cs +++ b/Source/DafnyTestGeneration/PathBasedModifier.cs @@ -116,13 +116,13 @@ private IEnumerable GeneratePaths(Implementation impl, int minPathLength, yield return new Path(impl, currPathVariables.ToList(), new() { block }, currPath.Append(block).ToList()); } else { - if (currPath.Count != 0 && ((GotoCmd)currPath.Last().TransferCmd).labelTargets.Count != 1) { + if (currPath.Count != 0 && ((GotoCmd)currPath.Last().TransferCmd).LabelTargets.Count != 1) { currPathVariables.Add(blockToVariable[block]); // only constrain the path if there is more than one goto } currPath.Add(block); otherGotos.Add(new List()); var gotoCmd = block.TransferCmd as GotoCmd; - foreach (var nextBlock in gotoCmd?.labelTargets ?? new List()) { + foreach (var nextBlock in gotoCmd?.LabelTargets ?? new List()) { if (currPathVariables.Contains(blockToVariable[nextBlock])) { // this prevents cycles continue; } diff --git a/customBoogie.patch b/customBoogie.patch index 3f1b02ac97e..1c73d305526 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + From 6651bdd4467508f154094c76d35528c9567bcc62 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 09:02:14 +0200 Subject: [PATCH 02/27] implemantation --- Source/DafnyCore/DafnyConsolePrinter.cs | 17 +- Source/DafnyCore/Options/CommonOptionBag.cs | 10 + Source/DafnyCore/Options/DafnyCommands.cs | 1 + Source/DafnyCore/ProofDependencyWarnings.cs | 182 +++++++++++++++++- .../Verifier/BoogieGenerator.Fields.cs | 2 +- .../Verifier/BoogieGenerator.Functions.cs | 11 +- .../Verifier/BoogieGenerator.Iterators.cs | 6 +- .../Verifier/BoogieGenerator.Methods.cs | 8 +- .../Verifier/BoogieGenerator.Types.cs | 2 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- Source/DafnyCore/Verifier/ProofDependency.cs | 8 +- .../Verifier/ProofDependencyManager.cs | 24 +-- .../Legacy/LegacyJsonVerificationLogger.cs | 2 +- 13 files changed, 238 insertions(+), 37 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index f49ee90c118..b3f75eac13f 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -26,8 +26,9 @@ public record VCResultLogEntry( DateTime StartTime, TimeSpan RunTime, SolverOutcome Outcome, - List<(Boogie.IToken Tok, string Description)> Asserts, + List<(Boogie.IToken Tok, string Description, string Id)> Asserts, IEnumerable CoveredElements, + IEnumerable AvailableAxioms, int ResourceCount); public record VerificationResultLogEntry( VcOutcome Outcome, @@ -43,10 +44,18 @@ public static VerificationResultLogEntry DistillVerificationResult(Implementatio verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors); } - private static VCResultLogEntry DistillVCResult(VerificationRunResult r) { + public static VCResultLogEntry DistillVCResult(VerificationRunResult r) { return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome, - r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.CoveredElements, - r.ResourceCount); + r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription, GetId(a))).ToList(), r.CoveredElements, + r.DeclarationsAfterPruning.OfType(), r.ResourceCount); + + string GetId(ICarriesAttributes construct) { + var values = construct.FindAllAttributes("id"); + if (!values.Any()) { + throw new ArgumentException($"No dependency ID in assertion"); + } + return (string)values.Last().Params.First(); + } } public ConcurrentBag VerificationResults { get; } = new(); diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 0c0ea425ff5..9585cb3fc85 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -280,6 +280,11 @@ May produce spurious warnings. May produce spurious warnings.") { IsHidden = true }; + public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", @" +(experimental) Emits suggestions for moving assertions into by-proofs and hiding unused function definitions. +May produce spurious suggestions. Use with --show-hints on the CLI.") { + IsHidden = true + }; public static readonly Option VerificationCoverageReport = new("--verification-coverage-report", "Emit verification coverage report to a given directory, in the same format as a test coverage report.") { ArgumentHelpName = "directory" @@ -453,6 +458,7 @@ statements in implementation methods. It also disables anything DafnyOptions.RegisterLegacyUi(WarnContradictoryAssumptions, DafnyOptions.ParseImplicitEnable, "Verification options", "warnContradictoryAssumptions"); DafnyOptions.RegisterLegacyUi(WarnRedundantAssumptions, DafnyOptions.ParseImplicitEnable, "Verification options", "warnRedundantAssumptions"); + DafnyOptions.RegisterLegacyUi(SuggestProofRefactoring, DafnyOptions.ParseImplicitEnable, "Verification options", "suggestProofRefactoring"); void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, DafnyOptions options) { if (ps.ConfirmArgumentCount(1)) { @@ -506,6 +512,9 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, DafnyOptions.RegisterLegacyBinding(WarnRedundantAssumptions, (options, value) => { if (value) { options.TrackVerificationCoverage = true; } }); + DafnyOptions.RegisterLegacyBinding(SuggestProofRefactoring, (options, value) => { + if (value) { options.TrackVerificationCoverage = true; } + }); DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; }); @@ -605,6 +614,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptionRegistry.RegisterOption(InternalIncludeRuntimeOptionForExecution, OptionScope.Cli); OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module); + OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module); OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module); diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 033c02f71e1..d901d9700e6 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -41,6 +41,7 @@ static DafnyCommands() { CommonOptionBag.DefaultFunctionOpacity, CommonOptionBag.WarnContradictoryAssumptions, CommonOptionBag.WarnRedundantAssumptions, + CommonOptionBag.SuggestProofRefactoring, CommonOptionBag.NoTimeStampForCoverageReport, CommonOptionBag.VerificationCoverageReport, CommonOptionBag.ExtractCounterexample, diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 319302df28f..58be42baafb 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,9 +1,9 @@ -using System.Collections.Concurrent; using System.Collections.Generic; using System.Linq; using DafnyCore.Verifier; using Microsoft.Boogie; using Microsoft.Dafny.ProofObligationDescription; +using Microsoft.Dafny.Triggers; using VC; namespace Microsoft.Dafny; @@ -34,7 +34,9 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er if (result.Outcome != VcOutcome.Correct) { continue; } - Warn(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements)); + var assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(e.Asserts))).ToList(); + var unusedFunctions = UnusedFunctions(depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); + Warn(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions); } } @@ -44,15 +46,93 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } + var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))).ToList(); + var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(tp.Item2.Asserts))).ToList(); + var unusedFunctions = UnusedFunctions(depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); + Warn(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); + } + + private static List UnusedFunctions(ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { + var unusedFunctions = new List(); + if (depManager.idsByMemberName[name].Decl is Method m) { + var referencedFunctions = ReferencedFunctions(m); + + var hiddenFunctions = HiddenFunctions(referencedFunctions); + + var usedFunctions = coveredElements.Select(depManager.GetFullIdDependency).OfType() + .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); + + unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); + + HashSet ReferencedFunctions(Method method) { + var fCEsinM = method.Body.AllSubExpressions(false, false).OfType(); + var fToDeps = new Dictionary>(); + + foreach (var fce in fCEsinM) { + var fun = fce.Function; + if (!fToDeps.ContainsKey(fun)) { + fToDeps[fun] = Dependents(fun); + } + + continue; + + IEnumerable Dependents(Function fn) { + var queue = new Queue(new[] { fn }); + var visited = new HashSet(); + while (queue.Any()) { + var f = queue.Dequeue(); + visited.Add(f); + + f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); + continue; + + IEnumerable AllSubFunctions(Expression e) { + return e.SubExpressions.OfType().Select(fce => fce.Function) + .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); + } + } + return visited.ToList(); + } + } + + var hashSet = new HashSet(); + foreach (var (f, deps) in fToDeps) { + hashSet.Add(f); + hashSet.UnionWith(deps); + } + + return hashSet; + } + + HashSet HiddenFunctions(HashSet functions) { + var hiddenFunctions = new HashSet(functions); - var coveredElements = results.SelectMany(r => r.CoveredElements); + foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { + hiddenFunctions.Remove(visibleFunction); + } + + return hiddenFunctions; - Warn(dafnyOptions, reporter, depManager, name, coveredElements); + Function GetFunctionFromAttributed(ICarriesAttributes construct) { + var values = construct.FindAllAttributes("id"); + if (!values.Any()) { + return null; + } + var id = (string)values.Last().Params.First(); + if (depManager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) { + return fdd.function; + } + return null; + } + } + } + return unusedFunctions; } private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, IEnumerable coveredElements) { + string scopeName, List<(IEnumerable CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage, List unusedFunctions) { var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); + var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = coveredElements .Select(depManager.GetFullIdDependency) @@ -97,6 +177,98 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo } } } + + if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) { + // Function hiding suggestion + if (unusedFunctions.Any()) { + reporter.Info(MessageSource.Verifier, m.Body.StartToken, + $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); + } + + SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage); + } + } + + private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDependencyManager depManager, + string scopeName, List<(IEnumerable CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage) { + var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet<(Boogie.IToken Tok, string Description, string Id)> { }); + + foreach (var (usedFacts, asserts) in assertCoverage) { + foreach (var fact in usedFacts) { + var dep = depManager.GetFullIdDependency(fact); + _ = dep is not EnsuresDependency && + dependencyTracker.TryAdd(dep, new HashSet<(Boogie.IToken Tok, string Description, string Id)>()); + if (dependencyTracker.ContainsKey(dep)) { + dependencyTracker[dep].UnionWith(asserts); + } + } + } + + foreach (var (dep, lAsserts) in dependencyTracker) { + foreach (var cmd in lAsserts) { + if (depManager.ProofDependenciesById.TryGetValue(cmd.Id, out var cmdDep)) { + if (dep == cmdDep || dep is CallRequiresDependency req && req.call == cmdDep) { + lAsserts.Remove(cmd); + } + } + } + } + + foreach (var (dep, lAsserts) in dependencyTracker) { + if (lAsserts.Count != 1) { + continue; + } + var en = lAsserts.GetEnumerator(); + if (!en.MoveNext()) { + continue; + } + + var cmd = en.Current; + depManager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer); + + if (consumer != null && (dep == consumer || consumer.Range.Intersects(dep.Range))) { + continue; + } + + RangeToken range = null; + var factProvider = ""; + var factConsumer = ""; + var recomendation = ""; + var completeInformation = true; + + switch (dep) { + case AssumptionDependency: { + range = dep.Range; + factProvider = "fact"; + recomendation = "moving it into"; + break; + } + case RequiresDependency: { + range = dep.Range; + factProvider = "requires clause"; + recomendation = "labelling it and revealing it in"; + break; + } + default: completeInformation = false; break; + } + + switch (consumer) { + case CallDependency call: { + factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.RangeString()}"; + break; + } + case ProofObligationDependency { ProofObligation: AssertStatementDescription }: { + factConsumer = $"assertion {consumer.RangeString()}"; + break; + } + default: completeInformation = false; break; + } + + if (completeInformation) { + reporter.Info(MessageSource.Verifier, range, + $"This {factProvider} was only used to prove the {factConsumer}. Consider {recomendation} a by-proof."); + } + } } /// diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 85eaa55d109..bee2cde6ffd 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -155,7 +155,7 @@ void AddWellformednessCheck(ConstantField decl) { Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); - proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness), null); if (!InVerificationScope(decl)) { // Checked in other file return; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 41058d9ba78..1fc6d898337 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -22,7 +22,7 @@ void AddWellformednessCheck(Function f) { Contract.Assert(InVerificationScope(f)); - proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.SpecWellformedness)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.SpecWellformedness), f); currentModule = f.EnclosingClass.EnclosingModuleDefinition; codeContext = f; @@ -927,9 +927,16 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { } else { comment += " (opaque)"; } - return new Axiom(f.tok, BplImp(activate, ax), comment) { + var axe = new Axiom(f.tok, BplImp(activate, ax), comment) { CanHide = true }; + if (proofDependencies == null) { + return axe; + } + + proofDependencies.SetCurrentDefinition(f.FullSanitizedName, f); + proofDependencies.AddProofDependencyId(axe, f.tok, new FunctionDefinitionDependency(f)); + return axe; } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index 6ba4aef2c77..8e5c969caad 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -65,7 +65,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { Contract.Ensures(currentModule == null && codeContext == null); Contract.Ensures(Contract.Result() != null); - proofDependencies.SetCurrentDefinition(MethodVerboseName(iter.FullDafnyName, kind)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(iter.FullDafnyName, kind), iter); currentModule = iter.EnclosingModuleDefinition; codeContext = iter; @@ -137,7 +137,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { Contract.Requires(currentModule == null && codeContext == null); Contract.Ensures(currentModule == null && codeContext == null); - proofDependencies.SetCurrentDefinition(proc.VerboseName); + proofDependencies.SetCurrentDefinition(proc.VerboseName, iter); currentModule = iter.EnclosingModuleDefinition; codeContext = iter; @@ -271,7 +271,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0); Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0); - proofDependencies.SetCurrentDefinition(proc.VerboseName); + proofDependencies.SetCurrentDefinition(proc.VerboseName, iter); currentModule = iter.EnclosingModuleDefinition; codeContext = iter; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index b50c0d48353..91d8cac898f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -534,7 +534,7 @@ private void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); - proofDependencies.SetCurrentDefinition(proc.VerboseName); + proofDependencies.SetCurrentDefinition(proc.VerboseName, m); currentModule = m.EnclosingClass.EnclosingModuleDefinition; codeContext = m; isAllocContext = new IsAllocContext(options, m.IsGhost); @@ -820,7 +820,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); - proofDependencies.SetCurrentDefinition(proc.VerboseName); + proofDependencies.SetCurrentDefinition(proc.VerboseName, m); currentModule = m.EnclosingClass.EnclosingModuleDefinition; codeContext = m; isAllocContext = new IsAllocContext(options, m.IsGhost); @@ -918,7 +918,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null); Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null); - proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.OverrideCheck)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.OverrideCheck), f); #region first procedure, no impl yet //Function nf = new Function(f.tok, "OverrideCheck_" + f.Name, f.IsStatic, f.IsGhost, f.TypeArgs, f.OpenParen, f.Formals, f.ResultType, f.Req, f.Reads, f.Ens, f.Decreases, f.Body, f.Attributes, f.SignatureEllipsis); //AddFunction(f); @@ -1691,7 +1691,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { Contract.Ensures(Contract.Result() != null); Contract.Assert(VisibleInScope(m)); - proofDependencies.SetCurrentDefinition(MethodVerboseName(m.FullDafnyName, kind)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(m.FullDafnyName, kind), m); currentModule = m.EnclosingClass.EnclosingModuleDefinition; codeContext = m; isAllocContext = new IsAllocContext(options, m.IsGhost); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 7ec946ea67e..0a59c9b84c7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -1417,7 +1417,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null); - proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness), null); if (!InVerificationScope(decl)) { // Checked in other file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 6a4da1fa878..b3173919ef7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2289,7 +2289,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); - proofDependencies.SetCurrentDefinition(MethodVerboseName(ctor.FullName, MethodTranslationKind.SpecWellformedness)); + proofDependencies.SetCurrentDefinition(MethodVerboseName(ctor.FullName, MethodTranslationKind.SpecWellformedness), ctor.EnclosingDatatype); if (!InVerificationScope(ctor)) { // Checked in other file diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index e7ab874bfad..e0a96f865ce 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -120,7 +120,7 @@ public EnsuresDependency(IToken token, Expression ensures) { // Represents the goal of proving a specific requires clause of a specific // call. public class CallRequiresDependency : ProofDependency { - private readonly CallDependency call; + public readonly CallDependency call; private readonly RequiresDependency requires; public override RangeToken Range => @@ -138,7 +138,7 @@ public CallRequiresDependency(CallDependency call, RequiresDependency requires) // Represents the assumption of a specific ensures clause of a specific // call. public class CallEnsuresDependency : ProofDependency { - private readonly CallDependency call; + public readonly CallDependency call; private readonly EnsuresDependency ensures; public override RangeToken Range => @@ -155,7 +155,7 @@ public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { // Represents the fact that a particular call occurred. public class CallDependency : ProofDependency { - private readonly CallStmt call; + public readonly CallStmt call; public override RangeToken Range => call.RangeToken; @@ -224,7 +224,7 @@ public class FunctionDefinitionDependency : ProofDependency { public override string Description => $"function definition for {function.Name}"; - private Function function; + public Function function; public FunctionDefinitionDependency(Function f) { function = f; diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index 52ec364eeb2..ff81039f59a 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -8,40 +8,42 @@ using System; using System.Collections.Generic; using System.Linq; -using Dafny; -using Bpl = Microsoft.Boogie; -using BplParser = Microsoft.Boogie.Parser; using Microsoft.Boogie; using DafnyCore.Verifier; -using PODesc = Microsoft.Dafny.ProofObligationDescription; namespace Microsoft.Dafny { public class ProofDependencyManager { // proof dependency tracking state public Dictionary ProofDependenciesById { get; } = new(); - private readonly Dictionary> idsByMemberName = new(); + public readonly Dictionary Deps)> idsByMemberName = new(); private UInt64 proofDependencyIdCount = 0; - private string currentDefinition; + private string currentDeclarationString; + private Declaration currentDeclaration; public string GetProofDependencyId(ProofDependency dep) { var idString = $"id{proofDependencyIdCount}"; ProofDependenciesById[idString] = dep; proofDependencyIdCount++; - var currentSet = idsByMemberName.GetOrCreate(currentDefinition, () => new HashSet()); + var (_, currentSet) = idsByMemberName.GetOrCreate(currentDeclarationString, () => (currentDeclaration, new HashSet())); currentSet.Add(dep); return idString; } - public void SetCurrentDefinition(string verificationScopeId) { - currentDefinition = verificationScopeId; + public void SetCurrentDefinition(string verificationScopeId, Declaration decl) { + currentDeclarationString = verificationScopeId; + currentDeclaration = decl; } public IEnumerable GetPotentialDependenciesForDefinition(string defName) { - return idsByMemberName[defName]; + return idsByMemberName[defName].Deps; + } + + public Declaration GetDeclerationForDefinition(string defName) { + return idsByMemberName[defName].Decl; } public IEnumerable GetAllPotentialDependencies() { - return idsByMemberName.Values.SelectMany(x => x); + return idsByMemberName.Values.SelectMany(x => x.Deps); } // The "id" attribute on a Boogie AST node is used by Boogie to label diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index ffdb3594ac2..ab5774b8eec 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -44,7 +44,7 @@ public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunRes var mockNumber = 42; var mockAsserts = vcResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description))); var runResult = new VerificationRunResult(vcResult.VCNum, mockNumber, vcResult.StartTime, vcResult.Outcome, vcResult.RunTime, mockNumber, null!, - mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null); + mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null, new List()); return new VerificationTaskResult(null, runResult); } From 1f1c402802eb53fbae3f5a6f802f8c30b1374317 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 17:25:54 +0200 Subject: [PATCH 03/27] review --- Source/DafnyCore/DafnyConsolePrinter.cs | 13 +- Source/DafnyCore/ProofDependencyWarnings.cs | 137 +++++++++--------- .../Legacy/LegacyJsonVerificationLogger.cs | 12 +- .../Legacy/LegacyVerificationResultLogger.cs | 2 +- .../Legacy/SynchronousCliCompilation.cs | 2 +- 5 files changed, 86 insertions(+), 80 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index b3f75eac13f..7d605c6c7c6 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -21,12 +21,13 @@ public class DafnyConsolePrinter : ConsolePrinter { private DafnyOptions options; public record ImplementationLogEntry(string Name, Boogie.IToken Tok); - public record VCResultLogEntry( + public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id); + public record VerificationRunResultPartialCopy( int VCNum, DateTime StartTime, TimeSpan RunTime, SolverOutcome Outcome, - List<(Boogie.IToken Tok, string Description, string Id)> Asserts, + List Asserts, IEnumerable CoveredElements, IEnumerable AvailableAxioms, int ResourceCount); @@ -34,7 +35,7 @@ public record VerificationResultLogEntry( VcOutcome Outcome, TimeSpan RunTime, int ResourceCount, - List VCResults, + List VCResults, List Counterexamples); public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result); @@ -44,9 +45,9 @@ public static VerificationResultLogEntry DistillVerificationResult(Implementatio verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors); } - public static VCResultLogEntry DistillVCResult(VerificationRunResult r) { - return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome, - r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription, GetId(a))).ToList(), r.CoveredElements, + public static VerificationRunResultPartialCopy DistillVCResult(VerificationRunResult r) { + return new VerificationRunResultPartialCopy(r.VcNum, r.StartTime, r.RunTime, r.Outcome, + r.Asserts.Select(a => new AssertCmdPartialCopy(a.tok, a.Description.SuccessDescription, GetId(a))).ToList(), r.CoveredElements, r.DeclarationsAfterPruning.OfType(), r.ResourceCount); string GetId(ICarriesAttributes construct) { diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index add06894685..16511b98b38 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -23,7 +23,7 @@ public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerabl } } - public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) { + public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) { var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList(); var orderedResults = verificationResults.OrderBy(vr => @@ -33,9 +33,9 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er if (result.Outcome != VcOutcome.Correct) { continue; } - var assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(e.Asserts))).ToList(); + var assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet(e.Asserts))).ToList(); var unusedFunctions = UnusedFunctions(depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); - Warn(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions); + WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions); } } @@ -46,90 +46,92 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions return; } var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))).ToList(); - var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(tp.Item2.Asserts))).ToList(); + var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet(tp.Item2.Asserts))).ToList(); var unusedFunctions = UnusedFunctions(depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); - Warn(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); + WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); } private static List UnusedFunctions(ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { var unusedFunctions = new List(); - if (depManager.idsByMemberName[name].Decl is Method m) { - var referencedFunctions = ReferencedFunctions(m); + if (depManager.idsByMemberName[name].Decl is not Method m) { + return unusedFunctions; + } - var hiddenFunctions = HiddenFunctions(referencedFunctions); + var referencedFunctions = ReferencedFunctions(m); - var usedFunctions = coveredElements.Select(depManager.GetFullIdDependency).OfType() - .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); + var hiddenFunctions = HiddenFunctions(referencedFunctions); - unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); + var usedFunctions = coveredElements.Select(depManager.GetFullIdDependency).OfType() + .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); - HashSet ReferencedFunctions(Method method) { - var fCEsinM = method.Body.AllSubExpressions(false, false).OfType(); - var fToDeps = new Dictionary>(); + unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); - foreach (var fce in fCEsinM) { - var fun = fce.Function; - if (!fToDeps.ContainsKey(fun)) { - fToDeps[fun] = Dependents(fun); - } + HashSet ReferencedFunctions(Method method) { + var functionCallsInMethod = method.Body.AllSubExpressions(false, false).OfType(); + var functionDependants = new Dictionary>(); - continue; + foreach (var fce in functionCallsInMethod) { + var fun = fce.Function; + if (!functionDependants.ContainsKey(fun)) { + functionDependants[fun] = Dependents(fun); + } + + continue; - IEnumerable Dependents(Function fn) { - var queue = new Queue(new[] { fn }); - var visited = new HashSet(); - while (queue.Any()) { - var f = queue.Dequeue(); - visited.Add(f); + IEnumerable Dependents(Function fn) { + var queue = new Queue(new[] { fn }); + var visited = new HashSet(); + while (queue.Any()) { + var f = queue.Dequeue(); + visited.Add(f); - f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); - continue; + f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); + continue; - IEnumerable AllSubFunctions(Expression e) { - return e.SubExpressions.OfType().Select(fce => fce.Function) - .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); - } + IEnumerable AllSubFunctions(Expression e) { + return e.SubExpressions.OfType().Select(fce => fce.Function) + .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); } - return visited.ToList(); } + return visited.ToList(); } + } - var hashSet = new HashSet(); - foreach (var (f, deps) in fToDeps) { - hashSet.Add(f); - hashSet.UnionWith(deps); - } - - return hashSet; + var hashSet = new HashSet(); + foreach (var (f, deps) in functionDependants) { + hashSet.Add(f); + hashSet.UnionWith(deps); } - HashSet HiddenFunctions(HashSet functions) { - var hiddenFunctions = new HashSet(functions); + return hashSet; + } - foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { - hiddenFunctions.Remove(visibleFunction); - } + HashSet HiddenFunctions(HashSet functions) { + var hiddenFunctions = new HashSet(functions); - return hiddenFunctions; + foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { + hiddenFunctions.Remove(visibleFunction); + } - Function GetFunctionFromAttributed(ICarriesAttributes construct) { - var values = construct.FindAllAttributes("id"); - if (!values.Any()) { - return null; - } - var id = (string)values.Last().Params.First(); - if (depManager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) { - return fdd.function; - } + return hiddenFunctions; + + Function GetFunctionFromAttributed(ICarriesAttributes construct) { + var values = construct.FindAllAttributes("id"); + if (!values.Any()) { return null; } + var id = (string)values.Last().Params.First(); + if (depManager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) { + return fdd.function; + } + return null; } } return unusedFunctions; } - private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, List<(IEnumerable CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage, List unusedFunctions) { + private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, + string scopeName, List<(IEnumerable CoveredElements, HashSet Asserts)> assertCoverage, List unusedFunctions) { var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = @@ -178,25 +180,28 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo } if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) { - // Function hiding suggestion - if (unusedFunctions.Any()) { - reporter.Info(MessageSource.Verifier, m.Body.StartToken, - $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); - } - + SuggestFunctionHiding(reporter, unusedFunctions, m); SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage); } } + private static void SuggestFunctionHiding(ErrorReporter reporter, List unusedFunctions, Method m) + { + if (unusedFunctions.Any()) { + reporter.Info(MessageSource.Verifier, m.Body.StartToken, + $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); + } + } + private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, List<(IEnumerable CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage) { - var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet<(Boogie.IToken Tok, string Description, string Id)> { }); + string scopeName, List<(IEnumerable CoveredElements, HashSet Asserts)> assertCoverage) { + var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet { }); foreach (var (usedFacts, asserts) in assertCoverage) { foreach (var fact in usedFacts) { var dep = depManager.GetFullIdDependency(fact); _ = dep is not EnsuresDependency && - dependencyTracker.TryAdd(dep, new HashSet<(Boogie.IToken Tok, string Description, string Id)>()); + dependencyTracker.TryAdd(dep, new HashSet()); if (dependencyTracker.ContainsKey(dep)) { dependencyTracker[dep].UnionWith(asserts); } diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index ab5774b8eec..683092cf02b 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -35,16 +35,16 @@ public DummyProofObligationDescription(string success) { } - private JsonNode SerializeVcResult(IEnumerable potentialDependencies, DafnyConsolePrinter.VCResultLogEntry vcResult) { - var runResult = VCResultLogEntryToPartialVerificationRunResult(vcResult); + private JsonNode SerializeVcResult(IEnumerable potentialDependencies, DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) { + var runResult = VCResultLogEntryToPartialVerificationRunResult(verificationRunResult); return JsonVerificationLogger.SerializeVcResult(depManager, potentialDependencies?.ToList(), runResult); } - public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VCResultLogEntry vcResult) { + public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) { var mockNumber = 42; - var mockAsserts = vcResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description))); - var runResult = new VerificationRunResult(vcResult.VCNum, mockNumber, vcResult.StartTime, vcResult.Outcome, vcResult.RunTime, mockNumber, null!, - mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null, new List()); + var mockAsserts = verificationRunResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description))); + var runResult = new VerificationRunResult(verificationRunResult.VCNum, mockNumber, verificationRunResult.StartTime, verificationRunResult.Outcome, verificationRunResult.RunTime, mockNumber, null!, + mockAsserts.ToList(), verificationRunResult.CoveredElements, verificationRunResult.ResourceCount, null, new List()); return new VerificationTaskResult(null, runResult); } diff --git a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs index b694ae5259c..4f182bdf842 100644 --- a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs @@ -72,7 +72,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa )); } - private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { + private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { var testResults = new List(); foreach (var ((verbName, currentFile), vcResults) in verificationResults) { diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 6c7a02f9b60..bffe29d28b3 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -291,7 +291,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId); if (options.TrackVerificationCoverage) { - ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager); + ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options, dafnyProgram.Reporter, depManager); var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport); if (coverageReportDir != null) { await new CoverageReporter(options).SerializeVerificationCoverageReport( From 95299e1075257b56c60e79f1935f69ee4691d085 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 17:45:30 +0200 Subject: [PATCH 04/27] style --- Source/DafnyCore/ProofDependencyWarnings.cs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 16511b98b38..47f6d7b60dc 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -185,8 +185,7 @@ private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, E } } - private static void SuggestFunctionHiding(ErrorReporter reporter, List unusedFunctions, Method m) - { + private static void SuggestFunctionHiding(ErrorReporter reporter, List unusedFunctions, Method m) { if (unusedFunctions.Any()) { reporter.Info(MessageSource.Verifier, m.Body.StartToken, $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); From a1ae235499252a9bc739a9bec40a49edde516fc0 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 19:24:57 +0200 Subject: [PATCH 05/27] avoid iterating over null --- Source/DafnyCore/ProofDependencyWarnings.cs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 47f6d7b60dc..21730ae206a 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -34,7 +34,7 @@ public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(Dafn continue; } var assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet(e.Asserts))).ToList(); - var unusedFunctions = UnusedFunctions(depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); + var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions); } } @@ -47,11 +47,15 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions } var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))).ToList(); var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet(tp.Item2.Asserts))).ToList(); - var unusedFunctions = UnusedFunctions(depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); + var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); } - private static List UnusedFunctions(ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { + private static List UnusedFunctions(DafnyOptions dafnyOptions, ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { + if (!(dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[name].Decl is Method)) { + return new List(); + } + var unusedFunctions = new List(); if (depManager.idsByMemberName[name].Decl is not Method m) { return unusedFunctions; @@ -67,7 +71,7 @@ private static List UnusedFunctions(ProofDependencyManager depManager, unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); HashSet ReferencedFunctions(Method method) { - var functionCallsInMethod = method.Body.AllSubExpressions(false, false).OfType(); + var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType() : new List(); var functionDependants = new Dictionary>(); foreach (var fce in functionCallsInMethod) { From 17eb6ff1d9ca7830afc9babb8a85ffe8b103ac10 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 8 Oct 2024 20:03:55 +0200 Subject: [PATCH 06/27] tests --- Source/DafnyCore/ProofDependencyWarnings.cs | 1 + .../LitTest/logger/ProofRefactorings.dfy | 110 ++++++++++++++++++ .../logger/ProofRefactorings.dfy.expect | 10 ++ docs/dev/news/5812.feat | 1 + 4 files changed, 122 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect create mode 100644 docs/dev/news/5812.feat diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 21730ae206a..f138c5a93da 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -244,6 +244,7 @@ private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDepen var completeInformation = true; switch (dep) { + case AssumedProofObligationDependency: case AssumptionDependency: { range = dep.Range; factProvider = "fact"; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy new file mode 100644 index 00000000000..e9af4924f25 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy @@ -0,0 +1,110 @@ +// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --show-hints --isolate-assertions --suggest-proof-refactoring --type-system-refresh "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +//Function Hiding + +function Id(i: int): int { i } + +function Pow(i: int): int { Id(i) * Id(i) } + +function Zero(i: int): int { i * 0 } + + +method NoEffect() returns (r: int) + ensures true +{ + r := Pow(Pow(3)); +} + +method Shallow() returns (r: int) + ensures r == 3 +{ + r := Zero(Pow(3)); + r := r + 3; +} + +method Deep() returns (r: int) + ensures r == 81 +{ + if Pow(Pow(3)) > 9 { + r := 81; + } else { + r := -81; + } +} + +method HiddenId() returns (r: int) + ensures r == 0 +{ + hide Id; + r := -1; + match Zero(Pow(3)) { + case 0 => { r := 0; } + case _ => {} + } +} + +method HiddenPow() returns (r: int) + ensures r == 0 +{ + hide Pow; + r := Zero(Pow(3)); + var i := 3; + while i > 0 + invariant r == 3 - i + decreases i + { + r := r+1; + i := i-1; + } + r := r - 3; +} + +// By-proofs + +opaque predicate P() { true } + +method M() requires P() { } + +method N() ensures P() { reveal P(); } + +method NoSuggestion() +{ + N(); + M(); +} + +method Call() +{ + assert P() by { reveal P(); } + M(); +} + +method CallFixed() +{ + M() by { + assert P() by { reveal P(); } + } +} + +method Requires() + requires P() +{ + assert P(); +} + +method RequiresFixed() + requires p: P() +{ + assert P() by { + reveal p; + } +} + +method CantMove(){ + var b := P(); + assert b by { reveal P(); } + b := !b; + assert !b; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect new file mode 100644 index 00000000000..8ba3856294f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect @@ -0,0 +1,10 @@ +ProofRefactorings.dfy(16,0): Info: Consider hiding these functions, which are unused by the proof: Pow, Id +ProofRefactorings.dfy(22,0): Info: Consider hiding these functions, which are unused by the proof: Pow, Id +ProofRefactorings.dfy(39,0): Info: Consider hiding this function, which is unused by the proof: Pow +ProofRefactorings.dfy(80,10): Info: This fact was only used to prove the precondtion of the method call ProofRefactorings.dfy(81,3)-(81,6). Consider moving it into a by-proof. +ProofRefactorings.dfy(93,0): Info: Consider hiding this function, which is unused by the proof: P +ProofRefactorings.dfy(92,11): Info: This requires clause was only used to prove the assertion ProofRefactorings.dfy(94,11)-(94,11). Consider labelling it and revealing it in a by-proof. +ProofRefactorings.dfy(99,0): Info: Consider hiding this function, which is unused by the proof: P +ProofRefactorings.dfy(107,9): Info: This fact was only used to prove the assertion ProofRefactorings.dfy(109,10)-(109,10). Consider moving it into a by-proof. + +Dafny program verifier finished with 44 verified, 0 errors diff --git a/docs/dev/news/5812.feat b/docs/dev/news/5812.feat new file mode 100644 index 00000000000..a1a0d51160e --- /dev/null +++ b/docs/dev/news/5812.feat @@ -0,0 +1 @@ +Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. \ No newline at end of file From faff8dff49d4fd72f2a59d5e4e4e4b33daae45f1 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 11:11:06 +0200 Subject: [PATCH 07/27] bump boogie --- Source/DafnyCore/DafnyConsolePrinter.cs | 2 +- Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/ProofDependencyWarnings.cs | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 7d605c6c7c6..b948d235b12 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -53,7 +53,7 @@ public static VerificationRunResultPartialCopy DistillVCResult(VerificationRunRe string GetId(ICarriesAttributes construct) { var values = construct.FindAllAttributes("id"); if (!values.Any()) { - throw new ArgumentException($"No dependency ID in assertion"); + return ""; } return (string)values.Last().Params.First(); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 3acc56618f8..6bfcfa15f26 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index f138c5a93da..4d8159352be 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -45,8 +45,8 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } - var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))).ToList(); - var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet(tp.Item2.Asserts))).ToList(); + var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))); + var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet(tp.Item2.Asserts))); var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); } @@ -135,7 +135,7 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) { } private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, List<(IEnumerable CoveredElements, HashSet Asserts)> assertCoverage, List unusedFunctions) { + string scopeName, IEnumerable<(IEnumerable CoveredElements, HashSet)> assertCoverage, List unusedFunctions) { var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = @@ -185,7 +185,7 @@ private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, E if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) { SuggestFunctionHiding(reporter, unusedFunctions, m); - SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage); + SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage.ToList()); } } From c66fa0ac9a220ae460b1996bf70a3e6c148bf671 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 11:17:46 +0200 Subject: [PATCH 08/27] reintroduce rename error --- Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 959c6a92339..d0daf463d62 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -332,7 +332,7 @@ string MoreInformation(Boogie.IToken? token, bool hoveringPostcondition) { } else { information += GetDescription(returnCounterexample.FailingReturn.Description); } - information += MoreInformation(returnCounterexample.FailingAssert.tok, currentlyHoveringPostcondition); + information += MoreInformation(returnCounterexample.FailingFailingAssert.tok, currentlyHoveringPostcondition); } else if (counterexample is CallCounterexample callCounterexample) { if (assertionNode.StatusVerification == GutterVerificationStatus.Error && callCounterexample.FailingRequires.Description.SuccessDescription != "assertion always holds" From 855e84f339d0b9573a070205db531393a5747227 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 11:30:13 +0200 Subject: [PATCH 09/27] fix patch --- customBoogie.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/customBoogie.patch b/customBoogie.patch index 1c73d305526..87eb5cc8dea 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + From 915bbcffa12f39729b497d631774e09bc6a644e7 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 12:04:41 +0200 Subject: [PATCH 10/27] review --- Source/DafnyCore/ProofDependencyWarnings.cs | 96 ++++++++++----------- 1 file changed, 47 insertions(+), 49 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 4d8159352be..e36e963688b 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -33,9 +33,8 @@ public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(Dafn if (result.Outcome != VcOutcome.Correct) { continue; } - var assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet(e.Asserts))).ToList(); var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); - WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions); + WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults, unusedFunctions); } } @@ -45,10 +44,8 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } - var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))); - var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet(tp.Item2.Asserts))); - var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms)); - WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions); + var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms)); + WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions); } private static List UnusedFunctions(DafnyOptions dafnyOptions, ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { @@ -70,46 +67,6 @@ private static List UnusedFunctions(DafnyOptions dafnyOptions, ProofDe unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); - HashSet ReferencedFunctions(Method method) { - var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType() : new List(); - var functionDependants = new Dictionary>(); - - foreach (var fce in functionCallsInMethod) { - var fun = fce.Function; - if (!functionDependants.ContainsKey(fun)) { - functionDependants[fun] = Dependents(fun); - } - - continue; - - IEnumerable Dependents(Function fn) { - var queue = new Queue(new[] { fn }); - var visited = new HashSet(); - while (queue.Any()) { - var f = queue.Dequeue(); - visited.Add(f); - - f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); - continue; - - IEnumerable AllSubFunctions(Expression e) { - return e.SubExpressions.OfType().Select(fce => fce.Function) - .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); - } - } - return visited.ToList(); - } - } - - var hashSet = new HashSet(); - foreach (var (f, deps) in functionDependants) { - hashSet.Add(f); - hashSet.UnionWith(deps); - } - - return hashSet; - } - HashSet HiddenFunctions(HashSet functions) { var hiddenFunctions = new HashSet(functions); @@ -134,8 +91,49 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) { return unusedFunctions; } + private static HashSet ReferencedFunctions(Method method) { + var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType() : new List(); + var functionDependants = new Dictionary>(); + + foreach (var fce in functionCallsInMethod) { + var fun = fce.Function; + if (!functionDependants.ContainsKey(fun)) { + functionDependants[fun] = Dependents(fun); + } + + continue; + + IEnumerable Dependents(Function fn) { + var queue = new Queue(new[] { fn }); + var visited = new HashSet(); + while (queue.Any()) { + var f = queue.Dequeue(); + visited.Add(f); + + f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); + continue; + + IEnumerable AllSubFunctions(Expression e) { + return e.SubExpressions.OfType().Select(fce => fce.Function) + .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); + } + } + return visited.ToList(); + } + } + + var hashSet = new HashSet(); + foreach (var (f, deps) in functionDependants) { + hashSet.Add(f); + hashSet.UnionWith(deps); + } + + return hashSet; + } + + private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, IEnumerable<(IEnumerable CoveredElements, HashSet)> assertCoverage, List unusedFunctions) { + string scopeName, IReadOnlyList assertCoverage, List unusedFunctions) { var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = @@ -197,10 +195,10 @@ private static void SuggestFunctionHiding(ErrorReporter reporter, List } private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, List<(IEnumerable CoveredElements, HashSet Asserts)> assertCoverage) { + string scopeName, IReadOnlyList vcResults) { var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet { }); - foreach (var (usedFacts, asserts) in assertCoverage) { + foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) { foreach (var fact in usedFacts) { var dep = depManager.GetFullIdDependency(fact); _ = dep is not EnsuresDependency && From da63cb5feb98c6a8448117622fb2be1f4334ce7f Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 12:18:52 +0200 Subject: [PATCH 11/27] fix tests --- .../dafny0/snapshots/Snapshots1.run.legacy.dfy.expect | 2 +- .../dafny0/snapshots/Snapshots2.run.legacy.dfy.expect | 10 +++++----- .../LitTest/logger/ProofRefactorings.dfy.expect | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect index a2ef2d3d341..8b42575e0c8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect @@ -4,7 +4,7 @@ Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id1"} Lit(false); Dafny program verifier finished with 1 verified, 0 errors Processing call to procedure N (call) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)): >>> added after: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id6"} Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id8"} Lit(false); >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect index 768491421f5..ff0fa5283af 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect @@ -16,16 +16,16 @@ Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id12"} Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id14"} Lit(false); >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion might not hold -Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id16"} Lit(true); +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id18"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id15"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id19"} Lit(true); +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id21"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id18"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id20"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect index 8ba3856294f..b9b77183bd7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect @@ -7,4 +7,4 @@ ProofRefactorings.dfy(92,11): Info: This requires clause was only used to prove ProofRefactorings.dfy(99,0): Info: Consider hiding this function, which is unused by the proof: P ProofRefactorings.dfy(107,9): Info: This fact was only used to prove the assertion ProofRefactorings.dfy(109,10)-(109,10). Consider moving it into a by-proof. -Dafny program verifier finished with 44 verified, 0 errors +Dafny program verifier finished with 22 verified, 0 errors From 3746748880af2c50b80be97f37a0d2c0ee0b825b Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 12:56:39 +0200 Subject: [PATCH 12/27] regnerate doos --- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1518 -> 1531 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1539 -> 1552 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1509 -> 1522 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 2027 -> 2040 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1498 -> 1511 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1505 -> 1518 bytes .../binaries/DafnyStandardLibraries.doo | Bin 57213 -> 57225 bytes 7 files changed, 0 insertions(+), 0 deletions(-) diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 472917014fca63fcff0f941f6ff184cb89df615d..3c0752af411a0b6aa604ae8390ce750d7c54d5de 100644 GIT binary patch delta 511 zcmaFI{hPZ!z?+#xgn@y9gP|(TKXS1nPi_q(1A{O#0|PHmG&eCXGcC2aM6V=2Hzzm9 zvG2A4&z|R^-1kLI-pWoiq4wPJvh(T z2TbAGUsEmVcijK5qQjHha<#T~wt79&Qa;RNDq8BHF}MEj$5iEcX@2wjmp}Zl`OH;? zzoiXRP8~fs)hjI6#iOg-;DOGIh3hs~v#l3xRkV!X!S&CmQ}#g ziJQM}w#;DVQ#hzvRWCf@ua@n_d~@!brzDiueH6QY?1{I-bM*=PBhJ4nX$sI2`#DiU zc}qxa&YSAib!Q%|{Kj**obj6E5wT5&Cmo7*I^HU5*klpC+;3XPpJ&^4zUbACnI6s8 z&U5Dt7iTe>yUeV5t7~)DIX%v>-|+A~@4NY*a+aShiPEjoyx7V5Ve1Jy^DC1|ZL1de z-K*NJyZ-){D;{dvbC0hJbKZSp?L_q}vA4S;3{0%sMgPg~=0}OC&C40jGV`HE+2kfx lU3rkuByr1sD}gb1l%Iit9Tm}f3=AKc7#MhgqPdBAnQ5uTC3+?KxjDH( zj(O6CJbQkN9=w-&C6jOO7jet296WA|$~rx+v`xwS{e5BC-L0`-tepAM+IW`AD6881 za}3n_^W}4<#hd-SyBQ|xe}8fM-|@P{Eh^3ZA``S-onF?zS^r-8ox`&tQ4e%AZADE6*^BgdYcN8zOSQp0RyMr#roY1ccNc*+TGDfnP%t~^H_IR@5$*6=lm7wH_p5Il4ao>olm-k zZW$|g-MI0cD|Y6=;J1=(;f&WLkMP_~^n7T$@bRHe3CB4%S58({+P^YatLh=w^QY4e z>oJ?}b~-fYpkVtm`M%Pnt1npG;?Mb!-u!yG%_&{aYm?bNZ9TEn{Q9R~+FJaT#*s^H zzGa$j;oog~p{45jQzIRTSyOXM|GB^8Mv0uwTNuwW^P$GlQ`k2vcz<5>hzj2eafsS-@R|Hd@Qo}91r^(MQ6?D9-Qav z1Ez58uc?;wJMMp2(c#H$xmw#gTfLrXDIaDs6)pA9m|Oq%W2*AJG{5=%%O8H&eCDdc z-_nLDr;Z++>J=93;?Y%Z@IdFq!gZUg+187;Dq6|@4~$n>O3dkSOTEtXc|aGdLZLFB4vndIvbr|qjRSZ+NNav{=Ts6?$+2ZR?d8BZ9Ge5lvQp1 zIR~{E-3$};zrQ&B?|5C}7M13HkqO$aPA}`M$~&V1$*8#~;UeXWEiKkI#56nj^|k>gcO)3O!oHk^)FF0?CV>b0LN>6g3ILM}FH z_0Cy4-`7#QfPqu*V*T!hJJByY?e6HLOfz(gd91su_vG}3bN&kT8|Php$+B>c&L>?% zw~Up$Zru3J6+81_@LS2YaK>wrM|f@~dOoyW`1nw#gyWo>D<`We?O&OzRrQeT`O|5K z^_b0fI~|&HP_X@(d|&C()fX&o@#p+VZ+^Yp=9I4IwaILsww_pOe*M!gZ7u#vhkqeRZ;EsT$t`A}nN@)A~Ed5}=TnZ@t+F*7jm Z2rw|P10xOwmNd?q{DD=9t(Fxe0st%K+U@`V diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 4c1f17a2c990772c64119a74a66d93f1feb8c7ef..c874419dd2261746fd893672223cd9937e19fa86 100644 GIT binary patch delta 510 zcmaFL{fWCiz?+#xgn@y9gP|tPKXS1nPi_q(1A{O#0|PHmG&eCXGcC2aM6V=2Hzzm9 zvG2A4&z|R^-1kLI-pWoiq4wPJvh(T z2TbAGUsEmVcijK5qQjHha<#T~wt79&Qa;RNDq8BHF}MEj$5iEcX@2wjmp}Zl`OH;? zzoiXRP8~fs)hjI6#iOg-;DOGIh3hs~v#l3xRkV!X!S&CmQ}#g ziJQM}w#;DVQ#hzvRWCf@ua@n_d~@!brzDiueH6QY?1{I-bM*=PBhJ4nX$sI2`#DiU zc}qxa&YSAib!Q%|{Kj**obj6E5wT5&Cmo7*I^HU5*klpC+;3XPpJ&^4zUbACnI6s8 z&U5Dt7iTe>yUeV5t7~)DIX%v>-|+A~@4NY*a+aShiPEjoyx7V5Ve1Jy^DC1|ZL1de z-K*NJyZ-){D;{dvbC0hJbKZSp?L_q}vA4S;3{0%sMgPg~=0}OC&C3~&F!P~C+2l%A oU1p%rm}f3=AKc7#MhgqPdBAnQ5uTC3+?KxjDH( zj(O6CJbQkN9=w-&C6jOO7jet296WA|$~rx+v`xwS{e5BC-L0`-tepAM+IW`AD6881 za}3n_^W}4<#hd-SyBQ|xe}8fM-|@P{Eh^3ZA``S-onF?zS^r-8ox`&tQ4e%AZADE6*^BgdYcN8zOSQp0RyMr#roY1ccNc*+TGDfnP%t~^H_IR@5$*6=lm7wH_p5Il4ao>olm-k zZW$|g-MI0cD|Y6=;J1=(;f&WLkMP_~^n7T$@bRHe3CB4%S58({+P^YatLh=w^QY4e z>oJ?}b~-fYpkVtm`M%Pnt1npG;?Mb!-u!yG%_&{aYm?bNZ9TEn{Q9R~+FJaT#*s^H zzGa$j;oog~p{45jQzIRTSyOXM|GB^8Mv0uwTNsZp^P$Glo@g8%>k diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index a7e521f03bd97391c456d74db0c59ceb1ef3ab81..69b896e4ada15f6b11f5b01d68bbac377a14be17 100644 GIT binary patch delta 489 zcmaFO|AW6iz?+#xgn@y9gP|eKKXS1nPi_q(1A{O#0|PHmG&eCXGcC2aM6V=2Hzzm9 zvG2A4&z|R^-1kLI-pWoiq4wPJvh(T z2TbAGUsEmVcijK5qQjHha<#T~wt79&Qa;RNDq8BHF}MEj$5iEcX@2wjmp}Zl`OH;? zzoiXRP8~fs)hjI6#iOg-;DOGIh3hs~v#l3xRkV!X!S&CmQ}#g ziJQM}w#;DVQ#hzvRWCf@ua@n_d~@!brzDiueH6QY?1{I-bM*=PBhJ4nX$sI2`#DiU zc}qxa&YSAib!Q%|{Kj**obj6E5wT5&Cmo7*I^HU5*klpC+;3XPpJ&^4zUbACnI6s8 z&U5Dt7iTe>yUeV5t7~)DIX%v>-|+A~@4NY*a+aShiPEjoyx7V5Ve1Jy^DC1|ZL1de z-K*NJyZ-){D;{dvbC0hJbKZSp?L_q}vA4S;3{0%sMgPg~=0}OC&C3~2vGSot+2ne5 ZU1p%r*jLRpVW|v|sVh2Vd0|4Co*0KNq delta 497 zcmeyt|C+x(z?+#xgn@y9gCV2BEwXLp*>m}f3=AKc7#MhgqPdBAnQ5uTC3+?KxjDH( zj(O6CJbQkN9=w-&C6jOO7jet296WA|$~rx+v`xwS{e5BC-L0`-tepAM+IW`AD6881 za}3n_^W}4<#hd-SyBQ|xe}8fM-|@P{Eh^3ZA``S-onF?zS^r-8ox`&tQ4e%AZADE6*^BgdYcN8zOSQp0RyMr#roY1ccNc*+TGDfnP%t~^H_IR@5$*6=lm7wH_p5Il4ao>olm-k zZW$|g-MI0cD|Y6=;J1=(;f&WLkMP_~^n7T$@bRHe3CB4%S58({+P^YatLh=w^QY4e z>oJ?}b~-fYpkVtm`M%Pnt1npG;?Mb!-u!yG%_&{aYm?bNZ9TEn{Q9R~+FJaT#*s^H zzGa$j;oog~p{45jQzIRTSyOXM|GB^8Mv0uwTNqEV@}b7k>wTh*;Lv% diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index a1da8699385a8a74833b2590ce2da153ddadc47a..91e26f57c5d9cae99142e83b4a172524e3d666a9 100644 GIT binary patch delta 489 zcmcb`{hYf#z?+#xgn@y9gP}alKXS1nPi_q(1A{O#0|PHmG&eCXGcC2aM6V=2Hzzm9 zvG2A4&z|R^-1kLI-pWoiq4wPJvh(T z2TbAGUsEmVcijK5qQjHha<#T~wt79&Qa;RNDq8BHF}MEj$5iEcX@2wjmp}Zl`OH;? zzoiXRP8~fs)hjI6#iOg-;DOGIh3hs~v#l3xRkV!X!S&CmQ}#g ziJQM}w#;DVQ#hzvRWCf@ua@n_d~@!brzDiueH6QY?1{I-bM*=PBhJ4nX$sI2`#DiU zc}qxa&YSAib!Q%|{Kj**obj6E5wT5&Cmo7*I^HU5*klpC+;3XPpJ&^4zUbACnI6s8 z&U5Dt7iTe>yUeV5t7~)DIX%v>-|+A~@4NY*a+aShiPEjoyx7V5Ve1Jy^DC1|ZL1de z-K*NJyZ-){D;{dvbC0hJbKZSp?L_q}vA4S;3{0%sMgPg~=0}OC&C3~gGV`HE+2lM{ ZU1p%rm}f3=AKc7#MhgqPdBAnQ5uTC3+?KxjDH( zj(O6CJbQkN9=w-&C6jOO7jet296WA|$~rx+v`xwS{e5BC-L0`-tepAM+IW`AD6881 za}3n_^W}4<#hd-SyBQ|xe}8fM-|@P{Eh^3ZA``S-onF?zS^r-8ox`&tQ4e%AZADE6*^BgdYcN8zOSQp0RyMr#roY1ccNc*+TGDfnP%t~^H_IR@5$*6=lm7wH_p5Il4ao>olm-k zZW$|g-MI0cD|Y6=;J1=(;f&WLkMP_~^n7T$@bRHe3CB4%S58({+P^YatLh=w^QY4e z>oJ?}b~-fYpkVtm`M%Pnt1npG;?Mb!-u!yG%_&{aYm?bNZ9TEn{Q9R~+FJaT#*s^H zzGa$j;oog~p{45jQzIRTSyOXM|GB^8Mv0uwTNrmT^P$Gloiq4wPJvh(T z2TbAGUsEmVcijK5qQjHha<#T~wt79&Qa;RNDq8BHF}MEj$5iEcX@2wjmp}Zl`OH;? zzoiXRP8~fs)hjI6#iOg-;DOGIh3hs~v#l3xRkV!X!S&CmQ}#g ziJQM}w#;DVQ#hzvRWCf@ua@n_d~@!brzDiueH6QY?1{I-bM*=PBhJ4nX$sI2`#DiU zc}qxa&YSAib!Q%|{Kj**obj6E5wT5&Cmo7*I^HU5*klpC+;3XPpJ&^4zUbACnI6s8 z&U5Dt7iTe>yUeV5t7~)DIX%v>-|+A~@4NY*a+aShiPEjoyx7V5Ve1Jy^DC1|ZL1de z-K*NJyZ-){D;{dvbC0hJbKZSp?L_q}vA4S;3{0%sMgPg~=0}OC&C3}NF!P~C+2m4I lU3rku#<$*Q<^W^x6h8w4J1`buU`gZh$p=}b*fLl_A^>8k+TQ>G delta 498 zcmaFI{gAspz?+#xgn@y9gCV!VEwXLp*>m}f3=AKc7#MhgqPdBAnQ5uTC3+?KxjDH( zj(O6CJbQkN9=w-&C6jOO7jet296WA|$~rx+v`xwS{e5BC-L0`-tepAM+IW`AD6881 za}3n_^W}4<#hd-SyBQ|xe}8fM-|@P{Eh^3ZA``S-onF?zS^r-8ox`&tQ4e%AZADE6*^BgdYcN8zOSQp0RyMr#roY1ccNc*+TGDfnP%t~^H_IR@5$*6=lm7wH_p5Il4ao>olm-k zZW$|g-MI0cD|Y6=;J1=(;f&WLkMP_~^n7T$@bRHe3CB4%S58({+P^YatLh=w^QY4e z>oJ?}b~-fYpkVtm`M%Pnt1npG;?Mb!-u!yG%_&{aYm?bNZ9TEn{Q9R~+FJaT#*s^H zzGa$j;oog~p{45jQzIRTSyOXM|GB^8Mv0uwTNn>8^P$GluRd-&wggYJNR zCGjcoWt&`B>`xtJ^acsqhps{cZoc=AfEK(WevN zkIYy&RjTOm4Q-xH4ohws^V}D`Ar=sSg5R4hpOu+gJc)&OpWj>?!J}t$i#KwITg2yE zzDaxVEL_9lyg)~AxBu~77eg~;{<53>@o&Dp+~#&<@!ZgUy-Ceg4H2&L&StTj*SY&& zIqCg=+u7IVwx`oRU8{Uk^m)-Pt2Hy#P5vl^`J8?Ku=oG@_p&GvwRt&X%w0az7@I73 aUzZsuG}-aKG~=?#vG=9enC}DQkO2U=Pur{j delta 499 zcmeC&&-`~EbA5m}Gm8iV0|N&`OodzIbC>Lnd`1R_&rA#qyg0URS0~$@=|$VcFcRvR|x>WeVDOmdYrr z+Wd14)cW(~mx;``^M~~uo}9M*Rr^1Azd_WbgYH}>rYbEgssHviRaq{L@BX*;#P6%m zTvhnHw|UB`lLu#dg$28KbcGu{(0Q?N-RAE+^R&5~i}n?We)#(O1!qg=acLQ!7de7m z)8BRHoUS@Fo551-W5$xm^rTCB3S-tSmR90$oa=u<?y&q$wW;fz9%tBZcvvqTWB>GGp68}{CKJ}X>h0Y*?Rvb{&12$` zYOkjp*9%|0aP{3;8BRy_lMY^3ll%H}eVsf? Date: Tue, 15 Oct 2024 19:01:36 +0200 Subject: [PATCH 13/27] review --- Source/DafnyCore/ProofDependencyWarnings.cs | 155 ++++++++++-------- .../BoogieGenerator.TrPredicateStatement.cs | 2 +- .../logger/FunctionHidingRefactoring.dfy | 59 +++++++ .../FunctionHidingRefactoring.dfy.expect | 5 + .../LitTest/logger/ProofRefactorings.dfy | 110 ------------- .../logger/ProofRefactorings.dfy.expect | 10 -- 6 files changed, 149 insertions(+), 192 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index e36e963688b..2791b3e8c3f 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.Linq; using DafnyCore.Verifier; @@ -10,20 +11,26 @@ namespace Microsoft.Dafny; public record VerificationTaskResult(IVerificationTask Task, VerificationRunResult Result); public class ProofDependencyWarnings { + private static DafnyOptions options; + private static ErrorReporter reporter; + private static ProofDependencyManager manager; - public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable parts, - ErrorReporter reporter, ProofDependencyManager manager) { + public static void ReportSuspiciousDependencies(DafnyOptions dafnyOptions, IEnumerable parts, + ErrorReporter reporter, ProofDependencyManager depManager) { + manager = depManager; + ProofDependencyWarnings.reporter = reporter; + options = dafnyOptions; foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) { - WarnAboutSuspiciousDependenciesForImplementation(options, - reporter, - manager, - resultsForScope.Key, + WarnAboutSuspiciousDependenciesForImplementation(resultsForScope.Key, resultsForScope.Select(p => p.Result).ToList()); } } public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) { + manager = depManager; + ProofDependencyWarnings.reporter = reporter; + options = dafnyOptions; var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList(); var orderedResults = verificationResults.OrderBy(vr => @@ -33,39 +40,39 @@ public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(Dafn if (result.Outcome != VcOutcome.Correct) { continue; } - var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); - WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults, unusedFunctions); + var unusedFunctions = UnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); + WarnAboutSuspiciousDependencies(implementation.Name, result.VCResults, unusedFunctions); } } - public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, - ProofDependencyManager depManager, string name, + public static void WarnAboutSuspiciousDependenciesForImplementation(string name, IReadOnlyList results) { if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } - var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms)); - WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions); + var unusedFunctions = UnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms)); + WarnAboutSuspiciousDependencies(name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions); } - private static List UnusedFunctions(DafnyOptions dafnyOptions, ProofDependencyManager depManager, string name, IEnumerable coveredElements, IEnumerable axioms) { - if (!(dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[name].Decl is Method)) { + private static List UnusedFunctions(string implementationName, IEnumerable coveredElements, + IEnumerable axioms) { + if (!(options.Get(CommonOptionBag.SuggestProofRefactoring) && manager.idsByMemberName[implementationName].Decl is Method)) { return new List(); } var unusedFunctions = new List(); - if (depManager.idsByMemberName[name].Decl is not Method m) { + if (manager.idsByMemberName[implementationName].Decl is not Method method) { return unusedFunctions; } - var referencedFunctions = ReferencedFunctions(m); - + var referencedFunctions = GetReferencedFunctions(method); var hiddenFunctions = HiddenFunctions(referencedFunctions); - - var usedFunctions = coveredElements.Select(depManager.GetFullIdDependency).OfType() + var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType() .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); + + return unusedFunctions; HashSet HiddenFunctions(HashSet functions) { var hiddenFunctions = new HashSet(functions); @@ -82,16 +89,15 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) { return null; } var id = (string)values.Last().Params.First(); - if (depManager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) { + if (manager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) { return fdd.function; } return null; } } - return unusedFunctions; } - private static HashSet ReferencedFunctions(Method method) { + private static HashSet GetReferencedFunctions(Method method) { var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType() : new List(); var functionDependants = new Dictionary>(); @@ -132,13 +138,13 @@ IEnumerable AllSubFunctions(Expression e) { } - private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, IReadOnlyList assertCoverage, List unusedFunctions) { - var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); + private static void WarnAboutSuspiciousDependencies(string scopeName, + IReadOnlyList assertCoverage, List unusedFunctions) { + var potentialDependencies = manager.GetPotentialDependenciesForDefinition(scopeName); var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = coveredElements - .Select(depManager.GetFullIdDependency) + .Select(manager.GetFullIdDependency) .OrderBy(dep => dep.Range) .ThenBy(dep => dep.Description); var unusedDependencies = @@ -148,9 +154,9 @@ private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, E .ThenBy(dep => dep.Description).ToList(); foreach (var unusedDependency in unusedDependencies) { - if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) { + if (options.Get(CommonOptionBag.WarnContradictoryAssumptions)) { if (unusedDependency is ProofObligationDependency obligation) { - if (ShouldWarnVacuous(dafnyOptions, scopeName, obligation)) { + if (ShouldWarnVacuous(scopeName, obligation)) { var message = $"proved using contradictory assumptions: {obligation.Description}"; if (obligation.ProofObligation is AssertStatementDescription) { message += ". (Use the `{:contradiction}` attribute on the `assert` statement to silence.)"; @@ -160,14 +166,14 @@ private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, E } if (unusedDependency is EnsuresDependency ensures) { - if (ShouldWarnVacuous(dafnyOptions, scopeName, ensures)) { + if (ShouldWarnVacuous(scopeName, ensures)) { reporter.Warning(MessageSource.Verifier, "", ensures.Range, $"ensures clause proved using contradictory assumptions"); } } } - if (dafnyOptions.Get(CommonOptionBag.WarnRedundantAssumptions)) { + if (options.Get(CommonOptionBag.WarnRedundantAssumptions)) { if (unusedDependency is RequiresDependency requires) { reporter.Warning(MessageSource.Verifier, "", requires.Range, $"unnecessary requires clause"); } @@ -181,55 +187,33 @@ private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, E } } - if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) { - SuggestFunctionHiding(reporter, unusedFunctions, m); - SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage.ToList()); + if (options.Get(CommonOptionBag.SuggestProofRefactoring) && manager.idsByMemberName[scopeName].Decl is Method m) { + SuggestFunctionHiding(unusedFunctions, m); + SuggestByProofRefactoring(scopeName, assertCoverage.ToList()); } } - private static void SuggestFunctionHiding(ErrorReporter reporter, List unusedFunctions, Method m) { + private static void SuggestFunctionHiding(List unusedFunctions, Method m) { if (unusedFunctions.Any()) { reporter.Info(MessageSource.Verifier, m.Body.StartToken, $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); } } - private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDependencyManager depManager, - string scopeName, IReadOnlyList vcResults) { - var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet { }); - - foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) { - foreach (var fact in usedFacts) { - var dep = depManager.GetFullIdDependency(fact); - _ = dep is not EnsuresDependency && - dependencyTracker.TryAdd(dep, new HashSet()); - if (dependencyTracker.ContainsKey(dep)) { - dependencyTracker[dep].UnionWith(asserts); - } - } - } - - foreach (var (dep, lAsserts) in dependencyTracker) { - foreach (var cmd in lAsserts) { - if (depManager.ProofDependenciesById.TryGetValue(cmd.Id, out var cmdDep)) { - if (dep == cmdDep || dep is CallRequiresDependency req && req.call == cmdDep) { - lAsserts.Remove(cmd); - } - } - } - } - - foreach (var (dep, lAsserts) in dependencyTracker) { - if (lAsserts.Count != 1) { + private static void SuggestByProofRefactoring(string scopeName, + IReadOnlyList verificationRunResults) { + foreach (var (dep, lAsserts) in ComputeAssertionsUsedByFact(scopeName, verificationRunResults)) { + var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1; + if (!factIsOnlyUsedByOneAssertion) { continue; } - var en = lAsserts.GetEnumerator(); - if (!en.MoveNext()) { - continue; + + DafnyConsolePrinter.AssertCmdPartialCopy cmd = null; + foreach (var assert in lAsserts) { + cmd = assert; } - var cmd = en.Current; - depManager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer); + manager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer); if (consumer != null && (dep == consumer || consumer.Range.Intersects(dep.Range))) { continue; @@ -238,7 +222,7 @@ private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDepen RangeToken range = null; var factProvider = ""; var factConsumer = ""; - var recomendation = ""; + var recommendation = ""; var completeInformation = true; switch (dep) { @@ -246,13 +230,13 @@ private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDepen case AssumptionDependency: { range = dep.Range; factProvider = "fact"; - recomendation = "moving it into"; + recommendation = "moving it into"; break; } case RequiresDependency: { range = dep.Range; factProvider = "requires clause"; - recomendation = "labelling it and revealing it in"; + recommendation = "labelling it and revealing it in"; break; } default: completeInformation = false; break; @@ -272,9 +256,37 @@ private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDepen if (completeInformation) { reporter.Info(MessageSource.Verifier, range, - $"This {factProvider} was only used to prove the {factConsumer}. Consider {recomendation} a by-proof."); + $"This {factProvider} was only used to prove the {factConsumer}. Consider {recommendation} a by-proof."); + } + } + } + + private static Dictionary> + ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList vcResults) + { + var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName) + .Where(dep => dep is not EnsuresDependency) + .ToDictionary(dep => dep, _ => new HashSet { }); + + foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) { + foreach (var factReference in usedFacts) { + var factDependency = manager.GetFullIdDependency(factReference); + var excludedDependencies = factDependency is EnsuresDependency; + if (excludedDependencies) { + continue; + } + + assertionsUsedByFact.TryAdd(factDependency, new HashSet()); + + bool NotSelfReferential(DafnyConsolePrinter.AssertCmdPartialCopy assert) => + !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) + || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency); + + assertionsUsedByFact[factDependency].UnionWith(asserts.Where(NotSelfReferential)); } } + + return assertionsUsedByFact; } /// @@ -287,10 +299,11 @@ private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDepen /// to not generate vacuous proof goals, but that may be a difficult /// change to make. /// + /// /// the dependency to examine /// false to skip warning about the absence of this /// dependency, true otherwise - private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName, ProofDependency dep) { + private static bool ShouldWarnVacuous(string verboseName, ProofDependency dep) { if (dep is ProofObligationDependency poDep) { // Dafny generates some assertions about definite assignment whose // proofs are always vacuous. Since these aren't written by Dafny diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs index 39d271c2c56..6aa63b5f0e9 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs @@ -153,7 +153,7 @@ private bool TrAssertCondition(PredicateStmt stmt, var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes); var splits = TrSplitExpr(proofBuilder.Context, stmt.Expr, etran, true, out var splitHappened); if (!splitHappened) { - var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr)); + IToken tok = enclosingToken == null ? stmt.RangeToken : new NestedToken(enclosingToken, stmt.RangeToken); var desc = new AssertStatementDescription(stmt, errorMessage, successMessage); proofBuilder.Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok, proofBuilder.Context, etran.TrAttributes(stmt.Attributes, null))); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy new file mode 100644 index 00000000000..bb08918946e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy @@ -0,0 +1,59 @@ +// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --show-hints --isolate-assertions --suggest-proof-refactoring --type-system-refresh "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function Id(i: int): int { i } + +function Square(i: int): int { Id(i) * Id(i) } + +function Zero(i: int): int { i * 0 } + + +method ResultIsUnused() returns (r: int) + ensures true +{ + r := Square(Square(3)); +} + +method UnusedAssignment() returns (r: int) + ensures r == 3 +{ + r := Zero(Square(3)); + r := r + 3; +} + +method ReferencedFunctionsAreUsed() returns (r: int) + ensures r == 81 +{ + if Square(Square(3)) > 9 { + r := 81; + } else { + r := -81; + } +} + +method HiddenId() returns (r: int) + ensures r == 0 +{ + hide Id; + r := -1; + match Zero(Square(3)) { + case 0 => { r := 0; } + case _ => {} + } +} + +method HiddenSquare() returns (r: int) + ensures r == 0 +{ + hide Square; + r := Zero(Square(3)); + var i := 3; + while i > 0 + invariant r == 3 - i + decreases i + { + r := r+1; + i := i-1; + } + r := r - 3; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect new file mode 100644 index 00000000000..1cc06ed876c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect @@ -0,0 +1,5 @@ +FunctionHidingRefactoring.dfy(13,0): Info: Consider hiding these functions, which are unused by the proof: Square, Id +FunctionHidingRefactoring.dfy(19,0): Info: Consider hiding these functions, which are unused by the proof: Square, Id +FunctionHidingRefactoring.dfy(36,0): Info: Consider hiding this function, which is unused by the proof: Square + +Dafny program verifier finished with 12 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy deleted file mode 100644 index e9af4924f25..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy +++ /dev/null @@ -1,110 +0,0 @@ -// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --show-hints --isolate-assertions --suggest-proof-refactoring --type-system-refresh "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -//Function Hiding - -function Id(i: int): int { i } - -function Pow(i: int): int { Id(i) * Id(i) } - -function Zero(i: int): int { i * 0 } - - -method NoEffect() returns (r: int) - ensures true -{ - r := Pow(Pow(3)); -} - -method Shallow() returns (r: int) - ensures r == 3 -{ - r := Zero(Pow(3)); - r := r + 3; -} - -method Deep() returns (r: int) - ensures r == 81 -{ - if Pow(Pow(3)) > 9 { - r := 81; - } else { - r := -81; - } -} - -method HiddenId() returns (r: int) - ensures r == 0 -{ - hide Id; - r := -1; - match Zero(Pow(3)) { - case 0 => { r := 0; } - case _ => {} - } -} - -method HiddenPow() returns (r: int) - ensures r == 0 -{ - hide Pow; - r := Zero(Pow(3)); - var i := 3; - while i > 0 - invariant r == 3 - i - decreases i - { - r := r+1; - i := i-1; - } - r := r - 3; -} - -// By-proofs - -opaque predicate P() { true } - -method M() requires P() { } - -method N() ensures P() { reveal P(); } - -method NoSuggestion() -{ - N(); - M(); -} - -method Call() -{ - assert P() by { reveal P(); } - M(); -} - -method CallFixed() -{ - M() by { - assert P() by { reveal P(); } - } -} - -method Requires() - requires P() -{ - assert P(); -} - -method RequiresFixed() - requires p: P() -{ - assert P() by { - reveal p; - } -} - -method CantMove(){ - var b := P(); - assert b by { reveal P(); } - b := !b; - assert !b; -} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect deleted file mode 100644 index b9b77183bd7..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect +++ /dev/null @@ -1,10 +0,0 @@ -ProofRefactorings.dfy(16,0): Info: Consider hiding these functions, which are unused by the proof: Pow, Id -ProofRefactorings.dfy(22,0): Info: Consider hiding these functions, which are unused by the proof: Pow, Id -ProofRefactorings.dfy(39,0): Info: Consider hiding this function, which is unused by the proof: Pow -ProofRefactorings.dfy(80,10): Info: This fact was only used to prove the precondtion of the method call ProofRefactorings.dfy(81,3)-(81,6). Consider moving it into a by-proof. -ProofRefactorings.dfy(93,0): Info: Consider hiding this function, which is unused by the proof: P -ProofRefactorings.dfy(92,11): Info: This requires clause was only used to prove the assertion ProofRefactorings.dfy(94,11)-(94,11). Consider labelling it and revealing it in a by-proof. -ProofRefactorings.dfy(99,0): Info: Consider hiding this function, which is unused by the proof: P -ProofRefactorings.dfy(107,9): Info: This fact was only used to prove the assertion ProofRefactorings.dfy(109,10)-(109,10). Consider moving it into a by-proof. - -Dafny program verifier finished with 22 verified, 0 errors From 6fb3807438ffaf770bfd3c4ff183e937eaa5dcfc Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 16 Oct 2024 14:00:15 +0200 Subject: [PATCH 14/27] review --- Source/DafnyCore/Options/CommonOptionBag.cs | 7 ++- Source/DafnyCore/Options/DafnyCommands.cs | 1 + Source/DafnyCore/ProofDependencyWarnings.cs | 61 +++---------------- .../LitTest/logger/ByProofRefactoring.dfy | 61 +++++++++++++++++++ .../logger/ByProofRefactoring.dfy.expect | 9 +++ .../FunctionHidingRefactoring.dfy.expect | 4 +- 6 files changed, 88 insertions(+), 55 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 8bf23e63cea..b4e12e56073 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -288,11 +288,15 @@ May produce spurious warnings. May produce spurious warnings.") { IsHidden = true }; - public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", @" + public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", () => Options.get, @" (experimental) Emits suggestions for moving assertions into by-proofs and hiding unused function definitions. May produce spurious suggestions. Use with --show-hints on the CLI.") { IsHidden = true }; + public static readonly Option AnalyseProofs = new("--analyse-proofs", @" +(experimental) Implies --warn-contradictory-assumptions, --warn-redundant-assumptions, and --suggest-proof-refactoring") { + IsHidden = true + }; public static readonly Option VerificationCoverageReport = new("--verification-coverage-report", "Emit verification coverage report to a given directory, in the same format as a test coverage report.") { ArgumentHelpName = "directory" @@ -631,6 +635,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module); + OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module); OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module); diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index b2b95ee2e63..6ac2f5719f6 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -42,6 +42,7 @@ static DafnyCommands() { CommonOptionBag.WarnContradictoryAssumptions, CommonOptionBag.WarnRedundantAssumptions, CommonOptionBag.SuggestProofRefactoring, + CommonOptionBag.AnalyseProofs, CommonOptionBag.NoTimeStampForCoverageReport, CommonOptionBag.VerificationCoverageReport, CommonOptionBag.ExtractCounterexample, diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 2791b3e8c3f..3fa295af4a8 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -56,7 +56,7 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(string name, private static List UnusedFunctions(string implementationName, IEnumerable coveredElements, IEnumerable axioms) { - if (!(options.Get(CommonOptionBag.SuggestProofRefactoring) && manager.idsByMemberName[implementationName].Decl is Method)) { + if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) { return new List(); } @@ -65,23 +65,21 @@ private static List UnusedFunctions(string implementationName, IEnumer return unusedFunctions; } - var referencedFunctions = GetReferencedFunctions(method); - var hiddenFunctions = HiddenFunctions(referencedFunctions); var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType() .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); - unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList(); + unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList(); return unusedFunctions; - HashSet HiddenFunctions(HashSet functions) { - var hiddenFunctions = new HashSet(functions); + HashSet VisibleFunctions() { + var functions = new HashSet(); foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { - hiddenFunctions.Remove(visibleFunction); + functions.Add(visibleFunction); } - return hiddenFunctions; + return functions; Function GetFunctionFromAttributed(ICarriesAttributes construct) { var values = construct.FindAllAttributes("id"); @@ -97,47 +95,6 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) { } } - private static HashSet GetReferencedFunctions(Method method) { - var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType() : new List(); - var functionDependants = new Dictionary>(); - - foreach (var fce in functionCallsInMethod) { - var fun = fce.Function; - if (!functionDependants.ContainsKey(fun)) { - functionDependants[fun] = Dependents(fun); - } - - continue; - - IEnumerable Dependents(Function fn) { - var queue = new Queue(new[] { fn }); - var visited = new HashSet(); - while (queue.Any()) { - var f = queue.Dequeue(); - visited.Add(f); - - f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue); - continue; - - IEnumerable AllSubFunctions(Expression e) { - return e.SubExpressions.OfType().Select(fce => fce.Function) - .Concat(e.SubExpressions.SelectMany(AllSubFunctions)); - } - } - return visited.ToList(); - } - } - - var hashSet = new HashSet(); - foreach (var (f, deps) in functionDependants) { - hashSet.Add(f); - hashSet.UnionWith(deps); - } - - return hashSet; - } - - private static void WarnAboutSuspiciousDependencies(string scopeName, IReadOnlyList assertCoverage, List unusedFunctions) { var potentialDependencies = manager.GetPotentialDependenciesForDefinition(scopeName); @@ -154,7 +111,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, .ThenBy(dep => dep.Description).ToList(); foreach (var unusedDependency in unusedDependencies) { - if (options.Get(CommonOptionBag.WarnContradictoryAssumptions)) { + if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) { if (unusedDependency is ProofObligationDependency obligation) { if (ShouldWarnVacuous(scopeName, obligation)) { var message = $"proved using contradictory assumptions: {obligation.Description}"; @@ -173,7 +130,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, } } - if (options.Get(CommonOptionBag.WarnRedundantAssumptions)) { + if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) { if (unusedDependency is RequiresDependency requires) { reporter.Warning(MessageSource.Verifier, "", requires.Range, $"unnecessary requires clause"); } @@ -187,7 +144,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, } } - if (options.Get(CommonOptionBag.SuggestProofRefactoring) && manager.idsByMemberName[scopeName].Decl is Method m) { + if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method m) { SuggestFunctionHiding(unusedFunctions, m); SuggestByProofRefactoring(scopeName, assertCoverage.ToList()); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy new file mode 100644 index 00000000000..8f725c08f15 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy @@ -0,0 +1,61 @@ +// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --show-hints --isolate-assertions --suggest-proof-refactoring --type-system-refresh "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +opaque predicate P() { true } + +method M() requires P() { } + +method N() ensures P() { reveal P(); } + +method NoSuggestion() +{ + N(); + M(); +} + +method Call() +{ + assert P() by { reveal P(); } + M(); +} + +method CallFixed() +{ + M() by { + assert P() by { reveal P(); } + } +} + +method Assert() +{ + assert P() by { reveal P(); } + assert P(); +} + +method AssertFixed() +{ + assert P() by { + assert P() by { reveal P(); } + } +} + +method Requires() + requires P() +{ + assert P(); +} + +method RequiresFixed() + requires p: P() +{ + assert P() by { + reveal p; + } +} + +method CantMove(){ + var b := P(); + assert b by { reveal P(); } + b := !b; + assert !b; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect new file mode 100644 index 00000000000..41c1df51d0d --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect @@ -0,0 +1,9 @@ +ByProofRefactoring.dfy(11,0): Info: Consider hiding this function, which is unused by the proof: P +ByProofRefactoring.dfy(18,2): Info: This fact was only used to prove the precondtion of the method call ByProofRefactoring.dfy(19,3)-(19,6). Consider moving it into a by-proof. +ByProofRefactoring.dfy(31,2): Info: This fact was only used to prove the assertion ByProofRefactoring.dfy(32,3)-(32,13). Consider moving it into a by-proof. +ByProofRefactoring.dfy(44,0): Info: Consider hiding this function, which is unused by the proof: P +ByProofRefactoring.dfy(43,11): Info: This requires clause was only used to prove the assertion ByProofRefactoring.dfy(45,3)-(45,13). Consider labelling it and revealing it in a by-proof. +ByProofRefactoring.dfy(50,0): Info: Consider hiding this function, which is unused by the proof: P +ByProofRefactoring.dfy(58,2): Info: This fact was only used to prove the assertion ByProofRefactoring.dfy(60,3)-(60,12). Consider moving it into a by-proof. + +Dafny program verifier finished with 14 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect index 1cc06ed876c..fe3c1324406 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect @@ -1,5 +1,5 @@ -FunctionHidingRefactoring.dfy(13,0): Info: Consider hiding these functions, which are unused by the proof: Square, Id -FunctionHidingRefactoring.dfy(19,0): Info: Consider hiding these functions, which are unused by the proof: Square, Id +FunctionHidingRefactoring.dfy(13,0): Info: Consider hiding these functions, which are unused by the proof: Id, Square +FunctionHidingRefactoring.dfy(19,0): Info: Consider hiding these functions, which are unused by the proof: Id, Square FunctionHidingRefactoring.dfy(36,0): Info: Consider hiding this function, which is unused by the proof: Square Dafny program verifier finished with 12 verified, 0 errors From 661eaea44c3dbb04f61b656de083308ab990f102 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 16 Oct 2024 14:01:23 +0200 Subject: [PATCH 15/27] fix --- Source/DafnyCore/Options/CommonOptionBag.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index b4e12e56073..42dfe28f87a 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -288,7 +288,7 @@ May produce spurious warnings. May produce spurious warnings.") { IsHidden = true }; - public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", () => Options.get, @" + public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", @" (experimental) Emits suggestions for moving assertions into by-proofs and hiding unused function definitions. May produce spurious suggestions. Use with --show-hints on the CLI.") { IsHidden = true From 67073ee47801c4e71c16510911e819ec0a4c9b8f Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 16 Oct 2024 15:08:54 +0200 Subject: [PATCH 16/27] fix tests --- Source/DafnyCore/Options/CommonOptionBag.cs | 4 ++-- Source/DafnyCore/ProofDependencyWarnings.cs | 7 +++---- .../Diagnostics/DiagnosticsTest.cs | 4 ++-- .../Diagnostics/VerificationDiagnostics.cs | 2 +- .../Lookup/HoverVerificationTest.cs | 4 ++-- 5 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 42dfe28f87a..f1f45c1223f 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -288,7 +288,7 @@ May produce spurious warnings. May produce spurious warnings.") { IsHidden = true }; - public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", @" + public static readonly Option SuggestProofRefactoring = new("--suggest-proof-refactoring", @" (experimental) Emits suggestions for moving assertions into by-proofs and hiding unused function definitions. May produce spurious suggestions. Use with --show-hints on the CLI.") { IsHidden = true @@ -635,7 +635,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module); - OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module); + OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module); OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module); diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 3fa295af4a8..7b2a9a7c828 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -69,7 +69,7 @@ private static List UnusedFunctions(string implementationName, IEnumer .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList(); - + return unusedFunctions; HashSet VisibleFunctions() { @@ -219,8 +219,7 @@ private static void SuggestByProofRefactoring(string scopeName, } private static Dictionary> - ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList vcResults) - { + ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList vcResults) { var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName) .Where(dep => dep is not EnsuresDependency) .ToDictionary(dep => dep, _ => new HashSet { }); @@ -236,7 +235,7 @@ private static void SuggestByProofRefactoring(string scopeName, assertionsUsedByFact.TryAdd(factDependency, new HashSet()); bool NotSelfReferential(DafnyConsolePrinter.AssertCmdPartialCopy assert) => - !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) + !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency); assertionsUsedByFact[factDependency].UnionWith(asserts.Where(NotSelfReferential)); diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index df98c5a6c91..c55da2e59f7 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -76,7 +76,7 @@ method ContradictoryAssumeMethod(n: int) ); Assert.Contains(diagnostics, diagnostic => diagnostic.Severity == DiagnosticSeverity.Warning && - diagnostic.Range == new Range(13, 11, 13, 17) && + diagnostic.Range == new Range(13, 4, 13, 18) && diagnostic.Message == "proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)" ); Assert.Contains(diagnostics, diagnostic => @@ -1025,7 +1025,7 @@ method test(i: int, j: int) { Assert.Single(diagnostics); Assert.Equal(MessageSource.Verifier.ToString(), diagnostics[0].Source); Assert.Equal(DiagnosticSeverity.Error, diagnostics[0].Severity); - Assert.Equal(new Range((1, 9), (1, 23)), diagnostics[0].Range); + Assert.Equal(new Range((1, 2), (1, 24)), diagnostics[0].Range); await AssertNoDiagnosticsAreComing(CancellationToken); } diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs b/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs index 003c73d3876..a5beddbe37f 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs @@ -190,7 +190,7 @@ method ImplicitAssertions(x: int) { var document = CreateAndOpenTestDocument(source, "ErrorLimitReached.dfy"); var diagnostics = await GetLastDiagnostics(document, DiagnosticSeverity.Hint); Assert.Contains(diagnostics, d => d.Message.Contains("Implicit assertion: non-zero divisor")); - Assert.Contains(diagnostics, d => d.Message.Contains("Explicit assertion: assert statement") && d.Range == new Range(2, 11, 2, 16)); + Assert.Contains(diagnostics, d => d.Message.Contains("Explicit assertion: assert statement") && d.Range == new Range(2, 4, 2, 17)); } public VerificationDiagnostics(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) { diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 64a9c4bb905..2cd8dea1851 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -138,8 +138,8 @@ await AssertVerificationHoverMatches(documentItem, (0, 36), - Total resource usage: ??? RU - Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches): - - #???/??? with 1 assertion at line ???, ??? RU - - #???/??? with 1 assertion at line ???, ??? RU" + - #???/??? with 1 assertion??? at line ???, ??? RU??? + - #???/??? with 1 assertion??? at line ???, ??? RU" ); } From e3ca1721d6567d0064bbbc7910ddf3e81f3b24c8 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 00:45:09 +0200 Subject: [PATCH 17/27] use different token --- Source/DafnyCore/Verifier/ProofDependency.cs | 4 ++-- .../BoogieGenerator.TrPredicateStatement.cs | 2 +- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1531 -> 1539 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1552 -> 1560 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1522 -> 1530 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 2040 -> 2048 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1511 -> 1519 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1518 -> 1526 bytes .../binaries/DafnyStandardLibraries.doo | Bin 57225 -> 57233 bytes 9 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index ac3147d235c..7f3b75b7da7 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -61,7 +61,7 @@ public class ProofObligationDependency : ProofDependency { $"{ProofObligation.SuccessDescription}"; public ProofObligationDependency(Microsoft.Boogie.IToken tok, ProofObligationDescription proofObligation) { - Range = BoogieGenerator.ToDafnyToken(true, tok).ToRange(); + Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.RangeToken ?? BoogieGenerator.ToDafnyToken(true, tok).ToRange(); ProofObligation = proofObligation; } } @@ -75,7 +75,7 @@ public class AssumedProofObligationDependency : ProofDependency { $"assumption that {ProofObligation.SuccessDescription}"; public AssumedProofObligationDependency(IToken tok, ProofObligationDescription proofObligation) { - Range = tok as RangeToken ?? new RangeToken(tok, tok); + Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.RangeToken ?? new RangeToken(tok, tok); ProofObligation = proofObligation; } } diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs index 6aa63b5f0e9..39d271c2c56 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs @@ -153,7 +153,7 @@ private bool TrAssertCondition(PredicateStmt stmt, var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes); var splits = TrSplitExpr(proofBuilder.Context, stmt.Expr, etran, true, out var splitHappened); if (!splitHappened) { - IToken tok = enclosingToken == null ? stmt.RangeToken : new NestedToken(enclosingToken, stmt.RangeToken); + var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr)); var desc = new AssertStatementDescription(stmt, errorMessage, successMessage); proofBuilder.Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok, proofBuilder.Context, etran.TrAttributes(stmt.Attributes, null))); diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 3c0752af411a0b6aa604ae8390ce750d7c54d5de..8d3d20da486875700188c6493ccfca56147e8afe 100644 GIT binary patch delta 470 zcmey(-OM8%;LXe;!oa}5!LY3{AhPI-NOTJ$1B2E?ak={LJEA6U<*HulS7imV#B^@z z^qMk#%B&yXy>G63EVB391m<%*&YIIbIQ8oTrf}`AskWTwKfkY?Vd8V!Usb=Vq9k-r zKHz43;x#eA>i6T*ZZ>b{*v~(A{P20B(B?1K8H2RK+0C^gbCsNe_B1o9JMx#_y=z>t zT7&20&qJXHuGfdJuUGJ~v3Zcte2#CSMR{zB^)+ETwh76C{cf{L)YQ&OAAh=UmtvE^ zm7grWfw76xH}ssJ?z^UnCEV7A{1*Y~I3nmYEkNf+qK|>M;XFChupJW?Vn{Hmej{ JEh{h{834@N&RPHf delta 505 zcmZqX`OPgJ;LXe;!oa}5!BCavAGz3(C%1-?fkAkpxLiH=eNmIQa#b(&tFi)FVmdc< zdQF)=W!97L-Zxi17TJ4_hkcHsv*vRT&hzyFQ@HlmR7?6D_dl%Y@Z`2!t!OsHmU?K+{rfRhd0v{|{Ql(+KWsj8RpD=G!<17;4^H(83wH77DmQqb^J3w;&DCt{ zMOzgu<9BfV`1Sq;Ykf=SadsJ>7de7m+uwEPoUS_5&R{9_F=I(&deWsmg)#3IODl0W z&h@__a#gfU@^y&Q_SKiH=0C`ayV#>;6|i*T=C7MAGg$c)4yslOPxz~4dokaf`{pSL z<#iv$?jL*N?eJWE!v2W!uS%K%^u&Hnlu+Ih5}Wg;x^>-|2P?nv94=?9zb1J^Y}4UM zhoYU1w+b6JSwt`Qo7VB?*|wc8dbMMwNAtDw+%yFO-&i|Q{YvcZ z?g#@D>vqw9^1JzwqJt^TfAb#3v&_6G5i@xjtDZebWRke$zm?1k3`hAH7}$Xk2m?zR emjffPpeR4RC^0v{o0SbD!32Z_K)RF_!~+0q=+m13 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index 58f5da1d665ecb6d2579eca11584c3c9c0e2c5e3..b7a7ceeeb432fd0db8932b614dad48085b29d0c1 100644 GIT binary patch delta 492 zcmbQhGlNGwz?+#xgn@y9gW*VHKxEMuk?0mi1_rH(;&S!fcSKFz%2mD8ugVH!iRs+b z={05glvzK%d*597SY+?H3C!nsoHeI=aO&3wOySyJQ*AlVe|}#(!^G#dzp8#!MM>zM ze8A26#A{-J)$hlr-E7{@v7dkL_~G+Lq0L{eGX`mevzu#0<|;V_?P+FIcjPaubVxY!i|N``u=hsHvTmKK^vyF2yE+ zD?eF$17j1XZ|qYo*{QYmGiTm1QQsAdm_wy3qU~lkg*{*pidkgNcys7J1WjJdswWQ;NjS6k-9Bap1|9(h X26kXX!oZTo^^-raO0i911&IIvLKo6m delta 483 zcmbQiGl54uz?+#xgn@y9gP|$SKXS1nPi_q(1B38Hak+Z#`=Taq<*HulS7imV#B^@z z^qMk#%B&~fy>G63EVB0;5BnTNXU*pxoagHUrf}`Ash0FR?tfU(;mK{eTH88Xy`E_) zA7(NYE%nft`}bq2^1L*^`Tffue%O5Gs>0vWhAF3x9-QhG7VP5DRc`P==f%Qxo2%K@ zi?%9S#_!?y&q`wYlq@9%tBZc=(?8 z-TY5E%g>fX=~ii8>}370^@QD(Nu{<`3;ga?ZP#6Y|H~B*HSM{_*M&LnzOif6kC=H;B4+YxRy}5*$mBb$(u&K0QB_cspI(%h8{o~# R28>1qCLk;T(p{_|9stze&@=!5 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index c874419dd2261746fd893672223cd9937e19fa86..45bfa768a27e7f3e6e54d22ae109d8ebcab92dcf 100644 GIT binary patch delta 513 zcmeyw{fk>Xz?+#xgn@y9gJD-=KxEMuk?0mi1_rH(;&S!fcSKFz%2mD8ugVH!iRs+b z={05glvzK%d*597SY+?H3C!nsoHeI=aO&3wOySyJQ*AlVe|}#(!^G#dzp8#!MM>zM ze8A26#A{-J)$hlr-E7{@v7dkL_~G+Lq0L{eGX`mevzu#0<|;V_?P+FIcjPaubVxY!i|N``u=hsHvTmKK^vyF2yE+ zD?eF$17j1XZ|qYo*{QYmGiTm1QQsAdm_wy3qU~lkg*{*pidkgNcysG63EVB0;5BnTNXU*pxoagHUrf}`Ash0FR?tfU(;mK{eTH88Xy`E_) zA7(NYE%nft`}bq2^1L*^`Tffue%O5Gs>0vWhAF3x9-QhG7VP5DRc`P==f%Qxo2%K@ zi?%9S#_!?y&q`wYlq@9%tBZc=(?8 z-TY5E%g>fX=~ii8>}370^@QD(Nu{<`3;ga?ZP#6Y|H~B*HSM{_*M&LnzOif6N0@n0B4%G63EVB391m<%*&YIIbIQ8oTrf}`AskWTwKfkY?Vd8V!Usb=Vq9k-r zKHz43;x#eA>i6T*ZZ>b{*v~(A{P20B(B?1K8H2RK+0C^gbCsNe_B1o9JMx#_y=z>t zT7&20&qJXHuGfdJuUGJ~v3Zcte2#CSMR{zB^)+ETwh76C{cf{L)YQ&OAAh=UmtvE^ zm7grWfw76xH}ssJ?z^UnCEV7A{1*Y~I3nij@~7f+lyf>oEgGChuXFR$LE^vVx-g Y^rFPv0B=?{V01Dt0bv1OsHmU?K+{rfRhd0v{|{Ql(+KWsj8RpD=G!<17;4^H(83wH77DmQqb^J3w;&DCt{ zMOzgu<9BfV`1Sq;Ykf=SadsJ>7de7m+uwEPoUS_5&R{9_F=I(&deWsmg)#3IODl0W z&h@__a#gfU@^y&Q_SKiH=0C`ayV#>;6|i*T=C7MAGg$c)4yslOPxz~4dokaf`{pSL z<#iv$?jL*N?eJWE!v2W!uS%K%^u&Hnlu+Ih5}Wg;x^>-|2P?nv94=?9zb1J^Y}4UM zhoYU1w+b6JSwt`Qo7VB?*|wc8dbMMwNAtDw+%yFO-&i|Q{YvcZ z?g#@D>vqw9^1JzwqJt^TfAb#3Q>?rw5i@x*yPiBqWWko6zspz|7@o>7Ft7t75C)bs OE}#5>U5c#;EC>Kra?(No diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index 91e26f57c5d9cae99142e83b4a172524e3d666a9..84aafd4cbd28272ffff14c976854a2197990968d 100644 GIT binary patch delta 491 zcmaFP{hnJqz?+#xgn@y9gJFGRKxEMuk?0mi1_rH(;&S!fcSKFz%2mD8ugVH!iRs+b z={05glvzK%d*597SY+?H3C!nsoHeI=aO&3wOySyJQ*AlVe|}#(!^G#dzp8#!MM>zM ze8A26#A{-J)$hlr-E7{@v7dkL_~G+Lq0L{eGX`mevzu#0<|;V_?P+FIcjPaubVxY!i|N``u=hsHvTmKK^vyF2yE+ zD?eF$17j1XZ|qYo*{QYmGiTm1QQsAdm_wy3qU~lkg*{*pidkgNcysT0yoyiK~0RU`i(B%LC delta 484 zcmaFQ{hV7oz?+#xgn@y9gP}alKXS1nPi_q(1B38Hak+Z#`=Taq<*HulS7imV#B^@z z^qMk#%B&~fy>G63EVB0;5BnTNXU*pxoagHUrf}`Ash0FR?tfU(;mK{eTH88Xy`E_) zA7(NYE%nft`}bq2^1L*^`Tffue%O5Gs>0vWhAF3x9-QhG7VP5DRc`P==f%Qxo2%K@ zi?%9S#_!?y&q`wYlq@9%tBZc=(?8 z-TY5E%g>fX=~ii8>}370^@QD(Nu{<`3;ga?ZP#6Y|H~B*HSM{_*M&LnzOif6JDGV=B4%zM ze8A26#A{-J)$hlr-E7{@v7dkL_~G+Lq0L{eGX`mevzu#0<|;V_?P+FIcjPaubVxY!i|N``u=hsHvTmKK^vyF2yE+ zD?eF$17j1XZ|qYo*{QYmGiTm1QQsAdm_wy3qU~lkg*{*pidkgNcysG63EVB0;5BnTNXU*pxoagHUrf}`Ash0FR?tfU(;mK{eTH88Xy`E_) zA7(NYE%nft`}bq2^1L*^`Tffue%O5Gs>0vWhAF3x9-QhG7VP5DRc`P==f%Qxo2%K@ zi?%9S#_!?y&q`wYlq@9%tBZc=(?8 z-TY5E%g>fX=~ii8>}370^@QD(Nu{<`3;ga?ZP#6Y|H~B*HSM{_*M&LnzOif62bg(LB4%c)V`b2k#-HZw9X=u8yXulJhb?dALD_tHmK3dQ!G z<6)np=&bqNgY$fS;1sU?HPw=S$Ndj0Iy_13ud}SPy(gi2@_{ky6R(K@R=*#YD$h&v zo8Q0u;fKv&`q_`7PscIpa0SBj2`EPd-#1?R30V z*s#gs_9j2EDSw`A+xg;<=(_E~{Ovq<-dJ!Jv$@O6s^9f+?mDN(8S6Jbte3hY|Kg_K z?3Y{CdCrMoi0^*0`JPrpy<&j+^tj5?uP57{Ho9q8@uq0&zg@T1&QuTiqaem}_FPK) zkNNklQ6u3E_oR;&cNsSCW(>K@ixMl7W$x=S14SnL-j`Nf2aKnJqWtut#M}UHRyJT9 PGB5#Q0g&dt58?p;vX|QP delta 483 zcmbQZpSg2Cvv`0vGm8iV0|N&`X_|jzcdX~RYDNYI(TU>v^{1A2d-;C)z4Xx)PqDq{ zc-ZGCPCj86eDHC6i1Nef`TBk@or_4~wwor{d72(+$tS|ji7zre@l z-oqz{9&`unD~V5uHxs&7&w3)#WYOe2Tj9xPrH>a$-xYB65KC%I%W$+f6QS;TcU{)& zn#Rr5sphLB4)nOq+dKd4L9GHN--Q=uH`%SbB>b1Jd(!$I%g0jhU)`RuNQI}6>2Lej zH3!u^iawqAeq_eNsZvFcZ)o#ua#(W9nCHIe4Y7du6a3z6`K-*`;z=yL`~2$X+6W#! zn_Ik*JKQ2Z-||h`gJ_Qq>00HRqR)$VS*@9=Zt_PV%;)U;hrR#Lzn4V~{5RZ_ zK3d#mU`VN9WngDu*nFDN=PoZwtV~w9uO|-@K~oBhKL}XTxNLIaeJM8P`yf656aUnN From 3c4be2facb4716ffea78f86ff7a376cdd6feab2d Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 01:29:32 +0200 Subject: [PATCH 18/27] review --- Source/DafnyCore/DafnyConsolePrinter.cs | 21 +++--- Source/DafnyCore/ProofDependencyWarnings.cs | 68 ++++++++----------- .../Legacy/LegacyJsonVerificationLogger.cs | 4 +- .../Legacy/LegacyVerificationResultLogger.cs | 2 +- .../logger/ByProofRefactoring.dfy.expect | 2 +- 5 files changed, 45 insertions(+), 52 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index b948d235b12..258aaf04c3b 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -9,6 +9,17 @@ namespace Microsoft.Dafny; +public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id); +public record VerificationRunResultPartialCopy( + int VCNum, + DateTime StartTime, + TimeSpan RunTime, + SolverOutcome Outcome, + List Asserts, + IEnumerable CoveredElements, + IEnumerable AvailableAxioms, + int ResourceCount); + public class DafnyConsolePrinter : ConsolePrinter { public new DafnyOptions Options { get => options; @@ -21,16 +32,6 @@ public class DafnyConsolePrinter : ConsolePrinter { private DafnyOptions options; public record ImplementationLogEntry(string Name, Boogie.IToken Tok); - public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id); - public record VerificationRunResultPartialCopy( - int VCNum, - DateTime StartTime, - TimeSpan RunTime, - SolverOutcome Outcome, - List Asserts, - IEnumerable CoveredElements, - IEnumerable AvailableAxioms, - int ResourceCount); public record VerificationResultLogEntry( VcOutcome Outcome, TimeSpan RunTime, diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 7b2a9a7c828..c202f32ad38 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -40,7 +40,7 @@ public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(Dafn if (result.Outcome != VcOutcome.Correct) { continue; } - var unusedFunctions = UnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); + var unusedFunctions = GetUnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms)); WarnAboutSuspiciousDependencies(implementation.Name, result.VCResults, unusedFunctions); } } @@ -50,36 +50,27 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(string name, if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } - var unusedFunctions = UnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms)); + var unusedFunctions = GetUnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.SelectMany(r => r.DeclarationsAfterPruning.OfType())); WarnAboutSuspiciousDependencies(name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions); } - private static List UnusedFunctions(string implementationName, IEnumerable coveredElements, + private static IEnumerable GetUnusedFunctions(string implementationName, IEnumerable coveredElements, IEnumerable axioms) { if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) { return new List(); } - var unusedFunctions = new List(); - if (manager.idsByMemberName[implementationName].Decl is not Method method) { - return unusedFunctions; + if (manager.idsByMemberName[implementationName].Decl is not Method) { + return new List(); } var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType() - .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); - - unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList(); - - return unusedFunctions; + .Select(dep => dep.function).Distinct(); - HashSet VisibleFunctions() { - var functions = new HashSet(); - - foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { - functions.Add(visibleFunction); - } + return GetVisibleFunctions().Except(usedFunctions); - return functions; + HashSet GetVisibleFunctions() { + return axioms.Select(GetFunctionFromAttributed).Where(f => f != null).ToHashSet(); Function GetFunctionFromAttributed(ICarriesAttributes construct) { var values = construct.FindAllAttributes("id"); @@ -96,7 +87,7 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) { } private static void WarnAboutSuspiciousDependencies(string scopeName, - IReadOnlyList assertCoverage, List unusedFunctions) { + IReadOnlyList assertCoverage, IEnumerable unusedFunctions) { var potentialDependencies = manager.GetPotentialDependenciesForDefinition(scopeName); var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements); var usedDependencies = @@ -144,28 +135,28 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, } } - if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method m) { - SuggestFunctionHiding(unusedFunctions, m); + if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) { + SuggestFunctionHiding(unusedFunctions, method); SuggestByProofRefactoring(scopeName, assertCoverage.ToList()); } } - private static void SuggestFunctionHiding(List unusedFunctions, Method m) { + private static void SuggestFunctionHiding(IEnumerable unusedFunctions, Method method) { if (unusedFunctions.Any()) { - reporter.Info(MessageSource.Verifier, m.Body.StartToken, - $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); + reporter.Info(MessageSource.Verifier, method.Body.StartToken, + $"Consider hiding {(unusedFunctions.Count() > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}"); } } private static void SuggestByProofRefactoring(string scopeName, - IReadOnlyList verificationRunResults) { - foreach (var (dep, lAsserts) in ComputeAssertionsUsedByFact(scopeName, verificationRunResults)) { + IReadOnlyList verificationRunResults) { + foreach (var (dep, lAsserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) { var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1; if (!factIsOnlyUsedByOneAssertion) { continue; } - DafnyConsolePrinter.AssertCmdPartialCopy cmd = null; + AssertCmdPartialCopy cmd = null; foreach (var assert in lAsserts) { cmd = assert; } @@ -201,7 +192,7 @@ private static void SuggestByProofRefactoring(string scopeName, switch (consumer) { case CallDependency call: { - factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.RangeString()}"; + factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.Range.Next.TokenToString(options)}"; break; } case ProofObligationDependency { ProofObligation: AssertStatementDescription }: { @@ -218,31 +209,32 @@ private static void SuggestByProofRefactoring(string scopeName, } } - private static Dictionary> - ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList vcResults) { - var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName) + private static Dictionary> + ComputeAssertionsProvenUsingFact(string scopeName, IReadOnlyList verificationRunResults) { + var assertionsProvenUsingFact = manager.GetPotentialDependenciesForDefinition(scopeName) + // Filter out noise .Where(dep => dep is not EnsuresDependency) - .ToDictionary(dep => dep, _ => new HashSet { }); + .ToDictionary(dep => dep, _ => new HashSet { }); - foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) { - foreach (var factReference in usedFacts) { + foreach (var verificationRun in verificationRunResults) { + foreach (var factReference in verificationRun.CoveredElements) { var factDependency = manager.GetFullIdDependency(factReference); var excludedDependencies = factDependency is EnsuresDependency; if (excludedDependencies) { continue; } - assertionsUsedByFact.TryAdd(factDependency, new HashSet()); + assertionsProvenUsingFact.TryAdd(factDependency, new HashSet()); - bool NotSelfReferential(DafnyConsolePrinter.AssertCmdPartialCopy assert) => + bool IsNotSelfReferential(AssertCmdPartialCopy assert) => !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency); - assertionsUsedByFact[factDependency].UnionWith(asserts.Where(NotSelfReferential)); + assertionsProvenUsingFact[factDependency].UnionWith(verificationRun.Asserts.Where(IsNotSelfReferential)); } } - return assertionsUsedByFact; + return assertionsProvenUsingFact; } /// diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index 683092cf02b..93087fe8e5d 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -35,12 +35,12 @@ public DummyProofObligationDescription(string success) { } - private JsonNode SerializeVcResult(IEnumerable potentialDependencies, DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) { + private JsonNode SerializeVcResult(IEnumerable potentialDependencies, VerificationRunResultPartialCopy verificationRunResult) { var runResult = VCResultLogEntryToPartialVerificationRunResult(verificationRunResult); return JsonVerificationLogger.SerializeVcResult(depManager, potentialDependencies?.ToList(), runResult); } - public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) { + public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(VerificationRunResultPartialCopy verificationRunResult) { var mockNumber = 42; var mockAsserts = verificationRunResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description))); var runResult = new VerificationRunResult(verificationRunResult.VCNum, mockNumber, verificationRunResult.StartTime, verificationRunResult.Outcome, verificationRunResult.RunTime, mockNumber, null!, diff --git a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs index 4f182bdf842..928e8d6d3c2 100644 --- a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs @@ -72,7 +72,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa )); } - private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { + private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { var testResults = new List(); foreach (var ((verbName, currentFile), vcResults) in verificationResults) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect index 41c1df51d0d..948d0eaff06 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect @@ -1,5 +1,5 @@ ByProofRefactoring.dfy(11,0): Info: Consider hiding this function, which is unused by the proof: P -ByProofRefactoring.dfy(18,2): Info: This fact was only used to prove the precondtion of the method call ByProofRefactoring.dfy(19,3)-(19,6). Consider moving it into a by-proof. +ByProofRefactoring.dfy(18,2): Info: This fact was only used to prove the precondtion of the method call ByProofRefactoring.dfy(19,3). Consider moving it into a by-proof. ByProofRefactoring.dfy(31,2): Info: This fact was only used to prove the assertion ByProofRefactoring.dfy(32,3)-(32,13). Consider moving it into a by-proof. ByProofRefactoring.dfy(44,0): Info: Consider hiding this function, which is unused by the proof: P ByProofRefactoring.dfy(43,11): Info: This requires clause was only used to prove the assertion ByProofRefactoring.dfy(45,3)-(45,13). Consider labelling it and revealing it in a by-proof. From a0e8acc3c8654718ac1df0383e65e917e51cea50 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 01:45:55 +0200 Subject: [PATCH 19/27] fix tests --- Source/DafnyCore/Verifier/ProofDependency.cs | 2 +- .../Diagnostics/DiagnosticsTest.cs | 4 ++-- .../Diagnostics/VerificationDiagnostics.cs | 2 +- .../Lookup/HoverVerificationTest.cs | 4 ++-- ...ProofDependencies.dfy_combined.html.expect | 24 +++++++++---------- ...endencies.dfy_combined_limited.html.expect | 7 +++--- ...fDependencies.dfy_verification.html.expect | 24 +++++++++---------- .../LitTest/logger/ProofDependencyLogging.dfy | 2 +- .../logger/ProofDependencyWarnings.dfy.expect | 8 +++---- .../ProofDependencyWarnings.dfy.expect2 | 8 +++---- 10 files changed, 42 insertions(+), 43 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index 7f3b75b7da7..551a11e85f5 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -61,7 +61,7 @@ public class ProofObligationDependency : ProofDependency { $"{ProofObligation.SuccessDescription}"; public ProofObligationDependency(Microsoft.Boogie.IToken tok, ProofObligationDescription proofObligation) { - Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.RangeToken ?? BoogieGenerator.ToDafnyToken(true, tok).ToRange(); + Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.RangeToken ?? BoogieGenerator.ToDafnyToken(true, tok).ToRange(); ProofObligation = proofObligation; } } diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index c55da2e59f7..df98c5a6c91 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -76,7 +76,7 @@ method ContradictoryAssumeMethod(n: int) ); Assert.Contains(diagnostics, diagnostic => diagnostic.Severity == DiagnosticSeverity.Warning && - diagnostic.Range == new Range(13, 4, 13, 18) && + diagnostic.Range == new Range(13, 11, 13, 17) && diagnostic.Message == "proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)" ); Assert.Contains(diagnostics, diagnostic => @@ -1025,7 +1025,7 @@ method test(i: int, j: int) { Assert.Single(diagnostics); Assert.Equal(MessageSource.Verifier.ToString(), diagnostics[0].Source); Assert.Equal(DiagnosticSeverity.Error, diagnostics[0].Severity); - Assert.Equal(new Range((1, 2), (1, 24)), diagnostics[0].Range); + Assert.Equal(new Range((1, 9), (1, 23)), diagnostics[0].Range); await AssertNoDiagnosticsAreComing(CancellationToken); } diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs b/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs index a5beddbe37f..003c73d3876 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs @@ -190,7 +190,7 @@ method ImplicitAssertions(x: int) { var document = CreateAndOpenTestDocument(source, "ErrorLimitReached.dfy"); var diagnostics = await GetLastDiagnostics(document, DiagnosticSeverity.Hint); Assert.Contains(diagnostics, d => d.Message.Contains("Implicit assertion: non-zero divisor")); - Assert.Contains(diagnostics, d => d.Message.Contains("Explicit assertion: assert statement") && d.Range == new Range(2, 4, 2, 17)); + Assert.Contains(diagnostics, d => d.Message.Contains("Explicit assertion: assert statement") && d.Range == new Range(2, 11, 2, 16)); } public VerificationDiagnostics(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) { diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 2cd8dea1851..64a9c4bb905 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -138,8 +138,8 @@ await AssertVerificationHoverMatches(documentItem, (0, 36), - Total resource usage: ??? RU - Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches): - - #???/??? with 1 assertion??? at line ???, ??? RU??? - - #???/??? with 1 assertion??? at line ???, ??? RU" + - #???/??? with 1 assertion at line ???, ??? RU + - #???/??? with 1 assertion at line ???, ??? RU" ); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect index d62764dd7ab..e5b6841d23d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect @@ -192,22 +192,22 @@ method {:testEntry} RedundantAssumeMethod(n: int) // either one or the other assumption shouldn't be covered assume n > 4; assume n > 3; - assert n > 1; -} + assert n > 1; +} method {:testEntry} ContradictoryAssumeMethod(n: int) { assume n > 0; assume n < 0; assume n == 5; // shouldn't be covered - assert n < 10; // shouldn't be covered + assert n < 10; // shouldn't be covered } method {:testEntry} AssumeFalseMethod(n: int) { assume n == 15; // shouldn't be covered assume false; - assert n < 10; // shouldn't be covered + assert n < 10; // shouldn't be covered } // Obvious contradiction in requires clauses. @@ -216,7 +216,7 @@ function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat) requires x < 10 ensures r < x // only provable vacuously { - assert x == 10; // contradicts both requires clauses + assert x == 10; // contradicts both requires clauses x - 1 // not necessarily a valid nat } @@ -225,7 +225,7 @@ method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat requires x < 10 ensures r < x // only provable vacuously { - assert x == 10; // contradicts both requires clauses + assert x == 10; // contradicts both requires clauses return x - 1; // not necessarily a valid nat } @@ -377,8 +377,8 @@ method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int) // False antecedent assert statement. method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) { var y := x*x; - assert y < 0 ==> x < 0; -} + assert y < 0 ==> x < 0; +} // False antecedent ensures clause. method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int) @@ -449,8 +449,8 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns ( method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) { assume x == x + 1; - assert false; -} + assert false; +} class C { var x: int @@ -465,8 +465,8 @@ function {:testEntry} GetX(c: C): int method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) { assume true; - assert 1 + x == x + 1; -} + assert 1 + x == x + 1; +} } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 1709907f977..1e9dd0cc5e5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -10,7 +10,7 @@

ProofDependencies.dfy, Combined Coverage Report

@@ -454,17 +454,16 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns ( class C { var x: int - constructor() {} } function {:testEntry} GetX(c: C): int reads c { - c.x + c.x } method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) { - assume true; + assume true; assert 1 + x == x + 1; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect index 190aaf70aed..17c0fdc81c1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect @@ -192,22 +192,22 @@ method {:testEntry} RedundantAssumeMethod(n: int) // either one or the other assumption shouldn't be covered assume n > 4; assume n > 3; - assert n > 1; -} + assert n > 1; +} method {:testEntry} ContradictoryAssumeMethod(n: int) { assume n > 0; assume n < 0; assume n == 5; // shouldn't be covered - assert n < 10; // shouldn't be covered + assert n < 10; // shouldn't be covered } method {:testEntry} AssumeFalseMethod(n: int) { assume n == 15; // shouldn't be covered assume false; - assert n < 10; // shouldn't be covered + assert n < 10; // shouldn't be covered } // Obvious contradiction in requires clauses. @@ -216,7 +216,7 @@ function {:testEntry} ObviouslyContradictoryRequiresFunc(x: nat): (r: nat) requires x < 10 ensures r < x // only provable vacuously { - assert x == 10; // contradicts both requires clauses + assert x == 10; // contradicts both requires clauses x - 1 // not necessarily a valid nat } @@ -225,7 +225,7 @@ method {:testEntry} ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat requires x < 10 ensures r < x // only provable vacuously { - assert x == 10; // contradicts both requires clauses + assert x == 10; // contradicts both requires clauses return x - 1; // not necessarily a valid nat } @@ -377,8 +377,8 @@ method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int) // False antecedent assert statement. method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) { var y := x*x; - assert y < 0 ==> x < 0; -} + assert y < 0 ==> x < 0; +} // False antecedent ensures clause. method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int) @@ -449,8 +449,8 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns ( method {:testEntry} DontWarnAboutVacuousAssertFalse(x: int) { assume x == x + 1; - assert false; -} + assert false; +} class C { var x: int @@ -465,8 +465,8 @@ function {:testEntry} GetX(c: C): int method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) { assume true; - assert 1 + x == x + 1; -} + assert 1 + x == x + 1; +} } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy index 1c2dbb7fde8..a51792b658f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy @@ -3,7 +3,7 @@ // CHECK: Results for M.RedundantAssumeMethod \(correctness\) // CHECK: Proof dependencies: // CHECK: ProofDependencies.dfy\(177,12\)-\(177,16\): assume statement -// CHECK: ProofDependencies.dfy\(178,12\)-\(178,16\): assertion always holds +// CHECK: ProofDependencies.dfy\(178,5\)-\(178,17\): assertion always holds // // CHECK: Results for M.ContradictoryAssumeMethod \(correctness\) // CHECK: Proof dependencies: diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect index dad3df68ca3..bbf5342ab20 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect @@ -1,12 +1,12 @@ ProofDependencies.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement ProofDependencies.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement -ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(186,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement -ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) -ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(193,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(202,2): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat' ProofDependencies.dfy(209,10): Warning: ensures clause proved using contradictory assumptions -ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(211,2): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat' ProofDependencies.dfy(226,11): Warning: unnecessary requires clause ProofDependencies.dfy(241,11): Warning: unnecessary requires clause diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2 b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2 index 6e17778f8ee..ad7ef92c378 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2 +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect2 @@ -1,13 +1,13 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format ProofDependencies.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement ProofDependencies.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement -ProofDependencies.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(186,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement -ProofDependencies.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) -ProofDependencies.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(193,4): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(202,2): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat' ProofDependencies.dfy(209,10): Warning: ensures clause proved using contradictory assumptions -ProofDependencies.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) +ProofDependencies.dfy(211,2): Warning: proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.) ProofDependencies.dfy(212,11): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat' ProofDependencies.dfy(226,11): Warning: unnecessary requires clause ProofDependencies.dfy(241,11): Warning: unnecessary requires clause From 7f7f92dc0b86d4dc7b3be42e997a69b1fa0b9374 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 08:41:32 +0200 Subject: [PATCH 20/27] fix tests --- Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs | 2 +- .../logger/ProofDependencies.dfy_combined_limited.html.expect | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index df98c5a6c91..9b1194c1f4c 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -76,7 +76,7 @@ method ContradictoryAssumeMethod(n: int) ); Assert.Contains(diagnostics, diagnostic => diagnostic.Severity == DiagnosticSeverity.Warning && - diagnostic.Range == new Range(13, 11, 13, 17) && + diagnostic.Range == new Range(13, 4, 13, 18) && diagnostic.Message == "proved using contradictory assumptions: assertion always holds. (Use the `{:contradiction}` attribute on the `assert` statement to silence.)" ); Assert.Contains(diagnostics, diagnostic => diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 1e9dd0cc5e5..10bf59ea072 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -10,7 +10,7 @@

ProofDependencies.dfy, Combined Coverage Report

From 9bedde6bf586a3773afedfb54f209021b8a9b547 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 11:08:35 +0200 Subject: [PATCH 21/27] try update --- .github/workflows/doc-tests.yml | 2 +- .github/workflows/integration-tests-reusable.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index c6a68115327..212fe5d6520 100644 --- a/.github/workflows/doc-tests.yml +++ b/.github/workflows/doc-tests.yml @@ -37,7 +37,7 @@ jobs: path: dafny - name: Load Z3 run: | - sudo apt-get install -qq libarchive-tools + sudo apt-get update && sudo apt-get install -qq libarchive-tools mkdir -p dafny/Binaries/z3/bin wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - mv z3-* dafny/Binaries/z3/bin/ diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 7dc0d80617f..3df76e1caea 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -142,7 +142,7 @@ jobs: - name: Load Z3 if: "!inputs.all_platforms" run: | - sudo apt-get install -qq libarchive-tools + sudo apt-get update && sudo apt-get install -qq libarchive-tools mkdir -p dafny/Binaries/z3/bin wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - mv z3-4.12.1 dafny/Binaries/z3/bin/ From 804aa4c1a2d4587431bee22da8f8cff57c273d81 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 12:06:40 +0200 Subject: [PATCH 22/27] try fix test --- .../ProofDependencies.dfy_combined_limited.html.expect | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 10bf59ea072..910cc8a5da9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -377,7 +377,7 @@ method {:testEntry} FalseAntecedentRequiresClauseMethod(x: int) returns (r: int) // False antecedent assert statement. method {:testEntry} FalseAntecedentAssertStatementMethod(x: int) { var y := x*x; - assert y < 0 ==> x < 0; + assert y < 0 ==> x < 0; } // False antecedent ensures clause. @@ -459,11 +459,11 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns ( function {:testEntry} GetX(c: C): int reads c { - c.x + c.x } method {:testEntry} DontWarnAboutUnusedAssumeTrue(x: int) { - assume true; + assume true; assert 1 + x == x + 1; } From f6d6f60c73f216d9009ded2fb4f2ab740daa10f6 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 12:38:42 +0200 Subject: [PATCH 23/27] try fix test --- .../logger/ProofDependencies.dfy_combined_limited.html.expect | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 910cc8a5da9..1f42fd81bad 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -454,6 +454,7 @@ method {:testEntry} ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns ( class C { var x: int + constructor() {} } function {:testEntry} GetX(c: C): int From cfb066d30b6993c016e30231c37bbf7152ccad27 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 18:04:13 +0200 Subject: [PATCH 24/27] review --- Source/DafnyCore/Options/CommonOptionBag.cs | 18 ++++++++---- Source/DafnyCore/Options/DafnyCommands.cs | 2 +- Source/DafnyCore/ProofDependencyWarnings.cs | 32 ++++++++++----------- 3 files changed, 29 insertions(+), 23 deletions(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index f1f45c1223f..b8f5813f2c8 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -293,10 +293,15 @@ May produce spurious warnings. May produce spurious suggestions. Use with --show-hints on the CLI.") { IsHidden = true }; - public static readonly Option AnalyseProofs = new("--analyse-proofs", @" -(experimental) Implies --warn-contradictory-assumptions, --warn-redundant-assumptions, and --suggest-proof-refactoring") { - IsHidden = true - }; + public static readonly Option AnalyzeProofs = new("--analyze-proofs", @" +Uses data from to prover to suggest ways to refine the proof: +Warning if any assertions are proved based on contradictory assumptions (vacuously). +Warning if any `requires` clause or `assume` statement was not needed to complete verification. +Suggestions for moving assertions into by-proofs and hiding unused function definitions. +May slow down verification slightly, or make it more brittle. +May produce spurious warnings. +Use the `{:contradiction}` attribute to mark any `assert` statement intended to be part of a proof by contradiction. +"); public static readonly Option VerificationCoverageReport = new("--verification-coverage-report", "Emit verification coverage report to a given directory, in the same format as a test coverage report.") { ArgumentHelpName = "directory" @@ -527,6 +532,9 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, DafnyOptions.RegisterLegacyBinding(SuggestProofRefactoring, (options, value) => { if (value) { options.TrackVerificationCoverage = true; } }); + DafnyOptions.RegisterLegacyBinding(AnalyzeProofs, (options, value) => { + if (value) { options.TrackVerificationCoverage = true; } + }); DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; }); @@ -635,7 +643,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module); OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module); - OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module); + OptionRegistry.RegisterOption(AnalyzeProofs, OptionScope.Module); OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli); OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module); diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 6ac2f5719f6..5d985b0bcb5 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -42,7 +42,7 @@ static DafnyCommands() { CommonOptionBag.WarnContradictoryAssumptions, CommonOptionBag.WarnRedundantAssumptions, CommonOptionBag.SuggestProofRefactoring, - CommonOptionBag.AnalyseProofs, + CommonOptionBag.AnalyzeProofs, CommonOptionBag.NoTimeStampForCoverageReport, CommonOptionBag.VerificationCoverageReport, CommonOptionBag.ExtractCounterexample, diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index c202f32ad38..b26e2a4d105 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -56,7 +56,7 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(string name, private static IEnumerable GetUnusedFunctions(string implementationName, IEnumerable coveredElements, IEnumerable axioms) { - if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) { + if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyzeProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) { return new List(); } @@ -102,7 +102,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, .ThenBy(dep => dep.Description).ToList(); foreach (var unusedDependency in unusedDependencies) { - if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) { + if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyzeProofs)) { if (unusedDependency is ProofObligationDependency obligation) { if (ShouldWarnVacuous(scopeName, obligation)) { var message = $"proved using contradictory assumptions: {obligation.Description}"; @@ -121,7 +121,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, } } - if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) { + if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyzeProofs)) { if (unusedDependency is RequiresDependency requires) { reporter.Warning(MessageSource.Verifier, "", requires.Range, $"unnecessary requires clause"); } @@ -135,7 +135,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName, } } - if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) { + if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyzeProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) { SuggestFunctionHiding(unusedFunctions, method); SuggestByProofRefactoring(scopeName, assertCoverage.ToList()); } @@ -150,20 +150,18 @@ private static void SuggestFunctionHiding(IEnumerable unusedFunctions, private static void SuggestByProofRefactoring(string scopeName, IReadOnlyList verificationRunResults) { - foreach (var (dep, lAsserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) { - var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1; + foreach (var (fact, asserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) { + var factIsOnlyUsedByOneAssertion = asserts.Count == 1; if (!factIsOnlyUsedByOneAssertion) { continue; } - AssertCmdPartialCopy cmd = null; - foreach (var assert in lAsserts) { - cmd = assert; - } + AssertCmdPartialCopy partialAssert = asserts.Single(); - manager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer); + manager.ProofDependenciesById.TryGetValue(partialAssert!.Id, out var assertDepProvenByFact); - if (consumer != null && (dep == consumer || consumer.Range.Intersects(dep.Range))) { + var factAlreadyInByBlock = assertDepProvenByFact != null && (fact == assertDepProvenByFact || assertDepProvenByFact.Range.Intersects(fact.Range)); + if (factAlreadyInByBlock) { continue; } @@ -173,16 +171,16 @@ private static void SuggestByProofRefactoring(string scopeName, var recommendation = ""; var completeInformation = true; - switch (dep) { + switch (fact) { case AssumedProofObligationDependency: case AssumptionDependency: { - range = dep.Range; + range = fact.Range; factProvider = "fact"; recommendation = "moving it into"; break; } case RequiresDependency: { - range = dep.Range; + range = fact.Range; factProvider = "requires clause"; recommendation = "labelling it and revealing it in"; break; @@ -190,13 +188,13 @@ private static void SuggestByProofRefactoring(string scopeName, default: completeInformation = false; break; } - switch (consumer) { + switch (assertDepProvenByFact) { case CallDependency call: { factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.Range.Next.TokenToString(options)}"; break; } case ProofObligationDependency { ProofObligation: AssertStatementDescription }: { - factConsumer = $"assertion {consumer.RangeString()}"; + factConsumer = $"assertion {assertDepProvenByFact.RangeString()}"; break; } default: completeInformation = false; break; From 2e23507662c99f767138c32d3066ed4abf673db3 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 22:46:54 +0200 Subject: [PATCH 25/27] update doos --- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1539 -> 1540 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1560 -> 1561 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1530 -> 1531 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 2048 -> 2049 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1519 -> 1520 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1526 -> 1527 bytes .../binaries/DafnyStandardLibraries.doo | Bin 57233 -> 57234 bytes 7 files changed, 0 insertions(+), 0 deletions(-) diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 8d3d20da486875700188c6493ccfca56147e8afe..31247ec268bad4f811798cb852824e6e1ab9e68e 100644 GIT binary patch delta 536 zcmZqXY2m34@MdNaVPIh3U|72~FmhRies(J(1A`Vb0|PHmG&eCXGcC2aM6V=2Hzzmf z;5uPLo;}~S=T-T;R?6)7AU?-o#V7AMvE4@^-?Wt7zyA2mw6|h~b2qxrlWY&tnoB4J!{ESNHtG`@+`8hLji%PS;$OLUyr1Uz(z2w2o!PHR?$xf{=^w%ZB_@4tUEQ$$|GGHG85I==4zkUabt-(f z>qOZa^%@?9<4SV9CNF(_W|{Y$t}S(DQC#tvbJn6=hxC$Vy!q5awPf;9a3;t$6s@z-&4`vgv1)v<5d zQ1h(ZWNy$SJ&v9WL8TivzCXFksB!tNwX*xUHux!&E&uAvmCq?F?stUa(VJ6NvjRWO zzO`(Tarh2hQF(sJ9g&ut#cb{}v+7@c@C#pBT(e(b#pL4tJx{-$oY! delta 535 zcmZqSY38X9@MdNaVPIh3VA$3e5Lxs^B)Wx>fkBIzfq@q&nwyxHnU-2yqF0iio0A*l z*mv82XU}ud?mMC;Z{@09>Q`k2vcz<5>hzj2eafsK-@R|Hd@Qo}+yv%xJkFZaJvjC2 z1Ez58uc@}2=Rd!%onhj0+h0|`s-h%xPd?yged0ASz^eZDp+$LY ziuE;NJGKeQg8go@O4QWON*{l^ZM01mh9A8`3TnRj;C4E_cESk z=7dMxtQo>%4XS}C*RgZLbW6`#E4#C9KveA7~P|N7%M)82{|&fVxfPqIBoZ=z6K z-C_;Vx}TqlZ06g^@G~l%ul{oR<>$=AEh^3WA``S-onF?z*?zsZ;+AE-&D{R>_o=Jc zUiLFD30cRN7qaP=OUsf9c4ogOxmUY(r+)|wl$i9nb#=q~|Lfu$XH--iILJ0v)~WE_ zt`lWz)N6PYjw{Lan!NP!nPuL0y0+ArMRCPv&RL6g9nwpd^?p$l8ueWGj*s@N09W=^ zCI#DS%vjeRU{u-RQlHPX$$qKzua|0y){@CbuHIX8dqxfCi$5Hn#9znF?Gre4RmZ+* zL(Q{tles~U^f-Dh1eI>w`2OTBqsHa8*2?bZ+Tf>9w*0FvS3ak#xZe?uM{iD9%?kW9 z`_{5W#^F13MdkS=cSKrp7PGm_%&LF&!7qGa;)d%tKE(6B3ba delta 513 zcmbQqGlQo-z?+#xgn@y9gW*VHKxEMuk?0mi1_mu=1_oZBXl`O&W?E`-iC#&5Zcc8H zW8ZB9o;}Y+yYGmayp^kZsb7^9$P&}Jsncu9^eMA`eD}V&^0CO?a}$`)@i=Qv_u$m8 z517KWzoy!9p8x#5c7}=1ZGTn$s)~}(J^6r}^@-QS0IT}nk59YVyq#k||J?Dz=Z!*} zzg%Yw(h6rc*NV(lathkh%&6|jUwZeham8v4o|8Whg&w$GAHH6}$HwMCLi0Jkg%;(p zDc0A7?bs$H3--IsDp6BAD}DUwzFmq<0#|;r_y)!%PT$z4TC!7X?Pt!sWum?-7BPoP zSw!2-ZVG$AAQZEx-kkB~{7bTb%O+2l+hh1BEB|7y&pwutI+mZ^rR)9NIi6-slXr}; z+q~%I6rpm*gqCTmx_fK=uTAB&xtjO(M{GkW(?;vH`9T%lFLo3txe26)U%S{d>HZZn z(YZSh<*xiuapJ()Q=T)7EgoI?6Wm_Di;K5;@3FT1<~!^!Y@TB_`|>V(tHLC<8r@Cb zce!l%=d{4@ob9J+*VU`Jv?iAxbeO4L0sA_ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 45bfa768a27e7f3e6e54d22ae109d8ebcab92dcf..c8c50e38ade8c2fb475e92c0ba325ba2feedfb55 100644 GIT binary patch delta 493 zcmV@6aWAK2mr6OQCX&VFKdMX001fj000dD003=aZfRy^b963r zZ*6RCQo*hhF$}!-E1r5!MR^>!@E4pwsPapkU5mt7?1XmT*W>J#?G|yJu}7X6hf*$) z5?+3zC>4JB@^U<%J{%7LBF}sD)9LeRVYDQJFBFg~MMCL+?6=pAc-lFCJe`k+?`5h6 z>5l`XRIUzgRI=Jcgrs-}15Sb->bkpU@K#Y6lJkYDfUp0qUO||6c)-C1ogG4P?z+f! ztS5X7AjcvejWp>@Oqw^2%YAi21R<#N37Vq1!Y*SSOXzY{TIUnoOe>mDMF*-haJGCl z1+BmVB)CL>ZvwJEr91lRCLuc+W5m_oqT85!3F!O?@)zq~osJO7)hs`PuzcosG@Vl7 zE(na!QgyMh@5#C{fv4K79lr{&P9S!t^-T(I2^|+s#0cW-$~u}+@|)VGqBB>xEfpUR z8Ms+F33CQV9GZXX@J?5uVX)WO@Lvt?5A-aj&E~W~u1=ho0bh&ky)F@~zYwUCbC0~` z^~s)s%4A*e(5KbVKI~S@BkHb%WmqsYYsq@}kK7+nO9KQH000080I#)Cv%CSs0|~FS jQCX&VFKdO9i3KtPueDK=z6Bcru#?&a8U}R*00000*0SE5 delta 492 zcmey({foOkz?+#xgn@y9gJD-=KxEMuk?0mi1_mu=1_oZBXl`O&W?E`-iC#&5Zcc8H zW8ZB9o;}Y+yYGmayp^kZsb7^9$P&}Jsncu9^eMA`eD}V&^0CO?a}$`)@i=Qv_u$m8 z517KWzoy!9p8x#5c7}=1ZGTn$s)~}(J^6r}^@-QS0IT}nk59YVyq#k||J?Dz=Z!*} zzg%Yw(h6rc*NV(lathkh%&6|jUwZeham8v4o|8Whg&w$GAHH6}$HwMCLi0Jkg%;(p zDc0A7?bs$H3--IsDp6BAD}DUwzFmq<0#|;r_y)!%PT$z4TC!7X?Pt!sWum?-7BPoP zSw!2-ZVG$AAQZEx-kkB~{7bTb%O+2l+hh1BEB|7y&pwutI+mZ^rR)9NIi6-slXr}; z+q~%I6rpm*gqCTmx_fK=uTAB&xtjO(M{GkW(?;vH`9T%lFLo3txe26)U%S{d>HZZn z(YZSh<*xiuapJ()Q=T)7EgoI?6Wm_Di;K5;@3FT1<~!^!Y@TB_`|>V(tHLC<8r@Cb zce!l%=d{4@ob9J+*VU`Jv?iAxbe`&p$K*H6C9D#cd93XDev0KX#Ft^fc4 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index a51707bb6cd0487ebbf0fa45ac3e10c1eefd28db..15dcd2b943d28b5a6a9453a9af2c397820e872cb 100644 GIT binary patch delta 515 zcmZn=XcVXq@MdNaVPIh3VA!}dFmhRies(J(1A`Vb0|PHmG&eCXGcC2aM6V=2Hzzmf z;5uPLo;}~S=T-T;R?6)7AU?-o#V7AMvE4@^-?Wt7zyA2mw6|h~b2qxrlWY&tnoB4J!{ESNHtG`@+`8hLji%PS;$OLUyr1Uz(z2w2o!PHR?$xf{=^w%ZB_@4tUEQ$$|GGHG85I==4zkUabt-(f z>qOZa^%@?9<4SV9CNF(_W|{Y$t}S(DQC#tvbJn6=hxC$Vy!q5awPf;9a3;t$6s@z-&4`vgv1)v<5d zQ1h(ZWNy$SJ&v9WL8TivzCXFksB!tNwX*xUHux!&E&uAvmCq?F?stUa(VJ6NvjRWO zzO`(Tarh2hQF(sJ9g&ut#cb{}v+7@c@C#pBT(e(b#pL4tJx{-$oY!fkBIzfq@q&nwyxHnU-2yqF0iio0A*l z*mv82XU}ud?mMC;Z{@09>Q`k2vcz<5>hzj2eafsK-@R|Hd@Qo}+yv%xJkFZaJvjC2 z1Ez58uc@}2=Rd!%onhj0+h0|`s-h%xPd?yged0ASz^eZDp+$LY ziuE;NJGKeQg8go@O4QWON*{l^ZM01mh9A8`3TnRj;C4E_cESh s<%CDwtQo>%4XS}C*RgZLbW6`#E4#C9KveA7~P|N7%M)82{|&fVxfPqIBoZ=z6K z-C_;Vx}TqlZ06g^@G~l%ul{oR<>$=AEh^3WA``S-onF?z*?zsZ;+AE-&D{R>_o=Jc zUiLFD30cRN7qaP=OUsf9c4ogOxmUY(r+)|wl$i9nb#=q~|Lfu$XH--iILJ0v)~WE_ zt`lWz)N6PYjw{Lan!NP!nPuL0y0+ArMRCPv&RL6g9nwpd^?p$l8ueWGj*s@N09W=^ zCI#DS%vjeRU{u-RQlHPX$$qKzua|0y){@CbuHIX8dqxfCi$5Hn#9znF?Gre4RmZ+* zL(Q{tles~U^f-Dh1eI>w`2OTBqsHa8*2?bZ+Tf>9w*0FvS3ak#xZe?uM{iD9%?kW9 z`_{5W#^F13MdkS=cSKrp7PGm_%&LF&!7qGa;)d%tKE(6Bm?Te|vSS;XUU|HZZn z(YZSh<*xiuapJ()Q=T)7EgoI?6Wm_Di;K5;@3FT1<~!^!Y@TB_`|>V(tHLC<8r@Cb zce!l%=d{4@ob9J+*VU`Jv?iAxbetQo>%4XS}C*RgZLbW6`#E4#C9KveA7~P|N7%M)82{|&fVxfPqIBoZ=z6K z-C_;Vx}TqlZ06g^@G~l%ul{oR<>$=AEh^3WA``S-onF?z*?zsZ;+AE-&D{R>_o=Jc zUiLFD30cRN7qaP=OUsf9c4ogOxmUY(r+)|wl$i9nb#=q~|Lfu$XH--iILJ0v)~WE_ zt`lWz)N6PYjw{Lan!NP!nPuL0y0+ArMRCPv&RL6g9nwpd^?p$l8ueWGj*s@N09W=^ zCI#DS%vjeRU{u-RQlHPX$$qKzua|0y){@CbuHIX8dqxfCi$5Hn#9znF?Gre4RmZ+* zL(Q{tles~U^f-Dh1eI>w`2OTBqsHa8*2?bZ+Tf>9w*0FvS3ak#xZe?uM{iD9%?kW9 z`_{5W#^F13MdkS=cSKrp7PGm_%&LF&!7qGa;)d%tKE(6B_ delta 513 zcmey){f)amz?+#xgn@y9gW*JDKxEMuk?0mi1_mu=1_oZBXl`O&W?E`-iC#&5Zcc8H zW8ZB9o;}Y+yYGmayp^kZsb7^9$P&}Jsncu9^eMA`eD}V&^0CO?a}$`)@i=Qv_u$m8 z517KWzoy!9p8x#5c7}=1ZGTn$s)~}(J^6r}^@-QS0IT}nk59YVyq#k||J?Dz=Z!*} zzg%Yw(h6rc*NV(lathkh%&6|jUwZeham8v4o|8Whg&w$GAHH6}$HwMCLi0Jkg%;(p zDc0A7?bs$H3--IsDp6BAD}DUwzFmq<0#|;r_y)!%PT$z4TC!7X?Pt!sWum?-7BPoP zSw!2-ZVG$AAQZEx-kkB~{7bTb%O+2l+hh1BEB|7y&pwutI+mZ^rR)9NIi6-slXr}; z+q~%I6rpm*gqCTmx_fK=uTAB&xtjO(M{GkW(?;vH`9T%lFLo3txe26)U%S{d>HZZn z(YZSh<*xiuapJ()Q=T)7EgoI?6Wm_Di;K5;@3FT1<~!^!Y@TB_`|>V(tHLC<8r@Cb zce!l%=d{4@ob9J+*VU`Jv?iAxbeyIG|b*8?N6peR4RC^0v{o0Sb1oeWGsSOBC8SV24htWnx- diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 16a2ebe97340106ee6dddabc7cc173fb9ad9026b..44716b7ba7425da6a1a7b6dd5bdc2f176467038f 100644 GIT binary patch delta 516 zcmbQZpLx=L=K26{W)=|!1_lm>6BGX<=kw&|zj^;0222Cgx?Pr52aymE`B< zG=ezd2Z}YmC*!BLfstc_8Bb0t!sqouP&bObwTHM`q*RF7`WWP;vd(gRw zLi6euYlznU{ADz!Prl8$;lydVzcqh~_83M@I+)INVye=@lKOAIm-kl8vaGe4*LJwy zD7^X0bH*SoarSVnNMAuk&3gwMHZN%3b?%+yo-mQNCp8bX9=!g2k()!fpWkA}g_}wu z)8BRHoUS_5&R{9_F=I(&deWsmg)#3IODl0W&h@__a#gfU@^y&Q_SKiH=0C`ayV#>; z6|i*T=C7MAGg$c)4ysnwi%$5fWqVQIocrb}3FUPk^Y-{`p@QP!CrSn8wI0Q>6v}o8yTMVA*6cC!`Te4d6KGc?e%Ao-vci2Mc@Xan_oR;&cNrK`YFHWAfe{G)r|p>=WZmvZDwR(&|zj^;0222Cgx?Pr52aymE`B< z7F`b(_y{343`TqI6^wE_FJwWQy1|HFz7Pg48qEbDCVN$8$@V9ff&Yhr*^{qM)6%Jb6v=Jzju_+j&z zs|tTh8>XB(dT^>&Sg?ynSGmChofiw&ZLVfpFWRbT8NY+;$FIUKOoxs2Iamo92B`bm()nk;=R_bB0O2%=F(c+Blp7o(r3}mbS(ovzmJ0?W!&3)OXAZH(A`p z7n1oT=Wh;QR3o!TLFc`CmX!To{$FmNb=qchtRs8R?EK_UstY~~pRiw(UTWp2A>RE* z&dpKjcyuNyeZoHZ`ZB0Gu1=>D2VZ#J(tq{WBz?>lnC3r zhcV_ZCp_jRE8aJ<2l3u;Px@$amw_RrhLwRG7>_Wpq;VZEb_ Date: Fri, 18 Oct 2024 11:39:17 +0200 Subject: [PATCH 26/27] Update CommonOptionBag.cs --- Source/DafnyCore/Options/CommonOptionBag.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index b8f5813f2c8..78044a9cbd3 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -294,7 +294,7 @@ May produce spurious warnings. IsHidden = true }; public static readonly Option AnalyzeProofs = new("--analyze-proofs", @" -Uses data from to prover to suggest ways to refine the proof: +Uses data from to verifier to suggest ways to refine the proof: Warning if any assertions are proved based on contradictory assumptions (vacuously). Warning if any `requires` clause or `assume` statement was not needed to complete verification. Suggestions for moving assertions into by-proofs and hiding unused function definitions. From 8d89dec5c30449df29fa8c64bb4828782b53d390 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 18 Oct 2024 11:40:09 +0200 Subject: [PATCH 27/27] Update CommonOptionBag.cs --- Source/DafnyCore/Options/CommonOptionBag.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 78044a9cbd3..f55690dfb47 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -294,7 +294,7 @@ May produce spurious warnings. IsHidden = true }; public static readonly Option AnalyzeProofs = new("--analyze-proofs", @" -Uses data from to verifier to suggest ways to refine the proof: +Uses data from the verifier to suggest ways to refine the proof: Warning if any assertions are proved based on contradictory assumptions (vacuously). Warning if any `requires` clause or `assume` statement was not needed to complete verification. Suggestions for moving assertions into by-proofs and hiding unused function definitions.