Skip Termination Checks for Imported (Pure) Functions & Methods#546
Skip Termination Checks for Imported (Pure) Functions & Methods#546
Conversation
|
I should maybe add that changing the termination measures should not be problematic because mutual recursion is impossible due to the acyclic nature of imports and therefore the call graph analysis performed by Viper does not result in wrong results |
| // when parsing imported packages (`specOnly` will be true), we trust the annotations of imported members | ||
| // therefore, e.g. bodies of non-pure functions & methods will be ignored. However, the body of pure | ||
| // functions & methods is retained. To avoid that Viper will generate proof obligations for checking termination | ||
| // of imported pure functions & methods, we simply translate tuple termination measures into wildcard measures (for | ||
| // a given condition). Therefore, no proof obligations will be created for checking termination of imported members. | ||
| // This is technically not necessary for imported non-pure functions & methods because they are abstract | ||
| // anyway but we apply the same transformation for simplicity as we do not have to perform a case distinction on | ||
| // whether the termination measure is part of a pure or non-pure member. |
There was a problem hiding this comment.
I wonder what happens if you import an interface whose methods have a termination measure. Do we change their termination measures to a wildcard then? If so, this sounds unsound to me, as one can still implement that interface in the importing package
There was a problem hiding this comment.
Very good point and you're absolutely right!
I've now adapted the approach to only adapt termination measures for method and function declarations. Since detecting this context within the parser seemed too hacky to me, I've added another parse tree postprocessor
There was a problem hiding this comment.
It seems to me that adapting the termination measure can improve performance but we still need to prove that the body satisfies the postcondition, which is probably the part that takes the longest. I am wondering if instead of rewriting the termination measure, we can have some transformation like:
pure
requires P
ensures Q
decreases X
func f(...) (res T) {
return body
}
==>
pure
requires P
ensures Q
ensures res === body // new postcondition
decreases X
func f(...) (res T)
This way, we do not have to reverify the body and we do not need to conditionally rewrite the termination measure.
There was a problem hiding this comment.
I have implemented your suggestion. However, I'm still turning decreases tuples into wildcards because Viper also checks whether postconditions terminate
There was a problem hiding this comment.
I would be carefull with that rewrite. If the function is recursive, then body would contain a call to itself which I vaguely remember to be unsound in Viper right now. Maybe ask Marco, Gaurav, or Thibault there.
There was a problem hiding this comment.
(As you might saw) I asked people, and I misremembered the problem: The problem are matching loops. For instance, the following program verifies:
function bar(x: Int): Int
ensures result == (x > 0 ? x + bar(x-1) : 0)
method test() {
assert bar(98) == 4851
}
Therefore, this part of the transformation should be removed.
There was a problem hiding this comment.
FYI there is some global bound on the unrollings and 98 is the most that is possible in the example. The following programs does not verify because of that (which makes a nice riddle):
function bar1(x: Int): Int
ensures result == (x > 0 ? x + bar1(x-1) : 0)
function bar2(x: Int): Int
ensures result == (x > 0 ? x + bar2(x-1) : 0)
method test() {
assert bar1(98) == 4851
assert bar2(1) == 1
}
|
I have to correct my statement from yesterday: The reduction in Viper code size is minimal and I do not see a difference in verification time unfortunately. @jcp19 you were right that the termination proofs I was seeing are coming from the implementation proofs. I'll have look at that next but in a separate branch |
jcp19
left a comment
There was a problem hiding this comment.
Looks good; I wonder if we could easily introduce unit tests for the termination postprocessor
Felalolf
left a comment
There was a problem hiding this comment.
In a comment in an existing thread I wrote that there might be a problem with the postcondition tranformation.
| def getBodyExpr(body: Option[(PBodyParameterInfo, PBlock)]): Option[PExpression] = body match { | ||
| case Some((_, block)) => | ||
| block.nonEmptyStmts match { | ||
| case Vector(PReturn(Vector(expr))) => Some(expr) | ||
| case _ => | ||
| failedNodes = failedNodes ++ createError(block, s"the imported pure function's or method's body is expected to contain only a return statement") | ||
| None | ||
| } | ||
| case None => None | ||
| } |
There was a problem hiding this comment.
Here and for getOutParam we duplicate checks, which add a bit of difficulty for maintenance as both these checks have to synced and might weaken in the future. I propose to add a comment to the other versions of these checks referencing the methods in this file, so that we do not forget that they are linked.
|
@Felalolf Thanks for your inputs! I've now removed the transformation of bodies such that only termination tuples are turned into wildcard termination measures (to avoid termination proof obligations) while keeping the rest of pure functions & pure methods as is |
|
This PR is currently blocked by Silver PR #618 extending the termination plugin to fix the CI errors |
…uch that no proof obligations will be emitted
…nctions and methods untouched
…rmination plugin's integration to emit the wellfounded order domain if at least one decreases tuple occurs in the program
5fd6eb4 to
8915a65
Compare
|
|
|
is this ready to be merged then? @ArquintL |
|
Yes |
The parser throws away the body of non-pure functions & methods. This correctly results in skipping the proof obligations as we assume that imported packages have been verified and thus we blindly trust their specification.
However, in the case of pure functions & methods, the body is retained. This PR transforms termination measures for imported members such that Viper skips creating proof obligations for checking termination.