Check by default that all pure and ghost functions have termination measures #718
Conversation
| @@ -177,13 +178,15 @@ pure func Join(elems []string, sep string) (res string) /*{ | |||
| // HasPrefix tests whether the string s begins with prefix. | |||
| pure | |||
| ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix) | |||
| decreases _ | |||
There was a problem hiding this comment.
| decreases _ | |
| decreases |
There was a problem hiding this comment.
I think it would be good to be consistent, i.e., to use decreases _ for abstract functions and decreases (or an appropriate non-constant measure) for non-abstract functions
There was a problem hiding this comment.
I thought about using decreases and dismissed it because these functions are imported and re-verified in every client. It feels wasteful to reverify termination everywhere. Note that, while the same could be said about reverifying the body, including the definition of the function may be useful for clients (and, unfortunately, Gobra/Viper does not allow us to define a function without verifying its correctness).
Update: I guess that my answer still does not account for the inconsistency, considering that some functions in these libraries are checked for termination. I guess we should opt for one: either all functions in the standard library are assumed to terminate, or we check the termination of all of them. I will merge your suggestions for now, and later we may decide to remove all termination measures
There was a problem hiding this comment.
I'm not sure whether we already do that but we could in principle turn decreases measures for imported pure functions into wildcard measures to avoid the additional overhead of re-verifying termination. I'd rather do this within Gobra as opposed to these stubs such that we can still verify the stubs (and thus check that they actually terminate)
| } | ||
| val hasMeasureIfNeeded = config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty | ||
| val needsMeasureError = | ||
| error(member, "All pure functions must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) |
There was a problem hiding this comment.
| error(member, "All pure functions must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) | |
| error(member, "All ghost methods and pure functions must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) |
There was a problem hiding this comment.
While looking at this body, I thought that the error message only captures some of the cases but actually you're calling this function only for pure functions and methods. However, shouldn't we call this check also for ghost (impure) functions and methods?
There was a problem hiding this comment.
I would be happy to make that change as well if the rest agrees. Tbh, I did not even consider that; instead, I was concerned about guaranteeing that our specifications are always meaningful, which may not be the case if they refer to non-terminating pure functions
There was a problem hiding this comment.
I changed Gobra to now check termination on all ghost methods as well. This PR should be ready to merge as soon as the tests go through
Co-authored-by: Linard Arquint <[email protected]>
jcp19
changed the title
In the past, we run into unsoundnesses and tricky corner cases of Gobra because, so far, we were able to use non-terminating functions in specifications. This PR changes the default behaviour of Gobra to expect a termination measure in any pure function or method. Please let me know if you agree with this being the default behaviour. Notice that I did not adapt all of the current tests. This can be done but it would take more time than I am willing to spend atm.