From 717eaee0063074b804098d3cfd44a7a3f822b064 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 16 Feb 2010 05:07:46 +0000 Subject: Implemented block coalescing invoked right after type checking. Controlled by the option /coalesceBlocks (default is to perform the optimization). --- Source/BoogieDriver/BoogieDriver.ssc | 5 +++ Source/Core/CommandLineOptions.ssc | 24 ++++++++++- Source/Core/DeadVarElim.ssc | 78 +++++++++++++++++++++++++++++++++++- Source/VCGeneration/VC.ssc | 2 +- 4 files changed, 106 insertions(+), 3 deletions(-) (limited to 'Source') diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 035879ec..7b22d6fe 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -420,6 +420,11 @@ namespace Microsoft.Boogie // Eliminate dead variables Microsoft.Boogie.UnusedVarEliminator.Eliminate(program); + // Coalesce blocks + if (CommandLineOptions.Clo.CoalesceBlocks) { + Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program); + } + // Inline List! TopLevelDeclarations = program.TopLevelDeclarations; if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) { diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index bd54d624..2dd85a65 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -162,7 +162,8 @@ namespace Microsoft.Boogie public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set public bool RemoveEmptyBlocks = true; - + public bool CoalesceBlocks = true; + [Rep] public ProverFactory TheProverFactory; public string ProverName; [Peer] public List! ProverOptions = new List(); @@ -842,6 +843,25 @@ namespace Microsoft.Boogie } break; + case "-coalesceBlocks": + case "/coalesceBlocks": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "0": + CoalesceBlocks = false; + break; + case "1": + CoalesceBlocks = true; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + case "/DoomDebug": vcVariety = VCVariety.Doomed; useDoomDebug = true; @@ -1846,6 +1866,8 @@ namespace Microsoft.Boogie 1 = perform live variable analysis (default) /noVerify : skip VC generation and invocation of the theorem prover /noRemoveEmptyBlocks : do not remove empty blocks during VC generation + /coalesceBlocks: : 0 = do not coalesce blocks + 1 = coalesce blocks (default) /vc: : n = nested block (default for non-/prover:z3), m = nested block reach, b = flat block, r = flat block reach, diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index c7b0c7d8..e60a59c3 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -45,8 +45,84 @@ namespace Microsoft.Boogie } } + public class BlockCoalescer : StandardVisitor { + public static void CoalesceBlocks(Program! program) { + BlockCoalescer blockCoalescer = new BlockCoalescer(); + blockCoalescer.Visit(program); + } + + private static Set! ComputeMultiPredecessorBlocks(Implementation !impl) { + Set visitedBlocks = new Set(); + Set multiPredBlocks = new Set(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block! b = dfsStack.Pop(); + if (visitedBlocks.Contains(b)) { + multiPredBlocks.Add(b); + continue; + } + visitedBlocks.Add(b); + if (b.TransferCmd == null) continue; + if (b.TransferCmd is ReturnCmd) continue; + assert b.TransferCmd is GotoCmd; + GotoCmd gotoCmd = (GotoCmd) b.TransferCmd; + if (gotoCmd.labelTargets == null) continue; + foreach (Block! succ in gotoCmd.labelTargets) { + dfsStack.Push(succ); + } + } + return multiPredBlocks; + } + + public override Implementation! VisitImplementation(Implementation! impl) { + Set multiPredBlocks = ComputeMultiPredecessorBlocks(impl); + Set visitedBlocks = new Set(); + Set removedBlocks = new Set(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block! b = dfsStack.Pop(); + if (visitedBlocks.Contains(b)) continue; + visitedBlocks.Add(b); + if (b.TransferCmd == null) continue; + if (b.TransferCmd is ReturnCmd) continue; + assert b.TransferCmd is GotoCmd; + GotoCmd gotoCmd = (GotoCmd) b.TransferCmd; + if (gotoCmd.labelTargets == null) continue; + if (gotoCmd.labelTargets.Length == 1) { + Block! succ = (!)gotoCmd.labelTargets[0]; + if (!multiPredBlocks.Contains(succ)) { + foreach (Cmd! cmd in succ.Cmds) { + b.Cmds.Add(cmd); + } + b.TransferCmd = succ.TransferCmd; + if (!b.tok.IsValid && succ.tok.IsValid) + b.tok = succ.tok; + removedBlocks.Add(succ); + dfsStack.Push(b); + visitedBlocks.Remove(b); + continue; + } + } + foreach (Block! succ in gotoCmd.labelTargets) { + dfsStack.Push(succ); + } + } + + List newBlocks = new List(); + foreach (Block! b in impl.Blocks) { + if (!removedBlocks.Contains(b)) { + newBlocks.Add(b); + } + } + impl.Blocks = newBlocks; + return impl; + } + } + public class LiveVariableAnalysis { - public static void ComputeLiveVariables(Program! program, Implementation! impl) { + public static void ComputeLiveVariables(Implementation! impl) { Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis"); Graphing.Graph dag = new Graph(); dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index 24104fb4..a9b47222 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1754,7 +1754,7 @@ namespace VC #endregion if (CommandLineOptions.Clo.LiveVariableAnalysis) { - Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(program, impl); + Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl); } Convert2PassiveCmd(impl); -- cgit v1.2.3