Feat: {:only} attribute for members (#4075)

This PR implements a feature that fixes #4074 I added the corresponding tests, auditor entries and documentations with appropriate links. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
dafny-lang · Jun 8, 2023 · 1517136 · 1517136
1 parent b03a067
commit 1517136
Show file tree

Hide file tree

Showing 21 changed files with 211 additions and 49 deletions.
diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs
@@ -155,6 +155,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() {

diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/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));
     }
 

diff --git a/Source/DafnyCore/AST/Members/MemberDecl.cs b/Source/DafnyCore/AST/Members/MemberDecl.cs
@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using Microsoft.Dafny.Auditor;
 
 namespace Microsoft.Dafny;
 
@@ -105,4 +106,13 @@ 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);
+    }
+  }
 }
diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/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;
     }
 

diff --git a/Source/DafnyCore/Auditor/Assumption.cs b/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
   );

diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -2697,6 +2697,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();
@@ -3451,7 +3459,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

diff --git a/Source/DafnyCore/Resolver/ResolutionErrors.cs b/Source/DafnyCore/Resolver/ResolutionErrors.cs
@@ -80,7 +80,9 @@ public enum ErrorId {
     r_assignment_to_ghost_constructor_only_in_ghost,
     r_assert_only_assumes_others,
     r_assert_only_before_after,
-    r_failure_methods_deprecated
+    r_failure_methods_deprecated,
+    r_member_only_assumes_other,
+    r_member_only_has_no_before_after
   }
 
   static ResolutionErrors() {
@@ -93,5 +95,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"));
   }
 }
diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/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;

diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
@@ -31,6 +31,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.
@@ -785,23 +786,35 @@ 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.Where(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.Where(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);
       }

diff --git a/Test/auditor/TestAuditor.dfy b/Test/auditor/TestAuditor.dfy
@@ -137,3 +137,7 @@ method AssertOnly() {
   assert {:only} true;
   assert false;
 }
+
+method {:only} MethodOnly() {
+  assert false;
+}
diff --git a/Test/auditor/TestAuditor.dfy-ietf.md.expect b/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.
diff --git a/Test/auditor/TestAuditor.dfy.expect b/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
diff --git a/Test/auditor/TestAuditor.dfy.html.expect b/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>

diff --git a/Test/auditor/TestAuditor.dfy.md.expect b/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. |
diff --git a/Test/git-issues/git-issue-4074.dfy b/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;
+  }
+}
diff --git a/Test/git-issues/git-issue-4074.dfy.expect b/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
diff --git a/Test/separate-verification/assumptions.dfy.expect b/Test/separate-verification/assumptions.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
@@ -27,5 +28,6 @@ TestAuditor.dfy(124,2): Error: Definition has [assume {:axiom}] statement in bod
 TestAuditor.dfy(126,2): Error: Definition contains [forall] statement with no body.
 TestAuditor.dfy(130,2): Error: Definition contains loop with no body.
 TestAuditor.dfy(137,2): Error: Assertion has explicit temporary [{:only}] attribute.
+TestAuditor.dfy(141,15): Error: Member has explicit temporary [{:only}] attribute.
 IgnoredAssumptions.dfy(2,15): Error: Ghost declaration has no body and has an ensures clause.
 Wrote textual form of partial target program to assumptions-lib/assumptions.doo