doomed stuff: minor bug fixes / improved output / more test cases

5 files changed, 111 insertions, 25 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 6eb16fa4..b9f3d5b2 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -272,7 +272,11 @@ namespace Microsoft.Boogie
       requires 0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories;

     {

       Console.WriteLine();

-      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+      if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

+      Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+      } else {

+      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");      

+      }

       if (inconclusives != 0) {

         Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

       }

@@ -517,8 +521,8 @@ namespace Microsoft.Boogie
               assert false;  // unexpected outcome

             case VCGen.Outcome.Correct:

               if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-                Inform(String.Format("{0}doomed", timeIndication));

-                errorCount++;

+                Inform(String.Format("{0}credible", timeIndication));

+                verified++;

               } else {

                 Inform(String.Format("{0}verified", timeIndication));

                 verified++;

@@ -538,9 +542,9 @@ namespace Microsoft.Boogie
               break;

             case VCGen.Outcome.Errors:

               if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-                Inform(String.Format("{0}credible", timeIndication));

-                verified++;

-              } else {

+                Inform(String.Format("{0}doomed", timeIndication));

+                errorCount++;                

+              } //else {

                 assert errors != null;  // guaranteed by postcondition of VerifyImplementation

                 if (errorReporter != null)

                 {

@@ -637,7 +641,7 @@ namespace Microsoft.Boogie
                     }

                     errorCount++;

                     }

-                }

+                //}

                 Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

               }

               break;

diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc
index e888d115..cdbdcb6a 100644
--- a/Source/VCGeneration/DoomCheck.ssc
+++ b/Source/VCGeneration/DoomCheck.ssc
@@ -309,8 +309,13 @@ namespace VC
 

                         // Check if there is an assert false in this node or in one of its parents

                         // if so do not report anything

-                        if (ECContainsAssertFalse(currentNode.EquivBlock)) {                        

+                        if (ECContainsAssertFalse(currentNode.EquivBlock)) {  

+                        

+                            ConsoleColor col = Console.ForegroundColor;

+                            Console.ForegroundColor = ConsoleColor.Blue; 

                             Console.WriteLine("Assert false was detected, but ignored");

+                            Console.ForegroundColor = col;                                              

+

                             currentNode.HasBeenChecked = true;  

                             currentNode.IsDoomed = false;                          

                             currentNode = currentNode.Parent; 

@@ -324,7 +329,7 @@ namespace VC
                         

 //                        cb.OnWarning("Doomed program points found!");

                         if (cb != null) {

-                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);

+                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);                            

                         }

                                                 

                         if (currentNode.EquivBlock.Count>0) {

diff --git a/Source/VCGeneration/DoomErrorHandler.ssc b/Source/VCGeneration/DoomErrorHandler.ssc
index 6c8a7ec7..08bc2217 100644
--- a/Source/VCGeneration/DoomErrorHandler.ssc
+++ b/Source/VCGeneration/DoomErrorHandler.ssc
@@ -39,7 +39,7 @@ namespace VC
         public void OnDoom(Variable! reachvar, List<Block!>! doomedblocks, List<Block!>! traceblocks) {

             m_Reachvar = reachvar;

             m_DoomedBlocks = doomedblocks;

-            m_TraceBlocks = traceblocks;

+            m_TraceBlocks = traceblocks;            

         }

     }

     

diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc
index 84df1be4..fc3d35f7 100644
--- a/Source/VCGeneration/VCDoomed.ssc
+++ b/Source/VCGeneration/VCDoomed.ssc
@@ -24,6 +24,7 @@ namespace VC
     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.

@@ -50,7 +51,7 @@ namespace VC
       if (CommandLineOptions.Clo.TraceVerify) { 

         Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);

       }

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

 

       #region Transform the Program into loop-free passive form

@@ -91,8 +92,7 @@ namespace VC
         }

         

         switch (outcome) {

-            case ProverInterface.Outcome.Valid: {

-                Console.WriteLine("[x] {0} is doomed", v.Name);

+            case ProverInterface.Outcome.Valid: {                

                 doomfound=true;

                 break;

             }

@@ -108,11 +108,22 @@ namespace VC
         

       }

       checker.Close();

-      

+      #region Try to produce a counter example (brute force)

       if (dc.DoomedSequences.Count>0 ) {

+

+        ConsoleColor col = Console.ForegroundColor;

+        Console.ForegroundColor = ConsoleColor.Red;              

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

+        Console.ForegroundColor = col;

+        

         SearchCounterexample(impl, dc.ErrorHandler, callback);

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

+        return Outcome.Errors;

       }

-      Console.WriteLine();

+      #endregion

+      

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

+      

       return Outcome.Correct;

     }

     

@@ -121,10 +132,8 @@ namespace VC
             assert false;

             return;

         }

-        Console.WriteLine("{0} is doomed due to the following statements:", errh.m_Reachvar.Name );

-        

-        // modify the impl

-        

+        m_doomedCmds.Clear();

+                

         assert errh.m_TraceBlocks != null;

         assert errh.m_DoomedBlocks !=null;

         List<Block!>! nondoomed = new List<Block!>();

@@ -138,8 +147,24 @@ namespace VC
         

         BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count/2-1);

         BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count/2,impl.Blocks.Count-1);

-                

         

+        BlockSeq! trace = new BlockSeq();

+        foreach (Block! b in cmdbackup.Keys ) {

+            trace.Add(b);

+        }

+        AssertCmd asrt = null;

+        foreach (Cmd! c in m_doomedCmds) {

+            AssertCmd ac = c as AssertCmd;

+            if (ac!=null) {

+                asrt=ac;

+            }

+        }

+        if (asrt==null) {

+            //callback.OnWarning("Sorry, cannot create counterexample");

+        } else {

+            //AssertCounterexample! ace = new AssertCounterexample(trace, asrt);

+            //callback.OnCounterexample(ace, "Todo: Build a reason");        

+        }        

         #region Undo all modifications        

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

             kvp.Key.Cmds = kvp.Value;

@@ -237,9 +262,19 @@ namespace VC
         } else if (outcome == ProverInterface.Outcome.Invalid) {

             b.Cmds = backup;

             if (startidx>=endidx) {

-                if (!ContainsReachVariable(b.Cmds[endidx])) {

-                    Console.Write("Candidate L{0}: ", b.Cmds[endidx].tok.line );

-                    b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

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

diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl
index a153e468..77eec249 100644
--- a/Test/doomed/doomed.bpl
+++ b/Test/doomed/doomed.bpl
@@ -1,5 +1,5 @@
 

-procedure a(x:int)

+procedure evilrequires(x:int)

   requires x>0;

 {

   var y : int;

@@ -12,7 +12,7 @@ procedure a(x:int)
 }

 

 

-procedure b(x:int)

+procedure evilbranch(x:int)

 {

   var y : int;

 

@@ -25,3 +25,45 @@ procedure b(x:int)
 }

 

 

+procedure evilloop(x:int)

+{

+  var y : int;

+  y:=x;

+  while (y<100) {

+     y := y -1;

+  }

+}

+

+procedure evilpath(x:int)

+{

+  var y : int;

+  y:=0;

+  if (x>10) {

+    y:=3;

+  } else {

+    assert y!=0;

+  }

+}

+

+procedure evilcondition(x:int)

+{

+  var y : int;

+  y:=0;

+  if (x!=0) {

+    y:=3;

+  } else {

+    assert x!=0;

+  }

+}

+

+procedure evilensures(x:int) returns  ($result: int)

+  ensures $result>0;

+{

+  var y : int;

+

+  if(x<0) {

+    y := 1;

+  } else {

+    $result:=-1;

+  }

+}