Feat: {:only} attribute for members

Source/DafnyCore/AST/DafnyAst.cs

@@ -178,6 +178,18 @@ public interface IAttributeBearingDeclaration {
     Attributes Attributes { get; }
   }
 
+  public static class IAttributeBearingDeclarationExtensions {
+    public static bool HasUserAttribute(this IAttributeBearingDeclaration decl, string name, out Attributes attribute) {
+      if (Attributes.Find(decl.Attributes, name) is UserSuppliedAttributes attr) {
+        attribute = attr;
+        return true;
+      }
+
+      attribute = null;
+      return false;
+    }
+  }
+
   public class Attributes : TokenNode {
     [ContractInvariantMethod]
     void ObjectInvariant() {

Source/DafnyCore/AST/Function.cs

@@ -48,7 +48,7 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
       yield return a;
     }
 
-    if (Body is null && HasPostcondition && !EnclosingClass.EnclosingModuleDefinition.IsAbstract && !HasExternAttribute) {
+    if (Body is null && HasPostcondition && !EnclosingClass.EnclosingModuleDefinition.IsAbstract && !HasExternAttribute && !HasAxiomAttribute) {
       yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
     }
 

Source/DafnyCore/AST/MemberDecls.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using Microsoft.Dafny.Auditor;
 
 namespace Microsoft.Dafny;
 
@@ -105,6 +106,15 @@ public virtual string FullSanitizedName {
   }
 
   public virtual IEnumerable<Expression> SubExpressions => Enumerable.Empty<Expression>();
+
+  public override IEnumerable<Assumption> Assumptions(Declaration decl) {
+    foreach (var a in base.Assumptions(this)) {
+      yield return a;
+    }
+    if (this.HasUserAttribute("only", out _)) {
+      yield return new Assumption(decl, tok, AssumptionDescription.MemberOnly);
+    }
+  }
 }
 
 public class Field : MemberDecl, ICanFormat, IHasDocstring {

Source/DafnyCore/AST/Statements/AssertStmt.cs

@@ -57,7 +57,7 @@ public override IEnumerable<Expression> SpecificationSubExpressions {
   }
 
   public override IEnumerable<Assumption> Assumptions(Declaration decl) {
-    if (Attributes.Contains(Attributes, "only")) {
+    if (this.HasUserAttribute("only", out _)) {
       yield return new Assumption(decl, tok, AssumptionDescription.AssertOnly);
     }
   }
@@ -67,9 +67,8 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   }
 
   public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) {
-
     assertOnlyKind = AssertOnlyKind.Single;
-    if (Attributes.Find(Attributes, "only") is not UserSuppliedAttributes attribute) {
+    if (!this.HasUserAttribute("only", out var attribute)) {
       return false;
     }
 

Source/DafnyCore/Auditor/Assumption.cs

@@ -103,10 +103,18 @@ public static AssumptionDescription NoBody(bool isGhost) {
       allowedInLibraries: false);
   }
 
-  public static AssumptionDescription AssertOnly = new(
+  public static readonly AssumptionDescription AssertOnly = new(
     issue: "Assertion has explicit temporary [{:only}] attribute.",
-    mitigation: "Remove the [{:only}] attribute",
-    mitigationIETF: "Must remove the [{:only}] attribute",
+    mitigation: "Remove the [{:only}] attribute.",
+    mitigationIETF: "MUST remove the [{:only}] attribute.",
+    isExplicit: true,
+    allowedInLibraries: false
+  );
+
+  public static readonly AssumptionDescription MemberOnly = new(
+    issue: "Member has explicit temporary [{:only}] attribute.",
+    mitigation: "Remove the [{:only}] attribute.",
+    mitigationIETF: "MUST remove the [{:only}] attribute.",
     isExplicit: true,
     allowedInLibraries: false
   );

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -3252,6 +3252,14 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) {
       currentClass = cl;
       foreach (MemberDecl member in cl.Members) {
         Contract.Assert(VisibleInScope(member));
+        if (member.HasUserAttribute("only", out var attribute)) {
+          reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.RangeToken.ToToken(),
+            "Members with {:only} temporarily disable the verification of other members in the entire file");
+          if (attribute.Args.Count >= 1) {
+            reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_has_no_before_after.ToString(), attribute.Args[0].RangeToken.ToToken(),
+              "{:only} on members does not support arguments");
+          }
+        }
         if (member is Field) {
           var resolutionContext = new ResolutionContext(new NoContext(currentClass.EnclosingModuleDefinition), false);
           scope.PushMarker();
@@ -4006,7 +4014,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           }
         }
 
-        if (assertStmt != null && Attributes.Find(assertStmt.Attributes, "only") is UserSuppliedAttributes attribute) {
+        if (assertStmt != null && assertStmt.HasUserAttribute("only", out var attribute)) {
           reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_assert_only_assumes_others.ToString(), attribute.RangeToken.ToToken(),
             "Assertion with {:only} temporarily transforms other assertions into assumptions");
           if (attribute.Args.Count >= 1

Source/DafnyCore/Resolver/ResolutionErrors.cs

@@ -10,7 +10,9 @@ public class ResolutionErrors {
   public enum ErrorId {
     // ReSharper disable once InconsistentNaming
     r_assert_only_assumes_others,
-    r_assert_only_before_after
+    r_assert_only_before_after,
+    r_member_only_assumes_other,
+    r_member_only_has_no_before_after
   }
 
   static ResolutionErrors() {
@@ -23,5 +25,14 @@ static ResolutionErrors() {
       @"
 The `{:only}` attribute accepts an optional argument ""after"" or ""before"" to indicate that the assertions afterwards
 (respectively before) should be transformed into assumptions.", Replace(@"""before""", "Replace with \"before\""));
+    Add(ErrorId.r_member_only_assumes_other,
+      @"
+When annotating a member with the `{:only}` attribute, all other members of any declaration in the same file are not verified.
+This is a good way to focus on a method, a function or a lemma and its proof, but this annotation has to be removed once finished.
+This warning is a reminder about it.", Remove(true, "Finish focusing and remove {:only}"));
+    Add(ErrorId.r_member_only_has_no_before_after,
+        @"
+The `{:only}` attribute on members does not accept optional argument like ""after"" or ""before"" like the `{:only}` attribute on assertions can.",
+        Remove(true, "Remove this unused argument"));
   }
 }

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -43,7 +43,12 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc
       foreach (MemberDecl member in c.Members.FindAll(VisibleInScope)) {
         Contract.Assert(isAllocContext == null);
         currentDeclaration = member;
-        SetAssertionOnlyFilter(member);
+        if (!filterOnlyMembers || member.HasUserAttribute("only", out _)) {
+          SetAssertionOnlyFilter(member);
+        } else {
+          assertionOnlyFilter = _ => false;
+        }
+
         if (member is Field) {
           Field f = (Field)member;
           Boogie.Declaration fieldDeclaration;

Source/DafnyCore/Verifier/Translator.cs

@@ -30,6 +30,7 @@ namespace Microsoft.Dafny {
   public partial class Translator {
     private DafnyOptions options;
     public const string NameSeparator = "$$";
+    private bool filterOnlyMembers;
 
     ErrorReporter reporter;
     // TODO(wuestholz): Enable this once Dafny's recommended Z3 version includes changeset 0592e765744497a089c42021990740f303901e67.
@@ -792,23 +793,36 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
       mods.Remove(forModule);
       mods.Insert(0, forModule);
 
-      foreach (ModuleDefinition m in mods) {
-        foreach (TopLevelDecl d in m.TopLevelDecls.FindAll(VisibleInScope)) {
-          currentDeclaration = d;
-          if (d is AbstractTypeDecl) {
-            var dd = (AbstractTypeDecl)d;
-            AddTypeDecl(dd);
-            AddClassMembers(dd, true, true);
-          } else if (d is ModuleDecl) {
-            // submodules have already been added as a top level module, ignore this.
-          } else if (d is RevealableTypeDecl) {
-            AddTypeDecl((RevealableTypeDecl)d);
-          } else {
-            Contract.Assert(false);
-          }
+
+      var visibleTopLevelDecls =
+        mods.SelectMany(m => m.TopLevelDecls.FindAll(VisibleInScope));
+
+      if (visibleTopLevelDecls.Any(
+            d => d is TopLevelDeclWithMembers memberContainer &&
+                 memberContainer.Members.Any(
+                   member =>
+                     Attributes.Contains(member.Attributes, "only")
+                 ))) {
+        filterOnlyMembers = true;
+      }
+
+      foreach (TopLevelDecl d in visibleTopLevelDecls) {
+        currentDeclaration = d;
+        if (d is AbstractTypeDecl) {
+          var dd = (AbstractTypeDecl)d;
+          AddTypeDecl(dd);
+          AddClassMembers(dd, true, true);
+        } else if (d is ModuleDecl) {
+          // submodules have already been added as a top level module, ignore this.
+        } else if (d is RevealableTypeDecl) {
+          AddTypeDecl((RevealableTypeDecl)d);
+        } else {
+          Contract.Assert(false);
         }
       }
 
+      filterOnlyMembers = false;
+
       foreach (var c in tytagConstants.Values) {
         sink.AddTopLevelDeclaration(c);
       }

Test/auditor/TestAuditor.dfy

@@ -137,3 +137,7 @@ method AssertOnly() {
   assert {:only} true;
   assert false;
 }
+
+method {:only} MethodOnly() {
+  assert false;
+}

Test/auditor/TestAuditor.dfy-ietf.md.expect

@@ -76,4 +76,8 @@
 
 ### Member `AssertOnly`
 
-* Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute
+* Assertion has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute.
+
+### Member `MethodOnly`
+
+* Member has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute.

Test/auditor/TestAuditor.dfy.expect

@@ -1,4 +1,5 @@
 TestAuditor.dfy(137,9): Warning: Assertion with {:only} temporarily transforms other assertions into assumptions
+TestAuditor.dfy(141,7): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
 TestAuditor.dfy(95,4): Warning: note, this forall statement has no body
 TestAuditor.dfy(102,4): Warning: note, this loop has no body (loop frame: i)
 TestAuditor.dfy(126,2): Warning: note, this forall statement has no body
@@ -23,7 +24,8 @@ TestAuditor.dfy(95,4): Warning: ForallWithoutBody: Definition contains `forall`
 TestAuditor.dfy(102,4): Warning: LoopWithoutBody: Definition contains loop with no body. Possible mitigation: Provide a body.
 TestAuditor.dfy(118,21): Warning: ConcurrentMethod: Declaration has `{:concurrent}` attribute. Possible mitigation: Manually review and test in a concurrent setting.
 TestAuditor.dfy(122,16): Warning: AxiomWithStuffInIt: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
-TestAuditor.dfy(137,2): Warning: AssertOnly: Assertion has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute
-Dafny auditor completed with 18 findings
+TestAuditor.dfy(137,2): Warning: AssertOnly: Assertion has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
+TestAuditor.dfy(141,15): Warning: MethodOnly: Member has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
+Dafny auditor completed with 19 findings
 
 Dafny program verifier did not attempt verification

Test/auditor/TestAuditor.dfy.html.expect

@@ -50,7 +50,8 @@
 <tr><td>LoopWithoutBody</td><td>True</td><td>False</td><td>False</td><td>Definition contains loop with no body.</td><td>Provide a body.</td></tr>
 <tr><td>ConcurrentMethod</td><td>True</td><td>False</td><td>False</td><td>Declaration has <code>{:concurrent}</code> attribute.</td><td>Manually review and test in a concurrent setting.</td></tr>
 <tr><td>AxiomWithStuffInIt</td><td>True</td><td>True</td><td>False</td><td>Declaration has explicit <code>{:axiom}</code> attribute.</td><td>Provide a proof or test.</td></tr>
-<tr><td>AssertOnly</td><td>True</td><td>False</td><td>False</td><td>Assertion has explicit temporary <code>{:only}</code> attribute.</td><td>Remove the <code>{:only}</code> attribute</td></tr>
+<tr><td>AssertOnly</td><td>True</td><td>False</td><td>False</td><td>Assertion has explicit temporary <code>{:only}</code> attribute.</td><td>Remove the <code>{:only}</code> attribute.</td></tr>
+<tr><td>MethodOnly</td><td>True</td><td>False</td><td>False</td><td>Member has explicit temporary <code>{:only}</code> attribute.</td><td>Remove the <code>{:only}</code> attribute.</td></tr>
 </table>
 <script>$( "table" ).last().addClass( "sortable" );</script>
 </body>

Test/auditor/TestAuditor.dfy.md.expect

@@ -17,4 +17,5 @@
 | LoopWithoutBody | True | False | False | Definition contains loop with no body. | Provide a body. |
 | ConcurrentMethod | True | False | False | Declaration has `{:concurrent}` attribute. | Manually review and test in a concurrent setting. |
 | AxiomWithStuffInIt | True | True | False | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. |
-| AssertOnly | True | False | False | Assertion has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute |
+| AssertOnly | True | False | False | Assertion has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. |
+| MethodOnly | True | False | False | Member has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. |

Test/git-issues/git-issue-4074.dfy

@@ -0,0 +1,30 @@
+// RUN: %exits-with 4 %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method {:only "wrongArgument"} TestReported() {
+  assert false; // An error here
+}
+
+method TestNotReported() {
+  assert false;
+}
+
+class A {
+  method {:only} TestReported() {
+    assert false; // An error here
+  }
+
+  method TestNotReported() {
+    assert false;
+  }
+}
+
+module B {
+  method {:only} TestReported() {
+    assert false; // An error here
+  }
+
+  method TestNotReported() {
+    assert false;
+  }
+}

Test/git-issues/git-issue-4074.dfy.expect

@@ -0,0 +1,9 @@
+git-issue-4074.dfy(23,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
+git-issue-4074.dfy(13,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
+git-issue-4074.dfy(4,7): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
+git-issue-4074.dfy(4,14): Warning: {:only} on members does not support arguments
+git-issue-4074.dfy(24,11): Error: assertion might not hold
+git-issue-4074.dfy(14,11): Error: assertion might not hold
+git-issue-4074.dfy(5,9): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 3 errors