From 9ed559a9353cb0d2230f3441fd93467ee11e984d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 20 Jul 2023 15:14:26 -0700 Subject: [PATCH 01/44] Basic implementation of proof dependency analysis When enabled with -trackVerificationCoverage (an internal Boogie flag that we don't expect most people to use), this calculates proof dependencies and includes them in the output of the "text" format verification logger. Some caveats: * Some important statements aren't labeled yet. * Some descriptions are different in different contexts. --- .../DafnyCore/AST/Expressions/Expression.cs | 1 - Source/DafnyCore/AST/Program.cs | 1 + Source/DafnyCore/AST/SystemModuleManager.cs | 1 - .../AST/TypeDeclarations/TupleTypeDecl.cs | 1 - .../Compilers/Python/Compiler-python.cs | 1 - Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Feature.cs | 1 - Source/DafnyCore/JsonDiagnostics.cs | 1 - Source/DafnyCore/Options/CommonOptionBag.cs | 1 - Source/DafnyCore/Resolver/BoundsDiscovery.cs | 1 - .../Resolver/FindFriendlyCalls_Visitor.cs | 1 - .../Resolver/GhostInterestVisitor.cs | 1 - .../NameResolutionAndTypeInference.cs | 1 - .../Resolver/PreType/PreTypeAdvice.cs | 1 - .../PreTypeResolve.ActualParameters.cs | 1 - .../PreType/PreTypeResolve.Expressions.cs | 1 - .../PreType/PreTypeResolve.Statements.cs | 1 - Source/DafnyCore/Resolver/TypeConstraint.cs | 2 - .../Rewriters/BitvectorOptimization.cs | 1 - .../Rewriters/RunAllTestsMainMethod.cs | 1 - .../DafnyCore/Triggers/QuantifierSplitter.cs | 1 - .../Triggers/QuantifiersCollection.cs | 1 - .../Triggers/QuantifiersCollector.cs | 1 - Source/DafnyCore/Verifier/ProofDependency.cs | 188 ++++++++++++++++++ .../Verifier/ProofObligationDescription.cs | 2 +- .../Verifier/Translator.BoogieFactory.cs | 8 + .../Verifier/Translator.ClassMembers.cs | 18 +- .../Translator.ExpressionTranslator.cs | 9 +- .../Translator.ExpressionWellformed.cs | 14 +- .../Verifier/Translator.TrStatement.cs | 46 ++--- Source/DafnyCore/Verifier/Translator.cs | 114 +++++++++-- Source/DafnyDriver/DafnyDriver.cs | 13 +- Source/DafnyDriver/TextLogger.cs | 15 +- .../DafnyDriver/VerificationResultLogger.cs | 4 +- .../Language/DafnyProgramVerifier.cs | 2 +- customBoogie.patch | 11 +- 36 files changed, 371 insertions(+), 98 deletions(-) create mode 100644 Source/DafnyCore/Verifier/ProofDependency.cs diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index aa652b3dc2e..061ffb299fa 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -2,7 +2,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Numerics; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 6b7a4e765b1..952bf6de783 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -30,6 +30,7 @@ void ObjectInvariant() { public SystemModuleManager SystemModuleManager; public DafnyOptions Options => Reporter.Options; public ErrorReporter Reporter { get; set; } + public Translator.ProofDependencyManager ProofDependencyManager { get; set; } public Program(string name, [Captured] LiteralModuleDecl module, [Captured] SystemModuleManager systemModuleManager, ErrorReporter reporter, CompilationData compilation) { diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index f017211705d..40b5ea1be43 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -6,7 +6,6 @@ using System.Linq; using System.Security.Cryptography; using System.Security.Policy; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs index e370a07ab71..df5be78a90f 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs @@ -2,7 +2,6 @@ using System.Diagnostics.Contracts; using System.Linq; using JetBrains.Annotations; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index cb63dcda004..df95bae0b51 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs @@ -10,7 +10,6 @@ using JetBrains.Annotations; using ExtensionMethods; using Microsoft.BaseTypes; -using Microsoft.Boogie; namespace ExtensionMethods { using Microsoft.Dafny; diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 49ad7566759..823adbc7b3b 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -32,7 +32,7 @@ - + diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs index 856b02e7edf..55afeadb45c 100644 --- a/Source/DafnyCore/Feature.cs +++ b/Source/DafnyCore/Feature.cs @@ -1,7 +1,6 @@ using System; using System.Diagnostics.Contracts; using System.Linq; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index 7d82ab0c089..f563822bcbd 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -6,7 +6,6 @@ using System.Linq; using System.Text.Json; using System.Text.Json.Nodes; -using Microsoft.Boogie; using VCGeneration; using static Microsoft.Dafny.ErrorRegistry; diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 228ed28284a..4f0bad26983 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -3,7 +3,6 @@ using System.IO; using System.Linq; using DafnyCore; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery.cs index ffee04d0e13..f592bf89973 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery.cs @@ -7,7 +7,6 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics.Contracts; -using Microsoft.Boogie; namespace Microsoft.Dafny { public partial class ModuleResolver { diff --git a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs b/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs index 27c58cc44f0..c9a8f379a38 100644 --- a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs +++ b/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs @@ -1,5 +1,4 @@ using System.Diagnostics.Contracts; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index b21503d47b0..b9bd9720443 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -1,7 +1,6 @@ using System.Diagnostics.Contracts; using System.Linq; using JetBrains.Annotations; -using Microsoft.Boogie; using static Microsoft.Dafny.ResolutionErrors; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 58488bc30ab..9f805e02485 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -15,7 +15,6 @@ using System.Reflection; using JetBrains.Annotations; using Microsoft.BaseTypes; -using Microsoft.Boogie; using Microsoft.CodeAnalysis.CSharp.Syntax; using Microsoft.Dafny.Plugins; diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs index e08506d20ba..782ee0ba2d6 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs @@ -9,7 +9,6 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics.Contracts; -using Microsoft.Boogie; namespace Microsoft.Dafny { public class Advice { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs index bc44e127e64..6114e713e8e 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs @@ -8,7 +8,6 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics.Contracts; -using Microsoft.Boogie; using ResolutionContext = Microsoft.Dafny.ResolutionContext; namespace Microsoft.Dafny { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 13509a417bb..8eca039be60 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -10,7 +10,6 @@ using System.Linq; using System.Numerics; using System.Diagnostics.Contracts; -using Microsoft.Boogie; using ResolutionContext = Microsoft.Dafny.ResolutionContext; namespace Microsoft.Dafny { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 4755f9e3ec8..70bbc1bbbda 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -13,7 +13,6 @@ using System.Diagnostics.Contracts; using System.Runtime.Intrinsics.X86; using JetBrains.Annotations; -using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using ResolutionContext = Microsoft.Dafny.ResolutionContext; diff --git a/Source/DafnyCore/Resolver/TypeConstraint.cs b/Source/DafnyCore/Resolver/TypeConstraint.cs index 8b077b8c131..d0f3823b952 100644 --- a/Source/DafnyCore/Resolver/TypeConstraint.cs +++ b/Source/DafnyCore/Resolver/TypeConstraint.cs @@ -11,8 +11,6 @@ using System.Numerics; using System.Diagnostics.Contracts; using JetBrains.Annotations; -using Microsoft.BaseTypes; -using Microsoft.Boogie; using Microsoft.CodeAnalysis.CSharp.Syntax; namespace Microsoft.Dafny { diff --git a/Source/DafnyCore/Rewriters/BitvectorOptimization.cs b/Source/DafnyCore/Rewriters/BitvectorOptimization.cs index f73112bfa89..09bd7732bfd 100644 --- a/Source/DafnyCore/Rewriters/BitvectorOptimization.cs +++ b/Source/DafnyCore/Rewriters/BitvectorOptimization.cs @@ -4,7 +4,6 @@ using System; using System.Linq.Expressions; using System.Numerics; -using Microsoft.Boogie; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index f2495551a01..677e9c324ca 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs @@ -1,7 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using Microsoft.Boogie; using System.Text.RegularExpressions; using static Microsoft.Dafny.RewriterErrors; diff --git a/Source/DafnyCore/Triggers/QuantifierSplitter.cs b/Source/DafnyCore/Triggers/QuantifierSplitter.cs index 4af13432bfd..ba03614ca9a 100644 --- a/Source/DafnyCore/Triggers/QuantifierSplitter.cs +++ b/Source/DafnyCore/Triggers/QuantifierSplitter.cs @@ -1,7 +1,6 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT -using Microsoft.Boogie; using System; using System.Collections.Generic; using System.Diagnostics.Contracts; diff --git a/Source/DafnyCore/Triggers/QuantifiersCollection.cs b/Source/DafnyCore/Triggers/QuantifiersCollection.cs index 72fcfb1515e..888dc57ef6a 100644 --- a/Source/DafnyCore/Triggers/QuantifiersCollection.cs +++ b/Source/DafnyCore/Triggers/QuantifiersCollection.cs @@ -7,7 +7,6 @@ using System.Collections.Generic; using System.Linq; using System.Text; -using Microsoft.Boogie; using System.Diagnostics.Contracts; using static Microsoft.Dafny.ErrorRegistry; diff --git a/Source/DafnyCore/Triggers/QuantifiersCollector.cs b/Source/DafnyCore/Triggers/QuantifiersCollector.cs index 08975598cac..a86f8f5ceaf 100644 --- a/Source/DafnyCore/Triggers/QuantifiersCollector.cs +++ b/Source/DafnyCore/Triggers/QuantifiersCollector.cs @@ -5,7 +5,6 @@ using System.Collections.Generic; using System.Linq; using System.Text; -using Microsoft.Boogie; using System.Collections.ObjectModel; using System.Diagnostics.Contracts; diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs new file mode 100644 index 00000000000..afbbfc4c357 --- /dev/null +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -0,0 +1,188 @@ +using System; +using JetBrains.Annotations; +using Microsoft.Boogie; +using Microsoft.Dafny; +using IToken = Microsoft.Dafny.IToken; +using PODesc = Microsoft.Dafny.ProofObligationDescription; + +namespace DafnyCore.Verifier; + +public abstract class ProofDependency { + public abstract string Description { get; } + + public abstract RangeToken RangeToken { get; } + + public string LocationString() { + return RangeToken?.StartToken is null + ? "" + : $"{RangeToken.StartToken.filename}({RangeToken.StartToken.line},{RangeToken.StartToken.col - 1})"; + } + + public string RangeString() { + if (RangeToken is null) { + return ""; + } + var fn = RangeToken.StartToken.filename; + var sl = RangeToken.StartToken.line; + var sc = RangeToken.StartToken.col - 1; + var el = RangeToken.EndToken.line; + var ec = RangeToken.EndToken.col - 1; + return $"{fn}({sl},{sc})-({el},{ec})"; + } + + public string OriginalString() { + return RangeToken?.PrintOriginal(); + } +} + +public class ProofObligationDependency : ProofDependency { + public override RangeToken RangeToken { get; } + + public PODesc.ProofObligationDescription ProofObligation { get; } + + public override string Description => + $"{ProofObligation.SuccessDescription}"; + + public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) { + RangeToken = tok as RangeToken ?? new RangeToken(tok, tok); + ProofObligation = proofObligation; + } +} + +public class RequiresDependency : ProofDependency { + private Expression requires; + + public override RangeToken RangeToken => + requires.RangeToken; + + public override string Description => + $"requires {requires.RangeToken.PrintOriginal()}"; + + public RequiresDependency(Expression requires) { + this.requires = requires; + } +} + +public class EnsuresDependency : ProofDependency { + private Expression ensures; + + public override RangeToken RangeToken => + ensures.RangeToken; + + public override string Description => + $"ensures {ensures.RangeToken.PrintOriginal()}"; + + public EnsuresDependency(Expression ensures) { + this.ensures = ensures; + } +} + +public class CallRequiresDependency : ProofDependency { + private CallDependency call; + private RequiresDependency requires; + + public override RangeToken RangeToken => + call.RangeToken; + + public override string Description => + $"{requires.Description} from call at {call.Description}"; + + public CallRequiresDependency(CallDependency call, RequiresDependency requires) { + this.call = call; + this.requires = requires; + } +} + +public class CallEnsuresDependency : ProofDependency { + private CallDependency call; + private EnsuresDependency ensures; + + public override RangeToken RangeToken => + call.RangeToken; + + public override string Description => + $"{ensures.Description} from call at {call.Description}"; + + public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { + this.call = call; + this.ensures = ensures; + } +} + +public class CallDependency : ProofDependency { + private CallStmt call; + + public override RangeToken RangeToken => + call.RangeToken; + + public override string Description => + $"{LocationString()}: {OriginalString()};"; + + public CallDependency(CallStmt call) { + this.call = call; + } +} + +public class AssertionDependency : ProofDependency { + private Expression expr; + + public override RangeToken RangeToken => + expr.RangeToken; + + public override string Description => + $"assert {OriginalString()};"; + + public AssertionDependency(Expression expr) { + this.expr = expr; + } +} + +public class AssumptionDependency : ProofDependency { + private Expression expr; + + public override RangeToken RangeToken => + expr.RangeToken; + + public override string Description => + $"assume {OriginalString()}"; + + public AssumptionDependency(Expression expr) { + this.expr = expr; + } +} + +public class InvariantDependency : ProofDependency { + private Expression invariant; + + public override RangeToken RangeToken => + invariant.RangeToken; + + public override string Description => + $"invariant {invariant.RangeToken.PrintOriginal()}"; + + public InvariantDependency(Expression invariant) { + this.invariant = invariant; + } +} + +public class InternalDependency : ProofDependency { + public override RangeToken RangeToken => null; + public override string Description { get; } + + public InternalDependency(string description) { + Description = description; + } +} + +// Temporary placeholder. Remove when all creation sites use a different +// implementation. +public class NodeOnlyDependency : ProofDependency { + public override RangeToken RangeToken { get; } + + public override string Description => + $"{LocationString()}: {OriginalString()}"; + + public NodeOnlyDependency([NotNull] Node node) { + RangeToken = node.RangeToken; + } +} diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 4e6d1f4e800..de343d8f971 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -350,7 +350,7 @@ public AssertStatement([CanBeNull] string customErrMsg, [CanBeNull] string custo // The Boogie version does not support custom error messages yet public class RequiresDescription : ProofObligationDescriptionCustomMessages { public override string DefaultSuccessDescription => - "the precondition always holds"; + "this precondition always holds"; public override string DefaultFailureDescription => "this is the precondition that could not be proved"; diff --git a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs index 2d4a2ccd661..886818206f2 100644 --- a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.IO; +using DafnyCore.Verifier; using Bpl = Microsoft.Boogie; using static Microsoft.Dafny.Util; @@ -197,6 +198,13 @@ public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyV return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes); } + public Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Bpl.QKeyValue attributes = null) { + var expr = etran.TrExpr(dafnyExpr); + var cmd = TrAssumeCmd(tok, expr, attributes); + proofDependencies.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(dafnyExpr)); + return cmd; + } + static Bpl.Expr RemoveLit(Bpl.Expr expr) { return GetLit(expr) ?? expr; } diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 81f200b828b..5ca67a3bde2 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -676,7 +676,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true); if (wh != null) { var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state"); - builder.Add(Assert(e.tok, wh, desc)); + builder.Add(Assert(e.RangeToken, wh, desc)); } } } @@ -1236,14 +1236,14 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex Contract.Requires(substMap != null); //generating class post-conditions foreach (var en in m.Ens) { - builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, en.E)); } //generating trait post-conditions with class variables FunctionCallSubstituter sub = null; foreach (var en in m.OverriddenMethod.Ens) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass); foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) { - builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger())); + builder.Add(Assert(m.RangeToken, s.E, new PODesc.EnsuresStronger())); } } } @@ -1259,11 +1259,11 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E FunctionCallSubstituter sub = null; foreach (var req in m.OverriddenMethod.Req) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass); - builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(sub.Substitute(req.E)))); + builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, sub.Substitute(req.E))); } //generating class pre-conditions foreach (var s in m.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { - builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker())); + builder.Add(Assert(m.RangeToken, s.E, new PODesc.RequiresWeaker())); } } @@ -1331,7 +1331,7 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo // as "false". bool allowNoChange = N == decrCountT && decrCountT <= decrCountC; var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false); - builder.Add(Assert(original.Tok, decrChk, new PODesc.TraitDecreases(original.WhatKind))); + builder.Add(Assert(original.RangeToken, decrChk, new PODesc.TraitDecreases(original.WhatKind))); } private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List localVariables, @@ -1376,7 +1376,7 @@ private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, Boogie.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Boogie.Expr q = new Boogie.ForallExpr(tok, new List { alpha }, new List { oVar, fVar }, Boogie.Expr.Imp(Boogie.Expr.And(ante, oInCallee), consequent2)); - builder.Add(Assert(tok, q, new PODesc.TraitFrame(m.WhatKind, true), kv)); + builder.Add(Assert(m.RangeToken, q, new PODesc.TraitFrame(m.WhatKind, true), kv)); } // Return a way to know if an assertion should be converted to an assumption @@ -1505,7 +1505,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } else if (s.IsOnlyFree && !bodyKind) { // don't include in split -- it would be ignored, anyhow } else { - req.Add(Requires(s.Tok, s.IsOnlyFree, s.E, errorMessage, successMessage, comment)); + req.Add(RequiresWithCoverage(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); comment = null; // the free here is not linked to the free on the original expression (this is free things generated in the splitting.) } @@ -1528,7 +1528,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } else if (s.IsOnlyChecked && !bodyKind) { // don't include in split } else { - AddEnsures(ens, Ensures(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, post, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithCoverage(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, p.E, post, errorMessage, successMessage, null)); } } } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index bff021ebe47..5af62a94318 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -8,8 +8,7 @@ namespace Microsoft.Dafny { public partial class Translator { - - internal class ExpressionTranslator { + public class ExpressionTranslator { private DafnyOptions options; // HeapExpr == null ==> translation of pure (no-heap) expression readonly Boogie.Expr _the_heap_expr; @@ -36,8 +35,8 @@ public Boogie.IdentifierExpr HeapCastToIdentifierExpr { public readonly string This; public readonly string modifiesFrame; // the name of the context's frame variable. readonly Function applyLimited_CurrentFunction; - public readonly FuelSetting layerInterCluster; - public readonly FuelSetting layerIntraCluster = null; // a value of null says to do the same as for inter-cluster calls + internal readonly FuelSetting layerInterCluster; + internal readonly FuelSetting layerIntraCluster = null; // a value of null says to do the same as for inter-cluster calls public int Statistics_CustomLayerFunctionCount = 0; public int Statistics_HeapAsQuantifierCount = 0; public int Statistics_HeapUses = 0; @@ -169,7 +168,7 @@ public ExpressionTranslator WithLayer(Boogie.Expr layerArgument) { return CloneExpressionTranslator(this, translator, predef, HeapExpr, This, null, new FuelSetting(translator, 0, layerArgument), new FuelSetting(translator, 0, layerArgument), modifiesFrame, stripLits); } - public ExpressionTranslator WithCustomFuelSetting(CustomFuelSettings customSettings) { + internal ExpressionTranslator WithCustomFuelSetting(CustomFuelSettings customSettings) { // Use the existing layers but with some per-function customizations Contract.Requires(customSettings != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index b287ca2c4f7..20def1ffb7d 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -154,7 +154,7 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List @@ -705,9 +705,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re var desc = new PODesc.PreconditionSatisfied(errorMessage, successMessage); if (wfOptions.AssertKv != null) { // use the given assert attribute only - builder.Add(Assert(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage, successMessage), wfOptions.AssertKv)); + builder.Add(Assert(tok, ss.E, desc, wfOptions.AssertKv)); } else { - builder.Add(AssertNS(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage, successMessage))); + builder.Add(AssertNS(tok, ss.E, desc)); } } } diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index ad89f22fee4..9f80cfb2bf4 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using DafnyCore.Verifier; using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; @@ -110,7 +111,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List: AddComment(b, stmt, "assume lhs"); - b.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(CalcStmt.Lhs(stmt.Steps[i])))); + b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, CalcStmt.Lhs(stmt.Steps[i]))); } // hint: AddComment(b, stmt, "Hint" + i.ToString()); @@ -734,7 +735,7 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List 1) { - builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(stmt.Result))); + builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Result)); } } CurrentIdGenerator.Pop(); @@ -1611,7 +1612,7 @@ void TrAlternatives(List alternatives, Bpl.Cmd elseCase0, Bp var exists = (ExistsExpr)alternative.Guard; // the original (that is, not alpha-renamed) guard IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran, isGhost); } else { - b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard))); + b.Add(TrAssumeCmdWithDependencies(etran, alternative.Guard.tok, alternative.Guard)); } var prevDefiniteAssignmentTrackerCount = definiteAssignmentTrackers.Count; TrStmtList(alternative.Body, b, locals, etran); @@ -1667,7 +1668,7 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List locals builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr)); } builder.Add(new CommentCmd("TrCallStmt: Before ProcessCallStmt")); - ProcessCallStmt(GetToken(s), tySubst, GetTypeParams(s.Method), s.Receiver, actualReceiver, s.Method, s.MethodSelect.AtLabel, s.Args, bLhss, lhsTypes, builder, locals, etran); + ProcessCallStmt(s, tySubst, actualReceiver, bLhss, lhsTypes, builder, locals, etran); builder.Add(new CommentCmd("TrCallStmt: After ProcessCallStmt")); for (int i = 0; i < lhsBuilders.Count; i++) { var lhs = s.Lhs[i]; @@ -1707,32 +1708,28 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List locals builder.AddCaptureState(s); } - void ProcessCallStmt(IToken tok, - Dictionary tySubst, List tyArgs, - Expression dafnyReceiver, Bpl.Expr bReceiver, - Method method, Label/*?*/ atLabel, List Args, + void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.Expr bReceiver, List Lhss, List LhsTypes, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { - Contract.Requires(tok != null); - Contract.Requires(dafnyReceiver != null || bReceiver != null); - Contract.Requires(method != null); - Contract.Requires(VisibleInScope(method)); - Contract.Requires(method is TwoStateLemma || atLabel == null); - Contract.Requires(Args != null); + Contract.Requires(cs != null); Contract.Requires(Lhss != null); Contract.Requires(LhsTypes != null); // Note, a Dafny class constructor is declared to have no output parameters, but it is encoded in Boogie as // having an output parameter. - Contract.Requires(method is Constructor || method.Outs.Count == Lhss.Count); - Contract.Requires(method is Constructor || method.Outs.Count == LhsTypes.Count); - Contract.Requires(!(method is Constructor) || (method.Outs.Count == 0 && Lhss.Count == 1 && LhsTypes.Count == 1)); + Contract.Requires(cs.Method is Constructor || cs.Method.Outs.Count == Lhss.Count); + Contract.Requires(cs.Method is Constructor || cs.Method.Outs.Count == LhsTypes.Count); + Contract.Requires(!(cs.Method is Constructor) || (cs.Method.Outs.Count == 0 && Lhss.Count == 1 && LhsTypes.Count == 1)); Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); Contract.Requires(tySubst != null); - Contract.Requires(tyArgs != null); - Contract.Requires(tyArgs.Count <= tySubst.Count); // more precisely, the members of tyArgs are required to be keys of tySubst, but this is a cheap sanity test + var tok = GetToken(cs); + var tyArgs = GetTypeParams(cs.Method); + var dafnyReceiver = cs.Receiver; + var method = cs.Method; + var atLabel = cs.MethodSelect.AtLabel; + var Args = cs.Args; // Figure out if the call is recursive or not, which will be used below to determine the need for a // termination check and the need to include an implicit _k-1 argument. @@ -1931,6 +1928,7 @@ void ProcessCallStmt(IToken tok, // Make the call AddReferencedMember(callee); Bpl.CallCmd call = Call(tok, MethodName(callee, kind), ins, outs); + proofDependencies.AddProofDependencyId(call, tok, new CallDependency(cs)); if ( (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 86edcc4ed16..55d69e37433 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -21,6 +21,7 @@ using Microsoft.Boogie; using static Microsoft.Dafny.Util; using Core; +using DafnyCore.Verifier; using Microsoft.BaseTypes; using Microsoft.Dafny.Triggers; using Action = System.Action; @@ -43,7 +44,7 @@ void AddOtherDefinition(Bpl.Declaration declaration, Axiom axiom) { case null: break; case Boogie.Function boogieFunction: - boogieFunction.AddOtherDefinitionAxiom(axiom); + boogieFunction.OtherDefinitionAxioms.Add(axiom); break; case Boogie.Constant boogieConstant: boogieConstant.DefinitionAxioms.Add(axiom); @@ -65,9 +66,10 @@ public TranslatorFlags(DafnyOptions options) { } [NotDelayed] - public Translator(ErrorReporter reporter, TranslatorFlags flags = null) { + public Translator(ErrorReporter reporter, ProofDependencyManager depManager, TranslatorFlags flags = null) { this.options = reporter.Options; this.flags = new TranslatorFlags(options); + this.proofDependencies = depManager; triggersCollector = new Triggers.TriggersCollector(new Dictionary>(), options); this.reporter = reporter; if (flags == null) { @@ -95,7 +97,6 @@ private void EstablishModuleScope(ModuleDefinition systemModule, ModuleDefinitio verificationScope.Augment(currentScope); currentScope.Augment(systemModule.VisibilityScope); - foreach (var decl in m.TopLevelDecls) { if (decl is ModuleDecl && !(decl is ModuleExportDecl)) { var mdecl = (ModuleDecl)decl; @@ -116,6 +117,56 @@ private void EstablishModuleScope(ModuleDefinition systemModule, ModuleDefinitio readonly Dictionary fieldConstants = new Dictionary(); readonly Dictionary tytagConstants = new Dictionary(); + public class ProofDependencyManager { + // proof dependency tracking state + public Dictionary ProofDependenciesById { get; } = new(); + private UInt64 proofDependencyIdCount = 0; + + public string GetProofDependencyId(ProofDependency dep) { + // TODO: track whether we've seen this node before + var idString = $"id{proofDependencyIdCount}"; + ProofDependenciesById[idString] = dep; + proofDependencyIdCount++; + return idString; + } + + public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, ProofDependency dep) { + var idString = GetProofDependencyId(dep); + boogieNode.Attributes = + new QKeyValue(tok, "id", new List() { idString }, boogieNode.Attributes); + } + + // Get the full ProofDependency indicated by a compound ID string. + public ProofDependency GetFullIdDependency(string idString) { + var parts = idString.Split('$'); + if (idString.EndsWith("$requires") && parts.Length == 3) { + var reqId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); + } else if (idString.EndsWith("$requires_assumed") && parts.Length == 3) { + var reqId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); + } else if (idString.EndsWith("$ensures") && parts.Length == 3) { + var ensId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallEnsuresDependency((CallDependency)callId, (EnsuresDependency)ensId); + } else if (idString.EndsWith("$established") && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (idString.EndsWith("$maintained") && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (idString.EndsWith("$assume_in_body") && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (parts.Length > 1) { + throw new ArgumentException($"Malformed dependency ID string: {idString}"); + } else { + return ProofDependenciesById[idString]; + } + } + } + + private ProofDependencyManager proofDependencies; + // optimizing translation readonly ISet referencedMembers = new HashSet(); @@ -203,7 +254,7 @@ bool InVerificationScope(RedirectingTypeDecl d) { private bool InsertChecksums { get { return flags.InsertChecksums; } } private string UniqueIdPrefix { get { return flags.UniqueIdPrefix; } } - internal class PredefinedDecls { + public class PredefinedDecls { public readonly Bpl.Type CharType; public readonly Bpl.Type RefType; public readonly Bpl.Type BoxType; @@ -877,7 +928,7 @@ public static IEnumerable VerifiableModules(Program p) { Type.ResetScopes(); foreach (ModuleDefinition outerModule in VerifiableModules(p)) { - var translator = new Translator(reporter, flags); + var translator = new Translator(reporter, p.ProofDependencyManager, flags); if (translator.sink == null || translator.sink == null) { // something went wrong during construction, which reads the prelude; an error has @@ -1726,7 +1777,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { // Next, we assume about this.* whatever we said that the iterator constructor promises foreach (var p in iter.Member_Init.Ens) { - builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); } // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this}) @@ -1859,12 +1910,12 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { // don't include this precondition here Contract.Assert(p.Label.E != null); // it should already have been recorded } else { - builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); } } foreach (var p in iter.Member_Init.Ens) { // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet - builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); } // add the _yieldCount variable, and assume its initial value to be 0 yieldCountVariable = new Bpl.LocalVariable(iter.tok, @@ -3606,7 +3657,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //generating class post-conditions foreach (var en in f.Ens) { - builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, en.E)); } //generating assume C.F(ins) == out, if a result variable was given @@ -3742,7 +3793,7 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde FunctionCallSubstituter sub = null; foreach (var req in f.OverriddenFunction.Req) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass); - builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(sub.Substitute(req.E)))); + builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, sub.Substitute(req.E))); } //generating class pre-conditions foreach (var s in f.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { @@ -4312,7 +4363,7 @@ void AddWellformednessCheck(Function f) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) { - AddEnsures(ens, Ensures(s.Tok, false, s.E, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithCoverage(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); } } } @@ -7367,7 +7418,9 @@ public override IToken WithVal(string newVal) { } Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) { - return Assert(tok, condition, description, tok, kv); + var cmd = Assert(tok, condition, description, tok, kv); + proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); + return cmd; } Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, IToken refinesToken, Bpl.QKeyValue kv = null) { @@ -7375,15 +7428,17 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe Contract.Requires(condition != null); Contract.Ensures(Contract.Result() != null); + Bpl.PredicateCmd cmd; if (assertAsAssume || (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce an assume instead - return TrAssumeCmd(tok, condition, kv); + cmd = TrAssumeCmd(tok, condition, kv); } else { - var cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv); - return cmd; + cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv); } + proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); + return cmd; } Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc) { @@ -7396,17 +7451,30 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation Contract.Requires(condition != null); Contract.Ensures(Contract.Result() != null); + Bpl.PredicateCmd cmd; if ((assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce a "skip" instead - return TrAssumeCmd(tok, Bpl.Expr.True, kv); + cmd = TrAssumeCmd(tok, Bpl.Expr.True, kv); } else { tok = ForceCheckToken.Unwrap(tok); var args = new List(); args.Add(Bpl.Expr.Literal(0)); - Bpl.AssertCmd cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv)); - return cmd; + cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv)); } + + proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, desc)); + return cmd; + } + + Bpl.Ensures EnsuresWithCoverage(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { + Contract.Requires(tok != null); + Contract.Requires(dafnyCondition != null); + Contract.Ensures(Contract.Result() != null); + + var ens = Ensures(tok, free, condition, errorMessage, successMessage, comment); + proofDependencies.AddProofDependencyId(ens, tok, new EnsuresDependency(dafnyCondition)); + return ens; } Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { @@ -7419,6 +7487,16 @@ Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessa return ens; } + Bpl.Requires RequiresWithCoverage(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { + Contract.Requires(tok != null); + Contract.Requires(dafnyCondition != null); + Contract.Ensures(Contract.Result() != null); + + var req = Requires(tok, free, condition, errorMessage, successMessage, comment); + proofDependencies.AddProofDependencyId(req, tok, new RequiresDependency(dafnyCondition)); + return req; + } + Bpl.Requires Requires(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { Contract.Requires(tok != null); Contract.Requires(condition != null); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 08161641ba2..7c8da967fb3 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -127,6 +127,7 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T var cliArgumentsResult = ProcessCommandLineArguments(outputWriter, errorWriter, inputReader, args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); ExitValue exitValue; + Translator.ProofDependencyManager depManager = new(); switch (cliArgumentsResult) { case CommandLineArgumentsResult.OK: @@ -146,7 +147,7 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T using (var driver = new DafnyDriver(dafnyOptions)) { #pragma warning disable VSTHRD002 - exitValue = driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), dafnyOptions).Result; + exitValue = driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), dafnyOptions, depManager).Result; #pragma warning restore VSTHRD002 } break; @@ -162,7 +163,7 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T if (dafnyOptions.VerificationLoggerConfigs.Any()) { try { - VerificationResultLogger.RaiseTestLoggerEvents(dafnyOptions); + VerificationResultLogger.RaiseTestLoggerEvents(dafnyOptions, depManager); } catch (ArgumentException ae) { dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, $"*** Error: {ae.Message}"); exitValue = ExitValue.PREPROCESSING_ERROR; @@ -384,7 +385,8 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter private async Task ProcessFilesAsync(IReadOnlyList/*!*/ dafnyFiles, ReadOnlyCollection otherFileNames, - DafnyOptions options, bool lookForSnapshots = true, string programId = null) { + DafnyOptions options, Translator.ProofDependencyManager depManager, + bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(dafnyFiles)); var dafnyFileNames = DafnyFile.FileNames(dafnyFiles); @@ -413,7 +415,7 @@ private async Task ProcessFilesAsync(IReadOnlyList/*! foreach (var f in dafnyFiles) { await options.OutputWriter.WriteLineAsync(); await options.OutputWriter.WriteLineAsync($"-------------------- {f} --------------------"); - var ev = await ProcessFilesAsync(new List { f }, new List().AsReadOnly(), options, lookForSnapshots, f.FilePath); + var ev = await ProcessFilesAsync(new List { f }, new List().AsReadOnly(), options, depManager, lookForSnapshots, f.FilePath); if (exitValue != ev && ev != ExitValue.SUCCESS) { exitValue = ev; } @@ -430,7 +432,7 @@ private async Task ProcessFilesAsync(IReadOnlyList/*! snapshots.Add(new DafnyFile(options, uri)); options.CliRootSourceUris.Add(uri); } - var ev = await ProcessFilesAsync(snapshots, new List().AsReadOnly(), options, false, programId); + var ev = await ProcessFilesAsync(snapshots, new List().AsReadOnly(), options, depManager, false, programId); if (exitValue != ev && ev != ExitValue.SUCCESS) { exitValue = ev; } @@ -455,6 +457,7 @@ private async Task ProcessFilesAsync(IReadOnlyList/*! } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck && options.DafnyVerify) { + dafnyProgram.ProofDependencyManager = depManager; var boogiePrograms = await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList()); diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index 76fe748c4aa..e91050ae32f 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -9,8 +9,10 @@ namespace Microsoft.Dafny; public class TextLogger { private TextWriter tw; private TextWriter outWriter; + private Translator.ProofDependencyManager depManager; - public TextLogger(TextWriter outWriter) { + public TextLogger(Translator.ProofDependencyManager depManager, TextWriter outWriter) { + this.depManager = depManager; this.outWriter = outWriter; } @@ -41,7 +43,16 @@ public void LogResults(List<(Implementation, VerificationResult)> verificationRe tw.WriteLine(" Assertions:"); foreach (var cmd in vcResult.asserts) { tw.WriteLine( - $" {((IToken)cmd.tok).Filepath}({cmd.tok.line},{cmd.tok.col}): {cmd.Description.SuccessDescription}"); + $" {((IToken)cmd.tok).filename}({cmd.tok.line},{cmd.tok.col}): {cmd.Description.SuccessDescription}"); + } + + if (vcResult.coveredElements.Any()) { + tw.WriteLine(""); + tw.WriteLine(" Proof dependencies:"); + foreach (var depId in vcResult.coveredElements) { + var dep = depManager.GetFullIdDependency(depId); + tw.WriteLine($" {dep.LocationString()}: {dep.Description}"); + } } } diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index 905a097c757..2be6f6b509d 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -27,7 +27,7 @@ public static class VerificationResultLogger { public static TestProperty ResourceCountProperty = TestProperty.Register("TestResult.ResourceCount", "TestResult.ResourceCount", typeof(int), typeof(TestResult)); - public static void RaiseTestLoggerEvents(DafnyOptions options) { + public static void RaiseTestLoggerEvents(DafnyOptions options, Translator.ProofDependencyManager depManager) { var loggerConfigs = options.VerificationLoggerConfigs; // Provide just enough configuration for the loggers to work var parameters = new Dictionary { @@ -63,7 +63,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options) { } else if (loggerName == "text") { // This logger doesn't implement the ITestLogger interface because // it uses information that's tricky to encode in a TestResult. - var textLogger = new TextLogger(options.OutputWriter); + var textLogger = new TextLogger(depManager, options.OutputWriter); textLogger.Initialize(parameters); textLogger.LogResults(verificationResults); return; diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 8dd4a4e9f4c..7335636ce82 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -51,7 +51,7 @@ public async Task> GetVerificationTasksAsync( InsertChecksums = 0 < engine.Options.VerifySnapshots, ReportRanges = true }; - var translator = new Translator(errorReporter, translatorFlags); + var translator = new Translator(errorReporter, new(), translatorFlags); return translator.DoTranslation(compilation.Program, moduleDefinition); }, cancellationToken); var suffix = moduleDefinition.SanitizedName; diff --git a/customBoogie.patch b/customBoogie.patch index 22f8535f3ea..b6b6d3a78d1 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -62,7 +62,16 @@ index 4a8b2f89b..a308be9bf 100644 - -+ ++ ++ ++ ++ ++ ++ ++ ++ ++ ++ From 088eca9da96763709fdab956ceffe0ae21ff6bd0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 23 Aug 2023 15:56:57 -0700 Subject: [PATCH 02/44] Rename utility methods --- Source/DafnyCore/Verifier/Translator.ClassMembers.cs | 4 ++-- Source/DafnyCore/Verifier/Translator.cs | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 5ca67a3bde2..3da0e91bee3 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -1505,7 +1505,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } else if (s.IsOnlyFree && !bodyKind) { // don't include in split -- it would be ignored, anyhow } else { - req.Add(RequiresWithCoverage(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); + req.Add(RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); comment = null; // the free here is not linked to the free on the original expression (this is free things generated in the splitting.) } @@ -1528,7 +1528,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } else if (s.IsOnlyChecked && !bodyKind) { // don't include in split } else { - AddEnsures(ens, EnsuresWithCoverage(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, p.E, post, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithDependencies(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, p.E, post, errorMessage, successMessage, null)); } } } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 55d69e37433..83bacf7bcc5 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -4363,7 +4363,7 @@ void AddWellformednessCheck(Function f) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) { - AddEnsures(ens, EnsuresWithCoverage(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); } } } @@ -7467,7 +7467,7 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation return cmd; } - Bpl.Ensures EnsuresWithCoverage(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { + Bpl.Ensures EnsuresWithDependencies(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { Contract.Requires(tok != null); Contract.Requires(dafnyCondition != null); Contract.Ensures(Contract.Result() != null); @@ -7487,7 +7487,7 @@ Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessa return ens; } - Bpl.Requires RequiresWithCoverage(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { + Bpl.Requires RequiresWithDependencies(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { Contract.Requires(tok != null); Contract.Requires(dafnyCondition != null); Contract.Ensures(Contract.Result() != null); From adbe5bc93afeb28e3107a1711b9dd71a0846c5e1 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 23 Aug 2023 15:57:16 -0700 Subject: [PATCH 03/44] Basic tracking of assignments --- Source/DafnyCore/Verifier/ProofDependency.cs | 10 ++++++++++ Source/DafnyCore/Verifier/Translator.cs | 17 ++++++++++++----- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index afbbfc4c357..6b53cdc3c2c 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -165,6 +165,16 @@ public InvariantDependency(Expression invariant) { } } +public class AssignmentDependency : ProofDependency { + public override RangeToken RangeToken { get; } + + public override string Description => "assignment"; + + public AssignmentDependency(RangeToken rangeToken) { + this.RangeToken = rangeToken; + } +} + public class InternalDependency : ProofDependency { public override RangeToken RangeToken => null; public override string Description { get; } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 83bacf7bcc5..24b52fbfa5f 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -8838,7 +8838,9 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi bLhss.Add(rhsCanAffectPreviouslyKnownExpressions ? null : bLhs); lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { - bldr.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs)); + var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, rhs); + proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); + bldr.Add(cmd); } if (!origRhsIsHavoc || ie.Type.IsNonempty) { @@ -8868,7 +8870,9 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi bLhss.Add(rhsCanAffectPreviouslyKnownExpressions ? null : bLhs); lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { - bldr.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, rhs)); + var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, rhs); + proofDependencies.AddProofDependencyId(cmd, fse.tok, new AssignmentDependency(fse.RangeToken)); + bldr.Add(cmd); } if (!origRhsIsHavoc || field.Type.IsNonempty) { @@ -8883,7 +8887,8 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Contract.Assert(fseField != null); Check_NewRestrictions(tok, obj, fseField, rhs, bldr, et); var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fseField)), rhs)); + var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fseField)), rhs)); + proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8911,7 +8916,8 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); + var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); + proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8934,7 +8940,8 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); + var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); + proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, etran)); From d260984b6752426dbe77f1c008f4721fb2f6b7ca Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 24 Aug 2023 16:38:50 -0700 Subject: [PATCH 04/44] Track a few more proof dependencies --- .../Verifier/Translator.BoogieFactory.cs | 7 +++++++ .../Verifier/Translator.ClassMembers.cs | 2 +- .../Verifier/Translator.ExpressionWellformed.cs | 15 ++++++++------- .../Verifier/Translator.TrStatement.cs | 14 ++++++++------ Source/DafnyCore/Verifier/Translator.cs | 17 +++++++++-------- 5 files changed, 33 insertions(+), 22 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs index 886818206f2..a40fb3de5b4 100644 --- a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs @@ -205,6 +205,13 @@ public Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl return cmd; } + public Bpl.AssumeCmd TrAssumeCmdWithDependenciesApp(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func func, Bpl.QKeyValue attributes = null) { + var expr = etran.TrExpr(dafnyExpr); + var cmd = TrAssumeCmd(tok, func(expr), attributes); + proofDependencies.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(dafnyExpr)); + return cmd; + } + static Bpl.Expr RemoveLit(Bpl.Expr expr) { return GetLit(expr) ?? expr; } diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 3da0e91bee3..341cb04e1c6 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -1003,7 +1003,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi var local = BplLocalVar(NameTypeParam(tp), predef.Ty, out var lhs); localVariables.Add(local); var rhs = TypeToTy(typeMap[tp]); - builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); + builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); // TODO: track? } } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index 20def1ffb7d..c585da2aa71 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -168,7 +168,7 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List Bpl.Expr.Eq(result, e))); builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType))); @@ -1345,7 +1345,8 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var rIe = new Bpl.IdentifierExpr(rhs.tok, r); CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran); CheckCasePatternShape(pat, rIe, rhs.tok, pat.Expr.Type, builder); - builder.Add(TrAssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe))); + var substExpr = Substitute(pat.Expr, null, substMap); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe))); } CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran); @@ -1389,7 +1390,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var rhs_prime = Substitute(e.RHSs[0], null, nonGhostMap_prime); var letBody_prime = Substitute(e.Body, null, nonGhostMap_prime); builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran))); - builder.Add(TrAssumeCmd(e.tok, etran.TrExpr(rhs_prime))); + builder.Add(TrAssumeCmdWithDependencies(etran, e.tok, rhs_prime)); builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran))); var eq = Expression.CreateEq(letBody, letBody_prime, e.Body.Type); builder.Add(Assert(GetToken(e), etran.TrExpr(eq), @@ -1404,7 +1405,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r Contract.Assert(resultType != null); var bResult = etran.TrExpr(letBody); CheckSubrange(letBody.tok, bResult, letBody.Type, resultType, builder); - builder.Add(TrAssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult))); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, letBody, e => Expr.Eq(result, e))); builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType))); diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index 9f80cfb2bf4..2886f558bfc 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -501,7 +501,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List Expr.Eq(e, rIe))); } else if (stmt is TryRecoverStatement haltRecoveryStatement) { // try/recover statements are currently internal-only AST nodes that cannot be // directly used in user Dafny code. They are only generated by rewriters, and verifying @@ -997,7 +997,7 @@ private void TrIfStmt(IfStmt stmt, BoogieStmtListBuilder builder, List Bpl.IfCmd elsIf = null; b = new BoogieStmtListBuilder(this, options); if (stmt.IsBindingGuard) { - b.Add(TrAssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard)))); + b.Add(TrAssumeCmdWithDependenciesApp(etran, guard.tok, guard, Expr.Not)); } if (stmt.Els == null) { els = b.Collect(stmt.Tok); @@ -1055,12 +1055,12 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi definedness.Add(TrAssumeCmd(s.Tok, typeAntecedent)); } TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); - definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); + definedness.Add(TrAssumeCmdWithDependencies(etran, s.Range.tok, s.Range)); var ensuresDefinedness = new BoogieStmtListBuilder(this, options); foreach (var ens in s.Ens) { TrStmt_CheckWellformed(ens.E, ensuresDefinedness, locals, etran, false); - ensuresDefinedness.Add(TrAssumeCmd(ens.E.tok, etran.TrExpr(ens.E))); + ensuresDefinedness.Add(TrAssumeCmdWithDependencies(etran, ens.E.tok, ens.E)); } PathAsideBlock(s.Tok, ensuresDefinedness, definedness); @@ -1409,7 +1409,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, foreach (AttributedExpression loopInv in s.Invariants) { var (errorMessage, successMessage) = CustomErrorMessage(loopInv.Attributes); TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false); - invDefinednessBuilder.Add(TrAssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E))); + invDefinednessBuilder.Add(TrAssumeCmdWithDependencies(etran, loopInv.E.tok, loopInv.E)); invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran)))); var ss = TrSplitExpr(loopInv.E, etran, false, out var splitHappened); @@ -1422,7 +1422,9 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, if (split.IsChecked) { invariants.Add(Assert(split.Tok, wInv, new PODesc.LoopInvariant(errorMessage, successMessage))); // TODO: it would be fine to have this use {:subsumption 0} } else { - invariants.Add(TrAssumeCmd(split.E.tok, wInv)); + var cmd = TrAssumeCmd(split.E.tok, wInv); + proofDependencies.AddProofDependencyId(cmd, loopInv.E.tok, new InvariantDependency(loopInv.E)); + invariants.Add(cmd); } } } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 24b52fbfa5f..516a267e6fe 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -123,7 +123,6 @@ public class ProofDependencyManager { private UInt64 proofDependencyIdCount = 0; public string GetProofDependencyId(ProofDependency dep) { - // TODO: track whether we've seen this node before var idString = $"id{proofDependencyIdCount}"; ProofDependenciesById[idString] = dep; proofDependencyIdCount++; @@ -1820,13 +1819,13 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type; // resolve here Expression cond = new FreshExpr(iter.tok, setDiff); cond.Type = Type.Bool; // resolve here - builder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(cond))); + builder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, cond)); // check wellformedness of postconditions var yeBuilder = new BoogieStmtListBuilder(this, options); var endBuilder = new BoogieStmtListBuilder(this, options); // In the yield-ensures case: assume this.Valid(); - yeBuilder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(validCall))); + yeBuilder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, validCall)); Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); for (int i = 0; i < iter.OutsFields.Count; i++) { var y = iter.OutsFields[i]; @@ -1841,9 +1840,9 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { concat.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; concat.Type = oldThisYs.Type; // resolve here // In the yield-ensures case: assume this.ys == old(this.ys) + [this.y]; - yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); + yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); // TODO: track? // In the ensures case: assume this.ys == old(this.ys); - endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); + endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); // TODO: track? } foreach (var p in iter.YieldEnsures) { @@ -3689,7 +3688,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable); - builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); + builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); // TODO: track? } //generating trait post-conditions with class variables @@ -4521,7 +4520,9 @@ void AddWellformednessCheck(Function f) { wfo = new WFOptions(null, true, true /* do delayed reads checks */); CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran); if (f.Result != null) { - bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, TrVar(f.tok, f.Result)))); + var cmd = TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, TrVar(f.tok, f.Result))); + proofDependencies.AddProofDependencyId(cmd, f.tok, new InternalDependency("function definition")); // TODO + bodyCheckBuilder.Add(cmd); } wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder); @@ -7689,7 +7690,7 @@ void YieldHavoc(IToken tok, IteratorDecl iter, BoogieStmtListBuilder builder, Ex new List())); // assume YieldRequires; foreach (var p in iter.YieldRequires) { - builder.Add(TrAssumeCmd(tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, tok, p.E)); } // $_OldIterHeap := Heap; builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr)); From d6f9eeacbd694feae857c69abbdb0be502aecb91 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 09:40:03 -0700 Subject: [PATCH 05/44] Fix customBoogie.patch --- customBoogie.patch | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/customBoogie.patch b/customBoogie.patch index b6b6d3a78d1..fac7c377fb8 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -57,21 +57,12 @@ diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.cspr index 4a8b2f89b..a308be9bf 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj -@@ -31,7 +31,7 @@ +@@ -31,5 +31,5 @@ -- -+ -+ -+ -+ -+ -+ -+ -+ -+ -+ +- ++ From 8bb2303364bf05fd99d332a4ddf8e1bd37cf9bad Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 13:13:57 -0700 Subject: [PATCH 06/44] Fix unit test for slightly different message --- Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 36ab1f6d369..58f2d9ea50f 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -145,7 +145,7 @@ await AssertHoverMatches(documentItem, (6, 6), Did prove: `i % 2 == 0`" ); await AssertHoverMatches(documentItem, (6, 6), - @"**Success:**???the precondition always holds + @"**Success:**???this precondition always holds Did prove: `i > 0`" ); await AssertHoverMatches(documentItem, (7, 6), From 671b7f6b81506f8c48aff6741bf1b2783a41a48e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 14:56:22 -0700 Subject: [PATCH 07/44] Revert message change for preconditions --- Source/DafnyCore/Verifier/ProofObligationDescription.cs | 2 +- Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index de343d8f971..4e6d1f4e800 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -350,7 +350,7 @@ public AssertStatement([CanBeNull] string customErrMsg, [CanBeNull] string custo // The Boogie version does not support custom error messages yet public class RequiresDescription : ProofObligationDescriptionCustomMessages { public override string DefaultSuccessDescription => - "this precondition always holds"; + "the precondition always holds"; public override string DefaultFailureDescription => "this is the precondition that could not be proved"; diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 58f2d9ea50f..05a3f536cf4 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -145,7 +145,7 @@ await AssertHoverMatches(documentItem, (6, 6), Did prove: `i % 2 == 0`" ); await AssertHoverMatches(documentItem, (6, 6), - @"**Success:**???this precondition always holds + @"**Success:**???the precondition always holds Did prove: `i > 0`" ); await AssertHoverMatches(documentItem, (7, 6), From 9ab8bfd0e51fad03869e589f3390bd3c2ec4326f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 16:40:29 -0700 Subject: [PATCH 08/44] Better dependency messages, assignment tracking --- Source/DafnyCore/Verifier/ProofDependency.cs | 76 +++++++--------- .../Verifier/Translator.BoogieFactory.cs | 11 +-- .../Verifier/Translator.ClassMembers.cs | 10 +-- .../Translator.ExpressionWellformed.cs | 67 +++++++------- .../Verifier/Translator.TrStatement.cs | 46 +++++----- Source/DafnyCore/Verifier/Translator.cs | 87 ++++++++++--------- 6 files changed, 145 insertions(+), 152 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index 6b53cdc3c2c..f014ab85ea1 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -1,9 +1,8 @@ -using System; using JetBrains.Annotations; -using Microsoft.Boogie; using Microsoft.Dafny; using IToken = Microsoft.Dafny.IToken; using PODesc = Microsoft.Dafny.ProofObligationDescription; +using ResolutionContext = Microsoft.Boogie.ResolutionContext; namespace DafnyCore.Verifier; @@ -13,13 +12,17 @@ public abstract class ProofDependency { public abstract RangeToken RangeToken { get; } public string LocationString() { - return RangeToken?.StartToken is null - ? "" - : $"{RangeToken.StartToken.filename}({RangeToken.StartToken.line},{RangeToken.StartToken.col - 1})"; + if (RangeToken?.StartToken is null) { + return ""; + } + var fn = RangeToken.StartToken.filename; + var sl = RangeToken.StartToken.line; + var sc = RangeToken.StartToken.col - 1; + return $"{fn}({sl},{sc})"; } public string RangeString() { - if (RangeToken is null) { + if (RangeToken?.StartToken is null) { return ""; } var fn = RangeToken.StartToken.filename; @@ -56,7 +59,7 @@ public class RequiresDependency : ProofDependency { requires.RangeToken; public override string Description => - $"requires {requires.RangeToken.PrintOriginal()}"; + $"requires clause"; public RequiresDependency(Expression requires) { this.requires = requires; @@ -70,7 +73,7 @@ public class EnsuresDependency : ProofDependency { ensures.RangeToken; public override string Description => - $"ensures {ensures.RangeToken.PrintOriginal()}"; + "ensures clause"; public EnsuresDependency(Expression ensures) { this.ensures = ensures; @@ -85,7 +88,7 @@ public class CallRequiresDependency : ProofDependency { call.RangeToken; public override string Description => - $"{requires.Description} from call at {call.Description}"; + $"requires clause at {requires.RangeString()} from call"; public CallRequiresDependency(CallDependency call, RequiresDependency requires) { this.call = call; @@ -101,7 +104,7 @@ public class CallEnsuresDependency : ProofDependency { call.RangeToken; public override string Description => - $"{ensures.Description} from call at {call.Description}"; + $"ensures clause at {ensures.RangeString()} from call"; public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { this.call = call; @@ -116,27 +119,13 @@ public class CallDependency : ProofDependency { call.RangeToken; public override string Description => - $"{LocationString()}: {OriginalString()};"; + $"call"; public CallDependency(CallStmt call) { this.call = call; } } -public class AssertionDependency : ProofDependency { - private Expression expr; - - public override RangeToken RangeToken => - expr.RangeToken; - - public override string Description => - $"assert {OriginalString()};"; - - public AssertionDependency(Expression expr) { - this.expr = expr; - } -} - public class AssumptionDependency : ProofDependency { private Expression expr; @@ -144,9 +133,12 @@ public class AssumptionDependency : ProofDependency { expr.RangeToken; public override string Description => - $"assume {OriginalString()}"; + comment ?? $"assume {OriginalString()}"; - public AssumptionDependency(Expression expr) { + private string comment; + + public AssumptionDependency(string comment, Expression expr) { + this.comment = comment; this.expr = expr; } } @@ -158,7 +150,7 @@ public class InvariantDependency : ProofDependency { invariant.RangeToken; public override string Description => - $"invariant {invariant.RangeToken.PrintOriginal()}"; + $"loop invariant"; public InvariantDependency(Expression invariant) { this.invariant = invariant; @@ -168,31 +160,23 @@ public InvariantDependency(Expression invariant) { public class AssignmentDependency : ProofDependency { public override RangeToken RangeToken { get; } - public override string Description => "assignment"; + public override string Description => + "assignment (or return)"; public AssignmentDependency(RangeToken rangeToken) { this.RangeToken = rangeToken; } } -public class InternalDependency : ProofDependency { - public override RangeToken RangeToken => null; - public override string Description { get; } - - public InternalDependency(string description) { - Description = description; - } -} - -// Temporary placeholder. Remove when all creation sites use a different -// implementation. -public class NodeOnlyDependency : ProofDependency { - public override RangeToken RangeToken { get; } +public class FunctionDefinitionDependency : ProofDependency { + public override RangeToken RangeToken => function.RangeToken; public override string Description => - $"{LocationString()}: {OriginalString()}"; + $"function definition for {function.Name}"; + + private Function function; - public NodeOnlyDependency([NotNull] Node node) { - RangeToken = node.RangeToken; + public FunctionDefinitionDependency(Function f) { + function = f; } -} +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs index a40fb3de5b4..e3998fd2972 100644 --- a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs @@ -198,17 +198,14 @@ public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyV return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes); } - public Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Bpl.QKeyValue attributes = null) { - var expr = etran.TrExpr(dafnyExpr); - var cmd = TrAssumeCmd(tok, expr, attributes); - proofDependencies.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(dafnyExpr)); - return cmd; + public Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, string comment = null, Bpl.QKeyValue attributes = null) { + return TrAssumeCmdWithDependenciesApp(etran, tok, dafnyExpr, e => e, comment, attributes); } - public Bpl.AssumeCmd TrAssumeCmdWithDependenciesApp(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func func, Bpl.QKeyValue attributes = null) { + public Bpl.AssumeCmd TrAssumeCmdWithDependenciesApp(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func func, string comment = null, Bpl.QKeyValue attributes = null) { var expr = etran.TrExpr(dafnyExpr); var cmd = TrAssumeCmd(tok, func(expr), attributes); - proofDependencies.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(dafnyExpr)); + proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(comment, dafnyExpr)); return cmd; } diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 341cb04e1c6..7916c259043 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -682,7 +682,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP } // check well-formedness of the preconditions, and then assume each one of them foreach (AttributedExpression p in m.Req) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "method requires clause"); } // check well-formedness of the modifies clauses CheckFrameWellFormed(new WFOptions(), m.Mod.Expressions, localVariables, builder, etran); @@ -719,7 +719,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP // check wellformedness of postconditions foreach (AttributedExpression p in m.Ens) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "method ensures clause"); } stmts = builder.Collect(m.tok); @@ -1003,7 +1003,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi var local = BplLocalVar(NameTypeParam(tp), predef.Ty, out var lhs); localVariables.Add(local); var rhs = TypeToTy(typeMap[tp]); - builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); // TODO: track? + builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); } } @@ -1236,7 +1236,7 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex Contract.Requires(substMap != null); //generating class post-conditions foreach (var en in m.Ens) { - builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, en.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, en.E, "overridden ensures clause")); } //generating trait post-conditions with class variables FunctionCallSubstituter sub = null; @@ -1259,7 +1259,7 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E FunctionCallSubstituter sub = null; foreach (var req in m.OverriddenMethod.Req) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass); - builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, sub.Substitute(req.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, sub.Substitute(req.E), "overridden requires clause")); } //generating class pre-conditions foreach (var s in m.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index c585da2aa71..3305a69cc53 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -128,7 +128,7 @@ public void ProcessSavedReadsChecks(List locals, BoogieStmtListBuilder } } - void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, string comment) { Contract.Requires(expr != null); Contract.Requires(expr.Type != null && expr.Type.IsBoolType); Contract.Requires(wfOptions != null); @@ -141,8 +141,8 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List e1; // } var bAnd = new BoogieStmtListBuilder(this, options); - CheckWellformedAndAssume(e.E0, wfOptions, locals, bAnd, etran); - CheckWellformedAndAssume(e.E1, wfOptions, locals, bAnd, etran); + CheckWellformedAndAssume(e.E0, wfOptions, locals, bAnd, etran, comment); + CheckWellformedAndAssume(e.E1, wfOptions, locals, bAnd, etran, comment); var bImp = new BoogieStmtListBuilder(this, options); - bImp.Add(TrAssumeCmdWithDependencies(etran, expr.tok, expr)); + bImp.Add(TrAssumeCmdWithDependencies(etran, expr.tok, expr, comment)); builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok))); } return; @@ -166,10 +166,10 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List @@ -246,7 +246,8 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, /// See class WFOptions for descriptions of the specified options. /// void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr result, Type resultType, - List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, + string resultDescription = null) { Contract.Requires(expr != null); Contract.Requires(wfOptions != null); Contract.Requires((result == null) == (resultType == null)); @@ -713,7 +714,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re } if (wfOptions.AssertKv == null) { // assume only if no given assert attribute is given - builder.Add(TrAssumeCmdWithDependencies(etran, callExpr.tok, precond)); + builder.Add(TrAssumeCmdWithDependencies(etran, callExpr.tok, precond, "function precondition")); } } if (wfOptions.DoReadsChecks) { @@ -1090,7 +1091,7 @@ void CheckOperand(Expression operand) { resultIe = new Bpl.IdentifierExpr(body.tok, resultVar); rangeType = lam.Type.AsArrowType.Result; } - CheckWellformedWithResult(body, newOptions, resultIe, rangeType, locals, b, comprehensionEtran); + CheckWellformedWithResult(body, newOptions, resultIe, rangeType, locals, b, comprehensionEtran, "lambda expression"); }); if (mc != null) { @@ -1138,15 +1139,16 @@ void CheckOperand(Expression operand) { Contract.Assert(letExpr != null); CheckWellformedLetExprWithResult(letExpr, wfOptions, result, resultType, locals, bThen, etran, false); } else { - CheckWellformedWithResult(e.Thn, wfOptions, result, resultType, locals, bThen, etran); + CheckWellformedWithResult(e.Thn, wfOptions, result, resultType, locals, bThen, etran, "if expression then branch"); } - CheckWellformedWithResult(e.Els, wfOptions, result, resultType, locals, bElse, etran); + CheckWellformedWithResult(e.Els, wfOptions, result, resultType, locals, bElse, etran, "if expression else branch"); builder.Add(new Bpl.IfCmd(iteExpr.tok, etran.TrExpr(e.Test), bThen.Collect(iteExpr.tok), null, bElse.Collect(iteExpr.tok))); result = null; break; } case MatchExpr matchExpr: result = TrMatchExpr(matchExpr, wfOptions, result, resultType, locals, builder, etran); + resultDescription = "match expression"; break; case DatatypeUpdateExpr updateExpr: { var e = updateExpr; @@ -1163,18 +1165,18 @@ void CheckOperand(Expression operand) { CheckNotGhostVariant(e.InCompiledContext, updateExpr, e.Root, "update of", e.Members, e.LegalSourceConstructors, builder, etran); - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran); + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran, resultDescription); result = null; break; } case ConcreteSyntaxExpression expression: { var e = expression; - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran); + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran, resultDescription); result = null; break; } case NestedMatchExpr nestedMatchExpr: - CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, result, resultType, locals, builder, etran); + CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, result, resultType, locals, builder, etran, resultDescription); result = null; break; case BoogieFunctionCall call: { @@ -1193,7 +1195,8 @@ void CheckOperand(Expression operand) { Contract.Assert(resultType != null); var bResult = etran.TrExpr(expr); CheckSubrange(expr.tok, bResult, expr.Type, resultType, builder); - builder.Add(TrAssumeCmdWithDependenciesApp(etran, expr.tok, expr, e => Bpl.Expr.Eq(result, e))); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, expr.tok, expr, e => Bpl.Expr.Eq(result, e), + resultDescription)); builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType))); @@ -1239,7 +1242,7 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); Bpl.Expr ct = CtorInvocation(mc, me.Source.Type, etran, locals, b, NOALLOC, false); // generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ... - CheckWellformedWithResult(mc.Body, wfOptions, result, resultType, locals, b, etran); + CheckWellformedWithResult(mc.Body, wfOptions, result, resultType, locals, b, etran, "match expression branch result"); ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els); els = null; } @@ -1262,7 +1265,7 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Expr TrStmt(stmtExpr.S, builder, locals, etran); } - CheckWellformedWithResult(stmtExpr.E, options, result, resultType, locals, builder, etran); + CheckWellformedWithResult(stmtExpr.E, options, result, resultType, locals, builder, etran, "statement expression result"); } /// @@ -1343,12 +1346,12 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type))); locals.Add(r); var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran); + CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran, "let expression binding RHS well-formed"); CheckCasePatternShape(pat, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); - builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe))); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); } - CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran, "let expression result"); } else { // CheckWellformed(var b :| RHS(b); Body(b)) = @@ -1390,7 +1393,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var rhs_prime = Substitute(e.RHSs[0], null, nonGhostMap_prime); var letBody_prime = Substitute(e.Body, null, nonGhostMap_prime); builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran))); - builder.Add(TrAssumeCmdWithDependencies(etran, e.tok, rhs_prime)); + builder.Add(TrAssumeCmdWithDependencies(etran, e.tok, rhs_prime, "assign-such-that constraint")); builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran))); var eq = Expression.CreateEq(letBody, letBody_prime, e.Body.Type); builder.Add(Assert(GetToken(e), etran.TrExpr(eq), @@ -1405,7 +1408,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r Contract.Assert(resultType != null); var bResult = etran.TrExpr(letBody); CheckSubrange(letBody.tok, bResult, letBody.Type, resultType, builder); - builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, letBody, e => Expr.Eq(result, e))); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, letBody, e => Expr.Eq(result, e), "let expression")); builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType))); diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index 2886f558bfc..d65878ae7fa 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -111,7 +111,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List lhs == null)); // This generates the assignments, and gives them to us as finalRhss. - var finalRhss = ProcessUpdateAssignRhss(lhss, rhss, builder, locals, etran); + var finalRhss = ProcessUpdateAssignRhss(lhss, rhss, builder, locals, etran, stmt); // ProcessLhss has laid down framing conditions and the ProcessUpdateAssignRhss will check subranges (nats), // but we need to generate the distinctness condition (two LHS are equal only when the RHS is also // equal). We need both the LHS and the RHS to do this, which is why we need to do it here. @@ -499,9 +499,9 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List Expr.Eq(e, rIe))); + builder.Add(TrAssumeCmdWithDependenciesApp(etran, s.tok, pat.Expr, e => Expr.Eq(e, rIe), "variable declaration")); } else if (stmt is TryRecoverStatement haltRecoveryStatement) { // try/recover statements are currently internal-only AST nodes that cannot be // directly used in user Dafny code. They are only generated by rewriters, and verifying @@ -595,7 +595,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, // Adding the assume stmt, resetting the stmtContext stmtContext = StmtType.ASSUME; adjustFuelForExists = true; - b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr)); + b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement")); stmtContext = StmtType.NONE; } } @@ -606,7 +606,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, // Adding the assume stmt, resetting the stmtContext stmtContext = StmtType.ASSUME; adjustFuelForExists = true; - builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr)); + builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement")); stmtContext = StmtType.NONE; } } else if (stmt is ExpectStmt) { @@ -634,7 +634,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, var s = (AssumeStmt)stmt; stmtContext = StmtType.ASSUME; TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false); - builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, etran.TrAttributes(stmt.Attributes, null))); + builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, "assume statement", etran.TrAttributes(stmt.Attributes, null))); stmtContext = StmtType.NONE; // done with translating assume stmt. } this.fuelContext = FuelSetting.PopFuelContext(); @@ -689,7 +689,7 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List: AddComment(b, stmt, "assume lhs"); - b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, CalcStmt.Lhs(stmt.Steps[i]))); + b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, CalcStmt.Lhs(stmt.Steps[i]), "calc statement step")); } // hint: AddComment(b, stmt, "Hint" + i.ToString()); @@ -735,7 +735,7 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List 1) { - builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Result)); + builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Result, "calc statement result")); } } CurrentIdGenerator.Pop(); @@ -997,7 +997,7 @@ private void TrIfStmt(IfStmt stmt, BoogieStmtListBuilder builder, List Bpl.IfCmd elsIf = null; b = new BoogieStmtListBuilder(this, options); if (stmt.IsBindingGuard) { - b.Add(TrAssumeCmdWithDependenciesApp(etran, guard.tok, guard, Expr.Not)); + b.Add(TrAssumeCmdWithDependenciesApp(etran, guard.tok, guard, Expr.Not, "if statement binding guard")); } if (stmt.Els == null) { els = b.Collect(stmt.Tok); @@ -1055,12 +1055,12 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi definedness.Add(TrAssumeCmd(s.Tok, typeAntecedent)); } TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); - definedness.Add(TrAssumeCmdWithDependencies(etran, s.Range.tok, s.Range)); + definedness.Add(TrAssumeCmdWithDependencies(etran, s.Range.tok, s.Range, "forall statement range")); var ensuresDefinedness = new BoogieStmtListBuilder(this, options); foreach (var ens in s.Ens) { TrStmt_CheckWellformed(ens.E, ensuresDefinedness, locals, etran, false); - ensuresDefinedness.Add(TrAssumeCmdWithDependencies(etran, ens.E.tok, ens.E)); + ensuresDefinedness.Add(TrAssumeCmdWithDependencies(etran, ens.E.tok, ens.E, "forall statement ensures clause")); } PathAsideBlock(s.Tok, ensuresDefinedness, definedness); @@ -1109,12 +1109,12 @@ void TrAssignment(Statement stmt, Expression lhs, AssignmentRhs rhs, Contract.Requires(predef != null); var lhss = new List() { lhs }; - ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, true, builder, locals, etran, + ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, true, builder, locals, etran, stmt, out var lhsBuilder, out var bLhss, out var ignore1, out var ignore2, out var ignore3); Contract.Assert(lhsBuilder.Count == 1 && bLhss.Count == 1); // guaranteed by postcondition of ProcessLhss var rhss = new List() { rhs }; - ProcessRhss(lhsBuilder, bLhss, lhss, rhss, builder, locals, etran); + ProcessRhss(lhsBuilder, bLhss, lhss, rhss, builder, locals, etran, stmt); builder.AddCaptureState(stmt); } @@ -1409,7 +1409,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, foreach (AttributedExpression loopInv in s.Invariants) { var (errorMessage, successMessage) = CustomErrorMessage(loopInv.Attributes); TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false); - invDefinednessBuilder.Add(TrAssumeCmdWithDependencies(etran, loopInv.E.tok, loopInv.E)); + invDefinednessBuilder.Add(TrAssumeCmdWithDependencies(etran, loopInv.E.tok, loopInv.E, "loop invariant")); invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran)))); var ss = TrSplitExpr(loopInv.E, etran, false, out var splitHappened); @@ -1423,7 +1423,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, invariants.Add(Assert(split.Tok, wInv, new PODesc.LoopInvariant(errorMessage, successMessage))); // TODO: it would be fine to have this use {:subsumption 0} } else { var cmd = TrAssumeCmd(split.E.tok, wInv); - proofDependencies.AddProofDependencyId(cmd, loopInv.E.tok, new InvariantDependency(loopInv.E)); + proofDependencies?.AddProofDependencyId(cmd, loopInv.E.tok, new InvariantDependency(loopInv.E)); invariants.Add(cmd); } } @@ -1614,7 +1614,7 @@ void TrAlternatives(List alternatives, Bpl.Cmd elseCase0, Bp var exists = (ExistsExpr)alternative.Guard; // the original (that is, not alpha-renamed) guard IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran, isGhost); } else { - b.Add(TrAssumeCmdWithDependencies(etran, alternative.Guard.tok, alternative.Guard)); + b.Add(TrAssumeCmdWithDependencies(etran, alternative.Guard.tok, alternative.Guard, "alternative guard")); } var prevDefiniteAssignmentTrackerCount = definiteAssignmentTrackers.Count; TrStmtList(alternative.Body, b, locals, etran); @@ -1636,7 +1636,7 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List locals Contract.Requires(!(s.Method is Constructor) || (s.Lhs.Count == 0 && actualReceiver != null)); var tySubst = s.MethodSelect.TypeArgumentSubstitutionsWithParents(); - ProcessLhss(s.Lhs, true, true, builder, locals, etran, out var lhsBuilders, out var bLhss, + ProcessLhss(s.Lhs, true, true, builder, locals, etran, s, out var lhsBuilders, out var bLhss, out _, out _, out _, s.OriginalInitialLhs); Contract.Assert(s.Lhs.Count == lhsBuilders.Count); Contract.Assert(s.Lhs.Count == bLhss.Count); @@ -1930,7 +1930,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E // Make the call AddReferencedMember(callee); Bpl.CallCmd call = Call(tok, MethodName(callee, kind), ins, outs); - proofDependencies.AddProofDependencyId(call, tok, new CallDependency(cs)); + proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs)); if ( (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 516a267e6fe..bf658e1b521 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -164,7 +164,7 @@ public ProofDependency GetFullIdDependency(string idString) { } } - private ProofDependencyManager proofDependencies; + private ProofDependencyManager? proofDependencies; // optimizing translation readonly ISet referencedMembers = new HashSet(); @@ -1764,7 +1764,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { } // check well-formedness of the preconditions, and then assume each one of them foreach (var p in iter.Requires) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "iterator requires clause"); } // check well-formedness of the modifies and reads clauses CheckFrameWellFormed(new WFOptions(), iter.Modifies.Expressions, localVariables, builder, etran); @@ -1776,7 +1776,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { // Next, we assume about this.* whatever we said that the iterator constructor promises foreach (var p in iter.Member_Init.Ens) { - builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E, "iterator ensures clause")); } // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this}) @@ -1798,7 +1798,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { // check well-formedness of the user-defined part of the yield-requires foreach (var p in iter.YieldRequires) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "iterator yield-requires clause"); } // save the heap (representing the state where yield-requires holds): $_OldIterHeap := Heap; @@ -1819,13 +1819,13 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type; // resolve here Expression cond = new FreshExpr(iter.tok, setDiff); cond.Type = Type.Bool; // resolve here - builder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, cond)); + builder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(cond))); // check wellformedness of postconditions var yeBuilder = new BoogieStmtListBuilder(this, options); var endBuilder = new BoogieStmtListBuilder(this, options); // In the yield-ensures case: assume this.Valid(); - yeBuilder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, validCall)); + yeBuilder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, validCall, "iterator validity")); Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); for (int i = 0; i < iter.OutsFields.Count; i++) { var y = iter.OutsFields[i]; @@ -1840,16 +1840,16 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { concat.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; concat.Type = oldThisYs.Type; // resolve here // In the yield-ensures case: assume this.ys == old(this.ys) + [this.y]; - yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); // TODO: track? + yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); // In the ensures case: assume this.ys == old(this.ys); - endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); // TODO: track? + endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); } foreach (var p in iter.YieldEnsures) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran, "iterator yield-ensures clause"); } foreach (var p in iter.Ensures) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, endBuilder, yeEtran); + CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, endBuilder, yeEtran, "iterator ensures clause"); } builder.Add(new Bpl.IfCmd(iter.tok, null, yeBuilder.Collect(iter.tok), null, endBuilder.Collect(iter.tok))); @@ -1909,12 +1909,12 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { // don't include this precondition here Contract.Assert(p.Label.E != null); // it should already have been recorded } else { - builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E, "iterator constructor requires clause")); } } foreach (var p in iter.Member_Init.Ens) { // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet - builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, p.E.tok, p.E, "iterator constructor ensures clause")); } // add the _yieldCount variable, and assume its initial value to be 0 yieldCountVariable = new Bpl.LocalVariable(iter.tok, @@ -3656,7 +3656,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //generating class post-conditions foreach (var en in f.Ens) { - builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, en.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, en.E, "overridden function ensures clause")); } //generating assume C.F(ins) == out, if a result variable was given @@ -3688,7 +3688,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable); - builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); // TODO: track? + builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); } //generating trait post-conditions with class variables @@ -3792,7 +3792,7 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde FunctionCallSubstituter sub = null; foreach (var req in f.OverriddenFunction.Req) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass); - builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, sub.Substitute(req.E))); + builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, sub.Substitute(req.E), "overridden function requires clause")); } //generating class pre-conditions foreach (var s in f.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { @@ -4423,7 +4423,7 @@ void AddWellformednessCheck(Function f) { p.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(p.E); CheckWellformed(p.E, wfo, locals, builder, etran); } else { - CheckWellformedAndAssume(p.E, wfo, locals, builder, etran); + CheckWellformedAndAssume(p.E, wfo, locals, builder, etran, "requires clause"); } } wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); @@ -4486,7 +4486,7 @@ void AddWellformednessCheck(Function f) { // Now for the ensures clauses foreach (AttributedExpression p in f.Ens) { // assume the postcondition for the benefit of checking the remaining postconditions - CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran); + CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); } // Here goes the body (and include both termination checks and reads checks) BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(this, options); @@ -4518,10 +4518,10 @@ void AddWellformednessCheck(Function f) { Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); wfo = new WFOptions(null, true, true /* do delayed reads checks */); - CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran); + CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran, "function call result"); if (f.Result != null) { var cmd = TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, TrVar(f.tok, f.Result))); - proofDependencies.AddProofDependencyId(cmd, f.tok, new InternalDependency("function definition")); // TODO + proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); bodyCheckBuilder.Add(cmd); } wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder); @@ -4632,7 +4632,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { var constraintCheckBuilder = new BoogieStmtListBuilder(this, options); var builderInitializationArea = new BoogieStmtListBuilder(this, options); var wfo = new WFOptions(null, true, true /* do delayed reads checks */); - CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran); + CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint"); wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, constraintCheckBuilder); // Check that the type is inhabited. @@ -7420,7 +7420,7 @@ public override IToken WithVal(string newVal) { Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) { var cmd = Assert(tok, condition, description, tok, kv); - proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); + proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); return cmd; } @@ -7438,7 +7438,7 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe } else { cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv); } - proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); + proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); return cmd; } @@ -7464,7 +7464,7 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation cmd = TrAssertCmdDesc(tok, condition, desc, new Bpl.QKeyValue(tok, "subsumption", args, kv)); } - proofDependencies.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, desc)); + proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, desc)); return cmd; } @@ -7474,7 +7474,7 @@ Bpl.Ensures EnsuresWithDependencies(IToken tok, bool free, Expression dafnyCondi Contract.Ensures(Contract.Result() != null); var ens = Ensures(tok, free, condition, errorMessage, successMessage, comment); - proofDependencies.AddProofDependencyId(ens, tok, new EnsuresDependency(dafnyCondition)); + proofDependencies?.AddProofDependencyId(ens, tok, new EnsuresDependency(dafnyCondition)); return ens; } @@ -7494,7 +7494,7 @@ Bpl.Requires RequiresWithDependencies(IToken tok, bool free, Expression dafnyCon Contract.Ensures(Contract.Result() != null); var req = Requires(tok, free, condition, errorMessage, successMessage, comment); - proofDependencies.AddProofDependencyId(req, tok, new RequiresDependency(dafnyCondition)); + proofDependencies?.AddProofDependencyId(req, tok, new RequiresDependency(dafnyCondition)); return req; } @@ -7690,7 +7690,7 @@ void YieldHavoc(IToken tok, IteratorDecl iter, BoogieStmtListBuilder builder, Ex new List())); // assume YieldRequires; foreach (var p in iter.YieldRequires) { - builder.Add(TrAssumeCmdWithDependencies(etran, tok, p.E)); + builder.Add(TrAssumeCmdWithDependencies(etran, tok, p.E, "iterator yield-requires clause")); } // $_OldIterHeap := Heap; builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr)); @@ -8581,7 +8581,7 @@ Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator void ProcessRhss(List lhsBuilder, List bLhss, List lhss, List rhss, - BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, Statement stmt) { Contract.Requires(lhsBuilder != null); Contract.Requires(bLhss != null); Contract.Requires(cce.NonNullElements(lhss)); @@ -8618,7 +8618,7 @@ void ProcessRhss(List lhsBuilder, List lhsBuilder, List ProcessUpdateAssignRhss(List lhss, List rhss, - BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, + Statement stmt) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(builder != null); @@ -8669,7 +8670,7 @@ void ProcessRhss(List lhsBuilder, List void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressions, bool checkDistinctness, - BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, + BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, Statement stmt, out List lhsBuilders, out List bLhss, out Bpl.Expr[] prevObj, out Bpl.Expr[] prevIndex, out string[] prevNames, Expression originalInitialLhs = null) { @@ -8840,7 +8841,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, rhs); - proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); + proofDependencies?.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(stmt.RangeToken)); bldr.Add(cmd); } @@ -8872,7 +8873,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, rhs); - proofDependencies.AddProofDependencyId(cmd, fse.tok, new AssignmentDependency(fse.RangeToken)); + proofDependencies?.AddProofDependencyId(cmd, fse.tok, new AssignmentDependency(stmt.RangeToken)); bldr.Add(cmd); } @@ -8889,7 +8890,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Check_NewRestrictions(tok, obj, fseField, rhs, bldr, et); var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fseField)), rhs)); - proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); + proofDependencies?.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(stmt.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8918,7 +8919,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); - proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); + proofDependencies?.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(stmt.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8942,7 +8943,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? var cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); - proofDependencies.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(lhs.RangeToken)); + proofDependencies?.AddProofDependencyId(cmd, lhs.tok, new AssignmentDependency(stmt.RangeToken)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, etran)); @@ -8974,7 +8975,8 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi /// Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhsVar, Type lhsType, AssignmentRhs rhs, Type rhsTypeConstraint, - BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, + Statement stmt) { Contract.Requires(tok != null); Contract.Requires(rhs != null); Contract.Requires(rhsTypeConstraint != null); @@ -9026,11 +9028,14 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment var cmd = Bpl.Cmd.SimpleAssign(tok, bGivenLhs, CondApplyBox(tok, bRhs, e.Expr.Type, lhsType)); + proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); builder.Add(cmd); return bGivenLhs; } else { // box from RHS type to tmp-var type, then do the assignment; then return LHS, boxed from tmp-var type to result type var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, CondApplyBox(tok, bRhs, e.Expr.Type, rhsTypeConstraint)); + var rhsTok = (Microsoft.Dafny.IToken)bRhs.tok; + proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); builder.Add(cmd); return CondApplyBox(tok, bLhs, rhsTypeConstraint, lhsType); } @@ -9128,11 +9133,15 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment - builder.Add(Bpl.Cmd.SimpleAssign(tok, bGivenLhs, CondApplyBox(tok, nw, tRhs.Type, lhsType))); + var cmd = Bpl.Cmd.SimpleAssign(tok, bGivenLhs, CondApplyBox(tok, nw, tRhs.Type, lhsType)); + proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); + builder.Add(cmd); return bGivenLhs; } else { // do the assignment, then box the result - builder.Add(Bpl.Cmd.SimpleAssign(tok, bLhs, nw)); + var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, nw); + proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); + builder.Add(cmd); return CondApplyBox(tok, bLhs, tRhs.Type, lhsType); } } From 2b8d5800a0a3644f4d5fc859079ddae5dfbb9c78 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 16:41:05 -0700 Subject: [PATCH 09/44] Order text logger output by source location Previously it was sorted by name --- Source/DafnyDriver/TextLogger.cs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index e91050ae32f..6d4975286c4 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -21,7 +21,9 @@ public void Initialize(Dictionary parameters) { } public void LogResults(List<(Implementation, VerificationResult)> verificationResults) { - var orderedResults = verificationResults.OrderBy(vr => vr.Item1.VerboseName); + var orderedResults = + verificationResults.OrderBy(vr => + (vr.Item1.tok.filename, vr.Item1.tok.line, vr.Item1.tok.col)); foreach (var (implementation, result) in orderedResults) { tw.WriteLine(""); tw.WriteLine($"Results for {implementation.VerboseName}"); @@ -51,7 +53,7 @@ public void LogResults(List<(Implementation, VerificationResult)> verificationRe tw.WriteLine(" Proof dependencies:"); foreach (var depId in vcResult.coveredElements) { var dep = depManager.GetFullIdDependency(depId); - tw.WriteLine($" {dep.LocationString()}: {dep.Description}"); + tw.WriteLine($" {dep.RangeString()}: {dep.Description}"); } } From ac55f3f05e2e00911b656135e0c8ba210c841c4b Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 16:41:28 -0700 Subject: [PATCH 10/44] Add test for proof dependency logging --- Test/logger/ProofDependencyLogging.dfy | 424 +++++++++++++++++++++++++ 1 file changed, 424 insertions(+) create mode 100644 Test/logger/ProofDependencyLogging.dfy diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy new file mode 100644 index 00000000000..1c88650c93b --- /dev/null +++ b/Test/logger/ProofDependencyLogging.dfy @@ -0,0 +1,424 @@ +// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK: Results for RedundantAssumeMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(177,11\)-\(177,15\): assume statement +// CHECK: ProofDependencyLogging.dfy\(178,11\)-\(178,11\): assertion always holds +// +// CHECK: Results for ContradictoryAssumeMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(183,11\)-\(183,15\): assume statement +// CHECK: ProofDependencyLogging.dfy\(184,11\)-\(184,15\): assume statement +// +// CHECK: Results for AssumeFalseMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(192,11\)-\(192,11\): assume statement +// +// CHECK: Results for ObviouslyContradictoryRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(198,11\)-\(198,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(199,11\)-\(199,15\): requires clause +// +// CHECK: Results for ObviouslyContradictoryRequiresMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(207,11\)-\(207,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(208,11\)-\(208,15\): requires clause +// +// CHECK: Results for ObviouslyRedundantRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(219,10\)-\(219,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(221,4\)-\(221,4\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(221,2\)-\(221,6\): function call result +// CHECK: ProofDependencyLogging.dfy\(216,0\)-\(222,0\): function definition for ObviouslyRedundantRequiresFunc +// CHECK: ProofDependencyLogging.dfy\(217,11\)-\(217,15\): requires clause +// +// CHECK: Results for ObviouslyRedundantRequiresMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(229,11\)-\(229,11\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(229,2\)-\(229,14\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(227,10\)-\(227,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(225,11\)-\(225,15\): requires clause +// +// CHECK: Results for ObviouslyUnnecessaryRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(237,31\)-\(237,31\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(237,20\)-\(237,20\): value always satisfies the subset constraints of 'nat' +// +// CHECK: Results for ObviouslyUnnecessaryRequiresMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(244,47\)-\(244,47\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(244,24\)-\(244,24\): value always satisfies the subset constraints of 'nat' +// +// CHECK: Results for ObviouslyUnconstrainedCodeFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(250,10\)-\(250,16\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(252,11\)-\(252,15\): let expression binding RHS well-formed +// CHECK: ProofDependencyLogging.dfy\(252,6\)-\(252,6\): let expression binding +// CHECK: ProofDependencyLogging.dfy\(254,2\)-\(254,2\): let expression result +// CHECK: ProofDependencyLogging.dfy\(248,0\)-\(256,0\): function definition for ObviouslyUnconstrainedCodeFunc +// CHECK: ProofDependencyLogging.dfy\(249,11\)-\(249,15\): requires clause +// +// CHECK: Results for ObviouslyUnconstrainedCodeMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(262,8\)-\(262,16\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(264,2\)-\(266,7\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(260,10\)-\(260,16\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(259,11\)-\(259,15\): requires clause +// +// CHECK: Results for PartiallyRedundantRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(272,10\)-\(272,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(274,4\)-\(274,4\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(274,2\)-\(274,6\): function call result +// CHECK: ProofDependencyLogging.dfy\(270,0\)-\(275,0\): function definition for PartiallyRedundantRequiresFunc +// CHECK: ProofDependencyLogging.dfy\(271,22\)-\(271,26\): requires clause +// +// CHECK: Results for PartiallyUnnecessaryRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(282,31\)-\(282,31\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(282,20\)-\(282,20\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(279,21\)-\(279,25\): requires clause +// +// CHECK: Results for MultiPartRedundantRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(292,10\)-\(292,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(294,2\)-\(294,2\): function call result +// CHECK: ProofDependencyLogging.dfy\(288,0\)-\(295,0\): function definition for MultiPartRedundantRequiresFunc +// CHECK: ProofDependencyLogging.dfy\(291,11\)-\(291,16\): requires clause +// +// CHECK: Results for MultiPartRedundantRequiresMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(301,10\)-\(301,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(300,11\)-\(300,16\): requires clause +// +// CHECK: Results for MultiPartContradictoryRequiresFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(313,10\)-\(313,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(315,2\)-\(315,2\): function call result +// CHECK: ProofDependencyLogging.dfy\(309,0\)-\(316,0\): function definition for MultiPartContradictoryRequiresFunc +// CHECK: ProofDependencyLogging.dfy\(310,11\)-\(310,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(311,11\)-\(311,15\): requires clause +// +// CHECK: Results for MultiPartContradictoryRequiresMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(322,10\)-\(322,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(319,11\)-\(319,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(320,11\)-\(320,15\): requires clause +// +// CHECK: Results for CallContradictoryFunctionFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(338,10\)-\(338,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(341,2\)-\(341,2\): function precondition satisfied +// CHECK: ProofDependencyLogging.dfy\(341,2\)-\(341,38\): function call result +// CHECK: ProofDependencyLogging.dfy\(336,0\)-\(342,0\): function definition for CallContradictoryFunctionFunc +// CHECK: ProofDependencyLogging.dfy\(337,11\)-\(337,15\): requires clause +// +// CHECK: Results for CallContradictoryMethodMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): requires clause at ProofDependencyLogging.dfy\(332,11\)-\(332,15\) from call +// CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): ensures clause at ProofDependencyLogging.dfy\(333,11\)-\(333,24\) from call +// CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): ensures clause at ProofDependencyLogging.dfy\(333,11\)-\(333,24\) from call +// CHECK: ProofDependencyLogging.dfy\(345,11\)-\(345,15\): requires clause +// +// CHECK: Results for FalseAntecedentRequiresClauseMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(357,2\)-\(357,14\): assignment \(or return\) +// +// CHECK: Results for FalseAntecedentAssertStatementMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(363,19\)-\(363,19\): assertion always holds +// CHECK: ProofDependencyLogging.dfy\(362,8\)-\(362,14\): assignment \(or return\) +// +// CHECK: Results for FalseAntecedentEnsuresClauseMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(370,2\)-\(370,12\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(368,10\)-\(368,24\): ensures clause +// +// CHECK: Results for ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(375,10\)-\(375,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(373,0\)-\(380,0\): function definition for ObviouslyUnreachableIfExpressionBranchFunc +// CHECK: ProofDependencyLogging.dfy\(379,7\)-\(379,11\): if expression else branch +// CHECK: ProofDependencyLogging.dfy\(374,11\)-\(374,15\): requires clause +// +// CHECK: Results for ObviouslyUnreachableIfStatementBranchMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(384,10\)-\(384,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(389,4\)-\(389,16\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(383,11\)-\(383,15\): requires clause +// +// CHECK: Results for ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\) +// +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(397,10\)-\(397,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(395,0\)-\(403,0\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction +// CHECK: ProofDependencyLogging.dfy\(401,14\)-\(401,14\): match expression branch result +// CHECK: ProofDependencyLogging.dfy\(396,11\)-\(396,16\): requires clause +// +// CHECK: Results for ObviouslyUnreachableMatchStatementCaseMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(407,10\)-\(407,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(411,14\)-\(411,22\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(406,11\)-\(406,16\): requires clause +// +// CHECK: Results for ObviouslyUnreachableReturnStatementMethod \(correctness\) +// CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(417,12\)-\(417,16\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(420,6\)-\(420,14\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(416,11\)-\(416,16\): requires clause + + + + +method RedundantAssumeMethod(n: int) +{ + // either one or the other assumption shouldn't be covered + assume n > 4; + assume n > 3; + assert n > 1; +} + +method ContradictoryAssumeMethod(n: int) +{ + assume n > 0; + assume n < 0; + assume n == 5; // shouldn't be covered + assert n < 10; // shouldn't be covered +} + +method AssumeFalseMethod(n: int) +{ + assume n == 15; // shouldn't be covered + assume false; + assert n < 10; // shouldn't be covered +} + +// Obvious contradiction in requires clauses. +function ObviouslyContradictoryRequiresFunc(x: nat): (r: nat) + requires x > 10 + requires x < 10 + ensures r < x // only provable vacuously +{ + assert x == 10; // contradicts both requires clauses + x - 1 // not necessarily a valid nat +} + +method ObviouslyContradictoryRequiresMethod(x: nat) returns (r: nat) + requires x > 10 + requires x < 10 + ensures r < x // only provable vacuously +{ + assert x == 10; // contradicts both requires clauses + return x - 1; // not necessarily a valid nat +} + +// Obvious redundancy in requires clauses. +function ObviouslyRedundantRequiresFunc(x: nat): (r: nat) + requires x < 10 + requires x < 100 // implied by previous requires clause + ensures r < 11 // should cause body and first requires clause to be covered +{ + x + 1 +} + +method ObviouslyRedundantRequiresMethod(x: nat) returns (r: nat) + requires x < 10 + requires x < 100 // implied by previous requires clause + ensures r < 11 // should cause body and first requires clause to be covered +{ + return x + 1; +} + +// Obviously unnecessary requires clauses. +function ObviouslyUnnecessaryRequiresFunc(x: nat): (r: nat) + requires x < 10 // not required for the proof +{ + // cause at least a little proof work to be necessary, for nat bounds + if (x > 5) then x + 2 else x + 1 +} + +method ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat) + requires x < 10 // not required for the proof +{ + // cause at least a little proof work to be necessary, for nat bounds + if (x > 5) { return x + 2; } else { return x + 1; } +} + +// Code obviously not constrained by ensures clause. +function ObviouslyUnconstrainedCodeFunc(x: int): (r: (int, int)) + requires x > 10 + ensures r.0 > 10 +{ + var a := x + 1; // constrained by ensures clause + var b := x - 1; // not constrained by ensures clause + (a, + b) +} + +method ObviouslyUnconstrainedCodeMethod(x: int) returns (r: (int, int)) + requires x > 10 + ensures r.0 > 10 +{ + var a := x + 1; // constrained by ensures clause + var b := x - 1; // not constrained by ensures clause + return + (a, + b); +} + +// Partial redundancy in requires clauses. +function PartiallyRedundantRequiresFunc(x: nat): (r: nat) + requires x < 100 && x < 10 // LHS implied by RHS + ensures r < 11 // should cause body and RHS clause to be covered +{ + x + 1 +} + +// Partly unnecessary requires clause. +function PartiallyUnnecessaryRequiresFunc(x: int): (r: nat) + requires x < 10 && x > 0 // RHS required for proof, but not LHS +{ + // cause at least a little proof work to be necessary, for nat bounds + if (x > 5) then x - 1 else x + 1 +} + + +// Redundancy of one requires clause due to at least two others, with at least +// one of the three being partly in a separately-defined function. +function MultiPartRedundantRequiresFunc(x: int): (r: int) + requires x > 10 + requires x < 12 + requires x == 11 // implied by the previous two, but neither individually + ensures r == 11 +{ + x +} + +method MultiPartRedundantRequiresMethod(x: int) returns (r: int) + requires x > 10 + requires x < 12 + requires x == 11 // implied by the previous two, but neither individually + ensures r == 11 +{ + return x; +} + +// Contradiction between three different requires clauses, with at least one of +// the three being partly in a separately-defined function (function and +// method). +function MultiPartContradictoryRequiresFunc(x: int, y: int): (r: int) + requires x > 10 + requires x < 12 + requires y != 11 // contradicts the previous two + ensures r == 11 // provable from first two preconditions, but shouldn't be covered +{ + x +} + +method MultiPartContradictoryRequiresMethod(x: int, y: int) returns (r: int) + requires x > 10 + requires x < 12 + requires y != 11 // contradicts the previous two + ensures r == 11 // provable from first two preconditions, but shouldn't be covered +{ + return x; +} + +function ContradictoryEnsuresClauseFunc(x: int): (r: int) + requires x > 1 + ensures r > x && r < 0 + +method ContradictoryEnsuresClauseMethod(x: int) returns (r: int) + requires x > 1 + ensures r > x && r < 0 + +// Call function that has contradictory ensures clauses. +function CallContradictoryFunctionFunc(x: int): (r: int) + requires x > 1 + ensures r < 0 +{ + // TODO: Dafny doesn't generate sufficient Boogie code to make the contradiction detectable + ContradictoryEnsuresClauseFunc(x) - 1 +} + +method CallContradictoryMethodMethod(x: int) returns (r: int) + requires x > 1 + ensures r < 0 +{ + var y := ContradictoryEnsuresClauseMethod(x); + return y - 1; +} + +// False antecedent requires clause +method FalseAntecedentRequiresClauseMethod(x: int) returns (r: int) + requires x*x < 0 ==> x == x + 1 + ensures r > x +{ + return x + 1; +} + +// False antecedent assert statement. +method FalseAntecedentAssertStatementMethod(x: int) { + var y := x*x; + assert y < 0 ==> x < 0; +} + +// False antecedent ensures clause. +method FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int) + ensures r < 0 ==> x < 0 +{ + return x*x; +} + +function ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int) + requires x > 0 + ensures r > 0 +{ + if x < 0 + then x - 1 // unreachable + else x + 1 +} + +method ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int) + requires x > 0 + ensures r > 0 +{ + if x < 0 { + return x - 1; // unreachable + } else { + return x + 1; + } +} + +datatype T = A | B + +function ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r:int) + requires t != A + ensures r > 1 // alt: r > 0 +{ + match t { + case A => 1 // unreachable + case B => 2 + } +} + +method ObviouslyUnreachableMatchStatementCaseMethod(t: T) returns (r:int) + requires t != A + ensures r > 1 // alt: r > 0 +{ + match t { + case A => return 1; // unreachable + case B => return 2; + } +} + +method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int) + requires t != A + ensures r > 1 // alt: r > 0 + { + if !t.A? { + return 2; + } + + return 1; // unreachable + } From d40f73a766a81a909f62b62c539a76fc45a8e99f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 25 Aug 2023 16:42:58 -0700 Subject: [PATCH 11/44] Adjust test output to account for changes --- .../snapshots/Snapshots0.run.dfy.expect | 4 +-- .../snapshots/Snapshots1.run.dfy.expect | 4 +-- .../snapshots/Snapshots2.run.dfy.expect | 20 ++++++------- .../snapshots/Snapshots3.run.dfy.expect | 6 ++-- .../snapshots/Snapshots4.run.dfy.expect | 8 ++--- .../snapshots/Snapshots5.run.dfy.expect | 14 ++++----- .../snapshots/Snapshots8.run.dfy.expect | 30 +++++++++---------- .../snapshots/Snapshots9.run.dfy.expect | 8 ++--- Test/git-issues/git-issue-2384.dfy.expect | 2 +- Test/git-issues/git-issue-2477.dfy.expect | 2 +- Test/git-issues/git-issue-2511.dfy.expect | 2 +- .../NonReferenceTraitsVerify.dfy.expect | 6 ++-- Test/traits/TraitOverride1.dfy.expect | 2 +- Test/traits/TraitsDecreases.dfy.expect | 22 +++++++------- 14 files changed, 65 insertions(+), 65 deletions(-) diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect index 69ea8b73caa..89bdd3ae0be 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -1,4 +1,4 @@ -Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v0.dfy(4,10)) assert {:id "id1"} Lit(false); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors @@ -7,7 +7,7 @@ Processing call to procedure bar (call) in implementation foo (correctness) (at >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id5"} Lit(false); >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion might not hold diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect index 7d909cf4ee4..a2ef2d3d341 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -1,10 +1,10 @@ -Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id1"} Lit(false); >>> DoNothingToAssert 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 Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id6"} Lit(false); >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion might not hold diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect index 1cc0741d3d5..7a88f9ecd56 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -1,12 +1,12 @@ -Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id1"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert true; +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} {:id "id5"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id4"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert true; +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} {:id "id9"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -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 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 true; +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id19"} {:id "id18"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert _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 true; +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} {:id "id22"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id21"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect index c7eb2ba7634..392746d306b 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -1,11 +1,11 @@ -Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v0.dfy(9,14)) assert {:id "id0"} Lit(0 != 0); >>> DoNothingToAssert Snapshots3.v0.dfy(9,13): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error -Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); +Processing command (at Snapshots3.v1.dfy(5,12)) assert {:id "id1"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v1.dfy(9,14)) assert {:id "id2"} Lit(0 != 0); >>> RecycleError Snapshots3.v0.dfy(9,13): Error: assertion might not hold diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect index 148109605a5..f5c1207363a 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -1,12 +1,12 @@ -Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0); +Processing command (at Snapshots4.v0.dfy(9,14)) assert {:id "id0"} LitInt(0) == LitInt(0); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors -Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1); +Processing command (at Snapshots4.v1.dfy(5,14)) assert {:id "id1"} Lit(1 != 1); >>> DoNothingToAssert -Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); +Processing command (at Snapshots4.v1.dfy(9,14)) assert {:id "id2"} LitInt(0) == LitInt(0); >>> MarkAsFullyVerified -Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2); +Processing command (at Snapshots4.v1.dfy(10,14)) assert {:id "id3"} Lit(2 != 2); >>> DoNothingToAssert Snapshots4.v1.dfy(5,13): Error: assertion might not hold Snapshots4.v1.dfy(10,13): Error: assertion might not hold diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect index f4a197e224d..2649fdc7257 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -2,11 +2,11 @@ Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on. Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on. Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on. Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on. -Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id1"} (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id3"} (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#3_1: bool :: true ==> b#3_1 || !b#3_1) || 1 != 1; +Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id4"} (forall b#3_1: bool :: true ==> b#3_1 || !b#3_1) || 1 != 1; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors @@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on. Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on. Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on. Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on. -Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id10"} (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id12"} (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(20,37)) assert (exists b#3_1: bool :: Lit(true)) || 4 != 4; +Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id13"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; >>> DoNothingToAssert -Processing command (at Snapshots5.v1.dfy(22,35)) assert (exists b#3: bool :: Lit(true)) || 5 != 5; +Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id14"} (exists b#3: bool :: Lit(true)) || 5 != 5; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect index dfa56ad8a67..9b66e66cf2c 100644 --- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect @@ -1,41 +1,41 @@ -Processing command (at Snapshots8.v0.dfy(2,37)) assert x#0 < 20 || LitInt(10) <= x#0; +Processing command (at Snapshots8.v0.dfy(2,37)) assert {:id "id0"} x#0 < 20 || LitInt(10) <= x#0; >>> DoNothingToAssert -Processing command (at Snapshots8.v0.dfy(3,12)) assert x#0 < 10; +Processing command (at Snapshots8.v0.dfy(3,12)) assert {:id "id1"} x#0 < 10; >>> DoNothingToAssert -Processing command (at Snapshots8.v0.dfy(4,8)) assert LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id4$id2$requires"} {:id "id2"} LitInt(0) <= call0formal#AT#y#0; >>> DoNothingToAssert Snapshots8.v0.dfy(3,11): Error: assertion might not hold Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved -Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved -Processing command (at Snapshots8.v0.dfy(13,13)) assert LitInt(2) <= z#0; +Snapshots8.v0.dfy(8,13): Related location: precondition could not be proved +Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id8"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53; +Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id10"} u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion might not hold -Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id11"} Lit(true); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 4 errors -Processing command (at Snapshots8.v1.dfy(30,17)) assert u#0 != 53; +Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id24"} u#0 != 53; >>> RecycleError Snapshots8.v1.dfy(30,16): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(3,15)) assert x#0 < 20 || LitInt(10) <= x#0; +Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id12"} x#0 < 20 || LitInt(10) <= x#0; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(5,17)) assert x#0 < 10; +Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id13"} x#0 < 10; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(6,8)) assert LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id17$id14$requires"} {:id "id14"} LitInt(0) <= call0formal#AT#y#0; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(7,12)) assert x#0 == LitInt(7); +Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id15"} x#0 == LitInt(7); >>> DoNothingToAssert Snapshots8.v1.dfy(5,16): Error: assertion might not hold Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved -Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved +Snapshots8.v1.dfy(12,20): Related location: precondition could not be proved Snapshots8.v1.dfy(7,11): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id23"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0; +Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id21"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved diff --git a/Test/dafny0/snapshots/Snapshots9.run.dfy.expect b/Test/dafny0/snapshots/Snapshots9.run.dfy.expect index 579a79fadc7..0657e360d51 100644 --- a/Test/dafny0/snapshots/Snapshots9.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots9.run.dfy.expect @@ -1,18 +1,18 @@ -Processing command (at Snapshots9.v0.dfy(2,11)) assert ok#0; +Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(2,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v0.dfy(12,11)) assert ok#0; +Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id7"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(13,0): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(12,10): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 2 errors -Processing command (at Snapshots9.v1.dfy(6,11)) assert ok#0; +Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id10"} ok#0; >>> RecycleError Snapshots9.v1.dfy(8,7): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(6,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v1.dfy(19,11)) assert ok#0; +Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id15"} ok#0; >>> RecycleError Snapshots9.v1.dfy(21,0): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(19,10): Related location: this is the postcondition that could not be proved diff --git a/Test/git-issues/git-issue-2384.dfy.expect b/Test/git-issues/git-issue-2384.dfy.expect index 9556d63ff12..88c0c7f25c2 100644 --- a/Test/git-issues/git-issue-2384.dfy.expect +++ b/Test/git-issues/git-issue-2384.dfy.expect @@ -1,4 +1,4 @@ -git-issue-2384.dfy(11,9): Error: method might modify an object not in the parent trait context's modifies clause +git-issue-2384.dfy(11,2): Error: method might modify an object not in the parent trait context's modifies clause git-issue-2384.dfy(14,18): Error: predicate might read an object not in the parent trait context's reads clause git-issue-2384.dfy(17,17): Error: function might read an object not in the parent trait context's reads clause diff --git a/Test/git-issues/git-issue-2477.dfy.expect b/Test/git-issues/git-issue-2477.dfy.expect index 0c6ee63284e..86a4eb7b1d7 100644 --- a/Test/git-issues/git-issue-2477.dfy.expect +++ b/Test/git-issues/git-issue-2477.dfy.expect @@ -1,3 +1,3 @@ -git-issue-2477.dfy(10,12): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +git-issue-2477.dfy(10,2): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait Dafny program verifier finished with 0 verified, 1 error diff --git a/Test/git-issues/git-issue-2511.dfy.expect b/Test/git-issues/git-issue-2511.dfy.expect index faf50333a0b..7ccf579b37e 100644 --- a/Test/git-issues/git-issue-2511.dfy.expect +++ b/Test/git-issues/git-issue-2511.dfy.expect @@ -1,5 +1,5 @@ git-issue-2511.dfy(14,11): Error: assertion might not hold git-issue-2511.dfy(24,12): Error: decreases clause might not decrease -git-issue-2511.dfy(51,11): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +git-issue-2511.dfy(51,4): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait Dafny program verifier finished with 3 verified, 3 errors diff --git a/Test/traits/NonReferenceTraitsVerify.dfy.expect b/Test/traits/NonReferenceTraitsVerify.dfy.expect index a5d7dab583a..8391abdb033 100644 --- a/Test/traits/NonReferenceTraitsVerify.dfy.expect +++ b/Test/traits/NonReferenceTraitsVerify.dfy.expect @@ -3,18 +3,18 @@ NonReferenceTraitsVerify.dfy(35,22): Related location: this is the postcondition NonReferenceTraitsVerify.dfy(43,4): Error: a postcondition could not be proved on this return path NonReferenceTraitsVerify.dfy(42,16): Related location: this is the postcondition that could not be proved NonReferenceTraitsVerify.dfy(49,13): Error: the function must provide an equal or more permissive precondition than in its parent trait -NonReferenceTraitsVerify.dfy(56,11): Error: the method must provide an equal or more detailed postcondition than in its parent trait +NonReferenceTraitsVerify.dfy(56,4): Error: the method must provide an equal or more detailed postcondition than in its parent trait NonReferenceTraitsVerify.dfy(103,13): Error: a postcondition could not be proved on this return path NonReferenceTraitsVerify.dfy(105,22): Related location: this is the postcondition that could not be proved NonReferenceTraitsVerify.dfy(113,4): Error: a postcondition could not be proved on this return path NonReferenceTraitsVerify.dfy(112,16): Related location: this is the postcondition that could not be proved NonReferenceTraitsVerify.dfy(119,13): Error: the function must provide an equal or more permissive precondition than in its parent trait -NonReferenceTraitsVerify.dfy(126,11): Error: the method must provide an equal or more detailed postcondition than in its parent trait +NonReferenceTraitsVerify.dfy(126,4): Error: the method must provide an equal or more detailed postcondition than in its parent trait NonReferenceTraitsVerify.dfy(173,13): Error: a postcondition could not be proved on this return path NonReferenceTraitsVerify.dfy(175,22): Related location: this is the postcondition that could not be proved NonReferenceTraitsVerify.dfy(183,4): Error: a postcondition could not be proved on this return path NonReferenceTraitsVerify.dfy(182,16): Related location: this is the postcondition that could not be proved NonReferenceTraitsVerify.dfy(189,13): Error: the function must provide an equal or more permissive precondition than in its parent trait -NonReferenceTraitsVerify.dfy(196,11): Error: the method must provide an equal or more detailed postcondition than in its parent trait +NonReferenceTraitsVerify.dfy(196,4): Error: the method must provide an equal or more detailed postcondition than in its parent trait Dafny program verifier finished with 42 verified, 12 errors diff --git a/Test/traits/TraitOverride1.dfy.expect b/Test/traits/TraitOverride1.dfy.expect index e28b26fe37f..0782b519ac2 100644 --- a/Test/traits/TraitOverride1.dfy.expect +++ b/Test/traits/TraitOverride1.dfy.expect @@ -1,4 +1,4 @@ -TraitOverride1.dfy(200,9): Error: the method must provide an equal or more detailed postcondition than in its parent trait +TraitOverride1.dfy(200,2): Error: the method must provide an equal or more detailed postcondition than in its parent trait TraitOverride1.dfy(205,2): Error: a postcondition could not be proved on this return path TraitOverride1.dfy(204,40): Related location: this is the postcondition that could not be proved TraitOverride1.dfy(188,32): Related location diff --git a/Test/traits/TraitsDecreases.dfy.expect b/Test/traits/TraitsDecreases.dfy.expect index 7aab08c866a..a823aad9da1 100644 --- a/Test/traits/TraitsDecreases.dfy.expect +++ b/Test/traits/TraitsDecreases.dfy.expect @@ -1,13 +1,13 @@ -TraitsDecreases.dfy(117,20): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(124,20): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(131,20): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(138,20): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(145,20): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(152,11): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(57,9): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(69,9): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(72,9): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(78,9): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait -TraitsDecreases.dfy(88,9): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(117,4): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(124,4): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(131,4): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(138,4): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(145,4): Error: predicate's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(152,4): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(57,2): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(69,2): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(72,2): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(78,2): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait +TraitsDecreases.dfy(88,2): Error: method's (possibly automatically generated) decreases clause must be below or equal to that in the trait Dafny program verifier finished with 12 verified, 11 errors From 595bdedbd62e96f8620e545003e1585d713009c3 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 28 Aug 2023 15:32:22 -0700 Subject: [PATCH 12/44] Silence warning --- Source/DafnyCore/Verifier/Translator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index bf658e1b521..8693dd23460 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -164,7 +164,7 @@ public ProofDependency GetFullIdDependency(string idString) { } } - private ProofDependencyManager? proofDependencies; + private ProofDependencyManager proofDependencies; // optimizing translation readonly ISet referencedMembers = new HashSet(); From 2804ef9a5e169ad3208cea05f92718703bcad1da Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 28 Aug 2023 15:32:36 -0700 Subject: [PATCH 13/44] Remove obsolete statement --- Source/DafnyCore/Verifier/Translator.cs | 1 - 1 file changed, 1 deletion(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 8693dd23460..479297159cb 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -9034,7 +9034,6 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs } else { // box from RHS type to tmp-var type, then do the assignment; then return LHS, boxed from tmp-var type to result type var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, CondApplyBox(tok, bRhs, e.Expr.Type, rhsTypeConstraint)); - var rhsTok = (Microsoft.Dafny.IToken)bRhs.tok; proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); builder.Add(cmd); return CondApplyBox(tok, bLhs, rhsTypeConstraint, lhsType); From 698b06765f7ad4a39365ec981025aea0c1ae2250 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 28 Aug 2023 16:52:49 -0700 Subject: [PATCH 14/44] Sort proof dependencies in text logger This helps ensure deterministic testing. --- Source/DafnyDriver/TextLogger.cs | 8 ++- Test/logger/ProofDependencyLogging.dfy | 70 +++++++++++++------------- 2 files changed, 41 insertions(+), 37 deletions(-) diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index 6d4975286c4..a7257c80f55 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -51,8 +51,12 @@ public void LogResults(List<(Implementation, VerificationResult)> verificationRe if (vcResult.coveredElements.Any()) { tw.WriteLine(""); tw.WriteLine(" Proof dependencies:"); - foreach (var depId in vcResult.coveredElements) { - var dep = depManager.GetFullIdDependency(depId); + var fullDependencies = + vcResult + .coveredElements + .Select(depManager.GetFullIdDependency) + .OrderBy(dep => (dep.RangeString(), dep.Description)); + foreach (var dep in fullDependencies) { tw.WriteLine($" {dep.RangeString()}: {dep.Description}"); } } diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy index 1c88650c93b..b8864d823ef 100644 --- a/Test/logger/ProofDependencyLogging.dfy +++ b/Test/logger/ProofDependencyLogging.dfy @@ -26,99 +26,99 @@ // // CHECK: Results for ObviouslyRedundantRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(219,10\)-\(219,14\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(221,4\)-\(221,4\): value always satisfies the subset constraints of 'nat' -// CHECK: ProofDependencyLogging.dfy\(221,2\)-\(221,6\): function call result // CHECK: ProofDependencyLogging.dfy\(216,0\)-\(222,0\): function definition for ObviouslyRedundantRequiresFunc // CHECK: ProofDependencyLogging.dfy\(217,11\)-\(217,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(219,10\)-\(219,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(221,2\)-\(221,6\): function call result +// CHECK: ProofDependencyLogging.dfy\(221,4\)-\(221,4\): value always satisfies the subset constraints of 'nat' // // CHECK: Results for ObviouslyRedundantRequiresMethod \(correctness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(225,11\)-\(225,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(227,10\)-\(227,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(229,11\)-\(229,11\): value always satisfies the subset constraints of 'nat' // CHECK: ProofDependencyLogging.dfy\(229,2\)-\(229,14\): assignment \(or return\) -// CHECK: ProofDependencyLogging.dfy\(227,10\)-\(227,14\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(225,11\)-\(225,15\): requires clause // // CHECK: Results for ObviouslyUnnecessaryRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(237,31\)-\(237,31\): value always satisfies the subset constraints of 'nat' // CHECK: ProofDependencyLogging.dfy\(237,20\)-\(237,20\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(237,31\)-\(237,31\): value always satisfies the subset constraints of 'nat' // // CHECK: Results for ObviouslyUnnecessaryRequiresMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(244,47\)-\(244,47\): value always satisfies the subset constraints of 'nat' // CHECK: ProofDependencyLogging.dfy\(244,24\)-\(244,24\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(244,47\)-\(244,47\): value always satisfies the subset constraints of 'nat' // // CHECK: Results for ObviouslyUnconstrainedCodeFunc \(well-formedness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(248,0\)-\(256,0\): function definition for ObviouslyUnconstrainedCodeFunc +// CHECK: ProofDependencyLogging.dfy\(249,11\)-\(249,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(250,10\)-\(250,16\): ensures clause // CHECK: ProofDependencyLogging.dfy\(252,11\)-\(252,15\): let expression binding RHS well-formed // CHECK: ProofDependencyLogging.dfy\(252,6\)-\(252,6\): let expression binding // CHECK: ProofDependencyLogging.dfy\(254,2\)-\(254,2\): let expression result -// CHECK: ProofDependencyLogging.dfy\(248,0\)-\(256,0\): function definition for ObviouslyUnconstrainedCodeFunc -// CHECK: ProofDependencyLogging.dfy\(249,11\)-\(249,15\): requires clause // // CHECK: Results for ObviouslyUnconstrainedCodeMethod \(correctness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(259,11\)-\(259,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(260,10\)-\(260,16\): ensures clause // CHECK: ProofDependencyLogging.dfy\(262,8\)-\(262,16\): assignment \(or return\) // CHECK: ProofDependencyLogging.dfy\(264,2\)-\(266,7\): assignment \(or return\) -// CHECK: ProofDependencyLogging.dfy\(260,10\)-\(260,16\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(259,11\)-\(259,15\): requires clause // // CHECK: Results for PartiallyRedundantRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(272,10\)-\(272,14\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(274,4\)-\(274,4\): value always satisfies the subset constraints of 'nat' -// CHECK: ProofDependencyLogging.dfy\(274,2\)-\(274,6\): function call result // CHECK: ProofDependencyLogging.dfy\(270,0\)-\(275,0\): function definition for PartiallyRedundantRequiresFunc // CHECK: ProofDependencyLogging.dfy\(271,22\)-\(271,26\): requires clause +// CHECK: ProofDependencyLogging.dfy\(272,10\)-\(272,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(274,2\)-\(274,6\): function call result +// CHECK: ProofDependencyLogging.dfy\(274,4\)-\(274,4\): value always satisfies the subset constraints of 'nat' // // CHECK: Results for PartiallyUnnecessaryRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(282,31\)-\(282,31\): value always satisfies the subset constraints of 'nat' -// CHECK: ProofDependencyLogging.dfy\(282,20\)-\(282,20\): value always satisfies the subset constraints of 'nat' // CHECK: ProofDependencyLogging.dfy\(279,21\)-\(279,25\): requires clause +// CHECK: ProofDependencyLogging.dfy\(282,20\)-\(282,20\): value always satisfies the subset constraints of 'nat' +// CHECK: ProofDependencyLogging.dfy\(282,31\)-\(282,31\): value always satisfies the subset constraints of 'nat' // // CHECK: Results for MultiPartRedundantRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(292,10\)-\(292,15\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(294,2\)-\(294,2\): function call result // CHECK: ProofDependencyLogging.dfy\(288,0\)-\(295,0\): function definition for MultiPartRedundantRequiresFunc // CHECK: ProofDependencyLogging.dfy\(291,11\)-\(291,16\): requires clause +// CHECK: ProofDependencyLogging.dfy\(292,10\)-\(292,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(294,2\)-\(294,2\): function call result // // CHECK: Results for MultiPartRedundantRequiresMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(301,10\)-\(301,15\): ensures clause // CHECK: ProofDependencyLogging.dfy\(300,11\)-\(300,16\): requires clause +// CHECK: ProofDependencyLogging.dfy\(301,10\)-\(301,15\): ensures clause // // CHECK: Results for MultiPartContradictoryRequiresFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(313,10\)-\(313,15\): ensures clause -// CHECK: ProofDependencyLogging.dfy\(315,2\)-\(315,2\): function call result // CHECK: ProofDependencyLogging.dfy\(309,0\)-\(316,0\): function definition for MultiPartContradictoryRequiresFunc // CHECK: ProofDependencyLogging.dfy\(310,11\)-\(310,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(311,11\)-\(311,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(313,10\)-\(313,15\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(315,2\)-\(315,2\): function call result // // CHECK: Results for MultiPartContradictoryRequiresMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(322,10\)-\(322,15\): ensures clause // CHECK: ProofDependencyLogging.dfy\(319,11\)-\(319,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(320,11\)-\(320,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(322,10\)-\(322,15\): ensures clause // // CHECK: Results for CallContradictoryFunctionFunc \(well-formedness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(336,0\)-\(342,0\): function definition for CallContradictoryFunctionFunc +// CHECK: ProofDependencyLogging.dfy\(337,11\)-\(337,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(338,10\)-\(338,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(341,2\)-\(341,2\): function precondition satisfied // CHECK: ProofDependencyLogging.dfy\(341,2\)-\(341,38\): function call result -// CHECK: ProofDependencyLogging.dfy\(336,0\)-\(342,0\): function definition for CallContradictoryFunctionFunc -// CHECK: ProofDependencyLogging.dfy\(337,11\)-\(337,15\): requires clause // // CHECK: Results for CallContradictoryMethodMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): requires clause at ProofDependencyLogging.dfy\(332,11\)-\(332,15\) from call +// CHECK: ProofDependencyLogging.dfy\(345,11\)-\(345,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): ensures clause at ProofDependencyLogging.dfy\(333,11\)-\(333,24\) from call // CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): ensures clause at ProofDependencyLogging.dfy\(333,11\)-\(333,24\) from call -// CHECK: ProofDependencyLogging.dfy\(345,11\)-\(345,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(348,8\)-\(348,46\): requires clause at ProofDependencyLogging.dfy\(332,11\)-\(332,15\) from call // // CHECK: Results for FalseAntecedentRequiresClauseMethod \(correctness\) // CHECK: Proof dependencies: @@ -126,46 +126,46 @@ // // CHECK: Results for FalseAntecedentAssertStatementMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(363,19\)-\(363,19\): assertion always holds // CHECK: ProofDependencyLogging.dfy\(362,8\)-\(362,14\): assignment \(or return\) +// CHECK: ProofDependencyLogging.dfy\(363,19\)-\(363,19\): assertion always holds // // CHECK: Results for FalseAntecedentEnsuresClauseMethod \(correctness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(370,2\)-\(370,12\): assignment \(or return\) // CHECK: ProofDependencyLogging.dfy\(368,10\)-\(368,24\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(370,2\)-\(370,12\): assignment \(or return\) // // CHECK: Results for ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\) // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(375,10\)-\(375,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(373,0\)-\(380,0\): function definition for ObviouslyUnreachableIfExpressionBranchFunc -// CHECK: ProofDependencyLogging.dfy\(379,7\)-\(379,11\): if expression else branch // CHECK: ProofDependencyLogging.dfy\(374,11\)-\(374,15\): requires clause +// CHECK: ProofDependencyLogging.dfy\(375,10\)-\(375,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(379,7\)-\(379,11\): if expression else branch // // CHECK: Results for ObviouslyUnreachableIfStatementBranchMethod \(correctness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(383,11\)-\(383,15\): requires clause // CHECK: ProofDependencyLogging.dfy\(384,10\)-\(384,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(389,4\)-\(389,16\): assignment \(or return\) -// CHECK: ProofDependencyLogging.dfy\(383,11\)-\(383,15\): requires clause // // CHECK: Results for ObviouslyUnreachableMatchExpressionCaseFunction \(well-formedness\) // // CHECK: Proof dependencies: -// CHECK: ProofDependencyLogging.dfy\(397,10\)-\(397,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(395,0\)-\(403,0\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction -// CHECK: ProofDependencyLogging.dfy\(401,14\)-\(401,14\): match expression branch result // CHECK: ProofDependencyLogging.dfy\(396,11\)-\(396,16\): requires clause +// CHECK: ProofDependencyLogging.dfy\(397,10\)-\(397,14\): ensures clause +// CHECK: ProofDependencyLogging.dfy\(401,14\)-\(401,14\): match expression branch result // // CHECK: Results for ObviouslyUnreachableMatchStatementCaseMethod \(correctness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(406,11\)-\(406,16\): requires clause // CHECK: ProofDependencyLogging.dfy\(407,10\)-\(407,14\): ensures clause // CHECK: ProofDependencyLogging.dfy\(411,14\)-\(411,22\): assignment \(or return\) -// CHECK: ProofDependencyLogging.dfy\(406,11\)-\(406,16\): requires clause // // CHECK: Results for ObviouslyUnreachableReturnStatementMethod \(correctness\) // CHECK: Proof dependencies: +// CHECK: ProofDependencyLogging.dfy\(416,11\)-\(416,16\): requires clause // CHECK: ProofDependencyLogging.dfy\(417,12\)-\(417,16\): ensures clause // CHECK: ProofDependencyLogging.dfy\(420,6\)-\(420,14\): assignment \(or return\) -// CHECK: ProofDependencyLogging.dfy\(416,11\)-\(416,16\): requires clause From 6803cad1bb334c8a43376c979a49c3129bcc55c2 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 28 Aug 2023 17:35:50 -0700 Subject: [PATCH 15/44] Fix some expected test outputs --- .../DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs | 2 +- Test/dafny0/Twostate-Functions.dfy.expect | 2 +- Test/dafny0/snapshots/Snapshots8.run.dfy.expect | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 05a3f536cf4..36ab1f6d369 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -145,7 +145,7 @@ await AssertHoverMatches(documentItem, (6, 6), Did prove: `i % 2 == 0`" ); await AssertHoverMatches(documentItem, (6, 6), - @"**Success:**???the precondition always holds + @"**Success:**???the precondition always holds Did prove: `i > 0`" ); await AssertHoverMatches(documentItem, (7, 6), diff --git a/Test/dafny0/Twostate-Functions.dfy.expect b/Test/dafny0/Twostate-Functions.dfy.expect index 9192165731f..a0e7a98f9b5 100644 --- a/Test/dafny0/Twostate-Functions.dfy.expect +++ b/Test/dafny0/Twostate-Functions.dfy.expect @@ -14,4 +14,4 @@ Twostate-Functions.dfy(167,13): Error: function precondition could not be proved Twostate-Functions.dfy(183,15): Error: argument ('d') might not be allocated in the two-state function's previous state Twostate-Functions.dfy(186,13): Error: function precondition could not be proved -Dafny program verifier finished with 23 verified, 13 errors +Dafny program verifier finished with 25 verified, 13 errors diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect index 9b66e66cf2c..20638ec1209 100644 --- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect @@ -6,7 +6,7 @@ Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id4$id2$requires"} { >>> DoNothingToAssert Snapshots8.v0.dfy(3,11): Error: assertion might not hold Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved -Snapshots8.v0.dfy(8,13): Related location: precondition could not be proved +Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id8"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path @@ -31,7 +31,7 @@ Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id15"} x#0 == LitIn >>> DoNothingToAssert Snapshots8.v1.dfy(5,16): Error: assertion might not hold Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved -Snapshots8.v1.dfy(12,20): Related location: precondition could not be proved +Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved Snapshots8.v1.dfy(7,11): Error: assertion might not hold Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id23"} Lit(true); >>> DoNothingToAssert From 80d174a6baff79ab748af9f3febeeef7486bea1a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 09:03:13 -0700 Subject: [PATCH 16/44] Move ProofDependencyManager to its own file --- Source/DafnyCore/AST/Program.cs | 2 +- .../Verifier/ProofDependencyManager.cs | 98 +++++++++++++++++++ Source/DafnyCore/Verifier/Translator.cs | 47 --------- Source/DafnyDriver/DafnyDriver.cs | 4 +- Source/DafnyDriver/TextLogger.cs | 4 +- .../DafnyDriver/VerificationResultLogger.cs | 2 +- 6 files changed, 104 insertions(+), 53 deletions(-) create mode 100644 Source/DafnyCore/Verifier/ProofDependencyManager.cs diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 952bf6de783..623a449158e 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -30,7 +30,7 @@ void ObjectInvariant() { public SystemModuleManager SystemModuleManager; public DafnyOptions Options => Reporter.Options; public ErrorReporter Reporter { get; set; } - public Translator.ProofDependencyManager ProofDependencyManager { get; set; } + public ProofDependencyManager ProofDependencyManager { get; set; } public Program(string name, [Captured] LiteralModuleDecl module, [Captured] SystemModuleManager systemModuleManager, ErrorReporter reporter, CompilationData compilation) { diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs new file mode 100644 index 00000000000..aa9ef0d6c52 --- /dev/null +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -0,0 +1,98 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +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 UInt64 proofDependencyIdCount = 0; + + public string GetProofDependencyId(ProofDependency dep) { + var idString = $"id{proofDependencyIdCount}"; + ProofDependenciesById[idString] = dep; + proofDependencyIdCount++; + return idString; + } + + // The "id" attribute on a Boogie AST node is used by Boogie to label + // that AST node in the SMT-Lib formula when constructing a verification + // condition. + private const string idAttributeName = "id"; + + public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, ProofDependency dep) { + var idString = GetProofDependencyId(dep); + boogieNode.Attributes = + new QKeyValue(tok, idAttributeName, new List() { idString }, boogieNode.Attributes); + } + + // This suffix indicates that an ID string represents the assumption of + // a specific ensures clause after a specific call. + private const string ensuresSuffix = "$ensures"; + + // This suffix indicates that an ID string represents the goal of + // proving a specific requires clause before a specific call. + private const string requiresSuffix = "$requires"; + + // This suffix indicates that an ID string represents the assumption + // of a specific requires clause after a specific call. + private const string requiresAssumedSuffix = "$requires_assumed"; + + // This suffix indicates that an ID string represents the goal of + // proving that a specific loop invariant is established. + private const string establishedSuffix = "$established"; + + // This suffix indicates that an ID string represents the goal of + // proving that a specific loop invariant is maintained. + private const string maintainedSuffix = "$maintained"; + + // This suffix indicates that an ID string represents the asssumption + // of a specific loop invariant in the body of the loop. + private const string assumeInBodySuffix = "$assume_in_body"; + + // Get the full ProofDependency indicated by a compound ID string. These strings are + // returned by the SMT solver to indicate which sub-formulas it used in constructing + // a proof of a particular goal (more technically, the UNSAT core of the negation of + // the goal). Because SMT-Lib only accepts strings as labels, we need to embed some + // extra information in those strings to represent ways in which the original Boogie + // commands and expressions are transformed and duplicated during Boogie's VC + // generation process. + public ProofDependency GetFullIdDependency(string idString) { + var parts = idString.Split('$'); + if (idString.EndsWith(requiresSuffix) && parts.Length == 3) { + var reqId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); + } else if (idString.EndsWith(requiresAssumedSuffix) && parts.Length == 3) { + var reqId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); + } else if (idString.EndsWith(ensuresSuffix) && parts.Length == 3) { + var ensId = ProofDependenciesById[parts[0]]; + var callId = ProofDependenciesById[parts[1]]; + return new CallEnsuresDependency((CallDependency)callId, (EnsuresDependency)ensId); + } else if (idString.EndsWith(establishedSuffix) && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (idString.EndsWith(maintainedSuffix) && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (idString.EndsWith(assumeInBodySuffix) && parts.Length == 2) { + return ProofDependenciesById[parts[0]]; + } else if (parts.Length > 1) { + throw new ArgumentException($"Malformed dependency ID string: {idString}"); + } else { + return ProofDependenciesById[idString]; + } + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 2c8a2ed69ea..8a04b9be8aa 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -126,53 +126,6 @@ private void EstablishModuleScope(ModuleDefinition systemModule, ModuleDefinitio readonly Dictionary fieldConstants = new Dictionary(); readonly Dictionary tytagConstants = new Dictionary(); - public class ProofDependencyManager { - // proof dependency tracking state - public Dictionary ProofDependenciesById { get; } = new(); - private UInt64 proofDependencyIdCount = 0; - - public string GetProofDependencyId(ProofDependency dep) { - var idString = $"id{proofDependencyIdCount}"; - ProofDependenciesById[idString] = dep; - proofDependencyIdCount++; - return idString; - } - - public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, ProofDependency dep) { - var idString = GetProofDependencyId(dep); - boogieNode.Attributes = - new QKeyValue(tok, "id", new List() { idString }, boogieNode.Attributes); - } - - // Get the full ProofDependency indicated by a compound ID string. - public ProofDependency GetFullIdDependency(string idString) { - var parts = idString.Split('$'); - if (idString.EndsWith("$requires") && parts.Length == 3) { - var reqId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; - return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); - } else if (idString.EndsWith("$requires_assumed") && parts.Length == 3) { - var reqId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; - return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); - } else if (idString.EndsWith("$ensures") && parts.Length == 3) { - var ensId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; - return new CallEnsuresDependency((CallDependency)callId, (EnsuresDependency)ensId); - } else if (idString.EndsWith("$established") && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (idString.EndsWith("$maintained") && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (idString.EndsWith("$assume_in_body") && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (parts.Length > 1) { - throw new ArgumentException($"Malformed dependency ID string: {idString}"); - } else { - return ProofDependenciesById[idString]; - } - } - } - private ProofDependencyManager proofDependencies; // optimizing translation diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index ac7778a0f7c..1c2903c424e 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -127,7 +127,7 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T var cliArgumentsResult = ProcessCommandLineArguments(outputWriter, errorWriter, inputReader, args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); ExitValue exitValue; - Translator.ProofDependencyManager depManager = new(); + ProofDependencyManager depManager = new(); switch (cliArgumentsResult) { case CommandLineArgumentsResult.OK: @@ -385,7 +385,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter private async Task ProcessFilesAsync(IReadOnlyList/*!*/ dafnyFiles, ReadOnlyCollection otherFileNames, - DafnyOptions options, Translator.ProofDependencyManager depManager, + DafnyOptions options, ProofDependencyManager depManager, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(dafnyFiles)); var dafnyFileNames = DafnyFile.FileNames(dafnyFiles); diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index a7257c80f55..637a5b4e624 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -9,9 +9,9 @@ namespace Microsoft.Dafny; public class TextLogger { private TextWriter tw; private TextWriter outWriter; - private Translator.ProofDependencyManager depManager; + private ProofDependencyManager depManager; - public TextLogger(Translator.ProofDependencyManager depManager, TextWriter outWriter) { + public TextLogger(ProofDependencyManager depManager, TextWriter outWriter) { this.depManager = depManager; this.outWriter = outWriter; } diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index 2be6f6b509d..434d9423aa6 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -27,7 +27,7 @@ public static class VerificationResultLogger { public static TestProperty ResourceCountProperty = TestProperty.Register("TestResult.ResourceCount", "TestResult.ResourceCount", typeof(int), typeof(TestResult)); - public static void RaiseTestLoggerEvents(DafnyOptions options, Translator.ProofDependencyManager depManager) { + public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyManager depManager) { var loggerConfigs = options.VerificationLoggerConfigs; // Provide just enough configuration for the loggers to work var parameters = new Dictionary { From 5c6deff1688b01a8b2518f784062c9a37e1e01fd Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 09:36:14 -0700 Subject: [PATCH 17/44] Clean up ProofDependency --- Source/DafnyCore/Verifier/ProofDependency.cs | 83 +++++++++++++------- 1 file changed, 55 insertions(+), 28 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index f014ab85ea1..f61aa7bc1e8 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -1,45 +1,59 @@ -using JetBrains.Annotations; +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- using Microsoft.Dafny; using IToken = Microsoft.Dafny.IToken; using PODesc = Microsoft.Dafny.ProofObligationDescription; -using ResolutionContext = Microsoft.Boogie.ResolutionContext; namespace DafnyCore.Verifier; +// A proof dependency represents a particular part of a Dafny program +// that may be used in the process of proving its correctness. When +// Boogie proves a particular verification condition, it returns a +// list of strings, returned by the SMT solver, indicating which +// program elements were used in completing the proof. After this, the +// ProofDependencyManager can map each string to a more structured +// ProofDependency. public abstract class ProofDependency { public abstract string Description { get; } - public abstract RangeToken RangeToken { get; } + public abstract RangeToken Range { get; } public string LocationString() { - if (RangeToken?.StartToken is null) { + if (Range?.StartToken is null) { return ""; } - var fn = RangeToken.StartToken.filename; - var sl = RangeToken.StartToken.line; - var sc = RangeToken.StartToken.col - 1; + var fn = Range.StartToken.filename; + var sl = Range.StartToken.line; + var sc = Range.StartToken.col - 1; return $"{fn}({sl},{sc})"; } public string RangeString() { - if (RangeToken?.StartToken is null) { + if (Range?.StartToken is null) { return ""; } - var fn = RangeToken.StartToken.filename; - var sl = RangeToken.StartToken.line; - var sc = RangeToken.StartToken.col - 1; - var el = RangeToken.EndToken.line; - var ec = RangeToken.EndToken.col - 1; + var fn = Range.StartToken.filename; + var sl = Range.StartToken.line; + var sc = Range.StartToken.col - 1; + var el = Range.EndToken.line; + var ec = Range.EndToken.col - 1; return $"{fn}({sl},{sc})-({el},{ec})"; } public string OriginalString() { - return RangeToken?.PrintOriginal(); + return Range?.PrintOriginal(); } } +// Represents the portion of a Dafny program corresponding to a proof +// obligation. This is particularly important to track because if a particular +// assertion batch can be proved without proving one of the assertions that is +// a proof obligation within it, that assertion must have been proved vacuously. public class ProofObligationDependency : ProofDependency { - public override RangeToken RangeToken { get; } + public override RangeToken Range { get; } public PODesc.ProofObligationDescription ProofObligation { get; } @@ -47,15 +61,17 @@ public class ProofObligationDependency : ProofDependency { $"{ProofObligation.SuccessDescription}"; public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) { - RangeToken = tok as RangeToken ?? new RangeToken(tok, tok); + Range = tok as RangeToken ?? new RangeToken(tok, tok); ProofObligation = proofObligation; } } +// Represents the assumption of a requires clause in the process of +// proving a Dafny definition. public class RequiresDependency : ProofDependency { private Expression requires; - public override RangeToken RangeToken => + public override RangeToken Range => requires.RangeToken; public override string Description => @@ -66,10 +82,11 @@ public RequiresDependency(Expression requires) { } } +// Represents the goal of proving an ensures clause of a Dafny definition. public class EnsuresDependency : ProofDependency { private Expression ensures; - public override RangeToken RangeToken => + public override RangeToken Range => ensures.RangeToken; public override string Description => @@ -80,12 +97,14 @@ public EnsuresDependency(Expression ensures) { } } +// Represents the goal of proving a specific requires clause of a specific +// call. public class CallRequiresDependency : ProofDependency { private CallDependency call; private RequiresDependency requires; - public override RangeToken RangeToken => - call.RangeToken; + public override RangeToken Range => + call.Range; public override string Description => $"requires clause at {requires.RangeString()} from call"; @@ -96,12 +115,14 @@ public CallRequiresDependency(CallDependency call, RequiresDependency requires) } } +// Represents the assumption of a specific ensures clause of a specific +// call. public class CallEnsuresDependency : ProofDependency { private CallDependency call; private EnsuresDependency ensures; - public override RangeToken RangeToken => - call.RangeToken; + public override RangeToken Range => + call.Range; public override string Description => $"ensures clause at {ensures.RangeString()} from call"; @@ -112,10 +133,11 @@ public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { } } +// Represents the fact that a particular call occurred. public class CallDependency : ProofDependency { private CallStmt call; - public override RangeToken RangeToken => + public override RangeToken Range => call.RangeToken; public override string Description => @@ -126,10 +148,11 @@ public CallDependency(CallStmt call) { } } +// Represents the assumption of a predicate in an `assume` statement. public class AssumptionDependency : ProofDependency { private Expression expr; - public override RangeToken RangeToken => + public override RangeToken Range => expr.RangeToken; public override string Description => @@ -143,10 +166,11 @@ public AssumptionDependency(string comment, Expression expr) { } } +// Represents the invariant of a loop. public class InvariantDependency : ProofDependency { private Expression invariant; - public override RangeToken RangeToken => + public override RangeToken Range => invariant.RangeToken; public override string Description => @@ -157,19 +181,22 @@ public InvariantDependency(Expression invariant) { } } +// Represents an assignment statement. This includes the assignment to an +// out parameter implicit in a return statement. public class AssignmentDependency : ProofDependency { - public override RangeToken RangeToken { get; } + public override RangeToken Range { get; } public override string Description => "assignment (or return)"; public AssignmentDependency(RangeToken rangeToken) { - this.RangeToken = rangeToken; + this.Range = rangeToken; } } +// Represents dependency of a proof on the definition of a specific function. public class FunctionDefinitionDependency : ProofDependency { - public override RangeToken RangeToken => function.RangeToken; + public override RangeToken Range => function.RangeToken; public override string Description => $"function definition for {function.Name}"; From 6a671dda8eaca41593a183d706392e8bd9ec6a0d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 10:04:51 -0700 Subject: [PATCH 18/44] Fix duplicate IDs in Boogie code --- Source/DafnyCore/Verifier/Translator.cs | 1 - Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 16 ++++++++-------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 8a04b9be8aa..3bb055a4b15 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -7382,7 +7382,6 @@ public override IToken WithVal(string newVal) { Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription description, Bpl.QKeyValue kv = null) { var cmd = Assert(tok, condition, description, tok, kv); - proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description)); return cmd; } diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect index 7a88f9ecd56..a9c4bb828b8 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -1,12 +1,12 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id1"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} {:id "id5"} true; +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id5"} true; >>> DoNothingToAssert Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id4"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} {:id "id9"} true; +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id8"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id7"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -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 "id14"} Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id12"} Lit(false); >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion might not hold -Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id19"} {:id "id18"} true; +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id16"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id15"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} {:id "id22"} true; +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id19"} true; >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id21"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id18"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error From 3e4a91b1da1e8ccd68486afcfaf4be0aad1c9e68 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 12:02:28 -0700 Subject: [PATCH 19/44] Fix NPE in test generation code This occurs due to a Boogie change that now dereferences a property that previously was supposed to never be null but wasn't blindly dereferenced. --- .../Inlining/AddImplementationForCallsRewriter.cs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs index 7c06530d4ae..d6844fa3c7b 100644 --- a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs +++ b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs @@ -82,6 +82,19 @@ public AddImplementationsForCallsRewriter(DafnyOptions options) { return node; } + public override Implementation VisitImplementation(Implementation node) { + this.VisitVariableSeq(node.LocVars); + this.VisitBlockList(node.Blocks); + if (node.Proc is not null) { + // TODO: The overall test generation code should be refactored so that + // this case can't occur. The default visitor for Implementation nodes + // has an invariant that node.Proc is never null. That invariant did + // not lead to an NPE until Boogie 3.0.1, however. + node.Proc = (Procedure)node.Proc.StdDispatch((StandardVisitor)this); + } + return (Implementation)this.VisitDeclWithFormals((DeclWithFormals)node); + } + public override Program VisitProgram(Program node) { program = node; implsToAdd = new(); From 9e2ad029dca5850d1de1a5680ed347d2b72ea0fe Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 16:26:44 -0700 Subject: [PATCH 20/44] Fix expected test output --- Source/DafnyPipeline.Test/InterMethodVerificationStability.cs | 4 ++-- Test/dafny0/ReadsOnMethods.dfy.expect | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs index 0298cee3ede..0c42611401a 100644 --- a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs @@ -131,8 +131,8 @@ modify heap { + assume k#0_0 < x#0; - x#1_0 := LitInt(0); + a#1_0 := LitInt(0); -- assume !(exists eg$y#1: int :: eg$y#1 < x#0); -+ assume !(exists eg$k#1: int :: eg$k#1 < x#0); +- assume {:id ""id2""} !(exists eg$y#1: int :: eg$y#1 < x#0); ++ assume {:id ""id2""} !(exists eg$k#1: int :: eg$k#1 < x#0); - y#2_0 := LitInt(0); + b#2_0 := LitInt(0); - x#3_0 := LitInt(2); diff --git a/Test/dafny0/ReadsOnMethods.dfy.expect b/Test/dafny0/ReadsOnMethods.dfy.expect index 589f533c82f..c2b5db022a2 100644 --- a/Test/dafny0/ReadsOnMethods.dfy.expect +++ b/Test/dafny0/ReadsOnMethods.dfy.expect @@ -31,6 +31,6 @@ ReadsOnMethods.dfy(530,50): Error: insufficient reads clause to read field ReadsOnMethods.dfy(169,10): Error: insufficient reads clause to read field ReadsOnMethods.dfy(172,19): Error: insufficient reads clause to read field ReadsOnMethods.dfy(183,25): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(469,9): Error: method might read an object not in the parent trait context's reads clause +ReadsOnMethods.dfy(469,2): Error: method might read an object not in the parent trait context's reads clause Dafny program verifier finished with 64 verified, 31 errors From 9133cf7b5ad3d5121c573eb7c81169d7c3286ed0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 30 Aug 2023 16:42:13 -0700 Subject: [PATCH 21/44] Various small cleanups --- Source/DafnyCore/Verifier/ProofDependency.cs | 18 +++++++++--------- .../Verifier/Translator.BoogieFactory.cs | 14 ++++++++++---- .../Translator.ExpressionWellformed.cs | 10 +++++----- .../Verifier/Translator.TrStatement.cs | 4 ++-- 4 files changed, 26 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index f61aa7bc1e8..044b9c40384 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -84,7 +84,7 @@ public RequiresDependency(Expression requires) { // Represents the goal of proving an ensures clause of a Dafny definition. public class EnsuresDependency : ProofDependency { - private Expression ensures; + private readonly Expression ensures; public override RangeToken Range => ensures.RangeToken; @@ -100,8 +100,8 @@ public EnsuresDependency(Expression ensures) { // Represents the goal of proving a specific requires clause of a specific // call. public class CallRequiresDependency : ProofDependency { - private CallDependency call; - private RequiresDependency requires; + private readonly CallDependency call; + private readonly RequiresDependency requires; public override RangeToken Range => call.Range; @@ -118,8 +118,8 @@ public CallRequiresDependency(CallDependency call, RequiresDependency requires) // Represents the assumption of a specific ensures clause of a specific // call. public class CallEnsuresDependency : ProofDependency { - private CallDependency call; - private EnsuresDependency ensures; + private readonly CallDependency call; + private readonly EnsuresDependency ensures; public override RangeToken Range => call.Range; @@ -135,7 +135,7 @@ public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { // Represents the fact that a particular call occurred. public class CallDependency : ProofDependency { - private CallStmt call; + private readonly CallStmt call; public override RangeToken Range => call.RangeToken; @@ -150,7 +150,7 @@ public CallDependency(CallStmt call) { // Represents the assumption of a predicate in an `assume` statement. public class AssumptionDependency : ProofDependency { - private Expression expr; + private readonly Expression expr; public override RangeToken Range => expr.RangeToken; @@ -158,7 +158,7 @@ public class AssumptionDependency : ProofDependency { public override string Description => comment ?? $"assume {OriginalString()}"; - private string comment; + private readonly string comment; public AssumptionDependency(string comment, Expression expr) { this.comment = comment; @@ -168,7 +168,7 @@ public AssumptionDependency(string comment, Expression expr) { // Represents the invariant of a loop. public class InvariantDependency : ProofDependency { - private Expression invariant; + private readonly Expression invariant; public override RangeToken Range => invariant.RangeToken; diff --git a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs index ea106849dec..bb9f4ad87fa 100644 --- a/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs @@ -198,13 +198,19 @@ public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyV return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes); } - public Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, string comment = null, Bpl.QKeyValue attributes = null) { - return TrAssumeCmdWithDependenciesApp(etran, tok, dafnyExpr, e => e, comment, attributes); + private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, string comment = null, Bpl.QKeyValue attributes = null) { + return TrAssumeCmdWithDependenciesAndExtend(etran, tok, dafnyExpr, e => e, comment, attributes); } - public Bpl.AssumeCmd TrAssumeCmdWithDependenciesApp(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func func, string comment = null, Bpl.QKeyValue attributes = null) { + // This method translates a Dafny expression to a Boogie expression, + // applies an arbitrary provided function to that Boogie expression + // to extend it (by combining it with other, already-translated + // expressions, for instance), creates an assume statement in Boogie, + // and then adds information to track that assumption as a potential + // proof dependency. + private Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func extendExpr, string comment = null, Bpl.QKeyValue attributes = null) { var expr = etran.TrExpr(dafnyExpr); - var cmd = TrAssumeCmd(tok, func(expr), attributes); + var cmd = TrAssumeCmd(tok, extendExpr(expr), attributes); proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(comment, dafnyExpr)); return cmd; } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index 2cc51f23eda..0780a66b9ad 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -167,7 +167,7 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List Bpl.Expr.Eq(result, e), + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr, e => Bpl.Expr.Eq(result, e), resultDescription)); builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); @@ -1364,7 +1364,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran, "let expression binding RHS well-formed"); CheckCasePatternShape(pat, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); - builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); } CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran, "let expression result"); @@ -1423,7 +1423,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r Contract.Assert(resultType != null); var bResult = etran.TrExpr(letBody); CheckSubrange(letBody.tok, bResult, letBody.Type, resultType, builder); - builder.Add(TrAssumeCmdWithDependenciesApp(etran, e.tok, letBody, e => Expr.Eq(result, e), "let expression")); + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, letBody, e => Expr.Eq(result, e), "let expression")); builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType))); diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index bb9d1ab2f2e..92e2d7a690b 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -501,7 +501,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List Expr.Eq(e, rIe), "variable declaration")); + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, s.tok, pat.Expr, e => Expr.Eq(e, rIe), "variable declaration")); } else if (stmt is TryRecoverStatement haltRecoveryStatement) { // try/recover statements are currently internal-only AST nodes that cannot be // directly used in user Dafny code. They are only generated by rewriters, and verifying @@ -997,7 +997,7 @@ private void TrIfStmt(IfStmt stmt, BoogieStmtListBuilder builder, List Bpl.IfCmd elsIf = null; b = new BoogieStmtListBuilder(this, options); if (stmt.IsBindingGuard) { - b.Add(TrAssumeCmdWithDependenciesApp(etran, guard.tok, guard, Expr.Not, "if statement binding guard")); + b.Add(TrAssumeCmdWithDependenciesAndExtend(etran, guard.tok, guard, Expr.Not, "if statement binding guard")); } if (stmt.Els == null) { els = b.Collect(stmt.Tok); From 04fca8835fcf22200705ea9c1af848757eae8ee5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 15:00:14 -0700 Subject: [PATCH 22/44] Use structured dependency labels from Boogie --- Source/DafnyCore/DafnyCore.csproj | 2 +- .../Verifier/ProofDependencyManager.cs | 70 +++++-------------- 2 files changed, 20 insertions(+), 52 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 823adbc7b3b..f8354da99f8 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -32,7 +32,7 @@ - + diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index aa9ef0d6c52..91d8eb461aa 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -37,61 +37,29 @@ public void AddProofDependencyId(ICarriesAttributes boogieNode, IToken tok, Proo new QKeyValue(tok, idAttributeName, new List() { idString }, boogieNode.Attributes); } - // This suffix indicates that an ID string represents the assumption of - // a specific ensures clause after a specific call. - private const string ensuresSuffix = "$ensures"; - - // This suffix indicates that an ID string represents the goal of - // proving a specific requires clause before a specific call. - private const string requiresSuffix = "$requires"; - - // This suffix indicates that an ID string represents the assumption - // of a specific requires clause after a specific call. - private const string requiresAssumedSuffix = "$requires_assumed"; - - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is established. - private const string establishedSuffix = "$established"; - - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is maintained. - private const string maintainedSuffix = "$maintained"; - - // This suffix indicates that an ID string represents the asssumption - // of a specific loop invariant in the body of the loop. - private const string assumeInBodySuffix = "$assume_in_body"; - - // Get the full ProofDependency indicated by a compound ID string. These strings are - // returned by the SMT solver to indicate which sub-formulas it used in constructing - // a proof of a particular goal (more technically, the UNSAT core of the negation of - // the goal). Because SMT-Lib only accepts strings as labels, we need to embed some - // extra information in those strings to represent ways in which the original Boogie - // commands and expressions are transformed and duplicated during Boogie's VC - // generation process. - public ProofDependency GetFullIdDependency(string idString) { - var parts = idString.Split('$'); - if (idString.EndsWith(requiresSuffix) && parts.Length == 3) { - var reqId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; + public ProofDependency GetFullIdDependency(TrackedNodeComponent component) { + if (component is TrackedCallRequiresGoal requiresGoal) { + var reqId = ProofDependenciesById[requiresGoal.requiresId]; + var callId = ProofDependenciesById[requiresGoal.callId]; return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); - } else if (idString.EndsWith(requiresAssumedSuffix) && parts.Length == 3) { - var reqId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; + } else if (component is TrackedCallRequiresAssumed requiresAssumed) { + var reqId = ProofDependenciesById[requiresAssumed.requiresId]; + var callId = ProofDependenciesById[requiresAssumed.callId]; return new CallRequiresDependency((CallDependency)callId, (RequiresDependency)reqId); - } else if (idString.EndsWith(ensuresSuffix) && parts.Length == 3) { - var ensId = ProofDependenciesById[parts[0]]; - var callId = ProofDependenciesById[parts[1]]; + } else if (component is TrackedCallEnsures callEnsures) { + var ensId = ProofDependenciesById[callEnsures.ensuresId]; + var callId = ProofDependenciesById[callEnsures.callId]; return new CallEnsuresDependency((CallDependency)callId, (EnsuresDependency)ensId); - } else if (idString.EndsWith(establishedSuffix) && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (idString.EndsWith(maintainedSuffix) && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (idString.EndsWith(assumeInBodySuffix) && parts.Length == 2) { - return ProofDependenciesById[parts[0]]; - } else if (parts.Length > 1) { - throw new ArgumentException($"Malformed dependency ID string: {idString}"); + } else if (component is TrackedInvariantEstablished invariantEstablished) { + return ProofDependenciesById[invariantEstablished.invariantId]; + } else if (component is TrackedInvariantMaintained invariantMaintained) { + return ProofDependenciesById[invariantMaintained.invariantId]; + } else if (component is TrackedInvariantAssumed invariantAssumed) { + return ProofDependenciesById[invariantAssumed.invariantId]; + } else if (component is LabeledNodeComponent labeledNodeComponent) { + return ProofDependenciesById[labeledNodeComponent.SolverLabel]; } else { - return ProofDependenciesById[idString]; + throw new ArgumentException($"Malformed dependency ID: {component.SolverLabel}"); } } } From 813b190b83d75d69487e3edfb230a17f9afabe8c Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 16:48:42 -0700 Subject: [PATCH 23/44] Limit proof dependency analysis to one core Temporary until we fix a Boogie concurrency bug --- Test/logger/ProofDependencyLogging.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy index b8864d823ef..aff40bf6e97 100644 --- a/Test/logger/ProofDependencyLogging.dfy +++ b/Test/logger/ProofDependencyLogging.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t" +// RUN: %baredafny verify --cores:1 --log-format:text --boogie -trackVerificationCoverage "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Results for RedundantAssumeMethod \(correctness\) // CHECK: Proof dependencies: From 5e756567e82efa5a1633cad0a414af221e0074b8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 16:57:31 -0700 Subject: [PATCH 24/44] Fix customBoogie.patch --- customBoogie.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/customBoogie.patch b/customBoogie.patch index fac7c377fb8..396797649e9 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + From 1f9f243a1ad9922a6a74249412dae5ac6a8821cf Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 Sep 2023 09:12:21 -0700 Subject: [PATCH 25/44] Bump Boogie dependency And remove concurrency limitation from proof dependency test. --- Source/DafnyCore/DafnyCore.csproj | 2 +- Test/logger/ProofDependencyLogging.dfy | 2 +- customBoogie.patch | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index f8354da99f8..ca893520925 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -32,7 +32,7 @@ - + diff --git a/Test/logger/ProofDependencyLogging.dfy b/Test/logger/ProofDependencyLogging.dfy index aff40bf6e97..b8864d823ef 100644 --- a/Test/logger/ProofDependencyLogging.dfy +++ b/Test/logger/ProofDependencyLogging.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny verify --cores:1 --log-format:text --boogie -trackVerificationCoverage "%s" > "%t" +// RUN: %baredafny verify --log-format:text --boogie -trackVerificationCoverage "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Results for RedundantAssumeMethod \(correctness\) // CHECK: Proof dependencies: diff --git a/customBoogie.patch b/customBoogie.patch index 396797649e9..a5ce1586f3e 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + From 9e4bd05e3ff2e1e3d9b43f589dedfa13aaf81f1d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 Sep 2023 10:15:23 -0700 Subject: [PATCH 26/44] Bump Boogie version in dotnet-tools.json, too --- dotnet-tools.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dotnet-tools.json b/dotnet-tools.json index 3f18a8db86e..b50d45ebe2b 100644 --- a/dotnet-tools.json +++ b/dotnet-tools.json @@ -15,10 +15,10 @@ ] }, "boogie": { - "version": "2.16.0", + "version": "3.0.3", "commands": [ "boogie" ] } } -} \ No newline at end of file +} From 1ced5195298e04f4580abce0b3a6726ed236610e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Sat, 2 Sep 2023 09:35:43 -0700 Subject: [PATCH 27/44] Warn about vacuous proofs and unused assumptions --- Source/DafnyCore/DafnyMain.cs | 52 +++++++++++++++++++ Source/DafnyCore/Options/CommonOptionBag.cs | 8 +++ Source/DafnyCore/Options/ICommandSpec.cs | 4 +- .../Verifier/ProofDependencyManager.cs | 16 ++++++ .../Verifier/Translator.ClassMembers.cs | 4 ++ Source/DafnyCore/Verifier/Translator.cs | 9 ++++ Source/DafnyDriver/DafnyDriver.cs | 6 +++ 7 files changed, 98 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index ad53637fe1d..a6e4edbe96d 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -13,6 +13,7 @@ using System.Threading; using System.Threading.Tasks; using DafnyCore; +using DafnyCore.Verifier; using Microsoft.Boogie; using Microsoft.Extensions.Logging; using Microsoft.Extensions.Logging.Abstractions; @@ -203,5 +204,56 @@ await options.OutputWriter.WriteLineAsync( } } + public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) { + var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList(); + var orderedResults = + verificationResults.OrderBy(vr => + (vr.Item1.tok.filename, vr.Item1.tok.line, vr.Item1.tok.col)); + foreach (var (implementation, result) in orderedResults) { + WarnAboutSuspiciousDependenciesForImplementation(dafnyOptions, reporter, depManager, implementation, result); + } + } + + public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, Implementation implementation, VerificationResult result) { + var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(implementation.VerboseName); + var usedDependencyIds = result.VCResults.SelectMany(vcResult => vcResult.coveredElements); + var usedDependencies = + usedDependencyIds + .Select(depManager.GetFullIdDependency) + .OrderBy(dep => (dep.RangeString(), dep.Description)); + var unusedDependencyIds = potentialDependencies.Except(usedDependencyIds); + var unusedDependencies = + unusedDependencyIds + .Select(depManager.GetFullIdDependency) + .OrderBy(dep => (dep.RangeString(), dep.Description)); + + var unusedObligations = unusedDependencies.OfType(); + var unusedRequires = unusedDependencies.OfType(); + var unusedEnsures = unusedDependencies.OfType(); + var unusedAssumeStatements = + unusedDependencies + .OfType() + .Where(d => d.Description.Contains("assume statement")); + if (dafnyOptions.Get(CommonOptionBag.WarnVacuity)) { + foreach (var dep in unusedObligations) { + reporter.Warning(MessageSource.Verifier, "", dep.Range, $"vacuous proof: {dep.Description}"); + } + + foreach (var dep in unusedEnsures) { + reporter.Warning(MessageSource.Verifier, "", dep.Range, $"vacuous proof of ensures clause"); + } + } + + if (dafnyOptions.Get(CommonOptionBag.WarnRedundantAssumptions)) { + foreach (var dep in unusedRequires) { + reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary requires clause"); + } + + foreach (var dep in unusedAssumeStatements) { + reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary assumption"); + } + } + } + } } diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 4378abbde2a..e1836caa569 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -185,6 +185,10 @@ Note that quantifier variable domains (<- ) are available in both syntax "Emits a warning when a constructor name in a case pattern is not followed by parentheses."); public static readonly Option WarnShadowing = new("--warn-shadowing", "Emits a warning if the name of a declared variable caused another variable to be shadowed."); + public static readonly Option WarnVacuity = new("--warn-vacuity", + "Emits a warning if any assertions are proved vacuously (that is, based on contradictory assumptions). May slow down verification slightly."); + public static readonly Option WarnRedundantAssumptions = new("--warn-redundant-assumptions", + "Emits a warning if any `requires` clause or `assume` statement was not needed to complete verification. May slow down verification slightly."); public static readonly Option IncludeRuntimeOption = new("--include-runtime", "Include the Dafny runtime as source in the target language."); @@ -248,6 +252,8 @@ static CommonOptionBag() { DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => { options.WarningsAsErrors = value; }); DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles, (options, value) => { options.VerifyAllModules = value; }); + DafnyOptions.RegisterLegacyBinding(WarnVacuity, (options, value) => { options.TrackVerificationCoverage = true; }); + DafnyOptions.RegisterLegacyBinding(WarnRedundantAssumptions, (options, value) => { options.TrackVerificationCoverage = true; }); DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; }); @@ -347,6 +353,8 @@ static CommonOptionBag() { WarnMissingConstructorParenthesis, UseJavadocLikeDocstringRewriterOption, IncludeRuntimeOption, + WarnVacuity, + WarnRedundantAssumptions, DefaultFunctionOpacity ); } diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs index 3e3775bbfbd..7c1c0e6cf38 100644 --- a/Source/DafnyCore/Options/ICommandSpec.cs +++ b/Source/DafnyCore/Options/ICommandSpec.cs @@ -42,7 +42,9 @@ static ICommandSpec() { BoogieOptionBag.SolverLog, CommonOptionBag.JsonDiagnostics, BoogieOptionBag.VerificationErrorLimit, - CommonOptionBag.DefaultFunctionOpacity + CommonOptionBag.DefaultFunctionOpacity, + CommonOptionBag.WarnVacuity, + CommonOptionBag.WarnRedundantAssumptions }.ToList(); public static IReadOnlyList