Refactoring to support decreases to
#5315
Conversation
atomb
changed the title
decreases todecreases to
There was a problem hiding this comment.
The computation of the oldExpr for the decreases clause of the loop requires one fix. Since the PR claims to be a refactoring, we could leave out the computation of the oldExpr for this PR and add it to the next where I guess you'll add a thoroughly tested proof obligation description?
| 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) { |
There was a problem hiding this comment.
Nice conversion from Boogie to Dafny.
| 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)); |
There was a problem hiding this comment.
It feels soo good to see Dafny expressions here. It will surely be helpful for making assertions explicit, but also possibly to consider another proving back-end.
There was a problem hiding this comment.
Yeah, I entirely agree. I sort of hope we can get to the point where every assertion in Boogie is a translation of an assertion in Dafny (which is perhaps synthetically constructed along the way). But that'll be a lot of refactoring, likely with significant impact on the shape of verification conditions and therefore brittleness.
| var olde = new OldExpr(e.tok, e, "LoopEntry") { | ||
| Type = e.Type | ||
| }; | ||
| oldDecreases.Add(olde); |
There was a problem hiding this comment.
Wrapping the decreases expression with old seems like it would work, but the only problem with that is that it does not work for local variables, i.e. old() is currently only taking the old heap for references, but not for stack variables.
Ideally, you should also traverse "e" and replace all modified local variables (like k) by new ghost identifiers (like prev_k), and store the mapping in the PODesc so that the proof obligation description could describe not only the assertion of the decreases, but also the additional ghost assignments that need to be done at the beginning of the loop (ghost var prev_k := k;)
| @@ -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); | |||
There was a problem hiding this comment.
We are lucky that it's the only difference. Since a Dafny literal is wrapped with Lit, I thought that creating a Dafny expression instead of a Boogie expression would create more differences.
Hopefully it's negligible for verification.
There was a problem hiding this comment.
Yeah, I was expecting that might happen, too. I also think this change will be reverted when we merge #4596.
Description
This is a refactoring-only PR intended to make implementing
decreases tomore 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.