Hide statements (#5562)

### Description - Introduce hide statements, which work together with the existing reveal statements. A function that has _not_ been declared `opaque`, can still be hidden using `hide`. Hiding all functions can be done using `hide *`. Hide statements can be used as an alternative to making functions `opaque`, and unlike `opaque`, allow optimizing the performance of specific proofs in your codebase without affecting the remaining code. ### How has this been tested? - Added several CLI tests related to hiding and revealing <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>
dafny-lang · Jul 24, 2024 · 281922d · 281922d
1 parent f1b0c01
commit 281922d
Show file tree

Hide file tree

Showing 66 changed files with 2,264 additions and 850 deletions.
diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs
@@ -61,7 +61,7 @@ public Expression GetSConclusion() {
     } else if (S is CalcStmt) {
       var s = (CalcStmt)S;
       return s.Result;
-    } else if (S is RevealStmt) {
+    } else if (S is HideRevealStmt) {
       return CreateBoolLiteral(tok, true);  // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
     } else if (S is UpdateStmt) {
       return CreateBoolLiteral(tok, true);  // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)

diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs
@@ -25,6 +25,8 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca
     theModule = new FileModuleDefinition(scanner.FirstToken);
   }
 
+  bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident);
+
   bool IsIdentifier(int kind) {
     return kind == _ident || kind == _least || kind == _greatest || kind == _older || kind == _opaque;
   }
@@ -156,7 +158,12 @@ bool IsWitness() {
   }
 
   bool IsFunctionDecl() {
-    switch (la.kind) {
+    var kind = la.kind;
+    return IsFunctionDecl(kind);
+  }
+
+  private bool IsFunctionDecl(int kind) {
+    switch (kind) {
       case _function:
       case _predicate:
       case _copredicate:
@@ -620,7 +627,6 @@ class DeclModifierData {
     public bool IsOpaque;
     public IToken OpaqueToken;
     public IToken FirstToken;
-
   }
 
   private ModuleKindEnum GetModuleKind(DeclModifierData mods) {

diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
@@ -70,8 +70,8 @@ public void PrintStatement(Statement stmt, int indent) {
         PrintAttributeArgs(s.Args, true);
         wr.Write(";");
 
-      } else if (stmt is RevealStmt revealStmt) {
-        PrintRevealStmt(revealStmt);
+      } else if (stmt is HideRevealStmt revealStmt) {
+        PrintHideReveal(revealStmt);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -457,17 +457,21 @@ public void PrintStatement(Statement stmt, int indent) {
       }
     }
 
-    private void PrintRevealStmt(RevealStmt revealStmt) {
-      wr.Write("reveal ");
-      var sep = "";
-      foreach (var e in revealStmt.Exprs) {
-        wr.Write(sep);
-        sep = ", ";
-        if (RevealStmt.SingleName(e) != null) {
-          // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
-          wr.Write(RevealStmt.SingleName(e));
-        } else {
-          PrintExpression(e, true);
+    private void PrintHideReveal(HideRevealStmt revealStmt) {
+      wr.Write(revealStmt.Mode == Bpl.HideRevealCmd.Modes.Hide ? "hide " : "reveal ");
+      if (revealStmt.Wildcard) {
+        wr.Write("*");
+      } else {
+        var sep = "";
+        foreach (var e in revealStmt.Exprs) {
+          wr.Write(sep);
+          sep = ", ";
+          if (HideRevealStmt.SingleName(e) != null) {
+            // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
+            wr.Write(HideRevealStmt.SingleName(e));
+          } else {
+            PrintExpression(e, true);
+          }
         }
       }
       wr.Write(";");

diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs
@@ -979,7 +979,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes,
       if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes) {
         bool verify = true;
         if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; }
-        if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; }
+        if (name.Contains("INTERNAL") || name.StartsWith(HideRevealStmt.RevealLemmaPrefix)) { return true; }
       }
       return false;
     }

diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs
@@ -402,14 +402,15 @@ public override void Resolve(ModuleResolver resolver) {
 
     resolver.ResolveParameterDefaultValues(Ins, ResolutionContext.FromCodeContext(this));
 
+    var contractContext = new ResolutionContext(this, this is TwoStateFunction);
     foreach (var req in Req) {
-      resolver.ResolveAttributes(req, new ResolutionContext(this, this is TwoStateFunction));
+      resolver.ResolveAttributes(req, contractContext);
       Expression r = req.E;
-      resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction));
+      resolver.ResolveExpression(r, contractContext);
       Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression
       resolver.ConstrainTypeExprBool(r, "Precondition must be a boolean (got {0})");
     }
-    resolver.ResolveAttributes(Reads, new ResolutionContext(this, this is TwoStateFunction));
+    resolver.ResolveAttributes(Reads, contractContext);
     foreach (FrameExpression fr in Reads.Expressions) {
       resolver.ResolveFrameExpressionTopLevel(fr, FrameExpressionUse.Reads, this);
     }
@@ -420,16 +421,16 @@ public override void Resolve(ModuleResolver resolver) {
     }
     foreach (AttributedExpression e in Ens) {
       Expression r = e.E;
-      resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateFunction));
-      resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction) with { InFunctionPostcondition = true });
+      resolver.ResolveAttributes(e, contractContext);
+      resolver.ResolveExpression(r, contractContext with { InFunctionPostcondition = true });
       Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression
       resolver.ConstrainTypeExprBool(r, "Postcondition must be a boolean (got {0})");
     }
     resolver.scope.PopMarker(); // function result name
 
-    resolver.ResolveAttributes(Decreases, new ResolutionContext(this, this is TwoStateFunction));
+    resolver.ResolveAttributes(Decreases, contractContext);
     foreach (Expression r in Decreases.Expressions) {
-      resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction));
+      resolver.ResolveExpression(r, contractContext);
       // any type is fine
     }
     resolver.SolveAllTypeConstraints(); // solve type constraints in the specification
@@ -458,7 +459,7 @@ public override void Resolve(ModuleResolver resolver) {
     if (Result != null) {
       resolver.scope.Push(Result.Name, Result);  // function return only visible in post-conditions (and in function attributes)
     }
-    resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateFunction), true);
+    resolver.ResolveAttributes(this, contractContext, true);
     resolver.scope.PopMarker(); // function result name
 
     resolver.scope.PopMarker(); // formals

diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs
@@ -46,6 +46,9 @@ public static ICodeContext Unwrap(ICodeContext codeContext) {
   }
 }
 
+interface ICodeContainer {
+  bool ContainsHide { get; set; }
+}
 
 /// <summary>
 /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl.

diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
@@ -28,7 +28,6 @@ static Method() {
     Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
     Concat(Req).Concat(Ens).Concat(Reads.Expressions).Concat(Mod.Expressions);
   public override IEnumerable<INode> PreResolveChildren => Children;
-
   public override string WhatKind => "method";
   public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } }
   public readonly IToken SignatureEllipsis;
@@ -142,7 +141,8 @@ public Method(RangeToken rangeToken, Name name,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,
     [Captured] BlockStmt body,
-    Attributes attributes, IToken signatureEllipsis, bool isByMethod = false)
+    Attributes attributes, IToken signatureEllipsis,
+    bool isByMethod = false)
     : base(rangeToken, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null,
       typeArgs, ins, req, ens, decreases) {
     Contract.Requires(rangeToken != null);
@@ -283,29 +283,31 @@ public override void Resolve(ModuleResolver resolver) {
         resolver.scope.Push(p.Name, p);
       }
 
-      resolver.ResolveParameterDefaultValues(Ins, new ResolutionContext(this, this is TwoStateLemma));
+      var resolutionContext = new ResolutionContext(this, this is TwoStateLemma);
+      resolver.ResolveParameterDefaultValues(Ins, resolutionContext);
 
       // Start resolving specification...
       foreach (AttributedExpression e in Req) {
-        resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateLemma));
-        resolver.ResolveExpression(e.E, new ResolutionContext(this, this is TwoStateLemma));
+        resolver.ResolveAttributes(e, resolutionContext);
+        resolver.ResolveExpression(e.E, resolutionContext);
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
         resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})");
       }
 
-      resolver.ResolveAttributes(Reads, new ResolutionContext(this, false));
+      var context = new ResolutionContext(this, false);
+      resolver.ResolveAttributes(Reads, context);
       foreach (FrameExpression fe in Reads.Expressions) {
         resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this);
       }
 
-      resolver.ResolveAttributes(Mod, new ResolutionContext(this, false));
+      resolver.ResolveAttributes(Mod, context);
       foreach (FrameExpression fe in Mod.Expressions) {
         resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Modifies, this);
       }
 
-      resolver.ResolveAttributes(Decreases, new ResolutionContext(this, false));
+      resolver.ResolveAttributes(Decreases, context);
       foreach (Expression e in Decreases.Expressions) {
-        resolver.ResolveExpression(e, new ResolutionContext(this, this is TwoStateLemma));
+        resolver.ResolveExpression(e, resolutionContext);
         // any type is fine
       }
 
@@ -331,8 +333,9 @@ public override void Resolve(ModuleResolver resolver) {
 
       // ... continue resolving specification
       foreach (AttributedExpression e in Ens) {
-        resolver.ResolveAttributes(e, new ResolutionContext(this, true));
-        resolver.ResolveExpression(e.E, new ResolutionContext(this, true));
+        var ensuresContext = new ResolutionContext(this, true);
+        resolver.ResolveAttributes(e, ensuresContext);
+        resolver.ResolveExpression(e.E, ensuresContext);
         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression
         resolver.ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})");
       }
@@ -366,7 +369,7 @@ public override void Resolve(ModuleResolver resolver) {
       }
 
       // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for greatest lemmas)
-      resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateLemma), true);
+      resolver.ResolveAttributes(this, resolutionContext, true);
 
       resolver.Options.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value
       resolver.scope.PopMarker();  // for the out-parameters and outermost-level locals

diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs
@@ -6,14 +6,16 @@
 
 namespace Microsoft.Dafny;
 
-public abstract class MethodOrFunction : MemberDecl {
+public abstract class MethodOrFunction : MemberDecl, ICodeContainer {
   public static readonly Option<bool> AllowExternalContracts = new("--allow-external-contracts",
     "Allow exporting callables with preconditions, and importing callables with postconditions");
 
   static MethodOrFunction() {
     DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError);
   }
 
+  [FilledInDuringResolution]
+  public bool ContainsHide { get; set; }
   public readonly List<TypeParameter> TypeArgs;
   public readonly List<AttributedExpression> Req;
   public readonly List<AttributedExpression> Ens;
@@ -39,6 +41,9 @@ protected MethodOrFunction(Cloner cloner, MethodOrFunction original) : base(clon
     this.Decreases = cloner.CloneSpecExpr(original.Decreases);
     this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr);
     this.Ins = original.Ins.ConvertAll(p => cloner.CloneFormal(p, false));
+    if (cloner.CloneResolvedFields) {
+      this.ContainsHide = original.ContainsHide;
+    }
   }
 
   protected abstract bool Bodyless { get; }

diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs b/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs
@@ -6,6 +6,7 @@ public class Label {
   public readonly IToken Tok;
   public readonly string Name;
   string uniqueId = null;
+
   public string AssignUniqueId(FreshIdGenerator idGen) {
     if (uniqueId == null) {
       uniqueId = idGen.FreshNumericId("label");

diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs
@@ -6,6 +6,7 @@ namespace Microsoft.Dafny;
 public abstract class LoopStmt : Statement, IHasNavigationToken {
   public readonly List<AttributedExpression> Invariants;
   public readonly Specification<Expression> Decreases;
+
   [FilledInDuringResolution] public bool InferredDecreases;  // says that no explicit "decreases" clause was given and an attempt was made to find one automatically (which may or may not have produced anything)
   public readonly Specification<FrameExpression> Mod;
   [ContractInvariantMethod]

diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs
@@ -9,6 +9,7 @@ public abstract class Statement : RangeNode, IAttributeBearingDeclaration {
   public override IToken Tok => PostLabelToken ?? StartToken;
   public IToken PostLabelToken { get; set; }
 
+  public int ScopeDepth { get; set; }
   public LList<Label> Labels;  // mutable during resolution
 
   private Attributes attributes;