From d5574270cc5d424f1b3ec6a8021f9ef42c2c265b Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 30 May 2013 09:12:51 -0700 Subject: Changed the prover interface to report traces for time outs and out of memory. --- Source/BoogieDriver/BoogieDriver.cs | 192 +++++++++++++++++------------ Source/Provers/SMTLib/ProverInterface.cs | 2 +- Source/VCGeneration/ConditionGeneration.cs | 2 +- Test/test2/Answer | 24 ++++ Test/test2/Timeouts0.bpl | 25 ++++ Test/test2/runtest.bat | 4 + 6 files changed, 170 insertions(+), 79 deletions(-) create mode 100644 Test/test2/Timeouts0.bpl 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 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 -- cgit v1.2.3