From 846a2f6159ca1c8cdce82b5684975eaa0d186538 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 19 Apr 2024 16:28:27 -0700 Subject: [PATCH] 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 31e18d6bde..836f650a29 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 96bbfcbaae..784c2ed116 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 23025289ac..2ea293d351 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 6c0c5460d5..eeb61c4999 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 a9c4bb828b..768491421f 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