//-----------------------------------------------------------------------------
//
// 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
  {
  
    private Dictionary<Block, Variable!>! m_BlockReachabilityMap;
    
    
    /// <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 class DummyErrorHandler : ProverInterface.ErrorHandler
    {
        Hashtable! label2Absy;
        VerifierCallback! callback;
        
        public DummyErrorHandler(Hashtable! label2Absy, VerifierCallback! callback) {
          this.label2Absy = label2Absy;
          this.callback = callback;
        }
        
        public override Absy! Label2Absy(string! label) {
          int id = int.Parse(label);
          return (Absy!) label2Absy[id];
        }
        
        public override void OnProverWarning(string! msg) {
          this.callback.OnWarning(msg);
        }
   
      public override void OnModel(IList<string!>! labels, ErrorModel errModel)
      {}
      public override void OnResourceExceeded(string! message)
      {}
    }

    /// <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;
    {
      if (CommandLineOptions.Clo.TraceVerify) { 
        Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
      }
      // MSchaef: The error handler errh can only be used to emmit warnings
      
      callback.OnProgress("doomdetector",0,0,0);
      #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!>();
  
      impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks);     
      ComputePredecessors(impl.Blocks);
       
      m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
      PassifyProgram(impl, program);
      #endregion
      
      int totalblocks = impl.Blocks.Count;
      
      Checker! checker = FindCheckerFor(impl, 1000);     

      Hashtable label2absy;

      VCExpr! vc = GenerateEVC(impl, out label2absy, checker);
      assert label2absy!=null;
      DummyErrorHandler errh = new DummyErrorHandler(label2absy, callback );      
      checker.PushVCExpr(vc);
      checkimplsanity(impl.Blocks[0]);

      InclusionOrder incorder = new InclusionOrder(impl);
      incorder.ToString();
      int totalchecks=0;
      

      
      Block b=null;      
      while ( incorder.GetNextBlock(out b) )
      {

        assert b!=null;
        if (CommandLineOptions.Clo.TraceVerify) {
            totalchecks++;
            Console.WriteLine("Checking Block {0}", b.Label);  
        }
        Variable v = null;
        m_BlockReachabilityMap.TryGetValue(b, out v);
        assert v!=null;

        VCExpr! currentlabel = checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v);
        ProverInterface.Outcome o = AskProver(b.Label, checker, currentlabel, errh);
        
        switch (o)
        {
          case ProverInterface.Outcome.Valid:
          {
            
            incorder.SetCurrentResult(true, callback, impl);                       
             
            // TODO: remove this return and make sure that the CE generation does not change the program
          checker.Close();
          return Outcome.Errors;
            break;
          }
          case ProverInterface.Outcome.Invalid:
          {
            // Todo: Try to use the counter example to minimize the number of checks needed
            incorder.SetCurrentResult(false, callback, null);
            break;
          }
          default:
          {
            incorder.SetCurrentResult(false, callback, null);
            if (CommandLineOptions.Clo.TraceVerify) {
                Console.WriteLine("I'm confused about Block {0}.", b.Label);
            }
            break;
          }
        }                        
      }
      if (CommandLineOptions.Clo.TraceVerify) {
        Console.WriteLine("total doomed points: {0}", incorder.DetectedBlock.Count );      
        Console.WriteLine("We had to ask {0} blocks out of {1}.\n \n", totalchecks, totalblocks );
      }
      
      checker.Close();

      //Todo: Implement dead code detection -> see smoke tester
      //Console.WriteLine(">>> Starting Dead Code Detection ");

      return Outcome.Correct;
    }

    private void checkimplsanity(Block! b) {
        GotoCmd gc = b.TransferCmd as GotoCmd;
        if (gc!=null) {
            assert gc.labelTargets != null;
            foreach (Block! b0 in gc.labelTargets) {
                bool sane=false;
                foreach (Block! b1 in b0.Predecessors) {
                    if (b1==b) {
                        sane=true; 
                        break;
                    }
                }
                if (!sane)
                Console.WriteLine("{{{{{{{{{{{{ {0} is not marked as pred of {1}", b.Label, b0.Label );                    
                
                checkimplsanity(b0);
            }
        }
    }

    private ProverInterface.Outcome AskProver(string! label, Checker! checker, VCExpr! vc, ProverInterface.ErrorHandler! errh) {
        checker.BeginCheck(label, vc, errh);
        WaitHandle[] wh = new WaitHandle[1];        
        ProverInterface.Outcome o = ProverInterface.Outcome.Undetermined;               
        
        wh[0] = checker.ProverDone;
        WaitHandle.WaitAny(wh);
        try {
          o = checker.ReadOutcome();
        } catch (UnexpectedProverOutputException e)
        {
          Console.WriteLine(e.ToString());
        }
        return o;    
    }



    protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)
    {
      return new Hashtable();
    }
    
    #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
    {
      public static List<Block!>! Convert2Dag(Implementation! impl, Program! program, List<Block!>! checkableBlocks)
      {
			  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();
        
        return pt.Blocks;
      }
      
      List<Block!>! Blocks;
      
      private List<Block!>! m_checkableBlocks;

      
      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);  
					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);				
				
									
				Block! arb = UnrollOnce(cutPoint, last,visited2,true, 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);

				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;
			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);  
			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);
			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 Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl, 
			                  Program! program)
	  {
	    Hashtable gotoCmdOrigins = new Hashtable();
	    Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
	    AddBlocksBetween(impl);
	    GenerateReachabilityPredicates(impl, exitBlock);
	    	    	    
	    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+"__ivebeenthere",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
   
    #region Error Verification Condition Generation
    
    VCExpr! GenerateEVC(Implementation! impl, out Hashtable label2absy, Checker! ch)
    {
			TypecheckingContext tc = new TypecheckingContext(null);
			impl.Typecheck(tc);
			label2absy = new Hashtable/*<int, Absy!>*/();
			VCExpr! vc;
			switch (CommandLineOptions.Clo.vcVariety) {
				case CommandLineOptions.VCVariety.Doomed:
					vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
					break;
				default:
					assert false;  // unexpected enumeration value
			}
			return vc;      
    }

    private Hashtable/* Block --> VCExprVar */! BlockVariableMap(List<Block!>! blocks, string! suffix,
                                                                        Microsoft.Boogie.VCExpressionGenerator! gen)
    {
      Hashtable/* Block --> VCExprVar */ map = new Hashtable/* Block --> (Let)Variable */();
      foreach (Block! b in blocks)
      {
        VCExprVar! v = gen.Variable(b.Label+suffix, Microsoft.Boogie.Type.Bool);
        map.Add(b, v);
      }
      return map;
    }


    VCExpr! LetVC(Block! startBlock,
                         Hashtable/*<int, Absy!>*/! label2absy,
                         ProverContext! proverCtxt)
    {
      Hashtable/*<Block, LetVariable!>*/! blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
      List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!>();
      VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);
      if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
        return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) );
      } else {
        return proverCtxt.ExprGen.Let(bindings, startCorrect );
      }
    }

    VCExpr! LetVC(Block! block,
                         Hashtable/*<int, Absy!>*/! label2absy,
                         Hashtable/*<Block, VCExprVar!>*/! blockVariables,
                         List<VCExprLetBinding!>! bindings,
                         ProverContext! proverCtxt)
    {
      VCExpressionGenerator! gen = proverCtxt.ExprGen;
      VCExprVar v = (VCExprVar)blockVariables[block];
      if (v == null) {
        /*
         * For block A (= block), generate:
         *   LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct))
         * with the side effect of adding the let bindings to "bindings" for any
         * successor not yet visited.
         */
        VCExpr SuccCorrect;
        GotoCmd gotocmd = block.TransferCmd as GotoCmd;
        if (gotocmd == null) {
            if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
                SuccCorrect = VCExpressionGenerator.False;
            } else {
                SuccCorrect = VCExpressionGenerator.True;
            }
        } else {
          assert gotocmd.labelTargets != null;
          List<VCExpr!> SuccCorrectVars = new List<VCExpr!>(gotocmd.labelTargets.Length);
          foreach (Block! successor in gotocmd.labelTargets) {
            VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);
            SuccCorrectVars.Add(s);
          }
          SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
        }

        VCContext context = new VCContext(label2absy, proverCtxt);
//        m_Context = context;
        VCExpr vc = Wlp.Block(block, SuccCorrect, context);
        
        v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
        bindings.Add(gen.LetBinding(v, vc));
        blockVariables.Add(block, v);
      }
      return v;
    }

    
    #endregion 
    
    #region Build Inclusion Order to minimize the number of checks
    
        class InclusionOrder 
        {
            [NotDelayed]
            public InclusionOrder(Implementation! impl) {
                /*
                    We now compute for each block the set of blocks that
                    are reached on every execution reaching this block.
                    We first compute it form the start block to the current
                    block and second from the Term block to the current one.
                    Finally we build the union.
                */
                                               
                
                Dictionary<Block!,TraceNode!>! map2 = new Dictionary<Block!,TraceNode!>();
                Dictionary<Block!,TraceNode!>! map = new Dictionary<Block!,TraceNode!>();
                
                Dictionary<Block!, List<Block!>!>! unavoidablemap = new Dictionary<Block!, List<Block!>!>();

                Block! exitblock = BreadthFirst(impl.Blocks[0], map2);
                BreadthFirstBwd(exitblock, map);               

                foreach (KeyValuePair<Block!, TraceNode!> kvp in map) {
                    List<Block!>! blist = new List<Block!>();
                    foreach (TraceNode tn in kvp.Value.Unavoidables ) {
                        blist.Add(tn.block);
                    }
                    unavoidablemap.Add(kvp.Key, blist);
                }
                foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
                    TraceNode tn = null;
                    if (map2.TryGetValue(kvp.Key, out tn) ) {
                        assert tn!=null;
                        foreach (TraceNode! t0 in tn.Unavoidables) {
                            if (!kvp.Value.Contains(t0.block))
                                kvp.Value.Add(t0.block);
                        }
                    } else {
                        assert false;
                    }
                }
                                                               
                foreach (KeyValuePair<Block!, List<Block!>!> kvp in unavoidablemap) {
                    Insert2Tree(RootNode,kvp);
                }
                InitCurrentNode(RootNode);
                //printtree(RootNode, "",0);                
            }
                      
            InclusionTree! RootNode = new InclusionTree(null); 
            
            InclusionTree currentNode = null;
            
            void InitCurrentNode(InclusionTree! n) {
                if (n.Children.Count>0) {
                    InitCurrentNode(n.Children[0]);
                } else {
                    currentNode = n;
                }
            }
            
            public bool GetNextBlock(out Block b) {
                if (currentNode!=null) {
                    b = currentNode.EquivBlock[0];
                    return true;
                }   
                b = null;
                return false;
            }
            
            public List<Block!>! DetectedBlock = new List<Block!>(); 
                        
            public void SetCurrentResult(bool isDoomed, VerifierCallback! cb, Implementation? impl) {                
                if (!isDoomed) { 
                    if (currentNode != null) {
                        currentNode.IsDoomed = false;
                        currentNode.HasBeenChecked = true;
                        MarkUndoomedParents(currentNode);                        
                        currentNode = FindNextNode(currentNode);
                    }
                } else {
                    if (currentNode != null) {    
                        string dblocks = "Doomed Blocks: ";
                        // WARNING THIS IS A HACK:
                        assert impl!=null;
                        impl.Blocks.Clear();
                        
                        foreach (Block! b in currentNode.EquivBlock) {
                            impl.Blocks.Add(b);
                            dblocks += String.Format("{0}, ", b.Label);
                        }
                        cb.OnWarning("Doomed program points found!");
                        cb.OnWarning(dblocks);
                        cb.OnUnreachableCode(impl);
                        
                        
                        if (currentNode.EquivBlock.Count>0) {
                            DetectedBlock.Add(currentNode.EquivBlock[0]);
                            // Todo: Remove all doomed blocks that are found
                            // in children.
                            // Maybe on should remove them only if all children
                            // are doomed, but this does not affect soundness                            
                        } else {
                            Console.WriteLine("An empty equivalence class has been detected");
                            assert false;
                        }
                        
                        currentNode.IsDoomed = true;
                        currentNode.HasBeenChecked = true;
                        MarkDoomedChildren(currentNode);
                        currentNode = currentNode.Parent;
                    }                        
                }
            }                        
                        
            InclusionTree FindNextNode(InclusionTree! n) {
                assert n!=n.Parent;
                InclusionTree next = n.Parent;                
                if (next!=null) {
                    foreach (InclusionTree! n0 in next.Children) {
                        if (!n0.HasBeenChecked) {
                            return n0;
                        }
                    }
                    return FindNextNode(next);                    
                }                
                return next;
            }
            
            void MarkUndoomedParents(InclusionTree! n) {
                if (n.Parent != null) {
                    n.Parent.HasBeenChecked = true;
                    n.Parent.IsDoomed = false;
                    MarkUndoomedParents(n.Parent);
                }
            }
            
            void MarkDoomedChildren(InclusionTree! n) {
                foreach (InclusionTree! t in n.Children) {
                    t.IsDoomed = true;
                    t.HasBeenChecked = true;
                    MarkDoomedChildren(t);
                }
            }
            
            
            void printtree(InclusionTree! n, string indent, int level) {
                Console.Write("{0}Level {1}: Blocks ", indent, level);
                foreach (Block! b in n.EquivBlock) {
                    Console.Write("{0}, ", b.Label);
                }
                Console.WriteLine();
                
                foreach (InclusionTree! t in n.Children) {
                    printtree(t, indent+"  ", level+1);
                }
            }
            
            bool Insert2Tree(InclusionTree! node, KeyValuePair<Block!, List<Block!>!> kvp) {
                if (IsSubset(node.PathBlocks, kvp.Value) ) {
                    if (IsSubset(kvp.Value, node.PathBlocks) ) {
                        // The set of unavoidable blocks is equal, so 
                        // we can put the block in the same node.
                        node.EquivBlock.Add(kvp.Key);
                        return true;
                    } else {
                        foreach (InclusionTree! n in node.Children) {
                            if (Insert2Tree(n,kvp) ) {
                                return true;
                            }
                        }
                        // we have not been able to add the block to one of
                        // the children, so we have to create a new child.
                        InclusionTree! it = new InclusionTree(node);
                        it.EquivBlock.Add(kvp.Key);
                        it.PathBlocks.AddRange(kvp.Value);
                        node.Children.Add(it);
                        return true;
                    }
                    // If we reached this point, we have to add a new node since
                    // our current set of pathnodes is not a subset of anything else
                } else {
                    // seems, that we have reached a new leaf.
                }                
                return false;
            }
            
            
            bool IsSubset(List<Block!>! sub, List<Block!>! super ) {
                foreach (Block! b in sub) {
                    if (!super.Contains(b) ) return false;                    
                }
                return true;
            }
            
            
            private class InclusionTree {
                public InclusionTree(InclusionTree p) {
                    Parent = p;
                    HasBeenChecked=false;  
                    IsDoomed = false;
                }
                
                public bool HasBeenChecked;
                public bool IsDoomed;
                public InclusionTree Parent;
                public List<Block!>! EquivBlock = new List<Block!>();
                public List<Block!>! PathBlocks = new List<Block!>();
                public List<InclusionTree!>! Children = new List<InclusionTree!>();
            }
            
     #region Collect Unavoidable Blocks
            private Block! BreadthFirst(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
                List<Block!>! JobList = new List<Block!>();
                List<Block!>! DoneList = new List<Block!>();
                Block exitblock=null;
                JobList.Add(start);
                Block! currentBlock = JobList[0];
                // Travers the Graph Breadth First and collect all 
                // predecessors of each node that are reached on any
                // path to this node
                while (JobList.Count>0)
                {                    
                    currentBlock = JobList[0];
                    TraceNode! tn = new TraceNode(currentBlock);
                    
                    if (currentBlock.Predecessors.Length>0 ) {                    
                        TraceNode t0 =null;
                        Block firstpred = currentBlock.Predecessors[0];
                        
                        assert firstpred!=null;
                        if (blockmap.TryGetValue(firstpred, out t0)) {
                            assert t0 !=null;
                            tn.Unavoidables.AddRange(t0.Unavoidables);                                
                        }
                    }   
                                         
                    foreach (Block! b0 in currentBlock.Predecessors) {
                        TraceNode t = null;
                        if (blockmap.TryGetValue(b0, out t)) {
                            assert t!=null;
                            tn.Predecessors.Add(t);                            
                            IntersectUnavoidables(t,tn);                            
                            if (!t.Successors.Contains(tn)) t.Successors.Add(tn);
                            blockmap[b0]=t;
                        }
                    }
                    if (!tn.Unavoidables.Contains(tn)) {
                        tn.Unavoidables.Add(tn);
                    } else
                    {
                        assert false;
                    }          
                    
                                        
                    blockmap.Add(currentBlock, tn);
                    
                    GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
                    if (gc!=null) {
                        assert gc.labelTargets!=null;
                        foreach (Block! b0 in gc.labelTargets) {
                            if (!JobList.Contains(b0) && !DoneList.Contains(b0)) {
                                
                                JobList.Add(b0);
                            }
                        }
                    } else {
                        exitblock=currentBlock;
                    }
                    DoneList.Add(currentBlock);
                    JobList.RemoveAt(0);
                }
                assert exitblock!=null;
                return exitblock;
            }
       
            // WARNING: It is only for testing reasons that
            // BreadthFirstBwd and BreadthFirst and separat functions
            // it should be implemented using one function later on.
            private void BreadthFirstBwd(Block! start, Dictionary<Block!, TraceNode!>! blockmap) {
                List<Block!>! JobList = new List<Block!>();                
                List<Block!>! DoneList = new List<Block!>();
                JobList.Add(start);
                Block! currentBlock = JobList[0];
                // Travers the Graph Breadth First and collect all 
                // predecessors of each node that are reached on any
                // path to this node
                while (JobList.Count>0)
                {                    
                    currentBlock = JobList[0];
                    TraceNode! tn = new TraceNode(currentBlock);
                    
                    GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
                    BlockSeq preds = null;
                    if (gc!=null) {
                        preds = gc.labelTargets;
                    }
                    
                    if (preds != null ) {
                    
                        TraceNode t0 =null;
                        Block firstpred = preds[0];
                        
                        assert firstpred!=null;
                        if (blockmap.TryGetValue(firstpred, out t0)) {
                            assert t0 !=null;
                            tn.Unavoidables.AddRange(t0.Unavoidables);                                
                        }
                      
                                         
                        foreach (Block! b0 in preds) {
                            TraceNode t = null;
                            if (blockmap.TryGetValue(b0, out t)) {
                                assert t!=null;
                                tn.Successors.Add(t);                            
                                IntersectUnavoidables(t,tn);                            
                                if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);
                                blockmap[b0]=t;
                            }
                        }
                    } 
                    if (!tn.Unavoidables.Contains(tn)) {
                        tn.Unavoidables.Add(tn);
                    } else
                    {
                        assert false;
                    }
                    blockmap.Add(currentBlock, tn);
                                        
                    if (currentBlock.Predecessors.Length>0) {                        
                        foreach (Block! b0 in currentBlock.Predecessors) {
                            if (!JobList.Contains(b0) && !DoneList.Contains(b0) ) 
                                JobList.Add(b0);
                        }
                    }
                    DoneList.Add(currentBlock);
                    JobList.RemoveAt(0);
                }
            }
       
            
            private void IntersectUnavoidables(TraceNode! parent, TraceNode! child) {
                List<TraceNode!>! ret = new List<TraceNode!>();
                List<TraceNode!>! tmp = new List<TraceNode!>();
                tmp.AddRange(parent.Unavoidables);
                tmp.AddRange(child.Unavoidables);
                
                foreach (TraceNode! tn in tmp) {                        
                    if (parent.Unavoidables.Contains(tn) && child.Unavoidables.Contains(tn) 
                        && !ret.Contains(tn) ) {
                        ret.Add(tn);
                    }
                }
                assert ret.Count <= parent.Unavoidables.Count && ret.Count <= child.Unavoidables.Count;
                child.Unavoidables = ret;
                
             }
            
            #region TraceNode Class  
            // We assume that the program is already loopfree, otherwise we will
            // not terminate      
            private class TraceNode  {
                public List<TraceNode!>! Predecessors = new List<TraceNode!>();
                public List<TraceNode!>! Successors = new List<TraceNode!>();
                public List<TraceNode!>! Unavoidables = new List<TraceNode!>();
                public Block! block;
            
               
                public TraceNode(Block! b) {                    
                    block=b;                          
                }
                
            }
            #endregion
         #endregion
        }
    #endregion
     
  }
}