From b6dcbcbe9c1ba5457938bc3b55f373bdc02c334d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 9 Oct 2024 10:27:21 -0500 Subject: [PATCH 01/20] Feat: @-attributes on top-level declarations --- Source/DafnyCore/AST/Attributes.cs | 288 +++++++++++++++++- Source/DafnyCore/AST/Cloner.cs | 5 +- .../Comprehensions/ComprehensionExpr.cs | 5 +- .../DafnyCore/AST/Expressions/Expression.cs | 19 +- Source/DafnyCore/AST/Grammar/ParseErrors.cs | 5 +- .../AST/Grammar/ParserNonGeneratedPart.cs | 51 +++- .../Statements/Assignment/AttributedToken.cs | 5 +- .../Statements/Assignment/LocalVariable.cs | 6 +- .../AST/TypeDeclarations/Declaration.cs | 5 +- Source/DafnyCore/AST/Types/Types.cs | 5 + Source/DafnyCore/Dafny.atg | 139 +++++---- Source/DafnyCore/Resolver/ModuleResolver.cs | 2 +- .../NameResolutionAndTypeInference.cs | 11 +- .../PreTypeResolve.ActualParameters.cs | 2 +- .../DafnyCore/Rewriters/ExpandAtAttributes.cs | 44 +++ .../DafnyCore/Rewriters/RewriterCollection.cs | 2 +- .../BoogieGenerator.ExpressionTranslator.cs | 3 +- .../DafnyDriver/Commands/BoogieExtractor.cs | 2 +- .../at-attributes-acceptable-builtin.dfy | 45 +++ .../at-attributes/at-attributes-typos.dfy | 29 ++ .../at-attributes-typos.dfy.expect | 8 + Source/XUnitExtensions/Lit/DiffCommand.cs | 3 + 22 files changed, 606 insertions(+), 78 deletions(-) create mode 100644 Source/DafnyCore/Rewriters/ExpandAtAttributes.cs create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index e3f44389b65..925f51258b5 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -15,6 +15,31 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) => Attributes.Contains(me.Attributes, "axiom"); } +// Syntax of a formal of a built-in @-attribute +// To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg() +public record BuiltInAtAttributeArgSyntax( + 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 Args) { + public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) { + var c = new List(Args) { + new(argName, argType, defaultValue) }; + return this with { Args = c }; + } +} + public class Attributes : TokenNode { [ContractInvariantMethod] void ObjectInvariant() { @@ -37,6 +62,7 @@ void ObjectInvariant() { public Attributes(string name, [Captured] List 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; @@ -207,6 +233,196 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object : new List { Prev }); public override IEnumerable PreResolveChildren => Children; + + + private static string TupleItem0Name => "0"; + // Helper to create a built-in @-attribute + static BuiltInAtAttributeSyntax B(string name) { + return new BuiltInAtAttributeSyntax( + name, new List()); + } + + // 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 i as not built-in for later resolution + public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute) { + 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 (name != "Induction" && name != "Trigger") { + var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray(); + ResolveLikeDatatypeConstructor(program, formals, name, toMatch.tok, bindings); + } // For @Induction and @Trigger, resolution is done in the generated version of the attributes + + 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 "Induction": { + return A("induction", bindings.ArgumentBindings.Select(binding => binding.Actual).ToArray()); + } + 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. + public static readonly List BuiltinAtAttributes = new() { + B("Compile").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true)), + B("Fuel") + .WithArg("low", Type.Int, DefaultInt(1)) + .WithArg("high", Type.Int, DefaultInt(2)) + .WithArg("functionName", Type.ResolvedString(), DefaultString("")), + B("Induction"), // Resolution is different + B("IsolateAssertions"), + B("Options").WithArg(TupleItem0Name, Type.ResolvedString()), + }; + + ////// 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, + IToken attrsTok, ActualBindings bindings) { + var datatypeName = new Name(RangeToken.NoToken, attrName); + var datatypeCtor = new DatatypeCtor(RangeToken.NoToken, datatypeName, false, formals.ToList(), null); + var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ; + var typeMap = new Dictionary(); + var resolver = new ModuleResolver(new ProgramResolver(program), program.Options); + resolver.reporter = program.Reporter; + resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo; + resolver.ResolveActualParameters(bindings, formals.ToList(), attrsTok, + datatypeCtor, resolutionContext, typeMap, null); + resolver.FillInDefaultValueExpressions(); + resolver.SolveAllTypeConstraints(); + } + + // 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 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 { @@ -221,6 +437,7 @@ public static IEnumerable AsEnumerable(this Attributes attr) { } } +// {:..} Attributes parsed are built using this class public class UserSuppliedAttributes : Attributes { public readonly IToken OpenBrace; public readonly IToken CloseBrace; @@ -237,11 +454,80 @@ 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() { 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 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()); + } + + // Gets the list of pre-resolved arguments of an @-Attribute, and an empty list otherwise + public static IEnumerable GetPreResolveArguments(Attributes a) { + if (a is UserSuppliedAtAttribute { UserSuppliedPreResolveBindings: var bindings }) { + return bindings.ArgumentBindings.Select(arg => arg.Actual); + } + + return new List(); + } + + // 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 GetUserSuppliedArguments(Attributes a) { + return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args; + } +} + /// /// A class implementing this interface is one that can carry attributes. /// public interface IAttributeBearingDeclaration { - Attributes Attributes { get; } + Attributes Attributes { get; internal set; } } public static class AttributeBearingDeclarationExtensions { diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index d42e6358abc..66ff187b38a 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -334,10 +334,11 @@ public Attributes CloneAttributes(Attributes attrs) { } else if (!CloneResolvedFields && attrs.Name.StartsWith("_")) { // skip this attribute, since it would have been produced during resolution return CloneAttributes(attrs.Prev); - } else if (attrs is UserSuppliedAttributes) { - var usa = (UserSuppliedAttributes)attrs; + } else if (attrs is UserSuppliedAttributes usa) { return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace), attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)); + } else if (attrs is UserSuppliedAtAttribute usaa) { + return new UserSuppliedAtAttribute(Tok(usaa.tok), CloneExpr(usaa.Arg), CloneAttributes(usaa.Prev)); } else { return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)); } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index 0abfc1614cd..b137babd8de 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -40,7 +40,10 @@ void ObjectInvariant() { } public Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + Attributes IAttributeBearingDeclaration.Attributes { + get => Attributes; + set => Attributes = value; + } [FilledInDuringResolution] public List Bounds; // invariant Bounds == null || Bounds.Count == BoundVars.Count; diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 7b4f54224e3..eef5c6e69d2 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -390,10 +390,21 @@ public static Expression CreateDecrement(Expression e, int n, Type ty = null) { if (n == 0) { return e; } - var nn = CreateIntLiteral(e.tok, n, ty); + var nn = CreateIntLiteralNonnegative(e.tok, n, ty); return CreateSubtract(e, nn); } + /// + /// Create a resolved expression of the form "n" when n is nonnegative + /// + public static LiteralExpr CreateIntLiteralNonnegative(IToken tok, int n, Type ty = null) { + Contract.Requires(tok != null); + Contract.Requires(0 <= n); + var nn = new LiteralExpr(tok, n); + nn.Type = ty ?? Type.Int; + return nn; + } + /// /// Create a resolved expression of the form "n" /// @@ -401,11 +412,9 @@ public static Expression CreateIntLiteral(IToken tok, int n, Type ty = null) { Contract.Requires(tok != null); Contract.Requires(n != int.MinValue); if (0 <= n) { - var nn = new LiteralExpr(tok, n); - nn.Type = ty ?? Type.Int; - return nn; + return CreateIntLiteralNonnegative(tok, n, ty); } else { - return CreateDecrement(CreateIntLiteral(tok, 0, ty), -n, ty); + return CreateDecrement(CreateIntLiteralNonnegative(tok, 0, ty), -n, ty); } } diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 8e666089d15..898e1161766 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -11,6 +11,7 @@ public class ParseErrors { public enum ErrorId { // ReSharper disable once InconsistentNaming none, + p_extra_attributes, p_duplicate_modifier, p_abstract_not_allowed, p_no_ghost_for_by_method, @@ -144,7 +145,9 @@ public enum ErrorId { } static ParseErrors() { - + Add(ErrorId.p_extra_attributes, + @" +@-attributes are not supported here".TrimStart(), Remove(true, "Remove this @-attribute")); Add(ErrorId.p_duplicate_modifier, @" No Dafny modifier, such as [`abstract`, `static`, `ghost`](https://dafny.org/latest/DafnyRef/DafnyRef#sec-declaration-modifiers) may be repeated diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 783e1716810..2284767b3e3 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -25,6 +25,14 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca theModule = new FileModuleDefinition(scanner.FirstToken); } + public void MergeInto(ref Attributes attrsStack, ref Attributes attrsTarget) { + Attributes.MergeInto(ref attrsStack, ref attrsTarget); + } + + public Attributes Consume(ref Attributes attrs) { + return Attributes.Consume(ref attrs); + } + bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident); bool IsIdentifier(int kind) { @@ -458,6 +466,30 @@ bool IsGenericInstantiation(bool inExpressionContext) { return false; } } + + // Returns true if the parser can parse an heap-referencing @-call + // The reason to do this is that expressions can be prefixed by @-Attributes, + // so the rule to distinguish them is that an @-call of the form name@label(args), + // the @ must be next to the name. Otherwise an attribute is parsed. + // Indeed 'name' could be the last expression of an ensures clause, and the attribute + // could belong to the next method declaration otherwise. + bool IsAtCall() { + IToken pt = la; + if (pt.val != "@") { + return false; + } + // If it's the beginning of the file, or the previous token is on a different line or separated by a space, it's not an At-call. Must be an attribute + var isFirstToken = pt.Prev == null; + var spaceExistsSincePreviousToken = + !isFirstToken && + (pt.Prev.line != pt.line || pt.Prev.col + pt.Prev.val.Length + pt.TrailingTrivia.Trim().Length < pt.col - pt.LeadingTrivia.Trim().Length); + if (isFirstToken || spaceExistsSincePreviousToken) { + return false; + } + + return true; + } + /* Returns true if the next thing is of the form: * "<" Type { "," Type } ">" */ @@ -608,7 +640,7 @@ int StringToInt(string s, int defaultValue, string errString, IToken tok) { int anonymousIds = 0; /// - /// Holds the modifiers given for a declaration + /// Holds the modifiers and attributes given for a declaration /// /// Not all modifiers are applicable to all kinds of declarations. /// Errors are given when a modify does not apply. @@ -627,6 +659,7 @@ class DeclModifierData { public bool IsOpaque; public IToken OpaqueToken; public IToken FirstToken; + public Attributes Attributes = null; } private ModuleKindEnum GetModuleKind(DeclModifierData mods) { @@ -644,6 +677,16 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) { return ModuleKindEnum.Concrete; } + /// + /// Before literals that end a block, we usually add CheckNoAttributes to avoid any non-attached or dangling attributes + /// + public void CheckNoAttributes(ref Attributes attrs) { + if (attrs != null) { + SemErr(ErrorId.p_extra_attributes, attrs.RangeToken, "Attribute not expected here"); + attrs = null; + } + } + // Check that token has not been set, then set it. public void CheckAndSetToken(ref IToken token) { if (token != null) { @@ -725,10 +768,10 @@ Expression ProcessTupleArgs(List args, IToken lp) { public void ApplyOptionsFromAttributes(Attributes attrs) { - var overrides = attrs.AsEnumerable().Where(a => a.Name == "options") + var overrides = attrs.AsEnumerable().Where(a => a.Name == "options" || a is UserSuppliedAtAttribute { UserSuppliedName: "Options" }) .Reverse().Select(a => - (token: (a as UserSuppliedAttributes)?.tok, - options: a.Args.Select(arg => { + (token: a.tok, + options: UserSuppliedAtAttribute.GetUserSuppliedArguments(a).Select(arg => { if (arg is not LiteralExpr { Value: string optStr }) { SemErr(ErrorId.p_literal_string_required, arg.tok, "argument to :options attribute must be a literal string"); return null; diff --git a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs index 49545c285a5..a1f60a99abc 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs @@ -12,5 +12,8 @@ namespace Microsoft.Dafny; /// attributes). /// public record AttributedToken(IToken Token, Attributes Attrs) : IAttributeBearingDeclaration { - Attributes IAttributeBearingDeclaration.Attributes => Attrs; + Attributes IAttributeBearingDeclaration.Attributes { + get => Attrs; + set => throw new System.NotImplementedException(); + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index ab2331d019f..c20a0ab46ad 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -9,7 +9,11 @@ public class LocalVariable : RangeNode, IVariable, IAttributeBearingDeclaration readonly string name; public string DafnyName => Name; public Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + Attributes IAttributeBearingDeclaration.Attributes { + get => Attributes; + set => Attributes = value; + } + public bool IsGhost; [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index db68fdf4112..44aa0d7d31c 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -124,7 +124,10 @@ public virtual string GetCompileName(DafnyOptions options) { } public Attributes Attributes; // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + Attributes IAttributeBearingDeclaration.Attributes { + get => Attributes; + set => Attributes = value; + } [Pure] public override string ToString() { diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 7c49af62df7..423797040a4 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -17,6 +17,11 @@ public abstract class Type : TokenNode { public override IEnumerable PreResolveChildren => TypeArgs.OfType(); public static Type Nat() { return new UserDefinedType(Token.NoToken, "nat", null); } // note, this returns an unresolved type public static Type String() { return new UserDefinedType(Token.NoToken, "string", null); } // note, this returns an unresolved type + + public static Type ResolvedString() { + return new SeqType(new CharType()); + } + public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType(); private static ThreadLocal> _scopes = new(); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index e41632969e0..0755626b118 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -213,6 +213,7 @@ PRODUCTIONS Dafny = (. IToken includeStartToken; IToken fileStartToken = t; + Attributes attrs = null; .) { "include" (. includeStartToken = t; .) stringToken (. { @@ -231,7 +232,9 @@ Dafny } .) } - { TopDecl } + { AtAttributes + TopDecl } + (. CheckNoAttributes(ref attrs); .) (. theModule.RangeToken = new RangeToken(fileStartToken.Next, t); .) @@ -250,8 +253,11 @@ DeclModifier . /*------------------------------------------------------------------------*/ -TopDecl<. ModuleDefinition module, bool isTopLevel .> -= (. DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule; +TopDecl += (. DeclModifierData dmod = new DeclModifierData() { + Attributes = Consume(ref attrs) + }; + ModuleDecl submodule; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; .) @@ -323,7 +329,7 @@ ModuleDefinition } (. ApplyOptionsFromAttributes(attrs); .) + { Attribute } (. ApplyOptionsFromAttributes(dmod.Attributes); .) ModuleQualifiedName (. var name = names[^1]; prefixIds = names.GetRange(0,names.Count-1).Select(n => n.StartToken).ToList(); @@ -334,12 +340,14 @@ ModuleDefinition (. SemErr(ErrorId.p_bad_module_decl, t, $"expected either a '{{' or a 'refines' keyword here, found {iderr.val}"); .) ] (. module = new ModuleDefinition(RangeToken.NoToken, name, prefixIds, GetModuleKind(dmod), false, - idRefined == null ? null : new Implements(implementationKind, new ModuleQualifiedId(idRefined)), parent, attrs); + idRefined == null ? null : new Implements(implementationKind, new ModuleQualifiedId(idRefined)), parent, dmod.Attributes); .) SYNC (. tokenWithTrailingDocString = t; .) "{" (. module.BodyStartTok = t; .) - { TopDecl} + { AtAttributes + TopDecl} "}" + (. CheckNoAttributes(ref attrs); .) (. module.RangeToken = new RangeToken(dmod.FirstToken, t); module.TokenWithTrailingDocString = tokenWithTrailingDocString; @@ -524,7 +532,7 @@ ClassDecl } + { Attribute } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) [ ExtendsClause @@ -630,7 +638,6 @@ DatatypeDecl typeArgs = new List(); List parentTraits = new List(); List ctors = new List(); @@ -644,7 +651,7 @@ DatatypeDecl } + { Attribute } DatatypeName [ GenericParameters ] [ ExtendsClause ] @@ -659,9 +666,9 @@ DatatypeDecl ] (. if (co) { - dt = new CoDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, attrs, isRefining); + dt = new CoDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, dmod.Attributes, isRefining); } else { - dt = new IndDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, attrs, isRefining); + dt = new IndDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, dmod.Attributes, isRefining); } dt.BodyStartTok = bodyStart; dt.TokenWithTrailingDocString = bodyStart; @@ -694,7 +701,9 @@ TypeMembers<. ModuleDefinition/*!*/ module, List members .> = (. DeclModifierData dmod; .) "{" - { (. dmod = new DeclModifierData(); .) + { (. dmod = new DeclModifierData(); + .) + AtAttributes { DeclModifier } ClassMemberDecl } @@ -763,7 +772,6 @@ LocalVarName = NoUSIdent . NewtypeDecl = (. Name name; IToken bvId; - Attributes attrs = null; td = null; Type baseType = null; Expression constraint; @@ -774,7 +782,7 @@ NewtypeDecl var typeParameters = new List(); .) "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) - { Attribute } + { Attribute } NewtypeName [ GenericParameters ] [ ExtendsClause ] @@ -792,13 +800,13 @@ NewtypeDecl [ TypeMembers ] (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, new BoundVar(bvId, bvId.val, baseType), - constraint, witnessKind, witness, parentTraits, members, attrs, isRefining: false); + constraint, witnessKind, witness, parentTraits, members, dmod.Attributes, isRefining: false); .) | Type WitnessClause [ TypeMembers ] (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, - baseType, witnessKind, witness, parentTraits, members, attrs, isRefining: false); + baseType, witnessKind, witness, parentTraits, members, dmod.Attributes, isRefining: false); .) ) | ellipsis @@ -806,7 +814,7 @@ NewtypeDecl (. baseType = null; // Base type is not known yet td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, baseType, SubsetTypeDecl.WKind.CompiledZero, null, - parentTraits, members, attrs, isRefining: true); + parentTraits, members, dmod.Attributes, isRefining: true); .) ) (. if (td != null) { td.TokenWithTrailingDocString = t; @@ -819,7 +827,6 @@ SynonymTypeName = Name . // The following includes Opaque type definitions SynonymTypeDecl = (. IToken bvId; - Attributes attrs = null; var characteristics = new TypeParameter.TypeParameterCharacteristics(false); var typeArgs = new List(); td = null; @@ -832,7 +839,7 @@ SynonymTypeDecl } + { Attribute } SynonymTypeName { TypeParameterCharacteristics } [ GenericParameters ] @@ -844,12 +851,12 @@ SynonymTypeDecl WitnessClause (. td = new SubsetTypeDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, - new BoundVar(bvId, bvId.val, ty), constraint, witnessKind, witness, attrs); + new BoundVar(bvId, bvId.val, ty), constraint, witnessKind, witness, dmod.Attributes); kind = "subset type"; .) | Type - (. td = new TypeSynonymDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, ty, attrs); + (. td = new TypeSynonymDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, ty, dmod.Attributes); kind = "type synonym"; .) ) @@ -864,7 +871,7 @@ SynonymTypeDecl } + { Attribute } (. MergeInto(ref attrs, ref dmod.Attributes); .) IteratorName ( [ GenericParameters ] @@ -1155,7 +1162,6 @@ MethodDecl bool hasName = false; Name name = new Name(""); IToken keywordToken; - Attributes attrs = null; List/*!*/ typeArgs = new List(); List ins = new List(); List outs = new List(); @@ -1219,7 +1225,7 @@ MethodDecl .) ) (. keywordToken = t; CheckDeclModifiers(ref dmod, caption, allowed); .) - { Attribute } + { Attribute } [ MethodFunctionName (. hasName = true; .) ] (. if (!hasName) { @@ -1262,25 +1268,25 @@ MethodDecl req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), - (DividedBlockStmt)body, attrs, signatureEllipsis); + (DividedBlockStmt)body, dmod.Attributes, signatureEllipsis); } else if (isLeastLemma) { m = new LeastLemma(range, name, dmod.IsStatic, kType, typeArgs, ins, outs, - req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, dmod.Attributes, signatureEllipsis); } else if (isGreatestLemma) { m = new GreatestLemma(range, name, dmod.IsStatic, kType, typeArgs, ins, outs, - req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, dmod.Attributes, signatureEllipsis); } else if (isLemma) { m = new Lemma(range, name, dmod.IsStatic, typeArgs, ins, outs, - req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, dmod.Attributes, signatureEllipsis); } else if (isTwoStateLemma) { m = new TwoStateLemma(range, name, dmod.IsStatic, typeArgs, ins, outs, req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), - ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + ens, new Specification(dec, decAttrs), body, dmod.Attributes, signatureEllipsis); } else { m = new Method(range, name, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs, req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, - new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + new Specification(dec, decAttrs), body, dmod.Attributes, signatureEllipsis); } m.BodyStartTok = bodyStart; m.TokenWithTrailingDocString = tokenWithTrailingDocString; @@ -1415,23 +1421,23 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow Expression defaultValue; bool isNameOnly; bool isOlder; - Attributes attributes = null; + Attributes attrs = null; RangeToken range; Name name; .) "(" [ - { Attribute } + { Attribute } GIdentType ParameterDefaultValue - (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder) + (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) - { "," - { Attribute } + { "," + { Attribute } GIdentType ParameterDefaultValue - (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder) + (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) } @@ -1681,7 +1687,6 @@ GenericInstantiation<.List gt.> /*------------------------------------------------------------------------*/ FunctionDecl = (. Contract.Ensures(Contract.ValueAtReturn(out f) != null); - Attributes attrs = null; Name name = null; // To please compiler List typeArgs = new List(); List formals = new List(); @@ -1691,6 +1696,7 @@ FunctionDecl List ens = new List(); List reads = new List(); List decreases; + Attributes attrs = null; Attributes decAttrs = null; Attributes readsAttrs = null; Expression body = null; @@ -1747,7 +1753,7 @@ FunctionDecl ( "function" (. headToken = t; CheckAndSetTokenOnce(ref dmod.FirstToken); .) [ "method" (. functionMethodToken = t; .) ] - { Attribute } + { Attribute } MethodFunctionName ( [ GenericParameters ] @@ -1770,7 +1776,7 @@ FunctionDecl | "predicate" (. headToken = t; isPredicate = true; CheckAndSetTokenOnce(ref dmod.FirstToken); .) [ "method" (. functionMethodToken = t; .) ] - { Attribute } + { Attribute } MethodFunctionName ( [ GenericParameters ] @@ -1811,7 +1817,7 @@ FunctionDecl | "copredicate" (. CheckAndSetTokenOnce(ref dmod.FirstToken); errors.Deprecated(ErrorId.p_deprecated_copredicate, t, "the old keyword 'copredicate' has been renamed to the keyword phrase 'greatest predicate'"); .) ) (. isGreatestPredicate = true; .) - { Attribute } + { Attribute } MethodFunctionName ( [ GenericParameters ] @@ -1982,39 +1988,38 @@ FunctionDecl /* ========================================= * Finally, we create the AST node for the function declaration we parsed. */ - var range = new RangeToken(dmod.FirstToken, t); if (isTwoState && isPredicate) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new TwoStatePredicate(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result, reqs, new Specification(reads, readsAttrs), ens, - new Specification(decreases, decAttrs), body, attrs, signatureEllipsis); + new Specification(decreases, decAttrs), body, dmod.Attributes, signatureEllipsis); } else if (isTwoState) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new TwoStateFunction(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result, returnType, reqs, new Specification(reads, readsAttrs), ens, - new Specification(decreases, decAttrs), body, attrs, signatureEllipsis); + new Specification(decreases, decAttrs), body, dmod.Attributes, signatureEllipsis); } else if (isPredicate) { Contract.Assert(functionMethodToken == null || !dmod.IsGhost); f = new Predicate(range, name, dmod.IsStatic, isGhost, dmod.IsOpaque, typeArgs, formals, result, reqs, new Specification(reads, readsAttrs), ens, new Specification(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited, - byMethodTok, byMethodBody, attrs, signatureEllipsis); + byMethodTok, byMethodBody, dmod.Attributes, signatureEllipsis); } else if (isLeastPredicate) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new LeastPredicate(range, name, dmod.IsStatic, dmod.IsOpaque, kType, typeArgs, formals, result, - reqs, new Specification(reads, readsAttrs), ens, body, attrs, signatureEllipsis); + reqs, new Specification(reads, readsAttrs), ens, body, dmod.Attributes, signatureEllipsis); } else if (isGreatestPredicate) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new GreatestPredicate(range, name, dmod.IsStatic, dmod.IsOpaque, kType, typeArgs, formals, result, - reqs, new Specification(reads, readsAttrs), ens, body, attrs, signatureEllipsis); + reqs, new Specification(reads, readsAttrs), ens, body, dmod.Attributes, signatureEllipsis); } else { Contract.Assert(functionMethodToken == null || !dmod.IsGhost); f = new Function(range, name, dmod.IsStatic, isGhost, dmod.IsOpaque, typeArgs, formals, result, returnType, reqs, new Specification(reads, readsAttrs), ens, new Specification(decreases, decAttrs), body, byMethodTok, byMethodBody, - attrs, signatureEllipsis); + dmod.Attributes, signatureEllipsis); } f.BodyStartTok = bodyStart; f.TokenWithTrailingDocString = tokenWithTrailingDocString; @@ -3833,7 +3838,9 @@ ParensExpression var args = new List(); e = dummyExpr; .) - "(" (. lp = t; .) + "(" + (. lp = t; + .) ( MaybeDecreasesToExpression ")" (. rp = t; @@ -4255,9 +4262,11 @@ NameSegment ( IF(IsGenericInstantiation(true)) (. typeArgs = new List(); .) GenericInstantiation - [ AtCall ] + [ IF(IsAtCall()) + AtCall ] | HashCall - | [ AtCall ] + | [ IF(IsAtCall()) + AtCall ] ) /* Note, since HashCall updates id.val, we make sure not to use id.val until after the possibility of calling HashCall. */ (. e = new NameSegment(id, id.val, typeArgs); @@ -4346,9 +4355,11 @@ Suffix ( IF(IsGenericInstantiation(true)) (. typeArgs = new List(); .) GenericInstantiation - [ AtCall ] + [ IF(IsAtCall()) + AtCall ] | HashCall - | [ AtCall ] + | [ IF(IsAtCall()) + AtCall ] ) (. e = new ExprDotName(id, e, id.val, typeArgs) { RangeToken = new RangeToken(startToken, id) @@ -4593,6 +4604,28 @@ Attribute .) . +AtAttributes += { AtAttribute } + . + +/* After literals that start a block, we usually add this + Note that it will parse all at-attributes at once since expression parsing + return attributes parsed after them. No need to wrap in a repeat statement +*/ +AtAttribute += (. IToken atToken = null; + Expression arg; + .) + "@" + (. atToken = t; .) + Expression + (. + var rtok = new RangeToken(atToken, t); + attrs = new UserSuppliedAtAttribute(t, arg, attrs); + attrs.RangeToken = rtok; + .) + . + /*------------------------------------------------------------------------*/ Ident = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index ae9de04f6b2..88ad0616f38 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -3512,7 +3512,7 @@ void ResolveCasePattern(CasePattern pat, Type sourceType, ResolutionCont /// /// This method is called at the tail end of Pass1 of the Resolver. /// - void FillInDefaultValueExpressions() { + internal void FillInDefaultValueExpressions() { var visited = new Dictionary(); foreach (var e in allDefaultValueExpressions) { e.FillIn(this, visited); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index f78d2a8e742..d6950c5f50c 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -319,15 +319,20 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu // order does not matter much for resolution, so resolve them in reverse order foreach (var attr in attributeHost.Attributes.AsEnumerable()) { - if (attr is UserSuppliedAttributes) { - var usa = (UserSuppliedAttributes)attr; + if (attr is UserSuppliedAtAttribute { Builtin: true }) { // Already resolved + continue; + } else if (attr is UserSuppliedAttributes usa) { usa.Recognized = IsRecognizedAttribute(usa, attributeHost); } if (attr.Args != null) { foreach (var arg in attr.Args) { Contract.Assert(arg != null); if (!(Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment)) { + var prevCount = reporter.ErrorCount; ResolveExpression(arg, resolutionContext); + if (prevCount == reporter.ErrorCount && attr is UserSuppliedAtAttribute { Builtin: false }) { + reporter.Error(MessageSource.Resolver, attr.tok, "User-supplied @-Attributes not supported yet"); + } } else { ResolveRevealLemmaAttribute(arg); } @@ -3200,7 +3205,7 @@ void ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type recei /// "typeMap" is applied to the type of each formal. /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method. /// - void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext resolutionContext, + internal void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext resolutionContext, Dictionary typeMap, Expression/*?*/ receiver) { Contract.Requires(bindings != null); Contract.Requires(formals != null); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs index 6b6a9af13a9..b8ea8118052 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs @@ -18,7 +18,7 @@ public partial class PreTypeResolver { /// "typeMap" is applied to the type of each formal. /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method. /// - void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext opts, + internal void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext opts, Dictionary typeMap, Expression/*?*/ receiver) { Contract.Requires(bindings != null); Contract.Requires(formals != null); diff --git a/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs new file mode 100644 index 00000000000..28a31de1e1b --- /dev/null +++ b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs @@ -0,0 +1,44 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny; + +/// +/// Expands @Attribute to their previous version {:attribute} when recognized +/// Marks recognized user-supplied @-attributes as .Builtin = true +/// That way, only those not .Builtin are resolved. +/// +public class ExpandAtAttributes : IRewriter { + private readonly SystemModuleManager systemModuleManager; + public ExpandAtAttributes(Program program, ErrorReporter reporter) + : base(reporter) { + Contract.Requires(reporter != null); + Contract.Requires(systemModuleManager != null); + systemModuleManager = program.SystemModuleManager; + } + + internal override void PreResolve(Program program) { + program.Visit((INode node) => { + if (node is not IAttributeBearingDeclaration attributeHost) { + return true; + } + + Attributes extraAttrs = null; + foreach (var attr in attributeHost.Attributes.AsEnumerable()) { + if (attr is not UserSuppliedAtAttribute userSuppliedAtAttribute) { + continue; + } + + var newAttributes = Attributes.ExpandAtAttribute(program, userSuppliedAtAttribute); + Attributes.MergeInto(ref newAttributes, ref extraAttrs); + } + + var newAttrs = attributeHost.Attributes; + Attributes.MergeInto(ref extraAttrs, ref newAttrs); + attributeHost.Attributes = newAttrs; + + return true; + }); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Rewriters/RewriterCollection.cs b/Source/DafnyCore/Rewriters/RewriterCollection.cs index 573ad83e3e1..220944c1d88 100644 --- a/Source/DafnyCore/Rewriters/RewriterCollection.cs +++ b/Source/DafnyCore/Rewriters/RewriterCollection.cs @@ -12,7 +12,7 @@ public static IList GetRewriters(ErrorReporter reporter, Program prog if (reporter.Options.AuditProgram) { result.Add(new Auditor.Auditor(reporter)); } - + result.Add(new ExpandAtAttributes(program, reporter)); result.Add(new AutoContractsRewriter(program, reporter)); result.Add(new OpaqueMemberRewriter(reporter)); result.Add(new AutoReqFunctionRewriter(program, reporter)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 10d78a37498..b12a28b7a2f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -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) ) { continue; } diff --git a/Source/DafnyDriver/Commands/BoogieExtractor.cs b/Source/DafnyDriver/Commands/BoogieExtractor.cs index dd9a226fdc0..6b76b853faf 100644 --- a/Source/DafnyDriver/Commands/BoogieExtractor.cs +++ b/Source/DafnyDriver/Commands/BoogieExtractor.cs @@ -186,7 +186,7 @@ public override void VisitMethod(Method method) { return triggers; } - private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) { + private QKeyValue? GetKeyValues(IToken tok, Attributes? attributes) { QKeyValue? kv = null; var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute); if (extractAttributes == null) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy new file mode 100644 index 00000000000..2e771767c22 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy @@ -0,0 +1,45 @@ +// RUN: %resolve "%s" +// Attributes on top-level declarations + +@Options("--function-syntax:3") +module SimpleLinearModule { +} + +function f(x:int) : bool + requires x > 3 +{ + x > 7 +} + +@Compile(true) +@Fuel(low := 1) +@Fuel(low := 1, high := 2) +function g(y:int, b:bool) : bool +{ + if b then f(y + 2) else f(2*y) +} + +@IsolateAssertions +method Test(a: int, b: int, c: int) + requires a < b && b < c +{ + assert a < c; + assert c > a; +} + +datatype Unary = Zero | Succ(Unary) + +function UnaryToNat(n: Unary): nat { + match n + case Zero => 0 + case Succ(p) => 1 + UnaryToNat(p) +} + +function NatToUnary(n: nat): Unary { + if n == 0 then Zero else Succ(NatToUnary(n - 1)) +} + +@Induction(n) +lemma ByInduction(n: int){ + +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy new file mode 100644 index 00000000000..e401748ab3f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -0,0 +1,29 @@ +// RUN: %exits-with -any %resolve "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Attributes on top-level declarations + +function f(x:int) : bool + requires x > 3 +{ + x > 7 +} + +@compile("true") // Should be Compile +@Compile("true") // Should be boolean +@Compile(true, false) // Should have one argument +@fuel(low := 1, 2) // Should be Fuel +@Fuel(2, low := 1) // Wrong position of arguments +function g(y:int, b:bool) : bool +{ + if b then f(y + 2) else f(2*y) +} + +@isolate_assertions // Should be IsolateAssertions +@IsolateAssertions("noargument") // Should have no argument. +// Above is not treated as a @call with label "IsolateAssertion" +method Test(a: int, b: int, c: int) + requires a < b && b < c +{ + assert a < c; + assert c > a; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect new file mode 100644 index 00000000000..17364533b1b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -0,0 +1,8 @@ +at-attributes-typos.dfy(15,9): Error: the parameter named 'low' is already given positionally +at-attributes-typos.dfy(13,8): Error: wrong number of arguments (got 2, but datatype constructor 'Compile' expects at most 1: (0: bool)) +at-attributes-typos.dfy(12,8): Error: incorrect argument type for datatype constructor parameter '0' (expected bool, found string) +at-attributes-typos.dfy(22,18): Error: wrong number of arguments (got 1, but datatype constructor 'IsolateAssertions' expects 0) +at-attributes-typos.dfy(14,1): Error: unresolved identifier: fuel +at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile +at-attributes-typos.dfy(21,1): Error: unresolved identifier: isolate_assertions +7 resolution/type errors detected in at-attributes-typos.dfy diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index 0fc0d11e4a9..db7408470f2 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -32,6 +32,9 @@ public static ILitCommand Parse(string[] args) { public static string? Run(string expectedOutputFile, string actualOutput) { if (UpdateExpectFile) { + if (Path.GetExtension(expectedOutputFile) == ".tmp") { + return "With DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=true, first argument of %diff cannot be a *.tmp file, it should be an *.expect file"; + } var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); File.WriteAllText(path, actualOutput); return null; From 09a845dc4117c9598927a5c5ca732055ef00ba41 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Oct 2024 10:57:48 -0500 Subject: [PATCH 02/20] Fixed class attributes --- Source/DafnyCore/AST/DafnyInterface.dfy | 10 +++++++--- Source/DafnyCore/AST/System.dfy | 10 +++++++--- .../Backends/Rust/Dafny-compiler-rust-proofs.dfy | 3 ++- Source/DafnyCore/Dafny.atg | 2 +- 4 files changed, 17 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/AST/DafnyInterface.dfy b/Source/DafnyCore/AST/DafnyInterface.dfy index 3825f2fd097..ad94ccce0c5 100644 --- a/Source/DafnyCore/AST/DafnyInterface.dfy +++ b/Source/DafnyCore/AST/DafnyInterface.dfy @@ -1,10 +1,13 @@ include "System.dfy" // Interface with existing Dafny code (IToken) -module {:extern "Microsoft.Dafny"} {:compile false} {:options "-functionSyntax:4"} MicrosoftDafny { +@Compile(false) +@Options("-functionSyntax:4") +module {:extern "Microsoft.Dafny"} MicrosoftDafny { import opened System - trait {:extern "IToken"} {:compile false} IToken { + @Compile(false) + trait {:extern "IToken"} IToken { var val: CsString var LeadingTrivia: CsString var TrailingTrivia: CsString @@ -57,7 +60,8 @@ module {:extern "Microsoft.Dafny"} {:compile false} {:options "-functionSyntax:4 } } } - class {:extern "TriviaFormatterHelper"} {:compile false} TriviaFormatterHelper { + @Compile(false) + class {:extern "TriviaFormatterHelper"} TriviaFormatterHelper { static predicate EndsWithNewline(input: CsString) } } diff --git a/Source/DafnyCore/AST/System.dfy b/Source/DafnyCore/AST/System.dfy index 2ecffd39ce3..1ffe067c229 100644 --- a/Source/DafnyCore/AST/System.dfy +++ b/Source/DafnyCore/AST/System.dfy @@ -1,7 +1,10 @@ // Interface with the System namespace -module {:extern "System"} {:compile false} {:options "-functionSyntax:4"} System { - class {:extern "Text.StringBuilder"} {:compile false} CsStringBuilder { +@Options("-functionSyntax:4") +@Compile(false) +module {:extern "System"} System { + @Compile(false) + class {:extern "Text.StringBuilder"} CsStringBuilder { ghost var built: CsString constructor {:extern} () method {:axiom} {:extern "Append"} Append(s: CsString) @@ -28,7 +31,8 @@ module {:extern "System"} {:compile false} {:options "-functionSyntax:4"} System s1.ContainsTransitive(s2, s3); } } - class {:extern "String"} {:compile false} String { + @Compile(false) + class {:extern "String"} String { static function {:axiom} {:extern} Concat(s1: CsString, s2: CsString): (r: CsString) ensures r.Contains(s1) ensures r.Contains(s2) diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy index 9b7e31813f0..611bb413f02 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy @@ -2,7 +2,8 @@ include "../Dafny/AST.dfy" /*This module does not contain any compiled code because it only proves properties about DCOMP. In a sense, it's a test file. */ -module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompilerProofs { +@Compile(false) +module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs { import opened DafnyToRustCompiler import opened DafnyToRustCompilerDefinitions diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 0755626b118..3bef34aad38 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -545,7 +545,7 @@ ClassDecl } "}" - (. c = new ClassDecl(new RangeToken(dmodClass.FirstToken, t), name, module, typeArgs, members, attrs, isRefining, parentTraits); + (. c = new ClassDecl(new RangeToken(dmodClass.FirstToken, t), name, module, typeArgs, members, dmodClass.Attributes, isRefining, parentTraits); c.BodyStartTok = bodyStart; c.TokenWithTrailingDocString = tokenWithTrailingDocString; .) From 53b2a01eed61728c4b6201b4882528bd25bd1237 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Oct 2024 10:59:00 -0500 Subject: [PATCH 03/20] Added missing tests --- .../LitTest/at-attributes/at-attributes-typos0.dfy | 11 +++++++++++ .../at-attributes/at-attributes-typos0.dfy.expect | 3 +++ 2 files changed, 14 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy new file mode 100644 index 00000000000..1eeb43fcb1e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy @@ -0,0 +1,11 @@ +// RUN: %exits-with -any %resolve "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Attributes on top-level declarations + +@Option("--function-syntax:3") // Should be Options +module SimpleLinearModule { +} + +function OtherUnresolvedfunction(): string { + 3 +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect new file mode 100644 index 00000000000..3e99f809de6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect @@ -0,0 +1,3 @@ +at-attributes-typos0.dfy(5,1): Error: unresolved identifier: Option +at-attributes-typos0.dfy(6,7): Error: not resolving module '_module' because there were errors in resolving its nested module 'SimpleLinearModule' +2 resolution/type errors detected in at-attributes-typos0.dfy From 034553cdba8c097746f154d9dbb9a0d44a9e5b9c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Oct 2024 16:34:52 -0500 Subject: [PATCH 04/20] Fixed formatting --- Source/DafnyCore/AST/Attributes.cs | 40 ++++++++++++- .../AST/Expressions/AttributedExpression.cs | 2 +- .../Comprehensions/ComprehensionExpr.cs | 8 +-- .../Conditional/NestedMatchCaseExpr.cs | 3 +- .../AST/Expressions/Variables/LetExpr.cs | 4 +- .../AST/Grammar/ParserNonGeneratedPart.cs | 15 ++++- .../AST/Modules/LiteralModuleDecl.cs | 3 + .../DafnyCore/AST/Modules/ModuleDefinition.cs | 8 +-- .../Statements/Assignment/LocalVariable.cs | 6 +- .../ControlFlow/GuardedAlternative.cs | 3 +- Source/DafnyCore/AST/Statements/Statement.cs | 6 +- .../AST/TypeDeclarations/ClassLikeDecl.cs | 4 ++ .../AST/TypeDeclarations/Declaration.cs | 2 +- Source/DafnyCore/Dafny.atg | 56 +++++++++---------- .../FormatterForTopLevelDeclarations.cs | 25 +++++++++ 15 files changed, 136 insertions(+), 49 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 925f51258b5..4959e12071c 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -40,7 +40,7 @@ public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression } } -public class Attributes : TokenNode { +public class Attributes : TokenNode, ICanFormat { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); @@ -233,8 +233,44 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object : new List { Prev }); public override IEnumerable 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 B(string name) { diff --git a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs index 8ac4b125fa0..b84638e1850 100644 --- a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs +++ b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs @@ -53,7 +53,7 @@ public void AddCustomizedErrorMessage(IToken tok, string s) { } public override IEnumerable Children => - (Attributes != null ? new List() { Attributes } : Enumerable.Empty()).Concat( + Attributes.AsEnumerable().Concat( new List() { E }); public override IEnumerable PreResolveChildren => Children; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index b137babd8de..c72f1c25a02 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -81,12 +81,12 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl } } public override IEnumerable Children => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()). - Concat(BoundVars).Concat(SubExpressions); + Attributes.AsEnumerable(). + Concat(BoundVars).Concat(SubExpressions); public override IEnumerable PreResolveChildren => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()) - .Concat(Range != null && Range.tok.line > 0 ? new List() { Range } : new List()) + Attributes.AsEnumerable() + .Concat(Range != null && Range.tok.line > 0 ? new List() { Range } : new List()) .Concat(Term != null && Term.tok.line > 0 ? new List { Term } : new List()); public override IEnumerable SubExpressions { diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs index 8ed0207b4b5..69f118ad527 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs @@ -17,7 +17,8 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att } public override IEnumerable Children => - (Attributes != null ? new Node[] { Attributes } : Enumerable.Empty()).Concat(new Node[] { Body, Pat }); + Attributes.AsEnumerable(). + Concat(new Node[] { Body, Pat }); public override IEnumerable PreResolveChildren => Children; diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index a71fd261412..792e1a118a0 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -122,8 +122,8 @@ public IEnumerable BoundVars { public IEnumerable AllBoundVars => BoundVars; public override IEnumerable Children => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()) - .Concat(LHSs) + Attributes.AsEnumerable(). + Concat(LHSs) .Concat(base.Children); public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 2284767b3e3..67a60daa61e 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -658,8 +658,21 @@ class DeclModifierData { public IToken StaticToken; public bool IsOpaque; public IToken OpaqueToken; - public IToken FirstToken; + public IToken FirstTokenExceptAttributes; public Attributes Attributes = null; + + public IToken FirstToken { + get { + IToken result = FirstTokenExceptAttributes; + foreach (var attr in Attributes.AsEnumerable()) { + if (result == null || result.pos > attr.tok.pos) { + result = attr.StartToken; + } + } + + return result; + } + } } private ModuleKindEnum GetModuleKind(DeclModifierData mods) { diff --git a/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs b/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs index 215b9a5b0d0..1267e23bf75 100644 --- a/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs @@ -82,6 +82,9 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { } } + Attributes.SetIndents(Attributes, indentBefore, formatter); + Attributes.SetIndents(ModuleDef.Attributes, indentBefore, formatter); + foreach (var decl2 in ModuleDef.TopLevelDecls) { formatter.SetDeclIndentation(decl2, innerIndent); } diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index c7b1b971f80..a21b52e195f 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -405,8 +405,8 @@ public bool IsEssentiallyEmptyModuleBody() { public IToken NavigationToken => tok; public override IEnumerable Children => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()). - Concat(DefaultClasses). + Attributes.AsEnumerable(). + Concat(DefaultClasses). Concat(SourceDecls). Concat(PrefixNamedModules.Any() ? PrefixNamedModules.Select(m => m.Module) : ResolvedPrefixNamedModules). Concat(Implements == null ? Enumerable.Empty() : new Node[] { Implements.Target }); @@ -416,8 +416,8 @@ public bool IsEssentiallyEmptyModuleBody() { public override IEnumerable PreResolveChildren { get { - var attributes = Attributes != null ? new List { Attributes } : Enumerable.Empty(); - return attributes.Concat(preResolveTopLevelDecls ?? TopLevelDecls). + return Attributes.AsEnumerable(). + Concat(preResolveTopLevelDecls ?? TopLevelDecls). Concat(preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Module)); } } diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index c20a0ab46ad..029f71d9e5c 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -133,11 +133,13 @@ public void MakeGhost() { public IToken NavigationToken => RangeToken.StartToken; public bool IsTypeExplicit { get; } public override IEnumerable Children => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( + Attributes.AsEnumerable(). + Concat( IsTypeExplicit ? new List() { type } : Enumerable.Empty()); public override IEnumerable PreResolveChildren => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( + Attributes.AsEnumerable(). + Concat( IsTypeExplicit ? new List() { SyntacticType ?? type } : Enumerable.Empty()); public SymbolKind? Kind => SymbolKind.Variable; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs index 3a9f8444480..9f733b3ee6c 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs @@ -9,7 +9,8 @@ public class GuardedAlternative : TokenNode, IAttributeBearingDeclaration { public readonly Expression Guard; public readonly List Body; public Attributes Attributes { get; set; } - public override IEnumerable Children => (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat(new List() { Guard }).Concat(Body); + public override IEnumerable Children => Attributes.AsEnumerable(). + Concat(new List() { Guard }).Concat(Body); public override IEnumerable PreResolveChildren => Children; [ContractInvariantMethod] diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index 9d1e2ed7f34..fd4c3e14dcd 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -186,11 +186,13 @@ public override string ToString() { } public override IEnumerable Children => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( + Attributes.AsEnumerable(). + Concat( SubStatements.Concat(SubExpressions)); public override IEnumerable PreResolveChildren => - (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat( + Attributes.AsEnumerable(). + Concat( PreResolveSubStatements).Concat(PreResolveSubExpressions); public virtual IEnumerable GetAssignedLocals() => Enumerable.Empty(); diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs index eca519a627e..983e59247f6 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs @@ -42,8 +42,10 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte foreach (var token in OwnedTokens) { switch (token.val) { + case "trait": case "class": { classToken = token; + formatter.SetOpeningIndentedRegion(token, indentBefore); break; } case "extends": { @@ -66,6 +68,8 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte } } + Attributes.SetIndents(Attributes, indentBefore, formatter); + foreach (var parent in ParentTraits) { formatter.SetTypeIndentation(parent); } diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index 44aa0d7d31c..f81818432ed 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -137,7 +137,7 @@ public override string ToString() { // For Boogie internal VerificationIdGenerator IdGenerator = new(); - public override IEnumerable Children => (Attributes != null ? new List { Attributes } : Enumerable.Empty()); + public override IEnumerable Children => Enumerable.Empty(); // Attributes should be enumerated by the parent, as they could be placed in different places public override IEnumerable PreResolveChildren => Children; public abstract SymbolKind? Kind { get; } public abstract string GetDescription(DafnyOptions options); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 3bef34aad38..abcf22bbffa 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -244,11 +244,11 @@ Dafny /*------------------------------------------------------------------------*/ DeclModifier -= ( "abstract" (. dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "replaceable" (. dmod.IsReplaceable = true; CheckAndSetToken(ref dmod.ReplaceableToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "opaque" (. dmod.IsOpaque = true; CheckAndSetToken(ref dmod.OpaqueToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) += ( "abstract" (. dmod.IsAbstract = true; CheckAndSetToken(ref dmod.AbstractToken); CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "replaceable" (. dmod.IsReplaceable = true; CheckAndSetToken(ref dmod.ReplaceableToken); CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "opaque" (. dmod.IsOpaque = true; CheckAndSetToken(ref dmod.OpaqueToken); CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) ) . @@ -317,7 +317,7 @@ SubModuleDecl = "module" - (. CheckAndSetTokenOnce(ref dmod.FirstToken); + (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); Attributes attrs = null; IToken/*!*/ iderr; IToken tokenWithTrailingDocString; @@ -531,7 +531,7 @@ ClassDecl } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) @@ -583,7 +583,7 @@ TraitDecl } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) @@ -650,7 +650,7 @@ DatatypeDecl } DatatypeName [ GenericParameters ] @@ -746,7 +746,7 @@ ConstantFieldDecl<.DeclModifierData dmod, List/*!*/ mm, bool mo CheckDeclModifiers(ref dmod, "field", AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Opaque); .) SYNC - "const" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + "const" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) { Attribute } ( IF(!IsIdentifier(la.kind) && la.kind != _digits) (. SemErr(ErrorId.p_const_decl_missing_identifier, la, "expected an identifier after 'const' and any attributes"); .) @@ -781,7 +781,7 @@ NewtypeDecl var members = new List(); var typeParameters = new List(); .) - "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) { Attribute } NewtypeName [ GenericParameters ] @@ -838,7 +838,7 @@ SynonymTypeDecl(); var isRefining = false; .) - "type" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + "type" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) { Attribute } SynonymTypeName { TypeParameterCharacteristics } @@ -1049,7 +1049,7 @@ IteratorDecl } (. MergeInto(ref attrs, ref dmod.Attributes); .) IteratorName ( @@ -1190,31 +1190,31 @@ MethodDecl .) SYNC ( "method" (. isPlainOlMethod = true; caption = "method"; - CheckAndSetTokenOnce(ref dmod.FirstToken); + CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); allowed = AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static; .) | "lemma" (. isLemma = true; caption = "lemma"; - CheckAndSetTokenOnce(ref dmod.FirstToken); + CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static; .) - | ( "greatest" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + | ( "greatest" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) "lemma" - | "colemma" (. CheckAndSetTokenOnce(ref dmod.FirstToken); + | "colemma" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); errors.Deprecated(ErrorId.p_deprecated_colemma, t, "the old keyword 'colemma' has been renamed to the keyword phrase 'greatest lemma'"); .) ) (. isGreatestLemma = true; caption = "greatest lemma"; allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static; .) - | ( "least" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "inductive" (. CheckAndSetTokenOnce(ref dmod.FirstToken); + | ( "least" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "inductive" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); errors.Deprecated(ErrorId.p_deprecated_inductive_lemma, t, "the old keyword phrase 'inductive lemma' has been renamed to 'least lemma'"); .) ) "lemma" (. isLeastLemma = true; caption = "least lemma"; allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static;.) - | "twostate" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + | "twostate" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) "lemma" (. isTwoStateLemma = true; caption = "two-state lemma"; allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static; .) - | "constructor" (. CheckAndSetTokenOnce(ref dmod.FirstToken); + | "constructor" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); if (allowConstructor) { isConstructor = true; } else { @@ -1748,9 +1748,9 @@ FunctionDecl */ /* ----- function ----- */ - [ "twostate" (. isTwoState = true; CheckAndSetTokenOnce(ref dmod.FirstToken); .) + [ "twostate" (. isTwoState = true; CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) ] - ( "function" (. headToken = t; CheckAndSetTokenOnce(ref dmod.FirstToken); .) + ( "function" (. headToken = t; CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) [ "method" (. functionMethodToken = t; .) ] { Attribute } @@ -1773,7 +1773,7 @@ FunctionDecl ) /* ----- predicate ----- */ - | "predicate" (. headToken = t; isPredicate = true; CheckAndSetTokenOnce(ref dmod.FirstToken); .) + | "predicate" (. headToken = t; isPredicate = true; CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) [ "method" (. functionMethodToken = t; .) ] { Attribute } @@ -1794,8 +1794,8 @@ FunctionDecl /* ----- least predicate ----- */ | (. Contract.Assert(!isTwoState); // the IsFunctionDecl check checks that "twostate" is not followed by "least" .) - ( "least" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | "inductive" (. CheckAndSetTokenOnce(ref dmod.FirstToken); errors.Deprecated(ErrorId.p_deprecated_inductive_predicate, t, "the old keyword phrase 'inductive predicate' has been renamed to 'least predicate'"); .) + ( "least" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) + | "inductive" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); errors.Deprecated(ErrorId.p_deprecated_inductive_predicate, t, "the old keyword phrase 'inductive predicate' has been renamed to 'least predicate'"); .) ) "predicate" (. isLeastPredicate = true; .) @@ -1812,9 +1812,9 @@ FunctionDecl /* ----- greatest predicate ----- */ | (. Contract.Assert(!isTwoState); // the IsFunctionDecl check checks that "twostate" is not followed by "greatest" .) - ( "greatest" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) + ( "greatest" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); .) "predicate" - | "copredicate" (. CheckAndSetTokenOnce(ref dmod.FirstToken); errors.Deprecated(ErrorId.p_deprecated_copredicate, t, "the old keyword 'copredicate' has been renamed to the keyword phrase 'greatest predicate'"); .) + | "copredicate" (. CheckAndSetTokenOnce(ref dmod.FirstTokenExceptAttributes); errors.Deprecated(ErrorId.p_deprecated_copredicate, t, "the old keyword 'copredicate' has been renamed to the keyword phrase 'greatest predicate'"); .) ) (. isGreatestPredicate = true; .) { Attribute } diff --git a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs index e8b59b3c345..b24685d8597 100644 --- a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs +++ b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs @@ -35,10 +35,32 @@ await FormatterWorksFor(@" [Fact] public async Task FormatterWorksForMultipleModules() { await FormatterWorksFor(@" +/* Comment about module */ +@Compile( + false +) +@Options( + ""-functionSyntax:4"" +) module Outer.A { import B import C const a := B.b + C.c + @Compile(false) + module Inner { + } + @Compile(false) + class Test { + } + @Compile(false) + trait TestTrait { + } + + @Compile(false) + datatype TestDatatype = TestDatatype + + @Compile(false) + type T = TestDatatype }"); } @@ -107,6 +129,9 @@ newtype Y [Fact] public async Task FormatWorksForModules() { await FormatterWorksFor(@" +include ""test.dfy"" + +@Compile(true) module AM { class A {} class B {} } From 4c602ceb9fe02b6be3e0648ebe8c7fba2b230340 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Oct 2024 16:48:49 -0500 Subject: [PATCH 05/20] Removed unused "attrs" --- Source/DafnyCore/Dafny.atg | 1 - 1 file changed, 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index abcf22bbffa..188bbaac422 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -522,7 +522,6 @@ ClassDecl parentTraits = new List(); - Attributes attrs = null; bool isRefining = false; List typeArgs = new List(); List members = new List(); From 8aa03354ad2140cdc7fba629712cb2b56354153c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Oct 2024 17:06:42 -0500 Subject: [PATCH 06/20] Fixed traitDecl --- Source/DafnyCore/Dafny.atg | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 188bbaac422..97dc896f662 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -574,7 +574,6 @@ TraitDecl parentTraits = new List(); - Attributes attrs = null; bool isRefining = false; List typeArgs = new List(); //traits should not support type parameters at the moment List members = new List(); @@ -583,7 +582,7 @@ TraitDecl } + { Attribute } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) [ ExtendsClause @@ -595,7 +594,7 @@ TraitDecl } "}" - (. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, attrs, isRefining, parentTraits); + (. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, dmodIn.Attributes, isRefining, parentTraits); trait.BodyStartTok = bodyStart; trait.TokenWithTrailingDocString = tokenWithTrailingDocString; .) From 5930792a1c72949239d6a233ba5a64d067b0d538 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 11 Oct 2024 08:39:54 -0500 Subject: [PATCH 07/20] Added missing iterator attributes --- Source/DafnyCore/Dafny.atg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 97dc896f662..e7f0c14ddcc 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1068,7 +1068,7 @@ IteratorDecl(mod, modAttrs), new Specification(decreases, decrAttrs), req, ens, yieldReq, yieldEns, - body, attrs, signatureEllipsis); + body, dmod.Attributes, signatureEllipsis); iter.BodyStartTok = bodyStart; .) . From 440cb47e96bd061b2693d65340e3f35f6f31afd1 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 11 Oct 2024 09:32:47 -0500 Subject: [PATCH 08/20] Formatting (more) --- Makefile | 1 + .../src/Std/TargetSpecific/Concurrent-go.dfy | 4 ++-- .../src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy | 6 +++--- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 2be7e1665f0..786c00e0a3a 100644 --- a/Makefile +++ b/Makefile @@ -12,6 +12,7 @@ exe: format-dfy: (cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .) + (cd "${DIR}"/Source/DafnyStandardLibraries ; ../../Binaries/Dafny.exe format .) dfy-to-cs: (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh) diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy index 43701986047..ddf6c76c38a 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy @@ -1,7 +1,7 @@ module {:compile false} -{:dummyImportMember "Dummy__", true} -Std.GoConcurrent replaces Concurrent { + {:dummyImportMember "Dummy__", true} + Std.GoConcurrent replaces Concurrent { class {:extern} MutableMap ... { diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy index 77680d67aa6..d0cb9f8d66e 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy @@ -12,9 +12,9 @@ module // across multiple Go files under the same path. // But it makes debugging the translated output a little clearer. {:compile false} -{:extern} -{:dummyImportMember "Dummy__", true} -Std.GoFileIOInternalExterns replaces FileIOInternalExterns { + {:extern} + {:dummyImportMember "Dummy__", true} + Std.GoFileIOInternalExterns replaces FileIOInternalExterns { method {:extern} INTERNAL_ReadBytesFromFile(path: string) From cc6f555f889b84bd5d66648e84c1bcce5f24b029 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 11 Oct 2024 10:51:13 -0500 Subject: [PATCH 09/20] make format and fixed least predicate attribute parsing --- Source/DafnyCore/AST/Attributes.cs | 26 +++++++++---------- Source/DafnyCore/Dafny.atg | 2 +- .../LitTest/dafny0/AttributeChecks.dfy.expect | 5 ++-- .../dafny0/AttributeChecks.dfy.refresh.expect | 5 ++-- 4 files changed, 18 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 4959e12071c..74a508ef79b 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -237,21 +237,21 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { foreach (var token in OwnedTokens) { switch (token.val) { case "}": { - formatter.SetClosingIndentedRegion(token, indentBefore); - break; - } + formatter.SetClosingIndentedRegion(token, indentBefore); + break; + } case "@": { - formatter.SetIndentations(token, indentBefore, indentBefore, indentBefore); - break; - } + formatter.SetIndentations(token, indentBefore, indentBefore, indentBefore); + break; + } case ",": { - formatter.SetDelimiterInsideIndentedRegions(token, indentBefore); - break; - } - case "{" or "{:":{ - formatter.SetOpeningIndentedRegion(token, indentBefore); - break; - } + formatter.SetDelimiterInsideIndentedRegions(token, indentBefore); + break; + } + case "{" or "{:": { + formatter.SetOpeningIndentedRegion(token, indentBefore); + break; + } } } foreach (var arg in Args) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index e7f0c14ddcc..a7fbdde1196 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1797,7 +1797,7 @@ FunctionDecl ) "predicate" (. isLeastPredicate = true; .) - { Attribute } + { Attribute } MethodFunctionName ( [ GenericParameters ] diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect index f621707a483..a325d732f36 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect @@ -378,7 +378,7 @@ module TwoStateAttributes { method {:myAttr old(data), x, y} M(x: int) returns (y: int) - least predicate {:myAttr old(data), x} LP(x: int) + least predicate LP(x: int) least lemma {:myAttr old(data), x} LL(x: int) } @@ -672,7 +672,6 @@ AttributeChecks.dfy(393,17): Error: type of right argument to + (int) must agree AttributeChecks.dfy(404,28): Error: old expressions are not allowed in this context AttributeChecks.dfy(408,19): Error: old expressions are not allowed in this context AttributeChecks.dfy(412,20): Error: old expressions are not allowed in this context -AttributeChecks.dfy(414,29): Error: old expressions are not allowed in this context AttributeChecks.dfy(416,25): Error: old expressions are not allowed in this context AttributeChecks.dfy(429,13): Error: old expressions are not allowed in this context AttributeChecks.dfy(428,13): Error: unresolved identifier: ys @@ -705,4 +704,4 @@ AttributeChecks.dfy(527,10): Error: least lemmas are not allowed to have reads c AttributeChecks.dfy(528,13): Error: least lemmas are not allowed to have modifies clauses AttributeChecks.dfy(533,10): Error: greatest lemmas are not allowed to have reads clauses (they are allowed to read all memory locations) AttributeChecks.dfy(534,13): Error: greatest lemmas are not allowed to have modifies clauses -254 resolution/type errors detected in AttributeChecks.dfy +253 resolution/type errors detected in AttributeChecks.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect index d53ea232024..5f9c3d94c71 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect @@ -378,7 +378,7 @@ module TwoStateAttributes { method {:myAttr old(data), x, y} M(x: int) returns (y: int) - least predicate {:myAttr old(data), x} LP(x: int) + least predicate LP(x: int) least lemma {:myAttr old(data), x} LL(x: int) } @@ -664,7 +664,6 @@ AttributeChecks.dfy(393,17): Error: type of right argument to + (int) must agree AttributeChecks.dfy(404,28): Error: old expressions are not allowed in this context AttributeChecks.dfy(408,19): Error: old expressions are not allowed in this context AttributeChecks.dfy(412,20): Error: old expressions are not allowed in this context -AttributeChecks.dfy(414,29): Error: old expressions are not allowed in this context AttributeChecks.dfy(416,25): Error: old expressions are not allowed in this context AttributeChecks.dfy(429,13): Error: old expressions are not allowed in this context AttributeChecks.dfy(428,13): Error: unresolved identifier: ys @@ -697,4 +696,4 @@ AttributeChecks.dfy(527,10): Error: least lemmas are not allowed to have reads c AttributeChecks.dfy(528,13): Error: least lemmas are not allowed to have modifies clauses AttributeChecks.dfy(533,10): Error: greatest lemmas are not allowed to have reads clauses (they are allowed to read all memory locations) AttributeChecks.dfy(534,13): Error: greatest lemmas are not allowed to have modifies clauses -246 resolution/type errors detected in AttributeChecks.dfy +245 resolution/type errors detected in AttributeChecks.dfy From 0b956b3fd60a9f9fbd465571c09e332af5719729 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 11 Oct 2024 10:55:38 -0500 Subject: [PATCH 10/20] Reverted two tests accidentally modified --- .../LitTests/LitTest/dafny0/AttributeChecks.dfy.expect | 5 +++-- .../LitTest/dafny0/AttributeChecks.dfy.refresh.expect | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect index a325d732f36..f621707a483 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.expect @@ -378,7 +378,7 @@ module TwoStateAttributes { method {:myAttr old(data), x, y} M(x: int) returns (y: int) - least predicate LP(x: int) + least predicate {:myAttr old(data), x} LP(x: int) least lemma {:myAttr old(data), x} LL(x: int) } @@ -672,6 +672,7 @@ AttributeChecks.dfy(393,17): Error: type of right argument to + (int) must agree AttributeChecks.dfy(404,28): Error: old expressions are not allowed in this context AttributeChecks.dfy(408,19): Error: old expressions are not allowed in this context AttributeChecks.dfy(412,20): Error: old expressions are not allowed in this context +AttributeChecks.dfy(414,29): Error: old expressions are not allowed in this context AttributeChecks.dfy(416,25): Error: old expressions are not allowed in this context AttributeChecks.dfy(429,13): Error: old expressions are not allowed in this context AttributeChecks.dfy(428,13): Error: unresolved identifier: ys @@ -704,4 +705,4 @@ AttributeChecks.dfy(527,10): Error: least lemmas are not allowed to have reads c AttributeChecks.dfy(528,13): Error: least lemmas are not allowed to have modifies clauses AttributeChecks.dfy(533,10): Error: greatest lemmas are not allowed to have reads clauses (they are allowed to read all memory locations) AttributeChecks.dfy(534,13): Error: greatest lemmas are not allowed to have modifies clauses -253 resolution/type errors detected in AttributeChecks.dfy +254 resolution/type errors detected in AttributeChecks.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect index 5f9c3d94c71..d53ea232024 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AttributeChecks.dfy.refresh.expect @@ -378,7 +378,7 @@ module TwoStateAttributes { method {:myAttr old(data), x, y} M(x: int) returns (y: int) - least predicate LP(x: int) + least predicate {:myAttr old(data), x} LP(x: int) least lemma {:myAttr old(data), x} LL(x: int) } @@ -664,6 +664,7 @@ AttributeChecks.dfy(393,17): Error: type of right argument to + (int) must agree AttributeChecks.dfy(404,28): Error: old expressions are not allowed in this context AttributeChecks.dfy(408,19): Error: old expressions are not allowed in this context AttributeChecks.dfy(412,20): Error: old expressions are not allowed in this context +AttributeChecks.dfy(414,29): Error: old expressions are not allowed in this context AttributeChecks.dfy(416,25): Error: old expressions are not allowed in this context AttributeChecks.dfy(429,13): Error: old expressions are not allowed in this context AttributeChecks.dfy(428,13): Error: unresolved identifier: ys @@ -696,4 +697,4 @@ AttributeChecks.dfy(527,10): Error: least lemmas are not allowed to have reads c AttributeChecks.dfy(528,13): Error: least lemmas are not allowed to have modifies clauses AttributeChecks.dfy(533,10): Error: greatest lemmas are not allowed to have reads clauses (they are allowed to read all memory locations) AttributeChecks.dfy(534,13): Error: greatest lemmas are not allowed to have modifies clauses -245 resolution/type errors detected in AttributeChecks.dfy +246 resolution/type errors detected in AttributeChecks.dfy From 78d7cf6502ecd7ffa9583487bc0f840515fb8c66 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 15 Oct 2024 16:02:08 -0500 Subject: [PATCH 11/20] Review comments --- Makefile | 4 ++-- Source/DafnyCore/AST/Attributes.cs | 23 +++++++++---------- Source/DafnyCore/Makefile | 5 ++-- .../NameResolutionAndTypeInference.cs | 5 +++- .../at-attributes-typos.dfy.expect | 6 ++--- docs/DafnyRef/Attributes.md | 15 ++++++++++++ docs/dev/news/at-attributes.feat | 1 + 7 files changed, 39 insertions(+), 20 deletions(-) create mode 100644 docs/dev/news/at-attributes.feat diff --git a/Makefile b/Makefile index 786c00e0a3a..297ffa16b81 100644 --- a/Makefile +++ b/Makefile @@ -11,8 +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/DafnyStandardLibraries ; ../../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) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 74a508ef79b..db9a6833403 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -273,7 +273,7 @@ public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndent } private static string TupleItem0Name => "0"; // Helper to create a built-in @-attribute - static BuiltInAtAttributeSyntax B(string name) { + static BuiltInAtAttributeSyntax BuiltIn(string name) { return new BuiltInAtAttributeSyntax( name, new List()); } @@ -293,7 +293,7 @@ private static Attributes A1(string name, ActualBindings bindings) { } // 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 + // or mark it as not built-in for later resolution public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute) { var toMatch = atAttribute.Arg; var name = atAttribute.UserSuppliedName; @@ -311,7 +311,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib if (name != "Induction" && name != "Trigger") { var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray(); - ResolveLikeDatatypeConstructor(program, formals, name, toMatch.tok, bindings); + ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings); } // For @Induction and @Trigger, resolution is done in the generated version of the attributes atAttribute.Builtin = true; @@ -355,14 +355,14 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib // This list could be obtained from parsing and resolving a .Dfy file // but for now it's good enough. public static readonly List BuiltinAtAttributes = new() { - B("Compile").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true)), - B("Fuel") + BuiltIn("Compile").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true)), + BuiltIn("Fuel") .WithArg("low", Type.Int, DefaultInt(1)) .WithArg("high", Type.Int, DefaultInt(2)) .WithArg("functionName", Type.ResolvedString(), DefaultString("")), - B("Induction"), // Resolution is different - B("IsolateAssertions"), - B("Options").WithArg(TupleItem0Name, Type.ResolvedString()), + BuiltIn("Induction"), // Resolution is different + BuiltIn("IsolateAssertions"), + BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()), }; ////// Helpers to create default values for the @-attribute definitions above ////// @@ -399,16 +399,15 @@ private static bool Get(ActualBindings bindings, int i, out Expression expr) { // obtained from built-in @-attribute definitions private static void ResolveLikeDatatypeConstructor( Program program, Formal[] formals, string attrName, - IToken attrsTok, ActualBindings bindings) { + UserSuppliedAtAttribute attrs, ActualBindings bindings) { var datatypeName = new Name(RangeToken.NoToken, attrName); - var datatypeCtor = new DatatypeCtor(RangeToken.NoToken, datatypeName, false, formals.ToList(), null); var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ; var typeMap = new Dictionary(); var resolver = new ModuleResolver(new ProgramResolver(program), program.Options); resolver.reporter = program.Reporter; resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo; - resolver.ResolveActualParameters(bindings, formals.ToList(), attrsTok, - datatypeCtor, resolutionContext, typeMap, null); + resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.tok, + attrs, resolutionContext, typeMap, null); resolver.FillInDefaultValueExpressions(); resolver.SolveAllTypeConstraints(); } diff --git a/Source/DafnyCore/Makefile b/Source/DafnyCore/Makefile index 60c0ad6123e..10976e977d3 100644 --- a/Source/DafnyCore/Makefile +++ b/Source/DafnyCore/Makefile @@ -3,6 +3,7 @@ # nmake that. --KRML GENERATED_FROM_DAFNY=GeneratedFromDafny REGENERATED_FROM_DAFNY=GeneratedFromDafnyRegenerated +DAFNY = dotnet run --project ../Dafny --no-build --roll-forward LatestMajor -- all: Parser.cs @@ -23,10 +24,10 @@ test: build-regenerated-from-dafny rm -rf ../DafnyCore.Test/$(REGENERATED_FROM_DAFNY) format: - ../../Scripts/dafny format . + $(DAFNY) format . check-format: - ../../Scripts/dafny format . --check + $(DAFNY) format . --check extract: (cd Prelude; make; cd ..) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index d6950c5f50c..8d7c44bcf6b 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3210,7 +3210,7 @@ internal void ResolveActualParameters(ActualBindings bindings, List form Contract.Requires(bindings != null); Contract.Requires(formals != null); Contract.Requires(callTok != null); - Contract.Requires(context is Method || context is Function || context is DatatypeCtor || context is ArrowType); + Contract.Requires(context is Method || context is Function || context is DatatypeCtor || context is ArrowType || context is UserSuppliedAtAttribute); Contract.Requires(typeMap != null); Contract.Requires(!bindings.WasResolved); @@ -3225,6 +3225,9 @@ internal void ResolveActualParameters(ActualBindings bindings, List form } else if (context is DatatypeCtor cCtor) { whatKind = "datatype constructor"; name = $"{whatKind} '{cCtor.Name}'"; + } else if (context is UserSuppliedAtAttribute usaa) { + whatKind = "attribute"; + name = $"{whatKind} '{usaa.UserSuppliedName}'"; } else { var cArrowType = (ArrowType)context; whatKind = "function application"; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect index 17364533b1b..71df34ea368 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -1,7 +1,7 @@ at-attributes-typos.dfy(15,9): Error: the parameter named 'low' is already given positionally -at-attributes-typos.dfy(13,8): Error: wrong number of arguments (got 2, but datatype constructor 'Compile' expects at most 1: (0: bool)) -at-attributes-typos.dfy(12,8): Error: incorrect argument type for datatype constructor parameter '0' (expected bool, found string) -at-attributes-typos.dfy(22,18): Error: wrong number of arguments (got 1, but datatype constructor 'IsolateAssertions' expects 0) +at-attributes-typos.dfy(13,20): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool)) +at-attributes-typos.dfy(12,15): Error: incorrect argument type for attribute parameter '0' (expected bool, found string) +at-attributes-typos.dfy(22,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) at-attributes-typos.dfy(14,1): Error: unresolved identifier: fuel at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile at-attributes-typos.dfy(21,1): Error: unresolved identifier: isolate_assertions diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index baf0bbf484b..0a85c695eb8 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -1,4 +1,5 @@ # 11. Attributes {#sec-attributes} + Dafny allows many of its entities to be annotated with _Attributes_. Attributes are declared between `{:` and `}` like this: @@ -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. + +Dafny rewrites `@`-attributes to old-style equivalent attribute, after type-checking them. The definition of these attributes would look something like this currently+: + +``` +datatype Attribute = + Fuel(low: int, high: int := low + 1, functionName: string := "") + | Options(string) + | Compile(bool) + | IsolateAssertions + | Induction(...) // Anything here +``` + ## 11.1. Attributes on top-level declarations ### 11.1.1. `{:autocontracts}` {#sec-attributes-autocontracts} @@ -276,6 +290,7 @@ although it is free to read and write newly allocated objects. See [`{:extern }`](#sec-extern). ### 11.2.8. `{:fuel X}` {#sec-fuel} + The fuel attribute is used to specify how much "fuel" a function should have, i.e., how many times the verifier is permitted to unfold its definition. The `{:fuel}` annotation can be added to the function itself, in which diff --git a/docs/dev/news/at-attributes.feat b/docs/dev/news/at-attributes.feat new file mode 100644 index 00000000000..ac6b88ca2fe --- /dev/null +++ b/docs/dev/news/at-attributes.feat @@ -0,0 +1 @@ +Support for Top-level @-attributes \ No newline at end of file From 7f24f81901375f974ec8c44eb0f8cf29a484ef34 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 16 Oct 2024 14:34:36 -0500 Subject: [PATCH 12/20] Resolution of attributes ensures arguments are literals --- Source/DafnyCore/AST/Attributes.cs | 7 ++++++- Source/DafnyCore/Dafny.atg | 1 - .../LitTest/at-attributes/at-attributes-typos.dfy | 1 + .../at-attributes/at-attributes-typos.dfy.expect | 11 ++++++----- 4 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index db9a6833403..a0fe3968a20 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -400,7 +400,6 @@ private static bool Get(ActualBindings bindings, int i, out Expression expr) { private static void ResolveLikeDatatypeConstructor( Program program, Formal[] formals, string attrName, UserSuppliedAtAttribute attrs, ActualBindings bindings) { - var datatypeName = new Name(RangeToken.NoToken, attrName); var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ; var typeMap = new Dictionary(); var resolver = new ModuleResolver(new ProgramResolver(program), program.Options); @@ -410,6 +409,12 @@ private static void ResolveLikeDatatypeConstructor( 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 diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index a7fbdde1196..9289a4f8380 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1694,7 +1694,6 @@ FunctionDecl List ens = new List(); List reads = new List(); List decreases; - Attributes attrs = null; Attributes decAttrs = null; Attributes readsAttrs = null; Expression body = null; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index e401748ab3f..309e33e82e3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -11,6 +11,7 @@ function f(x:int) : bool @compile("true") // Should be Compile @Compile("true") // Should be boolean @Compile(true, false) // Should have one argument +@Compile(true && false) @fuel(low := 1, 2) // Should be Fuel @Fuel(2, low := 1) // Wrong position of arguments function g(y:int, b:bool) : bool diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect index 71df34ea368..88deab2c752 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -1,8 +1,9 @@ -at-attributes-typos.dfy(15,9): Error: the parameter named 'low' is already given positionally +at-attributes-typos.dfy(16,9): Error: the parameter named 'low' is already given positionally +at-attributes-typos.dfy(14,9): Error: Argument to attribute Compile must be a literal at-attributes-typos.dfy(13,20): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool)) at-attributes-typos.dfy(12,15): Error: incorrect argument type for attribute parameter '0' (expected bool, found string) -at-attributes-typos.dfy(22,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) -at-attributes-typos.dfy(14,1): Error: unresolved identifier: fuel +at-attributes-typos.dfy(23,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) +at-attributes-typos.dfy(15,1): Error: unresolved identifier: fuel at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile -at-attributes-typos.dfy(21,1): Error: unresolved identifier: isolate_assertions -7 resolution/type errors detected in at-attributes-typos.dfy +at-attributes-typos.dfy(22,1): Error: unresolved identifier: isolate_assertions +8 resolution/type errors detected in at-attributes-typos.dfy From 91667fcac0d400e6d05bb530d71d144186f5022c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 17 Oct 2024 10:50:47 -0500 Subject: [PATCH 13/20] Removed induction --- Source/DafnyCore/AST/Attributes.cs | 12 +++--------- .../at-attributes-acceptable-builtin.dfy | 17 ----------------- docs/DafnyRef/Attributes.md | 1 - 3 files changed, 3 insertions(+), 27 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index a0fe3968a20..bc86e44a3c9 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -309,10 +309,8 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib return null; } - if (name != "Induction" && name != "Trigger") { - var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray(); - ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings); - } // For @Induction and @Trigger, resolution is done in the generated version of the attributes + 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 @@ -336,9 +334,6 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib return A("fuel"); } - case "Induction": { - return A("induction", bindings.ArgumentBindings.Select(binding => binding.Actual).ToArray()); - } case "IsolateAssertions": { return A("isolate_assertions"); } @@ -360,7 +355,6 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib .WithArg("low", Type.Int, DefaultInt(1)) .WithArg("high", Type.Int, DefaultInt(2)) .WithArg("functionName", Type.ResolvedString(), DefaultString("")), - BuiltIn("Induction"), // Resolution is different BuiltIn("IsolateAssertions"), BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()), }; @@ -414,7 +408,7 @@ private static void ResolveLikeDatatypeConstructor( 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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy index 2e771767c22..f2aedb6d4e9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy @@ -26,20 +26,3 @@ method Test(a: int, b: int, c: int) assert a < c; assert c > a; } - -datatype Unary = Zero | Succ(Unary) - -function UnaryToNat(n: Unary): nat { - match n - case Zero => 0 - case Succ(p) => 1 + UnaryToNat(p) -} - -function NatToUnary(n: nat): Unary { - if n == 0 then Zero else Succ(NatToUnary(n - 1)) -} - -@Induction(n) -lemma ByInduction(n: int){ - -} \ No newline at end of file diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 0a85c695eb8..ebfc5f8a1f1 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -43,7 +43,6 @@ datatype Attribute = | Options(string) | Compile(bool) | IsolateAssertions - | Induction(...) // Anything here ``` ## 11.1. Attributes on top-level declarations From 1bf9c63fb3faa44620bfd973726cdf069f1dec0f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 17 Oct 2024 13:10:01 -0500 Subject: [PATCH 14/20] Fixed the doc --- docs/DafnyRef/Attributes.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index ebfc5f8a1f1..0a8c7fb3f93 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -37,7 +37,8 @@ with no argument is interpreted as if it were true. Dafny rewrites `@`-attributes to old-style equivalent attribute, after type-checking them. The definition of these attributes would look something like this currently+: -``` + +```dafny datatype Attribute = Fuel(low: int, high: int := low + 1, functionName: string := "") | Options(string) From 2f9dfb72ad6b2fabc0990e12a23dadc6a0855042 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 17 Oct 2024 16:31:35 -0500 Subject: [PATCH 15/20] Review comment: Ensure we check whether attributes can be applied correctly --- Source/DafnyCore/AST/Attributes.cs | 34 ++++++++++++++----- .../AST/Expressions/AttributedExpression.cs | 2 ++ .../Conditional/NestedMatchCaseExpr.cs | 2 ++ .../Conditional/NestedMatchCaseStmt.cs | 1 + .../AST/Expressions/Specification.cs | 1 + .../AST/Expressions/Variables/LetExpr.cs | 1 + .../DafnyCore/AST/Modules/ModuleDefinition.cs | 1 + .../Statements/Assignment/AssignmentRhs.cs | 1 + .../Statements/Assignment/AttributedToken.cs | 1 + .../Statements/Assignment/LocalVariable.cs | 1 + .../ControlFlow/GuardedAlternative.cs | 1 + Source/DafnyCore/AST/Statements/Statement.cs | 1 + .../AST/TypeDeclarations/Declaration.cs | 6 ++++ .../DafnyCore/Rewriters/ExpandAtAttributes.cs | 2 +- .../at-attributes/at-attributes-typos.dfy | 19 +++++++++++ .../at-attributes-typos.dfy.expect | 12 +++++-- 16 files changed, 74 insertions(+), 12 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index bc86e44a3c9..3de7f90a2c4 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -32,12 +32,17 @@ public Formal ToFormal() { // To create such an attribute, use the Attributes.B() helper public record BuiltInAtAttributeSyntax( string Name, - List Args) { + List Args, + Func CanBeApplied) { public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) { var c = new List(Args) { new(argName, argType, defaultValue) }; return this with { Args = c }; } + + public BuiltInAtAttributeSyntax Filter(Func canBeApplied) { + return this with { CanBeApplied = canBeApplied }; + } } public class Attributes : TokenNode, ICanFormat { @@ -275,7 +280,7 @@ public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndent // Helper to create a built-in @-attribute static BuiltInAtAttributeSyntax BuiltIn(string name) { return new BuiltInAtAttributeSyntax( - name, new List()); + name, new List(), _ => true); } // Helper to create an old-style attribute @@ -294,13 +299,13 @@ private static Attributes A1(string name, ActualBindings bindings) { // 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) { + 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()); + program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString()); return null; } @@ -309,6 +314,10 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib 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); @@ -350,13 +359,19 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib // This list could be obtained from parsing and resolving a .Dfy file // but for now it's good enough. public static readonly List BuiltinAtAttributes = new() { - BuiltIn("Compile").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true)), + 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("")), - BuiltIn("IsolateAssertions"), - BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()), + .WithArg("functionName", Type.ResolvedString(), DefaultString("")) + .Filter(attributeHost => attributeHost is Function), + BuiltIn("IsolateAssertions") + .Filter(attributeHost => attributeHost is MemberDecl), + BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()) + .Filter(attributeHost => attributeHost is ModuleDecl), }; ////// Helpers to create default values for the @-attribute definitions above ////// @@ -555,6 +570,8 @@ public static IEnumerable GetPreResolveArguments(Attributes a) { public static IEnumerable GetUserSuppliedArguments(Attributes a) { return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args; } + + public override string ToString() => Prev + (Prev == null ? "" : " ") + "@" + Arg; } /// @@ -562,6 +579,7 @@ public static IEnumerable GetUserSuppliedArguments(Attributes a) { /// public interface IAttributeBearingDeclaration { Attributes Attributes { get; internal set; } + string WhatKind { get; } } public static class AttributeBearingDeclarationExtensions { diff --git a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs index b84638e1850..467e4a5ba16 100644 --- a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs +++ b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs @@ -22,6 +22,8 @@ public Attributes Attributes { attributes = value; } } + + string IAttributeBearingDeclaration.WhatKind => "expression"; public override RangeToken RangeToken => E.RangeToken; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs index 69f118ad527..ddab5b33980 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs @@ -9,6 +9,8 @@ namespace Microsoft.Dafny; public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration { public Expression Body; public Attributes Attributes { get; set; } + + string IAttributeBearingDeclaration.WhatKind => "match expression case"; public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) { Contract.Requires(body != null); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs index 4146864cdb2..a261b61b4dd 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs @@ -8,6 +8,7 @@ namespace Microsoft.Dafny; public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration, ICloneable { public readonly List Body; public Attributes Attributes { get; set; } + string IAttributeBearingDeclaration.WhatKind => "match statement case"; public NestedMatchCaseStmt(RangeToken rangeToken, ExtendedPattern pat, List body) : base(rangeToken.StartToken, pat) { RangeToken = rangeToken; Contract.Requires(body != null); diff --git a/Source/DafnyCore/AST/Expressions/Specification.cs b/Source/DafnyCore/AST/Expressions/Specification.cs index fc0a5ef3710..6bcf78867ad 100644 --- a/Source/DafnyCore/AST/Expressions/Specification.cs +++ b/Source/DafnyCore/AST/Expressions/Specification.cs @@ -24,6 +24,7 @@ public Specification(List exprs, Attributes attrs) { } public Attributes Attributes { get; set; } + string IAttributeBearingDeclaration.WhatKind => "specification clause"; public bool HasAttributes() { return Attributes != null; diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index 792e1a118a0..04f606740a9 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -10,6 +10,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression public Attributes Attributes { get; set; } + string IAttributeBearingDeclaration.WhatKind => "let expression"; [FilledInDuringResolution] public List Constraint_Bounds; // null for Exact=true and for when expression is in a ghost context // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count; private Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 60cd8013620..e5ba6b77d2a 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -72,6 +72,7 @@ public string FullName { // nested module declaration is outside its enclosing module public ModuleDefinition EnclosingModule; // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered public Attributes Attributes { get; set; } + public string WhatKind => "module definition"; public readonly Implements Implements; // null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved public readonly ModuleKindEnum ModuleKind; diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignmentRhs.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignmentRhs.cs index 6dcef77ae92..07d1fd50d83 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignmentRhs.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignmentRhs.cs @@ -10,6 +10,7 @@ public Attributes Attributes { get { return attributes; } set { attributes = value; } } + string IAttributeBearingDeclaration.WhatKind => "assignment right-hand-side"; public bool HasAttributes() { return Attributes != null; diff --git a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs index a1f60a99abc..2a9f001fcb9 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs @@ -16,4 +16,5 @@ Attributes IAttributeBearingDeclaration.Attributes { get => Attrs; set => throw new System.NotImplementedException(); } + string IAttributeBearingDeclaration.WhatKind => "token"; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index 029f71d9e5c..c7588f3285b 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -13,6 +13,7 @@ Attributes IAttributeBearingDeclaration.Attributes { get => Attributes; set => Attributes = value; } + string IAttributeBearingDeclaration.WhatKind => "local variable"; public bool IsGhost; [ContractInvariantMethod] diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs index 9f733b3ee6c..509c8257f01 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs @@ -9,6 +9,7 @@ public class GuardedAlternative : TokenNode, IAttributeBearingDeclaration { public readonly Expression Guard; public readonly List Body; public Attributes Attributes { get; set; } + string IAttributeBearingDeclaration.WhatKind => "alternative-based case"; public override IEnumerable Children => Attributes.AsEnumerable(). Concat(new List() { Guard }).Concat(Body); public override IEnumerable PreResolveChildren => Children; diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index fd4c3e14dcd..1d9f58bcdfa 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -21,6 +21,7 @@ public Attributes Attributes { attributes = value; } } + string IAttributeBearingDeclaration.WhatKind => "statement"; [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index f81818432ed..175f4f6f249 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -128,6 +128,12 @@ Attributes IAttributeBearingDeclaration.Attributes { get => Attributes; set => Attributes = value; } + string IAttributeBearingDeclaration.WhatKind => + this is TopLevelDecl topLevelDecl + ? topLevelDecl.WhatKind + : this is MemberDecl memberDecl + ? memberDecl.WhatKind + : "declaration"; [Pure] public override string ToString() { diff --git a/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs index 28a31de1e1b..a00539e55ec 100644 --- a/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs +++ b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs @@ -30,7 +30,7 @@ internal override void PreResolve(Program program) { continue; } - var newAttributes = Attributes.ExpandAtAttribute(program, userSuppliedAtAttribute); + var newAttributes = Attributes.ExpandAtAttribute(program, userSuppliedAtAttribute, attributeHost); Attributes.MergeInto(ref newAttributes, ref extraAttrs); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index 309e33e82e3..b750a00f901 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -19,6 +19,25 @@ function g(y:int, b:bool) : bool if b then f(y + 2) else f(2*y) } +@Fuel(1, 2) // Fuel not supported on datatype +datatype Useless = Useless + +@Fuel(1, 2) // Fuel not supported on codatatype +codatatype UselessCodatatype = UselessCodatatype + +@Fuel(1, 2) // Fuel not supported on method +method g_method() { +} + +@Fuel(1, 2) // Fuel not supported on type synonyms +type NewInt = int + +@Fuel(1, 2) // Fuel not supported on subset types +type NewInt2 = x: int | x >= 0 witness * + +@Fuel(1, 2) // Fuel not supported on subset types +newtype NewInt3 = int + @isolate_assertions // Should be IsolateAssertions @IsolateAssertions("noargument") // Should have no argument. // Above is not treated as a @call with label "IsolateAssertion" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect index 88deab2c752..48033188dac 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -2,8 +2,14 @@ at-attributes-typos.dfy(16,9): Error: the parameter named 'low' is already given at-attributes-typos.dfy(14,9): Error: Argument to attribute Compile must be a literal at-attributes-typos.dfy(13,20): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool)) at-attributes-typos.dfy(12,15): Error: incorrect argument type for attribute parameter '0' (expected bool, found string) -at-attributes-typos.dfy(23,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) +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 +at-attributes-typos.dfy(25,0): Error: @Fuel attribute cannot be applied to codatatype +at-attributes-typos.dfy(32,0): Error: @Fuel attribute cannot be applied to type synonym +at-attributes-typos.dfy(35,0): Error: @Fuel attribute cannot be applied to subset type +at-attributes-typos.dfy(38,0): Error: @Fuel attribute cannot be applied to newtype at-attributes-typos.dfy(15,1): Error: unresolved identifier: fuel at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile -at-attributes-typos.dfy(22,1): Error: unresolved identifier: isolate_assertions -8 resolution/type errors detected in at-attributes-typos.dfy +at-attributes-typos.dfy(41,1): Error: unresolved identifier: isolate_assertions +14 resolution/type errors detected in at-attributes-typos.dfy From 1f817437ae94b4a8d5fb13d175ed2c447b4d55c8 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 17 Oct 2024 16:39:32 -0500 Subject: [PATCH 16/20] Fixed CI --- Source/DafnyCore/AST/Attributes.cs | 2 +- Source/DafnyCore/AST/Expressions/AttributedExpression.cs | 2 +- .../AST/Expressions/Conditional/NestedMatchCaseExpr.cs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 3de7f90a2c4..ab946a79c67 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -371,7 +371,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib BuiltIn("IsolateAssertions") .Filter(attributeHost => attributeHost is MemberDecl), BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()) - .Filter(attributeHost => attributeHost is ModuleDecl), + .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition), }; ////// Helpers to create default values for the @-attribute definitions above ////// diff --git a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs index 467e4a5ba16..19bc7d7a847 100644 --- a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs +++ b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs @@ -22,7 +22,7 @@ public Attributes Attributes { attributes = value; } } - + string IAttributeBearingDeclaration.WhatKind => "expression"; public override RangeToken RangeToken => E.RangeToken; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs index ddab5b33980..613a2f6aa96 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny; public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration { public Expression Body; public Attributes Attributes { get; set; } - + string IAttributeBearingDeclaration.WhatKind => "match expression case"; public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) { From 73ce2b066090b55994606007908d83cd19743f43 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 06:36:15 -0500 Subject: [PATCH 17/20] Missing filter cases --- Source/DafnyCore/AST/Attributes.cs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index ab946a79c67..a48569b8806 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -369,8 +369,9 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib .WithArg("functionName", Type.ResolvedString(), DefaultString("")) .Filter(attributeHost => attributeHost is Function), BuiltIn("IsolateAssertions") - .Filter(attributeHost => attributeHost is MemberDecl), - BuiltIn("Options").WithArg(TupleItem0Name, Type.ResolvedString()) + .Filter(attributeHost => attributeHost is MemberDecl or DatatypeDecl or RedirectingTypeDecl), + BuiltIn("Options") + .WithArg(TupleItem0Name, Type.ResolvedString()) .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition), }; From 0e988bcb210e490b575770d23eb0c0d7b93fc417 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 10:19:44 -0500 Subject: [PATCH 18/20] ICanVerify is more general + Forward-compatibility for {:fuel} on AssertStmt --- Source/DafnyCore/AST/Attributes.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index a48569b8806..69d5cfe7d8f 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -367,9 +367,9 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib .WithArg("low", Type.Int, DefaultInt(1)) .WithArg("high", Type.Int, DefaultInt(2)) .WithArg("functionName", Type.ResolvedString(), DefaultString("")) - .Filter(attributeHost => attributeHost is Function), + .Filter(attributeHost => attributeHost is Function or AssertStmt), BuiltIn("IsolateAssertions") - .Filter(attributeHost => attributeHost is MemberDecl or DatatypeDecl or RedirectingTypeDecl), + .Filter(attributeHost => attributeHost is ICanVerify), BuiltIn("Options") .WithArg(TupleItem0Name, Type.ResolvedString()) .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition), From 858c8237bf0f39e16f2894a70a89eaebd1a935d4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 11:16:02 -0500 Subject: [PATCH 19/20] Updated documentation --- docs/DafnyRef/Attributes.md | 51 ++++++++++++++++++++++++-------- docs/dev/news/at-attributes.feat | 2 +- 2 files changed, 39 insertions(+), 14 deletions(-) diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 0a8c7fb3f93..dedf49f11e4 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -33,19 +33,6 @@ 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. - -Dafny rewrites `@`-attributes to old-style equivalent attribute, after type-checking them. The definition of these attributes would look something like this currently+: - - -```dafny -datatype Attribute = - Fuel(low: int, high: int := low + 1, functionName: string := "") - | Options(string) - | Compile(bool) - | IsolateAssertions -``` - ## 11.1. Attributes on top-level declarations ### 11.1.1. `{:autocontracts}` {#sec-attributes-autocontracts} @@ -1016,4 +1003,42 @@ following attributes. * `{:weight}` * `{:yields}` +## 11.9. New attribute syntax {#sec-at-attributes} + +There is a new syntax for typed prefix attributes that is being added: `@Attribute(...)`. +For now, the new syntax works only as top-level declarations. When all previous attributes will be migrated, this section will be rewritten. For example, you can write + + +```dafny +@IsolateAssertions +method Test() { +} +``` + +instead of + + +```dafny +method {:isolate_assertions} Test() { +} +``` + + +Dafny rewrites `@`-attributes to old-style equivalent attribute. The definition of these attributes is similar to the following+: + + +```dafny +datatype Attribute = + Fuel(low: int, high: int := low + 1, functionName: string := "") + | Options(string) + | Compile(bool) + | IsolateAssertions +``` + +@-attributes have the same checks as regular resolved datatype values +* The attribute should exist +* Arguments should be compatible with the parameters, like for a datatype constructor call +However, @-attributes have more checks: +* The attribute should be applied to a place where it can be used by Dafny +* Arguments should be literals diff --git a/docs/dev/news/at-attributes.feat b/docs/dev/news/at-attributes.feat index ac6b88ca2fe..a3baa4e8b82 100644 --- a/docs/dev/news/at-attributes.feat +++ b/docs/dev/news/at-attributes.feat @@ -1 +1 @@ -Support for Top-level @-attributes \ No newline at end of file +Support for [top-level @-attributes](https://dafny.org/latest/DafnyRef/DafnyRef#sec-at-attributes) \ No newline at end of file From 6a88606e4d1cca4bae230ba17fcaee6f85f40ec2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 11:33:15 -0500 Subject: [PATCH 20/20] Code review --- docs/DafnyRef/Attributes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index dedf49f11e4..b62fa757116 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -1024,7 +1024,7 @@ method {:isolate_assertions} Test() { ``` -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: ```dafny