Parameter attributes (#5036)

Fixes #5032 ### Description Support attributes in parameters ### How has this been tested? Updated an existing littish test <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>
dafny-lang · Feb 2, 2024 · c6cd10d · c6cd10d
1 parent 705f216
commit c6cd10d
Show file tree

Hide file tree

Showing 8 changed files with 38 additions and 25 deletions.
diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs
@@ -269,7 +269,8 @@ public virtual Formal CloneFormal(Formal formal, bool isReference) {
       return (Formal)clones.GetOrCreate(formal, () => isReference
        ? formal
        : new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost,
-         CloneExpr(formal.DefaultValue), formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) {
+         CloneExpr(formal.DefaultValue), CloneAttributes(formal.Attributes),
+         formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) {
          RangeToken = formal.RangeToken,
          IsTypeExplicit = formal.IsTypeExplicit
        });

diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs
@@ -5,6 +5,8 @@
 namespace Microsoft.Dafny;
 
 public class Formal : NonglobalVariable {
+  public Attributes Attributes { get; set; }
+
   public readonly bool InParam;  // true to in-parameter, false for out-parameter
   public override bool IsMutable => !InParam;
   public readonly bool IsOld;
@@ -14,6 +16,7 @@ public class Formal : NonglobalVariable {
   public readonly string NameForCompilation;
 
   public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue,
+    Attributes attributes = null,
     bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null)
     : base(tok, name, type, isGhost) {
     Contract.Requires(tok != null);
@@ -24,16 +27,13 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex
     InParam = inParam;
     IsOld = isOld;
     DefaultValue = defaultValue;
+    Attributes = attributes;
     IsNameOnly = isNameOnly;
     IsOlder = isOlder;
     NameForCompilation = nameForCompilation ?? name;
   }
 
-  public bool HasName {
-    get {
-      return !Name.StartsWith("#");
-    }
-  }
+  public bool HasName => !Name.StartsWith("#");
 
   private string sanitizedName;
   public override string SanitizedName =>
@@ -53,7 +53,7 @@ public bool HasName {
 /// </summary>
 public class ImplicitFormal : Formal {
   public ImplicitFormal(IToken tok, string name, Type type, bool inParam, bool isGhost)
-    : base(tok, name, type, inParam, isGhost, null) {
+    : base(tok, name, type, inParam, isGhost, null, null) {
     Contract.Requires(tok != null);
     Contract.Requires(name != null);
     Contract.Requires(type != null);

diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs
@@ -192,7 +192,7 @@ void AddMember(MemberDecl member, ValuetypeVariety valuetypeVariety) {
   }
 
   public void AddRotateMember(ValuetypeDecl enclosingType, string name, Type resultType) {
-    var formals = new List<Formal> { new Formal(Token.NoToken, "w", Type.Nat(), true, false, null, false) };
+    var formals = new List<Formal> { new Formal(Token.NoToken, "w", Type.Nat(), true, false, null) };
     var rotateMember = new SpecialFunction(RangeToken.NoToken, name, SystemModule, false, false,
       new List<TypeParameter>(), formals, resultType,
       new List<AttributedExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null), new List<AttributedExpression>(),

diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
@@ -964,16 +964,19 @@ IdentTypeOptional<out BoundVar var>
      }; .)
   .
 
-TypeIdentOptional<out RangeToken/*!*/ range, out Name/*!*/ identName, out Type/*!*/ ty, out bool isGhost, out Expression defaultValue, out bool isNameOnly>
+TypeIdentOptional<out RangeToken/*!*/ range, out Name/*!*/ identName, out Type/*!*/ ty, 
+  out bool isGhost, out Expression defaultValue, out bool isNameOnly, out Attributes attributes>
 = (.Contract.Ensures(Contract.ValueAtReturn(out range)!=null);
      Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
      Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
      IToken nameToken = null; ty = new BoolType()/*dummy*/; isGhost = false;
      IToken nameonlyToken = null;
+     attributes = null;
      identName = null;
      defaultValue = null;
   .)
   (. var beforeStartToken = t; .)
+  { Attribute<ref attributes> }
   { "ghost"                            (. isGhost = true; .)
   | "nameonly"                         (. nameonlyToken = t; .)
   }
@@ -1403,19 +1406,23 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow
      Expression defaultValue;
      bool isNameOnly;
      bool isOlder;
+     Attributes attributes = null;
      RangeToken range;
      Name name;
   .)
   "("
   [
+    { Attribute<ref attributes> }
     GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
     ParameterDefaultValue<incoming, out defaultValue>
-                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)
+                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder)
                         { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null }
                     ); .)
-    { "," GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
-    ParameterDefaultValue<incoming, out defaultValue>
-                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)
+    { "," 
+      { Attribute<ref attributes> }
+      GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
+      ParameterDefaultValue<incoming, out defaultValue>
+                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder)
                         { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null }
                     ); .)
     }
@@ -1441,16 +1448,17 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
 = (. Contract.Requires(cce.NonNullElements(formals));
      RangeToken/*!*/ range;  Type/*!*/ ty;  Name/*!*/ name;  bool isGhost;  Expression/*?*/ defaultValue;
      bool isNameOnly;
+     Attributes attributes;
   .)
   "("
   [
-    TypeIdentOptional<out range, out name, out ty, out isGhost, out defaultValue, out isNameOnly>
-            (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, false, isNameOnly) 
+    TypeIdentOptional<out range, out name, out ty, out isGhost, out defaultValue, out isNameOnly, out attributes>
+            (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) 
                     { RangeToken = range, IsTypeExplicit = ty != null}
                ); 
             .)
-    { "," TypeIdentOptional<out range, out name, out ty, out isGhost, out defaultValue, out isNameOnly>
-            (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, false, isNameOnly)
+    { "," TypeIdentOptional<out range, out name, out ty, out isGhost, out defaultValue, out isNameOnly, out attributes>
+            (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly)
                     { RangeToken = range, IsTypeExplicit = ty != null}
                ); 
             .)
@@ -1740,7 +1748,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
          "("
            GIdentType<false, false, false, false, out var range2, out var resultName, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder>
            (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder);
-              result = new Formal(resultName.Tok, resultName.Value, ty, false, false, null, false)
+              result = new Formal(resultName.Tok, resultName.Value, ty, false, false, null, null, false)
                 { RangeToken = range2, IsTypeExplicit = ty != null };
            .)
          ")"
@@ -2035,16 +2043,18 @@ FunctionSpec<.List<AttributedExpression> reqs, List<FrameExpression> reads, List
 PredicateResult<string name, out Formal result>
 = (. Type/*!*/ returnType = new BoolType();
      result = null;
+     Attributes attributes = null;
   .)
   ":"
   (  IF(IsParenIdentsColon())
      "("
+       { Attribute<ref attributes> }
        GIdentType<false, false, false, false, out var range, out var nameId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder>
        (.
           if (ty is not BoolType) {
             SemErr(ErrorId.p_predicate_return_type_must_be_bool, new RangeToken(ty.StartToken, t), $"{name} return type should be bool, got {ty}");
           }
-          result = new Formal(nameId.Tok, nameId.Value, ty, false, false, null, false)
+          result = new Formal(nameId.Tok, nameId.Value, ty, false, false, null, attributes, false)
             { RangeToken = range, IsTypeExplicit = ty != null };
        .)
      ")"

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
@@ -124,7 +124,7 @@ TopLevelDecl BuiltInTypeDecl(string name) {
     public void AddRotateMember(ValuetypeDecl bitvectorTypeDecl, string name, int width) {
       var argumentType = resolver.SystemModuleManager.Nat();
       var formals = new List<Formal> {
-        new Formal(Token.NoToken, "w", argumentType, true, false, null, false) {
+        new Formal(Token.NoToken, "w", argumentType, true, false, null) {
           PreType = Type2PreType(argumentType)
         }
       };

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy
@@ -1,13 +1,13 @@
 // RUN: %exits-with 4 %verify --relax-definite-assignment "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype List<T> = Nil | Cons(T, List<T>)
+datatype List<T> = Nil | Cons({:custom 3 } T, {:custom 3 } List<T>)
 
 class Node {
   var data: int
   var next: Node?
 
-  ghost function Repr(list: List<int>): bool
+  ghost function Repr({:custom} list: List<int>): bool
     reads *
     decreases list
   { match list
@@ -24,7 +24,7 @@ class Node {
     next := null;
   }
 
-  method Add(d: int, L: List<int>) returns (r: Node)
+  method Add(d: int, L: List<int>) returns ({:custom} r: Node)
     requires Repr(L)
     ensures r.Repr(Cons(d, L))
   {

diff --git a/docs/DafnyRef/GrammarDetails.md b/docs/DafnyRef/GrammarDetails.md
@@ -584,9 +584,9 @@ MethodSignature_(isGhost, isExtreme) =
 KType = "[" ( "nat" | "ORDINAL" ) "]"
 
 Formals(allowGhostKeyword, allowNewKeyword, allowOlderKeyword, allowDefault) =
-  "(" [ GIdentType(allowGhostKeyword, allowNewKeyword, allowOlderKeyword, 
+  "(" [ { Attribute } GIdentType(allowGhostKeyword, allowNewKeyword, allowOlderKeyword,
                    allowNameOnlyKeyword: true, allowDefault)
-        { "," GIdentType(allowGhostKeyword, allowNewKeyword, allowOlderKeyword,
+        { "," { Attribute } GIdentType(allowGhostKeyword, allowNewKeyword, allowOlderKeyword,
                          allowNameOnlyKeyword: true, allowDefault) }
       ]
   ")"
@@ -1823,6 +1823,7 @@ LocalIdentTypeOptional = WildIdent [ ":" Type ]
 IdentTypeOptional = WildIdent [ ":" Type ]
 
 TypeIdentOptional =
+  { Attribute }
   { "ghost" | "nameonly" } [ NoUSIdentOrDigits ":" ] Type
   [ ":=" Expression(allowLemma: true, allowLambda: true) ]
 

diff --git a/docs/dev/news/5032.feat b/docs/dev/news/5032.feat
@@ -0,0 +1 @@
+Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files.