//-----------------------------------------------------------------------------
//
// 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 VC
{
  public class DCGen : ConditionGeneration
  {
    #region Attributes
    private Dictionary<Block, Variable!>! m_BlockReachabilityMap;
    Dictionary<Block!, Block!>! m_copiedBlocks = new Dictionary<Block!, Block!>();
    const string reachvarsuffix = "__ivebeenthere";
    List<Cmd!>! m_doomedCmds = new List<Cmd!>();
    #endregion
    /// <summary>
    /// Constructor.  Initializes the theorem prover.
    /// </summary>
    public DCGen(Program! program, string/*?*/ logFilePath, bool appendLogFile)
    {
      base(program);
      this.appendLogFile = appendLogFile;
      this.logFilePath = logFilePath;
      m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
    }


    private void Impl2Dot(Implementation! impl, string! filename) {
        List<string!>! nodes = new List<string!>();
        List<string!>! edges = new List<string!>();
        
        string nodestyle = "[shape=box];" ;
        
        foreach (Block! b in impl.Blocks) {
            nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle) );
            GotoCmd gc = b.TransferCmd as GotoCmd;
            if (gc!=null) {
                assert gc.labelTargets!=null;
                foreach (Block! b_ in gc.labelTargets) {
                    edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label ) );
                }
            }
        }
        
        using (StreamWriter sw = new StreamWriter(filename)) 
        {
            sw.WriteLine(String.Format("digraph {0} {{", impl.Name));
//            foreach (string! s in nodes) {
//                sw.WriteLine(s);
//            }
            foreach (string! s in edges) {
                sw.WriteLine(s);
            }
            sw.WriteLine("}}");
            sw.Close();
        }
    }
    
    private const string _copyPrefix = "Yeah";
    
    private Block! CopyImplBlocks(Block! b, ref List<Block!>! blocklist, Block! targetBlock, ref Dictionary<Block!, Block!>! alreadySeen) {
        Block seen;
        if (alreadySeen.TryGetValue(b, out seen) ) {
            assert seen!=null;
            return seen;
        }
    
        GotoCmd gc = b.TransferCmd as GotoCmd;
        TransferCmd tcmd = null;
        if (gc!=null) {
            BlockSeq! bseq = new BlockSeq();
            assert gc.labelTargets!=null;
            foreach (Block! c in gc.labelTargets) {
                bseq.Add(CopyImplBlocks(c, ref blocklist, targetBlock, ref alreadySeen));
            }
            tcmd = new GotoCmd(gc.tok, bseq);
        } else {
//            BlockSeq! bseq_ = new BlockSeq();
//            bseq_.Add(targetBlock);
            assert b.TransferCmd != null;
//            tcmd = new GotoCmd(b.TransferCmd.tok, bseq_);
            tcmd = new ReturnCmd(b.TransferCmd.tok);
        }
        
        CodeCopier codeCopier = new CodeCopier();
        CmdSeq! cl = new CmdSeq();
        foreach (Cmd! _c in b.Cmds) {
            if (!ContainsReachVariable(_c))
                cl.Add( codeCopier.CopyCmd(_c));
         }
       
        Block! b_ = new Block(b.tok, b.Label+_copyPrefix, cl, tcmd);
        blocklist.Add(b_);
        
        alreadySeen[b] = b_;
        
        return b_;
    }
    
    /*
        After adding a copy of the implementation in front of our code
        we remove all the edges leading from the copy to the original code
    */
    private void RemoveArtificialGoto(Block! b, Block! target) {
        GotoCmd gc = b.TransferCmd as GotoCmd;

        if (gc!=null) {
            assert gc.labelTargets!=null;
            foreach (Block! gt in gc.labelTargets) {
                if (gt==target) {
                    assert gc.labelTargets.Length==1;
                    assert gc.labelTargets[0]!=null;
                    b.TransferCmd = new ReturnCmd(gc.tok);
                    return;
                } else {
                    RemoveArtificialGoto(gt, target);
                }                
            }        
        
        }
    }
    
    static public bool UseItAsDebugger = false; 
           
//    public static Implementation _tmpImpl = null; // (MsSchaef) HACK!
    
    public static Block firstNonDebugBlock = null;
    public static Block firstDebugBlock = null;
    
    private void ModifyImplForDebugging(Implementation! impl)
    {
      //List<Block!> backup_blocks=null;
      
                   
      if (UseItAsDebugger) {  
        #region Copy the Implementation /////////////////////   
        
        ConsoleColor col = Console.ForegroundColor;
        Console.ForegroundColor = ConsoleColor.Magenta; 
        Console.WriteLine("Warning you are using the Infinite Improbability Drive!");
        Console.ForegroundColor = col;           
                       
        List<Block!>! blist = new List<Block!>();
        Dictionary<Block!, Block!>! tmpdict = new Dictionary<Block!, Block!>();
        CopyImplBlocks(impl.Blocks[0], ref blist, impl.Blocks[0], ref tmpdict);        
        blist.Reverse();
        //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);              
        
        #endregion ////////////////////////////////////
        
        #region Add implementation copy in front of implementation
        // memorize where the original code starts
        firstNonDebugBlock = impl.Blocks[0];
        firstDebugBlock = blist[0];
        // now add the copied program in front of the original one
        blist.AddRange(impl.Blocks);
        //backup_blocks = new List<Block!>(impl.Blocks);
        
        BlockSeq! newbseq = new BlockSeq();
        newbseq.Add(firstNonDebugBlock);
        newbseq.Add(firstDebugBlock);
        
        GotoCmd! newtcmd = new GotoCmd(Token.NoToken, newbseq);
        Block! newfirst = new Block(Token.NoToken, "MySuperFirstBlock", new CmdSeq(), newtcmd);
        
                
        impl.Blocks = new List<Block!>();
        impl.Blocks.Add(newfirst);
        impl.Blocks.AddRange(blist);
                
        //Impl2Dot(impl, String.Format("c:/dot/{0}_copied.dot", impl.Name) );
        #endregion
      }
    } 
    
    void RemoveReachVars(Block! b) {
        GotoCmd gc = b.TransferCmd as GotoCmd;
        if (gc!=null) {
            assert gc.labelTargets!=null;
            
            CmdSeq! cs = new CmdSeq();
            foreach (Cmd! c in b.Cmds) {
                if (!ContainsReachVariable(c)) cs.Add(c);
            }
            b.Cmds = cs;
            
            foreach (Block! c in gc.labelTargets) {
                if (c.Label != "GeneratedUnifiedExit") {
                    RemoveReachVars(c);
                }
            }
        }
    }
    
    void RemoveLastBlock(Block! b) 
    {
        GotoCmd gc = b.TransferCmd as GotoCmd;
        if (gc==null) {
            //Console.WriteLine("WARNING: Check Node {0}", b.Label);
            return;
        }
        assert gc!=null;
        assert gc.labelTargets !=null;
        BlockSeq! tmp = new BlockSeq();
        foreach (Block! c in gc.labelTargets) {
            // Warning, we should not search by name!
            if (c.Label != "GeneratedUnifiedExit" ) {            
                tmp.Add(c);
                RemoveLastBlock(c);                
            } else {
                c.Predecessors.Remove(b);
            }
        }
        if (tmp.Length==0) {
            b.TransferCmd = new ReturnCmd(gc.tok);
        } else {
            b.TransferCmd = new GotoCmd(gc.tok, tmp);
        }
    }
    
    void FindCopiedBlocks(Block! b) {
        _copiedBlock.Add(b);
        GotoCmd gc = b.TransferCmd as GotoCmd;
        if (gc!=null) {
            assert gc.labelTargets!=null;
            foreach (Block! c in gc.labelTargets) {
                FindCopiedBlocks(c);
            }
        }      
    }
    
    private List<Block!>! _copiedBlock = new List<Block!>();
    
    /// <summary>
    /// MSchaef: 
    /// - remove loops and add reach variables
    /// - make it a passive program
    /// - compute the wlp for each block
    /// - check if |= (reach=false) => wlp.S.false holds for each reach
    ///
    /// </summary>
    public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)
      throws UnexpectedProverOutputException;
    {   
    
    UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;
        Stopwatch watch = new Stopwatch();
        
      //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) );               

      if (CommandLineOptions.Clo.TraceVerify) { 
        Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
      }
      Console.WriteLine("Checking function {0} for doomed points:", impl.Name);
      callback.OnProgress("doomdetector",0,0,0);

        watch.Reset();
        watch.Start();

      
        
      #region Transform the Program into loop-free passive form
      variable2SequenceNumber = new Hashtable/*Variable -> int*/();
      incarnationOriginMap = new Dictionary<Incarnation, Absy!>();      
      List<Block!>! cblocks = new List<Block!>();
      
      //List<Block!>! orig_blocks = new List<Block!>(impl.Blocks);
      
      Dictionary<Block!, Block!> copiedblocks;
      impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks, out copiedblocks);
      assert copiedblocks!=null;

//      List<Block!>! blist = new List<Block!>();
//      blist.AddRange(impl.Blocks);

      if (UseItAsDebugger) ModifyImplForDebugging(impl);

      ComputePredecessors(impl.Blocks);

      m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
      GenerateReachVars(impl);

      if (UseItAsDebugger) RemoveReachVars((!)firstDebugBlock);
                          
      PassifyProgram(impl);
      
      
      #endregion
      //EmitImpl(impl,false);    

    
        //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) );   

// ---------------------------------------------------------------------------
      if (UseItAsDebugger) {  
        assert firstNonDebugBlock != null && firstDebugBlock != null;
        firstNonDebugBlock.Predecessors.Remove(impl.Blocks[0]);   
        firstDebugBlock.Predecessors.Remove(impl.Blocks[0]);
//        impl.Blocks.Remove(impl.Blocks[0]); // remove the artificial first block
        RemoveLastBlock(firstDebugBlock); // remove the goto to the unified exit  
        _copiedBlock.Clear();
        FindCopiedBlocks(firstDebugBlock);
      }
// ---------------------------------------------------------------------------      
      
// EmitImpl(impl,false);    
      
      //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );               
            
      
      watch.Stop();
      Console.WriteLine("Transformations takes: {0}", watch.Elapsed.ToString() );
      watch.Reset();
      
      Checker! checker = FindCheckerFor(impl, 1000);     
      
      DoomCheck dc = new DoomCheck(impl, checker);
      
      int _totalchecks = 0;
      Block b = null;
      ProverInterface.Outcome outcome;
      dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
      bool doomfound = false;
      
      bool __debug = true;
      
      System.TimeSpan ts = watch.Elapsed;    
      
      while (dc.GetNextBlock(out b) && !doomfound) {
        assert b!=null;
        outcome = ProverInterface.Outcome.Undetermined;
        //Console.WriteLine("Checking block {0} ...",b.Label);
        Variable v = null;
        m_BlockReachabilityMap.TryGetValue(b, out v);
        assert v!=null;
        _totalchecks++;
        
        if (__debug) Console.WriteLine("Checking Block {0}", v.Name);
        
        
        watch.Start();
        if (!dc.CheckLabel(v, out outcome) ) {
            return Outcome.Inconclusive;
        }
        watch.Stop();
        ts+=watch.Elapsed;
        Console.WriteLine(" --- {0} elapsed", watch.Elapsed.ToString());
        watch.Reset();
        
        
        switch (outcome) {
            case ProverInterface.Outcome.Valid: {                
                doomfound=true;
                break;
            }
            case ProverInterface.Outcome.Invalid: {
            
                break;
            }
            default: {
            
                break;
            }
        }
        
      }
      checker.Close();
      
      Console.WriteLine("Number of Checked Blocks: {0}", _totalchecks);
      
      #region Try to produce a counter example (brute force)
      if (dc.DoomedSequences.Count>0 ) {

        ConsoleColor col = Console.ForegroundColor;
        Console.ForegroundColor = ConsoleColor.Red;              
        Console.WriteLine("  {0} is DOOMED!", impl.Name);
        Console.ForegroundColor = col;        
        
        SearchCounterexample(impl, dc.ErrorHandler, callback);
        Console.WriteLine("------------------------------ \n\n");
        return Outcome.Errors;
      }
      #endregion
      
      Console.WriteLine("------------------------------ \n\n");
      
      return Outcome.Correct;
    }
    
    
    
    private void SearchCounterexample(Implementation! impl, DoomErrorHandler! errh, VerifierCallback! callback) {        
        if (errh.m_Reachvar==null) {
            assert false;
            return;
        }
        m_doomedCmds.Clear();
                
        assert errh.m_TraceBlocks != null;
        assert errh.m_DoomedBlocks !=null;
        List<Block!>! nondoomed = new List<Block!>();
        foreach (Block! b in errh.m_DoomedBlocks) {
            if (!errh.m_TraceBlocks.Contains(b) ) {
                nondoomed.Add(b);
            }
        }   
        
        Dictionary<Block!, CmdSeq!>! cmdbackup = new Dictionary<Block!, CmdSeq!>();
        
        BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count/2-1);
        BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count/2,impl.Blocks.Count-1);
        
        BlockSeq! trace = new BlockSeq();
        foreach (Block! b in cmdbackup.Keys ) {
            trace.Add(b);
        }
        AssertCmd asrt = null;
        foreach (Cmd! c in m_doomedCmds) {
            AssertCmd ac = c as AssertCmd;
            if (ac!=null) {
                asrt=ac;
            }
        }
        if (asrt==null) {
            //callback.OnWarning("Sorry, cannot create counterexample");
        } else {
            //AssertCounterexample! ace = new AssertCounterexample(trace, asrt);
            //callback.OnCounterexample(ace, "Todo: Build a reason");        
        }        
        #region Undo all modifications        
        foreach (KeyValuePair<Block!, CmdSeq!> kvp in cmdbackup) {
            kvp.Key.Cmds = kvp.Value;
        }    
        #endregion   
    }
    
    bool BruteForceCESearch(Variable! reachvar, Implementation! impl, VerifierCallback! callback,
                        Dictionary<Block!, CmdSeq!>! cmdbackup, int startidx, int endidx) {
        #region Modify implementation
        for (int i=startidx; i<=endidx; i++) {
            if (_copiedBlock.Contains(impl.Blocks[i])) continue;
            CmdSeq! cs = new CmdSeq();            
            cmdbackup.Add(impl.Blocks[i],impl.Blocks[i].Cmds);
            foreach (Cmd! c in impl.Blocks[i].Cmds) {
                if (ContainsReachVariable(c)) {
                    cs.Add(c);
                    continue;
                }
                AssertCmd ac = c as AssertCmd;
                AssumeCmd uc = c as AssumeCmd;
                if (ac!=null) {
                    cs.Add(new AssertCmd(ac.tok, Expr.True) );
                } else if (uc!=null) {
                    cs.Add(new AssertCmd(uc.tok, Expr.True) );
                } else {
                    cs.Add(c);
                }
            }
            impl.Blocks[i].Cmds = cs;
        }
        #endregion   
            
        ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
        if (!ReCheckImpl(reachvar, impl, callback, out outcome) ) {
            UndoBlockModifications(impl, cmdbackup, startidx, endidx);
            return false;
        }
        if (outcome == ProverInterface.Outcome.Valid) {
            return true;                                                        
        } else  if (outcome == ProverInterface.Outcome.Invalid) {
            UndoBlockModifications(impl, cmdbackup, startidx, endidx);
            int mid = startidx + (endidx-startidx)/2;
            if (startidx>=endidx) {
                // Now we found an interesting Block and we have to
                // search for the interesting statements.
                int cmdcount = impl.Blocks[endidx].Cmds.Length-1;
                BruteForceCmd(impl.Blocks[endidx],0,cmdcount/2 -1,reachvar, impl, callback);
                BruteForceCmd(impl.Blocks[endidx],cmdcount/2,cmdcount,reachvar, impl, callback);
                return true; 
            } else {                
                BruteForceCESearch(reachvar,impl, callback, cmdbackup, startidx, mid);
                //if (startidx+mid+1>=endidx) mid--; //Hack
                BruteForceCESearch(reachvar,impl, callback, cmdbackup, mid+1, endidx);                       
                return true;
            }
        }  else {
            UndoBlockModifications(impl, cmdbackup, startidx, endidx);
            return false;
        }                      
    }
    
    bool BruteForceCmd(Block! b, int startidx, int endidx, Variable! reachvar, 
                       Implementation! impl, VerifierCallback! callback) {
        #region Modify Cmds
        CmdSeq! backup = b.Cmds;
        CmdSeq! cs = new CmdSeq();
        for (int i=0;i<startidx;i++) {
            cs.Add(b.Cmds[i]);
        }
        for (int i=startidx; i<=endidx; i++) {
            Cmd! c = b.Cmds[i];
            if (ContainsReachVariable(c)) {
                cs.Add(c);
                continue;
            }
            cs.Add(new AssertCmd(c.tok, Expr.True));
        }         
        for (int i=endidx+1; i<b.Cmds.Length;i++) {
            cs.Add(b.Cmds[i]);
        }

        b.Cmds = cs;       
        #endregion
        
        #region Recheck
        ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
        if (!ReCheckImpl(reachvar, impl, callback, out outcome) ) {
            b.Cmds = backup;
            return false;
        }
        #endregion

        if (outcome == ProverInterface.Outcome.Valid) {
            return true;                                                        
        } else if (outcome == ProverInterface.Outcome.Invalid) {
            b.Cmds = backup;
            if (startidx>=endidx) {
                if (!ContainsReachVariable(b.Cmds[endidx])) {                                
                    Console.Write("   Witness (");
                    
                    ConsoleColor col = Console.ForegroundColor;
                    Console.ForegroundColor = ConsoleColor.White; 
                    Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );                    
                    Console.ForegroundColor = col;
                    Console.Write("):   ");                    
                    Console.ForegroundColor = ConsoleColor.Yellow;
                    b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);                                        
                    Console.ForegroundColor = col;

                    m_doomedCmds.Add(b.Cmds[endidx]);
                    return true;
                } else {
                    return false;
                }
            } else {
                int mid = startidx + (endidx-startidx)/2;
                BruteForceCmd(b, startidx, mid, reachvar, impl, callback); 
                BruteForceCmd(b, mid+1, endidx, reachvar, impl, callback);
                return false; // This is pure random
            }
        } else {
            b.Cmds = backup;
            return false;
        }
                      
        return false;
    }
    
    void UndoBlockModifications(Implementation! impl, Dictionary<Block!, CmdSeq!>! cmdbackup, 
                                int startidx, int endidx) {
        for (int i=startidx; i<=endidx; i++) {
            CmdSeq cs = null;
            if (cmdbackup.TryGetValue(impl.Blocks[i], out cs) ) {
                assert cs!=null;
                impl.Blocks[i].Cmds = cs;
                cmdbackup.Remove(impl.Blocks[i]);
            }
        }                                        
    }
    
    bool ReCheckImpl(Variable! reachvar, Implementation! impl, VerifierCallback! callback,
                     out ProverInterface.Outcome outcome) {
        Checker! checker = FindCheckerFor(impl, 1000);
        DoomCheck dc = new DoomCheck(impl, checker);
        dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);                        
        outcome = ProverInterface.Outcome.Undetermined;        
        if (!dc.CheckLabel(reachvar, out outcome)) {
            checker.Close();
            return false;
        }
        checker.Close();
        return true;
    }

    
        
    bool ContainsReachVariable(Cmd! c) {
        AssertCmd artc = c as AssertCmd;
        AssumeCmd amec = c as AssumeCmd;
        Expr e;
        if (artc!=null) {
            e = artc.Expr;
        } else if (amec!=null) {
            e = amec.Expr;
        } else {             
            return false;
        }
        Set! freevars = new Set();
        e.ComputeFreeVariables(freevars);
        foreach (Variable! v in freevars) {
            if (v.Name.Contains(reachvarsuffix)) return true;
        }
        return false;
    }
    
    
    #region Loop Removal
    /// <summary>
    /// This class is accessed only via the static method Convert2Dag
    /// It converts the program into a loopfree one by unrolling the loop threetimes and adding the appropriate havoc
    /// statements. The first and the last unrolling represent the first and last iteration of the loop. The second
    /// unrolling stands for any other iteration.
    /// </summary>
    private class DCProgramTransformer
    {
      private List<Block!>! Blocks;
      private List<Block!>! m_checkableBlocks;
      private Dictionary<Block!, Block!>! m_copyMap = new Dictionary<Block!, Block!>();

      public static List<Block!>! Convert2Dag(Implementation! impl, Program! program, List<Block!>! checkableBlocks,
            out Dictionary<Block!, Block!> copiedblocks)
      {
        Block! start = impl.Blocks[0];
        Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();
        Set/*Block*/! beingVisited = new Set/*Block*/();
        GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);
      
        DCProgramTransformer pt = new DCProgramTransformer(checkableBlocks);
          pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");    
          pt.Blocks.Reverse();
        copiedblocks = pt.m_copyMap;
        return pt.Blocks;
      }
     
      
      DCProgramTransformer(List<Block!>! checkableBlocks)
      {
        Blocks = new List<Block!>();
        m_checkableBlocks = checkableBlocks;
      }
    

#region Loop Unrolling Methods
    
        private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
        {
            Block newb;
            if (visited.TryGetValue(node, out newb)) 
            {
                assert newb!=null;
                return newb;
            } else 
            {
                if (node.IsCutPoint)
                {
                    // compute the loop body and the blocks leaving the loop
                    
                    List<GraphNode!>! loopNodes = new List<GraphNode!>();
                    GatherLoopBodyNodes(node, node, loopNodes);

                    List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);
                    
                    // Continue Unrolling after the current loop
                    Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();
                    foreach (GraphNode! g in exitNodes)
                    {                    
                        Block b = LoopUnrolling(g, visited, unrollable, prefix);
                        _visited.Add(g,b);
                    }
                    newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);
                    visited.Add(node,newb);
                } else
                {
                    BlockSeq! newSuccs = new BlockSeq();
                    foreach(GraphNode! g in node.Succecessors)
                    {
                        newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
                    }
                    newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
                    Block b;
                    if (m_copyMap.TryGetValue(node.Block, out b) ) {
                        assert b!=null;
                        m_copyMap.Add(newb, b);
                    } else {
                        m_copyMap.Add(newb, node.Block);
                    }
                    
                    
                    assert newb!=null; assert newb.TransferCmd!=null;                    
                    if (newSuccs.Length == 0) 
                        newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
                    else 
                        newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
                                        
                    visited.Add(node, newb);
                    Blocks.Add(newb);
                    if (unrollable) 
                    {                      
                      m_checkableBlocks.Add(newb);
                    }
                }    
            }
            assert newb!=null;
            //newb.checkable = unrollable;
            return newb;                
        }

        private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited, 
                                List<GraphNode!>! loopNodes, bool unrollable, String! prefix)
        {
            if (unrollable)
            {
                Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);
                Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);
                Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);

                Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");
            
                Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");
                AddHavocCmd(last,loopNodes);                
                
                // You might use true for the unrollable flag as well.                     
                Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");
                AddHavocCmd(arb,loopNodes);
                
                        
                BlockSeq! succ = new BlockSeq();
                succ.Add(last); succ.Add(arb);
                assert arb.TransferCmd!=null;
                Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));
                Blocks.Add(tmp);
                m_checkableBlocks.Add(tmp);

                // check if arb is already a copy of something else
                // if not then write to m_copyMap that tmp is a copy
                // of arb
                Block b = null;
                if (m_copyMap.TryGetValue(arb,out b) ) {
                    assert b!=null;
                    m_copyMap.Add(tmp, b);
                } else {
                    m_copyMap.Add(tmp, arb);
                }

                Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");
                
                return first;

            } else
            {
                Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);
                Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");                
                Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);
                AddHavocCmd(ret, loopNodes);
                return ret;            
            }
        }
        
        private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
        {
            visited.Add(node, nextIter);
            Block newb,b;
            BlockSeq! newSuccs = new BlockSeq();
            foreach(GraphNode! g in node.Succecessors)
            {
                newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
            }
            newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); 
            if (m_copyMap.TryGetValue(node.Block, out b) ) {
                assert b!=null;
                m_copyMap.Add(newb, b);
            } else {
                m_copyMap.Add(newb, node.Block);
            }
             
            assert newb!=null; assert newb.TransferCmd!=null;                    
            if (newSuccs.Length == 0) 
                newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
            else 
                newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
                                            
            Blocks.Add(newb);
            if (unrollable) m_checkableBlocks.Add(newb);
            return newb;
        }

        private Block! AbstractIteration(GraphNode! node, String! prefix)
        {
            CmdSeq body = new CmdSeq();
            foreach (Cmd! c in node.Body)
            {
                if (c is PredicateCmd || c is CommentCmd)
                    body.Add(c );
                else
                    break;
            }
            body.Add(new AssumeCmd(node.Block.tok, Expr.False) );
            TransferCmd! tcmd = new ReturnCmd(node.Block.tok);
            Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);
            Blocks.Add(b);
            Block tmp; 
            if (m_copyMap.TryGetValue(node.Block, out tmp) ) {
                assert tmp!=null;
                m_copyMap.Add(b, tmp);
            } else {
                m_copyMap.Add(b, node.Block);
            }
            
            return b;
        }

        private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes, 
                                                Dictionary<GraphNode, Block!>! visited, String! prefix)
        {
            BlockSeq! newSucc = new BlockSeq();
            Block! orig = cutPoint.Block;
            
            // detect the block after the loop
            // FixMe: What happens when using break commands?
            foreach (GraphNode! g in cutPoint.Succecessors)
            {
                if (!loopNodes.Contains(g)) 
                {
                    Block b;
                    if (visited.TryGetValue(g,out b) )
                        newSucc.Add(b);
                }
            }
            TransferCmd tcmd;
            assert orig.TransferCmd!=null;
            if (newSucc.Length==0)
                tcmd = new ReturnCmd(orig.TransferCmd.tok);
            else
                tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);
            // FixMe: Genertate IToken for counterexample creation
            Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);
            Blocks.Add(newb);
            m_checkableBlocks.Add(newb); 
            return newb;
        }


        private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)
        {
            loopNodes.Add(current);
            if (false) System.Diagnostics.Debugger.Break();
            foreach (GraphNode! g in current.Predecessors)
            {
                if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;
                GatherLoopBodyNodes(g, cutPoint, loopNodes);
            }        
        }
        
        private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)
        {
            List<GraphNode!>! exitnodes = new List<GraphNode!>();
            
            foreach (GraphNode! g in loopNodes)
            {
                foreach (GraphNode! s in g.Succecessors)
                {
                    if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);
                }
            }            
            return exitnodes;
        }
        
        private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)
        {
            List<Block!>! loopBlocks = new List<Block!>();
            foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);
            HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);
            CmdSeq! body = new CmdSeq();
            body.Add(hcmd);
            body.AddRange(b.Cmds);
            b.Cmds = body;
        }

        private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)
        {
            VariableSeq varsToHavoc = new VariableSeq();
            foreach ( Block! b in bl )
            {
                foreach ( Cmd! c in b.Cmds )
                {
                    c.AddAssignedVariables(varsToHavoc);
                }
            }
            IdentifierExprSeq havocExprs = new IdentifierExprSeq();
            foreach ( Variable! v in varsToHavoc )
            {
                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
                if(!havocExprs.Has(ie))
                    havocExprs.Add(ie);
            }
            // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
            // the source location for this later on
            return new HavocCmd(tok,havocExprs);            
        }    
                
    #endregion

      
    #region GraphNode 
    private class GraphNode
    {
      public readonly Block! Block;
      public readonly CmdSeq! Body;
      public bool IsCutPoint;  // is set during ComputeGraphInfo
      [Rep] public readonly List<GraphNode!>! Predecessors = new List<GraphNode!>();
      [Rep] public readonly List<GraphNode!>! Succecessors = new List<GraphNode!>();
      public GraphNode firstPredecessor;
      public List<GraphNode!>! UnavoidableNodes = new List<GraphNode!>(); // should be done using a set

      GraphNode(Block! b, CmdSeq! body) 
      {
        Block = b; Body = body;
        IsCutPoint = false;
        
      }

      static CmdSeq! GetOptimizedBody(CmdSeq! cmds) 
      {
        int n = 0;
        foreach (Cmd c in cmds) 
        {
          n++;
          PredicateCmd pc = c as PredicateCmd;
          if (pc != null && pc.Expr is LiteralExpr && ((LiteralExpr)pc.Expr).IsFalse) 
            {
            // return a sequence consisting of the commands seen so far
            Cmd[] s = new Cmd[n];
            for (int i = 0; i < n; i++) 
            {
              s[i] = cmds[i];
            }
            return new CmdSeq(s);
          }
        }
        return cmds;
      }

      private static List<GraphNode!>! Intersect(List<GraphNode!>! left, List<GraphNode!>! right) 
      {
        List<GraphNode!>! ret = new List<GraphNode!>();
        List<GraphNode!>! tmp = left;
        tmp.AddRange(right);       
        foreach (GraphNode! gn in tmp) {
            if (ret.Contains(gn) ) continue;
            if (left.Contains(gn) && right.Contains(gn)) ret.Add(gn);
        }
        return ret;
      }
      
      public static GraphNode! ComputeGraphInfo(GraphNode from, Block! b, Dictionary<Block,GraphNode!>! gd, Set /*Block*/! beingVisited) 
      {
        GraphNode g;
        if (gd.TryGetValue(b, out g)) 
        {
          assume from != null;
          assert g != null;
           
          g.UnavoidableNodes = Intersect(g.UnavoidableNodes, from.UnavoidableNodes);
          if (!g.UnavoidableNodes.Contains(g)) g.UnavoidableNodes.Add(g);
          
          g.Predecessors.Add(from);
          if (g.firstPredecessor==null) 
            g.firstPredecessor = from;          
            
          if (beingVisited.Contains(b)) 
            g.IsCutPoint = true; // it's a cut point
          } else 
          {
            CmdSeq body = GetOptimizedBody(b.Cmds);
            g = new GraphNode(b, body);
            gd.Add(b, g);
            if (from != null) 
            {
              g.Predecessors.Add(from);
              if (from==null) 
                g.firstPredecessor = g;
                
              if (g.firstPredecessor==null) 
                g.firstPredecessor = from;
                
            }
            if (body != b.Cmds) 
            {
            // the body was optimized -- there is no way through this block
            } else 
            {
              beingVisited.Add(b);
              GotoCmd gcmd = b.TransferCmd as GotoCmd;
              if (gcmd != null) 
              {
                assume gcmd.labelTargets != null;
                foreach (Block! succ in gcmd.labelTargets) 
                {
                    g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );
                }
              }
              beingVisited.Remove(b);
            }
          }
          return g;
        }
      }
      
    }
    #endregion        

    #endregion 
     
    #region Program Passification
      private void GenerateReachVars(Implementation! impl)
      {
        Hashtable gotoCmdOrigins = new Hashtable();
        Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
        AddBlocksBetween(impl);
        
        #region Insert pre- and post-conditions and where clauses as assume and assert statements
        {
          CmdSeq cc = new CmdSeq();
          // where clauses of global variables
          foreach (Declaration d in program.TopLevelDeclarations) {
            GlobalVariable gvar = d as GlobalVariable;
            if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
              Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
              cc.Add(c);
            }
          }
          // where clauses of in- and out-parameters
          cc.AddRange( GetParamWhereClauses(impl));
          // where clauses of local variables
          foreach (Variable! lvar in impl.LocVars) {
            if (lvar.TypedIdent.WhereExpr != null) {
              Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);
              cc.Add(c);
            }
          }

          // add cc and the preconditions to new blocks preceding impl.Blocks[0]
          InjectPreconditions(impl, cc);

          // append postconditions, starting in exitBlock and continuing into other blocks, if needed
          exitBlock = InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
        }
        #endregion        
        GenerateReachabilityPredicates(impl, exitBlock);      
      }
    
    
      private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl)
      {                        
          current_impl = impl;
          Convert2PassiveCmd(impl);
          impl = current_impl;
          return new Hashtable();
      }
    
      /// <summary>
      /// Add additional variable to allow checking as described in the paper
      /// "It's doomed; we can prove it"
      /// </summary>
      private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)
      {
          ExprSeq! es = new ExprSeq();
          Cmd eblockcond = null;
                      
          foreach (Block! b in impl.Blocks)
          {
              //if (b.Predecessors.Length==0) continue;
              //if (b.Cmds.Length == 0 ) continue;

              Variable v_ = new LocalVariable(Token.NoToken, 
                                      new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );
              
              impl.LocVars.Add(v_);
              
              m_BlockReachabilityMap[b] = v_;
              
              IdentifierExpr! lhs =  new IdentifierExpr(b.tok, v_);
              
              es.Add( new IdentifierExpr(b.tok, v_) );
              
              List<AssignLhs!>! lhsl = new List<AssignLhs!>();
              lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );
              List<Expr!>! rhsl = new List<Expr!>();
              rhsl.Add(Expr.True);
              
              if (b!=exitBlock)
              {
                  CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));                    
                  cs.AddRange(b.Cmds);
                  b.Cmds = cs;
              } else
              {                
                  eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);
              }
              
              //checkBlocks.Add(new CheckableBlock(v_,b));
          }
          if (es.Length==0) return;

          Expr aexp = null;

          if (es.Length==1) 
          {
              aexp = es[0];            
          } else if (es.Length==2)
          {
              aexp =  Expr.Binary(Token.NoToken,
                  BinaryOperator.Opcode.And,
                  (!)es[0],
                  (!)es[1]);
          } else
          {
              aexp = Expr.True;
              foreach (Expr e_ in es)
              {
                  aexp = Expr.Binary(Token.NoToken, 
                      BinaryOperator.Opcode.And,
                      (!)e_, aexp);
              }        
          }
          assert (aexp!=null);
          assert (eblockcond!=null);
          
          AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);
          
          assert(exitBlock!=null);

          CmdSeq cseq = new CmdSeq(eblockcond);
          cseq.AddRange(exitBlock.Cmds);        
          cseq.Add(ac);
          
          exitBlock.Cmds = cseq;              
      }
    
    #endregion
   
  }
}