fix: For attributes, add missing resolution and fix pointless parsing

RELEASE_NOTES.md

@@ -12,6 +12,7 @@
 - fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (https://github.com/dafny-lang/dafny/pull/1862)
 - fix: Plug two memory leaks in Dafny's verification server (#1858, #1863)
 - fix: Generate missing termination measures for subset types on sequences (#1875)
+- fix: Resolve expressions in attributes in all specifications of functions and iterators. (https://github.com/dafny-lang/dafny/pull/1900)
 
 # 3.4.2
 

Source/Dafny/AST/DafnyAst.cs

@@ -395,6 +395,7 @@ public IEnumerable<BoundVar> AllBoundVars {
   /// A class implementing this interface is one that can carry attributes.
   /// </summary>
   public interface IAttributeBearingDeclaration {
+    Attributes Attributes { get; }
   }
 
   public class Attributes {
@@ -3443,6 +3444,7 @@ public bool IsExtern(out string/*?*/ qualification, out string/*?*/ name) {
       return false;
     }
     public Attributes Attributes;  // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
 
     public Declaration(IToken tok, string name, Attributes attributes, bool isRefining) {
       Contract.Requires(tok != null);
@@ -3949,6 +3951,7 @@ public string FullName {
     string INamedRegion.Name { get { return Name; } }
     public ModuleDefinition EnclosingModule;  // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered
     public readonly Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
     public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base
     public bool SuccessfullyResolved;  // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved
 
@@ -7765,6 +7768,7 @@ public class LocalVariable : IVariable, IAttributeBearingDeclaration {
     public readonly IToken EndTok;  // typically a terminating semi-colon or end-curly-brace
     readonly string name;
     public Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
     public bool IsGhost;
     [ContractInvariantMethod]
     void ObjectInvariant() {
@@ -8023,12 +8027,14 @@ public override IEnumerable<Expression> NonSpecificationSubExpressions {
     }
   }
 
-  public class GuardedAlternative {
+  public class GuardedAlternative : IAttributeBearingDeclaration {
     public readonly IToken Tok;
     public readonly bool IsBindingGuard;
     public readonly Expression Guard;
     public readonly List<Statement> Body;
     public Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(Tok != null);
@@ -11234,6 +11240,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari
     public readonly Expression Body;
     public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
     public readonly Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
     public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; 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
@@ -11336,6 +11343,7 @@ void ObjectInvariant() {
     }
 
     public Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
 
     public abstract class BoundedPool {
       [Flags]
@@ -12459,9 +12467,10 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) {
     }
   }
 
-  public class NestedMatchCaseExpr : NestedMatchCase {
+  public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration {
     public readonly Expression Body;
     public Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
 
     public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) {
       Contract.Requires(body != null);
@@ -12470,9 +12479,10 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att
     }
   }
 
-  public class NestedMatchCaseStmt : NestedMatchCase {
+  public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration {
     public readonly List<Statement> Body;
     public Attributes Attributes;
+    Attributes IAttributeBearingDeclaration.Attributes => Attributes;
     public NestedMatchCaseStmt(IToken tok, ExtendedPattern pat, List<Statement> body) : base(tok, pat) {
       Contract.Requires(body != null);
       this.Body = body;
@@ -12596,7 +12606,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public class AttributedExpression {
+  public class AttributedExpression : IAttributeBearingDeclaration {
     public readonly Expression E;
     public readonly AssertLabel/*?*/ Label;
 
@@ -13016,7 +13026,7 @@ public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List<ActualB
     }
   }
 
-  public class Specification<T> where T : class {
+  public class Specification<T> : IAttributeBearingDeclaration where T : class {
     public readonly List<T> Expressions;
 
     [ContractInvariantMethod]

Source/Dafny/Dafny.atg

@@ -1831,10 +1831,8 @@ DecreasesClause<.List<Expression> decreases, ref Attributes attrs,
 /*------------------------------------------------------------------------*/
 ReadsClause<.List<FrameExpression/*!*/>/*!*/ reads,
                   bool allowLemma, bool allowLambda, bool allowWild.>
-= "reads"                                             (. Attributes attrs = null;
-                                                         FrameExpression fe;
-                                                       .)
-  { Attribute<ref attrs> }
+= "reads"
+  (. FrameExpression fe; .)
   PossiblyWildFrameExpression<out fe, allowLemma, allowLambda, allowWild>          (. reads.Add(fe); .)
   { "," PossiblyWildFrameExpression<out fe, allowLemma, allowLambda, allowWild>    (. reads.Add(fe); .)
   }
@@ -2134,6 +2132,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      List<AttributedExpression> ens = new List<AttributedExpression>();
      List<FrameExpression> reads = new List<FrameExpression>();
      List<Expression> decreases;
+     Attributes decAttrs = null;
      Expression body = null;
      bool isPredicate = false; bool isLeastPredicate = false; bool isGreatestPredicate = false;
      IToken/*?*/ headToken = null; // used only for a basic "function" or "predicate"
@@ -2259,7 +2258,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
   )
 
   (. decreases = isLeastPredicate || isGreatestPredicate ? null : new List<Expression/*!*/>(); .)
-  FunctionSpec<reqs, reads, ens, decreases>
+  FunctionSpec<reqs, reads, ens, decreases, ref decAttrs>
   (. IToken byMethodTok = null; BlockStmt byMethodBody = null; .)
   [ FunctionBody<out body, out bodyStart, out bodyEnd, out byMethodTok, out byMethodBody> ]
 
@@ -2400,15 +2399,15 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      if (isTwoState && isPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals,
-                                 reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
+                                 reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
      } else if (isTwoState) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new TwoStateFunction(tok, id.val, dmod.IsStatic, typeArgs, formals, result, returnType,
-                                reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
+                                reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
      } else if (isPredicate) {
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
        f = new Predicate(tok, id.val, dmod.IsStatic, isGhost, typeArgs, formals,
-                         reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited,
+                         reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited,
                          byMethodTok, byMethodBody, attrs, signatureEllipsis);
      } else if (isLeastPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
@@ -2422,7 +2421,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
        f = new Function(tok, id.val, dmod.IsStatic, isGhost,
                         typeArgs, formals, result, returnType,
-                        reqs, reads, ens, new Specification<Expression>(decreases, null), body,
+                        reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body,
                         byMethodTok, byMethodBody,
                         attrs, signatureEllipsis);
      }
@@ -2437,11 +2436,10 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
   .
 
 /*------------------------------------------------------------------------*/
-FunctionSpec<.List<AttributedExpression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<AttributedExpression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>
+FunctionSpec<.List<AttributedExpression> reqs, List<FrameExpression> reads, List<AttributedExpression> ens, List<Expression> decreases, ref Attributes decAttrs.>
 = (. Contract.Requires(cce.NonNullElements(reqs));
      Contract.Requires(cce.NonNullElements(reads));
      Contract.Requires(decreases == null || cce.NonNullElements(decreases));
-     Attributes attrs = null;
   .)
   SYNC
   { RequiresClause<reqs, true>
@@ -2452,7 +2450,7 @@ FunctionSpec<.List<AttributedExpression/*!*/>/*!*/ reqs, List<FrameExpression/*!
          decreases = new List<Expression/*!*/>();
        }
     .)
-    DecreasesClause<decreases, ref attrs, false, false>
+    DecreasesClause<decreases, ref decAttrs, false, false>
   }
   .
 
@@ -3999,8 +3997,7 @@ LambdaExpression<out Expression e, bool allowLemma, bool allowBitwiseOps>
 // Coco says LambdaSpec is deletable. This is OK (it might be empty).
 LambdaSpec<.ref List<FrameExpression> reads, ref Expression req.>
 = { ReadsClause<reads, true, false, true>
-  | "requires"                             (. Attributes attrs = null; .)
-    { Attribute<ref attrs> }               (. Expression ee; .)
+  | "requires"                             (. Expression ee; .)
     Expression<out ee, true, false>        (. req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee); .)
   }
   .