From c6cd10dca4ce846001ead442d33145e9cc70454a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 23:16:07 +0100 Subject: [PATCH] Parameter attributes (#5036) Fixes #5032 ### Description Support attributes in parameters ### How has this been tested? Updated an existing littish test 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). --- Source/DafnyCore/AST/Cloner.cs | 3 +- .../AST/Expressions/Variables/Formal.cs | 12 +++---- Source/DafnyCore/AST/SystemModuleManager.cs | 2 +- Source/DafnyCore/Dafny.atg | 32 ++++++++++++------- .../Resolver/PreType/PreTypeResolve.cs | 2 +- .../LitTests/LitTest/dafny0/Datatypes.dfy | 6 ++-- docs/DafnyRef/GrammarDetails.md | 5 +-- docs/dev/news/5032.feat | 1 + 8 files changed, 38 insertions(+), 25 deletions(-) create mode 100644 docs/dev/news/5032.feat diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 1fb46b2f3e..d37e4b72b9 100644 --- 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 index de64e61812..cdbff00e75 100644 --- 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 { /// 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 index 8455b0f63e..8e6895f6ea 100644 --- 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 { new Formal(Token.NoToken, "w", Type.Nat(), true, false, null, false) }; + var formals = new List { new Formal(Token.NoToken, "w", Type.Nat(), true, false, null) }; var rotateMember = new SpecialFunction(RangeToken.NoToken, name, SystemModule, false, false, new List(), formals, resultType, new List(), new Specification(new List(), null), new List(), diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index a1b0a02b3a..fc7a2f34d7 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -964,16 +964,19 @@ IdentTypeOptional }; .) . -TypeIdentOptional +TypeIdentOptional = (.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 } { "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 } GIdentType ParameterDefaultValue - (. 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 - ParameterDefaultValue - (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder) + { "," + { Attribute } + GIdentType + ParameterDefaultValue + (. 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/*!*/ formals.> = (. Contract.Requires(cce.NonNullElements(formals)); RangeToken/*!*/ range; Type/*!*/ ty; Name/*!*/ name; bool isGhost; Expression/*?*/ defaultValue; bool isNameOnly; + Attributes attributes; .) "(" [ - TypeIdentOptional - (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, false, isNameOnly) + TypeIdentOptional + (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) { RangeToken = range, IsTypeExplicit = ty != null} ); .) - { "," TypeIdentOptional - (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, false, isNameOnly) + { "," TypeIdentOptional + (. 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 "(" GIdentType (. 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 reqs, List reads, List PredicateResult = (. Type/*!*/ returnType = new BoolType(); result = null; + Attributes attributes = null; .) ":" ( IF(IsParenIdentsColon()) "(" + { Attribute } GIdentType (. 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 index 9eed372062..96f0bf031a 100644 --- 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 { - 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 index e860c10502..6d3f284925 100644 --- 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 = Nil | Cons(T, List) +datatype List = Nil | Cons({:custom 3 } T, {:custom 3 } List) class Node { var data: int var next: Node? - ghost function Repr(list: List): bool + ghost function Repr({:custom} list: List): bool reads * decreases list { match list @@ -24,7 +24,7 @@ class Node { next := null; } - method Add(d: int, L: List) returns (r: Node) + method Add(d: int, L: List) 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 index 52f5182757..79d8be47d2 100644 --- 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 new file mode 100644 index 0000000000..549183181a --- /dev/null +++ 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. \ No newline at end of file