Skip to content

Commit

Permalink
Refactoring to support decreases to (#5315)
Browse files Browse the repository at this point in the history 
### Description

This is a refactoring-only PR intended to make implementing [`decreases
to`](#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.
  • Loading branch information
@atomb
atomb authored Apr 19, 2024
1 parent 44ca1b2 commit 846a2f6
Show file tree
Hide file tree
Showing 5 changed files with 76 additions and 24 deletions.
24 changes: 17 additions & 7 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,16 +33,15 @@ public partial class BoogieGenerator {
/// allowance || (calleeDecreases LESS contextDecreases).
/// </summary>
void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Expression> calleeDecreases,
Bpl.Expr allowance,
Expression allowance,
Expression receiverReplacement, Dictionary<IVariable, Expression> substMap,
Dictionary<TypeParameter, Type> 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
Expand All @@ -62,29 +61,40 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
var types1 = new List<Type>();
var callee = new List<Expr>();
var caller = new List<Expr>();
var oldExpressions = new List<Expression>();
var newExpressions = new List<Expression>();
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);
}
for (int i = 0; i < N; i++) {
Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap, typeMap);
Expression e1 = contextDecreases[i];
if (oldCaller) {
e1 = new OldExpr(e1.tok, e1) {
Type = e1.Type // To ensure that e1 stays resolved
};
}
if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
N = i;
break;
}
oldExpressions.Add(e1);
newExpressions.Add(e0);
toks.Add(new NestedToken(tok, e1.tok));
types0.Add(e0.Type.NormalizeExpand());
types1.Add(e1.Type.NormalizeExpand());
callee.Add(etranCurrent.TrExpr(e0));
caller.Add(etranInitial.TrExpr(e1));
caller.Add(etranCurrent.TrExpr(e1));
}
bool endsWithWinningTopComparison = N == contextDecreases.Count && N < calleeDecreases.Count;
Bpl.Expr decrExpr = DecreasesCheck(toks, types0, types1, callee, caller, builder, "", endsWithWinningTopComparison, false);
if (allowance != null) {
decrExpr = BplOr(allowance, decrExpr);
decrExpr = BplOr(etranCurrent.TrExpr(allowance), decrExpr);
}
builder.Add(Assert(tok, decrExpr, new PODesc.Terminates(inferredDecreases, false, hint)));
builder.Add(Assert(tok, decrExpr, new
PODesc.Terminates(inferredDecreases, null, allowance,
oldExpressions, newExpressions, hint)));
}

/// <summary>
Expand Down Expand Up @@ -347,4 +357,4 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
atmost = BplImp(b0, b1);
}
}
}
}
14 changes: 6 additions & 8 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -781,16 +781,14 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
List<Expression> contextDecreases = codeContext.Decreases.Expressions;
List<Expression> 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;
Expand Down Expand Up @@ -821,15 +819,15 @@ 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);
}
}
}
// all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(callExpr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool);
List<Bpl.Expr> 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) {
Expand Down
40 changes: 38 additions & 2 deletions Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1549,15 +1549,23 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
var toks = new List<IToken>();
var types = new List<Type>();
var decrs = new List<Expr>();
var oldDecreases = new List<Expression>();
var prevGhostLocals = new List<VarDeclStmt>();
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) {
Expand All @@ -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<CallCmd>(), 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<VarDeclStmt>, Expression) TranslateToLoopEntry(Specification<FrameExpression> mod, Expression e, string loopLabel) {
var prevGhostLocals = new List<VarDeclStmt>();
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);
Expand Down Expand Up @@ -1936,7 +1972,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
} else {
List<Expression> contextDecreases = codeContext.Decreases.Expressions;
List<Expression> 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);
}
}

Expand Down
14 changes: 11 additions & 3 deletions Source/DafnyCore/Verifier/ProofObligationDescription.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Expression> oldExpressions;
private readonly List<Expression> newExpressions;
private readonly List<VarDeclStmt> prevGhostLocals;

public Terminates(bool inferredDescreases, List<VarDeclStmt> prevGhostLocals, Expression allowance, List<Expression> oldExpressions, List<Expression> 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;
}
}
Expand Down
8 changes: 4 additions & 4 deletions ...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand Down

0 comments on commit 846a2f6

Please sign in to comment.