Export hidden functions (#989)

Export hidden functions, used by
dafny-lang/dafny#5929

Author: keyboardDrummer

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.4.2</Version>
+    <Version>3.4.3</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -48,7 +48,7 @@ public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, Tex
       var liveDeclarations =
         !options.Prune
           ? p.TopLevelDeclarations
-          : Pruner.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList();
+          : Pruner.GetLiveDeclarations(options, p, allBlocks.ToList()).LiveDeclarations.ToList();
 
       generator.WriteLine("-- Type constructors");
       // Always include all type constructors

Source/VCGeneration/Prune/DataflowAnalysis.cs

@@ -22,7 +22,9 @@ protected DataflowAnalysis(IReadOnlyList<TNode> roots,
     this.roots = roots;
   }
 
-  public IReadOnlyDictionary<TNode, TState> States => outStates;
+  public IReadOnlyDictionary<TNode, TState> OutStates => outStates;
+  public IReadOnlyDictionary<TNode, TState> InStates => inStates;
+
 
   protected abstract TState Empty { get; }
 

Source/VCGeneration/Prune/Pruner.cs

@@ -2,6 +2,7 @@
 using System;
 using System.Linq;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using Microsoft.Boogie.GraphUtil;
 using VCGeneration.Prune;
 
@@ -57,11 +58,11 @@ public class Pruner {
      * See Checker.Setup for more information.
      * Data type constructor declarations are not pruned and they do affect VC generation.
      */
-    public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options, Program program, IList<Block>? blocks)
+    public static (IEnumerable<Declaration> LiveDeclarations, ISet<Function> HiddenFunctions) GetLiveDeclarations(VCGenOptions options, Program program, IList<Block>? blocks)
     {
       if (program.DeclarationDependencies == null || blocks == null || !options.Prune)
       {
-        return program.TopLevelDeclarations;
+        return (program.TopLevelDeclarations, ImmutableHashSet<Function>.Empty);
       }
 
       var revealedState = GetRevealedState(blocks);
@@ -71,15 +72,28 @@ public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options,
         blocksVisitor.Visit(block);
       }
 
+      var hiddenFunctions = new HashSet<Function>();
       var keepRoots = program.TopLevelDeclarations.Where(d => d.Attributes.FindBoolAttribute("keep"));
       var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, 
         blocksVisitor.Outgoing.Concat(keepRoots).ToHashSet(), TraverseDeclaration).ToHashSet();
-      return program.TopLevelDeclarations.Where(d => 
+      var liveDeclarations = program.TopLevelDeclarations.Where(d => 
         d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d));
+      return (liveDeclarations, hiddenFunctions);
 
-      bool TraverseDeclaration(object parent, object child) {
-        return parent is not Function function || child is not Axiom axiom || revealedState.IsRevealed(function)
-               || !axiom.CanHide;
+      bool TraverseDeclaration(object parent, object child)
+      {
+        if (parent is not Function function || child is not Axiom axiom || !axiom.CanHide)
+        {
+          return true;
+        }
+
+        if (revealedState.IsRevealed(function))
+        {
+          return true;
+        }
+
+        hiddenFunctions.Add(function);
+        return false;
       }
     }
 
@@ -93,7 +107,7 @@ private static RevealedState GetRevealedState(IList<Block> blocks)
       revealedAnalysis.Run();
 
       var assertions = controlFlowGraph.Nodes.OfType<AssertCmd>();
-      return assertions.Select(assertCmd => revealedAnalysis.States[assertCmd].Peek()).
+      return assertions.Select(assertCmd => revealedAnalysis.OutStates[assertCmd].Peek()).
         Aggregate(RevealedState.AllHidden, RevealedAnalysis.MergeStates);
     }
 

Source/VCGeneration/Prune/RevealedAnalysis.cs

@@ -9,9 +9,9 @@ namespace VCGeneration.Prune;
 
 record RevealedState(HideRevealCmd.Modes Mode, IImmutableSet<Function> Offset) {
   public bool IsRevealed(Function function) {
-    return (Mode == HideRevealCmd.Modes.Hide) == Offset.Contains(function) || function.AlwaysRevealed;
+    return Mode == HideRevealCmd.Modes.Hide == Offset.Contains(function) || function.AlwaysRevealed;
   }
-
+  
   public static readonly RevealedState AllRevealed = new(HideRevealCmd.Modes.Reveal, ImmutableHashSet<Function>.Empty);
   public static readonly RevealedState AllHidden = new(HideRevealCmd.Modes.Hide, ImmutableHashSet<Function>.Empty);
 }

Source/VCGeneration/Splits/Split.cs

@@ -27,18 +27,35 @@ public class Split : ProofRun
 
       readonly List<Block> bigBlocks = new();
       public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.Cmds.OfType<AssertCmd>()).ToList();
-      public IReadOnlyList<Declaration> prunedDeclarations;
-      
+      private IReadOnlyList<Declaration> prunedDeclarations;
+
+      public ISet<Function> HiddenFunctions {
+        get {
+          if (hiddenFunctions == null) {
+            ComputePrunedDeclsAndHiddenFunctions();
+          }
+          return hiddenFunctions;
+        }
+      }
+
       public IReadOnlyList<Declaration> PrunedDeclarations {
         get {
           if (prunedDeclarations == null) {
-            prunedDeclarations = Pruner.GetLiveDeclarations(parent.Options, parent.program, Blocks).ToList();
+            ComputePrunedDeclsAndHiddenFunctions();
           }
 
           return prunedDeclarations;
         }
       }
 
+      private void ComputePrunedDeclsAndHiddenFunctions()
+      {
+        var (liveDeclarations, hiddenFunctions) =
+          Pruner.GetLiveDeclarations(parent.Options, parent.program, Blocks);
+        this.hiddenFunctions = hiddenFunctions;
+        prunedDeclarations = liveDeclarations.ToList();
+      }
+
       readonly Dictionary<Block /*!*/, BlockStats /*!*/> /*!*/
         stats = new Dictionary<Block /*!*/, BlockStats /*!*/>();
 
@@ -199,6 +216,7 @@ public void DumpDot(int splitNum)
 
       int bsid;
       private readonly Func<IList<Block>> getBlocks;
+      private ISet<Function> hiddenFunctions;
 
       BlockStats GetBlockStats(Block b)
       {