Feat: @-attributes on top-level declarations #5825
Conversation
MikaelMayer
force-pushed
the
feat-at-attributes-1
branch
from
676d245
to
953489e
Compare
MikaelMayer
force-pushed
the
feat-at-attributes-1
branch
from
988fa07
to
b6dcbcb
Compare
Makefile
Outdated
| @@ -12,6 +12,7 @@ exe: | |||
|
|
|||
| format-dfy: | |||
| (cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .) | |||
| (cd "${DIR}"/Source/DafnyStandardLibraries ; ../../Binaries/Dafny.exe format .) | |||
There was a problem hiding this comment.
FYI there's a make format target already for DafnyStandardLibraries which is slightly different (and I think more platform-independent)
Source/DafnyCore/AST/Attributes.cs
Outdated
| } | ||
|
|
||
| // Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute | ||
| // or mark i as not built-in for later resolution |
There was a problem hiding this comment.
| // or mark i as not built-in for later resolution | |
| // or mark it as not built-in for later resolution |
| @@ -134,7 +137,7 @@ public override string ToString() { | |||
|
|
|||
| // For Boogie | |||
| internal VerificationIdGenerator IdGenerator = new(); | |||
| public override IEnumerable<INode> Children => (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()); | |||
| public override IEnumerable<INode> Children => Enumerable.Empty<INode>(); // Attributes should be enumerated by the parent, as they could be placed in different places | |||
There was a problem hiding this comment.
Attributes are a chained list such that {:a} {:b} {:c} is converted into Attribute{Name="c", Prev=Attribute{Name="b", Prev=Attribute{Name = "a", Prev = null } } }
As such, it made sense and was acceptable that the last attribute {:c} is one of the children nodes of the declaration, and is itself a parent of {:b} which is itself a parent of {:a}. As such, the Start of both {:c} and {:b} are {:a}, which is ok but weird.
Now, these new @-attributes are stored in the same linked list, except they are placed usually a few keywords away, like
@IsolateAssertion method {:oldATtribute} Test().
so that would mean that the last attribute's span, {:oldAttribute}, starts at @IsolateAssertion. This is not acceptable for formatting as every token in a span not covered by a child belongs to the node, so the attribute would capture method. That is not acceptable. Moreover, now every attribute is positioned differently depending on its syntax.
With this change, attributes are no longer a single child under a declaration, but each attribute becomes an indpendent child, so that there is no conflict at all.
| @@ -2009,7 +2009,8 @@ public QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) { | |||
| // omit the extern attribute when /noExterns option is specified. | |||
| (name is "extern" && options.DisallowExterns) || | |||
| (name is "timeLimit" && hasNewTimeLimit) || | |||
| (name is "rlimit" && hasNewRLimit) | |||
| (name is "rlimit" && hasNewRLimit) || | |||
| (attr is UserSuppliedAtAttribute) | |||
There was a problem hiding this comment.
I like the side effect that all of the new-style attributes are not based to Boogie by default, so we have to consciously translate them to Boogie when needed.
| // This list could be obtained from parsing and resolving a .Dfy file | ||
| // but for now it's good enough. |
There was a problem hiding this comment.
Agreed, but it would be really nice to have a Dafny source file somewhere with these defined, just for documentation. Possibly even included in the reference manual.
| ResolveExpression(arg, resolutionContext); | ||
| if (prevCount == reporter.ErrorCount && attr is UserSuppliedAtAttribute { Builtin: false }) { | ||
| reporter.Error(MessageSource.Resolver, attr.tok, "User-supplied @-Attributes not supported yet"); |
There was a problem hiding this comment.
Is it possible to hit this or is this just forwards-compatible defensive programming?
There was a problem hiding this comment.
It's not possible to hit this yet, but if someone added the ability to define custom attributes, it would be hit. I'll add this ability later and update this error reporting one, so it's forwards-compatible defensive programming, good guess! It decreases a bit code coverage but I think it's worth it. Also, it's to let you know where user-supplied @-attributes will be actually tested to have the @Attribute attribute.
| /// </summary> | ||
| public void CheckNoAttributes(ref Attributes attrs) { | ||
| if (attrs != null) { | ||
| SemErr(ErrorId.p_extra_attributes, attrs.RangeToken, "Attribute not expected here"); |
There was a problem hiding this comment.
I can't test it for now because the way parsing code is generated, it's unreachable, but on the next update of the grammar there will be cases and this will be tested.
Source/DafnyCore/AST/Attributes.cs
Outdated
| } | ||
| private static string TupleItem0Name => "0"; | ||
| // Helper to create a built-in @-attribute | ||
| static BuiltInAtAttributeSyntax B(string name) { |
There was a problem hiding this comment.
I'd make the names just a bit longer for readability, e.g. BuiltIn
| // List of built-in @-attributes with their definitions. | ||
| // This list could be obtained from parsing and resolving a .Dfy file | ||
| // but for now it's good enough. | ||
| public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() { |
There was a problem hiding this comment.
I think we really want to define the rules for where it is valid to apply these attributes too. Otherwise users might put them in the wrong place and not realize they have no effect.
There was a problem hiding this comment.
I think we want to do this, but it's another incremental improvement that we should thoroughly discuss.
We need to think of
- Defining clear attribute application categories
- How to organize attribute constructors in a datatype categories
- How to organize traits to regroup attributes based on where they can be applied
- And for that the new resolver should work on all the test cases. It does not work yet on DafnyCore so I don't think we should have datatypes that extend traits at this point.
I leave this out of scope for now.
There was a problem hiding this comment.
@robin-aws the most basic way to do this is with a enumeration that defines a lot of locations like "Expression","Class","Trait","Method", etc.. but that does not feel very powerful or maintainable to me, since you're exposing part of Dafny's internals.
I wonder whether a better approach would be:
- Let every attribute specify to which command(s) it applies:
dafny verifyordafny translate java, etc.. - If an attribute applies to the command currently executing, require it to be handled during resolution, either by our code or by a plugin. (every attribute could just have a
bool Handledproperty). If an attribute is not handled, emit a warning. - Let the handlers report warnings/errors if attributes are placed incorrectly.
There was a problem hiding this comment.
I leave this out of scope for now.
I would not, because if it's left out of scope users could put these new attributes in the wrong place and not realize they have no effect (which is just as bad as misspelling {:tailrecursion} now). Then if we want to add the restriction later we'll break their code.
the most basic way to do this is with a enumeration that defines a lot of locations like "Expression","Class","Trait","Method", etc.. but that does not feel very powerful or maintainable to me, since you're exposing part of Dafny's internals.
It's not exposing internals though, it's just naming types of declarations in the language. C# has exactly that kind of enumeration too: https://learn.microsoft.com/en-us/dotnet/api/system.attributetargets?view=net-8.0
There was a problem hiding this comment.
It's not exposing internals though, it's just naming types of declarations in the language. C# has exactly that kind of enumeration too
I know and that's exactly what I meant. I don't like their approach because the list seems arbitrary and makes it more difficult to evolve the language. Would Dafny have different enum elements for Lemma,Function,Method,Predicate, Extreme variants..., Or would you have a single Callable ?
There was a problem hiding this comment.
I would imitate what they are doing as well. I think you need to be more specific to catch misuse: e.g. @TailRecursion applies to functions but not say methods, so the attribute should specify that.
IMO adding a new type of attribute-able program element is going to involve a lot of documentation updates anyway, I don't think adding a new AttibuteTarget enum value is much more cost (although we should be careful to make sure we can do that without breaking existing attributes).
There was a problem hiding this comment.
@robin-aws The enum based approach does not make sense to me because it only provides simplistic checking and requires ambiguous choices on granularity. What do you prefer about the enum approach over the command one I sketched above?
There was a problem hiding this comment.
I like the fact that it's self-documenting, and catches errors as early as possible (during resolution rather than translation for e.g.). Without it, there's more work for each attribute handler to do, even if it's just setting your bool Handled property to true. Plus the error message if an attribute is not handled has to be more vague, because it doesn't know why it wasn't handled.
We can always make the default AllTargets, and handlers can implement their own more precise conditions if they need to.
Since this is out-of-scope for this PR I think we can have a separate design discussion about this point.
Source/DafnyCore/AST/Attributes.cs
Outdated
| .WithArg("low", Type.Int, DefaultInt(1)) | ||
| .WithArg("high", Type.Int, DefaultInt(2)) | ||
| .WithArg("functionName", Type.ResolvedString(), DefaultString("")), | ||
| B("Induction"), // Resolution is different |
There was a problem hiding this comment.
I would leave this one out in the first batch, for two reasons:
- I don't think this should be a single datatype constructor, I imagine it as something like
datatype Induction = NoInduction | InductionByAllVariables | InductionBy(???) - I don't know how to declare a list of bound variables as an argument to a datatype constructor.
We may not ever want to support this as an @-attribute.
There was a problem hiding this comment.
I like the rule that attribute arguments must be resolve-able without knowing which attribute it is, so purely based on the location in which the attribute occurs, which would likely mean @Trigger can not be an attribute.
There was a problem hiding this comment.
I included @Trigger in the first batch because I want us to have a discussion and clear agreement about it before I continue, so thanks for bringing this to me.
As of today, {:induction] and {:trigger} are the only attributes which can't reasonably considered datatype constructors, because although their input needs to be resolved, they can have any number of arguments, their arguments can be of any type, and the arguments are not used for their literal values but for names and patterns.
{:Induction} takes a set of variables in scope, like the assigned() ghost construct. It won't accept any expression, but it can accept an unbounded number of variables. We can't enforce this in the Dafny language itself as you remarked in your 2., @robin-aws .
Similarly, {:trigger} has to take patterns with variables that are in the scope, and all its values must have a type but it could be whatever type.
As a recall, the goals when having new attributes were the following
- Make sure our users don't mistype a name (e.g. type
{:triggers}instead of{:trigger}) - Make sure arguments to attributes have an expected type
- Open up the ability for user to define their own typed attributes.
- Make it possible to migrate entirely to the new @-attribute syntax so that we don't have any more inline attributes, that are sometimes ambiguous where to place (like
{:trigger}) only prefix attributes.
That attributes be datatypes constructors felt the right choice as illustrated that we chose the PascalCase, regular constructor call syntax and even parameter naming when appropriate. I had then searched for ways to encode the special attributes {:induction} and {:trigger} but found none reasonable given the special nature of these constructors.
Hence, for built-in attributes, the idea attribute = datatype constructor gives no reasonable way to satisfy goal 4.
Fortunately, I've found that relaxing that initial idea, i.e. not resolving @Induction and @Trigger as datatypes constructors but only their name and their arguments, given their nature, makes it possible to satisfy all four goals at once. Since these two attributes have always been exceptions, these PRs is not changing this when including them in the new style syntax.
Moreover, having now implemented Robin's request here, it even feels more ok to me now that built-in attributes can be more flexible than datatypes constructors at least in two cases, as they are not reported as such.
Note that errors on user-defined attributes will still be reported as "datatype constructors", as their definition will be in scope.
I like the rule that attribute arguments must be resolve-able without knowing which attribute it is, so purely based on the location in which the attribute occurs, which would likely mean @trigger can not be an attribute.
The upcoming resolution of the @Trigger attribute does resolve attribute arguments purely based on the location in which the attribute occurs, thanks to the rewriting phase. Would you like to explain a bit more your thoughts? I'd love to understand better.
There was a problem hiding this comment.
Make it possible to migrate entirely to the new @-attribute syntax so that we don't have any more inline attributes, that are sometimes ambiguous where to place (like {:trigger}) only prefix attributes.
Moving away from old-style attributes doesn't mean everything they supported needs to be supported by @-attributes, right? We can have custom syntax for :trigger and :induction.
I think it could cause unnecessary migration effort if we first release @trigger and @induction, and then later replace those with custom syntax.
it even feels more ok to me now that built-in attributes can be more flexible than datatypes constructors at least in two cases
It feels wrong to me. If it doesn't behave like all the other attributes, why is it an attribute to begin with?
There was a problem hiding this comment.
Moving away from old-style attributes doesn't mean everything they supported needs to be supported by @-attributes, right?
I think that, as a user of a programming language, I would expect any new language feature that seems to aim at replacing another language feature to give me more, if not as many, ways to express what was possible to express before, but not less.
I think it could cause unnecessary migration effort if we first release https://github.com/trigger and https://github.com/induction, and then later replace those with custom syntax.
What custom syntax do you think of?
I just came to realize that the arguments of attributes is not a value, but it's an abstract syntax tree of a value. We want this abstract syntax tree to be typed for all attributes, of course. Moreover, except for induction and triggers, we also want the arguments to be literals. This was never a requirement for datatype constructors, so it's one more difference between attributes and constructors. We can't accept @Compile(true || false) although that would be acceptable as an expression given the expected type.
Therefore, I just added this error handling in the latest commit so the user knows these attributes can only use literals for now, but again this is not necessary nor desirable for induction and trigger.
There was a problem hiding this comment.
I think that, as a user of a programming language, I would expect any new language feature that seems to aim at replacing another language feature to give me more, if not as many, ways to express what was possible to express before, but not less.
Who says @ attributes aim to replace all {: attributes?
What custom syntax do you think of?
Instead of {:trigger x,y,z} you would write trigger x,y,z
| public class Attributes : TokenNode { | ||
| // Syntax of a formal of a built-in @-attribute | ||
| // To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg() | ||
| public record BuiltInAtAttributeArgSyntax( |
There was a problem hiding this comment.
This is perfect right now, but I'm curious about the future as well. If we add support for user defined @ attributes, should those behave exactly the same as predefined attributes? In that case, I would expect this record to be replaced by usages of the existing Datatype AST type.
There was a problem hiding this comment.
You mean, that instead of these records, that we would have a tree with a datatype declaration and datatype constructors direclty?
I think that's indeed the next step before one day being able to refactor them to another file that might be parsed in a prelude. That way, documentation, jumping to definition and other IDE interactions will be easier.
The builder pattern I wrote can be used for that as well.
For now, I like the idea of not touching the user's program yet by injecting definitions.
There was a problem hiding this comment.
You mean, that instead of these records, that we would have a tree with a datatype declaration and datatype constructors direclty?
I mean that we'd define the attributes in a .dfy file and they'd get parsed into DatatypeDecl and DatatypeCtor values.
| } | ||
|
|
||
| public BuiltInAtAttributeSyntax Filter(Func<IAttributeBearingDeclaration, bool> canBeApplied) { | ||
| return this with { CanBeApplied = canBeApplied }; |
There was a problem hiding this comment.
TIL C# supports this now, cool! Must have stolen it from Dafny's m[k := v] :)
| at-attributes-typos.dfy(12,15): Error: incorrect argument type for attribute parameter '0' (expected bool, found string) | ||
| at-attributes-typos.dfy(28,0): Error: @Fuel attribute cannot be applied to method | ||
| at-attributes-typos.dfy(42,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) | ||
| at-attributes-typos.dfy(22,0): Error: @Fuel attribute cannot be applied to datatype |
There was a problem hiding this comment.
Great, thanks for adding the filtering. This is good enough for now, but in the next iteration let's be more precise and helpful: "@fuel can only be applied to functions, but Useless is a datatype"
(that will require modeling the filter as a subset of attribute-able program elements of course, instead of a free-form predicate)
Source/DafnyCore/AST/Attributes.cs
Outdated
| .WithArg("functionName", Type.ResolvedString(), DefaultString("")) | ||
| .Filter(attributeHost => attributeHost is Function), | ||
| BuiltIn("IsolateAssertions") | ||
| .Filter(attributeHost => attributeHost is MemberDecl), |
There was a problem hiding this comment.
Does this have an effect on Fields? Shouldn't it be MethodOrFunction instead?
There was a problem hiding this comment.
Yes it has an effect on constant fields with a RHS because the RHS might have some well formedness to be proved.
But I realize it should also support type with witnesses since there is a well-formedness check for them, and datatypes since parameters have default values. Same for newtypes.
There was a problem hiding this comment.
Consider changing to attributeHost is ICanVerify
docs/dev/news/at-attributes.feat
Outdated
| @@ -0,0 +1 @@ | |||
| Support for Top-level @-attributes | |||
There was a problem hiding this comment.
I would link to the reference manual section for more details.
docs/DafnyRef/Attributes.md
Outdated
| @@ -32,6 +33,19 @@ overrides those further away. | |||
| For attributes with a single boolean expression argument, the attribute | |||
| with no argument is interpreted as if it were true. | |||
|
|
|||
| ** Migration notes: ** There is a new syntax for typed attributes that is being added: `@Attribute(...)`, and these attributes are going to be prefix attributes. For now, the new syntax works only as top-level declarations. When all previous attributes will be migrated, this section will be rewritten. | |||
There was a problem hiding this comment.
I would include a quick code example of what using one of these attributes looks like, before the next paragraph that is talking more about implementation.
docs/DafnyRef/Attributes.md
Outdated
| ``` | ||
|
|
||
|
|
||
| Dafny rewrites `@`-attributes to old-style equivalent attribute. The definition of these attributes is similar to the following+: |
There was a problem hiding this comment.
| Dafny rewrites `@`-attributes to old-style equivalent attribute. The definition of these attributes is similar to the following+: | |
| Dafny rewrites `@`-attributes to old-style equivalent attributes. The definition of these attributes is similar to the following: |
Related to #5795
Description
This is the first intruction of @-attributes in Dafny.
Future features in development not included in this PR
How has this been tested?
Compile(false)on the new version of someDafnyCore/**/.dfyfiles is tested by the fact that the generated code still does not contain the modules annotated that way.Note that I could not reach in this PR a failing test to trigger the "Attribute not expected here" error, because Coco interprets an @-attribute as the start of a TopLevelDecl for now. In an upcoming PR, non-empty @-attributes will be returned by TopDecl so this error message will be tested.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.