diff options
| -rw-r--r-- | Source/Core/Absy.cs | 9 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 3 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 14 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 | ||||
| -rw-r--r-- | Test/test2/Answer | 44 | ||||
| -rw-r--r-- | Test/test2/Timeouts0.bpl | 58 |
6 files changed, 120 insertions, 10 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 43523b55..5e69b179 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1186,6 +1186,15 @@ namespace Microsoft.Boogie { }
}
+ public int TimeLimit
+ {
+ get
+ {
+ int tl = CommandLineOptions.Clo.ProverKillTime;
+ CheckIntAttribute("timeLimit", ref tl);
+ return tl;
+ }
+ }
public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name)
: base(tok) {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 37d5b51b..a9bd25ee 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1491,6 +1491,9 @@ namespace Microsoft.Boogie { Assign a unique ID to an implementation to be used for verification
result caching (default: ""<impl. name>:0"").
+ {:timeLimit N}
+ Set the time limit for a given implementation.
+
---- On functions ----------------------------------------------------------
{:builtin ""spec""}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 0874541b..0064ee49 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1013,7 +1013,7 @@ namespace Microsoft.Boogie #region Process the verification results and statistics
- ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
@@ -1136,7 +1136,7 @@ namespace Microsoft.Boogie foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
{
- ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(x.errors, x.outcome, Console.Out, er);
}
//errorCount = outcome.ErrorCount;
@@ -1163,7 +1163,7 @@ namespace Microsoft.Boogie // Run Abstract Houdini
var abs = new Houdini.AbsHoudini(program, domain);
var absout = abs.ComputeSummaries();
- ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er);
+ ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(absout.errors, absout.outcome, Console.Out, er);
//Houdini.PredicateAbs.Initialize(program);
@@ -1192,7 +1192,7 @@ namespace Microsoft.Boogie private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
- PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
+ PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
{
Contract.Requires(stats != null);
@@ -1200,11 +1200,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
- ReportOutcome(outcome, er, implName, implTok, requestId, tw);
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
}
- private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
{
ErrorInformation errorInfo = null;
@@ -1216,7 +1216,7 @@ namespace Microsoft.Boogie case VCGen.Outcome.TimedOut:
if (implName != null && implTok != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
}
break;
case VCGen.Outcome.OutOfMemory:
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 89bcdbfa..80ffa072 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1495,7 +1495,7 @@ namespace VC { {
var timeout = (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime;
+ impl.TimeLimit;
var checker = s.parent.FindCheckerFor(timeout, false);
if (checker == null)
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5f8642e1..e9390250 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -502,5 +502,45 @@ Execution trace: 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
+Timeouts0.bpl(41,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(43,20): anon4_LoopBody
+Timeouts0.bpl(48,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(48,5): anon5_LoopDone
+Timeouts0.bpl(50,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(52,11): anon5_LoopBody
+Timeouts0.bpl(70,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(72,20): anon4_LoopBody
+Timeouts0.bpl(77,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(77,5): anon5_LoopDone
+Timeouts0.bpl(79,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(81,11): anon5_LoopBody
+
+Boogie program verifier finished with 0 verified, 0 errors, 3 time outs
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index c74e9320..c874a1c1 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -23,3 +23,61 @@ procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) i := i + 1;
}
}
+
+
+procedure TestTimeouts1(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);
+
+implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
+{
+ 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;
+ }
+}
+
+
+procedure TestTimeouts2(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);
+
+implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
+{
+ 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;
+ }
+}
|