Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebug.bpl

3 files changed, 353 insertions, 26 deletions

diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc
index 492f333c..70b026e9 100644
--- a/Source/VCGeneration/DoomCheck.ssc
+++ b/Source/VCGeneration/DoomCheck.ssc
@@ -82,18 +82,20 @@ namespace VC
             }

         }

         

-        private DoomErrorHandler m_ErrHandler;              

-        private Implementation! m_PassiveImpl;

+        private DoomErrorHandler m_ErrHandler;                      

         private Checker! m_Check;        

         private InclusionOrder! m_Order; 

         private Evc! m_Evc;       

         #endregion

         

         [NotDelayed]

-        public DoomCheck (Implementation! passive_impl, Checker! check) {

-            m_PassiveImpl = passive_impl;

-            m_Check = check;            

-            m_Order = new InclusionOrder(passive_impl);

+        public DoomCheck (Implementation! passive_impl, Checker! check) {            

+            m_Check = check;          

+            if (!VC.DCGen.UseItAsDebugger ) {  

+                m_Order = new InclusionOrder(passive_impl.Blocks[0]);

+            } else {

+                m_Order = new InclusionOrder((!)VC.DCGen.firstNonDebugBlock );

+            }

             Label2Absy = new Hashtable(); // This is only a dummy

             m_Evc = new Evc(check);

             base();

@@ -101,6 +103,7 @@ namespace VC
             VCExpr! vce = this.GenerateEVC(passive_impl, out l2a, check);

             assert l2a!=null;

             Label2Absy = l2a;

+//            vce = check.VCExprGen.Implies(vce, vce);

             m_Evc.Initialize(vce);            

         }

 

@@ -138,7 +141,17 @@ namespace VC
 

 

         #region Error Verification Condition Generation

-        

+       /*

+                   #region _TESTING_NEW_STUFF_

+            CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;

+            //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true

+            

+            CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;

+            #endregion

+

+       */ 

+        private bool _tmpUseFreshBVars;

+       

         VCExpr! GenerateEVC(Implementation! impl, out Hashtable label2absy, Checker! ch)

         {

 			    TypecheckingContext tc = new TypecheckingContext(null);

@@ -147,15 +160,48 @@ namespace VC
 			    VCExpr! vc;

 			    switch (CommandLineOptions.Clo.vcVariety) {

 				    case CommandLineOptions.VCVariety.Doomed:

-					    vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);

+

+                        if (!VC.DCGen.UseItAsDebugger ) {

+                            vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);

+                        }

+                        #region _TESTING_NEW_STUFF_

+                        else  {

+                        

+                                                                        

+                        CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;				        

+				        assert VC.DCGen.firstDebugBlock != null;

+				        VCExpr! a = LetVC(VC.DCGen.firstDebugBlock, label2absy, ch.TheoremProver.Context);				        				        				        

+				        CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;			

+

+                        				        

+                        VCExpr! b = LetVC((!)VC.DCGen.firstNonDebugBlock, label2absy, ch.TheoremProver.Context);

+

+					    //_tmpUseFreshBVars=false;

+					    //vc = ch.VCExprGen.Not(ch.VCExprGen.Implies( wp, ch.VCExprGen.Not(vc)));

+					    

+					    vc = ch.VCExprGen.Not(ch.VCExprGen.Implies(ch.VCExprGen.Not(a), ch.VCExprGen.Not(b)));

+					    

+					    

+					    /*

+                            ConsoleColor col = Console.ForegroundColor;

+                            Console.ForegroundColor = ConsoleColor.Green; 					    

+					        Console.WriteLine(vc.ToString());

+                            Console.ForegroundColor = col;   

+                            Console.WriteLine(" ... was asked.");   

+                        */

+                                                                 

+					    }

+					    #endregion

+					    					    

 					    break;

+					    

 				    default:

 					    assert false;  // unexpected enumeration value

 			    }

 			    return vc;      

         }

 

-        VCExpr! LetVC(Block! startBlock,

+        public VCExpr! LetVC(Block! startBlock,

                              Hashtable/*<int, Absy!>*/! label2absy,

                              ProverContext! proverCtxt)

         {

@@ -204,9 +250,11 @@ namespace VC
 

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

             

-            v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);

             bindings.Add(gen.LetBinding(v, vc));

             blockVariables.Add(block, v);

           }

@@ -223,14 +271,14 @@ namespace VC
 

             #region Attributes

             public List<List<Block!>!>! DetectedBlock = new List<List<Block!>!>(); 

-            Implementation! m_Impl;

+            

             InclusionTree! RootNode = new InclusionTree(null);             

             InclusionTree currentNode = null;

             

             #endregion

         

             [NotDelayed]

-            public InclusionOrder(Implementation! impl) {

+            public InclusionOrder(Block! rootblock) {

                 /*

                     We now compute for each block the set of blocks that

                     are reached on every execution reaching this block (dominator).

@@ -238,14 +286,14 @@ namespace VC
                     block and second from the Term block to the current one.

                     Finally we build the union.

                 */

-                m_Impl = impl;                               

+                

                 base();

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

+                Block! exitblock = BreadthFirst(rootblock, map2);

                 BreadthFirstBwd(exitblock, map);               

 

                 foreach (KeyValuePair<Block!, TraceNode!> kvp in map) {

@@ -264,7 +312,7 @@ namespace VC
                                 kvp.Value.Add(t0.block);

                         }

                     } else {

-                        assert false;

+                        //assert false;

                     }

                 }

                                                                

@@ -327,10 +375,13 @@ namespace VC
                         currentNode.HasBeenChecked = true;

                         MarkUndoomedParents(currentNode); 

                         if (cb != null) {

+                            //Console.WriteLine("CE contains: ");

                             foreach (Block! b in cb.TraceNodes)

                             {

+                                //Console.Write("{0}, ", b.Label);                                

                                 MarkUndoomedFromCE(b, RootNode);

                             }

+                            //Console.WriteLine();

                         } else {

                             Console.WriteLine("ErrorHandler is not valid! ------ (DoomCheck)");

                         }

diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc
index 775cd9e0..7a235424 100644
--- a/Source/VCGeneration/VCDoomed.ssc
+++ b/Source/VCGeneration/VCDoomed.ssc
@@ -37,6 +37,213 @@ namespace VC
       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

@@ -47,13 +254,24 @@ namespace VC
     /// </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!>();      

@@ -64,21 +282,63 @@ namespace VC
       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!>();

-      PassifyProgram(impl, program);

+      GenerateReachVars(impl);

+

+      if (UseItAsDebugger) RemoveReachVars((!)firstDebugBlock);

+                          

+      PassifyProgram(impl);

+      

+      

       #endregion

-      //EmitImpl(impl,false);

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

@@ -87,9 +347,19 @@ namespace VC
         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: {                

@@ -117,7 +387,7 @@ namespace VC
         ConsoleColor col = Console.ForegroundColor;

         Console.ForegroundColor = ConsoleColor.Red;              

         Console.WriteLine("  {0} is DOOMED!", impl.Name);

-        Console.ForegroundColor = col;

+        Console.ForegroundColor = col;        

         

         SearchCounterexample(impl, dc.ErrorHandler, callback);

         Console.WriteLine("------------------------------ \n\n");

@@ -130,6 +400,8 @@ namespace VC
       return Outcome.Correct;

     }

     

+    

+    

     private void SearchCounterexample(Implementation! impl, DoomErrorHandler! errh, VerifierCallback! callback) {        

         if (errh.m_Reachvar==null) {

             assert false;

@@ -179,6 +451,7 @@ namespace VC
                         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) {

@@ -752,10 +1025,8 @@ namespace VC
     #endregion 

      

     #region Program Passification

-    

-      private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl, 

-			                  Program! program)

-	  {

+      private void GenerateReachVars(Implementation! impl)

+      {

 	    Hashtable gotoCmdOrigins = new Hashtable();

 	    Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

 	    AddBlocksBetween(impl);

@@ -801,8 +1072,12 @@ namespace VC
             exitBlock = (!)gc.labelTargets[0];

         }

         #endregion	    

-	    GenerateReachabilityPredicates(impl, exitBlock);

-	    	    	    

+	    GenerateReachabilityPredicates(impl, exitBlock);      

+      }

+    

+    

+      private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl)

+	  {	    	    	    

 	    current_impl = impl;

 	    Convert2PassiveCmd(impl);

 	    impl = current_impl;

diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc
index d7692245..9700bc89 100644
--- a/Source/VCGeneration/Wlp.ssc
+++ b/Source/VCGeneration/Wlp.ssc
@@ -85,6 +85,7 @@ namespace VC {
         return gen.Implies(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

 

       } else {

+      Console.WriteLine(cmd.ToString());

         assert false;  // unexpected command

       }

     }