feat: Generate a warning when 'old' has no effect #2610
Conversation
# Conflicts: # RELEASE_NOTES.md
|
Thanks for implementing this! |
|
Could you resolve the conflicts with master? |
# Conflicts: # RELEASE_NOTES.md # Source/Dafny/Resolver.cs # Source/Dafny/Verifier/Translator.cs
| @@ -10622,6 +10624,8 @@ public enum FrameExpressionUse { Reads, Modifies, Unchanged } | |||
| void CreateIteratorMethodSpecs(IteratorDecl iter) { | |||
| Contract.Requires(iter != null); | |||
|
|
|||
| var tok = new AutoGeneratedToken(iter.tok); | |||
There was a problem hiding this comment.
Could we run 'the old has no effect' detection after we generate the iterator method specs? This works as well, but I'm curious what the best ordering of operations is. Maybe CreateIteratorMethodSpecs should not be part of the main resolution phase, but instead be part of the code-gen phase?
Can FreeVariableUtil.ComputeFreeVariables not be called before resolution? Maybe we should specify that in a comment on the before.
Side note: the AutoGeneratedToken concept seems strange to me. In generated code I wouldn't expect warnings/errors, and I wouldn't expect any non-nullish tokens there.
There was a problem hiding this comment.
The linter is run after resolution. At that time (and not before that time), we have information about heap usage and variable definitions. For example, we know whether s[i] is referring to a sequence element or an array element. The free-variable machinery already has the ability to detect heap usage, so it made sense to call it from the linter.
There are a number of desugaring tasks (match, datatype update, iterators, ...) that are being done quite early. Creating new AST nodes is easier pre-resolution, because then the resolution pass will fill in type information. To my taste, some of that desugaring is done too early, or perhaps shouldn't be done at all. It would be good to have a discussion and redesign of all of that sometime. But for iterators, the desugaring does need to be done early, because the iterator desugaring introduces names that the program is allowed to call. So, this means iterator desugaring is necessarily done before the linter runs.
One could consider making the iterator desugaring more clever, so that it never generates useless old expressions. But this is difficult to determine before resolution (cf. my s[i] example above).
Therefore, to avoid linter warnings from such generated code, we need some way to keep track of which expressions have been automatically generated. We already had a mechanism for this, which is to put some information into the tokens. This is not perfect, and I'm not sure that we're using nested token wrappers correctly. For linter warnings, any such imperfections seem okay, since at worst we'd generate bad warnings or omit some warnings.
There was a problem hiding this comment.
Thanks for the info. This approach seems good :)
Source/Dafny/Linter.cs
Outdated
|
|
||
| namespace Microsoft.Dafny { | ||
|
|
||
| class Linter : IRewriter { |
There was a problem hiding this comment.
Please use a more specific name while this class does a specific thing.
# Conflicts: # RELEASE_NOTES.md
|
Added a sentence in the RM about this warning. |
|
Does this solve #320 as well? |
Depends on PRs #2606 and #2607
Fixes #1989
If the argument to
oldhas no dereferences of the mutable heap, generate a warning saying that theoldhas no effect. This has been a common source of errors and confusion.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.