More @-attributes supported, top-level declarations and members (#5916)

### Description
This PR adds most remaining @-attributes on several top-level
declarations and members
I updated the documentation about these new @-attributes.
- Fixed the wrong documentation for `{:disableNonlinearArithmetic}`

### How has this been tested?
- Positive tests added to ensure the new @-attributes are supported
- Negative typo tests to ensure filtering is done for @-attributes
- Formatting tests for every new @-attribute introduced
- @-attribute formatting test on every possible declaration and member
- Replace old-style attributes with the new-style attributes in the
standard library

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Attributes.cs

@@ -18,7 +18,7 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) =>
 // Syntax of a formal of a built-in @-attribute
 // To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg()
 public record BuiltInAtAttributeArgSyntax(
-  String ArgName,
+  string ArgName,
   Type ArgType, // If null, it means it's not resolved (@Induction and @Trigger)
   Expression DefaultValue) {
   public Formal ToFormal() {
@@ -276,7 +276,7 @@ public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndent
       }
     }
   }
-  private static string TupleItem0Name => "0";
+  public static string TupleItem0Name => "0";
   // Helper to create a built-in @-attribute
   static BuiltInAtAttributeSyntax BuiltIn(string name) {
     return new BuiltInAtAttributeSyntax(
@@ -285,7 +285,8 @@ static BuiltInAtAttributeSyntax BuiltIn(string name) {
 
   // Helper to create an old-style attribute
   private static Attributes A(string name, params Expression[] args) {
-    return new Attributes(name, args.ToList(), null);
+    return new Attributes(name, args.Select(arg =>
+      arg is DefaultValueExpression defaultExpr ? defaultExpr.Resolved : arg).ToList(), null);
   }
 
   // Helper to create an old-style attribute with only one argument
@@ -318,16 +319,44 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
       program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
     }
 
+    var resolver = new ModuleResolver(new ProgramResolver(program), program.Options) {
+      reporter = program.Reporter
+    };
+    resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
     var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray();
-    ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings);
+    ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings, resolver);
 
     atAttribute.Builtin = true;
     atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes
+    var intDecl = resolver.SystemModuleManager.valuetypeDecls.First(valueTypeDecl => valueTypeDecl.Name == PreType.TypeNameInt);
+
+    atAttribute.Arg.PreType = new DPreType(intDecl, new List<PreType>(), null);
 
     switch (name) {
+      case "AutoContracts": {
+          return A("autocontracts");
+        }
+      case "AutoRequires": {
+          return A("autoReq");
+        }
+      case "AutoRevealDependenciesAll": {
+          return A1("autoRevealDependencies", bindings);
+        }
+      case "AutoRevealDependencies": {
+          return A1("autoRevealDependencies", bindings);
+        }
+      case "Axiom": {
+          return A(AxiomAttributeName);
+        }
       case "Compile": {
           return A1("compile", bindings);
         }
+      case "Concurrent": {
+          return A(ConcurrentAttributeName);
+        }
+      case "DisableNonlinearArithmetic": {
+          return A1("disableNonlinearArithmetic", bindings);
+        }
       case "Fuel": {
           if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
             if (Get(bindings, 1, out var highFuel) && highFuel != null) {
@@ -346,9 +375,99 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
       case "IsolateAssertions": {
           return A("isolate_assertions");
         }
+      case "NativeUInt8": {
+          return A("nativeType", DefaultString("byte"));
+        }
+      case "NativeInt8": {
+          return A("nativeType", DefaultString("sbyte"));
+        }
+      case "NativeUInt16": {
+          return A("nativeType", DefaultString("ushort"));
+        }
+      case "NativeInt16": {
+          return A("nativeType", DefaultString("short"));
+        }
+      case "NativeUInt32": {
+          return A("nativeType", DefaultString("uint"));
+        }
+      case "NativeInt32": {
+          return A("nativeType", DefaultString("int"));
+        }
+      case "NativeInt53": {
+          return A("nativeType", DefaultString("number"));
+        }
+      case "NativeUInt64": {
+          return A("nativeType", DefaultString("ulong"));
+        }
+      case "NativeInt64": {
+          return A("nativeType", DefaultString("long"));
+        }
+      case "NativeUInt128": {
+          return A("nativeType", DefaultString("udoublelong"));
+        }
+      case "NativeInt128": {
+          return A("nativeType", DefaultString("doublelong"));
+        }
+      case "NativeInt": {
+          return A("nativeType", DefaultBool(true));
+        }
+      case "NativeNone": {
+          return A("nativeType", DefaultBool(false));
+        }
+      case "NativeIntOrReal": {
+          return A("nativeType");
+        }
       case "Options": {
           return A1("options", bindings);
         }
+      case "Print": {
+          return A("print");
+        }
+      case "Priority": {
+          return A1("priority", bindings);
+        }
+      case "ResourceLimit": {
+          return A1("resource_limit", bindings);
+        }
+      case "Synthesize": {
+          return A("synthesize");
+        }
+      case "TimeLimit": {
+          return A1("timeLimit", bindings);
+        }
+      case "TimeLimitMultiplier": {
+          return A1("timeLimitMultiplier", bindings);
+        }
+      case "TailRecursion": {
+          return A("tailrecursion");
+        }
+      case "Test": {
+          return A("test");
+        }
+      case "TestEntry": {
+          return A("TestEntry");
+        }
+      case "TestInline": {
+          return A1("testInline", bindings);
+        }
+      case "Transparent": {
+          return A("transparent");
+        }
+      case "VcsMaxCost": {
+          return A1("vcs_max_cost", bindings);
+        }
+      case "VcsMaxKeepGoingSplits": {
+          return A1("vcs_max_keep_going_splits", bindings);
+        }
+      case "VcsMaxSplits": {
+          return A1("vcs_max_splits", bindings);
+        }
+      case "Verify": {
+          return A1(VerifyAttributeName, bindings);
+        }
+      case "VerifyOnly": {
+          return A("only");
+        }
       default: {
           throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
         }
@@ -359,20 +478,97 @@ 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<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() {
+    BuiltIn("AutoContracts")
+      .Filter(attributeHost => attributeHost is ClassDecl),
+    BuiltIn("AutoRequires")
+      .Filter(attributeHost => attributeHost is Function),
+    BuiltIn("AutoRevealDependenciesAll").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("AutoRevealDependencies").WithArg("level", Type.Int)
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("Axiom")
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
     BuiltIn("Compile")
       .WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
       .Filter(attributeHost =>
-          attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
+        attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
+    BuiltIn("Concurrent")
+      .Filter(attributeHost =>
+        attributeHost is MethodOrFunction),
+    BuiltIn("DisableNonlinearArithmetic")
+      .WithArg("disable", Type.Bool, DefaultBool(true))
+      .Filter(attributeHost =>
+        attributeHost is ModuleDefinition),
     BuiltIn("Fuel")
       .WithArg("low", Type.Int, DefaultInt(1))
       .WithArg("high", Type.Int, DefaultInt(2))
       .WithArg("functionName", Type.ResolvedString(), DefaultString(""))
-      .Filter(attributeHost => attributeHost is Function or AssertStmt),
+      .Filter(attributeHost => attributeHost is MethodOrFunction or AssertStmt),
     BuiltIn("IsolateAssertions")
       .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("NativeUInt8")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt8")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeUInt16")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt16")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeUInt32")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt32")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt53")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeUInt64")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt64")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeUInt128")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt128")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeInt")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeNone")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
+    BuiltIn("NativeIntOrReal")
+      .Filter(attributeHost => attributeHost is NewtypeDecl),
     BuiltIn("Options")
       .WithArg(TupleItem0Name, Type.ResolvedString())
       .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),
+    BuiltIn("Print")
+      .Filter(attributeHost => attributeHost is Method),
+    BuiltIn("Priority").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("ResourceLimit").WithArg(TupleItem0Name, Type.ResolvedString())
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("Synthesize")
+      .Filter(attributeHost => attributeHost is Method),
+    BuiltIn("TimeLimit").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("TimeLimitMultiplier").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("TailRecursion")
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("Test")
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("TestEntry")
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("TestInline").WithArg("level", Type.Int, DefaultInt(1))
+      .Filter(attributeHost => attributeHost is MethodOrFunction),
+    BuiltIn("Transparent")
+      .Filter(attributeHost => attributeHost is Function),
+    BuiltIn("VcsMaxCost").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("VcsMaxKeepGoingSplits").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("VcsMaxSplits").WithArg(TupleItem0Name, Type.Int)
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("Verify")
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("VerifyOnly")
+      .Filter(attributeHost => attributeHost is ICanVerify),
   };
 
   ////// Helpers to create default values for the @-attribute definitions above //////
@@ -407,19 +603,15 @@ private static bool Get(ActualBindings bindings, int i, out Expression expr) {
 
   // Resolves bindings given a list of datatype constructor-like formals,
   // obtained from built-in @-attribute definitions
-  private static void ResolveLikeDatatypeConstructor(
-    Program program, Formal[] formals, string attrName,
-    UserSuppliedAtAttribute attrs, ActualBindings bindings) {
+  private static void ResolveLikeDatatypeConstructor(Program program, Formal[] formals, string attrName,
+    UserSuppliedAtAttribute attrs, ActualBindings bindings, ModuleResolver resolver) {
     var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
     var typeMap = new Dictionary<TypeParameter, Type>();
-    var resolver = new ModuleResolver(new ProgramResolver(program), program.Options);
-    resolver.reporter = program.Reporter;
-    resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
     resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.tok,
       attrs, resolutionContext, typeMap, null);
     resolver.FillInDefaultValueExpressions();
     resolver.SolveAllTypeConstraints();
-    // Verify that arguments are given literally
+    // Verify that provided 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");

Source/DafnyCore/AST/Cloner.cs

@@ -336,11 +336,23 @@ public Attributes CloneAttributes(Attributes attrs) {
         return CloneAttributes(attrs.Prev);
       } 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));
+          attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
+          RangeToken = Tok(usa.RangeToken)
+        };
       } else if (attrs is UserSuppliedAtAttribute usaa) {
-        return new UserSuppliedAtAttribute(Tok(usaa.tok), CloneExpr(usaa.Arg), CloneAttributes(usaa.Prev));
+        var arg = CloneExpr(usaa.Arg);
+        if (usaa.Arg.Type != null) { // The attribute has already been expanded
+          arg.Type = usaa.Arg.Type;
+          arg.PreType = usaa.Arg.PreType;
+        }
+        return new UserSuppliedAtAttribute(Tok(usaa.tok), arg, CloneAttributes(usaa.Prev)) {
+          RangeToken = Tok(usaa.RangeToken),
+          Builtin = usaa.Builtin
+        };
       } else {
-        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
+        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
+          RangeToken = Tok(attrs.RangeToken)
+        };
       }
     }
 

Source/DafnyCore/AST/Formatting.dfy

@@ -9,7 +9,8 @@ include "System.dfy"
 include "DafnyInterface.dfy"
 
 // Provided new Dafny code (trait Microsoft.Dafny.Formatting.IIndentationFormatter)
-module {:extern "Microsoft"} {:options "-functionSyntax:4"}  Microsoft {
+@Options("-functionSyntax:4")
+module {:extern "Microsoft"} Microsoft {
   module {:extern "Dafny"} Dafny {
     module {:extern "Formatting"} Formatting {
       import opened MicrosoftDafny