From 86801f3d423500924baba3c0c9a5f7bb294a7034 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 26 Sep 2024 14:24:10 -0400 Subject: [PATCH 1/8] Added tests files that should pass --- .../at-attributes-acceptables-builtin.dfy | 164 ++++++++++++++++++ .../at-attributes-acceptables-userdefined.dfy | 7 + .../at-attributes/at-attributes-typos.dfy | 150 ++++++++++++++++ .../at-attributes-typos.dfy.expect | 3 + 4 files changed, 324 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.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/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy new file mode 100644 index 0000000000..5833be6f8a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy @@ -0,0 +1,164 @@ +// RUN: %baredafny resolve "%s" +// Attributes on top-level declarations + +@AutoContracts +class A { + predicate Valid() { + true + } +} + +@NativeType +newtype ubyte = x : int | 0 <= x < 256 + +@NativeType(native := true) // This is the default +newtype ubyte2 = x : int | 0 <= x < 256 + +@NativeType(native := false) +newtype ubyte3 = x : int | 0 <= x < 256 + +@NativeType(name := "byte") +newtype ubyte4 = x : int | 0 <= x < 256 + +@Extern +method ExternTest() + +@Extern(name := "MyFunction") +method ExternTest2() + +@Extern(moduleName := "MyModule", name := "MyFunction") +method ExternTest3() + +@DisableNonlinearArithmetic +@Options("--function-syntax:3") +module SimpleLinearModule { +} + +/// Attributes on functions and methods + +codatatype Stream = Stream(i: int, tail: Stream) { + @Abstemious + function Constant(): int { 1 } +} + +function f(x:int) : bool + requires x > 3 +{ + x > 7 +} + +@AutoRequires +@AutoRevealDependenciesAll(false) +@AutoRevealDependenciesAll(true) +@AutoRevealDependencies(level := 10) +@Axiom +@Compile(true) +@Fuel(low := 1) +@Fuel(low := 1, high := 2) +@Id("G#1") +function g(y:int, b:bool) : bool +{ + if b then f(y + 2) else f(2*y) +} +// TODO continue from https://dafny.org/latest/DafnyRef/DafnyRef#1122-autoreq + +@Concurrent +method ConcurrentMethod() + reads {} + modifies {} +{ + @Fuel(functionName := "g", low := 2, high := 3) + assert g(1, 0) == 2; +} + +@IsolateAssertions +method Test(a: int, b: int, c: int) + requires a < b && b < c +{ + @SplitHere + 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)) +} + +lemma Correspondence() + ensures forall n: nat @induction(n) @trigger(NatToUnary(n)) :: UnaryToNat(NatToUnary(n)) == n +{ +} + +@Only +@Print +@Priority(2) +@ResourceLimit(1000) +@SelectiveChecking +@TimeLimit(1000) +@TimeLimitMultiplier(2) +method VerifyThisOnly() { + print "hello"; + @StartCheckingHere + assert true; +} + +@TailRecursion +@Transparent +function Fib(n: nat, a: int, b: int): int { + if n == 0 then b + else Fib(n - 1, b, a + b) +} + +@Verify +@Test +@VcsMaxCost(10) +@VcsMaxKeepGoingSplits(10) +@VcsMaxSplits(10) +@IsolateAssertions +method TestItAll() { + expect true; +} + +@Synthesize +method Synthesizing(x: int) returns (y: int) + ensures x == y + 1 + +// Attributes on reads and modifies clauses + +@Concurrent +method Test(a: A) + @AssumeConcurrent reads a + @AssumeConcurrent modifies a + @Error("Error Message") + requires a != null + @Error("Error Message", "Success Message") + requires a != null +{ + @SplitHere + @SubSumption(0) + assert true; // Unchecked + @OnlyAfter + assert true; + @Focus assert true; + @OnlyBefore + assert true; // Checked + if false { + @Only + @Contradiction + assert false; + } + @Assumption + ghost var b := b && true; + +} + + + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy new file mode 100644 index 0000000000..e0e08fccaa --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy @@ -0,0 +1,7 @@ +// Attribute to use anywhere +@Attribute +datatype CustomAttribute = CustomAttribute + +@CustomAttribute +datatype CustomDeclarationAttribute = CustomDeclarationAttribute(@CustomAttribute n: string) + 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 0000000000..ebba890790 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -0,0 +1,150 @@ +// RUN: %baredafny resolve "%s" > "%t" +// RUN: %diff "%t" "%s.check" +// Attributes on top-level declarations + +@AutoContract // Should be AutoContracts +class A { + predicate Valid() { + true + } +} + +@Native // Should be NativeType +newtype ubyte = x : int | 0 <= x < 256 + +@Native(native := false) // Should be NativeType +newtype ubyte3 = x : int | 0 <= x < 256 + +@External // Should be Extern +method ExternTest() + +@DisableNonLinearArithmetic // Should be DisableNonlinearArithmetic +@Option("--function-syntax:3") // Should be Options +module SimpleLinearModule { +} + +/// Attributes on functions and methods + +codatatype Stream = Stream(i: int, tail: Stream) { + @ABstemious // Should be Abstemious + function Constant(): int { 1 } +} + +function f(x:int) : bool + requires x > 3 +{ + x > 7 +} + +@AutoReq // Should be AutoRequires +@AutorevealDependenciesAll(false) // Should be Auto_R_eveal... +@AutorevealDependenciesAll(true) +@AutorevealDependencies(level := 10) +@axiom // Should be Axiom +@Compilation(true) // Should be Compile +@Fuels(low := 1) // Should be Fuel +@Fuels(low := 1, high := 2) +@ID("G#1") // Should be Id +function g(y:int, b:bool) : bool +{ + if b then f(y + 2) else f(2*y) +} +// TODO continue from https://dafny.org/latest/DafnyRef/DafnyRef#1122-autoreq + +@concurrent // Should be Concurrent +method ConcurrentMethod() + reads {} + modifies {} +{ +} + +@Isolation // Should be IsolateAssertions +method Test(a: int, b: int, c: int) + requires a < b && b < c +{ + @Splithere // Should be SplitHere + 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)) +} + +lemma Correspondence() + ensures forall n: nat @inductive(n) @triggers(NatToUnary(n)) :: UnaryToNat(NatToUnary(n)) == n + // Should be induction and trigger +{ +} + +@only // Should be Only +@print // Should be Print +@priority(2) // Should be Priority +@RLimit(1000) // Should be ResourceLimit +@Selectivechecking // Should be SelectiveChecking +@TLimit(1000) // Should be TimeLimit +@TLimitMultiplier(2) // Should be TimeLimitMultiplier +method VerifyThisOnly() { + print "hello"; + @StartcheckingHere // Should be StartCheckingHere + assert true; +} + +@TailRecursive // Should be TailRecursion +@Transperent // Should be Transparent +function Fib(n: nat, a: int, b: int): int { + if n == 0 then b + else Fib(n - 1, b, a + b) +} + +@NoVerify // Should be Verify(false) +@Tests // Should be Test +@VcMaxCost(10) // SHould be Vcs... +@VcMaxKeepGoingSplits(10) +@VcMaxSplits(10) +@IsolateAssertion // Should be IsolateAssertion +method TestItAll() { + expect true; +} + +@Synthesizes // Should be Synthesize +method Synthesizing(x: int) returns (y: int) + ensures x == y + 1 + +// Attributes on reads and modifies clauses + +@concurrent // Should be Concurrent +method Test(a: A) + @Assumeconcurrent reads a // Should be AssumeConcurrent + @Assumeconcurrent modifies a + @error("Error Message") // Should be Error + requires a != null +{ + @Split // Should be SplitHere + @Subsumption(0) // Should be SubSumption + assert true; // Unchecked + @OnlyAfer // Should be OnlyAfter + assert true; + @Focuses assert true; // Should be Focus + @OnlyBefre // Should be OnlyBefore + assert true; // Checked + if false { + @Oly // Should be Only + @Contradicts // Should be Contradiction + assert false; + } + @assumption // Should be assumption + ghost var b := b && true; + +} + + + 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 0000000000..dc67492ba8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -0,0 +1,3 @@ + +Attribute 'AutoContract' not recognized. Did you mean 'AutoContracts' ? +... \ No newline at end of file From 8c16f8c761b80bd22ef55646eb54175df0900ad6 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 27 Sep 2024 16:45:56 -0500 Subject: [PATCH 2/8] WIP at attributes parsing not working yet --- Source/DafnyCore/AST/Attributes.cs | 44 +++ .../AST/Grammar/ParserNonGeneratedPart.cs | 9 + Source/DafnyCore/Dafny.atg | 256 +++++++++++------- .../at-attributes-acceptables-userdefined.dfy | 15 + 4 files changed, 224 insertions(+), 100 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index e3f44389b6..afef436103 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -42,6 +42,10 @@ public Attributes(string name, [Captured] List args, Attributes prev Prev = prev; } + public virtual Attributes CloneAfter(Attributes prev) { + return new Attributes(Name, Args, prev); + } + public override string ToString() { string result = Prev?.ToString() + "{:" + Name; if (Args == null || !Args.Any()) { @@ -207,6 +211,25 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object : new List { Prev }); public override IEnumerable PreResolveChildren => Children; + + // If tmpStack was parsed after attributesStack, places all attributes of + // tmpStack on top of attributesStack as if attributesStack was used all along + // Sets tmpStack to null to mark thes attributes as consumed. + public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) { + MergeIntoReadonly(tmpStack, ref attributesStack); + tmpStack = null; + } + 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 { @@ -235,6 +258,27 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L OpenBrace = openBrace; CloseBrace = closeBrace; } + + public override Attributes CloneAfter(Attributes prev) { + return new UserSuppliedAttributes(tok, OpenBrace, CloseBrace, Args, prev); + } +} + + +public class UserSuppliedAtAttribute : Attributes { + public static readonly string UserAttribute = "user_attribute"; + public readonly IToken AtSign; + public bool Recognized; // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE + public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev) + : base(UserAttribute, new List(){arg}, prev) { + Contract.Requires(tok != null); + this.tok = tok; + this.AtSign = tok; + } + + public override Attributes CloneAfter(Attributes prev) { + return new UserSuppliedAtAttribute(AtSign, Args[0], prev); + } } /// diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 783e171681..6c762e8afb 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -627,6 +627,15 @@ class DeclModifierData { public bool IsOpaque; public IToken OpaqueToken; public IToken FirstToken; + public Attributes Attributes = null; + } + + void CheckNoKeywordIfAtAttribute(DeclModifierData mods) { + if (mods is{FirstToken: not null, Attributes: UserSuppliedAtAttribute { RangeToken: {} range}}) { + SemErr(null, range.ToToken(), "Please declare @-attributes before declaration keywords"); + } else if (mods is {FirstToken: null, Attributes: UserSuppliedAtAttribute { RangeToken: {} range2}}) { + mods.FirstToken = range2.StartToken; + } } private ModuleKindEnum GetModuleKind(DeclModifierData mods) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 37ad2678c7..935d45dc01 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -246,6 +246,7 @@ DeclModifier | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) | "opaque" (. dmod.IsOpaque = true; CheckAndSetToken(ref dmod.OpaqueToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) + | AtAttribute (. CheckNoKeywordIfAtAttribute(dmod); .) ) . @@ -312,7 +313,6 @@ SubModuleDecl = "module" (. CheckAndSetTokenOnce(ref dmod.FirstToken); - Attributes attrs = null; IToken/*!*/ iderr; IToken tokenWithTrailingDocString; var prefixIds = new List(); @@ -323,7 +323,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,7 +334,7 @@ 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; .) @@ -514,7 +514,6 @@ ClassDecl parentTraits = new List(); - Attributes attrs = null; bool isRefining = false; List typeArgs = new List(); List members = new List(); @@ -524,7 +523,7 @@ ClassDecl } + { Attribute } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) [ ExtendsClause @@ -537,7 +536,7 @@ ClassDecl } "}" - (. c = new ClassDecl(new RangeToken(dmodClass.FirstToken, t), name, module, typeArgs, members, attrs, isRefining, parentTraits); + (. c = new ClassDecl(new RangeToken(dmodClass.FirstToken, t), name, module, typeArgs, members, dmodClass.Attributes, isRefining, parentTraits); c.BodyStartTok = bodyStart; c.TokenWithTrailingDocString = tokenWithTrailingDocString; .) @@ -567,7 +566,6 @@ TraitDecl parentTraits = new List(); - Attributes attrs = null; bool isRefining = false; List typeArgs = new List(); //traits should not support type parameters at the moment List members = new List(); @@ -576,7 +574,7 @@ TraitDecl } + { Attribute } ClassName (. tokenWithTrailingDocString = t; .) [ GenericParameters ] (. tokenWithTrailingDocString = t; .) [ ExtendsClause @@ -588,7 +586,7 @@ TraitDecl } "}" - (. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, attrs, isRefining, parentTraits); + (. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, dmodIn.Attributes, isRefining, parentTraits); trait.BodyStartTok = bodyStart; trait.TokenWithTrailingDocString = tokenWithTrailingDocString; .) @@ -630,7 +628,6 @@ DatatypeDecl typeArgs = new List(); List parentTraits = new List(); List ctors = new List(); @@ -644,7 +641,7 @@ DatatypeDecl } + { Attribute } DatatypeName [ GenericParameters ] [ ExtendsClause ] @@ -659,9 +656,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; @@ -673,12 +670,13 @@ DatatypeMemberName = NoUSIdentOrDigits . DatatypeMemberDecl<.List/*!*/ ctors.> = (. Contract.Requires(cce.NonNullElements(ctors)); - Attributes attrs = null; IToken/*!*/ id; List formals = new List(); var isGhost = false; + Attributes attrs = null; .) - // Note, "ghost" is parsed before any attributes. This means that the + { AtAttribute } + // Note, "ghost" is parsed before any {:} attributes. This means that the // attributes are parsed before the "id", which is consistent with other // declarations. [ "ghost" (. isGhost = true; .) ] @@ -704,7 +702,6 @@ TypeMembers<. ModuleDefinition/*!*/ module, List members .> /*------------------------------------------------------------------------*/ FieldDecl<.DeclModifierData dmod, List mm.> = (. Contract.Requires(cce.NonNullElements(mm)); - Attributes attrs = null; Type/*!*/ ty; Name name; CheckDeclModifiers(ref dmod, "field", AllowedDeclModifiers.Ghost); @@ -712,12 +709,12 @@ FieldDecl<.DeclModifierData dmod, List mm.> .) SYNC "var" (. startToken = startToken ?? t; .) - { Attribute } - FIdentType (. var f = new Field(new RangeToken(startToken, t), name, dmod.IsGhost, ty, attrs); + { Attribute } + FIdentType (. var f = new Field(new RangeToken(startToken, t), name, dmod.IsGhost, ty, dmod.Attributes); mm.Add(f); f.TokenWithTrailingDocString = t; .) { "," (. startToken = t; .) - FIdentType (. f = new Field(new RangeToken(startToken, t), name, dmod.IsGhost, ty, attrs); + FIdentType (. f = new Field(new RangeToken(startToken, t), name, dmod.IsGhost, ty, dmod.Attributes); mm.Add(f); f.TokenWithTrailingDocString = t; .) } @@ -727,7 +724,6 @@ FieldDecl<.DeclModifierData dmod, List mm.> /*------------------------------------------------------------------------*/ ConstantFieldDecl<.DeclModifierData dmod, List/*!*/ mm, bool moduleLevelDecl.> = (. Contract.Requires(cce.NonNullElements(mm)); - Attributes attrs = null; Type/*!*/ ty; Expression e = null; if (moduleLevelDecl && dmod.StaticToken != null) { @@ -738,7 +734,7 @@ ConstantFieldDecl<.DeclModifierData dmod, List/*!*/ mm, bool mo .) SYNC "const" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) - { Attribute } + { Attribute } ( IF(!IsIdentifier(la.kind) && la.kind != _digits) (. SemErr(ErrorId.p_const_decl_missing_identifier, la, "expected an identifier after 'const' and any attributes"); .) | @@ -749,7 +745,7 @@ ConstantFieldDecl<.DeclModifierData dmod, List/*!*/ mm, bool mo (. if (e == null && ty is InferredTypeProxy) { SemErr(ErrorId.p_const_is_missing_type_or_init, name.StartToken, "a const declaration must have a type or a RHS value"); } - var c = new ConstantField(new RangeToken(dmod.FirstToken, t), name, e, dmod.IsStatic, dmod.IsGhost, dmod.IsOpaque, ty, attrs); + var c = new ConstantField(new RangeToken(dmod.FirstToken, t), name, e, dmod.IsStatic, dmod.IsGhost, dmod.IsOpaque, ty, dmod.Attributes); mm.Add(c); .) OldSemi (. c.TokenWithTrailingDocString = t; .) @@ -763,7 +759,6 @@ LocalVarName = NoUSIdent . NewtypeDecl = (. Name name; IToken bvId; - Attributes attrs = null; td = null; Type baseType = null; Expression constraint; @@ -774,7 +769,7 @@ NewtypeDecl var typeParameters = new List(); .) "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) - { Attribute } + { Attribute } NewtypeName [ GenericParameters ] [ ExtendsClause ] @@ -792,13 +787,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 +801,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 +814,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 +826,7 @@ SynonymTypeDecl } + { Attribute } SynonymTypeName { TypeParameterCharacteristics } [ GenericParameters ] @@ -844,12 +838,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 +858,7 @@ SynonymTypeDecl = Name . IteratorDecl = (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null); - Attributes attrs = null; List/*!*/ typeArgs = new List(); List ins = new List(); List outs = new List(); @@ -1043,7 +1036,7 @@ IteratorDecl } + { Attribute } IteratorName ( [ GenericParameters ] @@ -1063,7 +1056,7 @@ IteratorDecl(mod, modAttrs), new Specification(decreases, decrAttrs), req, ens, yieldReq, yieldEns, - body, attrs, signatureEllipsis); + body, dmod.Attributes, signatureEllipsis); iter.BodyStartTok = bodyStart; .) . @@ -1155,7 +1148,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 +1211,7 @@ MethodDecl .) ) (. keywordToken = t; CheckDeclModifiers(ref dmod, caption, allowed); .) - { Attribute } + { Attribute } [ MethodFunctionName (. hasName = true; .) ] (. if (!hasName) { @@ -1262,25 +1254,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; @@ -1297,10 +1289,9 @@ KType req, bool allowLabel.> +RequiresClause<.List req, bool allowLabel, ref Attributes attrs.> = "requires" (. IToken lbl = null; IToken first = t; - Attributes attrs = null; Expression e; .) { Attribute } @@ -1308,26 +1299,32 @@ RequiresClause<.List req, bool allowLabel.> LabelName ":" ] Expression - OldSemi (. req.Add(new AttributedExpression(e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); .) + OldSemi (. + req.Add(new AttributedExpression(e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); + attrs = null; // Consume attributes + .) . /*------------------------------------------------------------------------*/ -EnsuresClause<.List ens, bool allowLambda.> +EnsuresClause<.List ens, bool allowLambda, ref Attributes attrs.> = "ensures" (. Expression e; - Attributes attrs = null; .) { Attribute } Expression - OldSemi (. ens.Add(new AttributedExpression(e, attrs)); .) + OldSemi (. + ens.Add(new AttributedExpression(e, attrs)); + attrs = null; // Consume attributes + .) . /*------------------------------------------------------------------------*/ -ModifiesClause<.ref List mod, ref Attributes attrs, +ModifiesClause<.ref List mod, ref Attributes attrs, ref Attributes modifiesAttrs, bool allowLambda, bool performThisDeprecatedCheck.> = "modifies" (. FrameExpression fe; + Attributes.MergeInto(ref attrs, ref modifiesAttrs); mod = mod ?? new List(); .) - { Attribute } + { Attribute } FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) { "," FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) } @@ -1335,9 +1332,9 @@ ModifiesClause<.ref List mod, ref Attributes attrs, . /*------------------------------------------------------------------------*/ -DecreasesClause<.List decreases, ref Attributes attrs, +DecreasesClause<.List decreases, ref Attributes attrs, ref Attributes decreasesAttr, bool allowWildcard, bool allowLambda.> -= "decreases" += "decreases" (. Attributes.MergeInto(ref attrs, ref decreasesAttr); .) { Attribute } DecreasesList OldSemi @@ -1345,9 +1342,11 @@ DecreasesClause<.List decreases, ref Attributes attrs, /*------------------------------------------------------------------------*/ ReadsClause<.List/*!*/ reads, ref Attributes attrs, + ref Attributes readAttrs, bool allowLemma, bool allowLambda, bool allowWild.> = "reads" - (. FrameExpression fe; .) + (. FrameExpression fe; + Attributes.MergeInto(ref attrs, ref readAttrs); .) { Attribute } PossiblyWildFrameExpression (. reads.Add(fe); .) { "," PossiblyWildFrameExpression (. reads.Add(fe); .) @@ -1360,9 +1359,8 @@ ReadsClause<.List/*!*/ reads, ref Attributes attrs, . /*------------------------------------------------------------------------*/ -InvariantClause<. List invariants.> = - "invariant" (. Attributes attrs = null; - Expression e; +InvariantClause<.List invariants, ref Attributes attrs.> = + "invariant" (. Expression e; .) { Attribute } Expression (. invariants.Add(new AttributedExpression(e, attrs)); .) @@ -1377,13 +1375,17 @@ MethodSpec<.bool isGhost, List req, List Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); + Attributes attrs = null; .) - SYNC - { ReadsClause - | ModifiesClause - | RequiresClause - | EnsuresClause - | DecreasesClause + { + { AtAttribute } + SYNC + ( ReadsClause + | ModifiesClause + | RequiresClause + | EnsuresClause + | DecreasesClause + ) } . @@ -1393,16 +1395,20 @@ IteratorSpec<.List/*!*/ reads, List/ List/*!*/ yieldReq, List/*!*/ yieldEns, ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.> = - SYNC - { ReadsClause - | ModifiesClause - | (. bool isYield = false; .) - [ "yield" (. isYield = true; .) - ] - ( RequiresClause<(isYield?yieldReq:req), !isYield> - | EnsuresClause<(isYield?yieldEns:ens), false> - ) - | DecreasesClause + (. Attributes attrs = null; .) + { + { AtAttribute } + SYNC + ( ReadsClause + | ModifiesClause + | (. bool isYield = false; .) + [ "yield" (. isYield = true; .) + ] + ( RequiresClause<(isYield?yieldReq:req), !isYield, ref attrs> + | EnsuresClause<(isYield?yieldEns:ens), false, ref attrs> + ) + | DecreasesClause + ) } . @@ -2032,21 +2038,26 @@ FunctionSpec<.List reqs, List reads, List Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); .) - SYNC - { RequiresClause - | ReadsClause - | EnsuresClause - | (. var decreasesToken = la; - var decreasesForbidden = decreases == null; - if (decreases == null) { - decreases = new List(); - } - .) - DecreasesClause - (. if (decreasesForbidden) { - var erange = new RangeToken(decreasesToken, t); - SemErr(ErrorId.p_no_decreases_for_extreme_predicates, erange, "'decreases' clauses are meaningless for least and greatest predicates, so they are not allowed"); - }.) + (. Attributes attrs = null; .) + { + { AtAttribute } + SYNC + ( RequiresClause + | ReadsClause + | EnsuresClause + | (. var decreasesToken = la; + var decreasesForbidden = decreases == null; + if (decreases == null) { + decreases = new List(); + } + .) + DecreasesClause + (. if (decreasesForbidden) { + var erange = new RangeToken(decreasesToken, t); + SemErr(ErrorId.p_no_decreases_for_extreme_predicates, erange, "'decreases' clauses are meaningless for least and greatest predicates, so they are not allowed"); + } + .) + ) } . @@ -2161,11 +2172,17 @@ OpaqueBlock List ensures = new(); List modifies = new List(); Attributes modifiesAttributes = null; + Attributes attrs = null; IToken start; .) + SYNC "opaque" (. start = t; .) - { ModifiesClause - | EnsuresClause + { + { AtAttribute } + SYNC + ( ModifiesClause + | EnsuresClause + ) } "{" { Stmt } @@ -2809,12 +2826,15 @@ ForLoopDirection /*------------------------------------------------------------------------*/ LoopSpec<.List invariants, List decreases, ref List mod, ref Attributes decAttrs, ref Attributes modAttrs.> -= { SYNC - InvariantClause - | SYNC - DecreasesClause - | SYNC - ModifiesClause += (. Attributes attrs; + .) + { + { AtAttribute } + SYNC + ( InvariantClause + | DecreasesClause + | ModifiesClause + ) } . @@ -2961,6 +2981,8 @@ AssertStmt IToken proofStart, proofEnd; IToken lbl = null; .) + { AtAttribute } + SYNC "assert" (. x = t; startToken = t; .) { Attribute } ( [ IF(IsLabel(true)) @@ -2995,6 +3017,8 @@ ExpectStmt IToken dotdotdot = null; IToken startToken = null; .) + { AtAttribute } + SYNC "expect" (. x = t; startToken = t; .) { Attribute } ( Expression @@ -3020,6 +3044,8 @@ AssumeStmt IToken dotdotdot = null; IToken startToken = null; .) + { AtAttribute } + SYNC "assume" (. x = t; startToken = t; .) { Attribute } ( Expression @@ -3084,6 +3110,7 @@ ForallStmt BlockStmt block = null; IToken bodyStart, bodyEnd; IToken tok = Token.NoToken; + Attributes ensuresAttr = null; .) "forall" (. x = t; tok = x; startToken = t; .) @@ -3099,7 +3126,8 @@ ForallStmt .) { - EnsuresClause + { AtAttribute } + EnsuresClause } [ IF(la.kind == _lbrace) /* if the input continues like a block statement, take it to be the body of the forall statement; a body-less forall statement must continue in some other way */ BlockStmt @@ -3121,6 +3149,8 @@ ModifyStmt IToken ellipsisToken = null; IToken startToken = null; .) + { AtAttribute } + SYNC "modify" (. tok = t; startToken = t; .) { Attribute } /* Note, there is an ambiguity here, because a curly brace may look like a FrameExpression and @@ -3161,6 +3191,8 @@ CalcStmt IToken opTok; IToken danglingOperator = null; .) + { AtAttribute } + SYNC "calc" (. x = t; startToken = t; .) { Attribute } [ CalcOp (. if (userSuppliedOp.ResultOp(userSuppliedOp) == null) { // guard against non-transitive calcOp (like !=) @@ -3809,9 +3841,19 @@ LambdaExpression // Coco says LambdaSpec is deletable. This is OK (it might be empty). LambdaSpec<.ref List reads, ref Attributes readsAttrs, ref Expression req.> -= { ReadsClause - | "requires" (. Expression ee; .) - Expression (. req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee) { RangeToken = new RangeToken(req.StartToken, ee.EndToken) } ; .) += { + { AtAttributes } + SYNC + ( ReadsClause + | "requires" (. + Expression ee; + if(attrs != null) { + SemErr(null, attrs.tok, "attributes not supported yet on lambda requires clauses"); + } + .) + Expression (. + req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee) { RangeToken = new RangeToken(req.StartToken, ee.EndToken) } ; .) + ) } . @@ -4581,6 +4623,20 @@ Attribute .) . +AtAttribute += (. IToken x = null; + IToken atToken = null; + Expression arg; + .) + "@" (. atToken = t; .) + Expression + (. + var rtok = new RangeToken(atToken, t); + attrs = new UserSuppliedAtAttribute(x, arg, attrs); + attrs.RangeToken = rtok; + .) + . + /*------------------------------------------------------------------------*/ Ident = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy index e0e08fccaa..49f4e0e9a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy @@ -5,3 +5,18 @@ datatype CustomAttribute = CustomAttribute @CustomAttribute datatype CustomDeclarationAttribute = CustomDeclarationAttribute(@CustomAttribute n: string) +method OtherUserDefinedAttributes() + @CustomAttribute + decreases * +{ + @CustomAttribute + calc { + 1; + 1; + } + while true + @CustomAttribute + invariant true + { + } +} \ No newline at end of file From 9b6d7841163c2d8b8af8541ff35371290bc15284 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 30 Sep 2024 05:13:17 -0500 Subject: [PATCH 3/8] Renames --- Source/DafnyCore/AST/Grammar/ParseErrors.cs | 6 +++++- Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs | 7 +++++-- ...es-builtin.dfy => at-attributes-acceptable-builtin.dfy} | 0 ...efined.dfy => at-attributes-acceptable-userdefined.dfy} | 1 + .../LitTests/LitTest/at-attributes/at-attributes-typos.dfy | 3 +++ 5 files changed, 14 insertions(+), 3 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/{at-attributes-acceptables-builtin.dfy => at-attributes-acceptable-builtin.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/{at-attributes-acceptables-userdefined.dfy => at-attributes-acceptable-userdefined.dfy} (92%) diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 8e666089d1..cd57c1261d 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_at_attributes_before_keywords, p_duplicate_modifier, p_abstract_not_allowed, p_no_ghost_for_by_method, @@ -144,7 +145,10 @@ public enum ErrorId { } static ParseErrors() { - + Add(ErrorId.p_at_attributes_before_keywords, + @" +@-Attributes, or at-attributes, must be placed before any keyword like static, const or method. +".TrimStart(), Remove(true, "Remove this at-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 6c762e8afb..3103b602c5 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -631,8 +631,11 @@ class DeclModifierData { } void CheckNoKeywordIfAtAttribute(DeclModifierData mods) { - if (mods is{FirstToken: not null, Attributes: UserSuppliedAtAttribute { RangeToken: {} range}}) { - SemErr(null, range.ToToken(), "Please declare @-attributes before declaration keywords"); + if (mods is {Attributes: UserSuppliedAtAttribute { RangeToken: {} range}} + and ({ReplaceableToken: not null} or {AbstractToken: not null} or {GhostToken: not null} + or {StaticToken: not null} or {OpaqueToken: not null}) + ) { + SemErr(ErrorId.p_at_attributes_before_keywords, range.ToToken(), "Please declare @-attributes before declaration keywords"); } else if (mods is {FirstToken: null, Attributes: UserSuppliedAtAttribute { RangeToken: {} range2}}) { mods.FirstToken = range2.StartToken; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-builtin.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy similarity index 92% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy index 49f4e0e9a1..1cf720d91a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptables-userdefined.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy @@ -1,3 +1,4 @@ +// RUN: %baredafny resolve "%s" // Attribute to use anywhere @Attribute datatype CustomAttribute = CustomAttribute diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index ebba890790..aa4285fd76 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -21,6 +21,9 @@ method ExternTest() @DisableNonLinearArithmetic // Should be DisableNonlinearArithmetic @Option("--function-syntax:3") // Should be Options module SimpleLinearModule { + class Test { + static @IsolateAssertions function Test(): int { 3 } // At-Attributes not after keywords + } } /// Attributes on functions and methods From 1f08836500b3fdf8c5cbfe00bdb1f466d85ef5d9 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 1 Oct 2024 16:37:05 -0500 Subject: [PATCH 4/8] Support for auto-completion of @ attributes on the language server --- .../Handlers/DafnyCompletionHandler.cs | 88 ++++++++++++++++++- .../Workspace/ProjectManager.cs | 5 ++ 2 files changed, 90 insertions(+), 3 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 9bf8edc631..df8576260e 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 = new List() { + "IsolateAssertions", // TODO: Put this list in Dafny Core + "TailRecursion" + }.Select(CreateCompletionItem); + return new CompletionList(completionItems); + } + private CompletionList CreateDotCompletionList() { IEnumerable members; if (symbolGuesser.TryGetTypeBefore(state, @@ -121,6 +194,15 @@ private CompletionList CreateCompletionListFromSymbols(IEnumerable Date: Tue, 1 Oct 2024 16:55:36 -0500 Subject: [PATCH 5/8] Disambiguation between @ calls and attributes --- .../AST/Grammar/ParserNonGeneratedPart.cs | 18 ++++++++++++++++++ Source/DafnyCore/Dafny.atg | 14 +++++++++----- .../at-attributes-acceptable-builtin.dfy | 6 ++++++ .../at-attributes-acceptable-userdefined.dfy | 3 +++ .../at-attributes/at-attributes-typos.dfy | 6 ++++++ 5 files changed, 42 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 3103b602c5..b388b75e65 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -458,6 +458,24 @@ bool IsGenericInstantiation(bool inExpressionContext) { return false; } } + /* The following is the largest lookahead there is. It needs to check if what follows + * can be nothing but "<" Type { "," Type } ">". + * If inExpressionContext == true, it also checks the token immediately after + * the ">" to help disambiguate some cases (see implementation comment). + */ + bool IsAtCall() { + IToken pt = la; + if (pt.val != "@") { + return false; + } + // Beginning of the file, on a different line or separated by a space: Not an At-call. Must be an attribute + if (pt.Prev == null || pt.Prev.line != pt.line || pt.Prev.col + pt.Prev.val.Length + pt.TrailingTrivia.Trim().Length < pt.col - pt.LeadingTrivia.Trim().Length) { + return false; + } + + return true; + } + /* Returns true if the next thing is of the form: * "<" Type { "," Type } ">" */ diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 935d45dc01..9ac8466805 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -973,7 +973,7 @@ TypeIdentOptional } + { Attribute | AtAttribute } { "ghost" (. isGhost = true; .) | "nameonly" (. nameonlyToken = t; .) } @@ -4285,9 +4285,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); @@ -4376,9 +4378,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) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy index 5833be6f8a..99374c559a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy @@ -3,6 +3,12 @@ @AutoContracts class A { + @Extern("b") + var x: int + + @Extern("c") + var y: int + predicate Valid() { true } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy index 1cf720d91a..a01ce7d2a4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-userdefined.dfy @@ -6,6 +6,9 @@ datatype CustomAttribute = CustomAttribute @CustomAttribute datatype CustomDeclarationAttribute = CustomDeclarationAttribute(@CustomAttribute n: string) +@CustomAttribute // Accepted +type ubytesynonym = ubyte + method OtherUserDefinedAttributes() @CustomAttribute decreases * diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index aa4285fd76..6f73ab2186 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -4,6 +4,12 @@ @AutoContract // Should be AutoContracts class A { + @extern("b") + var x: int // Should be Extern + + @extern("c") // Should be Extern + var y: int + predicate Valid() { true } From 3bc433f5f37dc356194181239a06622fe03fe10c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 3 Oct 2024 17:56:28 -0500 Subject: [PATCH 6/8] Initial support for at-attributes w/o parsing. --- Source/DafnyCore/AST/Attributes.cs | 379 +++++++++++++++++- .../Comprehensions/ComprehensionExpr.cs | 1 - .../Conditional/NestedMatchExpr.cs | 1 - .../DafnyCore/AST/Expressions/Expression.cs | 2 + .../AST/Expressions/Variables/LetExpr.cs | 2 +- Source/DafnyCore/AST/Grammar/ParseErrors.cs | 7 +- .../AST/Grammar/ParserNonGeneratedPart.cs | 18 +- Source/DafnyCore/AST/Types/Types.cs | 4 + Source/DafnyCore/Backends/BoogieExtractor.cs | 2 +- Source/DafnyCore/Dafny.atg | 339 ++++++++-------- .../NameResolutionAndTypeInference.cs | 2 +- .../Handlers/DafnyCompletionHandler.cs | 8 +- .../at-attributes-acceptable-builtin.dfy | 6 +- .../at-attributes/at-attributes-typos.dfy | 8 +- 14 files changed, 556 insertions(+), 223 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index afef436103..5a7f24abac 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -1,13 +1,15 @@ +#nullable enable using System; using System.Collections.Generic; +using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; using System.Numerics; +using JetBrains.Annotations; namespace Microsoft.Dafny; static class AttributeBearingDeclaration { - public static bool IsExtern(this IAttributeBearingDeclaration me, DafnyOptions options) => options.AllowExterns && Attributes.Contains(me.Attributes, "extern"); @@ -15,7 +17,336 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) => Attributes.Contains(me.Attributes, "axiom"); } +public record BuiltInAtAttributeArgSyntax( + String ArgName, + Type? ArgType, // If null, it means it's not resolved + bool HasDefaultValue, + Expression? DefaultValue) { + public Formal ToFormal() { + Contract.Assert(ArgType != null); + return new Formal(Token.NoToken, ArgName, ArgType, true, false, + HasDefaultValue + ? DefaultValue ?? (ArgType.IsStringType + ? new StringLiteralExpr(Token.NoToken, "", false) + : new StringLiteralExpr(Token.NoToken, "TODO", false)) + : null); + } +} + +public record BuiltInAtAttributeSyntax( + string Name, + List Args) { + public BuiltInAtAttributeSyntax WithArg(String argName, Type? argType, bool hasDefaultValue, Expression? defaultValue) { + var c = new List(Args) { + new(argName, argType, hasDefaultValue, defaultValue) }; + return this with { Args = c }; + } +} + public class Attributes : TokenNode { + static BuiltInAtAttributeSyntax B(string name) { + return new BuiltInAtAttributeSyntax( + name, new List()); + } + + private static (Attributes?, (string, IToken)?) A(string name, params Expression[] args) { + return (new Attributes(name, args.ToList(), null), null); + } + private static (Attributes?, (string, IToken)?) Error(string message, IToken tok) { + return (null, (message, tok)); + } + + public static (Attributes? attrs, (string, IToken)? error) ExpandAtAttribute(ModuleResolver resolver, ResolutionContext resolutionContext, Dictionary typeMap, Expression atAttribute) { + var toMatch = atAttribute; + if (atAttribute is IdentifierExpr) { + toMatch = new ApplySuffix(atAttribute.tok, null, atAttribute, new List(), atAttribute.EndToken); + } + + if (toMatch is not ApplySuffix { Lhs: IdentifierExpr { Name: var name }, Bindings: var bindings }) { + return Error("@-Attribute not recognized: " + atAttribute.ToString(), atAttribute.RangeToken); + } + + var resolution = ResolveLikeDatatypeConstructor(resolver, resolutionContext, typeMap, bindings, toMatch.tok); + if (!TryGetBuiltinAtAttribute(name, out var b) || b == null) { + resolver.ResolveExpression(atAttribute, resolutionContext); + return (null, null); + } + + if (name != "Induction" && name != "Trigger") { + var formals = b.Args.Select( + arg => arg.ToFormal() + ).ToArray(); + resolution(name, formals); + } else { + foreach (var argumentBinding in bindings.ArgumentBindings) { + resolver.ResolveExpression(argumentBinding.Actual, resolutionContext); + } + } + + switch (name) { + case "Abstemious": { + return A("abstemious"); + } + case "Assumption": { + return A("assumption"); + } + case "AssumeConcurrent": { + return A("assume_concurrent"); + } + 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("axiom"); + } + case "Compile": { + return A1("compile", bindings); + } + case "Concurrent": { + return A("concurrent"); + } + case "Contradiction": { + return A("contradiction"); + } + case "DisableNonlinearArithmetic": { + return A1("disable-nonlinear-arithmetic", bindings); + } + case "Error": { + if (Get(bindings, 0, out var failureMessage) && failureMessage != null) { + if (Get(bindings, 1, out var successMessage) && successMessage != null) { + return A("error", failureMessage, successMessage); + } + + return A("error", failureMessage); + } + + return Error("@error requires at least one argument", atAttribute.Tok); + } + case "Extern": { + if (Get(bindings, 0, out var externName) && externName != null) { + if (Get(bindings, 1, out var moduleName) && moduleName != null) { + return A("extern", moduleName, externName); + } + + return A("extern", externName); + } + + return A("extern"); + } + case "Focus": { + return A("focus"); + } + case "Fuel": { + if (Get(bindings, 0, out var externName) && externName != null) { + if (Get(bindings, 1, out var moduleName) && moduleName != null) { + return A("extern", moduleName, externName); + } + + return A("extern", externName); + } + + return A("extern"); + } + case "Id": { + return A1("id", bindings); + } + case "Induction": { + return A1("induction", bindings); + } + case "IsolateAssertions": { + return A("isolate_assertions"); + } + case "NativeType": { + if (Get(bindings, 0, out var native) && native != null) { + if (native is LiteralExpr { Value: false }) { + return A("nativeType", native); + } + + if (Get(bindings, 1, out var nameExpr) && nameExpr != null) { + return A("nativeType", nameExpr); + } + } + + 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 "SelectiveChecking": { + return A("selective_checking"); + } + case "SplitHere": { + return A("split_here"); + } + case "StartCheckingHere": { + return A("start_checking_here"); + } + case "Subsumption": { + return A1("subsumption", 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 "Transparent": { + return A("transparent"); + } + case "Trigger": { + return A("trigger", bindings.ArgumentBindings.Select(binding => binding.Actual).ToArray()); + } + 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("verify", bindings); + } + case "VerifyOnly": { + return A("only"); + } + case "VerifyOnlyAfter": { + return A("only", new StringLiteralExpr(atAttribute.tok, "after", false)); + } + case "VerifyOnlyBefore": { + return A("only", new StringLiteralExpr(atAttribute.tok, "before", false)); + } + default: { + return Error($"Built-in @-Attribute {name} not convertible yet", atAttribute.Tok); + } + } + } + + private static (Attributes? attrs, (string, IToken)? error) + A1(string name, ActualBindings bindings) + { + if (Get(bindings, 0, out var expr) && expr != null) { + return A(name, expr); + } + + return A(name); + } + + private static bool Get(ActualBindings bindings, int i, out Expression? expr) { + if (bindings.Arguments.Count < i + 1 || bindings.Arguments[i] is StringLiteralExpr { Value : "" }) { + expr = null; + return true; + } + + expr = bindings.Arguments[i]; + return false; + } + + private static Action ResolveLikeDatatypeConstructor( + ModuleResolver resolver, ResolutionContext resolutionContext, + Dictionary typeMap, ActualBindings bindings, IToken tok) { + return (name, formals) => { + var datatypeCtor = new DatatypeCtor(RangeToken.NoToken, new Name(RangeToken.NoToken, name), false, + formals.ToList(), null); + resolver.ResolveActualParameters(bindings, formals.ToList(), tok, + datatypeCtor, resolutionContext, typeMap, null); + }; + } + + public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeSyntax? builtinAtAttribute) { + return BuiltInAtAttributeDictionary.TryGetValue(name, out builtinAtAttribute); + } + + public static List BuiltinAtAttributes = new() { + B("Abstemious"), + B("Assumption"), + B("AssumeConcurrent"), + B("AutoContracts"), + B("AutoRequires"), + B("AutoRevealDependenciesAll").WithArg("0", Type.Bool, true, new LiteralExpr(Token.NoToken, true)), + B("AutoRevealDependencies").WithArg("level", Type.Int, false, null), + B("Axiom"), + B("Compile").WithArg("0", Type.Bool, false, new LiteralExpr(Token.NoToken, true)), + B("Concurrent"), + B("Contradiction"), + B("DisableNonlinearArithmetic"), + B("Error") + .WithArg("message", Type.ResolvedString(), false, null) + .WithArg("successMessage", Type.ResolvedString(), true, null), + B("Extern") + .WithArg("name", Type.ResolvedString(), true, null) + .WithArg("moduleName", Type.ResolvedString(), true, null), + B("Focus"), + B("Fuel") + .WithArg("low", Type.Int, true, new LiteralExpr(Token.NoToken, 1)) + .WithArg("high", Type.Int, true, new LiteralExpr(Token.NoToken, 2)) + .WithArg("functionName", Type.ResolvedString(), true, null), + B("Id").WithArg("0", Type.ResolvedString(), false, null), + B("Induction"), // Resolution is different + B("IsolateAssertions"), + B("NativeType") + .WithArg("native", Type.Bool, true, new LiteralExpr(Token.NoToken, true)) + .WithArg("name", Type.ResolvedString(), true, null), + B("Options").WithArg("0", Type.ResolvedString(), false, null), + B("Print"), + B("Priority").WithArg("0", Type.Int, false, null), + B("ResourceLimit").WithArg("0", Type.Int, false, null), + B("SelectiveChecking"), + B("SplitHere"), + B("StartCheckingHere"), + B("SubSumption").WithArg("0", Type.Int, false, null), + B("Synthesize"), + B("TimeLimit").WithArg("0", Type.Int, false, null), + B("TimeLimitMultiplier").WithArg("0", Type.Int, false, null), + B("TailRecursion"), + B("Test"), + B("Transparent"), + B("Trigger"), // Resolution is different + B("VcsMaxCost").WithArg("0", Type.Int, false, null), + B("VcsMaxKeepGoingSplits").WithArg("0", Type.Int, false, null), + B("VcsMaxSplits").WithArg("0", Type.Int, false, null), + B("Verify"), + B("VerifyOnly"), + B("VerifyOnlyAfter"), + B("VerifyOnlyBefore"), + }; + + 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); + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); @@ -33,16 +364,16 @@ void ObjectInvariant() { /*Frozen*/ public readonly List Args; - public readonly Attributes Prev; - public Attributes(string name, [Captured] List args, Attributes prev) { + public readonly Attributes? Prev; + public Attributes(string name, [Captured] List args, Attributes? prev) { Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(args)); - Name = name; + Name = name!; Args = args; Prev = prev; } - public virtual Attributes CloneAfter(Attributes prev) { + public virtual Attributes? CloneAfter(Attributes? prev) { return new Attributes(Name, Args, prev); } @@ -69,7 +400,7 @@ public static bool Contains(Attributes attrs, string nm) { /// Returns first occurrence of an attribute named nm, or null if there is no such /// attribute. /// - [Pure] + [System.Diagnostics.Contracts.Pure] public static Attributes/*?*/ Find(Attributes attrs, string nm) { Contract.Requires(nm != null); return attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm); @@ -83,7 +414,7 @@ public static bool Contains(Attributes attrs, string nm) { /// This method does NOT use type information of the attribute arguments, so it can safely /// be called very early during resolution before types are available and names have been resolved. /// - [Pure] + [System.Diagnostics.Contracts.Pure] public static bool ContainsBool(Attributes attrs, string nm, ref bool value) { Contract.Requires(nm != null); var attr = attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm); @@ -142,7 +473,7 @@ public static List FindExpressions(Attributes attrs, string nm) { /// /// Same as FindExpressions, but returns all matches /// - public static List> FindAllExpressions(Attributes attrs, string nm) { + public static List> FindAllExpressions(Attributes? attrs, string nm) { Contract.Requires(nm != null); List> ret = null; for (; attrs != null; attrs = attrs.Prev) { @@ -208,18 +539,20 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object public override IEnumerable Children => Args.Concat( Prev == null ? Enumerable.Empty() - : new List { Prev }); + : new List { Prev }); public override IEnumerable PreResolveChildren => Children; - // If tmpStack was parsed after attributesStack, places all attributes of - // tmpStack on top of attributesStack as if attributesStack was used all along - // Sets tmpStack to null to mark thes attributes as consumed. - public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) { + // Consumes all attributes of tmpStack and prepend them into attributesStack + // It assumes attributesStack was parsed after tmpStack, + // as if attributesStack was used all along + // Sets tmpStack to null to mark the attributes as consumed. + public static void MergeInto(ref Attributes? tmpStack, ref Attributes? attributesStack) { MergeIntoReadonly(tmpStack, ref attributesStack); tmpStack = null; } - private static void MergeIntoReadonly(Attributes tmpStack, ref Attributes attributesStack) { + + private static void MergeIntoReadonly(Attributes? tmpStack, ref Attributes? attributesStack) { if (tmpStack == null) { return; } @@ -236,7 +569,7 @@ public static class AttributesExtensions { /// /// By making this an extension method, it can also be invoked for a null receiver. /// - public static IEnumerable AsEnumerable(this Attributes attr) { + public static IEnumerable AsEnumerable(this Attributes? attr) { while (attr != null) { yield return attr; attr = attr.Prev; @@ -248,35 +581,37 @@ public class UserSuppliedAttributes : Attributes { public readonly IToken OpenBrace; public readonly IToken CloseBrace; public bool Recognized; // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE - public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, List args, Attributes prev) + public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, List args, Attributes? prev) : base(tok.val, args, prev) { Contract.Requires(tok != null); Contract.Requires(openBrace != null); Contract.Requires(closeBrace != null); Contract.Requires(args != null); this.tok = tok; - OpenBrace = openBrace; - CloseBrace = closeBrace; + OpenBrace = openBrace!; + CloseBrace = closeBrace!; } - public override Attributes CloneAfter(Attributes prev) { + public override Attributes? CloneAfter(Attributes? prev) { return new UserSuppliedAttributes(tok, OpenBrace, CloseBrace, Args, prev); } } public class UserSuppliedAtAttribute : Attributes { - public static readonly string UserAttribute = "user_attribute"; + public static readonly string UserAttribute = "@"; public readonly IToken AtSign; public bool Recognized; // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE - public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev) + public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes? prev) : base(UserAttribute, 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) { + public override Attributes? CloneAfter(Attributes? prev) { return new UserSuppliedAtAttribute(AtSign, Args[0], prev); } } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index 0abfc1614c..5150e328d9 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -39,7 +39,6 @@ void ObjectInvariant() { Contract.Invariant(Term != null); } - public Attributes Attributes; Attributes IAttributeBearingDeclaration.Attributes => Attributes; [FilledInDuringResolution] public List Bounds; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs index d5e5e2e4c2..cbf9c91860 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs @@ -19,7 +19,6 @@ public class NestedMatchExpr : Expression, ICloneable, ICanForm IReadOnlyList INestedMatch.Cases => Cases; public readonly bool UsesOptionalBraces; - public Attributes Attributes; [FilledInDuringResolution] public Expression Flattened { get; set; } diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 7b4f54224e..fc03649a7c 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -40,6 +40,8 @@ public Expression Resolved { public PreType PreType; + public Attributes Attributes; // @-attributes + public virtual IEnumerable TerminalExpressions { get { yield return this; diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index a71fd26141..a32f4c4834 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -9,7 +9,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari public readonly List RHSs; public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression - public Attributes Attributes { get; set; } + Attributes IAttributeBearingDeclaration.Attributes => Attributes; [FilledInDuringResolution] public List Constraint_Bounds; // null for Exact=true and for when expression is in a ghost context // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count; private Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index cd57c1261d..72fa309993 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -11,7 +11,7 @@ public class ParseErrors { public enum ErrorId { // ReSharper disable once InconsistentNaming none, - p_at_attributes_before_keywords, + p_extra_attributes, p_duplicate_modifier, p_abstract_not_allowed, p_no_ghost_for_by_method, @@ -145,10 +145,9 @@ public enum ErrorId { } static ParseErrors() { - Add(ErrorId.p_at_attributes_before_keywords, + Add(ErrorId.p_extra_attributes, @" -@-Attributes, or at-attributes, must be placed before any keyword like static, const or method. -".TrimStart(), Remove(true, "Remove this at-attribute")); +@-attributes cannot be placed here".TrimStart(), Remove(true, "Remove this at-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 b388b75e65..c42aabe27e 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -648,17 +648,6 @@ class DeclModifierData { public Attributes Attributes = null; } - void CheckNoKeywordIfAtAttribute(DeclModifierData mods) { - if (mods is {Attributes: UserSuppliedAtAttribute { RangeToken: {} range}} - and ({ReplaceableToken: not null} or {AbstractToken: not null} or {GhostToken: not null} - or {StaticToken: not null} or {OpaqueToken: not null}) - ) { - SemErr(ErrorId.p_at_attributes_before_keywords, range.ToToken(), "Please declare @-attributes before declaration keywords"); - } else if (mods is {FirstToken: null, Attributes: UserSuppliedAtAttribute { RangeToken: {} range2}}) { - mods.FirstToken = range2.StartToken; - } - } - private ModuleKindEnum GetModuleKind(DeclModifierData mods) { if (mods.IsReplaceable && mods.IsAbstract) { SemErr(null, mods.ReplaceableToken, "Can't be both replaceable and abstract"); @@ -674,6 +663,13 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) { return ModuleKindEnum.Concrete; } + 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) { diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 7c49af62df..85478b7166 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/Backends/BoogieExtractor.cs b/Source/DafnyCore/Backends/BoogieExtractor.cs index dd9a226fdc..6b76b853fa 100644 --- a/Source/DafnyCore/Backends/BoogieExtractor.cs +++ b/Source/DafnyCore/Backends/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/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 9ac8466805..e9fda415b0 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -246,7 +246,6 @@ DeclModifier | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) | "opaque" (. dmod.IsOpaque = true; CheckAndSetToken(ref dmod.OpaqueToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .) - | AtAttribute (. CheckNoKeywordIfAtAttribute(dmod); .) ) . @@ -256,6 +255,7 @@ TopDecl<. ModuleDefinition module, bool isTopLevel .> DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; .) + { AtAttribute } { DeclModifier } ( SubModuleDecl (. var litmod = submodule as LiteralModuleDecl; @@ -532,6 +532,7 @@ ClassDecl } { DeclModifier } ClassMemberDecl } @@ -582,6 +583,7 @@ TraitDecl } { DeclModifier } ClassMemberDecl } @@ -597,6 +599,7 @@ ClassMemberDecl<. DeclModifierData dmod, List mm, bool allowConstruc = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; + Attributes attrs = dmod.Attributes; .) ( (. if (moduleLevelDecl) { SemErr(ErrorId.p_top_level_field, la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); @@ -617,7 +620,7 @@ ClassMemberDecl<. DeclModifierData dmod, List mm, bool allowConstruc dmod.IsStatic = false; } .) - MethodDecl (. mm.Add(m); .) + MethodDecl (. mm.Add(m); .) ) . @@ -693,6 +696,7 @@ TypeMembers<. ModuleDefinition/*!*/ module, List members .> .) "{" { (. dmod = new DeclModifierData(); .) + { AtAttribute } { DeclModifier } ClassMemberDecl } @@ -1049,7 +1053,8 @@ IteratorDecl - [ BlockStmt + (. Attributes attrs = null; /*TODO: Recover from IteratorSpec*/ .) + [ BlockStmt ] (. iter = new IteratorDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ins, outs, new Specification(reads, readsAttrs), @@ -1143,7 +1148,7 @@ TPCharOption . /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); bool hasName = false; Name name = new Name(""); @@ -1211,7 +1216,7 @@ MethodDecl .) ) (. keywordToken = t; CheckDeclModifiers(ref dmod, caption, allowed); .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref dmod.Attributes); .) [ MethodFunctionName (. hasName = true; .) ] (. if (!hasName) { @@ -1240,13 +1245,14 @@ MethodDecl ] | ellipsis (. signatureEllipsis = t; .) ) (. tokenWithTrailingDocString = t; .) + { AtAttribute } MethodSpec + req, reads, mod, ens, dec, ref attrs, ref decAttrs, ref modAttrs, ref readsAttrs, caption, isConstructor> [ IF(isConstructor) - (. DividedBlockStmt dividedBody; .) - DividedBlockStmt + (. DividedBlockStmt dividedBody;.) + DividedBlockStmt (. body = dividedBody; .) - | BlockStmt + | BlockStmt ] (. var range = new RangeToken(dmod.FirstToken, t); if (isConstructor) { @@ -1289,9 +1295,10 @@ KType req, bool allowLabel, ref Attributes attrs.> +RequiresClause<.List req, bool allowLabel.> = "requires" (. IToken lbl = null; IToken first = t; + Attributes attrs = null; Expression e; .) { Attribute } @@ -1299,32 +1306,26 @@ RequiresClause<.List req, bool allowLabel, ref Attributes LabelName ":" ] Expression - OldSemi (. - req.Add(new AttributedExpression(e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); - attrs = null; // Consume attributes - .) + OldSemi (. req.Add(new AttributedExpression(e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); .) . /*------------------------------------------------------------------------*/ -EnsuresClause<.List ens, bool allowLambda, ref Attributes attrs.> +EnsuresClause<.List ens, bool allowLambda.> = "ensures" (. Expression e; + Attributes attrs = null; .) { Attribute } Expression - OldSemi (. - ens.Add(new AttributedExpression(e, attrs)); - attrs = null; // Consume attributes - .) + OldSemi (. ens.Add(new AttributedExpression(e, attrs)); .) . /*------------------------------------------------------------------------*/ -ModifiesClause<.ref List mod, ref Attributes attrs, ref Attributes modifiesAttrs, +ModifiesClause<.ref List mod, ref Attributes attrs, bool allowLambda, bool performThisDeprecatedCheck.> = "modifies" (. FrameExpression fe; - Attributes.MergeInto(ref attrs, ref modifiesAttrs); mod = mod ?? new List(); .) - { Attribute } + { Attribute } FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) { "," FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) } @@ -1332,9 +1333,9 @@ ModifiesClause<.ref List mod, ref Attributes attrs, ref Attribu . /*------------------------------------------------------------------------*/ -DecreasesClause<.List decreases, ref Attributes attrs, ref Attributes decreasesAttr, +DecreasesClause<.List decreases, ref Attributes attrs, bool allowWildcard, bool allowLambda.> -= "decreases" (. Attributes.MergeInto(ref attrs, ref decreasesAttr); .) += "decreases" { Attribute } DecreasesList OldSemi @@ -1342,11 +1343,9 @@ DecreasesClause<.List decreases, ref Attributes attrs, ref Attribute /*------------------------------------------------------------------------*/ ReadsClause<.List/*!*/ reads, ref Attributes attrs, - ref Attributes readAttrs, bool allowLemma, bool allowLambda, bool allowWild.> = "reads" - (. FrameExpression fe; - Attributes.MergeInto(ref attrs, ref readAttrs); .) + (. FrameExpression fe; .) { Attribute } PossiblyWildFrameExpression (. reads.Add(fe); .) { "," PossiblyWildFrameExpression (. reads.Add(fe); .) @@ -1359,8 +1358,9 @@ ReadsClause<.List/*!*/ reads, ref Attributes attrs, . /*------------------------------------------------------------------------*/ -InvariantClause<.List invariants, ref Attributes attrs.> = - "invariant" (. Expression e; +InvariantClause<. List invariants.> = + "invariant" (. Attributes attrs = null; + Expression e; .) { Attribute } Expression (. invariants.Add(new AttributedExpression(e, attrs)); .) @@ -1369,23 +1369,22 @@ InvariantClause<.List invariants, ref Attributes attrs.> = /*------------------------------------------------------------------------*/ MethodSpec<.bool isGhost, List req, List reads, List mod, List ens, - List decreases, ref Attributes decAttrs, ref Attributes modAttrs, ref Attributes readsAttrs, string caption, bool performThisDeprecatedCheck.> + List decreases, ref Attributes attrs, ref Attributes decAttrs, ref Attributes modAttrs, ref Attributes readsAttrs, string caption, bool performThisDeprecatedCheck.> = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); - Attributes attrs = null; .) + SYNC { - { AtAttribute } - SYNC - ( ReadsClause - | ModifiesClause - | RequiresClause - | EnsuresClause - | DecreasesClause - ) + ( ReadsClause + | ModifiesClause + | RequiresClause + | EnsuresClause + | DecreasesClause + ) + { AtAttribute } // For the next clause } . @@ -1395,20 +1394,16 @@ IteratorSpec<.List/*!*/ reads, List/ List/*!*/ yieldReq, List/*!*/ yieldEns, ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.> = - (. Attributes attrs = null; .) - { - { AtAttribute } - SYNC - ( ReadsClause - | ModifiesClause - | (. bool isYield = false; .) - [ "yield" (. isYield = true; .) - ] - ( RequiresClause<(isYield?yieldReq:req), !isYield, ref attrs> - | EnsuresClause<(isYield?yieldEns:ens), false, ref attrs> - ) - | DecreasesClause - ) + SYNC + { ReadsClause + | ModifiesClause + | (. bool isYield = false; .) + [ "yield" (. isYield = true; .) + ] + ( RequiresClause<(isYield?yieldReq:req), !isYield> + | EnsuresClause<(isYield?yieldEns:ens), false> + ) + | DecreasesClause } . @@ -2038,26 +2033,21 @@ FunctionSpec<.List reqs, List reads, List Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); .) - (. Attributes attrs = null; .) - { - { AtAttribute } - SYNC - ( RequiresClause - | ReadsClause - | EnsuresClause - | (. var decreasesToken = la; - var decreasesForbidden = decreases == null; - if (decreases == null) { - decreases = new List(); - } - .) - DecreasesClause - (. if (decreasesForbidden) { - var erange = new RangeToken(decreasesToken, t); - SemErr(ErrorId.p_no_decreases_for_extreme_predicates, erange, "'decreases' clauses are meaningless for least and greatest predicates, so they are not allowed"); - } - .) - ) + SYNC + { RequiresClause + | ReadsClause + | EnsuresClause + | (. var decreasesToken = la; + var decreasesForbidden = decreases == null; + if (decreases == null) { + decreases = new List(); + } + .) + DecreasesClause + (. if (decreasesForbidden) { + var erange = new RangeToken(decreasesToken, t); + SemErr(ErrorId.p_no_decreases_for_extreme_predicates, erange, "'decreases' clauses are meaningless for least and greatest predicates, so they are not allowed"); + }.) } . @@ -2149,21 +2139,26 @@ FunctionBody + (. Attributes attrs = null; /* TODO: Have FunctionBody return attributes */ .) + { AtAttribute } + BlockStmt ] . /*------------------------------------------------------------------------*/ -BlockStmt +BlockStmt = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); List body = new List(); .) - "{" (. bodyStart = t; .) + "{" (. bodyStart = t; Attributes blockAttrs = attrs; attrs = null; .) { Stmt } "}" (. bodyEnd = t; - block = new BlockStmt(new RangeToken(bodyStart, bodyEnd), body); + block = new BlockStmt(new RangeToken(bodyStart, bodyEnd), body) { + Attributes = blockAttrs + }; .) + { AtAttribute } . OpaqueBlock @@ -2172,17 +2167,11 @@ OpaqueBlock List ensures = new(); List modifies = new List(); Attributes modifiesAttributes = null; - Attributes attrs = null; IToken start; .) - SYNC "opaque" (. start = t; .) - { - { AtAttribute } - SYNC - ( ModifiesClause - | EnsuresClause - ) + { ModifiesClause + | EnsuresClause } "{" { Stmt } @@ -2194,20 +2183,23 @@ OpaqueBlock . /*------------------------------------------------------------------------*/ -DividedBlockStmt +DividedBlockStmt = (. Contract.Ensures(Contract.ValueAtReturn(out body) != null); List bodyInit = new List(); IToken separatorTok = null; List bodyProper = new List(); .) - "{" (. bodyStart = t; .) + "{" (. bodyStart = t; Attributes blockAttrs = attrs; attrs = null; .) { Stmt } [ "new" (. separatorTok = t; .) ";" { Stmt } ] "}" (. bodyEnd = t; .) - (. body = new DividedBlockStmt(new RangeToken(bodyStart, t), bodyInit, separatorTok, bodyProper); .) + (. body = new DividedBlockStmt(new RangeToken(bodyStart, t), bodyInit, separatorTok, bodyProper) { + Attributes = blockAttrs + }; .) + { AtAttribute } . /*------------------------------------------------------------------------*/ @@ -2223,9 +2215,10 @@ OneStmt s = dummyStmt; /* to please the compiler */ BlockStmt bs; IToken bodyStart, bodyEnd; + Attributes attrs = null; // TODO: Have OneStmt accept ref Attributes attrs .) SYNC - ( BlockStmt (. s = bs; .) + ( BlockStmt (. s = bs; .) | OpaqueBlock | IF(IsReveal(scanner.Peek())) RevealStmt | AssignStatement // includes UpdateFailure @@ -2345,7 +2338,7 @@ AssignStatement IToken x = Token.NoToken; IToken endTok = Token.NoToken; IToken startToken = Token.NoToken; - Attributes attrs = null; + Attributes attrs = null; // TODO: Capture attributes if Lhs parses Attributes tokenAttrs = null; AttributedToken suchThatAssume = null; Expression suchThat = null; @@ -2375,20 +2368,25 @@ AssignStatement { Attribute } (. keywordToken = new AttributedToken(tok, tokenAttrs); .) ] Expression - { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .) + { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); attrs = null; .) { "," Rhs (. rhss.Add(r); .) } ) + (. CheckNoAttributes(ref attrs); .) ( - "by" BlockStmt - | ";" + "by" { AtAttribute } + BlockStmt + | ";" { AtAttribute } ) | ":" (. SemErr(ErrorId.p_invalid_colon, new RangeToken(startToken, t), "invalid statement beginning here (is a 'label' keyword missing? or a 'const' or 'var' keyword?)"); .) - | { Attribute } (. endToken = t; .) + | { Attribute } (. endToken = t; var rhsAttrs = attrs; attrs = null; .) + (. CheckNoAttributes(ref attrs); .) ( - "by" BlockStmt + "by" { AtAttribute } + BlockStmt | ";" - ) (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .) + ) (. endTok = t; rhss.Add(new ExprRhs(e, rhsAttrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .) + { AtAttribute } | { Attribute } (. endToken = t; .) (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); SemErr(ErrorId.p_missing_semicolon, new RangeToken(startToken, t), "missing semicolon at end of statement"); @@ -2400,12 +2398,15 @@ AssignStatement { Attribute } (. keywordToken = new AttributedToken(tok, tokenAttrs); .) ] Expression - { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .) + { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); attrs = null; .) { "," Rhs (. rhss.Add(r); .) } + (. CheckNoAttributes(ref attrs); .) ( - "by" BlockStmt + "by" { AtAttribute} + BlockStmt | ";" (. endTok = t; .) + { AtAttribute} ) ) (. var rangeToken = new RangeToken(startToken, t); @@ -2550,14 +2551,18 @@ VarDeclStatement<.out Statement/*!*/ s.> { Attribute } (. keywordToken = new AttributedToken(tok, tokenAttrs); .) ] Expression - { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .) + { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); attrs = null; .) { "," Rhs (. rhss.Add(r); .) } ] - SYNC ( "by" - BlockStmt - | ";" (. endTok = t; .) + SYNC + ( (. CheckNoAttributes(ref attrs); .) + "by" { AtAttribute } + BlockStmt + | (. CheckNoAttributes(ref attrs); .) + ";" (. endTok = t; .) ) + { AtAttribute } (. ConcreteAssignStatement assignment; var lhsExprs = new List(); if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init @@ -2607,7 +2612,8 @@ IfStmt BlockStmt/*!*/ bs; Statement/*!*/ s; Statement els = null; - Attributes attrs = null; + Attributes ifAttrs = null; + Attributes attrs = null; // TODO: Recover at-attributes from the context Attributes elsattrs = null; IToken bodyStart, bodyEnd; IToken endTok; @@ -2617,11 +2623,11 @@ IfStmt bool usesOptionalBraces; .) "if" (. x = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref ifAttrs); .) ( IF(IsAlternative()) AlternativeBlock - (. ifStmt = new AlternativeStmt(new RangeToken(startToken, t), alternatives, usesOptionalBraces, attrs); + (. ifStmt = new AlternativeStmt(new RangeToken(startToken, t), alternatives, usesOptionalBraces, ifAttrs); .) | ( IF(IsBindingGuard()) @@ -2631,10 +2637,10 @@ IfStmt errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated"); .) ) - BlockStmt + BlockStmt [ "else" ( IfStmt (. els = s; .) - | { Attribute } BlockStmt (. els = bs; .) + | { Attribute } BlockStmt (. els = bs; .) ) ] (. @@ -2646,7 +2652,7 @@ IfStmt ifStmt = new IfStmt(rangeToken, isBindingGuard, guard, thn, els); ifStmt = new SkeletonStatement(ifStmt, guardEllipsis, null); } else { - ifStmt = new IfStmt(rangeToken, isBindingGuard, guard, thn, els, attrs); + ifStmt = new IfStmt(rangeToken, isBindingGuard, guard, thn, els, ifAttrs); } .) ) @@ -2706,7 +2712,8 @@ AlternativeBlockCase<.bool allowBindingGuards, out GuardedAlternative alt.> WhileStmt = (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken x; Expression guard = null; IToken guardEllipsis = null; - Attributes attrs = null; + Attributes attrs = null; // TODO: Recover attributes from the context + Attributes whileAttrs = null; List invariants = new List(); List decreases = new List(); IToken startToken = null; @@ -2722,12 +2729,12 @@ WhileStmt bool usesOptionalBraces; .) "while" (. x = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref whileAttrs); .) ( IF(IsLoopSpec() || IsAlternative()) LoopSpec AlternativeBlock - (. stmt = new AlternativeLoopStmt(new RangeToken(startToken, t), invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives, usesOptionalBraces, attrs); + (. stmt = new AlternativeLoopStmt(new RangeToken(startToken, t), invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives, usesOptionalBraces, whileAttrs); .) | ( Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) @@ -2737,7 +2744,7 @@ WhileStmt ) LoopSpec ( IF(la.kind == _lbrace) /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */ - BlockStmt (. isDirtyLoop = false; .) + BlockStmt (. isDirtyLoop = false; .) | IF(la.kind == _ellipsis) /* if there's an ellipsis, claim it as standing for the loop body (as opposed to a "...;" statement following the loop) */ ellipsis (. bodyEllipsis = t; isDirtyLoop = false; errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated"); @@ -2753,14 +2760,14 @@ WhileStmt if (body == null && !isDirtyLoop) { body = new BlockStmt(rangeToken, new List()); } - stmt = new WhileStmt(rangeToken, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body, attrs); + stmt = new WhileStmt(rangeToken, guard, invariants, new Specification(decreases, decAttrs), new Specification(null, null), body, whileAttrs); stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis); } else { // The following statement protects against crashes in case of parsing errors if (body == null && !isDirtyLoop) { body = new BlockStmt(rangeToken, new List()); } - stmt = new WhileStmt(rangeToken, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body, attrs); + stmt = new WhileStmt(rangeToken, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body, whileAttrs); } .) ) @@ -2773,7 +2780,7 @@ ForLoopStmt Expression start; Expression end = null; bool goingUp = true; - + Attributes forAttrs = null; Attributes attrs = null; List invariants = new List(); @@ -2789,7 +2796,7 @@ ForLoopStmt bool isDirtyLoop = true; .) "for" (. x = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref forAttrs); .) IdentTypeOptional ":=" Expression @@ -2799,7 +2806,7 @@ ForLoopStmt ) LoopSpec ( IF(la.kind == _lbrace) /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */ - BlockStmt (. isDirtyLoop = false; .) + BlockStmt (. isDirtyLoop = false; .) | /* go body-less */ ) (. @@ -2809,7 +2816,7 @@ ForLoopStmt body = new BlockStmt(rangeToken, new List()); } stmt = new ForLoopStmt(rangeToken, loopIndex, start, end, goingUp, - invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body, attrs); + invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body, forAttrs); .) . @@ -2826,15 +2833,12 @@ ForLoopDirection /*------------------------------------------------------------------------*/ LoopSpec<.List invariants, List decreases, ref List mod, ref Attributes decAttrs, ref Attributes modAttrs.> -= (. Attributes attrs; - .) - { - { AtAttribute } - SYNC - ( InvariantClause - | DecreasesClause - | ModifiesClause - ) += { SYNC + InvariantClause + | SYNC + DecreasesClause + | SYNC + ModifiesClause } . @@ -2974,38 +2978,41 @@ CaseStmt /*------------------------------------------------------------------------*/ AssertStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; - Expression e = dummyExpr; Attributes attrs = null; + Expression e = dummyExpr; + Attributes attrs = null; // TODO: Recover from context + Attributes assertAttrs = null; IToken dotdotdot = null; BlockStmt proof = null; IToken startToken = null; IToken proofStart, proofEnd; IToken lbl = null; .) - { AtAttribute } SYNC "assert" (. x = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref assertAttrs); .) ( [ IF(IsLabel(true)) LabelName ":" ] Expression - ( "by" - BlockStmt + (. CheckNoAttributes(ref attrs); .) + ( "by" { AtAttribute } + BlockStmt | ";" | (. SemErr(ErrorId.p_assert_needs_by_or_semicolon, t, "expected either 'by' or a semicolon following the assert expression"); .) ) + { AtAttribute } | ellipsis (. dotdotdot = t; errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated"); .) ";" ) (. if (dotdotdot != null) { - s = new AssertStmt(new RangeToken(startToken, t), new LiteralExpr(x, true), null, null, attrs); + s = new AssertStmt(new RangeToken(startToken, t), new LiteralExpr(x, true), null, null, assertAttrs); s = new SkeletonStatement(s, dotdotdot, null); } else { - s = new AssertStmt(new RangeToken(startToken, t), e, proof, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs); + s = new AssertStmt(new RangeToken(startToken, t), e, proof, lbl == null ? null : new AssertLabel(lbl, lbl.val), assertAttrs); } .) . @@ -3013,11 +3020,10 @@ AssertStmt /*------------------------------------------------------------------------*/ ExpectStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; - Expression e = dummyExpr; Expression m = null; Attributes attrs = null; + Expression e = dummyExpr; Expression m = null; Attributes attrs = null; // TODO: Accept ref attrs in ExpectStmt IToken dotdotdot = null; IToken startToken = null; .) - { AtAttribute } SYNC "expect" (. x = t; startToken = t; .) { Attribute } @@ -3044,8 +3050,6 @@ AssumeStmt IToken dotdotdot = null; IToken startToken = null; .) - { AtAttribute } - SYNC "assume" (. x = t; startToken = t; .) { Attribute } ( Expression @@ -3103,6 +3107,7 @@ ForallStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x = Token.NoToken; List bvars = null; + Attributes attrs = null; // TODO: Have ForallStmt accept and return this Attributes qattrs = null; Expression range = null; var ens = new List(); @@ -3110,7 +3115,6 @@ ForallStmt BlockStmt block = null; IToken bodyStart, bodyEnd; IToken tok = Token.NoToken; - Attributes ensuresAttr = null; .) "forall" (. x = t; tok = x; startToken = t; .) @@ -3126,11 +3130,10 @@ ForallStmt .) { - { AtAttribute } - EnsuresClause + EnsuresClause } [ IF(la.kind == _lbrace) /* if the input continues like a block statement, take it to be the body of the forall statement; a body-less forall statement must continue in some other way */ - BlockStmt + BlockStmt ] (. if (theOptions.DisallowSoundnessCheating && block == null && 0 < ens.Count) { SemErr(ErrorId.p_forall_with_ensures_must_have_body, t, "a forall statement with an ensures clause must have a body"); @@ -3143,16 +3146,15 @@ ForallStmt /*------------------------------------------------------------------------*/ ModifyStmt = (. IToken tok; IToken endTok = Token.NoToken; - Attributes attrs = null; + Attributes attrs = null; // TODO: Should be a ref argument + Attributes modifyAttrs = null; FrameExpression fe; var mod = new List(); BlockStmt body = null; IToken bodyStart; IToken ellipsisToken = null; IToken startToken = null; .) - { AtAttribute } - SYNC "modify" (. tok = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref modifyAttrs); .) /* Note, there is an ambiguity here, because a curly brace may look like a FrameExpression and * may also look like a BlockStmt. We're happy to parse the former, because if the user intended * the latter, then an explicit FrameExpression of {} could be given. @@ -3164,12 +3166,13 @@ ModifyStmt errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated"); .) ) - ( BlockStmt + ( BlockStmt (. errors.Deprecated(ErrorId.p_deprecated_modify_statement_with_block, bodyStart, "the modify statement with a block statement is deprecated"); .) - | SYNC ";" (. endTok = t; .) + | SYNC ";" (. endTok = t; CheckNoAttributes(ref attrs); .) ) - (. s = new ModifyStmt(new RangeToken(startToken, t), mod, attrs, body); + { AtAttribute } + (. s = new ModifyStmt(new RangeToken(startToken, t), mod, modifyAttrs, body); if (ellipsisToken != null) { s = new SkeletonStatement(s, ellipsisToken, null); } @@ -3180,7 +3183,8 @@ ModifyStmt CalcStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken x; - Attributes attrs = null; + Attributes calcAttrs = null; + Attributes attrs = null; // TODO: Have it a ref arg of CalcStmt CalcStmt.CalcOp op, userSuppliedOp = null, resOp = Microsoft.Dafny.CalcStmt.DefaultOp; var lines = new List(); var hints = new List(); @@ -3191,10 +3195,8 @@ CalcStmt IToken opTok; IToken danglingOperator = null; .) - { AtAttribute } - SYNC "calc" (. x = t; startToken = t; .) - { Attribute } + { Attribute } (. Attributes.MergeInto(ref attrs, ref calcAttrs); .) [ CalcOp (. if (userSuppliedOp.ResultOp(userSuppliedOp) == null) { // guard against non-transitive calcOp (like !=) SemErr(ErrorId.p_calc_operator_must_be_transitive, opTok, "the main operator of a calculation must be transitive"); } else { @@ -3225,7 +3227,8 @@ CalcStmt { IF(la.kind == _lbrace || la.kind == _calc) /* Grab as a hint if possible, not a next line in the calculation whose expression begins with an open brace * or StmtExpr containing a calc. A user has to rewrite such a line to be enclosed in parentheses. */ - ( BlockStmt (. hintEnd = subBlock.EndToken; subhints.Add(subBlock); .) + ( BlockStmt + (. hintEnd = subBlock.EndToken; subhints.Add(subBlock); .) | CalcStmt (. hintEnd = subCalc.EndToken; subhints.Add(subCalc); .) ) } @@ -3243,7 +3246,7 @@ CalcStmt // Repeat the last line to create a dummy line for the dangling hint lines.Add(lines[lines.Count - 1]); } - s = new CalcStmt(new RangeToken(startToken, t), userSuppliedOp, lines, hints, stepOps, attrs); + s = new CalcStmt(new RangeToken(startToken, t), userSuppliedOp, lines, hints, stepOps, calcAttrs); .) . @@ -3841,19 +3844,9 @@ LambdaExpression // Coco says LambdaSpec is deletable. This is OK (it might be empty). LambdaSpec<.ref List reads, ref Attributes readsAttrs, ref Expression req.> -= { - { AtAttributes } - SYNC - ( ReadsClause - | "requires" (. - Expression ee; - if(attrs != null) { - SemErr(null, attrs.tok, "attributes not supported yet on lambda requires clauses"); - } - .) - Expression (. - req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee) { RangeToken = new RangeToken(req.StartToken, ee.EndToken) } ; .) - ) += { ReadsClause + | "requires" (. Expression ee; .) + Expression (. req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee) { RangeToken = new RangeToken(req.StartToken, ee.EndToken) } ; .) } . @@ -4552,10 +4545,12 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow // optional "| " suffix Expression ] - { IF( la.kind == _lbracecolon) Attribute } // Ambiguity -- if the next optional block is not present, - // this {Attribute} ends a QuantifierVariableDecl so it can end a SetComprehensionExpr - // so it can end an Expression - // But an Expression can be followed by {Attribute} as in VarDeclStatement, Rhs, AssignStatement + { IF( la.kind == _lbracecolon) Attribute + | IF(la.kind == _at) AtAttribute + } // Ambiguity -- if the next optional block is not present, + // this {Attribute} ends a QuantifierVariableDecl so it can end a SetComprehensionExpr + // so it can end an Expression + // But an Expression can be followed by {Attribute} as in VarDeclStatement, Rhs, AssignStatement [ // Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement. // That can happen because the grammar allows a QuantifierDecl to end a QuantifierDomain, which can end // a SetComprehensionExpr, and a Expression can be followed by a bitvector '|'. diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index f78d2a8e74..ede0b164dd 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3200,7 +3200,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/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index df8576260e..80f646a3eb 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -157,10 +157,10 @@ private bool IsAtAttribute() { } private CompletionList CreateAtAttributeCompletionList() { - var completionItems = new List() { - "IsolateAssertions", // TODO: Put this list in Dafny Core - "TailRecursion" - }.Select(CreateCompletionItem); + var completionItems = + Attributes.BuiltinAtAttributes.Select(b => + CreateCompletionItem(b.Name) + ).ToList(); return new CompletionList(completionItems); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy index 99374c559a..153bff4d16 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy @@ -99,7 +99,9 @@ function NatToUnary(n: nat): Unary { } lemma Correspondence() - ensures forall n: nat @induction(n) @trigger(NatToUnary(n)) :: UnaryToNat(NatToUnary(n)) == n + ensures + @Induction(n) @Trigger(NatToUnary(n)) + forall n: nat :: UnaryToNat(NatToUnary(n)) == n { } @@ -149,7 +151,7 @@ method Test(a: A) requires a != null { @SplitHere - @SubSumption(0) + @Subsumption(0) assert true; // Unchecked @OnlyAfter assert true; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index 6f73ab2186..9bd2d5c015 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -89,8 +89,10 @@ function NatToUnary(n: nat): Unary { } lemma Correspondence() - ensures forall n: nat @inductive(n) @triggers(NatToUnary(n)) :: UnaryToNat(NatToUnary(n)) == n - // Should be induction and trigger + ensures + @inductive(n) @triggers(NatToUnary(n)) + forall n: nat :: UnaryToNat(NatToUnary(n)) == n + // Should be Induction and Trigger { } @@ -138,7 +140,7 @@ method Test(a: A) requires a != null { @Split // Should be SplitHere - @Subsumption(0) // Should be SubSumption + @SubSumption(0) // Should be SubSumption assert true; // Unchecked @OnlyAfer // Should be OnlyAfter assert true; From 5377e13bbbed2c1aa47179bfb3bbeba64387f13e Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 3 Oct 2024 22:57:00 -0500 Subject: [PATCH 7/8] Attributes on some statements --- Source/DafnyCore/AST/Attributes.cs | 1 + .../AST/Grammar/ParserNonGeneratedPart.cs | 3 + Source/DafnyCore/Dafny.atg | 61 ++++++++++++------- 3 files changed, 42 insertions(+), 23 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 5a7f24abac..b2d9372eff 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -543,6 +543,7 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object public override IEnumerable PreResolveChildren => Children; + // # After ensuring we started to parse something, we assign its attributes // Consumes all attributes of tmpStack and prepend them into attributesStack // It assumes attributesStack was parsed after tmpStack, // as if attributesStack was used all along diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index c42aabe27e..d160d79945 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -663,6 +663,9 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) { return ModuleKindEnum.Concrete; } + /// + /// Before literals that end a block, we usually add CheckNoAttributes to avoid any non-attached attributes + /// public void CheckNoAttributes(ref Attributes attrs) { if (attrs != null) { SemErr(ErrorId.p_extra_attributes, attrs.RangeToken, "Attribute not expected here"); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index e9fda415b0..4e14d1cd81 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2150,10 +2150,13 @@ FunctionBody = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); List body = new List(); + Attributes blockAttrs = null; .) - "{" (. bodyStart = t; Attributes blockAttrs = attrs; attrs = null; .) - { Stmt } + "{" (. bodyStart = t; Attributes.MergeInto(ref attrs, ref blockAttrs); .) + { AtAttribute } + { Stmt } "}" (. bodyEnd = t; + CheckNoAttributes(ref attrs); block = new BlockStmt(new RangeToken(bodyStart, bodyEnd), body) { Attributes = blockAttrs }; @@ -2168,18 +2171,22 @@ OpaqueBlock List modifies = new List(); Attributes modifiesAttributes = null; IToken start; + Attributes attrs = null; // TODO: Get from context .) "opaque" (. start = t; .) { ModifiesClause | EnsuresClause } - "{" - { Stmt } + "{" (. CheckNoAttributes(ref attrs); .) + { AtAttribute } + { Stmt } "}" (. + CheckNoAttributes(ref attrs); s = new OpaqueBlock(new RangeToken(start, t), body, ensures, new Specification(modifies, modifiesAttributes)); .) + { AtAttribute } . /*------------------------------------------------------------------------*/ @@ -2188,14 +2195,17 @@ DividedBlockStmt bodyInit = new List(); IToken separatorTok = null; List bodyProper = new List(); + Attributes blockAttrs = null; .) - "{" (. bodyStart = t; Attributes blockAttrs = attrs; attrs = null; .) - { Stmt } - [ "new" (. separatorTok = t; .) + "{" (. bodyStart = t; Attributes.MergeInto(ref attrs, ref blockAttrs); .) + { AtAttribute } + { Stmt } + [ "new" (. separatorTok = t; CheckNoAttributes(ref attrs); .) ";" - { Stmt } + { AtAttribute } + { Stmt } ] - "}" (. bodyEnd = t; .) + "}" (. bodyEnd = t; CheckNoAttributes(ref attrs); .) (. body = new DividedBlockStmt(new RangeToken(bodyStart, t), bodyInit, separatorTok, bodyProper) { Attributes = blockAttrs }; .) @@ -2203,19 +2213,18 @@ DividedBlockStmt/*!*/ ss.> +Stmt<.List/*!*/ ss, ref Attributes attrs.> = (. Statement/*!*/ s; .) - OneStmt (. ss.Add(s); .) + OneStmt (. ss.Add(s); .) . /*------------------------------------------------------------------------*/ -OneStmt +OneStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); s = dummyStmt; /* to please the compiler */ BlockStmt bs; IToken bodyStart, bodyEnd; - Attributes attrs = null; // TODO: Have OneStmt accept ref Attributes attrs .) SYNC ( BlockStmt (. s = bs; .) @@ -2227,7 +2236,7 @@ OneStmt | IfStmt | WhileStmt | ForLoopStmt - | AssertStmt + | AssertStmt | AssumeStmt | BreakStmt | CalcStmt @@ -2246,10 +2255,12 @@ OneStmt LabeledStmt = (. IToken colonToken; IToken labelToken; + Attributes attrs = null; // TODO: Get it from the context .) "label" (. IToken id; labelToken = t; .) LabelName ":" (. colonToken = t; .) - OneStmt + { AtAttribute } + OneStmt (. s.Labels = new LList