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<Implementation>() != 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<Variable>/*!*/ vars = new List<Variable>();
      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<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ 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<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

      HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
      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<Variable>());
            }
        }
      }

      moreProcessingRequired = true;
      while (moreProcessingRequired) {
        moreProcessingRequired = false;
        ModSetCollector modSetCollector = new ModSetCollector();
        modSetCollector.Visit(program);
      }

      foreach (Procedure x in modSets.Keys)
      {
          x.Modifies = new List<IdentifierExpr>();
          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<Implementation>() != 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<Cmd>() != 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<Cmd>() != 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<Cmd>() != 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<Variable/*!*/>();
      }
      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<Variable/*!*/>/*!*/ usedVars;
    public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(usedVars));
      Contract.Invariant(cce.NonNullElements(oldVarsUsed));
    }

    int insideOldExpr;

    public VariableCollector() {
      usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();
      oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();
      insideOldExpr = 0;
    }

    public override Expr VisitOldExpr(OldExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != 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<Expr>() != 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<Block/*!*/>/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) {
      Contract.Requires(impl != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));
      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();
      HashSet<Block/*!*/> multiPredBlocks = new HashSet<Block/*!*/>();
      Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();
      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<Implementation>() != null);
      //Console.WriteLine("Procedure {0}", impl.Name);
      //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);

      HashSet<Block/*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
      Contract.Assert(cce.NonNullElements(multiPredBlocks));
      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();
      HashSet<Block/*!*/> removedBlocks = new HashSet<Block/*!*/>();
      Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();
      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<Block/*!*/> newBlocks = new List<Block/*!*/>();
      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<Block> dag = new Graph<Block>();
      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<Block> sortedNodes = dag.TopologicalSort();
      foreach (Block/*!*/ block in sortedNodes) {
        Contract.Assert(block != null);
        HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();
        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<Cmd> 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<Variable/*!*/>/*!*/ 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<int> indexSet = new HashSet<int>();
        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<Cmd>/*!*/ 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<Variable/*!*/>/*!*/ gen;
    HashSet<Variable/*!*/>/*!*/ 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<Variable/*!*/>(), new HashSet<Variable/*!*/>());
    public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight();

    // initializes to zero
    public GenKillWeight() {
      this.isZero = true;
      this.gen = new HashSet<Variable/*!*/>();
      this.kill = new HashSet<Variable/*!*/>();
    }

    public GenKillWeight(HashSet<Variable/*!*/> gen, HashSet<Variable/*!*/> 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<GenKillWeight>() != null);
      return oneWeight;
    }

    public static GenKillWeight zero() {
      Contract.Ensures(Contract.Result<GenKillWeight>() != null);
      return zeroWeight;
    }

    public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2) {
      Contract.Requires(w2 != null);
      Contract.Requires(w1 != null);
      Contract.Ensures(Contract.Result<GenKillWeight>() != null);
      if (w1.isZero || w2.isZero)
        return zero();

      HashSet<Variable> t = new HashSet<Variable>(w2.gen);
      t.ExceptWith(w1.kill);
      HashSet<Variable> g = new HashSet<Variable>(w1.gen);
      g.UnionWith(t);
      HashSet<Variable> k = new HashSet<Variable>(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<GenKillWeight>() != null);
      if (w1.isZero)
        return w2;
      if (w2.isZero)
        return w1;

      HashSet<Variable> g = new HashSet<Variable>(w1.gen);
      g.UnionWith(w2.gen);
      HashSet<Variable> k = new HashSet<Variable>(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<GenKillWeight>() != null);
      HashSet<Variable/*!*/> gen = new HashSet<Variable>();
      foreach (Variable v in w.gen)
      {
          if (isGlobal(v))
              gen.Add(v);
      }
      HashSet<Variable/*!*/> kill = new HashSet<Variable>();
      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<string>() != null);
      return string.Format("({0},{1})", gen.ToString(), kill.ToString());
    }

    public HashSet<Variable/*!*/>/*!*/ getLiveVars() {
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
      return gen;
    }

    public HashSet<Variable/*!*/>/*!*/ getLiveVars(HashSet<Variable/*!*/>/*!*/ lv) {
      Contract.Requires(cce.NonNullElements(lv));
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
      HashSet<Variable> temp = new HashSet<Variable>(lv);
      temp.ExceptWith(kill);
      temp.UnionWith(gen);
      return temp;
    }

  }

  public class ICFG {
    public Graph<Block/*!*/>/*!*/ graph;
    // Map from procedure to the list of blocks that call that procedure
    public Dictionary<string/*!*/, List<Block/*!*/>/*!*/>/*!*/ procsCalled;
    public HashSet<Block/*!*/>/*!*/ nodes;
    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ succEdges;
    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ predEdges;
    private Dictionary<Block/*!*/, int>/*!*/ priority;

    public HashSet<Block/*!*/>/*!*/ srcNodes;
    public HashSet<Block/*!*/>/*!*/ exitNodes;

    public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightBefore;
    public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightAfter;
    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ liveVarsAfter;
    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ 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<Block/*!*/>();
      this.procsCalled = new Dictionary<string/*!*/, List<Block/*!*/>/*!*/>();
      this.nodes = new HashSet<Block/*!*/>();
      this.succEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();
      this.predEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();

      this.priority = new Dictionary<Block/*!*/, int>();

      this.srcNodes = new HashSet<Block/*!*/>();
      this.exitNodes = new HashSet<Block/*!*/>();

      this.weightBefore = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();
      this.weightAfter = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();
      this.liveVarsAfter = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();
      this.liveVarsBefore = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();

      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<Block/*!*/>());
            }
            procsCalled[procName].Add(b);
          }
        }
      }

      List<Block>/*!*/ 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<Block/*!*/>());
      }

      if (!predEdges.ContainsKey(b)) {
        predEdges.Add(b, new HashSet<Block/*!*/>());
      }

      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<string/*!*/, ICFG/*!*/>/*!*/ procICFG;
    Dictionary<string/*!*/, Procedure/*!*/>/*!*/ name2Proc;
    Dictionary<string/*!*/, List<WorkItem/*!*/>/*!*/>/*!*/ callers;
    Graph<string/*!*/>/*!*/ callGraph;
    Dictionary<string/*!*/, int>/*!*/ procPriority;
    int maxBlocksInProc;

    WorkList/*!*/ workList;

    Implementation/*!*/ mainImpl;

    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtExit = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();
    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtEntry = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();
    static Dictionary<string/*!*/, GenKillWeight/*!*/>/*!*/ varsLiveSummary = new Dictionary<string/*!*/, GenKillWeight/*!*/>();
    [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<string/*!*/, ICFG/*!*/>();
      name2Proc = new Dictionary<string/*!*/, Procedure/*!*/>();
      workList = new WorkList();
      this.callers = new Dictionary<string/*!*/, List<WorkItem/*!*/>/*!*/>();
      this.callGraph = new Graph<string/*!*/>();
      this.procPriority = new Dictionary<string/*!*/, int>();
      this.maxBlocksInProc = 0;
      this.mainImpl = impl;

      Dictionary<string/*!*/, Implementation/*!*/>/*!*/ name2Impl = new Dictionary<string/*!*/, Implementation/*!*/>();
      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<ICFG/*!*/>/*!*/ procsToConsider = new List<ICFG/*!*/>();
      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<WorkItem/*!*/>());
          }
          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<string>/*!*/ 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<Variable/*!*/>/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) {
      Contract.Requires(prog != null);
      Contract.Requires(impl != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
      if (varsLiveAtExit.ContainsKey(impl.Name)) {
        return varsLiveAtExit[impl.Name];
      }
      // Return default: all globals and out params
      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();
      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<Variable/*!*/>/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) {
      Contract.Requires(prog != null);
      Contract.Requires(impl != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
      if (varsLiveAtEntry.ContainsKey(impl.Name)) {
        return varsLiveAtEntry[impl.Name];
      }
      // Return default: all globals and in params
      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();
      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<Variable/*!*/>/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet<Variable/*!*/>/*!*/ lvAfter) {
      Contract.Requires(cmd != null);
      Contract.Requires(cce.NonNullElements(lvAfter));
      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
      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<Variable/*!*/>/*!*/ ret = new HashSet<Variable/*!*/>();
      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<GenKillWeight>() != 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<string>() != 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<int, int>/*!*/ priorities;
      HashSet<string/*!*/>/*!*/ labels;

      Dictionary<int, List<WorkItem/*!*/>/*!*/>/*!*/ 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<string/*!*/>();
        priorities = new SortedList<int, int>();
        workList = new Dictionary<int, List<WorkItem/*!*/>/*!*/>();
      }

      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<WorkItem/*!*/>());
        }
        workList[priority].Add(wi);
        if (!priorities.ContainsKey(priority)) {
          priorities.Add(priority, 0);
        }

        priorities[priority] = priorities[priority] + 1;
      }

      public WorkItem Get() {
        Contract.Ensures(Contract.Result<WorkItem>() != 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<GenKillWeight>() != 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<Variable/*!*/>());
          cfg.liveVarsBefore.Add(b, new HashSet<Variable/*!*/>());
        }
      }

      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<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();
        foreach (Block/*!*/ eb in cfg.exitNodes) {
          Contract.Assert(eb != null);
          lv.UnionWith(cfg.liveVarsAfter[eb]);
        }
        varsLiveAtExit.Add(cfg.impl.Name, lv);
        lv = new HashSet<Variable/*!*/>();
        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<Variable!> 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<Variable/*!*/>/*!*/ lv = cfg.liveVarsAfter[block];
      Contract.Assert(cce.NonNullElements(lv));
      // Propagate backwards in the block
      HashSet<Variable/*!*/>/*!*/ prop = new HashSet<Variable/*!*/>();
      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<Variable/*!*/>/*!*/ elv = new HashSet<Variable/*!*/>();
            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<Variable/*!*/>/*!*/ prev = cfg.liveVarsAfter[b];
        Contract.Assert(cce.NonNullElements(prev));
        HashSet<Variable/*!*/>/*!*/ curr = new HashSet<Variable>(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<Cmd/*!*/, GenKillWeight/*!*/>/*!*/ weightCache = new Dictionary<Cmd/*!*/, GenKillWeight/*!*/>();

    private static GenKillWeight getWeight(Cmd cmd) {
      Contract.Requires(cmd != null);
      Contract.Ensures(Contract.Result<GenKillWeight>() != null);
      return getWeight(cmd, null, null);
    }

    private GenKillWeight getWeightCall(CallCmd cmd) {
      Contract.Requires(cmd != null);
      Contract.Ensures(Contract.Result<GenKillWeight>() != 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<GenKillWeight>() != null);

      if (weightCache.ContainsKey(cmd))
        return weightCache[cmd];

      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();
      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();
      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<GlobalVariable/*!*/>/*!*/ 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<Cmd>/*!*/ 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<Cmd/*!*/, GenKillWeight/*!*/>/*!*/ weightCacheAfterCall = new Dictionary<Cmd/*!*/, GenKillWeight/*!*/>();
    static Dictionary<Cmd/*!*/, GenKillWeight/*!*/>/*!*/ weightCacheBeforeCall = new Dictionary<Cmd/*!*/, GenKillWeight/*!*/>();

    private static GenKillWeight getWeightAfterCall(Cmd cmd) {
      Contract.Requires(cmd != null);
      Contract.Ensures(Contract.Result<GenKillWeight>() != null);

      if (weightCacheAfterCall.ContainsKey(cmd))
        return weightCacheAfterCall[cmd];

      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();
      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

      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<GenKillWeight>() != null);
      Contract.Assert((cmd is CallCmd));
      if (weightCacheBeforeCall.ContainsKey(cmd))
        return weightCacheBeforeCall[cmd];

      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();
      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();
      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;
    }
  }
}