//-----------------------------------------------------------------------------
//
// 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 Microsoft.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;

namespace Microsoft.Boogie
{
  public abstract class Counterexample 
  {
    [Peer] public BlockSeq! Trace;
    [Peer] public List<string!>! relatedInformation;
    
    internal Counterexample(BlockSeq! trace)
    {
      this.Trace = trace;
      this.relatedInformation = new List<string!>();
      // base();
    }
    
    public abstract int GetLocation();
  }

  public class CounterexampleComparer : IComparer<Counterexample!>
  {
    public int Compare(Counterexample! c1, Counterexample! c2) {
      if (c1.GetLocation() == c2.GetLocation()) return 0;
      if (c1.GetLocation() > c2.GetLocation()) return 1;
      return -1;
    }
  }
    
  public class AssertCounterexample : Counterexample
  {
    [Peer] public AssertCmd! FailingAssert;
    
    public AssertCounterexample(BlockSeq! trace, AssertCmd! failingAssert)
      : base(trace)
    {
      this.FailingAssert = failingAssert;
      // base(trace);
    }
    
    public override int GetLocation() {
      return FailingAssert.tok.line * 1000 + FailingAssert.tok.col;
    }
  }
  
  public class CallCounterexample : Counterexample
  {
    public CallCmd! FailingCall;
    public Requires! FailingRequires;
    
    public CallCounterexample(BlockSeq! trace, CallCmd! failingCall, Requires! failingRequires)
      : base(trace)
      requires !failingRequires.Free;
    {
      this.FailingCall = failingCall;
      this.FailingRequires = failingRequires;
      // base(trace);
    }

    public override int GetLocation() {
      return FailingCall.tok.line * 1000 + FailingCall.tok.col;
    }
  }
  
  public class ReturnCounterexample : Counterexample
  {
    public TransferCmd! FailingReturn;
    public Ensures! FailingEnsures;
    
    public ReturnCounterexample(BlockSeq! trace, TransferCmd! failingReturn, Ensures! failingEnsures)
      : base(trace)
      requires !failingEnsures.Free;
    {
      this.FailingReturn = failingReturn;
      this.FailingEnsures = failingEnsures;
      // base(trace);
    }

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

  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)
    {
    }

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

    public virtual void OnOutOfMemory(string! reason)
    {
    }

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

    public virtual void OnUnreachableCode(Implementation! impl)
    {
    }
    
    public virtual void OnWarning(string! msg) 
    {
      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:
          assume false;  // unexpected case
      }
    }
  }
}

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

namespace VC
{
  using Bpl = Microsoft.Boogie;

  public class VCGenException : Exception 
  {
    public VCGenException(string s) : base(s)
    {
    }
  }

  public abstract class ConditionGeneration
  {
    protected internal object CheckerCommonState;

    public enum Outcome { Correct, Errors, TimedOut, OutOfMemory, Inconclusive }
 
    protected readonly List<Checker!>! provers = new List<Checker!>();
    protected Implementation current_impl = null;


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

    // used only by FindCheckerFor
    protected Program! program;
    protected string/*?*/ logFilePath;
    protected bool appendLogFile;
    
    public ConditionGeneration(Program! p)
    {
      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, Program! program, out List<Counterexample!>? errors)
      ensures result == Outcome.Errors ==> errors != null;
      throws UnexpectedProverOutputException;
    {
      Helpers.ExtraTraceInformation("Starting implementation verification");

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

      Helpers.ExtraTraceInformation("Finished implementation verification");
      return outcome;
    }
  
    public abstract Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
        throws UnexpectedProverOutputException;
        

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

#region Methods for injecting pre- and postconditions
    private static void
      ThreadInBlockExpr(Implementation! impl,
                        Block! targetBlock,
                        BlockExpr! blockExpr,
                        bool replaceWithAssert,
                        TokenTextWriter debugWriter){
      // Go through blockExpr 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 blockExpr to the implementation (at the end)
      foreach (Block! b in blockExpr.Blocks){
        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);
            Cmd! c = new AssertEnsuresCmd(ens);
            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){
        blockExpr.Emit(debugWriter, 1,false);
      }
      return;
    }
    
    private static void AddAsPrefix(Block! b, CmdSeq! cs){
      CmdSeq newCommands = new CmdSeq();
      newCommands.AddRange(cs);
      newCommands.AddRange(b.Cmds);
      b.Cmds = newCommands;
    }
      

    /// <summary>
    /// Modifies an implementation by inserting all preconditions
    /// as assume statements at the beginning of the implementation
    /// </summary>
    /// <param name="impl"></param>
    protected static void InjectPreconditions(Implementation! impl)
      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());
      
      Block! originalEntryPoint = (!) impl.Blocks[0];
      Block! currentEntryPoint = (!) impl.Blocks[0];
      CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" preconditions

      // (free and checked) requires clauses
      for (int i = impl.Proc.Requires.Length-1; 0 <= i; i--){
        
        // need to process the preconditions from bottom up, because
        // for any that are BlockExprs, we need to thread them on
        // to the top of the implementation

        Requires req = impl.Proc.Requires[i];
        Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);
        BlockExpr be = req.Condition as BlockExpr;
        if (be != null){
          if (currentClump.Length > 0){
            AddAsPrefix(currentEntryPoint, currentClump);
            currentClump = new CmdSeq();
          }
          ThreadInBlockExpr(impl,currentEntryPoint, be,false,debugWriter);
          currentEntryPoint = (!)be.Blocks[0];
        }else{
          Cmd! c = new AssumeCmd(req.tok, e);
          currentClump.Add(c);
          if (debugWriter != null) { c.Emit(debugWriter, 1); }
        }
        
      }
      
      if (currentClump.Length > 0){
        AddAsPrefix(currentEntryPoint, currentClump);
      }
      
      if (currentEntryPoint != originalEntryPoint){
        string EntryLabel = "PreconditionGeneratedEntry";
        Block! newEntry = new Block(new Token(-17, -4),EntryLabel,new CmdSeq(),
                  new GotoCmd(Token.NoToken,
              new StringSeq(currentEntryPoint.Label),
              new BlockSeq(currentEntryPoint)));
        currentEntryPoint.Predecessors.Add(newEntry);
        List<Block!> newBody = new List<Block!>();
        newBody.Add(newEntry);
        newBody.AddRange(impl.Blocks);
        impl.Blocks = newBody;
      }

      if (debugWriter != null) { debugWriter.WriteLine(); }
      
      return;
    }
    /// <summary>
    /// Modifies an implementation by inserting all postconditions
    /// as assert statements at the end 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 void InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)
      requires impl.Proc != null;
    {
      TokenTextWriter debugWriter = null;
      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
        debugWriter = new TokenTextWriter("<console>", Console.Out, false);
        debugWriter.WriteLine("Effective postcondition:");
      }
      
      string ExitLabel = "ReallyLastGeneratedExit";
      Block! newExit = new Block(new Token(-17, -4),ExitLabel,new CmdSeq(),new ReturnCmd(Token.NoToken));
      impl.Blocks.Add(newExit);
      Block! currentEntryPoint = newExit;
      CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" postconditions

      Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());

      // (free and checked) ensures clauses
      for (int i = impl.Proc.Ensures.Length-1; 0 <= i; i--){
        
        // need to process the postconditions from bottom up, because
        // for any that are BlockExprs, we need to thread them on
        // to the top of the implementation

        Ensures ens = (impl.Proc).Ensures[i];
        if (!ens.Free) { // free ensures aren't needed for verifying the implementation
          Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);
          BlockExpr be = ens.Condition as BlockExpr;
          if (be != null){
            if (currentClump.Length > 0){
              AddAsPrefix(currentEntryPoint, currentClump);
              currentClump = new CmdSeq();
            }
            ThreadInBlockExpr(impl,currentEntryPoint,be,true,debugWriter);
            currentEntryPoint = (!)be.Blocks[0];
          }else{
            Ensures! ensCopy = (Ensures!) ens.Clone();
            ensCopy.Condition = e;
            Cmd! c = new AssertEnsuresCmd(ensCopy);
            ((AssertEnsuresCmd) c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
            currentClump.Add(c);
            if (debugWriter != null) { c.Emit(debugWriter, 1); }
          }
        }
          
      }
      
      if (currentClump.Length > 0){
        AddAsPrefix(currentEntryPoint, currentClump);
      }
      
      GotoCmd gtc = new GotoCmd(Token.NoToken,
            new StringSeq(currentEntryPoint.Label),
            new BlockSeq(currentEntryPoint));
      gotoCmdOrigins[gtc] = unifiedExitBlock.TransferCmd;
      unifiedExitBlock.TransferCmd = gtc;
      currentEntryPoint.Predecessors.Add(unifiedExitBlock);
      
      if (debugWriter != null) { debugWriter.WriteLine(); }
      
      return;
    }


    /// <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)
      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());
      CmdSeq! pre = new CmdSeq();

      // (free and checked) requires clauses
      foreach (Requires! req in impl.Proc.Requires)
      {
        Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);
        Cmd! c = new AssumeCmd(req.tok, e);
        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)
      requires impl.Proc != 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)
      {
        if (!ens.Free) {
          Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);
          Ensures! ensCopy = (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)
      requires impl.Proc != 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)
      {
        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
      assert impl.OutParams.Length == impl.Proc.OutParams.Length;
      for (int i = 0; i < impl.OutParams.Length; i++) {
        Variable f = (!)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 = (!)impl.OutParams[i];
          assume fi.TypedIdent.WhereExpr == null;
          fi.TypedIdent.WhereExpr = e;
        
          if (debugWriter != null) { c.Emit(debugWriter, 1); }
        }
      }

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

#endregion

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

    public void Close() { foreach (Checker! prover in provers) prover.Close(); }


    protected class CounterexampleCollector : VerifierCallback
    {
      public readonly List<Counterexample!>! examples = new List<Counterexample!>();
      public override void OnCounterexample(Counterexample! ce, string? reason)
      {
        examples.Add(ce);
      }

      public override void OnUnreachableCode(Implementation! impl)
      {
        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) {
      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)
    {
      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));
          
          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);
        }
        assert exitBlock != null;
      }
      return exitBlock;
      #endregion    
    }

    /// <summary>
    /// Helperfunction to restore the predecessor relations after loop unrolling
    /// </summary> 
 		protected void ComputePredecessors(List<Block!>! blocks)
		{
				#region Compute and store the Predecessor Relation on the blocks
				// This code just here to try things out.
				// Compute the predecessor relation for each block
				// Store it in the Predecessors field within each block
				foreach (Block b in blocks)
				{
					GotoCmd gtc = b.TransferCmd as GotoCmd;
					if (gtc != null)
					{
						assume gtc.labelTargets != null;
						foreach (Block! dest in gtc.labelTargets)
						{
							dest.Predecessors.Add(b);
						}
					}
				}
				#endregion Compute and store the Predecessor Relation on the blocks	
		}

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

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


    protected Variable! CreateIncarnation(Variable! x, Absy a)
      requires this.variable2SequenceNumber != null;
      requires this.current_impl != null;
      requires a is Block || a is AssignCmd || a is HavocCmd;
    {
      int currentIncarnationNumber =
        variable2SequenceNumber.ContainsKey(x) 
        ?
        (int) ((!)variable2SequenceNumber[x])
        :
        -1;
      Variable v = new Incarnation(x,currentIncarnationNumber + 1);
      variable2SequenceNumber[x] = currentIncarnationNumber + 1;
      Debug.Assert(current_impl != null, "The field current_impl wasn't set.");
      current_impl.LocVars.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)
    {
      if (b.Predecessors.Length == 0)
      {
        return new Hashtable /*Variable -> Expr*/ ();
      }

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

        ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();
        foreach (Variable! v in incarnationMap.Keys)
        {
          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)
        {
          incarnationMap.Remove(v);
        }
        foreach (Variable! v in predMap.Keys)
        {
          if (!incarnationMap.Contains(v))
          {
            // v was not in the domain of the precessors 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 )
      {
        Variable v_prime = CreateIncarnation(v, b);
        IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime);
        assert incarnationMap != null;
        incarnationMap[v] = ie;
        foreach (Block! pred in b.Predecessors )
        {
          #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*/) 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
          Expr e = Expr.Binary(Token.NoToken,
            BinaryOperator.Opcode.Eq,
            v_prime_exp,
            pred_incarnation_exp
            );
          AssumeCmd ac = new AssumeCmd(v.tok,e);
          pred.Cmds.Add(ac);
          #endregion
          #endregion
        }
      }
      #endregion

    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, Substitution! oldFrameSubst)
    {
      #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)
      { // walk forward over the commands because the map gets modified in a forward direction      
          TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds);
      }
      b.Cmds = passiveCmds;

      #endregion
    }


    protected void Convert2PassiveCmd(Implementation! impl)
    {
      #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((!)impl.Blocks[0]); // there is always at least one node in the graph
      foreach (Block b in impl.Blocks)
      {
        GotoCmd gtc = b.TransferCmd as GotoCmd;
        if (gtc != null)
        {
          assume gtc.labelTargets != null;
          foreach (Block! dest in gtc.labelTargets)
          {
            dag.AddEdge(b,dest);
          }
        }
      }
      IEnumerable! sortedNodes = dag.TopologicalSort();
      //Debug.Assert( sortedNodes != null, "Topological Sort returned null." );
      #endregion
      
      // Create substitution for old expressions
      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
      assume impl.Proc != null;
      foreach (IdentifierExpr! ie in impl.Proc.Modifies) {
        if (!oldFrameMap.Contains((!)ie.Decl))
          oldFrameMap.Add(ie.Decl, ie);
      }
      Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);
    
      // 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*/();
      foreach (Block! b in sortedNodes )
      {
        Debug.Assert( !block2Incarnation.Contains(b) );
        Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
        
        #region Each block's map needs to be available to successor blocks
        block2Incarnation.Add(b,incarnationMap);
        #endregion Each block's map needs to be available to successor blocks

        TurnIntoPassiveBlock(b, incarnationMap, oldFrameSubst);
      }
      
      // 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) {
        f.TypedIdent.WhereExpr = null;
      }
      #endregion Convert to Passive Commands

      #region Debug Tracing
      if (CommandLineOptions.Clo.TraceVerify) 
      {
        Console.WriteLine("after conversion to passive commands");
        EmitImpl(impl, true);
      }
      #endregion    
    }
        
    /// <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 remebers the incarnation map BEFORE the havoc
    /// </summary> 
    protected void TurnIntoPassiveCmd(Cmd! c, Hashtable /*Variable -> Expr*/! incarnationMap, Substitution! oldFrameSubst, CmdSeq! passiveCmds)
    {
        Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
        #region assert/assume P |--> assert/assume P[x := in(x)], out := in
        if ( c is PredicateCmd )
        {          
          Debug.Assert( c is AssertCmd || c is AssumeCmd, "Internal Error: Found a PredicateCmd h is not an assert or an assume." );
           
          PredicateCmd! pc = (PredicateCmd) c.Clone();
              
          if(pc is AssumeCmd && pc.Expr is LoopPredicate   // Check if the PredicateCmd is in the form of "assume J", with J loop invariant predicate
              && this.preHavocIncarnationMap != null)      // Furthermore, the command just before was a (list of) havoc statements 
          {
            LoopPredicate! lp = (LoopPredicate!) pc.Expr;
            lp.SetPreAndPostHavocIncarnationMaps(this.preHavocIncarnationMap, (Hashtable /*Variable -> Expr*/!) incarnationMap.Clone());
          }
    
          Expr! copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
          if (pc is AssertCmd) {
            ((AssertCmd) pc).OrigExpr = pc.Expr;
            assert ((AssertCmd) pc).IncarnationMap == null;
            ((AssertCmd) pc).IncarnationMap = (Hashtable /*Variable -> Expr*/!) 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
          #region Substitute all variables in E with the current map
          List<Expr!>! copies = new List<Expr!> ();
          foreach (Expr! e in assign.Rhss)
            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 =
              ((SimpleAssignLhs!)assign.Lhss[i]).AssignedVariable;
            Variable! lhs = (!)lhsIdExpr.Decl;
            Expr! rhs = assign.Rhss[i];

            // 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((!)ie.Decl) )
                newIncarnationMappings[lhs] = (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(Expr.Eq(x_prime_exp, copies[i]));
              #endregion
            }
          }

          foreach (KeyValuePair<Variable!, Expr!> pair in newIncarnationMappings)
            incarnationMap[pair.Key] = pair.Value;

          if (assumptions.Count > 0) {
            Expr! assumption = assumptions[0];
            for (int i = 1; i < assumptions.Count; ++i)
              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;
          IdentifierExprSeq havocVars = hc.Vars;
          // First, compute the new incarnations
          foreach (IdentifierExpr! ie in havocVars)
          {
            if ( !(ie.Decl is Incarnation) )
            {
              Variable x = (!)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)
          {
            if ( !(ie.Decl is Incarnation) )
            {
              Variable x = (!)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;
            Cmd! cmd = sug.Desugaring;
            TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds);
        }
        else if (c is StateCmd)
        {
            this.preHavocIncarnationMap = null;       // we do not need to remeber the previous incarnations
            StateCmd! st = (StateCmd)c;
            // account for any where clauses among the local variables
            foreach (Variable! v in st.Locals) {
                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) {
                TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds);
            }
            // remove the local variables from the incarnation map
            foreach (Variable! v in st.Locals) {
                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 rember 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
    }

    /// <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)
      requires 0 <= predIndex && predIndex < succ.Predecessors.Length;
    {
      Block! pred = (!) 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!) pred.TransferCmd;
      assume gtc.labelTargets != null;
      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(Implementation! impl)
    {
      #region Introduce empty blocks before all blocks with more than one predecessor
      List<Block!> tweens = new List<Block!>();
      foreach ( Block b in impl.Blocks )
      {
        int nPreds = b.Predecessors.Length;
        if ( nPreds > 1 ) 
        {
          for (int i = 0; i < nPreds; i++ ) 
          {
            tweens.Add(CreateBlockBetween(i, b));
          }
        }
      }
      impl.Blocks.AddRange(tweens);  // must wait until iteration is done before changing the list
      #endregion    
    }     
     
  }
}