using System; using System.Collections.Generic; using Microsoft.Boogie.GraphUtil; using PureCollections; 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 : StandardVisitor { static Procedure proc; static Dictionary/*!*/>/*!*/ modSets; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v))); } static bool moreProcessingRequired; public static 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);*/ } modSets = new Dictionary/*!*/>(); HashSet implementedProcs = new HashSet(); foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); if (decl is Implementation) { Implementation impl = (Implementation)decl; if (impl.Proc != null) implementedProcs.Add(impl.Proc); } } foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); if (decl is Procedure) { if (!implementedProcs.Contains(cce.NonNull((Procedure)decl))) { proc = (Procedure)decl; foreach (IdentifierExpr/*!*/ expr in proc.Modifies) { Contract.Assert(expr != null); ProcessVariable(expr.Decl); } proc = null; } else { modSets.Add(decl as Procedure, new HashSet()); } } } moreProcessingRequired = true; while (moreProcessingRequired) { moreProcessingRequired = false; ModSetCollector modSetCollector = new ModSetCollector(); modSetCollector.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)); } } if (false /*CommandLineOptions.Clo.Trace*/) { 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(""); } } } public override Implementation VisitImplementation(Implementation node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); proc = node.Proc; Implementation/*!*/ ret = base.VisitImplementation(node); Contract.Assert(ret != null); proc = null; return ret; } 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); } } return ret; } private static void ProcessVariable(Variable var) { Procedure/*!*/ localProc = cce.NonNull(proc); 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 VariableCollector : StandardVisitor { public HashSet/*!*/ usedVars; public HashSet/*!*/ oldVarsUsed; [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 : StandardVisitor { 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 = dag.TopologicalSort(); foreach (Block/*!*/ block in sortedNodes) { Contract.Assert(block != null); HashSet/*!*/ liveVarsAfter = new HashSet(); 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) { 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.TopologicalSort())); 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.TopologicalSort())); 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 (Declaration/*!*/ 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) { List/*!*/ 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; } } }