Changed the prover interface to report traces for time outs and out of memory.

6 files changed, 170 insertions, 79 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 26763f95..99e9ee9e 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -520,94 +520,132 @@ namespace Microsoft.Boogie {
           if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

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

             errorCount++;

-          } //else {

+          }

           Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+          break;

+      }

+      if (errors != null)      

+      {

+        // BP1xxx: Parsing errors

+        // BP2xxx: Name resolution errors

+        // BP3xxx: Typechecking errors

+        // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+        // BP5xxx: Verification errors

+

+        var cause = "Error";

+        if (outcome == VCGen.Outcome.TimedOut)

+        {

+          cause = "Timed out on";

+        }

+        else if (outcome == VCGen.Outcome.OutOfMemory)

+        {

+          cause = "Out of memory on";

+        }

+        // TODO(wuestholz): Take the error cause into account when writing to the XML sink.

 

+        errors.Sort(new CounterexampleComparer());

+        foreach (Counterexample error in errors)

+        {

+          if (error is CallCounterexample)

+          {

+            CallCounterexample err = (CallCounterexample)error;

+            if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null)

+            {

+              ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

+            }

+            else

+            {

+              ReportBplError(err.FailingCall, cause + " BP5002: A precondition for this call might not hold.", true, true);

+              ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+            }

+            if (CommandLineOptions.Clo.XmlSink != null)

+            {

+              CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+            }

+          }

+          else if (error is ReturnCounterexample)

+          {

+            ReturnCounterexample err = (ReturnCounterexample)error;

+            if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null)

+            {

+              ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

+            }

+            else

+            {

+              ReportBplError(err.FailingReturn, cause + " BP5003: A postcondition might not hold on this return path.", true, true);

+              ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+            }

+            if (CommandLineOptions.Clo.XmlSink != null)

+            {

+              CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+            }

+          }

+          else // error is AssertCounterexample

+          {

+            AssertCounterexample err = (AssertCounterexample)error;

+            if (err.FailingAssert is LoopInitAssertCmd)

+            {

+              ReportBplError(err.FailingAssert, cause + " BP5004: This loop invariant might not hold on entry.", true, true);

+              if (CommandLineOptions.Clo.XmlSink != null)

               {

-            // BP1xxx: Parsing errors

-            // BP2xxx: Name resolution errors

-            // BP3xxx: Typechecking errors

-            // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-            // BP5xxx: Verification errors

-

-            errors.Sort(new CounterexampleComparer());

-            foreach (Counterexample error in errors) {

-              if (error is CallCounterexample) {

-                CallCounterexample err = (CallCounterexample)error;

-                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) {

-                  ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

-                }

-                else {

-                  ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true);

-                  ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

-                }

-                if (CommandLineOptions.Clo.XmlSink != null) {

-                  CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

-                }

+                CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

               }

-              else if (error is ReturnCounterexample) {

-                ReturnCounterexample err = (ReturnCounterexample)error;

-                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) {

-                  ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

-                }

-                else {

-                  ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true);

-                  ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

-                }

-                if (CommandLineOptions.Clo.XmlSink != null) {

-                  CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

-                }

+            }

+            else if (err.FailingAssert is LoopInvMaintainedAssertCmd)

+            {

+              // this assertion is a loop invariant which is not maintained

+              ReportBplError(err.FailingAssert, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true);

+              if (CommandLineOptions.Clo.XmlSink != null)

+              {

+                CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

               }

-              else // error is AssertCounterexample

-                    {

-                AssertCounterexample err = (AssertCounterexample)error;

-                if (err.FailingAssert is LoopInitAssertCmd) {

-                  ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true);

-                  if (CommandLineOptions.Clo.XmlSink != null) {

-                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

-                  }

-                }

-                else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

-                  // this assertion is a loop invariant which is not maintained

-                  ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true);

-                  if (CommandLineOptions.Clo.XmlSink != null) {

-                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

-                  }

-                }

-                else {

-                  if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) {

-                    ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

-                  }

-                  else if (err.FailingAssert.ErrorData is string) {

-                    ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

-                  }

-                  else {

-                    ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true);

-                  }

-                  if (CommandLineOptions.Clo.XmlSink != null) {

-                    CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

-                  }

-                }

+            }

+            else

+            {

+              if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null)

+              {

+                ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

               }

-              if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

-                foreach (string info in error.relatedInformation) {

-                  Contract.Assert(info != null);

-                  Console.WriteLine("       " + info);

-                }

+              else if (err.FailingAssert.ErrorData is string)

+              {

+                ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

               }

-              if (CommandLineOptions.Clo.ErrorTrace > 0) {

-                Console.WriteLine("Execution trace:");

-                error.Print(4);

+              else

+              {

+                ReportBplError(err.FailingAssert, cause + " BP5001: This assertion might not hold.", true, true);

               }

-              if (CommandLineOptions.Clo.ModelViewFile != null) {

-                error.PrintModel();

+              if (CommandLineOptions.Clo.XmlSink != null)

+              {

+                CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

               }

-              errorCount++;

             }

-            //}

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

           }

-              break;

+          if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)

+          {

+            foreach (string info in error.relatedInformation)

+            {

+              Contract.Assert(info != null);

+              Console.WriteLine("       " + info);

+            }

+          }

+          if (CommandLineOptions.Clo.ErrorTrace > 0)

+          {

+            Console.WriteLine("Execution trace:");

+            error.Print(4);

+          }

+          if (CommandLineOptions.Clo.ModelViewFile != null)

+          {

+            error.PrintModel();

+          }

+          if (cause == "Error")

+          {

+            errorCount++;

+          }

+        }

+        if (cause == "Error")

+        {

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

+        }

       }

     }

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 7cd3b3cd..de9be1b9 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -776,7 +776,7 @@ namespace Microsoft.Boogie.SMTLib
           if (globalResult == Outcome.Undetermined)

             globalResult = result;

 

-          if (result == Outcome.Invalid) {

+          if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

             IList<string> xlabels;

             if (CommandLineOptions.Clo.UseLabels) {

               labels = GetLabelsInfo();

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cabc9d9e..dc9f496b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -597,7 +597,7 @@ namespace VC {
 

       CounterexampleCollector collector = new CounterexampleCollector();

       Outcome outcome = VerifyImplementation(impl, collector);

-      if (outcome == Outcome.Errors) {

+      if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory) {

         errors = collector.examples;

       } else {

         errors = null;

diff --git a/Test/test2/Answer b/Test/test2/Answer
index b936ef87..5f8642e1 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -480,3 +480,27 @@ Execution trace:
     ContractEvaluationOrder.bpl(23,5): anon0

 

 Boogie program verifier finished with 1 verified, 3 errors

+

+-------------------- Timeouts0.bpl --------------------

+Timeouts0.bpl(12,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.

+Execution trace:

+    Timeouts0.bpl(8,7): anon0

+    Timeouts0.bpl(10,5): anon4_LoopHead

+    Timeouts0.bpl(14,20): anon4_LoopBody

+Timeouts0.bpl(19,5): Timed out on BP5003: A postcondition might not hold on this return path.

+Timeouts0.bpl(4,3): Related location: This is the postcondition that might not hold.

+Execution trace:

+    Timeouts0.bpl(8,7): anon0

+    Timeouts0.bpl(10,5): anon4_LoopHead

+    Timeouts0.bpl(10,5): anon4_LoopDone

+    Timeouts0.bpl(19,5): anon5_LoopHead

+    Timeouts0.bpl(19,5): anon5_LoopDone

+Timeouts0.bpl(21,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.

+Execution trace:

+    Timeouts0.bpl(8,7): anon0

+    Timeouts0.bpl(10,5): anon4_LoopHead

+    Timeouts0.bpl(10,5): anon4_LoopDone

+    Timeouts0.bpl(19,5): anon5_LoopHead

+    Timeouts0.bpl(23,11): anon5_LoopBody

+

+Boogie program verifier finished with 0 verified, 0 errors, 1 time out

diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl
new file mode 100644
index 00000000..c74e9320
--- /dev/null
+++ b/Test/test2/Timeouts0.bpl
@@ -0,0 +1,25 @@
+procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)

+  requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);

+  requires 0 < len;

+  ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);

+{

+    var i : int;

+

+    i := 0;

+    out[i] := 0;

+    while (i < len)

+      invariant 0 <= i && i <= len;

+      invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);

+    {

+        out[i + 1] := out[i] + 1;

+        i := i + 1;

+    }

+

+    i := 0;

+    while (i < len)

+      invariant 0 <= i && i <= len;

+      invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);

+    {

+        i := i + 1;

+    }

+}

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 89715252..1c10c6e8 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -32,3 +32,7 @@ for %%f in (ContractEvaluationOrder.bpl) do (
   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

 )

+

+echo.

+echo -------------------- Timeouts0.bpl --------------------

+%BGEXE% %* /timeLimit:4 Timeouts0.bpl