Boogie\VCGeneration: Renaming sources in preparation for my addition of the ported C# version

1 files changed, 0 insertions, 1258 deletions

diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc
deleted file mode 100644
index 50307c0b..00000000
--- a/Source/VCGeneration/VCDoomed.ssc
+++ /dev/null
@@ -1,1258 +0,0 @@
-//-----------------------------------------------------------------------------

-//

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

-            

-      bool __debug = false;

-      

-      watch.Stop();

-      if (__debug) Console.WriteLine("Transformation 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);                 

-      

-      System.TimeSpan ts = watch.Elapsed;    

-      

-      while (dc.GetNextBlock(out b) ) {

-        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++;

-               

-        

-        watch.Start();

-        if (!dc.CheckLabel(v, out outcome) ) {

-            return Outcome.Inconclusive;

-        }

-        watch.Stop();

-        ts+=watch.Elapsed;

-        if (__debug) Console.WriteLine(" Time for Block {0}: {1} elapsed",b.Label, watch.Elapsed.ToString());

-        watch.Reset();

-        

-        

-        switch (outcome) {

-            case ProverInterface.Outcome.Valid: {                

-                break;

-            }

-            case ProverInterface.Outcome.Invalid: {

-            

-                break;

-            }

-            default: {

-            

-                break;

-            }

-        }

-        

-      }

-      checker.Close();

-      

-      if (__debug) Console.WriteLine("Number of Checked Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count );

-      if (__debug) Console.WriteLine("Total time for this method: {0}", ts.ToString());

-      

-      #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);

-//        foreach (List<Block!> bl in dc.DoomedSequences) {

-//            Console.Write("Doomed Blocks: ");

-//            foreach (Block! b_ in bl) {

-//                Console.Write("{0}, ", b_.Label);

-//                }

-//                Console.WriteLine();

-//        }        

-        Console.ForegroundColor = col;        

-        

-        int counter=1;

-        foreach (List<Block!>! bl in dc.DoomedSequences) {

-        Console.WriteLine("Doomed program point {0} of {1}", counter++, dc.DoomedSequences.Count);

-            dc.ErrorHandler.m_DoomedBlocks = bl;

-            foreach (Block! b_ in bl) {

-                if (m_BlockReachabilityMap.TryGetValue(b_, out dc.ErrorHandler.m_Reachvar) )break;

-            }

-            SearchCounterexample(impl, dc.ErrorHandler, callback);

-        }

-        

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

-        }

-        m_doomedCmds.Clear();

-                        

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

-                

-        List<Cmd!>! causals = CollectCausalStatements(impl.Blocks[0]);

-        foreach (Cmd! c in causals ) {            

-            GenerateErrorMessage(c, causals);            

-        }

-        

-        #region Undo all modifications        

-        foreach (KeyValuePair<Block!, CmdSeq!> kvp in cmdbackup) {

-            kvp.Key.Cmds = kvp.Value;

-        }    

-        #endregion   

-    }

-    

-#region Causal Statement Tree    

-

-    private void GenerateErrorMessage(Cmd! causalStatement, List<Cmd!>! causals) 

-    {

-        AssumeCmd uc = causalStatement as AssumeCmd;

-        AssertCmd ac = causalStatement as AssertCmd;

-        ConsoleColor col = Console.ForegroundColor;                              

-        

-        // Trivial case. Must be either assume or assert false

-        if (m_doomedCmds.Count==1) {

-            Console.WriteLine("Found a trivial error:" );

-            if (uc!=null) {

-                Console.Write("Trivial false assumption: " );

-                Console.Write("({0};{1}):", uc.tok.line, uc.tok.col );                

-            }

-            if (ac!=null) {

-                Console.Write("Trivial false assertion: " );

-                Console.Write("({0};{1}):", ac.tok.line, ac.tok.col );                

-            }            

-            causalStatement.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-        } else {

-            // Safety error

-            if (ac!=null) {

-                Console.ForegroundColor = ConsoleColor.Red; 

-                Console.WriteLine("Safety error:");

-                Console.ForegroundColor = col; 

-                Console.Write("This assertion is violated: ");

-                Console.Write("({0};{1}):", ac.tok.line, ac.tok.col );                

-                ac.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-            }

-            if (uc!=null) {

-                bool containsAssert = false;

-                foreach (Cmd! c in m_doomedCmds) {

-                    if (causals.Contains(c) ) {

-                        continue;

-                    }

-                    AssertCmd asrt = c as AssertCmd;

-                    if (asrt!=null) {

-                        containsAssert=true;

-                        break;

-                    }

-                }

-                // Plausibility error

-                if (containsAssert) {

-                    Console.ForegroundColor = ConsoleColor.Yellow ; 

-                    Console.WriteLine("Plausibility error:");

-                    Console.ForegroundColor = col; 

-                    Console.Write("There is no legal exeuction passing: ");

-                    Console.Write("({0};{1})", uc.tok.line, uc.tok.col );

-                    uc.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-                } else { // Reachability error

-                    Console.ForegroundColor = ConsoleColor.DarkRed ; 

-                    Console.WriteLine("Reachability error:");

-                    Console.ForegroundColor = col; 

-                    Console.Write("No execution can reach: ");

-                    Console.Write("({0};{1})", uc.tok.line, uc.tok.col );                

-                    uc.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-                }

-                

-            }  

-            

-            Console.ForegroundColor = ConsoleColor.White; 

-            Console.WriteLine("...on any execution passing through:");

-            foreach (Cmd! c in m_doomedCmds) {

-                if (causals.Contains(c) ) {

-                    continue;

-                }

-                Console.ForegroundColor = col; 

-                Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col );

-                Console.ForegroundColor = ConsoleColor.DarkYellow ;

-                c.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

-            }            

-            Console.ForegroundColor = col;

-            Console.WriteLine("--");

-              

-        }

-    }

-

-    private List<Cmd!>! CollectCausalStatements(Block! b) {

-        Cmd lastCausal=null;

-        foreach (Cmd! c in b.Cmds) {

-            AssertCmd ac = c as AssertCmd;

-            AssumeCmd uc = c as AssumeCmd;

-            if (ac!=null && !ContainsReachVariable(ac)) {

-                if (ac.Expr!=Expr.True) {

-                    lastCausal = c;

-                }

-            } else if (uc!=null && !ContainsReachVariable(uc)) {

-                lastCausal = c;

-            }            

-        }

-        

-        List<Cmd!> causals = new List<Cmd!>();

-        GotoCmd gc = b.TransferCmd as GotoCmd;

-        if (gc!=null && gc.labelTargets!=null) {            

-            List<Cmd!> tmp;

-            //bool allcausal = true;

-            foreach (Block! b_ in gc.labelTargets) {

-                tmp = CollectCausalStatements(b_);

-

-                foreach (Cmd cau in tmp) {

-                    if (!causals.Contains(cau)) causals.Add(cau);

-                }

-            }

-            //if (allcausal) 

-            if (causals.Count>0) return causals;

-        }

-        if (lastCausal!=null) causals.Add( lastCausal);

-        return causals;

-    }

-    

-#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;

-                BruteForceCmd(impl.Blocks[endidx],0,cmdcount/2 -1,reachvar, impl, callback);

-                BruteForceCmd(impl.Blocks[endidx],cmdcount/2,cmdcount-1,reachvar, impl, callback);

-                return true; 

-            } else {                

-                BruteForceCESearch(reachvar,impl, callback, cmdbackup, startidx, mid);

-                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

-   

-  }

-}