From 03be2f186637abda08d9351a37313b1e19850011 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 12 Feb 2010 04:52:41 +0000 Subject: --- Source/BoogieDriver/BoogieDriver.ssc | 4 +- Source/Core/AbsyCmd.ssc | 7 ++ Source/Core/CommandLineOptions.ssc | 27 ++++- Source/Core/DeadVarElim.ssc | 148 ++++++++++++++++++++++++++-- Source/VCGeneration/ConditionGeneration.ssc | 5 +- Source/VCGeneration/VC.ssc | 4 + 6 files changed, 179 insertions(+), 16 deletions(-) (limited to 'Source') diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 423b436f..035879ec 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -70,7 +70,7 @@ namespace Microsoft.Boogie SelectPlatform(CommandLineOptions.Clo); - Helpers.ExtraTraceInformation("Becoming sentinent"); + Helpers.ExtraTraceInformation("Becoming sentient"); // Make sure the Spec# runtime is initialized. // This happens when the static constructor for the Runtime type is executed. @@ -418,7 +418,7 @@ namespace Microsoft.Boogie static PipelineOutcome EliminateDeadVariablesAndInline(Program! program) { // Eliminate dead variables - Microsoft.Boogie.DeadVarEliminator.Eliminate(program); + Microsoft.Boogie.UnusedVarEliminator.Eliminate(program); // Inline List! TopLevelDeclarations = program.TopLevelDeclarations; diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index 723b40e3..d0c65c96 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -696,6 +696,12 @@ namespace Microsoft.Boogie // VC generation and SCC computation public BlockSeq! Predecessors; + public Set liveVarsBefore; + public bool IsLive(Variable! v) { + if (liveVarsBefore == null) return true; + return liveVarsBefore.Contains(v); + } + public Block() { this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken));} public Block (IToken! tok, string! label, CmdSeq! cmds, TransferCmd transferCmd) @@ -707,6 +713,7 @@ namespace Microsoft.Boogie this.PreInvariant = null; this.PostInvariant = null; this.Predecessors = new BlockSeq(); + this.liveVarsBefore = null; this.TraversingStatus = VisitState.ToVisit; this.iterations = 0; // base(tok); diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 6a9eac04..bd54d624 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -228,6 +228,8 @@ namespace Microsoft.Boogie public bool ReflectAdd = false; + public bool LiveVariableAnalysis = true; + // Static constructor static CommandLineOptions() { @@ -821,6 +823,25 @@ namespace Microsoft.Boogie } break; + case "-liveVariableAnalysis": + case "/liveVariableAnalysis": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "0": + LiveVariableAnalysis = false; + break; + case "1": + LiveVariableAnalysis = 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; @@ -1141,7 +1162,7 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("z3types", ref Z3types) || ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) || ps.CheckBooleanFlag("monomorphize", ref Monomorphize) || - ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) + ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ) { // one of the boolean flags matched @@ -1820,7 +1841,9 @@ namespace Microsoft.Boogie /break[:method] : break into debugger ---- Verification-condition generation options ----------------------------- - + + /liveVariableAnalysis: : 0 = do not perform live variable analysis + 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 /vc: : n = nested block (default for non-/prover:z3), diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index 897ca9e8..c7b0c7d8 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -1,18 +1,17 @@ using System; using System.Collections.Generic; - +using Graphing; + namespace Microsoft.Boogie { - public class DeadVarEliminator : StandardVisitor { + public class UnusedVarEliminator : VariableCollector { public static void Eliminate(Program! program) { - DeadVarEliminator elim = new DeadVarEliminator(); + UnusedVarEliminator elim = new UnusedVarEliminator(); elim.Visit(program); } - - private System.Collections.Generic.Set! usedVars; - private DeadVarEliminator() { - usedVars = new System.Collections.Generic.Set(); + private UnusedVarEliminator() { + base(); } public override Implementation! VisitImplementation(Implementation! node) { @@ -30,12 +29,141 @@ namespace Microsoft.Boogie usedVars.Clear(); return impl; } + } + + public class VariableCollector : StandardVisitor { + public System.Collections.Generic.Set! usedVars; + public VariableCollector() { + usedVars = new System.Collections.Generic.Set(); + } - public override Expr! VisitIdentifierExpr(IdentifierExpr! node) - { - if (node.Decl != null) + public override Expr! VisitIdentifierExpr(IdentifierExpr! node) { + if (node.Decl != null) { usedVars.Add(node.Decl); + } return node; } + } + + public class LiveVariableAnalysis { + public static void ComputeLiveVariables(Program! program, 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 + foreach (Block b in impl.Blocks) + { + GotoCmd gtc = b.TransferCmd as GotoCmd; + if (gtc != null) + { + assume gtc.labelTargets != null; + foreach (Block! dest in gtc.labelTargets) + { + dag.AddEdge(dest, b); + } + } + } + + IEnumerable sortedNodes = dag.TopologicalSort(); + foreach (Block! block in sortedNodes) { + Set! liveVarsAfter = new Set(); + if (block.TransferCmd is GotoCmd) { + GotoCmd gotoCmd = (GotoCmd) block.TransferCmd; + if (gotoCmd.labelTargets != null) { + foreach (Block! succ in gotoCmd.labelTargets) { + assert succ.liveVarsBefore != null; + liveVarsAfter.AddAll(succ.liveVarsBefore); + } + } + } + + CmdSeq cmds = block.Cmds; + int len = cmds.Length; + for (int i = len - 1; i >= 0; i--) { + Propagate(cmds[i], liveVarsAfter); + } + + block.liveVarsBefore = liveVarsAfter; + } + } + + // perform in place update of liveSet + private static void Propagate(Cmd! cmd, Set! liveSet) { + if (cmd is AssignCmd) { + AssignCmd! assignCmd = (AssignCmd) cmd; + // I must first iterate over all the targets and remove the live ones. + // After the removals are done, I must add the variables referred on + // the right side of the removed targets + Set indexSet = new Set(); + int index = 0; + foreach (AssignLhs! lhs in assignCmd.Lhss) { + Variable var = lhs.DeepAssignedVariable; + if (var != null && liveSet.Contains(var)) { + indexSet.Add(index); + if (lhs is SimpleAssignLhs) { + // we should only remove non-map target variables because there is an implicit + // read of a map variable in an assignment to it + liveSet.Remove(var); + } + } + index++; + } + index = 0; + foreach (Expr! expr in assignCmd.Rhss) { + if (indexSet.Contains(index)) { + VariableCollector! collector = new VariableCollector(); + collector.Visit(expr); + liveSet.AddAll(collector.usedVars); + AssignLhs lhs = assignCmd.Lhss[index]; + if (lhs is MapAssignLhs) { + // If the target is a map, then all indices are also read + MapAssignLhs malhs = (MapAssignLhs) lhs; + foreach (Expr e in malhs.Indexes) { + VariableCollector! c = new VariableCollector(); + c.Visit(e); + liveSet.AddAll(c.usedVars); + } + } + } + index++; + } + } else if (cmd is HavocCmd) { + HavocCmd! havocCmd = (HavocCmd) cmd; + foreach (IdentifierExpr! expr in havocCmd.Vars) { + if (expr.Decl != null) { + liveSet.Remove(expr.Decl); + } + } + } else if (cmd is PredicateCmd) { + assert (cmd is AssertCmd || cmd is AssumeCmd); + PredicateCmd! predicateCmd = (PredicateCmd) cmd; + if (predicateCmd.Expr is LiteralExpr) { + LiteralExpr le = (LiteralExpr) predicateCmd.Expr; + if (le.IsFalse) { + liveSet.Clear(); + } + } else { + VariableCollector! collector = new VariableCollector(); + collector.Visit(predicateCmd.Expr); + liveSet.AddAll(collector.usedVars); + } + } else if (cmd is CommentCmd) { + // comments are just for debugging and don't affect verification + } else if (cmd is SugaredCmd) { + SugaredCmd! sugCmd = (SugaredCmd) cmd; + Propagate(sugCmd.Desugaring, liveSet); + } else if (cmd is StateCmd) { + StateCmd! stCmd = (StateCmd) cmd; + CmdSeq! cmds = stCmd.Cmds; + int len = cmds.Length; + for (int i = len - 1; i >= 0; i--) { + Propagate(cmds[i], liveSet); + } + foreach (Variable! v in stCmd.Locals) { + liveSet.Remove(v); + } + } else { + assert false; + } + } } } \ No newline at end of file diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index e0088bb8..922ee68d 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -718,7 +718,7 @@ namespace VC { if (!incarnationMap.Contains(v)) { - // v was not in the domain of the precessors seen so far, so it needs to be fixed up + // v was not in the domain of the predecessors seen so far, so it needs to be fixed up fixUps.Add(v); } else @@ -735,8 +735,9 @@ namespace VC } #region Second, for all variables in the fixups list, introduce a new incarnation and push it back into the preds. - foreach (Variable! v in fixUps ) + foreach (Variable! v in fixUps) { + if (!b.IsLive(v)) continue; Variable v_prime = CreateIncarnation(v, b); IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime); assert incarnationMap != null; diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index 7a3a772c..24104fb4 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1753,6 +1753,10 @@ namespace VC } #endregion + if (CommandLineOptions.Clo.LiveVariableAnalysis) { + Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(program, impl); + } + Convert2PassiveCmd(impl); #region Peep-hole optimizations -- cgit v1.2.3