path: root/Source/VCGeneration/ConditionGeneration.cs

//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
using Graphing;
using AI = Microsoft.AbstractInterpretationFramework;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
using Set = Microsoft.Boogie.GSet<object>;

namespace Microsoft.Boogie {

  public class CalleeCounterexampleInfo {
    public Counterexample counterexample;
    public List<Model.Element>/*!>!*/ args;

    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(args));
    }

    public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {
      Contract.Requires(cce.NonNullElements(x));
      counterexample = cex;
      args = x;
    }
  }

  public class TraceLocation : IEquatable<TraceLocation>
  {
      public int numBlock;
      public int numInstr;

      public TraceLocation(int numBlock, int numInstr)
      {
          this.numBlock = numBlock;
          this.numInstr = numInstr;
      }

      public override bool Equals(object obj)
      {
          TraceLocation that = obj as TraceLocation;
          if (that == null) return false;
          return (numBlock == that.numBlock && numInstr == that.numInstr);
      }

      public bool Equals(TraceLocation that)
      {
          return (numBlock == that.numBlock && numInstr == that.numInstr);
      }

      public override int GetHashCode()
      {
          return numBlock.GetHashCode() ^ 131 * numInstr.GetHashCode();
      }
  }

  public abstract class Counterexample {
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Trace != null);
      Contract.Invariant(Context != null);
      Contract.Invariant(cce.NonNullElements(relatedInformation));
      Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples));
    }

    [Peer]
    public BlockSeq Trace;
    public Model Model;
    public VC.ModelViewInfo MvInfo;
    public ProverContext Context;
    [Peer]
    public List<string>/*!>!*/ relatedInformation;

    public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

    internal Counterexample(BlockSeq trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {
      Contract.Requires(trace != null);
      Contract.Requires(context != null);
      this.Trace = trace;
      this.Model = model;
      this.MvInfo = mvInfo;
      this.Context = context;
      this.relatedInformation = new List<string>();
      this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
    }

    // Create a shallow copy of the counterexample
    public abstract Counterexample Clone();

    public void AddCalleeCounterexample(TraceLocation loc, CalleeCounterexampleInfo cex)
    {
      Contract.Requires(cex != null);
      calleeCounterexamples[loc] = cex;
    }

    public void AddCalleeCounterexample(int numBlock, int numInstr, CalleeCounterexampleInfo cex)
    {
        Contract.Requires(cex != null);
        calleeCounterexamples[new TraceLocation(numBlock, numInstr)] = cex;
    }

    public void AddCalleeCounterexample(Dictionary<TraceLocation, CalleeCounterexampleInfo> cs)
    {
      Contract.Requires(cce.NonNullDictionaryAndValues(cs));
      foreach (TraceLocation loc in cs.Keys)
      {
          AddCalleeCounterexample(loc, cs[loc]);
      }
    }

    // Looks up the Cmd at a given index into the trace
    public Cmd getTraceCmd(TraceLocation loc)
    {
        Debug.Assert(loc.numBlock < Trace.Length);
        Block b = Trace[loc.numBlock];
        Debug.Assert(loc.numInstr < b.Cmds.Length);
        return b.Cmds[loc.numInstr];
    }

    // Looks up the name of the called procedure.
    // Asserts that the name exists
    public string getCalledProcName(Cmd cmd)
    {
        // There are two options:
        // 1. cmd is a CallCmd
        // 2. cmd is an AssumeCmd (passified version of a CallCmd)
        if(cmd is CallCmd) {
            return (cmd as CallCmd).Proc.Name;
        }
        AssumeCmd assumeCmd = cmd as AssumeCmd;
        Debug.Assert(assumeCmd != null);

        NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
        Debug.Assert(naryExpr != null);

        return naryExpr.Fun.FunctionName;
    }

    public void Print(int indent) {
      int numBlock = -1;
      string ind = new string(' ', indent);
      foreach (Block b in Trace) {
        Contract.Assert(b != null);
        numBlock++;
        if (b.tok == null) {
          Console.WriteLine("{0}<intermediate block>", ind);
        } else {
          // for ErrorTrace == 1 restrict the output;
          // do not print tokens with -17:-4 as their location because they have been
          // introduced in the translation and do not give any useful feedback to the user
          if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {
            Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
            for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)
            {
                var loc = new TraceLocation(numBlock, numInstr);
                if (calleeCounterexamples.ContainsKey(loc))
                {
                    var cmd = getTraceCmd(loc);
                    var calleeName = getCalledProcName(cmd);
                    if (calleeName.StartsWith(VC.StratifiedVCGen.recordProcName) && CommandLineOptions.Clo.StratifiedInlining > 0)
                    {
                        Contract.Assert(calleeCounterexamples[loc].args.Count == 1);
                        var arg = calleeCounterexamples[loc].args[0];
                        Console.WriteLine("{0}value = {1}", ind, arg.ToString());
                    }
                    else
                    {
                        Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
                        calleeCounterexamples[loc].counterexample.Print(indent + 4);
                        Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
                    }
                }
            }
          }
        }
      }
    }

    public static bool firstModelFile = true;

    public void PrintModel()
    {
      var filename = CommandLineOptions.Clo.ModelViewFile;
      if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;

      var m = this.GetModelWithStates();

      if (filename == "-") {
        m.Write(Console.Out);
        Console.Out.Flush();
      } else {
        using (var wr = new StreamWriter(filename, !firstModelFile)) {
          firstModelFile = false;
          m.Write(wr);
        }
      }
    }

    void ApplyRedirections(Model m) {
      var mapping = new Dictionary<Model.Element, Model.Element>();
      foreach (var name in new string[] { "U_2_bool", "U_2_int" }) {
        Model.Func f = m.TryGetFunc(name);
        if (f != null && f.Arity == 1) {
          foreach (var ft in f.Apps) mapping[ft.Args[0]] = ft.Result;
        }
      }
      m.Substitute(mapping);
    }

    public Model GetModelWithStates()
    {
      if (Model == null) return null;

      Model m = Model;
      ApplyRedirections(m); 

      var mvstates = m.TryGetFunc("@MV_state");
      if (MvInfo == null || mvstates == null)
        return m;

      Contract.Assert(mvstates.Arity == 2);

      foreach (Variable v in MvInfo.AllVariables) {
        m.InitialState.AddBinding(v.Name, GetModelValue(m, v));
      }

      var states = new List<int>();
      foreach (var t in mvstates.Apps)
        states.Add(t.Args[1].AsInt());

      states.Sort();

      for (int i = 0; i < states.Count; ++i) {
        var s = states[i];
        if (0 <= s && s < MvInfo.CapturePoints.Count) {
          VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];
          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();
          var cs = m.MkState(map.Description);

          foreach (Variable v in MvInfo.AllVariables) {
            var e = (Expr)map.IncarnationMap[v];
            if (e == null) continue;

            if (prevInc[v] == e) continue; // skip unchanged variables

            Model.Element elt;

            if (e is IdentifierExpr) {
              IdentifierExpr ide = (IdentifierExpr)e;
              elt = GetModelValue(m, ide.Decl);
            } else if (e is LiteralExpr) {
              LiteralExpr lit = (LiteralExpr)e;
              elt = m.MkElement(lit.Val.ToString());
            } else {
              elt = m.MkFunc(e.ToString(), 0).GetConstant();
            }

            cs.AddBinding(v.Name, elt);
          }

        } else {
          Contract.Assume(false);
        }
      }

      return m;
    }

    private Model.Element GetModelValue(Model m, Variable v) {
      Model.Element elt;
      // first, get the unique name
      string uniqueName;
      VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);
      if (vvar == null) {
        uniqueName = v.Name;
      } else {
        uniqueName = Context.Lookup(vvar);
      }

      var f = m.TryGetFunc(uniqueName);
      if (f == null) {
        f = m.MkFunc(uniqueName, 0);
      }
      elt = f.GetConstant();
      return elt;
    }

    public abstract int GetLocation();
  }

  public class CounterexampleComparer : IComparer<Counterexample> {
    public int Compare(Counterexample c1, Counterexample c2) {
      //Contract.Requires(c1 != null);
      //Contract.Requires(c2 != null);
      if (c1.GetLocation() == c2.GetLocation())
        return 0;
      if (c1.GetLocation() > c2.GetLocation())
        return 1;
      return -1;
    }
  }

  public class AssertCounterexample : Counterexample {
    [Peer]
    public AssertCmd FailingAssert;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(FailingAssert != null);
    }


    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
      : base(trace, model, mvInfo, context) {
      Contract.Requires(trace != null);
      Contract.Requires(failingAssert != null);
      Contract.Requires(context != null);
      this.FailingAssert = failingAssert;
    }

    public override int GetLocation() {
      return FailingAssert.tok.line * 1000 + FailingAssert.tok.col;
    }

    public override Counterexample Clone()
    {
        var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context);
        ret.calleeCounterexamples = calleeCounterexamples;
        return ret;
    }
  }

  public class CallCounterexample : Counterexample {
    public CallCmd FailingCall;
    public Requires FailingRequires;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(FailingCall != null);
      Contract.Invariant(FailingRequires != null);
    }


    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
      : base(trace, model, mvInfo, context) {
      Contract.Requires(!failingRequires.Free);
      Contract.Requires(trace != null);
      Contract.Requires(context != null);
      Contract.Requires(failingCall != null);
      Contract.Requires(failingRequires != null);
      this.FailingCall = failingCall;
      this.FailingRequires = failingRequires;
    }

    public override int GetLocation() {
      return FailingCall.tok.line * 1000 + FailingCall.tok.col;
    }

    public override Counterexample Clone()
    {
        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);
        ret.calleeCounterexamples = calleeCounterexamples;
        return ret;
    }
  }

  public class ReturnCounterexample : Counterexample {
    public TransferCmd FailingReturn;
    public Ensures FailingEnsures;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(FailingEnsures != null);
      Contract.Invariant(FailingReturn != null);
    }


    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
      : base(trace, model, mvInfo, context) {
      Contract.Requires(trace != null);
      Contract.Requires(context != null);
      Contract.Requires(failingReturn != null);
      Contract.Requires(failingEnsures != null);
      Contract.Requires(!failingEnsures.Free);
      this.FailingReturn = failingReturn;
      this.FailingEnsures = failingEnsures;
    }

    public override int GetLocation() {
      return FailingReturn.tok.line * 1000 + FailingReturn.tok.col;
    }

    public override Counterexample Clone()
    {
        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context);
        ret.calleeCounterexamples = calleeCounterexamples;
        return ret;
    }
  }

  public class VerifierCallback {
    // reason == null means this is genuine counterexample returned by the prover
    // other reason means it's time out/memory out/crash
    public virtual void OnCounterexample(Counterexample ce, string/*?*/ reason) {
      Contract.Requires(ce != null);
    }

    // called in case resource is exceeded and we don't have counterexample
    public virtual void OnTimeout(string reason) {
      Contract.Requires(reason != null);
    }

    public virtual void OnOutOfMemory(string reason) {
      Contract.Requires(reason != null);
    }

    public virtual void OnProgress(string phase, int step, int totalSteps, double progressEstimate) {
    }

    public virtual void OnUnreachableCode(Implementation impl) {
      Contract.Requires(impl != null);
    }

    public virtual void OnWarning(string msg) {
      Contract.Requires(msg != null);
      switch (CommandLineOptions.Clo.PrintProverWarnings) {
        case CommandLineOptions.ProverWarnings.None:
          break;
        case CommandLineOptions.ProverWarnings.Stdout:
          Console.WriteLine("Prover warning: " + msg);
          break;
        case CommandLineOptions.ProverWarnings.Stderr:
          Console.Error.WriteLine("Prover warning: " + msg);
          break;
        default:
          Contract.Assume(false);
          throw new cce.UnreachableException();  // unexpected case
      }
    }
  }
}

////////////////////////////////////////////

namespace VC {
  using Bpl = Microsoft.Boogie;

  public class VCGenException : Exception {
    public VCGenException(string s)
      : base(s) {
    }
  }
  [ContractClassFor(typeof(ConditionGeneration))]
  public abstract class ConditionGenerationContracts : ConditionGeneration {
    public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
      Contract.Requires(impl != null);
      Contract.Requires(callback != null);
      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
      throw new NotImplementedException();
    }
    public ConditionGenerationContracts(Program p)
      : base(p) {
    }
  }

  [ContractClass(typeof(ConditionGenerationContracts))]
  public abstract class ConditionGeneration {
    protected internal object CheckerCommonState;

    public enum Outcome {
      Correct,
      Errors,
      TimedOut,
      OutOfMemory,
      Inconclusive,
      ReachedBound
    }

    public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome) {
      switch (outcome) {
        case ProverInterface.Outcome.Invalid:
          return Outcome.Errors;
        case ProverInterface.Outcome.OutOfMemory:
          return Outcome.OutOfMemory;
        case ProverInterface.Outcome.TimeOut:
          return Outcome.TimedOut;
        case ProverInterface.Outcome.Undetermined:
          return Outcome.Inconclusive;
        case ProverInterface.Outcome.Valid:
          return Outcome.Correct;
      }
      return Outcome.Inconclusive;  // unreachable but the stupid compiler does not understand
    }

    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(checkers));
      Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
      Contract.Invariant(program != null);
    }

    public int CumulativeAssertionCount;  // for statistics

    protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
    protected VariableSeq CurrentLocalVariables = null;

    // shared across each implementation; created anew for each implementation
    protected Hashtable /*Variable -> int*/ variable2SequenceNumber;
    public Dictionary<Incarnation, Absy>/*!>!*/ incarnationOriginMap = new Dictionary<Incarnation, Absy>();

    public Program program;
    protected string/*?*/ logFilePath;
    protected bool appendLogFile;

    public static List<Model> errorModelList;

    public ConditionGeneration(Program p) {
      Contract.Requires(p != null);
      program = p;
    }

    /// <summary>
    /// Takes an implementation and constructs a verification condition and sends
    /// it to the theorem prover.
    /// Returns null if "impl" is correct.  Otherwise, returns a list of counterexamples,
    /// each counterexample consisting of an array of labels.
    /// </summary>
    /// <param name="impl"></param>
    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {
      Contract.Requires(impl != null);

      Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));
      Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
      Helpers.ExtraTraceInformation("Starting implementation verification");

      CounterexampleCollector collector = new CounterexampleCollector();
      Outcome outcome = VerifyImplementation(impl, collector);
      if (outcome == Outcome.Errors) {
        errors = collector.examples;
      } else {
        errors = null;
      }

      Helpers.ExtraTraceInformation("Finished implementation verification");
      return outcome;
    }

    /// <summary>
    /// Takes an implementation and constructs a verification condition and sends
    /// it to the theorem prover.
    /// Returns null if "impl" is correct.  Otherwise, returns a list of counterexamples,
    /// each counterexample consisting of an array of labels.
    /// </summary>
    /// <param name="impl"></param>
    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample> errors, out List<Model> errorsModel)
    {
        Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);
        Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
        List<Counterexample> errorsOut;

        Outcome outcome;
        errorModelList = new List<Model>();
        outcome = VerifyImplementation(impl, out errorsOut);
        errors = errorsOut;
        errorsModel = errorModelList;

        return outcome;
    }

    public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback);

    /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////

    #region Methods for injecting pre- and postconditions
    private static void
      ThreadInCodeExpr(Implementation impl,
                       Block targetBlock,
                       CodeExpr codeExpr,
                       bool replaceWithAssert,
                       TokenTextWriter debugWriter) {
      Contract.Requires(impl != null);
      Contract.Requires(codeExpr != null);
      Contract.Requires(targetBlock != null);
      // Go through codeExpr and for all blocks that have a "return e"
      // as their transfer command:
      //   Replace all "return e" with "assert/assume e"
      //   Change the transfer command to "goto targetBlock"
      // Then add all of the blocks in codeExpr to the implementation (at the end)
      foreach (Block b in codeExpr.Blocks) {
        Contract.Assert(b != null);
        ReturnExprCmd rec = b.TransferCmd as ReturnExprCmd;
        if (rec != null) { // otherwise it is a goto command
          if (replaceWithAssert) {
            Ensures ens = new Ensures(rec.tok, false, rec.Expr, null);
            Contract.Assert(ens != null);
            Cmd c = new AssertEnsuresCmd(ens);
            Contract.Assert(c != null);
            b.Cmds.Add(c);
          } else {
            b.Cmds.Add(new AssumeCmd(rec.tok, rec.Expr));
          }
          b.TransferCmd = new GotoCmd(Token.NoToken,
            new StringSeq(targetBlock.Label),
            new BlockSeq(targetBlock));
          targetBlock.Predecessors.Add(b);
        }
        impl.Blocks.Add(b);
      }
      if (debugWriter != null) {
        codeExpr.Emit(debugWriter, 1, false);
      }
      return;
    }

    private static void AddAsPrefix(Block b, CmdSeq cs) {
      Contract.Requires(b != null);
      Contract.Requires(cs != null);
      CmdSeq newCommands = new CmdSeq();
      newCommands.AddRange(cs);
      newCommands.AddRange(b.Cmds);
      b.Cmds = newCommands;
    }


    /// <summary>
    /// Modifies an implementation by prepending it with startCmds and then, as assume
    /// statements, all preconditions.  Insert new blocks as needed, and adjust impl.Blocks[0]
    /// accordingly to make it the new implementation entry block.
    /// </summary>
    /// <param name="impl"></param>
    /// <param name="startCmds"></param>
    protected static void InjectPreconditions(Implementation impl, [Captured] CmdSeq startCmds) {
      Contract.Requires(impl != null);
      Contract.Requires(startCmds != null);
      Contract.Requires(impl.Proc != null);

      TokenTextWriter debugWriter = null;
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        debugWriter = new TokenTextWriter("<console>", Console.Out, false);
        debugWriter.WriteLine("Effective precondition:");
      }

      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
      string blockLabel = "PreconditionGeneratedEntry";

      Block origStartBlock = impl.Blocks[0];
      Block insertionPoint = new Block(
        new Token(-17, -4), blockLabel, startCmds,
        new GotoCmd(Token.NoToken, new StringSeq(origStartBlock.Label), new BlockSeq(origStartBlock)));

      impl.Blocks[0] = insertionPoint;  // make insertionPoint the start block
      impl.Blocks.Add(origStartBlock);  // and put the previous start block at the end of the list

      // (free and checked) requires clauses
      foreach (Requires req in impl.Proc.Requires)
      // invariant:  insertionPoint.TransferCmd is "goto origStartBlock;", but origStartBlock.Predecessors has not yet been updated
      {
        Contract.Assert(req != null);
        Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
        Cmd c = new AssumeCmd(req.tok, e);
        insertionPoint.Cmds.Add(c);
        if (debugWriter != null) {
          c.Emit(debugWriter, 1);
        }
      }
      origStartBlock.Predecessors.Add(insertionPoint);

      if (debugWriter != null) {
        debugWriter.WriteLine();
      }
    }
    /// <summary>
    /// Modifies an implementation by inserting all postconditions
    /// as assert statements at the end of the implementation
    /// Returns the possibly-new unified exit block of the implementation
    /// </summary>
    /// <param name="impl"></param>
    /// <param name="unifiedExitblock">The unified exit block that has
    /// already been constructed for the implementation (and so
    /// is already an element of impl.Blocks)
    /// </param>
    protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) {
      Contract.Requires(impl != null);
      Contract.Requires(unifiedExitBlock != null);
      Contract.Requires(gotoCmdOrigins != null);
      Contract.Requires(impl.Proc != null);
      Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd);
      Contract.Ensures(Contract.Result<Block>() != null);
      Contract.Ensures(Contract.Result<Block>().TransferCmd is ReturnCmd);

      TokenTextWriter debugWriter = null;
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        debugWriter = new TokenTextWriter("<console>", Console.Out, false);
        debugWriter.WriteLine("Effective postcondition:");
      }

      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
      Block insertionPoint = unifiedExitBlock;
      string LabelPrefix = "ReallyLastGeneratedExit";
      int k = 0;

      // (free and checked) ensures clauses
      foreach (Ensures ens in impl.Proc.Ensures) {
        cce.LoopInvariant(insertionPoint.TransferCmd is ReturnCmd);

        Contract.Assert(ens != null);
        if (!ens.Free) { // skip free ensures clauses
          Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
          CodeExpr be = ens.Condition as CodeExpr;
          if (be == null) {
            // This is the normal case, where the postcondition is an ordinary expression
            Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
            ensCopy.Condition = e;
            AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy);
            c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
            insertionPoint.Cmds.Add(c);
            if (debugWriter != null) {
              c.Emit(debugWriter, 1);
            }
          } else {
            // This is a CodeExpr, so append all of its blocks (changing return expressions
            // to assert statements), insert a goto to its head block from the current insertion
            // point, and create a new empty block as the current insertion point.
            // Here goes:  First, create the new block, which will become the new insertion
            // point and which will serve as a target for the CodeExpr.  Steal the TransferCmd
            // from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.
            Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
            k++;
            // Second, append the CodeExpr blocks to the implementation's blocks
            ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);
            // Third, make the old insertion-point block goto the entry block of the CodeExpr
            Block beEntry = cce.NonNull(be.Blocks[0]);
            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));
            beEntry.Predecessors.Add(insertionPoint);
            // Fourth, update the insertion point
            insertionPoint = nextIP;
          }
        }
      }

      if (debugWriter != null) {
        debugWriter.WriteLine();
      }
      return insertionPoint;
    }


    /// <summary>
    /// Get the pre-condition of an implementation, including the where clauses from the in-parameters.
    /// </summary>
    /// <param name="impl"></param>
    protected static CmdSeq GetPre(Implementation impl) {
      Contract.Requires(impl != null);
      Contract.Requires(impl.Proc != null);
      Contract.Ensures(Contract.Result<CmdSeq>() != null);


      TokenTextWriter debugWriter = null;
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        debugWriter = new TokenTextWriter("<console>", Console.Out, false);
        debugWriter.WriteLine("Effective precondition:");
      }

      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
      CmdSeq pre = new CmdSeq();

      // (free and checked) requires clauses
      foreach (Requires req in impl.Proc.Requires) {
        Contract.Assert(req != null);
        Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
        Contract.Assert(e != null);
        Cmd c = new AssumeCmd(req.tok, e);
        Contract.Assert(c != null);
        pre.Add(c);

        if (debugWriter != null) {
          c.Emit(debugWriter, 1);
        }
      }

      if (debugWriter != null) {
        debugWriter.WriteLine();
      }

      return pre;
    }

    /// <summary>
    /// Get the post-condition of an implementation.
    /// </summary>
    /// <param name="impl"></param>
    protected static CmdSeq GetPost(Implementation impl) {


      Contract.Requires(impl != null);
      Contract.Requires(impl.Proc != null);
      Contract.Ensures(Contract.Result<CmdSeq>() != null);
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        Console.WriteLine("Effective postcondition:");
      }

      // Construct an Expr for the post-condition
      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
      CmdSeq post = new CmdSeq();
      foreach (Ensures ens in impl.Proc.Ensures) {
        Contract.Assert(ens != null);
        if (!ens.Free) {
          Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
          Contract.Assert(e != null);
          Ensures ensCopy = cce.NonNull((Ensures)ens.Clone());
          ensCopy.Condition = e;
          Cmd c = new AssertEnsuresCmd(ensCopy);
          ((AssertEnsuresCmd)c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
          post.Add(c);

          if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
            c.Emit(new TokenTextWriter("<console>", Console.Out, false), 1);
          }
        }
      }

      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        Console.WriteLine();
      }

      return post;
    }

    /// <summary>
    /// Get the where clauses from the in- and out-parameters as
    /// a sequence of assume commands.
    /// As a side effect, this method adds these where clauses to the out parameters.
    /// </summary>
    /// <param name="impl"></param>
    protected static CmdSeq GetParamWhereClauses(Implementation impl) {
      Contract.Requires(impl != null);
      Contract.Requires(impl.Proc != null);
      Contract.Ensures(Contract.Result<CmdSeq>() != null);
      TokenTextWriter debugWriter = null;
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        debugWriter = new TokenTextWriter("<console>", Console.Out, false);
        debugWriter.WriteLine("Effective precondition from where-clauses:");
      }

      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
      CmdSeq whereClauses = new CmdSeq();

      // where clauses of in-parameters
      foreach (Formal f in impl.Proc.InParams) {
        Contract.Assert(f != null);
        if (f.TypedIdent.WhereExpr != null) {
          Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr);
          Cmd c = new AssumeCmd(f.tok, e);
          whereClauses.Add(c);

          if (debugWriter != null) {
            c.Emit(debugWriter, 1);
          }
        }
      }

      // where clauses of out-parameters
      Contract.Assert(impl.OutParams.Length == impl.Proc.OutParams.Length);
      for (int i = 0; i < impl.OutParams.Length; i++) {
        Variable f = cce.NonNull(impl.Proc.OutParams[i]);
        if (f.TypedIdent.WhereExpr != null) {
          Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr);
          Cmd c = new AssumeCmd(f.tok, e);
          whereClauses.Add(c);

          Variable fi = cce.NonNull(impl.OutParams[i]);
          Contract.Assume(fi.TypedIdent.WhereExpr == null);
          fi.TypedIdent.WhereExpr = e;

          if (debugWriter != null) {
            c.Emit(debugWriter, 1);
          }
        }
      }

      if (debugWriter != null) {
        debugWriter.WriteLine();
      }

      return whereClauses;
    }

    protected static void RestoreParamWhereClauses(Implementation impl) {
      Contract.Requires(impl != null);
      // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation
      foreach (Formal f in impl.OutParams) {
        Contract.Assert(f != null);
        f.TypedIdent.WhereExpr = null;
      }
    }
    #endregion


    protected Checker FindCheckerFor(Implementation impl, int timeout) {
      Contract.Ensures(Contract.Result<Checker>() != null);

      int i = 0;
      while (i < checkers.Count) {
        if (checkers[i].Closed) {
          checkers.RemoveAt(i);
          continue;
        } else {
          if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))
            return checkers[i];
        }
        ++i;
      }
      string log = logFilePath;
      if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
        log = log + "." + checkers.Count;
      Checker ch = new Checker(this, program, log, appendLogFile, timeout);
      Contract.Assert(ch != null);
      checkers.Add(ch);
      return ch;
    }


    virtual public void Close() {
      foreach (Checker checker in checkers) {
        Contract.Assert(checker != null);
        checker.Close();
      }
    }


    public class CounterexampleCollector : VerifierCallback {
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(cce.NonNullElements(examples));
      }

      public readonly List<Counterexample>/*!>!*/ examples = new List<Counterexample>();
      public override void OnCounterexample(Counterexample ce, string/*?*/ reason) {
        //Contract.Requires(ce != null);
        examples.Add(ce);
      }

      public override void OnUnreachableCode(Implementation impl) {
        //Contract.Requires(impl != null);
        System.Console.WriteLine("found unreachable code:");
        EmitImpl(impl, false);
        // TODO report error about next to last in seq
      }
    }

    protected static void EmitImpl(Implementation impl, bool printDesugarings) {
      Contract.Requires(impl != null);
      int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
      CommandLineOptions.Clo.PrintUnstructured = 2;  // print only the unstructured program
      bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;
      CommandLineOptions.Clo.PrintDesugarings = printDesugarings;
      impl.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
      CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
      CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
    }


    protected Block GenerateUnifiedExit(Implementation impl, Hashtable gotoCmdOrigins) {
      Contract.Requires(impl != null);
      Contract.Requires(gotoCmdOrigins != null);
      Contract.Ensures(Contract.Result<Block>() != null);

      Contract.Ensures(Contract.Result<Block>().TransferCmd is ReturnCmd);
      Block/*?*/ exitBlock = null;
      #region Create a unified exit block, if there's more than one
      {
        int returnBlocks = 0;
        foreach (Block b in impl.Blocks) {
          if (b.TransferCmd is ReturnCmd) {
            exitBlock = b;
            returnBlocks++;
          }
        }
        if (returnBlocks > 1) {
          string unifiedExitLabel = "GeneratedUnifiedExit";
          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new CmdSeq(), new ReturnCmd(Token.NoToken));
          Contract.Assert(unifiedExit != null);
          foreach (Block b in impl.Blocks) {
            if (b.TransferCmd is ReturnCmd) {
              StringSeq labels = new StringSeq();
              labels.Add(unifiedExitLabel);
              BlockSeq bs = new BlockSeq();
              bs.Add(unifiedExit);
              GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);
              gotoCmdOrigins[go] = b.TransferCmd;
              b.TransferCmd = go;
              unifiedExit.Predecessors.Add(b);
            }
          }

          exitBlock = unifiedExit;
          impl.Blocks.Add(unifiedExit);
        }
        Contract.Assert(exitBlock != null);
      }
      return exitBlock;
      #endregion
    }

    protected static void ResetPredecessors(List<Block> blocks) {
      Contract.Requires(blocks != null);
      foreach (Block b in blocks) {
        Contract.Assert(b != null);
        b.Predecessors = new BlockSeq();
      }
      foreach (Block b in blocks) {
        Contract.Assert(b != null);
        foreach (Block ch in Exits(b)) {
          Contract.Assert(ch != null);
          ch.Predecessors.Add(b);
        }
      }
    }

    protected static IEnumerable Exits(Block b) {
      Contract.Requires(b != null);
      GotoCmd g = b.TransferCmd as GotoCmd;
      if (g != null) {
        return cce.NonNull(g.labelTargets);
      }
      return new List<Block>();
    }

    protected Variable CreateIncarnation(Variable x, Absy a) {
      Contract.Requires(this.variable2SequenceNumber != null);
      Contract.Requires(this.CurrentLocalVariables != null);
      Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd);

      Contract.Requires(x != null);
      Contract.Ensures(Contract.Result<Variable>() != null);

      int currentIncarnationNumber =
        variable2SequenceNumber.ContainsKey(x)
        ?
        (int)cce.NonNull(variable2SequenceNumber[x])
        :
        -1;
      Variable v = new Incarnation(x, currentIncarnationNumber + 1);
      variable2SequenceNumber[x] = currentIncarnationNumber + 1;
      CurrentLocalVariables.Add(v);
      incarnationOriginMap.Add((Incarnation)v, a);
      return v;
    }

    /// <summary>
    /// Compute the incarnation map at the beginning of block "b" from the incarnation blocks of the
    /// predecessors of "b".
    ///
    /// The predecessor map b.map for block "b" is defined as follows:
    ///   b.map.Domain == Union{Block p in b.predecessors; p.map.Domain}
    ///   Forall{Variable v in b.map.Domain;
    ///              b.map[v] == (v in Intersection{Block p in b.predecessors; p.map}.Domain
    ///                           ?  b.predecessors[0].map[v]
    ///                           :  new Variable())}
    /// Every variable that b.map maps to a fresh variable requires a fixup in all predecessor blocks.
    /// </summary>
    /// <param name="b"></param>
    /// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>
    /// <returns></returns>
    protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) {
      Contract.Requires(b != null);
      Contract.Requires(block2Incarnation != null);
      Contract.Ensures(Contract.Result<Hashtable>() != null);

      if (b.Predecessors.Length == 0) {
        return new Hashtable();
      }

      Hashtable /*Variable -> Expr*/ incarnationMap = null;
      Set /*Variable*/ fixUps = new Set /*Variable*/ ();
      foreach (Block pred in b.Predecessors) {
        Contract.Assert(pred != null);
        Contract.Assert(block2Incarnation.Contains(pred));  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet
        Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)block2Incarnation[pred];
        Contract.Assert(predMap != null);
        if (incarnationMap == null) {
          incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();
          continue;
        }

        ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();
        foreach (Variable v in incarnationMap.Keys) {
          Contract.Assert(v != null);
          if (!predMap.Contains(v)) {
            // conflict!!
            conflicts.Add(v);
            fixUps.Add(v);
          }
        }
        // Now that we're done with enumeration, we'll do all the removes
        foreach (Variable v in conflicts) {
          Contract.Assert(v != null);
          incarnationMap.Remove(v);
        }
        foreach (Variable v in predMap.Keys) {
          Contract.Assert(v != null);
          if (!incarnationMap.Contains(v)) {
            // v was not in the domain of the predecessors seen so far, so it needs to be fixed up
            fixUps.Add(v);
          } else {
            // v in incarnationMap ==> all pred blocks (up to now) all agree on its incarnation
            if (predMap[v] != incarnationMap[v]) {
              // conflict!!
              incarnationMap.Remove(v);
              fixUps.Add(v);
            }
          }
        }
      }

      #region Second, for all variables in the fixups list, introduce a new incarnation and push it back into the preds.
      foreach (Variable v in fixUps) {
        Contract.Assert(v != null);
        if (!b.IsLive(v))
          continue;
        Variable v_prime = CreateIncarnation(v, b);
        IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime);
        Contract.Assert(incarnationMap != null);
        incarnationMap[v] = ie;
        foreach (Block pred in b.Predecessors) {
          Contract.Assert(pred != null);
          #region Create an assume command equating v_prime with its last incarnation in pred
          #region Create an identifier expression for the last incarnation in pred
          Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);

          Expr pred_incarnation_exp;
          Expr o = (Expr)predMap[v];
          if (o == null) {
            Variable predIncarnation = v;
            IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation);
            pred_incarnation_exp = ie2;
          } else {
            pred_incarnation_exp = o;
          }
          #endregion
          #region Create an identifier expression for the new incarnation
          IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);
          #endregion
          #region Create the assume command itself
          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp));
          pred.Cmds.Add(ac);
          #endregion
          #endregion
        }
      }
      #endregion

      Contract.Assert(incarnationMap != null);
      return incarnationMap;
    }

    Hashtable preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

    protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {
      Contract.Requires(b != null);
      Contract.Requires(incarnationMap != null);
      Contract.Requires(mvInfo != null);
      Contract.Requires(oldFrameSubst != null);
      #region Walk forward over the commands in this block and convert them to passive commands

      CmdSeq passiveCmds = new CmdSeq();
      foreach (Cmd c in b.Cmds) {
        Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction
        TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
      }
      b.Cmds = passiveCmds;

      if (b.TransferCmd is ReturnExprCmd) {
        ReturnExprCmd rec = (ReturnExprCmd)b.TransferCmd.Clone();
        Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
        rec.Expr = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, rec.Expr);
        b.TransferCmd = rec;
      }
      #endregion
    }

    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {
      Contract.Requires(impl != null);
      Contract.Requires(mvInfo != null);

      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

      RestoreParamWhereClauses(impl);

      #region Debug Tracing
      if (CommandLineOptions.Clo.TraceVerify) {
        Console.WriteLine("after conversion to passive commands");
        EmitImpl(impl, true);
      }
      #endregion

      return r;
    }

    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {
      Contract.Requires(blocks != null);
      Contract.Requires(modifies != null);
      Contract.Requires(mvInfo != null);
      #region Convert to Passive Commands

      #region Topological sort -- need to process in a linearization of the partial order
      Graph<Block> dag = new Graph<Block>();
      dag.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
      foreach (Block b in 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(b, dest);
          }
        }
      }
      IEnumerable sortedNodes = dag.TopologicalSort();
      Contract.Assert(sortedNodes != null);
      #endregion

      Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies);

      // Now we can process the nodes in an order so that we're guaranteed to have
      // processed all of a node's predecessors before we process the node.
      Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();
      Block exitBlock = null;
      Hashtable exitIncarnationMap = null;
      foreach (Block b in sortedNodes) {
        Contract.Assert(b != null);
        Contract.Assert(!block2Incarnation.Contains(b));
        Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

        // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.
        b.liveVarsBefore = null;

        // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, 
        // all its successors have been passified.  Consequently, its entry in block2Incarnation can be removed.
        foreach (Block p in b.Predecessors) {
          p.succCount--;
          if (p.succCount == 0)
            block2Incarnation.Remove(p);
        }

        #region Each block's map needs to be available to successor blocks
        GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
        if (gotoCmd == null) {
          b.succCount = 0;
        }
        else {
          // incarnationMap needs to be added only if there is some successor of b
          b.succCount = gotoCmd.labelNames.Length;
          block2Incarnation.Add(b, incarnationMap);
        }
        #endregion Each block's map needs to be available to successor blocks

        TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst);
        exitBlock = b;
        exitIncarnationMap = incarnationMap;
      }

      // Verify that exitBlock is indeed the unique exit block
      Contract.Assert(exitBlock != null);
      Contract.Assert(exitBlock.TransferCmd is ReturnCmd);
      #endregion Convert to Passive Commands

      return exitIncarnationMap;
    }

    /// <summary>
    /// Compute the substitution for old expressions.
    /// </summary>
    protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)
    {
      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
      foreach (IdentifierExpr ie in modifies)
      {
        Contract.Assert(ie != null);
        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))
          oldFrameMap.Add(ie.Decl, ie);
      }
      return Substituter.SubstitutionFromHashtable(oldFrameMap);
    }

    /// <summary>
    /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc
    /// Meanwhile, record any information needed to later reconstruct a model view.
    /// </summary>
    protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {
      Contract.Requires(c != null);
      Contract.Requires(incarnationMap != null);
      Contract.Requires(oldFrameSubst != null);
      Contract.Requires(passiveCmds != null);
      Contract.Requires(mvInfo != null);
      Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
      #region assert/assume P |--> assert/assume P[x := in(x)], out := in
      if (c is PredicateCmd) {
        Contract.Assert(c is AssertCmd || c is AssumeCmd);  // otherwise, unexpected PredicateCmd type

        PredicateCmd pc = (PredicateCmd)c.Clone();
        Contract.Assert(pc != null);

        Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
        if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
          string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
          if (description != null) {
            Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));
            copy = Bpl.Expr.And(mv, copy);
            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));
          }
        }
        Contract.Assert(copy != null);
        if (pc is AssertCmd) {
          ((AssertCmd)pc).OrigExpr = pc.Expr;
          Contract.Assert(((AssertCmd)pc).IncarnationMap == null);
          ((AssertCmd)pc).IncarnationMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(incarnationMap.Clone());
        }
        pc.Expr = copy;
        passiveCmds.Add(pc);
      }
      #endregion
      #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
 else if (c is AssignCmd) {
        AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments
        Contract.Assert(assign != null);
        #region Substitute all variables in E with the current map
        List<Expr> copies = new List<Expr>();
        foreach (Expr e in assign.Rhss) {
          Contract.Assert(e != null);
          copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst,
                                                        oldFrameSubst,
                                                        e));
        }
        #endregion

        List<Expr/*!>!*/> assumptions = new List<Expr>();
        // it might be too slow to create a new dictionary each time ...
        IDictionary<Variable, Expr> newIncarnationMappings =
          new Dictionary<Variable, Expr>();

        for (int i = 0; i < assign.Lhss.Count; ++i) {
          IdentifierExpr lhsIdExpr =
            cce.NonNull((SimpleAssignLhs)assign.Lhss[i]).AssignedVariable;
          Variable lhs = cce.NonNull(lhsIdExpr.Decl);
          Contract.Assert(lhs != null);
          Expr rhs = assign.Rhss[i];
          Contract.Assert(rhs != null);

          // don't create incarnations for assignments of literals or single variables.
          if (rhs is LiteralExpr) {
            incarnationMap[lhs] = rhs;
          } else if (rhs is IdentifierExpr) {
            IdentifierExpr ie = (IdentifierExpr)rhs;
            if (incarnationMap.ContainsKey(cce.NonNull(ie.Decl)))
              newIncarnationMappings[lhs] = cce.NonNull((Expr)incarnationMap[ie.Decl]);
            else
              newIncarnationMappings[lhs] = ie;
          } else {
            IdentifierExpr x_prime_exp = null;
            #region Make a new incarnation, x', for variable x, but only if x is *not* already an incarnation
            if (lhs is Incarnation) {
              // incarnations are already written only once, no need to make an incarnation of an incarnation
              x_prime_exp = lhsIdExpr;
            } else {
              Variable v = CreateIncarnation(lhs, c);
              x_prime_exp = new IdentifierExpr(lhsIdExpr.tok, v);
              newIncarnationMappings[lhs] = x_prime_exp;
            }
            #endregion
            #region Create an assume command with the new variable
            assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
            #endregion
          }
        }

        foreach (KeyValuePair<Variable, Expr> pair in newIncarnationMappings) {
          Contract.Assert(pair.Key != null && pair.Value != null);
          incarnationMap[pair.Key] = pair.Value;
        }

        if (assumptions.Count > 0) {
          Expr assumption = assumptions[0];

          for (int i = 1; i < assumptions.Count; ++i) {
            Contract.Assert(assumption != null);
            assumption = Expr.And(assumption, assumptions[i]);
          }
          passiveCmds.Add(new AssumeCmd(c.tok, assumption));
        }
      }
      #endregion
      #region havoc w |--> assume whereClauses, out := in( w |-> w' )
 else if (c is HavocCmd) {
        if (this.preHavocIncarnationMap == null)      // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
          this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();

        HavocCmd hc = (HavocCmd)c;
        Contract.Assert(c != null);
        IdentifierExprSeq havocVars = hc.Vars;
        // First, compute the new incarnations
        foreach (IdentifierExpr ie in havocVars) {
          Contract.Assert(ie != null);
          if (!(ie.Decl is Incarnation)) {
            Variable x = cce.NonNull(ie.Decl);
            Variable x_prime = CreateIncarnation(x, c);
            incarnationMap[x] = new IdentifierExpr(x_prime.tok, x_prime);
          }
        }
        // Then, perform the assume of the where clauses, using the updated incarnations
        Substitution updatedIncarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
        foreach (IdentifierExpr ie in havocVars) {
          Contract.Assert(ie != null);
          if (!(ie.Decl is Incarnation)) {
            Variable x = cce.NonNull(ie.Decl);
            Bpl.Expr w = x.TypedIdent.WhereExpr;
            if (w != null) {
              Expr copy = Substituter.ApplyReplacingOldExprs(updatedIncarnationSubst, oldFrameSubst, w);
              passiveCmds.Add(new AssumeCmd(c.tok, copy));
            }
          }
        }
      }
      #endregion
 else if (c is CommentCmd) {
        // comments are just for debugging and don't affect verification
      } else if (c is SugaredCmd) {
        SugaredCmd sug = (SugaredCmd)c;
        Contract.Assert(sug != null);
        Cmd cmd = sug.Desugaring;
        Contract.Assert(cmd != null);
        TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
      } else if (c is StateCmd) {
        this.preHavocIncarnationMap = null;       // we do not need to remeber the previous incarnations
        StateCmd st = (StateCmd)c;
        Contract.Assert(st != null);
        // account for any where clauses among the local variables
        foreach (Variable v in st.Locals) {
          Contract.Assert(v != null);
          Expr w = v.TypedIdent.WhereExpr;
          if (w != null) {
            passiveCmds.Add(new AssumeCmd(v.tok, w));
          }
        }
        // do the sub-commands
        foreach (Cmd s in st.Cmds) {
          Contract.Assert(s != null);
          TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
        }
        // remove the local variables from the incarnation map
        foreach (Variable v in st.Locals) {
          Contract.Assert(v != null);
          incarnationMap.Remove(v);
        }
      }
      #region There shouldn't be any other types of commands at this point
 else {
        Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");
      }
      #endregion


      #region We remember if we have put an havoc statement into a passive form

      if (!(c is HavocCmd))
        this.preHavocIncarnationMap = null;
      // else: it has already been set by the case for the HavocCmd
      #endregion
    }

    NAryExpr TypedExprEq(Expr e0, Expr e1) {
      Contract.Requires(e0 != null);
      Contract.Requires(e1 != null);
      NAryExpr e = Expr.Eq(e0, e1);
      e.Type = Bpl.Type.Bool;
      e.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
      return e;
    }

    /// <summary>
    /// Creates a new block to add to impl.Blocks, where impl is the implementation that contains
    /// succ.  Caller must do the add to impl.Blocks.
    /// </summary>
    protected Block CreateBlockBetween(int predIndex, Block succ) {
      Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Length);


      Contract.Requires(succ != null);
      Contract.Ensures(Contract.Result<Block>() != null);

      Block pred = cce.NonNull(succ.Predecessors[predIndex]);

      string newBlockLabel = pred.Label + "_@2_" + succ.Label;

      // successor of newBlock list
      StringSeq ls = new StringSeq();
      ls.Add(succ.Label);
      BlockSeq bs = new BlockSeq();
      bs.Add(succ);

      Block newBlock = new Block(
          new Token(-17, -4),
          newBlockLabel,
          new CmdSeq(),
          new GotoCmd(Token.NoToken, ls, bs)
          );

      // predecessors of newBlock
      BlockSeq ps = new BlockSeq();
      ps.Add(pred);
      newBlock.Predecessors = ps;

      // fix successors of pred
      #region Change the edge "pred->succ" to "pred->newBlock"
      GotoCmd gtc = (GotoCmd)cce.NonNull(pred.TransferCmd);
      Contract.Assume(gtc.labelTargets != null);
      Contract.Assume(gtc.labelNames != null);
      for (int i = 0, n = gtc.labelTargets.Length; i < n; i++) {
        if (gtc.labelTargets[i] == succ) {
          gtc.labelTargets[i] = newBlock;
          gtc.labelNames[i] = newBlockLabel;
          break;
        }
      }
      #endregion Change the edge "pred->succ" to "pred->newBlock"

      // fix predecessors of succ
      succ.Predecessors[predIndex] = newBlock;

      return newBlock;
    }

    protected void AddBlocksBetween(List<Block> blocks) {
      Contract.Requires(blocks != null);
      #region Introduce empty blocks between join points and their multi-successor predecessors
      List<Block> tweens = new List<Block>();
      foreach (Block b in blocks) {
        int nPreds = b.Predecessors.Length;
        if (nPreds > 1) {
          // b is a join point (i.e., it has more than one predecessor)
          for (int i = 0; i < nPreds; i++) {
            GotoCmd gotocmd = (GotoCmd)(cce.NonNull(b.Predecessors[i]).TransferCmd);
            if (gotocmd.labelNames != null && gotocmd.labelNames.Length > 1) {
              tweens.Add(CreateBlockBetween(i, b));
            }
          }
        }
      }
      blocks.AddRange(tweens);  // must wait until iteration is done before changing the list
      #endregion
    }

  }

  public class ModelViewInfo
  {
    public readonly List<Variable> AllVariables = new List<Variable>();
    public readonly List<Mapping> CapturePoints = new List<Mapping>();
    public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "@MV_state",
      new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),
                      new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),
      new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));
    public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));

    public ModelViewInfo(Program program, Implementation impl) {
      Contract.Requires(program != null);
      Contract.Requires(impl != null);

      // global variables
      foreach (Declaration d in program.TopLevelDeclarations) {
        if (d is Constant) continue;
        if (d is Variable) {
          AllVariables.Add((Variable)d);
        }
      }
      // implementation parameters
      foreach (Variable p in impl.InParams) {
        AllVariables.Add(p);
      }
      foreach (Variable p in impl.OutParams) {
        AllVariables.Add(p);
      }
      // implementation locals
      foreach (Variable v in impl.LocVars) {
        AllVariables.Add(v);
      }
    }

    public ModelViewInfo(CodeExpr codeExpr) {
      Contract.Requires(codeExpr != null);
      // TODO: also need all variables of enclosing scopes (the global variables of the program, the parameters
      // and perhaps locals of the implementation (if any), any enclosing code expressions).

      foreach (Variable v in codeExpr.LocVars) {
        AllVariables.Add(v);
      }
    }

    public class Mapping
    {
      public readonly string Description;
      public readonly Hashtable /*Variable -> Expr*/ IncarnationMap;
      public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) {
        Description = description;
        IncarnationMap = incarnationMap;
      }
    }
  }
}