From e60e05a198970d64ea50b99bc605240d7a04e4cc Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 15 Jun 2015 20:45:32 -0700 Subject: fixed bug reported by Chris --- Source/Core/DeadVarElim.cs | 3513 ++++++++++++++++++++++--------------------- Test/civl/chris4.bpl | 16 + Test/civl/chris4.bpl.expect | 5 + 3 files changed, 1782 insertions(+), 1752 deletions(-) create mode 100644 Test/civl/chris4.bpl create mode 100644 Test/civl/chris4.bpl.expect diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 0feb5e35..fc39debb 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -1,1753 +1,1762 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; - - -namespace Microsoft.Boogie { - public class UnusedVarEliminator : VariableCollector { - public static void Eliminate(Program program) { - Contract.Requires(program != null); - UnusedVarEliminator elim = new UnusedVarEliminator(); - elim.Visit(program); - } - - private UnusedVarEliminator() - : base() { - - } - - public override Implementation VisitImplementation(Implementation node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - //Console.WriteLine("Procedure {0}", node.Name); - Implementation/*!*/ impl = base.VisitImplementation(node); - Contract.Assert(impl != null); - //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length); - List/*!*/ vars = new List(); - foreach (Variable/*!*/ var in impl.LocVars) { - Contract.Assert(var != null); - if (_usedVars.Contains(var)) - vars.Add(var); - } - impl.LocVars = vars; - //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length); - //Console.WriteLine("---------------------------------"); - _usedVars.Clear(); - return impl; - } - } - - public class ModSetCollector : ReadOnlyVisitor { - private Procedure enclosingProc; - private Dictionary/*!*/>/*!*/ modSets; - private HashSet yieldingProcs; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); - Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v))); - } - - public ModSetCollector() { - modSets = new Dictionary/*!*/>(); - yieldingProcs = new HashSet(); - } - - private bool moreProcessingRequired; - - public void DoModSetAnalysis(Program program) { - Contract.Requires(program != null); - - if (CommandLineOptions.Clo.Trace) - { -// Console.WriteLine(); -// Console.WriteLine("Running modset analysis ..."); -// int procCount = 0; -// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) -// { -// Contract.Assert(decl != null); -// if (decl is Procedure) -// procCount++; -// } -// Console.WriteLine("Number of procedures = {0}", procCount);*/ - } - - HashSet implementedProcs = new HashSet(); - foreach (var impl in program.Implementations) { - if (impl.Proc != null) - implementedProcs.Add(impl.Proc); - } - foreach (var proc in program.Procedures) { - if (!implementedProcs.Contains(proc)) - { - enclosingProc = proc; - foreach (var expr in proc.Modifies) - { - Contract.Assert(expr != null); - ProcessVariable(expr.Decl); - } - enclosingProc = null; - } - else - { - modSets.Add(proc, new HashSet()); - } - } - - moreProcessingRequired = true; - while (moreProcessingRequired) { - moreProcessingRequired = false; - this.Visit(program); - } - - foreach (Procedure x in modSets.Keys) - { - x.Modifies = new List(); - foreach (Variable v in modSets[x]) - { - x.Modifies.Add(new IdentifierExpr(v.tok, v)); - } - } - foreach (Procedure x in yieldingProcs) - { - if (!QKeyValue.FindBoolAttribute(x.Attributes, "yields")) - { - x.AddAttribute("yields"); - } - } - -#if DEBUG_PRINT - Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); - foreach (Procedure/*!*/ x in modSets.Keys) { - Contract.Assert(x != null); - Console.Write("{0} : ", x.Name); - bool first = true; - foreach (Variable/*!*/ y in modSets[x]) { - Contract.Assert(y != null); - if (first) - first = false; - else - Console.Write(", "); - Console.Write("{0}", y.Name); - } - Console.WriteLine(""); - } -#endif - } - - public override Implementation VisitImplementation(Implementation node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - enclosingProc = node.Proc; - Implementation/*!*/ ret = base.VisitImplementation(node); - Contract.Assert(ret != null); - enclosingProc = null; - - return ret; - } - public override YieldCmd VisitYieldCmd(YieldCmd node) - { - if (!yieldingProcs.Contains(enclosingProc)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - return base.VisitYieldCmd(node); - } - public override Cmd VisitAssignCmd(AssignCmd assignCmd) { - //Contract.Requires(assignCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitAssignCmd(assignCmd); - foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { - Contract.Assert(lhs != null); - ProcessVariable(lhs.DeepAssignedVariable); - } - return ret; - } - public override Cmd VisitHavocCmd(HavocCmd havocCmd) { - //Contract.Requires(havocCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitHavocCmd(havocCmd); - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - ProcessVariable(expr.Decl); - } - return ret; - } - public override Cmd VisitCallCmd(CallCmd callCmd) { - //Contract.Requires(callCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitCallCmd(callCmd); - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (ie != null) ProcessVariable(ie.Decl); - } - Procedure callee = callCmd.Proc; - if (callee == null) - return ret; - if (modSets.ContainsKey(callee)) { - foreach (Variable var in modSets[callee]) { - ProcessVariable(var); - } - } - if (!yieldingProcs.Contains(enclosingProc) && (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - if (callCmd.IsAsync) - { - if (!yieldingProcs.Contains(callCmd.Proc)) - { - yieldingProcs.Add(callCmd.Proc); - moreProcessingRequired = true; - } - } - return ret; - } - public override Cmd VisitParCallCmd(ParCallCmd node) - { - //Contract.Requires(callCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitParCallCmd(node); - if (!yieldingProcs.Contains(enclosingProc)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - foreach (CallCmd callCmd in node.CallCmds) - { - if (!yieldingProcs.Contains(callCmd.Proc)) - { - yieldingProcs.Add(callCmd.Proc); - moreProcessingRequired = true; - } - } - return ret; - } - private void ProcessVariable(Variable var) { - Procedure/*!*/ localProc = cce.NonNull(enclosingProc); - if (var == null) - return; - if (!(var is GlobalVariable)) - return; - if (!modSets.ContainsKey(localProc)) { - modSets[localProc] = new HashSet(); - } - if (modSets[localProc].Contains(var)) - return; - moreProcessingRequired = true; - modSets[localProc].Add(var); - } - public override Expr VisitCodeExpr(CodeExpr node) { - // don't go into the code expression, since it can only modify variables local to the code expression, - // and the mod-set analysis is interested in global variables - return node; - } - } - - public class MutableVariableCollector : ReadOnlyVisitor - { - public HashSet UsedVariables = new HashSet(); - - public void AddUsedVariables(HashSet usedVariables) - { - Contract.Requires(usedVariables != null); - - foreach (var v in usedVariables) - { - UsedVariables.Add(v); - } - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - Contract.Ensures(Contract.Result() != null); - - if (node.Decl != null && node.Decl.IsMutable) - { - UsedVariables.Add(node.Decl); - } - return base.VisitIdentifierExpr(node); - } - } - - public class VariableCollector : ReadOnlyVisitor { - protected HashSet/*!*/ _usedVars; - public IEnumerable/*!*/ usedVars - { - get - { - return _usedVars.AsEnumerable(); - } - } - - protected HashSet/*!*/ _oldVarsUsed; - public IEnumerable/*!*/ oldVarsUsed - { - get - { - return _oldVarsUsed.AsEnumerable(); - } - } - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(_usedVars)); - Contract.Invariant(cce.NonNullElements(_oldVarsUsed)); - } - - int insideOldExpr; - - public VariableCollector() { - _usedVars = new System.Collections.Generic.HashSet(); - _oldVarsUsed = new System.Collections.Generic.HashSet(); - insideOldExpr = 0; - } - - public override Expr VisitOldExpr(OldExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - insideOldExpr++; - node.Expr = this.VisitExpr(node.Expr); - insideOldExpr--; - return node; - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - if (node.Decl != null) { - _usedVars.Add(node.Decl); - if (insideOldExpr > 0) { - _oldVarsUsed.Add(node.Decl); - } - } - return node; - } - } - - public class BlockCoalescer : ReadOnlyVisitor { - public static void CoalesceBlocks(Program program) { - Contract.Requires(program != null); - BlockCoalescer blockCoalescer = new BlockCoalescer(); - blockCoalescer.Visit(program); - } - - private static HashSet/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - HashSet visitedBlocks = new HashSet(); - HashSet multiPredBlocks = new HashSet(); - Stack dfsStack = new Stack(); - dfsStack.Push(impl.Blocks[0]); - while (dfsStack.Count > 0) { - Block/*!*/ b = dfsStack.Pop(); - Contract.Assert(b != null); - if (visitedBlocks.Contains(b)) { - multiPredBlocks.Add(b); - continue; - } - visitedBlocks.Add(b); - if (b.TransferCmd == null) - continue; - if (b.TransferCmd is ReturnCmd) - continue; - Contract.Assert(b.TransferCmd is GotoCmd); - GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; - if (gotoCmd.labelTargets == null) - continue; - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - dfsStack.Push(succ); - } - } - return multiPredBlocks; - } - - public override Implementation VisitImplementation(Implementation impl) { - //Contract.Requires(impl != null); - Contract.Ensures(Contract.Result() != null); - //Console.WriteLine("Procedure {0}", impl.Name); - //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count); - - HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl); - Contract.Assert(cce.NonNullElements(multiPredBlocks)); - HashSet visitedBlocks = new HashSet(); - HashSet removedBlocks = new HashSet(); - Stack dfsStack = new Stack(); - dfsStack.Push(impl.Blocks[0]); - while (dfsStack.Count > 0) { - Block/*!*/ b = dfsStack.Pop(); - Contract.Assert(b != null); - if (visitedBlocks.Contains(b)) - continue; - visitedBlocks.Add(b); - if (b.TransferCmd == null) - continue; - if (b.TransferCmd is ReturnCmd) - continue; - Contract.Assert(b.TransferCmd is GotoCmd); - GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; - if (gotoCmd.labelTargets == null) - continue; - if (gotoCmd.labelTargets.Count == 1) { - Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]); - if (!multiPredBlocks.Contains(succ)) { - foreach (Cmd/*!*/ cmd in succ.Cmds) { - Contract.Assert(cmd != null); - b.Cmds.Add(cmd); - } - b.TransferCmd = succ.TransferCmd; - if (!b.tok.IsValid && succ.tok.IsValid) { - b.tok = succ.tok; - b.Label = succ.Label; - } - removedBlocks.Add(succ); - dfsStack.Push(b); - visitedBlocks.Remove(b); - continue; - } - } - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - dfsStack.Push(succ); - } - } - - List newBlocks = new List(); - foreach (Block/*!*/ b in impl.Blocks) { - Contract.Assert(b != null); - if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b)) { - newBlocks.Add(b); - } - } - impl.Blocks = newBlocks; - - // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count); - return impl; - } - } - - public class LiveVariableAnalysis { - public static void ClearLiveVariables(Implementation impl) { - Contract.Requires(impl != null); - foreach (Block/*!*/ block in impl.Blocks) { - Contract.Assert(block != null); - block.liveVarsBefore = null; - } - } - - public static void ComputeLiveVariables(Implementation impl) { - Contract.Requires(impl != null); - Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis"); - Graph dag = new Graph(); - dag.AddSource(cce.NonNull(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) { - Contract.Assume(gtc.labelTargets != null); - foreach (Block/*!*/ dest in gtc.labelTargets) { - Contract.Assert(dest != null); - dag.AddEdge(dest, b); - } - } - } - - IEnumerable sortedNodes; - if (CommandLineOptions.Clo.ModifyTopologicalSorting) { - sortedNodes = dag.TopologicalSort(true); - } else { - sortedNodes = dag.TopologicalSort(); - } - foreach (Block/*!*/ block in sortedNodes) { - Contract.Assert(block != null); - HashSet/*!*/ liveVarsAfter = new HashSet(); - - // The injected assumption variables should always be considered to be live. - foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables)) - { - liveVarsAfter.Add(v); - } - - if (block.TransferCmd is GotoCmd) { - GotoCmd gotoCmd = (GotoCmd)block.TransferCmd; - if (gotoCmd.labelTargets != null) { - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - Contract.Assert(succ.liveVarsBefore != null); - liveVarsAfter.UnionWith(succ.liveVarsBefore); - } - } - } - - List cmds = block.Cmds; - int len = cmds.Count; - for (int i = len - 1; i >= 0; i--) { - if (cmds[i] is CallCmd) { - Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc); - if (InterProcGenKill.HasSummary(proc.Name)) { - liveVarsAfter = - InterProcGenKill.PropagateLiveVarsAcrossCall(cce.NonNull((CallCmd/*!*/)cmds[i]), liveVarsAfter); - continue; - } - } - Propagate(cmds[i], liveVarsAfter); - } - - block.liveVarsBefore = liveVarsAfter; - - } - } - - // perform in place update of liveSet - public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet) { - Contract.Requires(cmd != null); - Contract.Requires(cce.NonNullElements(liveSet)); - if (cmd is AssignCmd) { - AssignCmd/*!*/ assignCmd = (AssignCmd)cce.NonNull(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 - - AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd; - HashSet indexSet = new HashSet(); - int index = 0; - foreach (AssignLhs/*!*/ lhs in simpleAssignCmd.Lhss) { - Contract.Assert(lhs != null); - SimpleAssignLhs salhs = lhs as SimpleAssignLhs; - Contract.Assert(salhs != null); - Variable var = salhs.DeepAssignedVariable; - if (var != null && liveSet.Contains(var)) { - indexSet.Add(index); - liveSet.Remove(var); - } - index++; - } - index = 0; - foreach (Expr/*!*/ expr in simpleAssignCmd.Rhss) { - Contract.Assert(expr != null); - if (indexSet.Contains(index)) { - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - liveSet.UnionWith(collector.usedVars); - } - index++; - } - } else if (cmd is HavocCmd) { - HavocCmd/*!*/ havocCmd = (HavocCmd)cmd; - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { - liveSet.Remove(expr.Decl); - } - } - } else if (cmd is PredicateCmd) { - Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); - PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(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.UnionWith(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)cce.NonNull(cmd); - Propagate(sugCmd.Desugaring, liveSet); - } else if (cmd is StateCmd) { - StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd); - List/*!*/ cmds = cce.NonNull(stCmd.Cmds); - int len = cmds.Count; - for (int i = len - 1; i >= 0; i--) { - Propagate(cmds[i], liveSet); - } - foreach (Variable/*!*/ v in stCmd.Locals) { - Contract.Assert(v != null); - liveSet.Remove(v); - } - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - } - } - - /* - // An idempotent semiring interface - abstract public class Weight { - abstract public Weight! one(); - abstract public Weight! zero(); - abstract public Weight! extend(Weight! w1, Weight! w2); - abstract public Weight! combine(Weight! w1, Weight! w2); - abstract public Weight! isEqual(Weight! w); - abstract public Weight! projectLocals() - } - */ - - // Weight domain for LiveVariableAnalysis (Gen/Kill) - - public class GenKillWeight { - // lambda S. (S - kill) union gen - HashSet/*!*/ gen; - HashSet/*!*/ kill; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(gen)); - Contract.Invariant(cce.NonNullElements(kill)); - Contract.Invariant(oneWeight != null); - Contract.Invariant(zeroWeight != null); - } - - bool isZero; - - public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet(), new HashSet()); - public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight(); - - // initializes to zero - public GenKillWeight() { - this.isZero = true; - this.gen = new HashSet(); - this.kill = new HashSet(); - } - - public GenKillWeight(HashSet gen, HashSet kill) { - Contract.Requires(cce.NonNullElements(gen)); - Contract.Requires(cce.NonNullElements(kill)); - Contract.Assert(gen != null); - Contract.Assert(kill != null); - this.gen = gen; - this.kill = kill; - this.isZero = false; - } - - public static GenKillWeight one() { - Contract.Ensures(Contract.Result() != null); - return oneWeight; - } - - public static GenKillWeight zero() { - Contract.Ensures(Contract.Result() != null); - return zeroWeight; - } - - public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - Contract.Ensures(Contract.Result() != null); - if (w1.isZero || w2.isZero) - return zero(); - - HashSet t = new HashSet(w2.gen); - t.ExceptWith(w1.kill); - HashSet g = new HashSet(w1.gen); - g.UnionWith(t); - HashSet k = new HashSet(w1.kill); - k.UnionWith(w2.kill); - return new GenKillWeight(g, k); - //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill)); - } - - public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - Contract.Ensures(Contract.Result() != null); - if (w1.isZero) - return w2; - if (w2.isZero) - return w1; - - HashSet g = new HashSet(w1.gen); - g.UnionWith(w2.gen); - HashSet k = new HashSet(w1.kill); - k.IntersectWith(w2.kill); - return new GenKillWeight(g, k); - //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill)); - } - - public static GenKillWeight projectLocals(GenKillWeight w) { - Contract.Requires(w != null); - Contract.Ensures(Contract.Result() != null); - HashSet gen = new HashSet(); - foreach (Variable v in w.gen) - { - if (isGlobal(v)) - gen.Add(v); - } - HashSet kill = new HashSet(); - foreach (Variable v in w.kill) - { - if (isGlobal(v)) - kill.Add(v); - } - - return new GenKillWeight(gen, kill); - } - - public static bool isEqual(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - if (w1.isZero) - return w2.isZero; - if (w2.isZero) - return w1.isZero; - - return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill)); - } - - private static bool isGlobal(Variable v) { - Contract.Requires(v != null); - return (v is GlobalVariable); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return string.Format("({0},{1})", gen.ToString(), kill.ToString()); - } - - public HashSet/*!*/ getLiveVars() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return gen; - } - - public HashSet/*!*/ getLiveVars(HashSet/*!*/ lv) { - Contract.Requires(cce.NonNullElements(lv)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - HashSet temp = new HashSet(lv); - temp.ExceptWith(kill); - temp.UnionWith(gen); - return temp; - } - - } - - public class ICFG { - public Graph/*!*/ graph; - // Map from procedure to the list of blocks that call that procedure - public Dictionary/*!*/>/*!*/ procsCalled; - public HashSet/*!*/ nodes; - public Dictionary/*!*/>/*!*/ succEdges; - public Dictionary/*!*/>/*!*/ predEdges; - private Dictionary/*!*/ priority; - - public HashSet/*!*/ srcNodes; - public HashSet/*!*/ exitNodes; - - public Dictionary/*!*/ weightBefore; - public Dictionary/*!*/ weightAfter; - public Dictionary/*!*/>/*!*/ liveVarsAfter; - public Dictionary/*!*/>/*!*/ liveVarsBefore; - - public GenKillWeight/*!*/ summary; - public Implementation/*!*/ impl; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(graph.Nodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled)); - Contract.Invariant(cce.NonNullElements(nodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges)); - Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges)); - Contract.Invariant(priority != null); - Contract.Invariant(cce.NonNullElements(srcNodes)); - Contract.Invariant(cce.NonNullElements(exitNodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter)); - Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter)); - Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore)); - Contract.Invariant(summary != null); - Contract.Invariant(impl != null); - } - - - [NotDelayed] - public ICFG(Implementation impl) { - Contract.Requires(impl != null); - this.graph = new Graph(); - this.procsCalled = new Dictionary/*!*/>(); - this.nodes = new HashSet(); - this.succEdges = new Dictionary/*!*/>(); - this.predEdges = new Dictionary/*!*/>(); - - this.priority = new Dictionary(); - - this.srcNodes = new HashSet(); - this.exitNodes = new HashSet(); - - this.weightBefore = new Dictionary(); - this.weightAfter = new Dictionary(); - this.liveVarsAfter = new Dictionary/*!*/>(); - this.liveVarsBefore = new Dictionary/*!*/>(); - - summary = GenKillWeight.zero(); - this.impl = impl; - - Initialize(impl); - - } - - private void Initialize(Implementation impl) { - Contract.Requires(impl != null); - addSource(impl.Blocks[0]); - graph.AddSource(impl.Blocks[0]); - - foreach (Block/*!*/ b in impl.Blocks) { - Contract.Assert(b != null); - if (b.TransferCmd is ReturnCmd) { - exitNodes.Add(b); - } else { - GotoCmd gc = b.TransferCmd as GotoCmd; - Contract.Assert(gc != null); - Contract.Assert(gc.labelTargets != null); - foreach (Block/*!*/ t in gc.labelTargets) { - Contract.Assert(t != null); - addEdge(b, t); - graph.AddEdge(b, t); - } - } - - weightBefore[b] = GenKillWeight.zero(); - weightAfter[b] = GenKillWeight.zero(); - - foreach (Cmd/*!*/ c in b.Cmds) { - Contract.Assert(c != null); - if (c is CallCmd) { - CallCmd/*!*/ cc = cce.NonNull((CallCmd/*!*/)c); - Contract.Assert(cc.Proc != null); - string/*!*/ procName = cc.Proc.Name; - Contract.Assert(procName != null); - if (!procsCalled.ContainsKey(procName)) { - procsCalled.Add(procName, new List()); - } - procsCalled[procName].Add(b); - } - } - } - - List/*!*/ sortedNodes; - bool acyclic; - - graph.TarjanTopSort(out acyclic, out sortedNodes); - - if (!acyclic) { - Console.WriteLine("Warning: graph is not a dag"); - } - - int num = sortedNodes.Count; - foreach (Block/*!*/ b in sortedNodes) { - Contract.Assert(b != null); - priority.Add(b, num); - num--; - } - - } - - public int getPriority(Block b) { - Contract.Requires(b != null); - if (priority.ContainsKey(b)) - return priority[b]; - return Int32.MaxValue; - } - - private void addSource(Block b) { - Contract.Requires(b != null); - registerNode(b); - this.srcNodes.Add(b); - } - - private void addExit(Block b) { - Contract.Requires(b != null); - registerNode(b); - this.exitNodes.Add(b); - } - - private void registerNode(Block b) { - Contract.Requires(b != null); - if (!succEdges.ContainsKey(b)) { - succEdges.Add(b, new HashSet()); - } - - if (!predEdges.ContainsKey(b)) { - predEdges.Add(b, new HashSet()); - } - - nodes.Add(b); - } - - private void addEdge(Block src, Block tgt) { - Contract.Requires(tgt != null); - Contract.Requires(src != null); - registerNode(src); - registerNode(tgt); - - succEdges[src].Add(tgt); - predEdges[tgt].Add(src); - } - - - } - - // Interprocedural Gen/Kill Analysis - public class InterProcGenKill { - Program/*!*/ program; - Dictionary/*!*/ procICFG; - Dictionary/*!*/ name2Proc; - Dictionary/*!*/>/*!*/ callers; - Graph/*!*/ callGraph; - Dictionary/*!*/ procPriority; - int maxBlocksInProc; - - WorkList/*!*/ workList; - - Implementation/*!*/ mainImpl; - - static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); - static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); - static Dictionary/*!*/ varsLiveSummary = new Dictionary(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(workList != null); - Contract.Invariant(mainImpl != null); - Contract.Invariant(program != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(procICFG)); - Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc)); - Contract.Invariant(cce.NonNullDictionaryAndValues(callers) && - Contract.ForAll(callers.Values, v => cce.NonNullElements(v))); - Contract.Invariant(cce.NonNullElements(callGraph.Nodes)); - Contract.Invariant(procPriority != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry)); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) && - Contract.ForAll(varsLiveAtExit.Values, v => cce.NonNullElements(v))); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveSummary)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheAfterCall)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheBeforeCall)); - } - - - [NotDelayed] - public InterProcGenKill(Implementation impl, Program program) { - Contract.Requires(program != null); - Contract.Requires(impl != null); - this.program = program; - procICFG = new Dictionary(); - name2Proc = new Dictionary(); - workList = new WorkList(); - this.callers = new Dictionary/*!*/>(); - this.callGraph = new Graph(); - this.procPriority = new Dictionary(); - this.maxBlocksInProc = 0; - this.mainImpl = impl; - - Dictionary/*!*/ name2Impl = new Dictionary(); - varsLiveAtExit.Clear(); - varsLiveAtEntry.Clear(); - varsLiveSummary.Clear(); - - foreach (var decl in program.TopLevelDeclarations) { - Contract.Assert(decl != null); - if (decl is Implementation) { - Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl); - name2Impl[imp.Name] = imp; - } else if (decl is Procedure) { - Procedure/*!*/ proc = cce.NonNull(decl as Procedure); - name2Proc[proc.Name] = proc; - } - } - - ICFG/*!*/ mainICFG = new ICFG(mainImpl); - Contract.Assert(mainICFG != null); - procICFG.Add(mainICFG.impl.Name, mainICFG); - callGraph.AddSource(mainICFG.impl.Name); - - List/*!*/ procsToConsider = new List(); - procsToConsider.Add(mainICFG); - - while (procsToConsider.Count != 0) { - ICFG/*!*/ p = procsToConsider[0]; - Contract.Assert(p != null); - procsToConsider.RemoveAt(0); - - foreach (string/*!*/ callee in p.procsCalled.Keys) { - Contract.Assert(callee != null); - if (!name2Impl.ContainsKey(callee)) - continue; - - callGraph.AddEdge(p.impl.Name, callee); - - if (maxBlocksInProc < p.nodes.Count) { - maxBlocksInProc = p.nodes.Count; - } - - if (!callers.ContainsKey(callee)) { - callers.Add(callee, new List()); - } - foreach (Block/*!*/ b in p.procsCalled[callee]) { - Contract.Assert(b != null); - callers[callee].Add(new WorkItem(p, b)); - } - - if (procICFG.ContainsKey(callee)) - continue; - ICFG/*!*/ ncfg = new ICFG(name2Impl[callee]); - Contract.Assert(ncfg != null); - procICFG.Add(callee, ncfg); - procsToConsider.Add(ncfg); - } - } - - bool acyclic; - List/*!*/ sortedNodes; - callGraph.TarjanTopSort(out acyclic, out sortedNodes); - - Contract.Assert(acyclic); - - int cnt = 0; - for (int i = sortedNodes.Count - 1; i >= 0; i--) { - string s = sortedNodes[i]; - if (s == null) - continue; - procPriority.Add(s, cnt); - cnt++; - } - - } - - public static HashSet/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (varsLiveAtExit.ContainsKey(impl.Name)) { - return varsLiveAtExit[impl.Name]; - } - // Return default: all globals and out params - HashSet/*!*/ lv = new HashSet(); - foreach (Variable/*!*/ v in prog.GlobalVariables) { - Contract.Assert(v != null); - lv.Add(v); - } - foreach (Variable/*!*/ v in impl.OutParams) { - Contract.Assert(v != null); - lv.Add(v); - } - return lv; - } - - public static HashSet/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (varsLiveAtEntry.ContainsKey(impl.Name)) { - return varsLiveAtEntry[impl.Name]; - } - // Return default: all globals and in params - HashSet/*!*/ lv = new HashSet(); - foreach (Variable/*!*/ v in prog.GlobalVariables) { - Contract.Assert(v != null); - lv.Add(v); - } - foreach (Variable/*!*/ v in impl.InParams) { - Contract.Assert(v != null); - lv.Add(v); - } - return lv; - } - - public static bool HasSummary(string name) { - Contract.Requires(name != null); - return varsLiveSummary.ContainsKey(name); - } - - public static HashSet/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet/*!*/ lvAfter) { - Contract.Requires(cmd != null); - Contract.Requires(cce.NonNullElements(lvAfter)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Procedure/*!*/ proc = cce.NonNull(cmd.Proc); - if (varsLiveSummary.ContainsKey(proc.Name)) { - GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); - Contract.Assert(w1 != null); - GenKillWeight/*!*/ w2 = varsLiveSummary[proc.Name]; - Contract.Assert(w2 != null); - GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); - Contract.Assert(w3 != null); - GenKillWeight/*!*/ w = GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); - Contract.Assert(w != null); - return w.getLiveVars(lvAfter); - } - HashSet/*!*/ ret = new HashSet(); - ret.UnionWith(lvAfter); - LiveVariableAnalysis.Propagate(cmd, ret); - return ret; - } - - class WorkItem { - public ICFG/*!*/ cfg; - public Block/*!*/ block; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cfg != null); - Contract.Invariant(block != null); - } - - - public WorkItem(ICFG cfg, Block block) { - Contract.Requires(block != null); - Contract.Requires(cfg != null); - this.cfg = cfg; - this.block = block; - } - - public GenKillWeight getWeightAfter() { - Contract.Ensures(Contract.Result() != null); - return cfg.weightAfter[block]; - } - - public bool setWeightBefore(GenKillWeight w) { - Contract.Requires(w != null); - GenKillWeight/*!*/ prev = cfg.weightBefore[block]; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(w, prev); - Contract.Assert(curr != null); - if (GenKillWeight.isEqual(prev, curr)) - return false; - cfg.weightBefore[block] = curr; - return true; - } - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object other) { - WorkItem/*!*/ wi = (WorkItem/*!*/)cce.NonNull(other); - return (wi.cfg == cfg && wi.block == block); - } - - [Pure] - public override int GetHashCode() { - return 0; - } - - public string getLabel() { - Contract.Ensures(Contract.Result() != null); - return cfg.impl.Name + "::" + block.Label; - } - - } - - private void AddToWorkList(WorkItem wi) { - Contract.Requires(wi != null); - int i = procPriority[wi.cfg.impl.Name]; - int j = wi.cfg.getPriority(wi.block); - int priority = (i * maxBlocksInProc) + j; - - workList.Add(wi, priority); - } - - private void AddToWorkListReverse(WorkItem wi) { - Contract.Requires(wi != null); - int i = procPriority[wi.cfg.impl.Name]; - int j = wi.cfg.getPriority(wi.block); - int priority = (procPriority.Count - i) * maxBlocksInProc + j; - workList.Add(wi, priority); - } - - class WorkList { - SortedList/*!*/ priorities; - HashSet/*!*/ labels; - - Dictionary/*!*/>/*!*/ workList; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(priorities != null); - Contract.Invariant(cce.NonNullElements(labels)); - Contract.Invariant(cce.NonNullDictionaryAndValues(workList) && - Contract.ForAll(workList.Values, v => cce.NonNullElements(v))); - } - - - public WorkList() { - labels = new HashSet(); - priorities = new SortedList(); - workList = new Dictionary/*!*/>(); - } - - public void Add(WorkItem wi, int priority) { - Contract.Requires(wi != null); - string/*!*/ lab = wi.getLabel(); - Contract.Assert(lab != null); - if (labels.Contains(lab)) { - // Already on worklist - return; - } - labels.Add(lab); - if (!workList.ContainsKey(priority)) { - workList.Add(priority, new List()); - } - workList[priority].Add(wi); - if (!priorities.ContainsKey(priority)) { - priorities.Add(priority, 0); - } - - priorities[priority] = priorities[priority] + 1; - } - - public WorkItem Get() { - Contract.Ensures(Contract.Result() != null); - // Get minimum priority - int p = cce.NonNull(priorities.Keys)[0]; - priorities[p] = priorities[p] - 1; - if (priorities[p] == 0) { - priorities.Remove(p); - } - - // Get a WI with this priority - WorkItem/*!*/ wi = workList[p][0]; - Contract.Assert(wi != null); - workList[p].RemoveAt(0); - - // update labels - labels.Remove(wi.getLabel()); - return wi; - } - - public int Count { - get { - return labels.Count; - } - } - } - - private GenKillWeight getSummary(CallCmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert(cmd.Proc != null); - string/*!*/ procName = cmd.Proc.Name; - Contract.Assert(procName != null); - if (procICFG.ContainsKey(procName)) { - ICFG/*!*/ cfg = procICFG[procName]; - Contract.Assert(cfg != null); - return GenKillWeight.projectLocals(cfg.summary); - } - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - - public static void ComputeLiveVars(Implementation impl, Program/*!*/ prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - InterProcGenKill/*!*/ ipgk = new InterProcGenKill(impl, prog); - Contract.Assert(ipgk != null); - ipgk.Compute(); - } - - public void Compute() { - // Put all exit nodes in the worklist - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - foreach (Block/*!*/ eb in cfg.exitNodes) { - Contract.Assert(eb != null); - WorkItem/*!*/ wi = new WorkItem(cfg, eb); - Contract.Assert(wi != null); - cfg.weightAfter[eb] = GenKillWeight.one(); - AddToWorkList(wi); - } - } - - while (workList.Count != 0) { - WorkItem/*!*/ wi = workList.Get(); - Contract.Assert(wi != null); - process(wi); - } - - // Propagate LV to all procedures - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - foreach (Block/*!*/ b in cfg.nodes) { - Contract.Assert(b != null); - cfg.liveVarsAfter.Add(b, new HashSet()); - cfg.liveVarsBefore.Add(b, new HashSet()); - } - } - - ICFG/*!*/ mainCfg = procICFG[mainImpl.Name]; - Contract.Assert(mainCfg != null); - foreach (Block/*!*/ eb in mainCfg.exitNodes) { - Contract.Assert(eb != null); - WorkItem/*!*/ wi = new WorkItem(mainCfg, eb); - Contract.Assert(wi != null); - AddToWorkListReverse(wi); - } - - while (workList.Count != 0) { - WorkItem/*!*/ wi = workList.Get(); - Contract.Assert(wi != null); - processLV(wi); - } - - // Set live variable info - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - HashSet/*!*/ lv = new HashSet(); - foreach (Block/*!*/ eb in cfg.exitNodes) { - Contract.Assert(eb != null); - lv.UnionWith(cfg.liveVarsAfter[eb]); - } - varsLiveAtExit.Add(cfg.impl.Name, lv); - lv = new HashSet(); - foreach (Block/*!*/ eb in cfg.srcNodes) { - Contract.Assert(eb != null); - lv.UnionWith(cfg.liveVarsBefore[eb]); - } - varsLiveAtEntry.Add(cfg.impl.Name, lv); - varsLiveSummary.Add(cfg.impl.Name, cfg.summary); - } - - /* - foreach(Block/*!*/ - /* b in mainImpl.Blocks){ -Contract.Assert(b != null); -//Set lv = cfg.weightBefore[b].getLiveVars(); -b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; -//foreach(GlobalVariable/*!*/ - /* v in program.GlobalVariables){Contract.Assert(v != null); -// b.liveVarsBefore.Add(v); -//} -} -*/ - } - - // Called when summaries have already been computed - private void processLV(WorkItem wi) { - Contract.Requires(wi != null); - ICFG/*!*/ cfg = wi.cfg; - Contract.Assert(cfg != null); - Block/*!*/ block = wi.block; - Contract.Assert(block != null); - HashSet/*!*/ lv = cfg.liveVarsAfter[block]; - Contract.Assert(cce.NonNullElements(lv)); - // Propagate backwards in the block - HashSet/*!*/ prop = new HashSet(); - prop.UnionWith(lv); - for (int i = block.Cmds.Count - 1; i >= 0; i--) { - Cmd/*!*/ cmd = block.Cmds[i]; - Contract.Assert(cmd != null); - if (cmd is CallCmd) { - string/*!*/ procName = cce.NonNull(cce.NonNull((CallCmd)cmd).Proc).Name; - Contract.Assert(procName != null); - if (procICFG.ContainsKey(procName)) { - ICFG/*!*/ callee = procICFG[procName]; - Contract.Assert(callee != null); - // Inter propagation - // Remove local variables; add return variables - HashSet/*!*/ elv = new HashSet(); - foreach (Variable/*!*/ v in prop) { - Contract.Assert(v != null); - if (v is GlobalVariable) - elv.Add(v); - } - foreach (Variable/*!*/ v in callee.impl.OutParams) { - Contract.Assert(v != null); - elv.Add(v); - } - - foreach (Block/*!*/ eb in callee.exitNodes) { - Contract.Assert(eb != null); - callee.liveVarsAfter[eb].UnionWith(elv); - // TODO: check if modified before inserting - AddToWorkListReverse(new WorkItem(callee, eb)); - } - - // Continue with intra propagation - GenKillWeight/*!*/ summary = getWeightCall(cce.NonNull((CallCmd/*!*/)cmd)); - prop = summary.getLiveVars(prop); - } else { - LiveVariableAnalysis.Propagate(cmd, prop); - } - } else { - LiveVariableAnalysis.Propagate(cmd, prop); - } - } - - cfg.liveVarsBefore[block].UnionWith(prop); - - foreach (Block/*!*/ b in cfg.predEdges[block]) { - Contract.Assert(b != null); - HashSet/*!*/ prev = cfg.liveVarsAfter[b]; - Contract.Assert(cce.NonNullElements(prev)); - HashSet/*!*/ curr = new HashSet(prev); - curr.UnionWith(cfg.liveVarsBefore[block]); - Contract.Assert(cce.NonNullElements(curr)); - if (curr.Count != prev.Count) { - cfg.liveVarsAfter[b] = curr; - AddToWorkListReverse(new WorkItem(cfg, b)); - } - } - } - - private void process(WorkItem wi) { - Contract.Requires(wi != null); - GenKillWeight/*!*/ w = wi.getWeightAfter(); - Contract.Assert(w != null); - - for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) { - Cmd/*!*/ c = wi.block.Cmds[i]; - Contract.Assert(c != null); - if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) { - w = GenKillWeight.extend(getWeightCall(cce.NonNull((CallCmd)c)), w); - } else { - GenKillWeight/*!*/ cweight = getWeight(c, wi.cfg.impl, program); - Contract.Assert(cweight != null); - w = GenKillWeight.extend(cweight, w); - } - } - - bool change = wi.setWeightBefore(w); - - if (change && wi.cfg.srcNodes.Contains(wi.block)) { - GenKillWeight/*!*/ prev = wi.cfg.summary; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, wi.cfg.weightBefore[wi.block]); - Contract.Assert(curr != null); - if (!GenKillWeight.isEqual(prev, curr)) { - wi.cfg.summary = curr; - // push callers onto the worklist - if (callers.ContainsKey(wi.cfg.impl.Name)) { - foreach (WorkItem/*!*/ caller in callers[wi.cfg.impl.Name]) { - Contract.Assert(caller != null); - AddToWorkList(caller); - } - } - } - } - - foreach (Block/*!*/ b in wi.cfg.predEdges[wi.block]) { - Contract.Assert(b != null); - GenKillWeight/*!*/ prev = wi.cfg.weightAfter[b]; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, w); - Contract.Assert(curr != null); - if (!GenKillWeight.isEqual(prev, curr)) { - wi.cfg.weightAfter[b] = curr; - AddToWorkList(new WorkItem(wi.cfg, b)); - } - } - - } - - static Dictionary/*!*/ weightCache = new Dictionary(); - - private static GenKillWeight getWeight(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - return getWeight(cmd, null, null); - } - - private GenKillWeight getWeightCall(CallCmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); - GenKillWeight/*!*/ w2 = getSummary(cmd); - GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); - Contract.Assert(w1 != null); - Contract.Assert(w2 != null); - Contract.Assert(w3 != null); - return GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); - } - - private static GenKillWeight getWeight(Cmd cmd, Implementation impl, Program prog) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - - if (weightCache.ContainsKey(cmd)) - return weightCache[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - GenKillWeight/*!*/ ret; - - if (cmd is AssignCmd) { - AssignCmd/*!*/ assignCmd = (AssignCmd)cmd; - Contract.Assert(cmd != null); - // 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 - foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { - Contract.Assert(lhs != null); - Variable var = lhs.DeepAssignedVariable; - if (var != null) { - 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 - kill.Add(var); - } - } - } - int index = 0; - foreach (Expr/*!*/ expr in assignCmd.Rhss) { - Contract.Assert(expr != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - gen.UnionWith(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); - gen.UnionWith(c.usedVars); - } - } - index++; - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is HavocCmd) { - HavocCmd/*!*/ havocCmd = (HavocCmd)cce.NonNull(cmd); - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - if (expr.Decl != null) { - kill.Add(expr.Decl); - } - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is PredicateCmd) { - Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); - PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); - if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) { - LiteralExpr le = (LiteralExpr)predicateCmd.Expr; - if (le.IsFalse) { - var globals = prog.GlobalVariables; - Contract.Assert(cce.NonNullElements(globals)); - foreach (Variable/*!*/ v in globals) { - Contract.Assert(v != null); - kill.Add(v); - } - foreach (Variable/*!*/ v in impl.LocVars) { - Contract.Assert(v != null); - kill.Add(v); - } - foreach (Variable/*!*/ v in impl.OutParams) { - Contract.Assert(v != null); - kill.Add(v); - } - } - } else { - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(predicateCmd.Expr); - gen.UnionWith(collector.usedVars); - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is CommentCmd) { - ret = new GenKillWeight(gen, kill); - // comments are just for debugging and don't affect verification - } else if (cmd is SugaredCmd) { - SugaredCmd/*!*/ sugCmd = (SugaredCmd)cmd; - Contract.Assert(sugCmd != null); - ret = getWeight(sugCmd.Desugaring, impl, prog); - } else if (cmd is StateCmd) { - StateCmd/*!*/ stCmd = (StateCmd)cmd; - Contract.Assert(stCmd != null); - List/*!*/ cmds = stCmd.Cmds; - Contract.Assert(cmds != null); - int len = cmds.Count; - ret = GenKillWeight.one(); - for (int i = len - 1; i >= 0; i--) { - GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog); - Contract.Assert(w != null); - ret = GenKillWeight.extend(w, ret); - } - foreach (Variable/*!*/ v in stCmd.Locals) { - Contract.Assert(v != null); - kill.Add(v); - } - ret = GenKillWeight.extend(new GenKillWeight(gen, kill), ret); - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - - weightCache[cmd] = ret; - return ret; - } - - static Dictionary/*!*/ weightCacheAfterCall = new Dictionary(); - static Dictionary/*!*/ weightCacheBeforeCall = new Dictionary(); - - private static GenKillWeight getWeightAfterCall(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - - if (weightCacheAfterCall.ContainsKey(cmd)) - return weightCacheAfterCall[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - - Contract.Assert(cmd is CallCmd); - CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd); - - foreach (IdentifierExpr/*!*/ ie in ccmd.Outs) { - Contract.Assert(ie != null); - if (ie.Decl != null) - kill.Add(ie.Decl); - } - - // Variables in ensures are considered as "read" - foreach (Ensures/*!*/ re in cce.NonNull(ccmd.Proc).Ensures) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.usedVars) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); - Contract.Assert(ret != null); - weightCacheAfterCall[cmd] = ret; - return ret; - } - - private static GenKillWeight getWeightBeforeCall(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert((cmd is CallCmd)); - if (weightCacheBeforeCall.ContainsKey(cmd)) - return weightCacheBeforeCall[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd); - - foreach (Expr/*!*/ expr in ccmd.Ins) { - Contract.Assert(expr != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - gen.UnionWith(collector.usedVars); - } - - Contract.Assert(ccmd.Proc != null); - - // Variables in requires are considered as "read" - foreach (Requires/*!*/ re in ccmd.Proc.Requires) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.usedVars) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - // Old variables in ensures are considered as "read" - foreach (Ensures/*!*/ re in ccmd.Proc.Ensures) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.oldVarsUsed) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); - Contract.Assert(ret != null); - weightCacheAfterCall[cmd] = ret; - return ret; - } - } - - public class TokenEliminator : ReadOnlyVisitor - { - public int TokenCount = 0; - public override Expr VisitExpr(Expr node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitExpr(node); - } - public override Variable VisitVariable(Variable node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitVariable(node); - } - public override Function VisitFunction(Function node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitFunction(node); - } - public override Implementation VisitImplementation(Implementation node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitImplementation(node); - } - public override Procedure VisitProcedure(Procedure node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitProcedure(node); - } - public override Axiom VisitAxiom(Axiom node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAxiom(node); - } - public override Cmd VisitAssignCmd(AssignCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAssignCmd(node); - } - public override Cmd VisitAssumeCmd(AssumeCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAssumeCmd(node); - } - public override Cmd VisitHavocCmd(HavocCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitHavocCmd(node); - } - public override Constant VisitConstant(Constant node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitConstant(node); - } - public override TransferCmd VisitTransferCmd(TransferCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitTransferCmd(node); - } - public override Block VisitBlock(Block node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitBlock(node); - } - } +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie.GraphUtil; +using System.Diagnostics.Contracts; + + +namespace Microsoft.Boogie { + public class UnusedVarEliminator : VariableCollector { + public static void Eliminate(Program program) { + Contract.Requires(program != null); + UnusedVarEliminator elim = new UnusedVarEliminator(); + elim.Visit(program); + } + + private UnusedVarEliminator() + : base() { + + } + + public override Implementation VisitImplementation(Implementation node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + //Console.WriteLine("Procedure {0}", node.Name); + Implementation/*!*/ impl = base.VisitImplementation(node); + Contract.Assert(impl != null); + //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length); + List/*!*/ vars = new List(); + foreach (Variable/*!*/ var in impl.LocVars) { + Contract.Assert(var != null); + if (_usedVars.Contains(var)) + vars.Add(var); + } + impl.LocVars = vars; + //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length); + //Console.WriteLine("---------------------------------"); + _usedVars.Clear(); + return impl; + } + } + + public class ModSetCollector : ReadOnlyVisitor { + private Procedure enclosingProc; + private Dictionary/*!*/>/*!*/ modSets; + private HashSet yieldingProcs; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); + Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v))); + } + + public ModSetCollector() { + modSets = new Dictionary/*!*/>(); + yieldingProcs = new HashSet(); + } + + private bool moreProcessingRequired; + + public void DoModSetAnalysis(Program program) { + Contract.Requires(program != null); + + if (CommandLineOptions.Clo.Trace) + { +// Console.WriteLine(); +// Console.WriteLine("Running modset analysis ..."); +// int procCount = 0; +// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) +// { +// Contract.Assert(decl != null); +// if (decl is Procedure) +// procCount++; +// } +// Console.WriteLine("Number of procedures = {0}", procCount);*/ + } + + HashSet implementedProcs = new HashSet(); + foreach (var impl in program.Implementations) { + if (impl.Proc != null) + implementedProcs.Add(impl.Proc); + } + foreach (var proc in program.Procedures) { + if (!implementedProcs.Contains(proc)) + { + enclosingProc = proc; + foreach (var expr in proc.Modifies) + { + Contract.Assert(expr != null); + ProcessVariable(expr.Decl); + } + enclosingProc = null; + } + else + { + modSets.Add(proc, new HashSet()); + } + } + + moreProcessingRequired = true; + while (moreProcessingRequired) { + moreProcessingRequired = false; + this.Visit(program); + } + + foreach (Procedure x in modSets.Keys) + { + x.Modifies = new List(); + foreach (Variable v in modSets[x]) + { + x.Modifies.Add(new IdentifierExpr(v.tok, v)); + } + } + foreach (Procedure x in yieldingProcs) + { + if (!QKeyValue.FindBoolAttribute(x.Attributes, "yields")) + { + x.AddAttribute("yields"); + } + } + +#if DEBUG_PRINT + Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); + foreach (Procedure/*!*/ x in modSets.Keys) { + Contract.Assert(x != null); + Console.Write("{0} : ", x.Name); + bool first = true; + foreach (Variable/*!*/ y in modSets[x]) { + Contract.Assert(y != null); + if (first) + first = false; + else + Console.Write(", "); + Console.Write("{0}", y.Name); + } + Console.WriteLine(""); + } +#endif + } + + public override Implementation VisitImplementation(Implementation node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + enclosingProc = node.Proc; + Implementation/*!*/ ret = base.VisitImplementation(node); + Contract.Assert(ret != null); + enclosingProc = null; + + return ret; + } + public override YieldCmd VisitYieldCmd(YieldCmd node) + { + if (!yieldingProcs.Contains(enclosingProc)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + return base.VisitYieldCmd(node); + } + public override Cmd VisitAssignCmd(AssignCmd assignCmd) { + //Contract.Requires(assignCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitAssignCmd(assignCmd); + foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { + Contract.Assert(lhs != null); + ProcessVariable(lhs.DeepAssignedVariable); + } + return ret; + } + public override Cmd VisitHavocCmd(HavocCmd havocCmd) { + //Contract.Requires(havocCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitHavocCmd(havocCmd); + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + ProcessVariable(expr.Decl); + } + return ret; + } + public override Cmd VisitCallCmd(CallCmd callCmd) { + //Contract.Requires(callCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitCallCmd(callCmd); + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (ie != null) ProcessVariable(ie.Decl); + } + Procedure callee = callCmd.Proc; + if (callee == null) + return ret; + if (modSets.ContainsKey(callee)) { + foreach (Variable var in modSets[callee]) { + ProcessVariable(var); + } + } + if (!yieldingProcs.Contains(enclosingProc) && (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + if (callCmd.IsAsync) + { + if (!yieldingProcs.Contains(callCmd.Proc)) + { + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; + } + } + return ret; + } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + //Contract.Requires(callCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitParCallCmd(node); + if (!yieldingProcs.Contains(enclosingProc)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + foreach (CallCmd callCmd in node.CallCmds) + { + if (!yieldingProcs.Contains(callCmd.Proc)) + { + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; + } + } + return ret; + } + private void ProcessVariable(Variable var) { + Procedure/*!*/ localProc = cce.NonNull(enclosingProc); + if (var == null) + return; + if (!(var is GlobalVariable)) + return; + if (!modSets.ContainsKey(localProc)) { + modSets[localProc] = new HashSet(); + } + if (modSets[localProc].Contains(var)) + return; + moreProcessingRequired = true; + modSets[localProc].Add(var); + } + public override Expr VisitCodeExpr(CodeExpr node) { + // don't go into the code expression, since it can only modify variables local to the code expression, + // and the mod-set analysis is interested in global variables + return node; + } + } + + public class MutableVariableCollector : ReadOnlyVisitor + { + public HashSet UsedVariables = new HashSet(); + + public void AddUsedVariables(HashSet usedVariables) + { + Contract.Requires(usedVariables != null); + + foreach (var v in usedVariables) + { + UsedVariables.Add(v); + } + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + Contract.Ensures(Contract.Result() != null); + + if (node.Decl != null && node.Decl.IsMutable) + { + UsedVariables.Add(node.Decl); + } + return base.VisitIdentifierExpr(node); + } + } + + public class VariableCollector : ReadOnlyVisitor { + protected HashSet/*!*/ _usedVars; + public IEnumerable/*!*/ usedVars + { + get + { + return _usedVars.AsEnumerable(); + } + } + + protected HashSet/*!*/ _oldVarsUsed; + public IEnumerable/*!*/ oldVarsUsed + { + get + { + return _oldVarsUsed.AsEnumerable(); + } + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(_usedVars)); + Contract.Invariant(cce.NonNullElements(_oldVarsUsed)); + } + + int insideOldExpr; + + public VariableCollector() { + _usedVars = new System.Collections.Generic.HashSet(); + _oldVarsUsed = new System.Collections.Generic.HashSet(); + insideOldExpr = 0; + } + + public override Expr VisitOldExpr(OldExpr node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + insideOldExpr++; + node.Expr = this.VisitExpr(node.Expr); + insideOldExpr--; + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + if (node.Decl != null) { + _usedVars.Add(node.Decl); + if (insideOldExpr > 0) { + _oldVarsUsed.Add(node.Decl); + } + } + return node; + } + } + + public class BlockCoalescer : ReadOnlyVisitor { + public static void CoalesceBlocks(Program program) { + Contract.Requires(program != null); + BlockCoalescer blockCoalescer = new BlockCoalescer(); + blockCoalescer.Visit(program); + } + + private static HashSet/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + HashSet visitedBlocks = new HashSet(); + HashSet multiPredBlocks = new HashSet(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block/*!*/ b = dfsStack.Pop(); + Contract.Assert(b != null); + if (visitedBlocks.Contains(b)) { + multiPredBlocks.Add(b); + continue; + } + visitedBlocks.Add(b); + if (b.TransferCmd == null) + continue; + if (b.TransferCmd is ReturnCmd) + continue; + Contract.Assert(b.TransferCmd is GotoCmd); + GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; + if (gotoCmd.labelTargets == null) + continue; + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + dfsStack.Push(succ); + } + } + return multiPredBlocks; + } + + public override Implementation VisitImplementation(Implementation impl) { + //Contract.Requires(impl != null); + Contract.Ensures(Contract.Result() != null); + //Console.WriteLine("Procedure {0}", impl.Name); + //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count); + + HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl); + Contract.Assert(cce.NonNullElements(multiPredBlocks)); + HashSet visitedBlocks = new HashSet(); + HashSet removedBlocks = new HashSet(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block/*!*/ b = dfsStack.Pop(); + Contract.Assert(b != null); + if (visitedBlocks.Contains(b)) + continue; + visitedBlocks.Add(b); + if (b.TransferCmd == null) + continue; + if (b.TransferCmd is ReturnCmd) + continue; + Contract.Assert(b.TransferCmd is GotoCmd); + GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; + if (gotoCmd.labelTargets == null) + continue; + if (gotoCmd.labelTargets.Count == 1) { + Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]); + if (!multiPredBlocks.Contains(succ)) { + foreach (Cmd/*!*/ cmd in succ.Cmds) { + Contract.Assert(cmd != null); + b.Cmds.Add(cmd); + } + b.TransferCmd = succ.TransferCmd; + if (!b.tok.IsValid && succ.tok.IsValid) { + b.tok = succ.tok; + b.Label = succ.Label; + } + removedBlocks.Add(succ); + dfsStack.Push(b); + visitedBlocks.Remove(b); + continue; + } + } + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + dfsStack.Push(succ); + } + } + + List newBlocks = new List(); + foreach (Block/*!*/ b in impl.Blocks) { + Contract.Assert(b != null); + if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b)) { + newBlocks.Add(b); + } + } + impl.Blocks = newBlocks; + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd) continue; + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + gotoCmd.labelNames = new List(); + foreach (Block succ in gotoCmd.labelTargets) + { + gotoCmd.labelNames.Add(succ.Label); + } + } + // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count); + return impl; + } + } + + public class LiveVariableAnalysis { + public static void ClearLiveVariables(Implementation impl) { + Contract.Requires(impl != null); + foreach (Block/*!*/ block in impl.Blocks) { + Contract.Assert(block != null); + block.liveVarsBefore = null; + } + } + + public static void ComputeLiveVariables(Implementation impl) { + Contract.Requires(impl != null); + Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis"); + Graph dag = new Graph(); + dag.AddSource(cce.NonNull(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) { + Contract.Assume(gtc.labelTargets != null); + foreach (Block/*!*/ dest in gtc.labelTargets) { + Contract.Assert(dest != null); + dag.AddEdge(dest, b); + } + } + } + + IEnumerable sortedNodes; + if (CommandLineOptions.Clo.ModifyTopologicalSorting) { + sortedNodes = dag.TopologicalSort(true); + } else { + sortedNodes = dag.TopologicalSort(); + } + foreach (Block/*!*/ block in sortedNodes) { + Contract.Assert(block != null); + HashSet/*!*/ liveVarsAfter = new HashSet(); + + // The injected assumption variables should always be considered to be live. + foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables)) + { + liveVarsAfter.Add(v); + } + + if (block.TransferCmd is GotoCmd) { + GotoCmd gotoCmd = (GotoCmd)block.TransferCmd; + if (gotoCmd.labelTargets != null) { + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + Contract.Assert(succ.liveVarsBefore != null); + liveVarsAfter.UnionWith(succ.liveVarsBefore); + } + } + } + + List cmds = block.Cmds; + int len = cmds.Count; + for (int i = len - 1; i >= 0; i--) { + if (cmds[i] is CallCmd) { + Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc); + if (InterProcGenKill.HasSummary(proc.Name)) { + liveVarsAfter = + InterProcGenKill.PropagateLiveVarsAcrossCall(cce.NonNull((CallCmd/*!*/)cmds[i]), liveVarsAfter); + continue; + } + } + Propagate(cmds[i], liveVarsAfter); + } + + block.liveVarsBefore = liveVarsAfter; + + } + } + + // perform in place update of liveSet + public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet) { + Contract.Requires(cmd != null); + Contract.Requires(cce.NonNullElements(liveSet)); + if (cmd is AssignCmd) { + AssignCmd/*!*/ assignCmd = (AssignCmd)cce.NonNull(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 + + AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd; + HashSet indexSet = new HashSet(); + int index = 0; + foreach (AssignLhs/*!*/ lhs in simpleAssignCmd.Lhss) { + Contract.Assert(lhs != null); + SimpleAssignLhs salhs = lhs as SimpleAssignLhs; + Contract.Assert(salhs != null); + Variable var = salhs.DeepAssignedVariable; + if (var != null && liveSet.Contains(var)) { + indexSet.Add(index); + liveSet.Remove(var); + } + index++; + } + index = 0; + foreach (Expr/*!*/ expr in simpleAssignCmd.Rhss) { + Contract.Assert(expr != null); + if (indexSet.Contains(index)) { + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + liveSet.UnionWith(collector.usedVars); + } + index++; + } + } else if (cmd is HavocCmd) { + HavocCmd/*!*/ havocCmd = (HavocCmd)cmd; + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { + liveSet.Remove(expr.Decl); + } + } + } else if (cmd is PredicateCmd) { + Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); + PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(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.UnionWith(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)cce.NonNull(cmd); + Propagate(sugCmd.Desugaring, liveSet); + } else if (cmd is StateCmd) { + StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd); + List/*!*/ cmds = cce.NonNull(stCmd.Cmds); + int len = cmds.Count; + for (int i = len - 1; i >= 0; i--) { + Propagate(cmds[i], liveSet); + } + foreach (Variable/*!*/ v in stCmd.Locals) { + Contract.Assert(v != null); + liveSet.Remove(v); + } + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + } + } + + /* + // An idempotent semiring interface + abstract public class Weight { + abstract public Weight! one(); + abstract public Weight! zero(); + abstract public Weight! extend(Weight! w1, Weight! w2); + abstract public Weight! combine(Weight! w1, Weight! w2); + abstract public Weight! isEqual(Weight! w); + abstract public Weight! projectLocals() + } + */ + + // Weight domain for LiveVariableAnalysis (Gen/Kill) + + public class GenKillWeight { + // lambda S. (S - kill) union gen + HashSet/*!*/ gen; + HashSet/*!*/ kill; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(gen)); + Contract.Invariant(cce.NonNullElements(kill)); + Contract.Invariant(oneWeight != null); + Contract.Invariant(zeroWeight != null); + } + + bool isZero; + + public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet(), new HashSet()); + public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight(); + + // initializes to zero + public GenKillWeight() { + this.isZero = true; + this.gen = new HashSet(); + this.kill = new HashSet(); + } + + public GenKillWeight(HashSet gen, HashSet kill) { + Contract.Requires(cce.NonNullElements(gen)); + Contract.Requires(cce.NonNullElements(kill)); + Contract.Assert(gen != null); + Contract.Assert(kill != null); + this.gen = gen; + this.kill = kill; + this.isZero = false; + } + + public static GenKillWeight one() { + Contract.Ensures(Contract.Result() != null); + return oneWeight; + } + + public static GenKillWeight zero() { + Contract.Ensures(Contract.Result() != null); + return zeroWeight; + } + + public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + Contract.Ensures(Contract.Result() != null); + if (w1.isZero || w2.isZero) + return zero(); + + HashSet t = new HashSet(w2.gen); + t.ExceptWith(w1.kill); + HashSet g = new HashSet(w1.gen); + g.UnionWith(t); + HashSet k = new HashSet(w1.kill); + k.UnionWith(w2.kill); + return new GenKillWeight(g, k); + //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill)); + } + + public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + Contract.Ensures(Contract.Result() != null); + if (w1.isZero) + return w2; + if (w2.isZero) + return w1; + + HashSet g = new HashSet(w1.gen); + g.UnionWith(w2.gen); + HashSet k = new HashSet(w1.kill); + k.IntersectWith(w2.kill); + return new GenKillWeight(g, k); + //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill)); + } + + public static GenKillWeight projectLocals(GenKillWeight w) { + Contract.Requires(w != null); + Contract.Ensures(Contract.Result() != null); + HashSet gen = new HashSet(); + foreach (Variable v in w.gen) + { + if (isGlobal(v)) + gen.Add(v); + } + HashSet kill = new HashSet(); + foreach (Variable v in w.kill) + { + if (isGlobal(v)) + kill.Add(v); + } + + return new GenKillWeight(gen, kill); + } + + public static bool isEqual(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + if (w1.isZero) + return w2.isZero; + if (w2.isZero) + return w1.isZero; + + return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill)); + } + + private static bool isGlobal(Variable v) { + Contract.Requires(v != null); + return (v is GlobalVariable); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return string.Format("({0},{1})", gen.ToString(), kill.ToString()); + } + + public HashSet/*!*/ getLiveVars() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return gen; + } + + public HashSet/*!*/ getLiveVars(HashSet/*!*/ lv) { + Contract.Requires(cce.NonNullElements(lv)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + HashSet temp = new HashSet(lv); + temp.ExceptWith(kill); + temp.UnionWith(gen); + return temp; + } + + } + + public class ICFG { + public Graph/*!*/ graph; + // Map from procedure to the list of blocks that call that procedure + public Dictionary/*!*/>/*!*/ procsCalled; + public HashSet/*!*/ nodes; + public Dictionary/*!*/>/*!*/ succEdges; + public Dictionary/*!*/>/*!*/ predEdges; + private Dictionary/*!*/ priority; + + public HashSet/*!*/ srcNodes; + public HashSet/*!*/ exitNodes; + + public Dictionary/*!*/ weightBefore; + public Dictionary/*!*/ weightAfter; + public Dictionary/*!*/>/*!*/ liveVarsAfter; + public Dictionary/*!*/>/*!*/ liveVarsBefore; + + public GenKillWeight/*!*/ summary; + public Implementation/*!*/ impl; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(graph.Nodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled)); + Contract.Invariant(cce.NonNullElements(nodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges)); + Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges)); + Contract.Invariant(priority != null); + Contract.Invariant(cce.NonNullElements(srcNodes)); + Contract.Invariant(cce.NonNullElements(exitNodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter)); + Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter)); + Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore)); + Contract.Invariant(summary != null); + Contract.Invariant(impl != null); + } + + + [NotDelayed] + public ICFG(Implementation impl) { + Contract.Requires(impl != null); + this.graph = new Graph(); + this.procsCalled = new Dictionary/*!*/>(); + this.nodes = new HashSet(); + this.succEdges = new Dictionary/*!*/>(); + this.predEdges = new Dictionary/*!*/>(); + + this.priority = new Dictionary(); + + this.srcNodes = new HashSet(); + this.exitNodes = new HashSet(); + + this.weightBefore = new Dictionary(); + this.weightAfter = new Dictionary(); + this.liveVarsAfter = new Dictionary/*!*/>(); + this.liveVarsBefore = new Dictionary/*!*/>(); + + summary = GenKillWeight.zero(); + this.impl = impl; + + Initialize(impl); + + } + + private void Initialize(Implementation impl) { + Contract.Requires(impl != null); + addSource(impl.Blocks[0]); + graph.AddSource(impl.Blocks[0]); + + foreach (Block/*!*/ b in impl.Blocks) { + Contract.Assert(b != null); + if (b.TransferCmd is ReturnCmd) { + exitNodes.Add(b); + } else { + GotoCmd gc = b.TransferCmd as GotoCmd; + Contract.Assert(gc != null); + Contract.Assert(gc.labelTargets != null); + foreach (Block/*!*/ t in gc.labelTargets) { + Contract.Assert(t != null); + addEdge(b, t); + graph.AddEdge(b, t); + } + } + + weightBefore[b] = GenKillWeight.zero(); + weightAfter[b] = GenKillWeight.zero(); + + foreach (Cmd/*!*/ c in b.Cmds) { + Contract.Assert(c != null); + if (c is CallCmd) { + CallCmd/*!*/ cc = cce.NonNull((CallCmd/*!*/)c); + Contract.Assert(cc.Proc != null); + string/*!*/ procName = cc.Proc.Name; + Contract.Assert(procName != null); + if (!procsCalled.ContainsKey(procName)) { + procsCalled.Add(procName, new List()); + } + procsCalled[procName].Add(b); + } + } + } + + List/*!*/ sortedNodes; + bool acyclic; + + graph.TarjanTopSort(out acyclic, out sortedNodes); + + if (!acyclic) { + Console.WriteLine("Warning: graph is not a dag"); + } + + int num = sortedNodes.Count; + foreach (Block/*!*/ b in sortedNodes) { + Contract.Assert(b != null); + priority.Add(b, num); + num--; + } + + } + + public int getPriority(Block b) { + Contract.Requires(b != null); + if (priority.ContainsKey(b)) + return priority[b]; + return Int32.MaxValue; + } + + private void addSource(Block b) { + Contract.Requires(b != null); + registerNode(b); + this.srcNodes.Add(b); + } + + private void addExit(Block b) { + Contract.Requires(b != null); + registerNode(b); + this.exitNodes.Add(b); + } + + private void registerNode(Block b) { + Contract.Requires(b != null); + if (!succEdges.ContainsKey(b)) { + succEdges.Add(b, new HashSet()); + } + + if (!predEdges.ContainsKey(b)) { + predEdges.Add(b, new HashSet()); + } + + nodes.Add(b); + } + + private void addEdge(Block src, Block tgt) { + Contract.Requires(tgt != null); + Contract.Requires(src != null); + registerNode(src); + registerNode(tgt); + + succEdges[src].Add(tgt); + predEdges[tgt].Add(src); + } + + + } + + // Interprocedural Gen/Kill Analysis + public class InterProcGenKill { + Program/*!*/ program; + Dictionary/*!*/ procICFG; + Dictionary/*!*/ name2Proc; + Dictionary/*!*/>/*!*/ callers; + Graph/*!*/ callGraph; + Dictionary/*!*/ procPriority; + int maxBlocksInProc; + + WorkList/*!*/ workList; + + Implementation/*!*/ mainImpl; + + static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); + static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); + static Dictionary/*!*/ varsLiveSummary = new Dictionary(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(workList != null); + Contract.Invariant(mainImpl != null); + Contract.Invariant(program != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(procICFG)); + Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc)); + Contract.Invariant(cce.NonNullDictionaryAndValues(callers) && + Contract.ForAll(callers.Values, v => cce.NonNullElements(v))); + Contract.Invariant(cce.NonNullElements(callGraph.Nodes)); + Contract.Invariant(procPriority != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry)); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) && + Contract.ForAll(varsLiveAtExit.Values, v => cce.NonNullElements(v))); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveSummary)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheAfterCall)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheBeforeCall)); + } + + + [NotDelayed] + public InterProcGenKill(Implementation impl, Program program) { + Contract.Requires(program != null); + Contract.Requires(impl != null); + this.program = program; + procICFG = new Dictionary(); + name2Proc = new Dictionary(); + workList = new WorkList(); + this.callers = new Dictionary/*!*/>(); + this.callGraph = new Graph(); + this.procPriority = new Dictionary(); + this.maxBlocksInProc = 0; + this.mainImpl = impl; + + Dictionary/*!*/ name2Impl = new Dictionary(); + varsLiveAtExit.Clear(); + varsLiveAtEntry.Clear(); + varsLiveSummary.Clear(); + + foreach (var decl in program.TopLevelDeclarations) { + Contract.Assert(decl != null); + if (decl is Implementation) { + Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl); + name2Impl[imp.Name] = imp; + } else if (decl is Procedure) { + Procedure/*!*/ proc = cce.NonNull(decl as Procedure); + name2Proc[proc.Name] = proc; + } + } + + ICFG/*!*/ mainICFG = new ICFG(mainImpl); + Contract.Assert(mainICFG != null); + procICFG.Add(mainICFG.impl.Name, mainICFG); + callGraph.AddSource(mainICFG.impl.Name); + + List/*!*/ procsToConsider = new List(); + procsToConsider.Add(mainICFG); + + while (procsToConsider.Count != 0) { + ICFG/*!*/ p = procsToConsider[0]; + Contract.Assert(p != null); + procsToConsider.RemoveAt(0); + + foreach (string/*!*/ callee in p.procsCalled.Keys) { + Contract.Assert(callee != null); + if (!name2Impl.ContainsKey(callee)) + continue; + + callGraph.AddEdge(p.impl.Name, callee); + + if (maxBlocksInProc < p.nodes.Count) { + maxBlocksInProc = p.nodes.Count; + } + + if (!callers.ContainsKey(callee)) { + callers.Add(callee, new List()); + } + foreach (Block/*!*/ b in p.procsCalled[callee]) { + Contract.Assert(b != null); + callers[callee].Add(new WorkItem(p, b)); + } + + if (procICFG.ContainsKey(callee)) + continue; + ICFG/*!*/ ncfg = new ICFG(name2Impl[callee]); + Contract.Assert(ncfg != null); + procICFG.Add(callee, ncfg); + procsToConsider.Add(ncfg); + } + } + + bool acyclic; + List/*!*/ sortedNodes; + callGraph.TarjanTopSort(out acyclic, out sortedNodes); + + Contract.Assert(acyclic); + + int cnt = 0; + for (int i = sortedNodes.Count - 1; i >= 0; i--) { + string s = sortedNodes[i]; + if (s == null) + continue; + procPriority.Add(s, cnt); + cnt++; + } + + } + + public static HashSet/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (varsLiveAtExit.ContainsKey(impl.Name)) { + return varsLiveAtExit[impl.Name]; + } + // Return default: all globals and out params + HashSet/*!*/ lv = new HashSet(); + foreach (Variable/*!*/ v in prog.GlobalVariables) { + Contract.Assert(v != null); + lv.Add(v); + } + foreach (Variable/*!*/ v in impl.OutParams) { + Contract.Assert(v != null); + lv.Add(v); + } + return lv; + } + + public static HashSet/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (varsLiveAtEntry.ContainsKey(impl.Name)) { + return varsLiveAtEntry[impl.Name]; + } + // Return default: all globals and in params + HashSet/*!*/ lv = new HashSet(); + foreach (Variable/*!*/ v in prog.GlobalVariables) { + Contract.Assert(v != null); + lv.Add(v); + } + foreach (Variable/*!*/ v in impl.InParams) { + Contract.Assert(v != null); + lv.Add(v); + } + return lv; + } + + public static bool HasSummary(string name) { + Contract.Requires(name != null); + return varsLiveSummary.ContainsKey(name); + } + + public static HashSet/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet/*!*/ lvAfter) { + Contract.Requires(cmd != null); + Contract.Requires(cce.NonNullElements(lvAfter)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Procedure/*!*/ proc = cce.NonNull(cmd.Proc); + if (varsLiveSummary.ContainsKey(proc.Name)) { + GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); + Contract.Assert(w1 != null); + GenKillWeight/*!*/ w2 = varsLiveSummary[proc.Name]; + Contract.Assert(w2 != null); + GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); + Contract.Assert(w3 != null); + GenKillWeight/*!*/ w = GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); + Contract.Assert(w != null); + return w.getLiveVars(lvAfter); + } + HashSet/*!*/ ret = new HashSet(); + ret.UnionWith(lvAfter); + LiveVariableAnalysis.Propagate(cmd, ret); + return ret; + } + + class WorkItem { + public ICFG/*!*/ cfg; + public Block/*!*/ block; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cfg != null); + Contract.Invariant(block != null); + } + + + public WorkItem(ICFG cfg, Block block) { + Contract.Requires(block != null); + Contract.Requires(cfg != null); + this.cfg = cfg; + this.block = block; + } + + public GenKillWeight getWeightAfter() { + Contract.Ensures(Contract.Result() != null); + return cfg.weightAfter[block]; + } + + public bool setWeightBefore(GenKillWeight w) { + Contract.Requires(w != null); + GenKillWeight/*!*/ prev = cfg.weightBefore[block]; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(w, prev); + Contract.Assert(curr != null); + if (GenKillWeight.isEqual(prev, curr)) + return false; + cfg.weightBefore[block] = curr; + return true; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) { + WorkItem/*!*/ wi = (WorkItem/*!*/)cce.NonNull(other); + return (wi.cfg == cfg && wi.block == block); + } + + [Pure] + public override int GetHashCode() { + return 0; + } + + public string getLabel() { + Contract.Ensures(Contract.Result() != null); + return cfg.impl.Name + "::" + block.Label; + } + + } + + private void AddToWorkList(WorkItem wi) { + Contract.Requires(wi != null); + int i = procPriority[wi.cfg.impl.Name]; + int j = wi.cfg.getPriority(wi.block); + int priority = (i * maxBlocksInProc) + j; + + workList.Add(wi, priority); + } + + private void AddToWorkListReverse(WorkItem wi) { + Contract.Requires(wi != null); + int i = procPriority[wi.cfg.impl.Name]; + int j = wi.cfg.getPriority(wi.block); + int priority = (procPriority.Count - i) * maxBlocksInProc + j; + workList.Add(wi, priority); + } + + class WorkList { + SortedList/*!*/ priorities; + HashSet/*!*/ labels; + + Dictionary/*!*/>/*!*/ workList; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(priorities != null); + Contract.Invariant(cce.NonNullElements(labels)); + Contract.Invariant(cce.NonNullDictionaryAndValues(workList) && + Contract.ForAll(workList.Values, v => cce.NonNullElements(v))); + } + + + public WorkList() { + labels = new HashSet(); + priorities = new SortedList(); + workList = new Dictionary/*!*/>(); + } + + public void Add(WorkItem wi, int priority) { + Contract.Requires(wi != null); + string/*!*/ lab = wi.getLabel(); + Contract.Assert(lab != null); + if (labels.Contains(lab)) { + // Already on worklist + return; + } + labels.Add(lab); + if (!workList.ContainsKey(priority)) { + workList.Add(priority, new List()); + } + workList[priority].Add(wi); + if (!priorities.ContainsKey(priority)) { + priorities.Add(priority, 0); + } + + priorities[priority] = priorities[priority] + 1; + } + + public WorkItem Get() { + Contract.Ensures(Contract.Result() != null); + // Get minimum priority + int p = cce.NonNull(priorities.Keys)[0]; + priorities[p] = priorities[p] - 1; + if (priorities[p] == 0) { + priorities.Remove(p); + } + + // Get a WI with this priority + WorkItem/*!*/ wi = workList[p][0]; + Contract.Assert(wi != null); + workList[p].RemoveAt(0); + + // update labels + labels.Remove(wi.getLabel()); + return wi; + } + + public int Count { + get { + return labels.Count; + } + } + } + + private GenKillWeight getSummary(CallCmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert(cmd.Proc != null); + string/*!*/ procName = cmd.Proc.Name; + Contract.Assert(procName != null); + if (procICFG.ContainsKey(procName)) { + ICFG/*!*/ cfg = procICFG[procName]; + Contract.Assert(cfg != null); + return GenKillWeight.projectLocals(cfg.summary); + } + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + public static void ComputeLiveVars(Implementation impl, Program/*!*/ prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + InterProcGenKill/*!*/ ipgk = new InterProcGenKill(impl, prog); + Contract.Assert(ipgk != null); + ipgk.Compute(); + } + + public void Compute() { + // Put all exit nodes in the worklist + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + foreach (Block/*!*/ eb in cfg.exitNodes) { + Contract.Assert(eb != null); + WorkItem/*!*/ wi = new WorkItem(cfg, eb); + Contract.Assert(wi != null); + cfg.weightAfter[eb] = GenKillWeight.one(); + AddToWorkList(wi); + } + } + + while (workList.Count != 0) { + WorkItem/*!*/ wi = workList.Get(); + Contract.Assert(wi != null); + process(wi); + } + + // Propagate LV to all procedures + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + foreach (Block/*!*/ b in cfg.nodes) { + Contract.Assert(b != null); + cfg.liveVarsAfter.Add(b, new HashSet()); + cfg.liveVarsBefore.Add(b, new HashSet()); + } + } + + ICFG/*!*/ mainCfg = procICFG[mainImpl.Name]; + Contract.Assert(mainCfg != null); + foreach (Block/*!*/ eb in mainCfg.exitNodes) { + Contract.Assert(eb != null); + WorkItem/*!*/ wi = new WorkItem(mainCfg, eb); + Contract.Assert(wi != null); + AddToWorkListReverse(wi); + } + + while (workList.Count != 0) { + WorkItem/*!*/ wi = workList.Get(); + Contract.Assert(wi != null); + processLV(wi); + } + + // Set live variable info + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + HashSet/*!*/ lv = new HashSet(); + foreach (Block/*!*/ eb in cfg.exitNodes) { + Contract.Assert(eb != null); + lv.UnionWith(cfg.liveVarsAfter[eb]); + } + varsLiveAtExit.Add(cfg.impl.Name, lv); + lv = new HashSet(); + foreach (Block/*!*/ eb in cfg.srcNodes) { + Contract.Assert(eb != null); + lv.UnionWith(cfg.liveVarsBefore[eb]); + } + varsLiveAtEntry.Add(cfg.impl.Name, lv); + varsLiveSummary.Add(cfg.impl.Name, cfg.summary); + } + + /* + foreach(Block/*!*/ + /* b in mainImpl.Blocks){ +Contract.Assert(b != null); +//Set lv = cfg.weightBefore[b].getLiveVars(); +b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; +//foreach(GlobalVariable/*!*/ + /* v in program.GlobalVariables){Contract.Assert(v != null); +// b.liveVarsBefore.Add(v); +//} +} +*/ + } + + // Called when summaries have already been computed + private void processLV(WorkItem wi) { + Contract.Requires(wi != null); + ICFG/*!*/ cfg = wi.cfg; + Contract.Assert(cfg != null); + Block/*!*/ block = wi.block; + Contract.Assert(block != null); + HashSet/*!*/ lv = cfg.liveVarsAfter[block]; + Contract.Assert(cce.NonNullElements(lv)); + // Propagate backwards in the block + HashSet/*!*/ prop = new HashSet(); + prop.UnionWith(lv); + for (int i = block.Cmds.Count - 1; i >= 0; i--) { + Cmd/*!*/ cmd = block.Cmds[i]; + Contract.Assert(cmd != null); + if (cmd is CallCmd) { + string/*!*/ procName = cce.NonNull(cce.NonNull((CallCmd)cmd).Proc).Name; + Contract.Assert(procName != null); + if (procICFG.ContainsKey(procName)) { + ICFG/*!*/ callee = procICFG[procName]; + Contract.Assert(callee != null); + // Inter propagation + // Remove local variables; add return variables + HashSet/*!*/ elv = new HashSet(); + foreach (Variable/*!*/ v in prop) { + Contract.Assert(v != null); + if (v is GlobalVariable) + elv.Add(v); + } + foreach (Variable/*!*/ v in callee.impl.OutParams) { + Contract.Assert(v != null); + elv.Add(v); + } + + foreach (Block/*!*/ eb in callee.exitNodes) { + Contract.Assert(eb != null); + callee.liveVarsAfter[eb].UnionWith(elv); + // TODO: check if modified before inserting + AddToWorkListReverse(new WorkItem(callee, eb)); + } + + // Continue with intra propagation + GenKillWeight/*!*/ summary = getWeightCall(cce.NonNull((CallCmd/*!*/)cmd)); + prop = summary.getLiveVars(prop); + } else { + LiveVariableAnalysis.Propagate(cmd, prop); + } + } else { + LiveVariableAnalysis.Propagate(cmd, prop); + } + } + + cfg.liveVarsBefore[block].UnionWith(prop); + + foreach (Block/*!*/ b in cfg.predEdges[block]) { + Contract.Assert(b != null); + HashSet/*!*/ prev = cfg.liveVarsAfter[b]; + Contract.Assert(cce.NonNullElements(prev)); + HashSet/*!*/ curr = new HashSet(prev); + curr.UnionWith(cfg.liveVarsBefore[block]); + Contract.Assert(cce.NonNullElements(curr)); + if (curr.Count != prev.Count) { + cfg.liveVarsAfter[b] = curr; + AddToWorkListReverse(new WorkItem(cfg, b)); + } + } + } + + private void process(WorkItem wi) { + Contract.Requires(wi != null); + GenKillWeight/*!*/ w = wi.getWeightAfter(); + Contract.Assert(w != null); + + for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) { + Cmd/*!*/ c = wi.block.Cmds[i]; + Contract.Assert(c != null); + if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) { + w = GenKillWeight.extend(getWeightCall(cce.NonNull((CallCmd)c)), w); + } else { + GenKillWeight/*!*/ cweight = getWeight(c, wi.cfg.impl, program); + Contract.Assert(cweight != null); + w = GenKillWeight.extend(cweight, w); + } + } + + bool change = wi.setWeightBefore(w); + + if (change && wi.cfg.srcNodes.Contains(wi.block)) { + GenKillWeight/*!*/ prev = wi.cfg.summary; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, wi.cfg.weightBefore[wi.block]); + Contract.Assert(curr != null); + if (!GenKillWeight.isEqual(prev, curr)) { + wi.cfg.summary = curr; + // push callers onto the worklist + if (callers.ContainsKey(wi.cfg.impl.Name)) { + foreach (WorkItem/*!*/ caller in callers[wi.cfg.impl.Name]) { + Contract.Assert(caller != null); + AddToWorkList(caller); + } + } + } + } + + foreach (Block/*!*/ b in wi.cfg.predEdges[wi.block]) { + Contract.Assert(b != null); + GenKillWeight/*!*/ prev = wi.cfg.weightAfter[b]; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, w); + Contract.Assert(curr != null); + if (!GenKillWeight.isEqual(prev, curr)) { + wi.cfg.weightAfter[b] = curr; + AddToWorkList(new WorkItem(wi.cfg, b)); + } + } + + } + + static Dictionary/*!*/ weightCache = new Dictionary(); + + private static GenKillWeight getWeight(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + return getWeight(cmd, null, null); + } + + private GenKillWeight getWeightCall(CallCmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); + GenKillWeight/*!*/ w2 = getSummary(cmd); + GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); + Contract.Assert(w1 != null); + Contract.Assert(w2 != null); + Contract.Assert(w3 != null); + return GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); + } + + private static GenKillWeight getWeight(Cmd cmd, Implementation impl, Program prog) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + + if (weightCache.ContainsKey(cmd)) + return weightCache[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + GenKillWeight/*!*/ ret; + + if (cmd is AssignCmd) { + AssignCmd/*!*/ assignCmd = (AssignCmd)cmd; + Contract.Assert(cmd != null); + // 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 + foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { + Contract.Assert(lhs != null); + Variable var = lhs.DeepAssignedVariable; + if (var != null) { + 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 + kill.Add(var); + } + } + } + int index = 0; + foreach (Expr/*!*/ expr in assignCmd.Rhss) { + Contract.Assert(expr != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + gen.UnionWith(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); + gen.UnionWith(c.usedVars); + } + } + index++; + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is HavocCmd) { + HavocCmd/*!*/ havocCmd = (HavocCmd)cce.NonNull(cmd); + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + if (expr.Decl != null) { + kill.Add(expr.Decl); + } + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is PredicateCmd) { + Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); + PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); + if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) { + LiteralExpr le = (LiteralExpr)predicateCmd.Expr; + if (le.IsFalse) { + var globals = prog.GlobalVariables; + Contract.Assert(cce.NonNullElements(globals)); + foreach (Variable/*!*/ v in globals) { + Contract.Assert(v != null); + kill.Add(v); + } + foreach (Variable/*!*/ v in impl.LocVars) { + Contract.Assert(v != null); + kill.Add(v); + } + foreach (Variable/*!*/ v in impl.OutParams) { + Contract.Assert(v != null); + kill.Add(v); + } + } + } else { + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(predicateCmd.Expr); + gen.UnionWith(collector.usedVars); + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is CommentCmd) { + ret = new GenKillWeight(gen, kill); + // comments are just for debugging and don't affect verification + } else if (cmd is SugaredCmd) { + SugaredCmd/*!*/ sugCmd = (SugaredCmd)cmd; + Contract.Assert(sugCmd != null); + ret = getWeight(sugCmd.Desugaring, impl, prog); + } else if (cmd is StateCmd) { + StateCmd/*!*/ stCmd = (StateCmd)cmd; + Contract.Assert(stCmd != null); + List/*!*/ cmds = stCmd.Cmds; + Contract.Assert(cmds != null); + int len = cmds.Count; + ret = GenKillWeight.one(); + for (int i = len - 1; i >= 0; i--) { + GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog); + Contract.Assert(w != null); + ret = GenKillWeight.extend(w, ret); + } + foreach (Variable/*!*/ v in stCmd.Locals) { + Contract.Assert(v != null); + kill.Add(v); + } + ret = GenKillWeight.extend(new GenKillWeight(gen, kill), ret); + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + weightCache[cmd] = ret; + return ret; + } + + static Dictionary/*!*/ weightCacheAfterCall = new Dictionary(); + static Dictionary/*!*/ weightCacheBeforeCall = new Dictionary(); + + private static GenKillWeight getWeightAfterCall(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + + if (weightCacheAfterCall.ContainsKey(cmd)) + return weightCacheAfterCall[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + + Contract.Assert(cmd is CallCmd); + CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd); + + foreach (IdentifierExpr/*!*/ ie in ccmd.Outs) { + Contract.Assert(ie != null); + if (ie.Decl != null) + kill.Add(ie.Decl); + } + + // Variables in ensures are considered as "read" + foreach (Ensures/*!*/ re in cce.NonNull(ccmd.Proc).Ensures) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.usedVars) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); + Contract.Assert(ret != null); + weightCacheAfterCall[cmd] = ret; + return ret; + } + + private static GenKillWeight getWeightBeforeCall(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert((cmd is CallCmd)); + if (weightCacheBeforeCall.ContainsKey(cmd)) + return weightCacheBeforeCall[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd); + + foreach (Expr/*!*/ expr in ccmd.Ins) { + Contract.Assert(expr != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + gen.UnionWith(collector.usedVars); + } + + Contract.Assert(ccmd.Proc != null); + + // Variables in requires are considered as "read" + foreach (Requires/*!*/ re in ccmd.Proc.Requires) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.usedVars) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + // Old variables in ensures are considered as "read" + foreach (Ensures/*!*/ re in ccmd.Proc.Ensures) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.oldVarsUsed) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); + Contract.Assert(ret != null); + weightCacheAfterCall[cmd] = ret; + return ret; + } + } + + public class TokenEliminator : ReadOnlyVisitor + { + public int TokenCount = 0; + public override Expr VisitExpr(Expr node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitExpr(node); + } + public override Variable VisitVariable(Variable node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitVariable(node); + } + public override Function VisitFunction(Function node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitFunction(node); + } + public override Implementation VisitImplementation(Implementation node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitImplementation(node); + } + public override Procedure VisitProcedure(Procedure node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitProcedure(node); + } + public override Axiom VisitAxiom(Axiom node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAxiom(node); + } + public override Cmd VisitAssignCmd(AssignCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAssignCmd(node); + } + public override Cmd VisitAssumeCmd(AssumeCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAssumeCmd(node); + } + public override Cmd VisitHavocCmd(HavocCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitHavocCmd(node); + } + public override Constant VisitConstant(Constant node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitConstant(node); + } + public override TransferCmd VisitTransferCmd(TransferCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitTransferCmd(node); + } + public override Block VisitBlock(Block node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitBlock(node); + } + } } \ No newline at end of file diff --git a/Test/civl/chris4.bpl b/Test/civl/chris4.bpl new file mode 100644 index 00000000..7a19f975 --- /dev/null +++ b/Test/civl/chris4.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:yields}{:layer 94,95} Test() +{ + yield; + L: + yield; +} + +procedure{:yields}{:layer 94,95} Test2() +{ + yield; + assert{:layer 94} 2 + 2 == 3; + L: + yield; +} diff --git a/Test/civl/chris4.bpl.expect b/Test/civl/chris4.bpl.expect new file mode 100644 index 00000000..d3d00979 --- /dev/null +++ b/Test/civl/chris4.bpl.expect @@ -0,0 +1,5 @@ +chris4.bpl(13,3): Error BP5001: This assertion might not hold. +Execution trace: + chris4.bpl(12,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error -- cgit v1.2.3