Feat: Default function opacity setting + autoreveal option (#4342)

This PR adds an additional cmdline flag `--default-function-opacity`
which controls the default opacity of functions from `transparent`,
`autoRevealDependencies`, or `opaque`.

`transparent` is synonymous with the present behavior.
`autoRevealDependencies` is a mode which makes functions opaque by
default and inserts reveal stmts in each callable for each function
dependency. `opaque` is a mode which makes functions opaque by default,
leaving the user to insert all required function dependencies.

<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->

<!-- Is this a bug fix? Remember to include a test in Test/git-issues/
-->

<!-- Is this a bug fix for an issue introduced in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

<!-- Does this PR need tests? Add them to `Test/` or to
`Source/*.Test/…` and run them with `dotnet test` -->

<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to
learn how to do that while maintaining git history -->

<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: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: David Cok <david.r.cok@gmail.com>
Co-authored-by: davidcok <davidcok@github.com>
Co-authored-by: Mikael Mayer <mimayere@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>

Source/DafnyCore/AST/Attributes.cs

@@ -88,7 +88,7 @@ public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {
   /// the enclosing class, or any enclosing module.  Settings closer to the declaration
   /// override those further away.
   /// </summary>
-  public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName) {
+  public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName, bool defaultVal = false) {
     bool setting = true;
     if (Attributes.ContainsBool(decl.Attributes, attribName, ref setting)) {
       return setting;
@@ -107,7 +107,7 @@ public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName) {
       mod = mod.EnclosingModule;
     }
 
-    return false;
+    return defaultVal;
   }
 
   /// <summary>

Source/DafnyCore/AST/CompilationData.cs

@@ -75,6 +75,10 @@ private IList<IRewriter> GetRewriters() {
     result.Add(new LocalLinter(reporter));
     result.Add(new PrecedenceLinter(reporter, this));
 
+    if (Options.Get(CommonOptionBag.DefaultFunctionOpacity) == CommonOptionBag.DefaultFunctionOpacityOptions.AutoRevealDependencies) {
+      result.Add(new AutoRevealFunctionDependencies(reporter));
+    }
+
     foreach (var plugin in Options.Plugins) {
       result.AddRange(plugin.GetRewriters(reporter));
     }

Source/DafnyCore/AST/Expressions/Variables/Formal.cs

@@ -8,7 +8,7 @@ public class Formal : NonglobalVariable {
   public readonly bool InParam;  // true to in-parameter, false for out-parameter
   public override bool IsMutable => !InParam;
   public readonly bool IsOld;
-  public readonly Expression DefaultValue;
+  public Expression DefaultValue;
   public readonly bool IsNameOnly;
   public readonly bool IsOlder;
   public readonly string NameForCompilation;

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -4,9 +4,9 @@
 
 namespace Microsoft.Dafny;
 
-public class ConstantField : SpecialField, ICallable, ICanVerify {
+public class ConstantField : SpecialField, ICallable, ICanAutoRevealDependencies, ICanVerify {
   public override string WhatKind => "const field";
-  public readonly Expression Rhs;
+  public Expression Rhs;
 
   public override bool IsOpaque { get; }
 
@@ -51,4 +51,17 @@ public bool InferredDecreases {
   public override IEnumerable<INode> PreResolveChildren => Children;
   public ModuleDefinition ContainingModule => EnclosingModule;
   public bool ShouldVerify => Rhs != null; // This could be made more accurate by checking whether the Rhs needs to be verified.
+  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options, ErrorReporter Reporter) {
+    if (Rhs is null) {
+      return;
+    }
+
+    var addedReveals = Rewriter.ExprToFunctionalDependencies(Rhs, EnclosingModule);
+    Rhs = Rewriter.AddRevealStmtsToExpression(Rhs, addedReveals);
+
+    if (addedReveals.Any()) {
+      Reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, tok,
+        AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList()));
+    }
+  }
 }

Source/DafnyCore/AST/Members/Function.cs

@@ -8,7 +8,7 @@
 
 namespace Microsoft.Dafny;
 
-public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat, IHasDocstring, ISymbol, ICanVerify {
+public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat, IHasDocstring, ISymbol, ICanAutoRevealDependencies, ICanVerify {
   public override string WhatKind => "function";
 
   public string GetFunctionDeclarationKeywords(DafnyOptions options) {
@@ -33,6 +33,17 @@ public string GetFunctionDeclarationKeywords(DafnyOptions options) {
 
   public override bool IsOpaque { get; }
 
+  public bool IsMadeImplicitlyOpaque(DafnyOptions options) {
+    return
+       !IsOpaque &&
+       !Attributes.Contains(Attributes, "opaque") &&
+       options.Get(CommonOptionBag.DefaultFunctionOpacity) != CommonOptionBag.DefaultFunctionOpacityOptions.Transparent
+       && this is not ExtremePredicate
+       && this is not PrefixPredicate
+       && Name != "reads" && Name != "requires"
+       && !Attributes.Contains(this.Attributes, "transparent");
+  }
+
   public override bool CanBeRevealed() {
     return true;
   }
@@ -481,4 +492,77 @@ public string GetDescription(DafnyOptions options) {
     var resultType = ResultType.TypeName(options, null, false);
     return $"{WhatKind} {AstExtensions.GetMemberQualification(this)}{Name}({formals}): {resultType}";
   }
+
+  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options,
+    ErrorReporter Reporter) {
+    if (Body is null) {
+      return;
+    }
+
+    if (ByMethodDecl is not null) {
+      ByMethodDecl.AutoRevealDependencies(Rewriter, Options, Reporter);
+    }
+
+    object autoRevealDepsVal = null;
+    bool autoRevealDeps = Attributes.ContainsMatchingValue(Attributes, "autoRevealDependencies",
+      ref autoRevealDepsVal, new List<Attributes.MatchingValueOption> {
+        Attributes.MatchingValueOption.Bool,
+        Attributes.MatchingValueOption.Int
+      }, s => Reporter.Error(MessageSource.Rewriter, ErrorLevel.Error, Tok, s));
+
+    // Default behavior is reveal all dependencies
+    int autoRevealDepth = int.MaxValue;
+
+    if (autoRevealDeps) {
+      if (autoRevealDepsVal is false) {
+        autoRevealDepth = 0;
+      } else if (autoRevealDepsVal is BigInteger i) {
+        autoRevealDepth = (int)i;
+      }
+    }
+
+    var currentClass = EnclosingClass;
+    List<AutoRevealFunctionDependencies.RevealStmtWithDepth> addedReveals = new();
+
+    foreach (var func in Rewriter.GetEnumerator(this, currentClass, SubExpressions)) {
+      var revealStmt =
+        AutoRevealFunctionDependencies.BuildRevealStmt(func.Function, Tok, EnclosingClass.EnclosingModuleDefinition);
+
+      if (revealStmt is not null) {
+        addedReveals.Add(new AutoRevealFunctionDependencies.RevealStmtWithDepth(revealStmt, func.Depth));
+      }
+    }
+
+    if (autoRevealDepth > 0) {
+      Expression reqExpr = new LiteralExpr(Tok, true);
+      reqExpr.Type = Type.Bool;
+
+      var bodyExpr = Body;
+
+      foreach (var revealStmt in addedReveals) {
+        if (revealStmt.Depth <= autoRevealDepth) {
+          bodyExpr = new StmtExpr(Tok, revealStmt.RevealStmt, bodyExpr) {
+            Type = bodyExpr.Type
+          };
+
+          reqExpr = new StmtExpr(reqExpr.tok, revealStmt.RevealStmt, reqExpr) {
+            Type = Type.Bool
+          };
+        } else {
+          break;
+        }
+      }
+
+      Body = bodyExpr;
+
+      if (Req.Any() || Ens.Any()) {
+        Req.Insert(0, new AttributedExpression(reqExpr));
+      }
+    }
+
+    if (addedReveals.Any()) {
+      Reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, tok,
+        AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
+    }
+  }
 }

Source/DafnyCore/AST/Members/ICanAutoReveal.cs

@@ -0,0 +1,5 @@
+namespace Microsoft.Dafny; 
+
+public interface ICanAutoRevealDependencies {
+  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options, ErrorReporter Reporter);
+}

Source/DafnyCore/AST/Members/Method.cs

@@ -1,11 +1,13 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using System.Numerics;
 using Microsoft.Dafny.Auditor;
 
 namespace Microsoft.Dafny;
 
-public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanVerify {
+public class Method : MemberDecl, TypeParameter.ParentType,
+  IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanAutoRevealDependencies, ICanVerify {
   public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).
     Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
     Concat(Req).Concat(Ens).Concat(Reads).Concat(Mod.Expressions);
@@ -423,4 +425,72 @@ public IEnumerable<ISymbol> ChildSymbols {
 
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingClass.EnclosingModuleDefinition;
+
+  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options,
+    ErrorReporter Reporter) {
+    if (Body is null) {
+      return;
+    }
+
+    object autoRevealDepsVal = null;
+    bool autoRevealDeps = Attributes.ContainsMatchingValue(Attributes, "autoRevealDependencies",
+      ref autoRevealDepsVal, new List<Attributes.MatchingValueOption> {
+        Attributes.MatchingValueOption.Bool,
+        Attributes.MatchingValueOption.Int
+      }, s => Reporter.Error(MessageSource.Rewriter, ErrorLevel.Error, Tok, s));
+
+    // Default behavior is reveal all dependencies
+    int autoRevealDepth = int.MaxValue;
+
+    if (autoRevealDeps) {
+      if (autoRevealDepsVal is false) {
+        autoRevealDepth = 0;
+      } else if (autoRevealDepsVal is BigInteger i) {
+        autoRevealDepth = (int)i;
+      }
+    }
+
+    var currentClass = EnclosingClass;
+    List<AutoRevealFunctionDependencies.RevealStmtWithDepth> addedReveals = new();
+
+    foreach (var func in Rewriter.GetEnumerator(this, currentClass, SubExpressions)) {
+      var revealStmt =
+        AutoRevealFunctionDependencies.BuildRevealStmt(func.Function, Tok, EnclosingClass.EnclosingModuleDefinition);
+
+      if (revealStmt is not null) {
+        addedReveals.Add(new AutoRevealFunctionDependencies.RevealStmtWithDepth(revealStmt, func.Depth));
+      }
+    }
+
+    if (autoRevealDepth > 0) {
+      Expression reqExpr = new LiteralExpr(Tok, true) {
+        Type = Type.Bool
+      };
+
+      foreach (var revealStmt in addedReveals) {
+        if (revealStmt.Depth <= autoRevealDepth) {
+          if (this is Constructor c) {
+            c.BodyInit.Insert(0, revealStmt.RevealStmt);
+          } else {
+            Body.Body.Insert(0, revealStmt.RevealStmt);
+          }
+
+          reqExpr = new StmtExpr(reqExpr.tok, revealStmt.RevealStmt, reqExpr) {
+            Type = Type.Bool
+          };
+        } else {
+          break;
+        }
+      }
+
+      if (Req.Any() || Ens.Any()) {
+        Req.Insert(0, new AttributedExpression(reqExpr));
+      }
+    }
+
+    if (addedReveals.Any()) {
+      Reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, tok,
+        AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
+    }
+  }
 }