From 44ca1b2a165c69a32f39714e95cdd07002da2ebb Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 19 Apr 2024 14:01:13 -0700 Subject: [PATCH 001/152] Retry LSP tests in case of error (#5342) ### Description This PR changes how the language server unit tests execute, retrying them up to three times if they fail. Ultimately, this is what we're doing by hand, anyway, so we might as well automate it. The proper solution to this problem is to ensure that the language server tests don't spuriously fail, but this will accelerate our development process in the meantime. ### How has this been tested? By running CI normally. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --- .github/workflows/xunit-tests-reusable.yml | 24 +++++++++++----------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml index b4f7c95c86c..09f0e6f5e2e 100644 --- a/.github/workflows/xunit-tests-reusable.yml +++ b/.github/workflows/xunit-tests-reusable.yml @@ -45,10 +45,6 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: 6.0.x - - name: Install dependencies - run: | - dotnet restore ${{env.solutionPath}} - dotnet tool install dotnet-coverage - name: Load Z3 shell: pwsh run: | @@ -64,17 +60,21 @@ jobs: run: | chmod +x Binaries/z3/bin/z3* - name: Build - run: dotnet build --no-restore ${{env.solutionPath}} + run: dotnet build ${{env.solutionPath}} - name: Run DafnyCore Tests run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test + # Retry LSP tests 3 times because there are some spurious errors + # Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package - name: Run DafnyLanguageServer Tests - run: | - ## Run twice to catch unstable code (Issue #2673) - dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test - ## On the second run, collect test coverage data - ## Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package - dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test - + uses: nick-fields/retry@v3 + with: + timeout_minutes: 45 + max_attempts: 3 + command: | + cd dafny + dotnet restore ${{env.solutionPath}} + dotnet tool install dotnet-coverage + dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test - name: Run DafnyDriver Tests run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test - name: Run DafnyPipeline Tests From 846a2f6159ca1c8cdce82b5684975eaa0d186538 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 19 Apr 2024 16:28:27 -0700 Subject: [PATCH 002/152] Refactoring to support `decreases to` (#5315) ### Description This is a refactoring-only PR intended to make implementing [`decreases to`](https://github.com/dafny-lang/dafny/issues/5252) more straightforward when we do it. ### How has this been tested? With the existing test suite, as it's purely a refactoring. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --- .../Verifier/BoogieGenerator.Decreases.cs | 24 +++++++---- .../BoogieGenerator.ExpressionWellformed.cs | 14 +++---- .../Verifier/BoogieGenerator.TrStatement.cs | 40 ++++++++++++++++++- .../Verifier/ProofObligationDescription.cs | 14 +++++-- .../Snapshots2.run.legacy.dfy.expect | 8 ++-- 5 files changed, 76 insertions(+), 24 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs index 31e18d6bde2..836f650a29a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs @@ -33,16 +33,15 @@ public partial class BoogieGenerator { /// allowance || (calleeDecreases LESS contextDecreases). /// void CheckCallTermination(IToken tok, List contextDecreases, List calleeDecreases, - Bpl.Expr allowance, + Expression allowance, Expression receiverReplacement, Dictionary substMap, Dictionary typeMap, - ExpressionTranslator etranCurrent, ExpressionTranslator etranInitial, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) { + ExpressionTranslator etranCurrent, bool oldCaller, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(contextDecreases)); Contract.Requires(cce.NonNullElements(calleeDecreases)); Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); Contract.Requires(etranCurrent != null); - Contract.Requires(etranInitial != null); Contract.Requires(builder != null); // The interpretation of the given decreases-clause expression tuples is as a lexicographic tuple, extended into @@ -62,6 +61,8 @@ void CheckCallTermination(IToken tok, List contextDecreases, List(); var callee = new List(); var caller = new List(); + var oldExpressions = new List(); + var newExpressions = new List(); if (RefinementToken.IsInherited(tok, currentModule) && contextDecreases.All(e => !RefinementToken.IsInherited(e.tok, currentModule))) { // the call site is inherited but all the context decreases expressions are new tok = new ForceCheckToken(tok); @@ -69,22 +70,31 @@ void CheckCallTermination(IToken tok, List contextDecreases, List @@ -347,4 +357,4 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out atmost = BplImp(b0, b1); } } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 96bbfcbaae5..784c2ed1165 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -769,7 +769,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv); } } - Bpl.Expr allowance = null; + Expression allowance = null; if (codeContext != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is ExtremePredicate)) { // check that the decreases measure goes down var calleeSCCLookup = e.IsByMethodCall ? (ICallable)e.Function.ByMethodDecl : e.Function; @@ -781,16 +781,14 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re List contextDecreases = codeContext.Decreases.Expressions; List calleeDecreases = e.Function.Decreases.Expressions; if (e.Function == wfOptions.SelfCallsAllowance) { - allowance = Bpl.Expr.True; + allowance = Expression.CreateBoolLiteral(e.tok, true); if (!e.Function.IsStatic) { - allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This))); + allowance = Expression.CreateAnd(allowance, Expression.CreateEq(e.Receiver, new ThisExpr(e.Function), e.Receiver.Type)); } for (int i = 0; i < e.Args.Count; i++) { Expression ee = e.Args[i]; Formal ff = e.Function.Formals[i]; - allowance = BplAnd(allowance, - Bpl.Expr.Eq(etran.TrExpr(ee), - new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration.IdGenerator), TrType(ff.Type)))); + allowance = Expression.CreateAnd(allowance, Expression.CreateEq(ee, Expression.CreateIdentExpr(ff), ff.Type)); } } string hint; @@ -821,7 +819,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re hint = hint == null ? e.CoCallHint : string.Format("{0}; {1}", hint, e.CoCallHint); } CheckCallTermination(callExpr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, e.GetTypeArgumentSubstitutions(), - etran, etran, builder, codeContext.InferredDecreases, hint); + etran, false, builder, codeContext.InferredDecreases, hint); } } } @@ -829,7 +827,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(callExpr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool); List args = etran.FunctionInvocationArguments(e, null, null); Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(GetToken(expr), new Bpl.FunctionCall(canCallFuncID), args); - builder.Add(TrAssumeCmd(callExpr.tok, allowance == null ? canCallFuncAppl : BplOr(allowance, canCallFuncAppl))); + builder.Add(TrAssumeCmd(callExpr.tok, allowance == null ? canCallFuncAppl : BplOr(etran.TrExpr(allowance), canCallFuncAppl))); var returnType = e.Type.AsDatatype; if (returnType != null && returnType.Ctors.Count == 1) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 23025289acf..2ea293d3513 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1549,15 +1549,23 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, var toks = new List(); var types = new List(); var decrs = new List(); + var oldDecreases = new List(); + var prevGhostLocals = new List(); foreach (Expression e in theDecreases) { toks.Add(e.tok); types.Add(e.Type.NormalizeExpand()); + // Note: the label "LoopEntry" doesn't exist in the program, and is + // useful only for explanatory purposes. + var (vars, olde) = TranslateToLoopEntry(s.Mod, e, "LoopEntry"); + oldDecreases.Add(olde); + prevGhostLocals.AddRange(vars); decrs.Add(etran.TrExpr(e)); } if (includeTerminationCheck) { AddComment(loopBodyBuilder, s, "loop termination check"); Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false); - loopBodyBuilder.Add(Assert(s.Tok, decrCheck, new PODesc.Terminates(s.InferredDecreases, true))); + loopBodyBuilder.Add(Assert(s.Tok, decrCheck, new + PODesc.Terminates(s.InferredDecreases, prevGhostLocals, null, oldDecreases, theDecreases))); } } } else if (isBodyLessLoop) { @@ -1584,6 +1592,34 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, new List(), body)); } + // Return the version of e that holds at the beginnging of the loop, + // Along with the local variable assignments that need to happen at + // the beginning of the loop for it to be valid. + private (List, Expression) TranslateToLoopEntry(Specification mod, Expression e, string loopLabel) { + var prevGhostLocals = new List(); + Expression olde = new OldExpr(e.tok, e, "LoopEntry") { + Type = e.Type + }; + + if (mod is null || mod.Expressions is null) { + return (prevGhostLocals, olde); + } + + foreach (var x in mod.Expressions) { + if (x.E is IdentifierExpr { Var: LocalVariable v }) { + var prevName = $"prev_{v.Name}"; + var prevVar = new LocalVariable(RangeToken.NoToken, prevName, v.Type, true); + var declStmt = Statement.CreateLocalVariable(RangeToken.NoToken, prevName, x.E); + prevGhostLocals.Add(declStmt); + var prevExpr = new IdentifierExpr(x.E.tok, prevVar); + olde = Substitute(olde, v, prevExpr); + } + } + + return (prevGhostLocals, olde); + + } + void InsertContinueTarget(LoopStmt loop, BoogieStmtListBuilder builder) { Contract.Requires(loop != null); Contract.Requires(builder != null); @@ -1936,7 +1972,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E } else { List contextDecreases = codeContext.Decreases.Expressions; List calleeDecreases = callee.Decreases.Expressions; - CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, tySubst, etran, etran.Old, builder, codeContext.InferredDecreases, null); + CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, tySubst, etran, true, builder, codeContext.InferredDecreases, null); } } diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 6c0c5460d5b..eeb61c49991 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -628,13 +628,21 @@ public class Terminates : ProofObligationDescription { public override string ShortDescription => "termination"; private readonly bool inferredDescreases; - private readonly bool isLoop; + private bool isLoop => prevGhostLocals is not null; private readonly string hint; private string FormDescription => isLoop ? "expression" : "clause"; - public Terminates(bool inferredDescreases, bool isLoop, string hint = null) { + private readonly Expression allowance; + private readonly List oldExpressions; + private readonly List newExpressions; + private readonly List prevGhostLocals; + + public Terminates(bool inferredDescreases, List prevGhostLocals, Expression allowance, List oldExpressions, List newExpressions, string hint = null) { this.inferredDescreases = inferredDescreases; - this.isLoop = isLoop; + this.prevGhostLocals = prevGhostLocals; + this.allowance = allowance; + this.oldExpressions = oldExpressions; + this.newExpressions = newExpressions; this.hint = hint; } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect index a9c4bb828b8..768491421f5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect @@ -1,10 +1,10 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id1"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id5"} true; +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id5"} Lit(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 "id8"} true; +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id8"} Lit(true); >>> DoNothingToAssert Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id7"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert @@ -19,11 +19,11 @@ Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)): 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 "id16"} true; +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id16"} Lit(true); >>> DoNothingToAssert 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 "id19"} true; +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id19"} Lit(true); >>> DoNothingToAssert Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id18"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert From 2e6a08c2882d10caa5f6bbfef09c5b1bdd31752f Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Fri, 19 Apr 2024 17:29:20 -0700 Subject: [PATCH 003/152] Add first pass of proof obligation description expressions (#5317) ### Description Adds a first pass of proof obligation description expressions, towards resolving https://github.com/dafny-lang/dafny/issues/2987. It also adds a new hidden option, `--show-proof-obligation-expressions`, which adds to each (supported) failed proof obligation error message an equivalent Dafny assertion. This option is used to automate tests for the newly added proof obligation description expressions, but this PR does not backfill tests for existing PODesc expressions. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aaron Tomb --- Source/DafnyCore/DafnyOptions.cs | 6 + .../DafnyCore/Generic/ReporterExtensions.cs | 3 +- Source/DafnyCore/Options/CommonOptionBag.cs | 13 +- Source/DafnyCore/Options/DafnyCommands.cs | 3 +- Source/DafnyCore/Pipeline/Compilation.cs | 38 +++ .../BoogieGenerator.ExpressionWellformed.cs | 56 ++-- .../Verifier/BoogieGenerator.Functions.cs | 2 +- .../Verifier/BoogieGenerator.Methods.cs | 7 +- .../Verifier/BoogieGenerator.TrStatement.cs | 41 ++- .../Verifier/BoogieGenerator.Types.cs | 68 +++-- Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- .../Verifier/ProofObligationDescription.cs | 271 ++++++++++++++++-- .../array-init-empty.dfy | 6 + .../array-init-empty.dfy.expect | 4 + .../array-init-size-valid.dfy | 6 + .../array-init-size-valid.dfy.expect | 4 + .../char-overflow-non-unicode.dfy | 6 + .../char-overflow-non-unicode.dfy.expect | 5 + .../char-overflow-unicode.dfy | 6 + .../char-overflow-unicode.dfy.expect | 4 + .../char-underflow-non-unicode.dfy | 6 + .../char-underflow-non-unicode.dfy.expect | 5 + .../char-underflow-unicode.dfy | 6 + .../char-underflow-unicode.dfy.expect | 4 + .../proof-obligation-desc/conversion-fit.dfy | 7 + .../conversion-fit.dfy.expect | 4 + .../conversion-is-natural.dfy | 7 + .../conversion-is-natural.dfy.expect | 4 + .../conversion-positive.dfy | 7 + .../conversion-positive.dfy.expect | 4 + .../conversion-satisfies-constraints.dfy | 9 + ...onversion-satisfies-constraints.dfy.expect | 4 + .../for-range-assignable.dfy | 7 + .../for-range-assignable.dfy.expect | 4 + .../for-range-bounds-valid.dfy | 7 + .../for-range-bounds-valid.dfy.expect | 4 + .../forall-postcondition.dfy | 7 + .../forall-postcondition.dfy.expect | 5 + .../proof-obligation-desc/is-allocated.dfy | 12 + .../is-allocated.dfy.expect | 4 + .../proof-obligation-desc/is-integer.dfy | 7 + .../is-integer.dfy.expect | 4 + .../proof-obligation-desc/non-negative.dfy | 7 + .../non-negative.dfy.expect | 4 + .../proof-obligation-desc/non-null.dfy | 7 + .../proof-obligation-desc/non-null.dfy.expect | 4 + .../ordinal-subtraction-is-natural.dfy | 8 + .../ordinal-subtraction-is-natural.dfy.expect | 4 + .../ordinal-subtraction-underflow.dfy | 8 + .../ordinal-subtraction-underflow.dfy.expect | 4 + .../shift-lower-bound.dfy | 6 + .../shift-lower-bound.dfy.expect | 4 + .../shift-upper-bound.dfy | 6 + .../shift-upper-bound.dfy.expect | 4 + .../proof-obligation-desc/witness-check.dfy | 4 + .../witness-check.dfy.expect | 4 + 56 files changed, 666 insertions(+), 87 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index ad51aac1252..f5855a8962e 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -380,6 +380,8 @@ public enum IncludesModes { [CanBeNull] private TestGenerationOptions testGenOptions = null; public bool ExtractCounterexample = false; + public bool ShowProofObligationExpressions = false; + public bool AuditProgram = false; public static string DefaultZ3Version = "4.12.1"; @@ -796,6 +798,10 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p EnhancedErrorMessages = 1; return true; + case "showProofObligationExpressions": + ShowProofObligationExpressions = true; + return true; + case "testContracts": if (ps.ConfirmArgumentCount(1)) { if (args[ps.i].Equals("Externs")) { diff --git a/Source/DafnyCore/Generic/ReporterExtensions.cs b/Source/DafnyCore/Generic/ReporterExtensions.cs index 2c7db254918..579cea5939d 100644 --- a/Source/DafnyCore/Generic/ReporterExtensions.cs +++ b/Source/DafnyCore/Generic/ReporterExtensions.cs @@ -11,7 +11,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati var usingSnippets = reporter.Options.Get(Snippets.ShowSnippets); var relatedInformation = new List(); foreach (var auxiliaryInformation in error.Aux) { - if (auxiliaryInformation.Category == RelatedMessageCategory) { + if (auxiliaryInformation.Category == RelatedMessageCategory || auxiliaryInformation.Category == AssertedExprCategory) { error.Msg += "\n" + auxiliaryInformation.FullMsg; } else if (auxiliaryInformation.Category == RelatedLocationCategory) { relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets)); @@ -46,6 +46,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati private const string RelatedLocationCategory = "Related location"; public const string RelatedLocationMessage = RelatedLocationCategory; private const string RelatedMessageCategory = "Related message"; + public const string AssertedExprCategory = "Asserted expression"; public static readonly string PostConditionFailingMessage = new ProofObligationDescription.EnsuresDescription(null, null).FailureDescription; private static string FormatRelated(string related) { return $"Could not prove: {related}"; diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index f461a222ec1..ef7563b8a05 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -359,6 +359,12 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) { }; + public static readonly Option ShowProofObligationExpressions = new("--show-proof-obligation-expressions", () => false, + @" +(Experimental) Show Dafny expressions corresponding to unverified proof obligations.".TrimStart()) { + IsHidden = true + }; + static CommonOptionBag() { DafnyOptions.RegisterLegacyBinding(WarnAsErrors, (options, value) => { if (!options.Get(AllowWarnings) && !options.Get(WarnAsErrors)) { @@ -571,6 +577,10 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, options.EnhancedErrorMessages = 1; }); + DafnyOptions.RegisterLegacyBinding(ShowProofObligationExpressions, (options, value) => { + options.ShowProofObligationExpressions = value; + }); + DooFile.RegisterLibraryChecks( new Dictionary() { { UnicodeCharacters, DooFile.CheckOptionMatches }, @@ -635,7 +645,8 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, AddCompileSuffix, SystemModule, ExecutionCoverageReport, - ExtractCounterexample + ExtractCounterexample, + ShowProofObligationExpressions ); } diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index a0e8f66cb57..d482ab458f8 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -48,7 +48,8 @@ static DafnyCommands() { CommonOptionBag.NoTimeStampForCoverageReport, CommonOptionBag.VerificationCoverageReport, CommonOptionBag.ExtractCounterexample, - CommonOptionBag.ManualTriggerOption + CommonOptionBag.ManualTriggerOption, + CommonOptionBag.ShowProofObligationExpressions }.ToList(); public static IReadOnlyList