fix: Add uniform checking of type characteristics in refinement modules #5146
Conversation
| type T(!new, ==) | ||
|
|
||
| twostate lemma L(new t: T) | ||
| ensures old(allocated(t)) // Uses the !new annotation on T |
There was a problem hiding this comment.
Since it's hard to view the expect file and this one at the same time, could you clarify if this is a warning or an error?
| @@ -0,0 +1,35 @@ | |||
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T', type synonym 'OpaqueType.T' must support the type characteristic "no references" | |||
There was a problem hiding this comment.
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T', type synonym 'OpaqueType.T' must support the type characteristic "no references" | |
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T' declared `(!new)`, type synonym 'OpaqueType.T' must contain no references |
There was a problem hiding this comment.
Great suggestions about the wording of the error messages. I have made the changes.
| @@ -0,0 +1,35 @@ | |||
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T', type synonym 'OpaqueType.T' must support the type characteristic "no references" | |||
| git-issue-2064.dfy(14,9): Error: to be a refinement of abstract type 'UnitTestParent.U', type synonym 'OpaqueType.U' must support the type characteristic "equality" | |||
There was a problem hiding this comment.
| git-issue-2064.dfy(14,9): Error: to be a refinement of abstract type 'UnitTestParent.U', type synonym 'OpaqueType.U' must support the type characteristic "equality" | |
| git-issue-2064.dfy(14,9): Error: to be a refinement of abstract type 'UnitTestParent.U' declared `(==)`, type synonym 'OpaqueType.U' must support equality |
| @@ -0,0 +1,35 @@ | |||
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T', type synonym 'OpaqueType.T' must support the type characteristic "no references" | |||
| git-issue-2064.dfy(14,9): Error: to be a refinement of abstract type 'UnitTestParent.U', type synonym 'OpaqueType.U' must support the type characteristic "equality" | |||
| git-issue-2064.dfy(15,9): Error: to be a refinement of abstract type 'UnitTestParent.V', type synonym 'OpaqueType.V' must support the type characteristic "auto-initialization" | |||
There was a problem hiding this comment.
| git-issue-2064.dfy(15,9): Error: to be a refinement of abstract type 'UnitTestParent.V', type synonym 'OpaqueType.V' must support the type characteristic "auto-initialization" | |
| git-issue-2064.dfy(15,9): Error: to be a refinement of abstract type 'UnitTestParent.V' declared `(0)`, type synonym 'OpaqueType.V' must support auto-initialization |
| git-issue-2064.dfy(13,9): Error: to be a refinement of abstract type 'UnitTestParent.T', type synonym 'OpaqueType.T' must support the type characteristic "no references" | ||
| git-issue-2064.dfy(14,9): Error: to be a refinement of abstract type 'UnitTestParent.U', type synonym 'OpaqueType.U' must support the type characteristic "equality" | ||
| git-issue-2064.dfy(15,9): Error: to be a refinement of abstract type 'UnitTestParent.V', type synonym 'OpaqueType.V' must support the type characteristic "auto-initialization" | ||
| git-issue-2064.dfy(16,9): Error: to be a refinement of abstract type 'UnitTestParent.W', type synonym 'OpaqueType.W' must support the type characteristic "nonempty" |
There was a problem hiding this comment.
| git-issue-2064.dfy(16,9): Error: to be a refinement of abstract type 'UnitTestParent.W', type synonym 'OpaqueType.W' must support the type characteristic "nonempty" | |
| git-issue-2064.dfy(16,9): Error: to be a refinement of abstract type 'UnitTestParent.W' declared `(00)`, type synonym 'OpaqueType.W' must be provably non-empty |
There was a problem hiding this comment.
I changed it to "be nonempty". Do you think I should also include "provably" (which may suggest verification, and which may be inconsistent with the other type characteristics)? Another possibility would be "be declared nonempty". (Thinking about these possibilities, I vote for "be nonempty", but don't feel strongly and would be happy to change again, if you suggest.)
There was a problem hiding this comment.
"be nonempty" is good, since 0 could be an auto-inferred witness. We can omit the "provably" because the requirement is not a proof from the engineer's perspective, it's an expression at the declaration site (even though providing an element for a given type is like giving a proof :-) ).
| git-issue-2064.dfy(76,9): Error: to be a refinement of abstract type 'UnitTestParent.V', type synonym 'Class.V' must support the type characteristic "auto-initialization" | ||
| git-issue-2064.dfy(77,9): Error: to be a refinement of abstract type 'UnitTestParent.W', type synonym 'Class.W' must support the type characteristic "nonempty" | ||
| git-issue-2064.dfy(81,10): Error: to be a refinement of abstract type 'UnitTestParent.T', class 'ClassDirect.T' must support the type characteristic "no references" | ||
| git-issue-2064.dfy(83,10): Error: to be a refinement of abstract type 'UnitTestParent.V', class 'ClassDirect.V' must support the type characteristic "auto-initialization" |
There was a problem hiding this comment.
| git-issue-2064.dfy(83,10): Error: to be a refinement of abstract type 'UnitTestParent.V', class 'ClassDirect.V' must support the type characteristic "auto-initialization" | |
| git-issue-2064.dfy(83,10): Error: to be a refinement of abstract type 'UnitTestParent.V' declared `(0)`, class 'ClassDirect.V' would need to support auto-initialization, which non-null objects do not support - you might want to refine `type V = ClassName?" for your class, so that `null` can be used to auto-initialize the type `V` |
Otherwise, the question our user would have is "then how do I make my class auto-initialize" which is a dead end :-)
There was a problem hiding this comment.
I did not act on this suggest or the next two. These three suggestions would apply if the refinement module use a type synonym and the RHS of that type synonym is a type for which we can offer a hint. While I do like error messages that suggest what to do, I'm unconvinced these hints are worth the added logic in the Dafny implementation. But if you insist on these hints, push back and I'll reconsider.
There was a problem hiding this comment.
Strike that.
I added some text to the How-To FAQ. For example, I added the ClassName? suggestion there.
| git-issue-2064.dfy(77,9): Error: to be a refinement of abstract type 'UnitTestParent.W', type synonym 'Class.W' must support the type characteristic "nonempty" | ||
| git-issue-2064.dfy(81,10): Error: to be a refinement of abstract type 'UnitTestParent.T', class 'ClassDirect.T' must support the type characteristic "no references" | ||
| git-issue-2064.dfy(83,10): Error: to be a refinement of abstract type 'UnitTestParent.V', class 'ClassDirect.V' must support the type characteristic "auto-initialization" | ||
| git-issue-2064.dfy(84,10): Error: to be a refinement of abstract type 'UnitTestParent.W', class 'ClassDirect.W' must support the type characteristic "nonempty" |
There was a problem hiding this comment.
| git-issue-2064.dfy(84,10): Error: to be a refinement of abstract type 'UnitTestParent.W', class 'ClassDirect.W' must support the type characteristic "nonempty" | |
| git-issue-2064.dfy(84,10): Error: to be a refinement of abstract type 'UnitTestParent.W' declared `(00)`, class 'ClassDirect.W' must provably be non-empty, which is not possible for objects - you might want to refine `type V = ClassName?` so that `null` is a proof `V` is not empty |
| EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype | ||
| EqualityTypes.dfy(35,11): Error: type 'Y', which does not support equality, is used to refine an abstract type with equality support | ||
| EqualityTypes.dfy(34,13): Error: to be a refinement of abstract type 'C.X', codatatype 'E.X' must support the type characteristic "equality" | ||
| EqualityTypes.dfy(35,11): Error: to be a refinement of abstract type 'C.Y', datatype 'E.Y' must support the type characteristic "equality" |
There was a problem hiding this comment.
| EqualityTypes.dfy(35,11): Error: to be a refinement of abstract type 'C.Y', datatype 'E.Y' must support the type characteristic "equality" | |
| EqualityTypes.dfy(35,11): Error: to be a refinement of abstract type 'C.Y' declared `(==)`, datatype 'E.Y' must support equality, e.g. all its type parameters and its field types must support equality |
| if (!CheckCharacteristics(formal.Characteristics, actual, inGhostContext, out var whatIsWrong, out var hint)) { | ||
| reporter.Error(MessageSource.Resolver, tok, "type parameter{0} ({1}) passed to {2} {3} must support {4} (got {5}){6}", | ||
| actualTypeArgs.Count == 1 ? "" : " " + i, formal.Name, what, className, whatIsWrong, actual, hint); | ||
| if (!CheckCharacteristics(formal.Characteristics, actual, inGhostContext, out var whatIsNeeded, out var hint)) { |
There was a problem hiding this comment.
Excellent philosophical renaming of a variable! Good error messages always indicate how to fix them, not that the user did wrong :-)
docs/HowToFAQ/Errors-Refinement.md
Outdated
|
|
||
| ## **Error: type '_name_', which does not support equality, is used to refine an abstract type with equality support** {#ref_mismatched_type_equality_support} | ||
| ## **Error: to be a refinement of _kind_ '_name_' declared with (!new), _kind_ '_name_' must contain no references {#ref_mismatched_type_characteristics} |
There was a problem hiding this comment.
IDs declared in curly braces must be unique. Could you either regroup these sections together (so that the user knows there is no other section with the same ID), or make separate error IDs in the code? I'm fine with both, although I'd slightly prefer the second since you worked hard on making each example unique.
If a module
Mdeclares an abstract typeTwith specific type characteristics, then any module that refinesMand replacesTmust make sure that the newTlives up to those type characteristics. Some of those checks were missing. This PR adds them for all replacements ofT.Also, previously, some of the checks that were performed were stronger than necessary. For example, they did not allow
M.T(00)to be refined by a type that satisfies(0). This PR makes those checks less forceful.Implementation-wise, the previous checks were done by looking at the specific type declarations in the refinement module. This is a bad idea, since it does not make use of the standard mechanisms in the Dafny resolver to figure out what type characteristics a given type supports. This PR fixes that by calling the standard
CheckCharacteristicsmethod.Fixes #2064
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.