//-----------------------------------------------------------------------------
//
// 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);
          }
        }

        InjectPreconditions(impl);
        //cc.AddRange(GetPre(impl));

        Block! entryBlock = (!) impl.Blocks[0];
        cc.AddRange(entryBlock.Cmds);
        entryBlock.Cmds = cc;
          
        InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
        //CmdSeq! post = GetPost(impl);
        //exitBlock.Cmds.AddRange(post);
        }
        // Check If a new Unified Exit has been generated
        GotoCmd gc = exitBlock.TransferCmd as GotoCmd;
        if (gc!=null) {
            assert gc.labelTargets !=null;
            assert gc.labelTargets.Length==1;
            assert gc.labelTargets[0]!=null;
            exitBlock = (!)gc.labelTargets[0];
        }
        #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
   
  }
}