From 676d2454aee131bdc74f4524fdb563eee9efaa6a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 9 Oct 2024 10:27:21 -0500 Subject: [PATCH] Feat: @-attributes on top-level declarations --- Source/DafnyCore/AST/Attributes.cs | 290 +++++++++++++++++- 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 | 53 +++- .../Statements/Assignment/AttributedToken.cs | 5 +- .../Statements/Assignment/LocalVariable.cs | 6 +- .../AST/TypeDeclarations/Declaration.cs | 5 +- Source/DafnyCore/AST/Types/Types.cs | 4 + 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 +- .../Handlers/DafnyCompletionHandler.cs | 88 +++++- .../Workspace/ProjectManager.cs | 5 + .../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 + 24 files changed, 698 insertions(+), 82 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..2df671a3d7f 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,197 @@ 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 +438,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 +455,81 @@ 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..63670ea3084 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -390,9 +390,20 @@ 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..0504d0cda0d 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny; public partial class Parser { - + public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, CancellationToken cancellationToken) : this(scanner, errors, cancellationToken) // the real work { @@ -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..85478b71662 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -17,6 +17,10 @@ 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/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 9bf8edc6313..80f646a3ebc 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -32,7 +32,7 @@ protected override CompletionRegistrationOptions CreateRegistrationOptions(Compl return new CompletionRegistrationOptions { DocumentSelector = DocumentSelector.ForLanguage("dafny"), ResolveProvider = false, - TriggerCharacters = new Container(".") + TriggerCharacters = new Container(".", "@") }; } @@ -49,7 +49,7 @@ public override async Task Handle(CompletionParams request, Canc logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return new CompletionList(); } - return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options).Process(); + return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, await projects.GetProjectManager(request.TextDocument.Uri)).Process(); } private class CompletionProcessor { @@ -59,15 +59,18 @@ private class CompletionProcessor { private readonly IdeState state; private readonly CompletionParams request; private readonly CancellationToken cancellationToken; + private readonly ProjectManager? projectManager; public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger logger, IdeState state, - CompletionParams request, CancellationToken cancellationToken, DafnyOptions options) { + CompletionParams request, CancellationToken cancellationToken, DafnyOptions options, + ProjectManager? projectManager) { this.symbolGuesser = symbolGuesser; this.state = state; this.request = request; this.cancellationToken = cancellationToken; this.options = options; this.logger = logger; + this.projectManager = projectManager; } public CompletionList Process() { @@ -75,6 +78,10 @@ public CompletionList Process() { return CreateDotCompletionList(); } + if (IsAtAttribute()) { + return CreateAtAttributeCompletionList(); + } + if (logger.IsEnabled(LogLevel.Trace)) { var program = (Program)state.ResolvedProgram!; var writer = new StringWriter(); @@ -86,11 +93,77 @@ public CompletionList Process() { return new CompletionList(); } + private static string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) + { + // To track the last two characters + char? prevChar = null; + char? currentChar = null; + + // Read line by line + for (int lineNum = 0; lineNum <= position.Line; lineNum++) + { + string? line = fileContent.ReadLine(); + if (line == null) + { + throw new InvalidOperationException("Reached end of file before finding the specified line."); + } + + // If we are on the line of the specified position, handle the partial line case + if (lineNum == position.Line) + { + int columnIndex = position.Column - 1; // Convert 1-based to 0-based index + for (int i = 0; i <= columnIndex; i++) + { + prevChar = currentChar; + currentChar = line[i]; + } + break; + } + else + { + // Otherwise, track the last two characters of this full line (including newline) + foreach (char c in line + '\n') // Include '\n' for line end tracking + { + prevChar = currentChar; + currentChar = c; + } + } + } + + // Handle case where fewer than 2 characters are available + if (prevChar == null) + { + return currentChar?.ToString() ?? ""; + } + return $"{prevChar}{currentChar}"; + } + private bool IsDotExpression() { var node = state.Program.FindNode(request.TextDocument.Uri.ToUri(), request.Position.ToDafnyPosition()); return node?.RangeToken.EndToken.val == "."; } + private bool IsAtAttribute() { + var position = request.Position.ToDafnyPosition(); + if (projectManager == null) { + return false; + } + var fileContent = projectManager.ReadFile(request.TextDocument.Uri.ToUri()); + var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position); + var isAtAttribute = + lastTwoChars == "@" || + lastTwoChars.Length >= 2 && lastTwoChars[1] == '@' && char.IsWhiteSpace(lastTwoChars[0]); + return isAtAttribute; + } + + private CompletionList CreateAtAttributeCompletionList() { + var completionItems = + Attributes.BuiltinAtAttributes.Select(b => + CreateCompletionItem(b.Name) + ).ToList(); + return new CompletionList(completionItems); + } + private CompletionList CreateDotCompletionList() { IEnumerable members; if (symbolGuesser.TryGetTypeBefore(state, @@ -121,6 +194,15 @@ private CompletionList CreateCompletionListFromSymbols(IEnumerable 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;