From 517cdac5a51325db09bb07bdd399e179a4747764 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 16:05:47 +0100 Subject: [PATCH] Export hidden functions (#989) Export hidden functions, used by https://github.com/dafny-lang/dafny/pull/5929 --- Source/Directory.Build.props | 2 +- Source/Provers/LeanAuto/LeanAutoGenerator.cs | 2 +- Source/VCGeneration/Prune/DataflowAnalysis.cs | 4 ++- Source/VCGeneration/Prune/Pruner.cs | 28 ++++++++++++++----- Source/VCGeneration/Prune/RevealedAnalysis.cs | 4 +-- Source/VCGeneration/Splits/Split.cs | 24 ++++++++++++++-- 6 files changed, 49 insertions(+), 15 deletions(-) diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 0fbe10344..0c24a6c28 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.4.2 + 3.4.3 net6.0 false Boogie diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs index 2235ad2b1..d58995b64 100644 --- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs +++ b/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 diff --git a/Source/VCGeneration/Prune/DataflowAnalysis.cs b/Source/VCGeneration/Prune/DataflowAnalysis.cs index 3a1896f1a..9862fc90f 100644 --- a/Source/VCGeneration/Prune/DataflowAnalysis.cs +++ b/Source/VCGeneration/Prune/DataflowAnalysis.cs @@ -22,7 +22,9 @@ protected DataflowAnalysis(IReadOnlyList roots, this.roots = roots; } - public IReadOnlyDictionary States => outStates; + public IReadOnlyDictionary OutStates => outStates; + public IReadOnlyDictionary InStates => inStates; + protected abstract TState Empty { get; } diff --git a/Source/VCGeneration/Prune/Pruner.cs b/Source/VCGeneration/Prune/Pruner.cs index 43af44c9d..28f4f9763 100644 --- a/Source/VCGeneration/Prune/Pruner.cs +++ b/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 GetLiveDeclarations(VCGenOptions options, Program program, IList? blocks) + public static (IEnumerable LiveDeclarations, ISet HiddenFunctions) GetLiveDeclarations(VCGenOptions options, Program program, IList? blocks) { if (program.DeclarationDependencies == null || blocks == null || !options.Prune) { - return program.TopLevelDeclarations; + return (program.TopLevelDeclarations, ImmutableHashSet.Empty); } var revealedState = GetRevealedState(blocks); @@ -71,15 +72,28 @@ public static IEnumerable GetLiveDeclarations(VCGenOptions options, blocksVisitor.Visit(block); } + var hiddenFunctions = new HashSet(); 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 blocks) revealedAnalysis.Run(); var assertions = controlFlowGraph.Nodes.OfType(); - return assertions.Select(assertCmd => revealedAnalysis.States[assertCmd].Peek()). + return assertions.Select(assertCmd => revealedAnalysis.OutStates[assertCmd].Peek()). Aggregate(RevealedState.AllHidden, RevealedAnalysis.MergeStates); } diff --git a/Source/VCGeneration/Prune/RevealedAnalysis.cs b/Source/VCGeneration/Prune/RevealedAnalysis.cs index 5e671b9ba..e2563d01c 100644 --- a/Source/VCGeneration/Prune/RevealedAnalysis.cs +++ b/Source/VCGeneration/Prune/RevealedAnalysis.cs @@ -9,9 +9,9 @@ namespace VCGeneration.Prune; record RevealedState(HideRevealCmd.Modes Mode, IImmutableSet 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.Empty); public static readonly RevealedState AllHidden = new(HideRevealCmd.Modes.Hide, ImmutableHashSet.Empty); } diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs index 3b8b1c6e4..8285894a4 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -27,18 +27,35 @@ public class Split : ProofRun readonly List bigBlocks = new(); public List Asserts => Blocks.SelectMany(block => block.Cmds.OfType()).ToList(); - public IReadOnlyList prunedDeclarations; - + private IReadOnlyList prunedDeclarations; + + public ISet HiddenFunctions { + get { + if (hiddenFunctions == null) { + ComputePrunedDeclsAndHiddenFunctions(); + } + return hiddenFunctions; + } + } + public IReadOnlyList 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 /*!*/ stats = new Dictionary(); @@ -199,6 +216,7 @@ public void DumpDot(int splitNum) int bsid; private readonly Func> getBlocks; + private ISet hiddenFunctions; BlockStats GetBlockStats(Block b) {