fix: Use reveal_ constant as function argument in override axiom #5111
Conversation
| // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel. | ||
| // Instead, we do the next best thing: use the literal false. | ||
| reveal = new Boogie.LiteralExpr(f.tok, false); | ||
| reveal = GetRevealConstant(overridingFunction); |
There was a problem hiding this comment.
This sounds largely plausible to be the cause of the issue. Thanks for spotting!
| git-issue-5017b.dfy(44,14): Error: overridden predicate 'Valid' in 'M2' must be 'opaque' since the member is 'opaque' in trait 'C' | ||
| git-issue-5017b.dfy(66,14): Error: overridden predicate 'Valid' in 'Y0' must be 'opaque' since the member is 'opaque' in trait 'C' | ||
| git-issue-5017b.dfy(69,14): Error: overridden predicate 'Valid' in 'Y1' must be 'opaque' since the member is 'opaque' in trait 'C' | ||
| git-issue-5017b.dfy(94,13): Error: member 'reveal_Valid' does not exist in trait 'A' |
There was a problem hiding this comment.
I worried a bit about this issue. It seems that, to resolver it, one would need to implement this member, but the resolution is to actually. make Valid opaque in A. Could you detect that particular case and emit a more useful error message?
There was a problem hiding this comment.
Excellent idea. I improved many messages. However, it became more difficult for some of them. The problem is that, early on during resolution, we change reveal X(); expressions into reveal_X(); lemma calls. By the time that these attempted lemma calls go through the resolver, the name looked up is reveal_X. To improve the error message, we then have to detect that we're in a reveal-statement context and that the thing we're trying to look up has a name that starts with "reveal_" (which is not actually guaranteed to be one of the rewritten calls, since this could have been a user-defined name in the first place), and then remove the "reveal_" prefix, try to find what the name X might have referred to, and finally reconstruct the reason why no reveal_X lemma was created in the first place. It would have been much better not to have done the reveal_X-lemma surgery so early in the pipeline. Then, the symbol we'd be looking at during resolution would be X. (Btw, I've seen this mistake many times--a change is made too early in the resolution pipeline, because it seems as if that's a quick way to get a new feature into the language, but then this bites later on.)
Anyhow, I feel okay with the error messages I did improve. At some point in the future, I expect that we'll revisit reveal statements to expand their role. That would be a good time to handle reveal in a way that's less hacky than today's reveal_-lemmas.
| @@ -94,8 +94,7 @@ ExportResolve.dfy(288,39): Error: member 'u' has not been imported in this scope | |||
| ExportResolve.dfy(290,18): Error: type of corresponding source/RHS (G.Trait) does not match type of bound variable (object?) | |||
| ExportResolve.dfy(290,46): Error: type of corresponding source/RHS (G.Klass) does not match type of bound variable (object?) | |||
| ExportResolve.dfy(298,19): Error: member '_ctor' has not been imported in this scope and cannot be accessed here | |||
| ExportResolve.dfy(342,15): Error: unresolved identifier: reveal_OpaqueFunction | |||
| ExportResolve.dfy(342,29): Error: expression has no reveal lemma | |||
| ExportResolve.dfy(342,15): Error: cannot reveal 'OpaqueFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'OpaqueFunction' | |||
There was a problem hiding this comment.
Not blocking, but I thought it should not be an error but a warning. Otherwise, it makes experimenting with opaque to be hard.
Fixes #5017
Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types.
Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. Previously, this had caused a crash.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.