Print effects (#1353)

This PR adds a way to control print effects. It follows the suggestion described in #1346, except that it names the command-line option `/trackPrintEffects`.

Fixes #1346

Also:

* Document {:axiom} attribute

* Add Attributes.Find method

Author: RustanLeino

RELEASE_NOTES.md

@@ -2,6 +2,7 @@
 
 - feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section [19.2](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-break-continue) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839)
 - feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option `/functionSyntax` (see `/help`) allows early adoption of the new syntax. (https://github.com/dafny-lang/dafny/pull/1832)
+- feat: Attribute `{:print}` declares that a method may have print effects. Print effects are enforced only with `/trackPrintEffects:1`.
 - fix: No warning "File contains no code" if a file only contains a submodule (https://github.com/dafny-lang/dafny/pull/1840)
 - fix: Stuck in verifying in VSCode - support for verification cancellation (https://github.com/dafny-lang/dafny/pull/1771)
 - fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855)

Source/Dafny/AST/DafnyAst.cs

@@ -426,6 +426,16 @@ public static bool Contains(Attributes attrs, string nm) {
       return attrs.AsEnumerable().Any(aa => aa.Name == nm);
     }
 
+    /// <summary>
+    /// Returns first occurrence of an attribute named <c>nm</c>, or <c>null</c> if there is no such
+    /// attribute.
+    /// </summary>
+    [Pure]
+    public static Attributes/*?*/ Find(Attributes attrs, string nm) {
+      Contract.Requires(nm != null);
+      return attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm);
+    }
+
     /// <summary>
     /// Returns true if "nm" is a specified attribute.  If it is, then:
     /// - if the attribute is {:nm true}, then value==true

Source/Dafny/DafnyOptions.cs

@@ -89,6 +89,7 @@ public enum CompilationTarget {
 
     public CompilationTarget CompileTarget = CompilationTarget.Csharp;
     public bool CompileVerbose = true;
+    public bool EnforcePrintEffects = false;
     public string DafnyPrintCompiledFile = null;
     public string CoverageLegendFile = null;
     public string MainMethod = null;
@@ -267,6 +268,14 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
             return true;
           }
 
+        case "trackPrintEffects": {
+            int printEffects = 0;
+            if (ps.GetNumericArgument(ref printEffects, 2)) {
+              EnforcePrintEffects = printEffects == 1;
+            }
+            return true;
+          }
+
         case "Main":
         case "main": {
             if (ps.ConfirmArgumentCount(1)) {
@@ -631,9 +640,6 @@ The ReferenceName is the name used to refer to the entity in the target language
       Dafny does not perform sanity checks on the arguments---it is the user's responsibility not to generate
       malformed target code.
 
-    {:axiom}
-      TODO
-
     {:handle}
       TODO
 
@@ -647,11 +653,25 @@ malformed target code.
       TODO
 
     {:axiom}
-      TODO
+      Ordinarily, the compiler gives an error for every function or
+      method without a body. If the function or method is ghost, then
+      marking it with {:axiom} suppresses the error. The {:axiom}
+      attribute says you're taking responsibility for the existence
+      of a body for the function or method.
 
     {:abstemious}
       TODO
 
+    {:print}
+      This attributes declares that a method may have print effects,
+      that is, it may use 'print' statements and may call other methods
+      that have print effects. The attribute can be applied to compiled
+      methods, constructors, and iterators, and it gives an error if
+      applied to functions or ghost methods. An overriding method is
+      allowed to use a {:print} attribute only if the overridden method
+      does.
+      Print effects are enforced only with /trackPrintEffects:1.
+
     {:nativeType}
       Can be applied to newtype declarations for integer types and
       indicates an expectation of what native type (or not) the
@@ -916,7 +936,7 @@ It can also extend Microsoft.Dafny.Plugins.PluginConfiguration to receive argume
     https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md#about-plugins
 /Main:<name>
     The (fully-qualified) name of the method to use as the executable entry point.
-    Default is the method with the {{:main}} atrribute, or else the method named 'Main'.
+    Default is the method with the {{:main}} attribute, or else the method named 'Main'.
 /compileVerbose:<n>
     0 - don't print status of compilation to the console
     1 (default) - print information such as files being written by
@@ -942,6 +962,11 @@ The compiler emits branch-coverage calls and outputs into
     <file> a legend that gives a description of each
     source-location identifier used in the branch-coverage calls.
     (use - as <file> to print to console)
+/trackPrintEffects:<n>
+    0 (default) - Every compiled method, constructor, and iterator, whether or not
+       it bears a {{:print}} attribute, may have print effects.
+    1 - A compiled method, constructor, or iterator is allowed to have print effects
+       only if it is marked with {{:print}}.
 /noCheating:<n>
     0 (default) - allow assume statements and free invariants
     1 - treat all assumptions as asserts, and drop free.

Source/Dafny/Resolver.cs

@@ -438,6 +438,7 @@ public void ResolveProgram(Program prog) {
       }
 
       rewriters.Add(new InductionRewriter(reporter));
+      rewriters.Add(new PrintEffectEnforcement(reporter));
 
       foreach (var plugin in DafnyOptions.O.Plugins) {
         rewriters.AddRange(plugin.GetRewriters(reporter));
@@ -2046,7 +2047,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport
             new Specification<FrameExpression>(new List<FrameExpression>(), null),
             new List<AttributedExpression>(),
             new Specification<Expression>(new List<Expression>(), null),
-            null, null, null);
+            null, Attributes.Find(iter.Attributes, "print"), null);
           // add these implicit members to the class
           init.EnclosingClass = iter;
           init.InheritVisibility(iter);

Source/Dafny/Resolver/PrintEffectEnforcement.cs

@@ -0,0 +1,86 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+  // ------------------- PrintEffectEnforcement -------------------
+
+  public class PrintEffectEnforcement : IRewriter {
+    internal PrintEffectEnforcement(ErrorReporter reporter) : base(reporter) {
+      Contract.Requires(reporter != null);
+    }
+
+    internal override void PostDecreasesResolve(ModuleDefinition m) {
+      foreach (var decl in m.TopLevelDecls) {
+        if (decl is IteratorDecl iter) {
+          var hasPrintAttribute = HasPrintAttribute(iter.Attributes);
+          if (!hasPrintAttribute && iter.Body != null) {
+            if (DafnyOptions.O.EnforcePrintEffects) {
+              iter.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, iter));
+            }
+          }
+        } else if (decl is TopLevelDeclWithMembers cl) {
+          foreach (var member in cl.Members) {
+            var hasPrintAttribute = HasPrintAttribute(member.Attributes);
+            if (member is Function f) {
+              if (hasPrintAttribute) {
+                Reporter.Error(MessageSource.Rewriter, member.tok, ":print attribute is not allowed on functions");
+              }
+              if (f.ByMethodDecl != null && DafnyOptions.O.EnforcePrintEffects) {
+                f.ByMethodDecl.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, f.ByMethodDecl));
+              }
+            } else if (member is Method method) {
+              if (hasPrintAttribute) {
+                if (member.IsGhost) {
+                  Reporter.Error(MessageSource.Rewriter, member.tok, ":print attribute is not allowed on ghost methods");
+                } else if (method.OverriddenMethod != null && !HasPrintAttribute(method.OverriddenMethod.Attributes, false)) {
+                  Reporter.Error(MessageSource.Rewriter, member.tok,
+                    "not allowed to override a non-printing method with a possibly printing method ('{0}')", method.Name);
+                }
+              } else if (!member.IsGhost && method.Body != null) {
+                if (DafnyOptions.O.EnforcePrintEffects) {
+                  method.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, method));
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+
+    bool HasPrintAttribute(Attributes attrs, bool checkParameters = true) {
+      var printAttribute = Attributes.Find(attrs, "print");
+      if (checkParameters && printAttribute != null && printAttribute.Args.Count != 0) {
+        Reporter.Error(MessageSource.Rewriter, printAttribute.Args[0].tok, ":print attribute does not take any arguments");
+      }
+      return printAttribute != null;
+    }
+
+    private void CheckNoPrintEffects(Statement stmt, IMethodCodeContext codeContext) {
+      if (stmt is PrintStmt) {
+        var method = codeContext as Method;
+        if (method != null && method.IsByMethod) {
+          Reporter.Error(MessageSource.Rewriter, stmt.Tok, "a function-by-method is not allowed to use print statements");
+        } else {
+          Reporter.Error(MessageSource.Rewriter, stmt.Tok,
+            "to use a print statement, the enclosing {0} must be marked with {{:print}}", method?.WhatKind ?? ((IteratorDecl)codeContext).WhatKind);
+        }
+      } else if (stmt is CallStmt call) {
+        if (HasPrintAttribute(call.Method.Attributes, false)) {
+          var method = codeContext as Method;
+          if (method != null && method.IsByMethod) {
+            Reporter.Error(MessageSource.Rewriter, stmt.Tok, "a function-by-method is not allowed to call a method with print effects");
+          } else {
+            Reporter.Error(MessageSource.Rewriter, stmt.Tok,
+              "to call a method with print effects, the enclosing {0} must be marked with {{:print}}",
+              method?.WhatKind ?? ((IteratorDecl)codeContext).WhatKind);
+          }
+        }
+      }
+      stmt.SubStatements.Iter(s => CheckNoPrintEffects(s, codeContext));
+    }
+  }
+}

Source/Dafny/Rewriter.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
 using Bpl = Microsoft.Boogie;
 using IToken = Microsoft.Boogie.IToken;
 
@@ -2058,5 +2059,3 @@ internal override void PostResolve(Program program) {
     }
   }
 }
-
-

Test/dafny0/PrintEffects.dfy

@@ -0,0 +1,107 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %dafny /compile:3 /trackPrintEffects:1 "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "hello, Main\n"; // error: cannot print from this method
+  P(); // error: cannot call printing method
+  var iter0 := new NoPrintIter(3);
+  var iter1 := new PrintIter(3);
+  var _ := iter0.MoveNext();
+  var _ := iter1.MoveNext(); // error: cannot call printing method
+  var cl0 := new Cl.NoPrint();
+  var cl1 := new Cl.Print(); // error: cannot call printing constructor
+}
+
+method {:print} P() {
+  print "method P here\n";
+  M();
+  var iter0 := new NoPrintIter(3);
+  var iter1 := new PrintIter(3);
+  print "calling MoveNexts\n";
+  MoveNexts(iter0, iter1);
+  var cl := new Cl.NoPrint();
+  cl := new Cl.Print();
+
+  TestOverrides();
+}
+
+method MoveNexts(iter0: NoPrintIter, iter1: PrintIter)
+  requires iter0.Valid() && iter1.Valid()
+  requires iter0._modifies == iter0._new == iter0._reads == {}
+  requires iter1._modifies == iter1._new == iter1._reads == {}
+  modifies iter0, iter1
+{
+  var more0 := iter0.MoveNext();
+  var more1 := iter1.MoveNext(); // error: cannot print from this method
+}
+
+method M() {
+  var x := F(3);
+  print "bye, from M\n"; // error: cannot print from this method
+}
+
+function F(x: int): int {
+  10
+} by method {
+  print "function-by-method F\n"; // error: cannot print from this method
+  return 10;
+}
+
+iterator NoPrintIter(a: int) yields (x: int)
+{
+  print "Start of Iter 0\n"; // error: cannot print from this method
+  yield 3 + a;
+  print "End of Iter 0\n"; // error: cannot print from this method
+}
+
+iterator {:print} PrintIter(a: int) yields (x: int)
+{
+  print "Start of Iter 1\n";
+  yield 3 + a;
+  print "End of Iter 1\n";
+}
+
+class Cl {
+  constructor NoPrint() {
+    print "Cl.NoPrint ctor\n"; // error: cannot print from this method
+  }
+  constructor {:print} Print() {
+    print "Cl.Print ctor\n";
+  }
+}
+
+trait Trait {
+  method {:print} MayPrint()
+  method {:print} AlwaysPrints()
+}
+
+class Overrides extends Trait {
+  method MayPrint() { // allowed to drop {:print} attribute
+    print "Override X"; // error: cannot print without a {:print} attribute
+  }
+  method {:print} AlwaysPrints() {
+    print " Y\n";
+  }
+}
+
+method {:print} TestOverrides() {
+  var c: Overrides := new Overrides;
+  var t: Trait := c;
+
+  t.MayPrint();
+  t.AlwaysPrints();
+
+  c.MayPrint();
+  c.AlwaysPrints();
+
+  TestOverridesNoPrint(c, t);
+}
+
+method TestOverridesNoPrint(c: Overrides, t: Trait) {
+  t.MayPrint(); // error: cannot call printing method
+  t.AlwaysPrints(); // error: cannot call printing method
+
+  c.MayPrint();
+  c.AlwaysPrints(); // error: cannot call printing method
+}

Test/dafny0/PrintEffects.dfy.expect

@@ -0,0 +1,34 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
+hello, Main
+method P here
+function-by-method F
+bye, from M
+calling MoveNexts
+Start of Iter 0
+Start of Iter 1
+Cl.NoPrint ctor
+Cl.Print ctor
+Override X Y
+Override X Y
+Override X Y
+Override X Y
+Start of Iter 0
+Start of Iter 1
+Cl.NoPrint ctor
+Cl.Print ctor
+PrintEffects.dfy(53,2): Error: to use a print statement, the enclosing iterator must be marked with {:print}
+PrintEffects.dfy(55,2): Error: to use a print statement, the enclosing iterator must be marked with {:print}
+PrintEffects.dfy(67,4): Error: to use a print statement, the enclosing constructor must be marked with {:print}
+PrintEffects.dfy(81,4): Error: to use a print statement, the enclosing method must be marked with {:print}
+PrintEffects.dfy(6,2): Error: to use a print statement, the enclosing method must be marked with {:print}
+PrintEffects.dfy(7,3): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(11,25): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(13,20): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(36,29): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(41,2): Error: to use a print statement, the enclosing method must be marked with {:print}
+PrintEffects.dfy(47,2): Error: a function-by-method is not allowed to use print statements
+PrintEffects.dfy(102,12): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(103,16): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+PrintEffects.dfy(106,16): Error: to call a method with print effects, the enclosing method must be marked with {:print}
+14 resolution/type errors detected in PrintEffects.dfy