Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feat: @-attributes on top-level declarations #5825

Merged
merged 25 commits into from
Oct 18, 2024
Merged
Show file tree
Hide file tree
Changes from 23 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
b6dcbcb
Feat: @-attributes on top-level declarations
MikaelMayer Oct 9, 2024
09a845d
Fixed class attributes
MikaelMayer Oct 10, 2024
53b2a01
Added missing tests
MikaelMayer Oct 10, 2024
034553c
Fixed formatting
MikaelMayer Oct 10, 2024
4c602ce
Removed unused "attrs"
MikaelMayer Oct 10, 2024
8aa0335
Fixed traitDecl
MikaelMayer Oct 10, 2024
5930792
Added missing iterator attributes
MikaelMayer Oct 11, 2024
440cb47
Formatting (more)
MikaelMayer Oct 11, 2024
cc6f555
make format and fixed least predicate attribute parsing
MikaelMayer Oct 11, 2024
0b956b3
Reverted two tests accidentally modified
MikaelMayer Oct 11, 2024
78d7cf6
Review comments
MikaelMayer Oct 15, 2024
7f24f81
Resolution of attributes ensures arguments are literals
MikaelMayer Oct 16, 2024
b7779ec
Merge branch 'master' into feat-at-attributes-1
MikaelMayer Oct 16, 2024
91667fc
Removed induction
MikaelMayer Oct 17, 2024
87166b1
Merge branch 'master' into feat-at-attributes-1
MikaelMayer Oct 17, 2024
d7dab0f
Merge branch 'master' into feat-at-attributes-1
MikaelMayer Oct 17, 2024
1bf9c63
Fixed the doc
MikaelMayer Oct 17, 2024
2f9dfb7
Review comment: Ensure we check whether attributes can be applied cor…
MikaelMayer Oct 17, 2024
1f81743
Fixed CI
MikaelMayer Oct 17, 2024
73ce2b0
Missing filter cases
MikaelMayer Oct 18, 2024
4958d39
Merge branch 'master' into feat-at-attributes-1
MikaelMayer Oct 18, 2024
0e988bc
ICanVerify is more general + Forward-compatibility for {:fuel} on Ass…
MikaelMayer Oct 18, 2024
858c823
Updated documentation
MikaelMayer Oct 18, 2024
2cf4f65
Merge branch 'master' into feat-at-attributes-1
MikaelMayer Oct 18, 2024
6a88606
Code review
MikaelMayer Oct 18, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ exe:
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

format-dfy:
(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
(cd "${DIR}"/Source/DafnyCore ; make format)
(cd "${DIR}"/Source/DafnyStandardLibraries ; make format)

dfy-to-cs:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
Expand Down
343 changes: 341 additions & 2 deletions Source/DafnyCore/AST/Attributes.cs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,37 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) =>
Attributes.Contains(me.Attributes, "axiom");
}

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(
Copy link
Member

@keyboardDrummer keyboardDrummer Oct 14, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

String ArgName,
Type ArgType, // If null, it means it's not resolved (@Induction and @Trigger)
Expression DefaultValue) {
public Formal ToFormal() {
Contract.Assert(ArgType != null);
return new Formal(Token.NoToken, ArgName, ArgType, true, false,
DefaultValue);
}
}

// Syntax for a built-in @-attribute.
// To create such an attribute, use the Attributes.B() helper
public record BuiltInAtAttributeSyntax(
string Name,
List<BuiltInAtAttributeArgSyntax> Args,
Func<IAttributeBearingDeclaration, bool> CanBeApplied) {
public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) {
var c = new List<BuiltInAtAttributeArgSyntax>(Args) {
new(argName, argType, defaultValue) };
return this with { Args = c };
}

public BuiltInAtAttributeSyntax Filter(Func<IAttributeBearingDeclaration, bool> canBeApplied) {
return this with { CanBeApplied = canBeApplied };
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TIL C# supports this now, cool! Must have stolen it from Dafny's m[k := v] :)

}
}

public class Attributes : TokenNode, ICanFormat {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Name != null);
Expand All @@ -37,6 +67,7 @@ void ObjectInvariant() {
public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(args));
Contract.Requires(name != UserSuppliedAtAttribute.AtName || this is UserSuppliedAtAttribute);
Name = name;
Args = args;
Prev = prev;
Expand Down Expand Up @@ -207,6 +238,241 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
: new List<Node> { Prev });

public override IEnumerable<INode> PreResolveChildren => Children;
public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
foreach (var token in OwnedTokens) {
switch (token.val) {
case "}": {
formatter.SetClosingIndentedRegion(token, indentBefore);
break;
}
case "@": {
formatter.SetIndentations(token, indentBefore, indentBefore, indentBefore);
break;
}
case ",": {
formatter.SetDelimiterInsideIndentedRegions(token, indentBefore);
break;
}
case "{" or "{:": {
formatter.SetOpeningIndentedRegion(token, indentBefore);
break;
}
}
}
foreach (var arg in Args) {
formatter.SetExpressionIndentation(arg);
}
formatter.SetClosingIndentedRegion(EndToken, indentBefore);
return false; // Don't do inner attributes, they should be performed independently
}

// Typically, {:} are indented when @-attributes are not
public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndentCollector formatter) {
foreach (var attribute in attrs.AsEnumerable()) {
if (attribute.StartToken.val == UserSuppliedAtAttribute.AtName) {
attribute.SetIndent(indentBefore, formatter);
} else {
attribute.SetIndent(indentBefore + formatter.SpaceTab, formatter);
}
}
}
private static string TupleItem0Name => "0";
// Helper to create a built-in @-attribute
static BuiltInAtAttributeSyntax BuiltIn(string name) {
return new BuiltInAtAttributeSyntax(
name, new List<BuiltInAtAttributeArgSyntax>(), _ => true);
}

// Helper to create an old-style attribute
private static Attributes A(string name, params Expression[] args) {
return new Attributes(name, args.ToList(), null);
}

// Helper to create an old-style attribute with only one argument
private static Attributes A1(string name, ActualBindings bindings) {
if (Get(bindings, 0, out var expr) && expr != null) {
return A(name, expr);
}

return A(name);
}

// Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute
// or mark it as not built-in for later resolution
public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute, IAttributeBearingDeclaration attributeHost) {
var toMatch = atAttribute.Arg;
var name = atAttribute.UserSuppliedName;
var bindings = atAttribute.UserSuppliedPreResolveBindings;

if (name == null) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString());
return null;
}

if (!TryGetBuiltinAtAttribute(name, out var builtinSyntax) || builtinSyntax == null) {
atAttribute.Builtin = false; // Will be resolved after
return null;
}

if (!builtinSyntax.CanBeApplied(attributeHost)) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
}

var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray();
ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings);

atAttribute.Builtin = true;
atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes

switch (name) {
case "Compile": {
return A1("compile", bindings);
}
case "Fuel": {
if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
if (Get(bindings, 1, out var highFuel) && highFuel != null) {
if (Get(bindings, 2, out var functionName) && IsStringNotEmpty(functionName)) {
return A("fuel", functionName, lowFuel, highFuel);
}

return A("fuel", lowFuel, highFuel);
}

return A("fuel", lowFuel);
}

return A("fuel");
}
case "IsolateAssertions": {
return A("isolate_assertions");
}
case "Options": {
return A1("options", bindings);
}
default: {
throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
}
}
}

// 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.
Comment on lines +359 to +360
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

@MikaelMayer MikaelMayer Oct 15, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

@keyboardDrummer keyboardDrummer Oct 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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 verify or dafny 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 Handled property). If an attribute is not handled, emit a warning.
  • Let the handlers report warnings/errors if attributes are placed incorrectly.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Member

@keyboardDrummer keyboardDrummer Oct 18, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

BuiltIn("Compile")
.WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
.Filter(attributeHost =>
attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
BuiltIn("Fuel")
.WithArg("low", Type.Int, DefaultInt(1))
.WithArg("high", Type.Int, DefaultInt(2))
.WithArg("functionName", Type.ResolvedString(), DefaultString(""))
.Filter(attributeHost => attributeHost is Function or AssertStmt),
BuiltIn("IsolateAssertions")
.Filter(attributeHost => attributeHost is ICanVerify),
BuiltIn("Options")
.WithArg(TupleItem0Name, Type.ResolvedString())
.Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),
};

////// Helpers to create default values for the @-attribute definitions above //////

public static LiteralExpr DefaultString(string value) {
return Expression.CreateStringLiteral(Token.NoToken, value);
}

public static LiteralExpr DefaultBool(bool value) {
return Expression.CreateBoolLiteral(Token.NoToken, value);
}

public static LiteralExpr DefaultInt(int value) {
return Expression.CreateIntLiteralNonnegative(Token.NoToken, value);
}

private static bool IsStringNotEmpty(Expression value) {
return value is StringLiteralExpr { Value: string and not "" };
}

// Given resolved bindings, gets the i-th argument according to the
// declaration formals order
private static bool Get(ActualBindings bindings, int i, out Expression expr) {
if (bindings.Arguments.Count < i + 1) {
expr = null;
return false;
}

expr = bindings.Arguments[i];
return true;
}

// Resolves bindings given a list of datatype constructor-like formals,
// obtained from built-in @-attribute definitions
private static void ResolveLikeDatatypeConstructor(
Program program, Formal[] formals, string attrName,
UserSuppliedAtAttribute attrs, ActualBindings bindings) {
var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
var typeMap = new Dictionary<TypeParameter, Type>();
var resolver = new ModuleResolver(new ProgramResolver(program), program.Options);
resolver.reporter = program.Reporter;
resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.tok,
attrs, resolutionContext, typeMap, null);
resolver.FillInDefaultValueExpressions();
resolver.SolveAllTypeConstraints();
// Verify that arguments are given literally
foreach (var binding in bindings.ArgumentBindings) {
if (binding.Actual is not LiteralExpr) {
program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal");
}
}
}

// Recovers a built-in @-Attribute if it exists
public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeSyntax builtinAtAttribute) {
return BuiltInAtAttributeDictionary.TryGetValue(name, out builtinAtAttribute);
}

// Builtin @-attributes dictionary based on the sequence of definitions of @-attributes
public static Dictionary<string, BuiltInAtAttributeSyntax> BuiltInAtAttributeDictionary =
BuiltinAtAttributes.ToDictionary(b => {
if (b.Name.Contains("_") || b.Name.Contains("-") || Char.IsLower(b.Name[0])) {
throw new Exception("Builtin @-attributes are PascalCase for consistency");
}
return b.Name;
}, b => b);

// Overridable method to clone the attribute as if the new attribute was placed after "prev" in the source code
public virtual Attributes CloneAfter(Attributes prev) {
return new Attributes(Name, Args, prev);
}

//////// Helpers for parsing attributes //////////////////

// Returns the memory location's attributes content and set the memory location to null (no attributes)
public static Attributes Consume(ref Attributes tmpStack) {
var result = tmpStack;
tmpStack = null;
return result;
}

// Empties the first attribute memory location while prepending its attributes to the second attribute memory location, in the same order
public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) {
MergeIntoReadonly(tmpStack, ref attributesStack);
tmpStack = null;
}

// Prepends the attributes tmpStack before the attributes contained in the memory location attributesStack
private static void MergeIntoReadonly(Attributes tmpStack, ref Attributes attributesStack) {
if (tmpStack == null) {
return;
}
if (attributesStack == null) {
attributesStack = tmpStack;
return;
}
MergeIntoReadonly(tmpStack.Prev, ref attributesStack);
attributesStack = tmpStack.CloneAfter(attributesStack);
}
}

public static class AttributesExtensions {
Expand All @@ -221,6 +487,7 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {
}
}

// {:..} Attributes parsed are built using this class
public class UserSuppliedAttributes : Attributes {
public readonly IToken OpenBrace;
public readonly IToken CloseBrace;
Expand All @@ -237,11 +504,83 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
}
}

// @-Attributes parsed are built using this class
public class UserSuppliedAtAttribute : Attributes {
public static readonly string AtName = "@";
public readonly IToken AtSign;
public bool Builtin; // set to true to indicate it was recognized as a builtin attribute
// Otherwise it's a user-defined one and Arg needs to be fully resolved
public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev)
: base(AtName, new List<Expression>() { arg }, prev) {
Contract.Requires(tok != null);
this.tok = tok;
this.AtSign = tok;
}

public Expression Arg => Args[0];

public override Attributes CloneAfter(Attributes prev) {
return new UserSuppliedAtAttribute(AtSign, Args[0], prev);
}

// Name of this @-Attribute, which is the part right after the @
public string UserSuppliedName =>
GetName(this);

// Pre-resolved bindings of this @-Attribute
public ActualBindings UserSuppliedPreResolveBindings =>
GetPreResolveBindings(this);

// Pre-resolved arguments of this @-Attributes. The order is the one provided by the user,
// not by any binding. Used for
public IEnumerable<Expression> UserSuppliedPreResolveArguments =>
GetPreResolveArguments(this);

// Gets the name of an @-attribute. Attributes might be applied.
public static string GetName(Attributes a) {
if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Lhs: NameSegment { Name: var name } } }) {
return name;
}
if (a is UserSuppliedAtAttribute { Arg: NameSegment { Name: var singleName } }) {
return singleName;
}

return null;
}

// Gets the pre-resolved bindings of an @-Attribute.
// Returns an empty bindings if it's anything else
public static ActualBindings GetPreResolveBindings(Attributes a) {
if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Bindings: var bindings } }) {
return bindings;
}
return new ActualBindings(new List<ActualBinding>());
}

// Gets the list of pre-resolved arguments of an @-Attribute, and an empty list otherwise
public static IEnumerable<Expression> GetPreResolveArguments(Attributes a) {
if (a is UserSuppliedAtAttribute { UserSuppliedPreResolveBindings: var bindings }) {
return bindings.ArgumentBindings.Select(arg => arg.Actual);
}

return new List<Expression>();
}

// Gets the list of pre-resolved arguments of an @-Attribute, and the list of arguments
// for any other kind of attributes. Used for example to extract module options for parsing.
public static IEnumerable<Expression> GetUserSuppliedArguments(Attributes a) {
return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args;
}

public override string ToString() => Prev + (Prev == null ? "" : " ") + "@" + Arg;
}

/// <summary>
/// A class implementing this interface is one that can carry attributes.
/// </summary>
public interface IAttributeBearingDeclaration {
Attributes Attributes { get; }
Attributes Attributes { get; internal set; }
string WhatKind { get; }
}

public static class AttributeBearingDeclarationExtensions {
Expand Down
Loading
Loading