diff options
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 23 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 15 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 183 |
3 files changed, 152 insertions, 69 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 7e2ec984..b317dc71 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -115,21 +115,26 @@ void ObjectInvariant() // Todo: Check if vc is trivial true or false
outcome = ProverInterface.Outcome.Undetermined;
- Contract.Assert( m_ErrorHandler !=null);
- m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverTask.Wait();
-
- try {
+ Contract.Assert(m_ErrorHandler != null);
+ try
+ {
+ m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+ m_Checker.ProverTask.Wait();
outcome = m_Checker.ReadOutcome();
- m_Checker.GoBackToIdle();
- } catch (UnexpectedProverOutputException e)
+ }
+ catch (UnexpectedProverOutputException e)
{
- if (CommandLineOptions.Clo.TraceVerify) {
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);
Console.WriteLine(e.ToString());
}
return false;
- }
+ }
+ finally
+ {
+ m_Checker.GoBackToIdle();
+ }
return true;
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 5bc5eba3..62f180d7 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -972,10 +972,11 @@ namespace VC { #endregion
- protected Checker FindCheckerFor(int timeout)
+ protected Checker FindCheckerFor(int timeout, bool isBlocking = true)
{
Contract.Ensures(Contract.Result<Checker>() != null);
+ var maxRetries = 3;
lock (checkers)
{
retry:
@@ -1008,8 +1009,16 @@ namespace VC { if (Cores <= checkers.Count)
{
- Monitor.Wait(checkers, 50);
- goto retry;
+ if (isBlocking || 0 < maxRetries)
+ {
+ Monitor.Wait(checkers, 50);
+ maxRetries--;
+ goto retry;
+ }
+ else
+ {
+ return null;
+ }
}
// Create a new checker.
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 5369d13e..d40b1008 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -312,10 +312,22 @@ namespace VC { System.Console.WriteLine(" --- smoke #{0}, after passify", id);
Emit();
}
- ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
- ch.ProverTask.Wait();
+ try
+ {
+ ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
+ ch.ProverTask.Wait();
+ }
+ catch
+ {
+ throw;
+ }
+ finally
+ {
+ ch.GoBackToIdle();
+ }
+
ProverInterface.Outcome outcome = ch.ReadOutcome();
- ch.GoBackToIdle();
+
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
@@ -1190,13 +1202,16 @@ namespace VC { /// <summary>
/// As a side effect, updates "this.parent.CumulativeAssertionCount".
/// </summary>
- public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
+ public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
+ Contract.Requires(checker != null);
Contract.Requires(callback != null);
+
splitNo = no;
impl.Blocks = blocks;
- checker = parent.FindCheckerFor(timeout);
+ this.checker = checker;
+
lock (checker)
{
Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
@@ -1240,7 +1255,7 @@ namespace VC { }
return vce;
}
- ));
+ ));
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
@@ -1457,101 +1472,155 @@ namespace VC { remaining_cost = work.Peek().Cost;
}
- while (work.Any() || currently_running.Any()) {
+ while (work.Any() || currently_running.Any())
+ {
bool prover_failed = false;
- Split s;
+ Split s = null;
+ var isWaiting = !work.Any();
- if (work.Any() && currently_running.Count < Cores) {
- s = work.Pop();
+ if (!isWaiting)
+ {
+ s = work.Peek();
- if (first_round && max_splits > 1) {
+ if (first_round && max_splits > 1)
+ {
prover_failed = true;
remaining_cost -= s.Cost;
- } else {
- if (CommandLineOptions.Clo.Trace && no >= 0) {
- System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
+ }
+ else
+ {
+ var timeout = (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
+ keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
+ CommandLineOptions.Clo.ProverKillTime;
+
+ var checker = s.parent.FindCheckerFor(timeout, false);
+ if (checker == null)
+ {
+ isWaiting = true;
+ goto waiting;
+ }
+ else
+ {
+ s = work.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace && no >= 0)
+ {
+ System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
}
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
Contract.Assert(s.parent == this);
- s.BeginCheck(callback, mvInfo, no,
- (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
- keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime);
+ s.BeginCheck(checker, callback, mvInfo, no, timeout);
no++;
currently_running.Add(s);
}
- } else {
+ }
+
+ waiting:
+ if (isWaiting)
+ {
// Wait for one split to terminate.
var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();
- int index = Task.WaitAny(tasks);
- s = currently_running[index];
- currently_running.RemoveAt(index);
- if (do_splitting) {
- remaining_cost -= s.Cost;
- }
+ if (tasks.Any())
+ {
+ try
+ {
+ int index = Task.WaitAny(tasks);
+ s = currently_running[index];
+ currently_running.RemoveAt(index);
- s.ReadOutcome(ref outcome, out prover_failed);
+ if (do_splitting)
+ {
+ remaining_cost -= s.Cost;
+ }
- if (do_splitting) {
- if (prover_failed) {
- // even if the prover fails, we have learned something, i.e., it is
- // annoying to watch Boogie say Timeout, 0.00% a couple of times
- proven_cost += s.Cost / 100;
- } else {
- proven_cost += s.Cost;
- }
- }
- callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+ s.ReadOutcome(ref outcome, out prover_failed);
- if (prover_failed && !first_round && s.LastChance) {
- string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
- msg = s.reporter.resourceExceededMessage;
- }
- callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
- outcome = Outcome.Errors;
- break;
- }
+ if (do_splitting)
+ {
+ if (prover_failed)
+ {
+ // even if the prover fails, we have learned something, i.e., it is
+ // annoying to watch Boogie say Timeout, 0.00% a couple of times
+ proven_cost += s.Cost / 100;
+ }
+ else
+ {
+ proven_cost += s.Cost;
+ }
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
- s.Checker.GoBackToIdle();
+ if (prover_failed && !first_round && s.LastChance)
+ {
+ string msg = "some timeout";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
+ outcome = Outcome.Errors;
+ break;
+ }
+ }
+ catch
+ {
+ throw;
+ }
+ finally
+ {
+ s.Checker.GoBackToIdle();
+ }
- Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ Contract.Assert(prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ }
}
- if (prover_failed) {
+ if (prover_failed)
+ {
int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;
- if (splits > 1) {
+ if (splits > 1)
+ {
List<Split> tmp = Split.DoSplit(s, max_vc_cost, splits);
Contract.Assert(tmp != null);
max_vc_cost = 1.0; // for future
first_round = false;
//tmp.Sort(new Comparison<Split!>(Split.Compare));
- foreach (Split a in tmp) {
+ foreach (Split a in tmp)
+ {
Contract.Assert(a != null);
work.Push(a);
total++;
remaining_cost += a.Cost;
}
- if (outcome != Outcome.Errors) {
+ if (outcome != Outcome.Errors)
+ {
outcome = Outcome.Correct;
}
- } else {
- Contract.Assert( outcome != Outcome.Correct);
- if (outcome == Outcome.TimedOut) {
+ }
+ else
+ {
+ Contract.Assert(outcome != Outcome.Correct);
+ if (outcome == Outcome.TimedOut)
+ {
string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnTimeout(msg);
- } else if (outcome == Outcome.OutOfMemory) {
+ }
+ else if (outcome == Outcome.OutOfMemory)
+ {
string msg = "out of memory";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnOutOfMemory(msg);
|