diff options
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 291 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 23 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 19 |
5 files changed, 194 insertions, 149 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 1cbbeabf..1b78afc3 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -117,7 +117,7 @@ void ObjectInvariant() outcome = ProverInterface.Outcome.Undetermined;
Contract.Assert( m_ErrorHandler !=null);
m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverDone.WaitOne();
+ m_Checker.ProverTask.Wait();
try {
outcome = m_Checker.ReadOutcome();
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index a2eb52c8..75cd172a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -396,7 +396,6 @@ namespace Microsoft.Boogie using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
{
- //BoogiePL.Errors.count = 0;
Program program = ParseBoogieProgram(fileNames, false);
if (program == null)
return;
@@ -408,7 +407,6 @@ namespace Microsoft.Boogie PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
- //BoogiePL.Errors.count = 0;
// Do bitvector analysis
if (CommandLineOptions.Clo.DoBitVectorAnalysis)
@@ -776,172 +774,215 @@ namespace Microsoft.Boogie #region Verify each implementation
- var outputs = new StringWriter[stablePrioritizedImpls.Count()];
- var nextPrintableIndex = 0;
+ var outputCollector = new OutputCollector(stablePrioritizedImpls);
+ var outcome = PipelineOutcome.VerificationCompleted;
+ var tasks = new Task[stablePrioritizedImpls.Length];
+ for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
+ {
+ var taskIndex = i;
+ var t = Task.Factory.StartNew(() =>
+ {
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector);
+ });
+ tasks[taskIndex] = t;
+ try
+ {
+ Task.WaitAll(new Task[] { t });
+ }
+ catch (AggregateException ae)
+ {
+ ae.Handle(e =>
+ {
+ var pe = e as ProverException;
+ if (pe != null)
+ {
+ printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
+ outcome = PipelineOutcome.FatalError;
+ return true;
+ }
+ return false;
+ });
+ }
+ }
+
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+ outputCollector.WriteMoreOutput();
+
+ #endregion
+
+ return outcome;
+ }
+
+
+ private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector)
+ {
+ Implementation impl = stablePrioritizedImpls[index];
+ VerificationResult verificationResult = null;
+ var output = new StringWriter();
+
+ printer.Inform(string.Format("\nVerifying {0} ...", impl.Name), output);
+
+ if (CommandLineOptions.Clo.VerifySnapshots)
+ {
+ verificationResult = Cache.Lookup(impl);
+ }
- try
+ if (verificationResult != null)
{
- Parallel.For(0, stablePrioritizedImpls.Count(), new ParallelOptions { MaxDegreeOfParallelism = 1 }, index =>
+ if (CommandLineOptions.Clo.XmlSink != null)
{
- Implementation impl = stablePrioritizedImpls[index];
- VerificationResult verificationResult = null;
- var output = new StringWriter();
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
+ }
- printer.Inform(string.Format("\nVerifying {0} ...", impl.Name), output);
+ printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ }
+ else
+ {
+ #region Verify the implementation
- if (CommandLineOptions.Clo.VerifySnapshots)
- {
- verificationResult = Cache.Lookup(impl);
- }
+ verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);
+ verificationResult.ImplementationName = impl.Name;
+ verificationResult.ImplementationToken = impl.tok;
- if (verificationResult != null)
- {
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
- }
+ using (var vcgen = CreateVCGen(program))
+ {
+ verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
+ verificationResult.Start = DateTime.UtcNow;
- printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
}
- else
+ try
{
- #region Verify the implementation
-
- verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);
- verificationResult.ImplementationName = impl.Name;
- verificationResult.ImplementationToken = impl.tok;
-
- using (var vcgen = CreateVCGen(program))
+ if (CommandLineOptions.Clo.inferLeastForUnsat != null)
{
- verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
- verificationResult.Start = DateTime.UtcNow;
-
- if (CommandLineOptions.Clo.XmlSink != null)
+ var svcgen = vcgen as VC.StratifiedVCGen;
+ Contract.Assert(svcgen != null);
+ var ss = new HashSet<string>();
+ foreach (var tdecl in program.TopLevelDeclarations)
{
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
- }
- try
- {
- if (CommandLineOptions.Clo.inferLeastForUnsat != null)
- {
- var svcgen = vcgen as VC.StratifiedVCGen;
- Contract.Assert(svcgen != null);
- var ss = new HashSet<string>();
- foreach (var tdecl in program.TopLevelDeclarations)
- {
- var c = tdecl as Constant;
- if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
- ss.Add(c.Name);
- }
- verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
- verificationResult.Errors = new List<Counterexample>();
- output.WriteLine("Result: {0}", string.Join(" ", ss));
- }
- else
- {
- verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);
- if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)
- {
- var vcg = vcgen as VCGen;
- if (vcg != null)
- {
- for (int i = 0; i < verificationResult.Errors.Count; i++)
- {
- verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo);
- }
- }
- }
- }
+ var c = tdecl as Constant;
+ if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+ ss.Add(c.Name);
}
- catch (VCGenException e)
+ verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
+ verificationResult.Errors = new List<Counterexample>();
+ output.WriteLine("Result: {0}", string.Join(" ", ss));
+ }
+ else
+ {
+ verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);
+ if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)
{
- var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");
- errorInfo.BoogieErrorCode = "BP5010";
- errorInfo.ImplementationName = impl.Name;
- printer.WriteErrorInformation(errorInfo, output);
- if (er != null)
+ var vcg = vcgen as VCGen;
+ if (vcg != null)
{
- lock (er)
+ for (int i = 0; i < verificationResult.Errors.Count; i++)
{
- er(errorInfo);
+ verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo);
}
}
- verificationResult.Errors = null;
- verificationResult.Outcome = VCGen.Outcome.Inconclusive;
}
- catch (UnexpectedProverOutputException upo)
+ }
+ }
+ catch (VCGenException e)
+ {
+ var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");
+ errorInfo.BoogieErrorCode = "BP5010";
+ errorInfo.ImplementationName = impl.Name;
+ printer.WriteErrorInformation(errorInfo, output);
+ if (er != null)
+ {
+ lock (er)
{
- printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
- verificationResult.Errors = null;
- verificationResult.Outcome = VCGen.Outcome.Inconclusive;
+ er(errorInfo);
}
-
- verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
- verificationResult.End = DateTime.UtcNow;
}
+ verificationResult.Errors = null;
+ verificationResult.Outcome = VCGen.Outcome.Inconclusive;
+ }
+ catch (UnexpectedProverOutputException upo)
+ {
+ printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
+ verificationResult.Errors = null;
+ verificationResult.Outcome = VCGen.Outcome.Inconclusive;
+ }
- #endregion
+ verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
+ verificationResult.End = DateTime.UtcNow;
+ }
- #region Cache the verification result
+ #endregion
- if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
- {
- Cache.Insert(impl.Id, verificationResult);
- }
+ #region Cache the verification result
- #endregion
- }
+ if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
+ {
+ Cache.Insert(impl.Id, verificationResult);
+ }
- #region Process the verification results and statistics
+ #endregion
+ }
- ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
+ #region Process the verification results and statistics
- ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);
- }
+ ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
- outputs[index] = output;
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);
+ }
- lock (outputs)
- {
- for (; nextPrintableIndex < stablePrioritizedImpls.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
- {
- Console.Write(outputs[nextPrintableIndex].ToString());
- Console.Out.Flush();
- }
- }
+ outputCollector.Add(index, output);
- if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
- {
- Console.Out.Flush();
- }
+ outputCollector.WriteMoreOutput();
- #endregion
- });
- }
- catch (ProverException e)
+ if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
{
- printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
- return PipelineOutcome.FatalError;
+ Console.Out.Flush();
}
- cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+ #endregion
+ }
+
+
+ class OutputCollector
+ {
+ StringWriter[] outputs;
- lock (outputs)
+ int nextPrintableIndex = 0;
+
+ public OutputCollector(Implementation[] implementations)
+ {
+ outputs = new StringWriter[implementations.Length];
+ }
+
+ public void WriteMoreOutput()
{
- for (; nextPrintableIndex < stablePrioritizedImpls.Count() && nextPrintableIndex != null; nextPrintableIndex++)
+ lock (outputs)
{
- Console.Write(outputs[nextPrintableIndex].ToString());
- Console.Out.Flush();
+ for (; nextPrintableIndex < outputs.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
+ {
+ Console.Write(outputs[nextPrintableIndex].ToString());
+ Console.Out.Flush();
+ }
}
}
- #endregion
+ public void Add(int index, StringWriter output)
+ {
+ Contract.Requires(0 <= index && index < outputs.Length);
+ Contract.Requires(output != null);
- return PipelineOutcome.VerificationCompleted;
+ lock (this)
+ {
+ outputs[index] = output;
+ }
+ }
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index a0454229..0a1059fe 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -15,6 +15,7 @@ using System.Diagnostics.Contracts; using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
+using System.Threading.Tasks;
namespace Microsoft.Boogie {
/// <summary>
@@ -28,7 +29,6 @@ namespace Microsoft.Boogie { void ObjectInvariant() {
Contract.Invariant(gen != null);
Contract.Invariant(thmProver != null);
- Contract.Invariant(ProverDone != null);
}
private readonly VCExpressionGenerator gen;
@@ -46,7 +46,7 @@ namespace Microsoft.Boogie { private volatile ProverInterface.ErrorHandler handler;
private volatile bool closed;
- public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
+ public Task ProverTask { get; set; }
public bool WillingToHandle(Implementation impl, int timeout) {
return !closed && timeout == this.timeout;
@@ -262,8 +262,6 @@ namespace Microsoft.Boogie { Contract.Assert(busy);
hasOutput = true;
proverRunTime = DateTime.UtcNow - proverStart;
-
- ProverDone.Set();
}
public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
@@ -282,7 +280,7 @@ namespace Microsoft.Boogie { thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
- ThreadPool.QueueUserWorkItem(WaitForOutput);
+ ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); });
}
public ProverInterface.Outcome ReadOutcome() {
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index bcafb9cb..bb2deb29 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -970,23 +970,30 @@ namespace VC { #endregion
- protected Checker FindCheckerFor(Implementation impl, int timeout) {
+ protected Checker FindCheckerFor(Implementation impl, int timeout)
+ {
Contract.Ensures(Contract.Result<Checker>() != null);
- int i = 0;
- while (i < checkers.Count) {
- if (checkers[i].Closed) {
+ // Look for existing checker.
+ for (int i = 0; i < checkers.Count; i++)
+ {
+ if (checkers[i].Closed)
+ {
checkers.RemoveAt(i);
continue;
- } else {
- if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))
- return checkers[i];
}
- ++i;
+ if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))
+ {
+ return checkers[i];
+ }
}
+
+ // Create a new checker.
string log = logFilePath;
if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
+ {
log = log + "." + checkers.Count;
+ }
Checker ch = new Checker(this, program, log, appendLogFile, timeout);
Contract.Assert(ch != null);
checkers.Add(ch);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index bea79f13..121cab46 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -18,6 +18,7 @@ using Microsoft.Boogie.VCExprAST; namespace VC {
using Bpl = Microsoft.Boogie;
+ using System.Threading.Tasks;
public class VCGen : ConditionGeneration {
private const bool _print_time = false;
@@ -312,7 +313,7 @@ namespace VC { Emit();
}
ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
- ch.ProverDone.WaitOne();
+ ch.ProverTask.Wait();
ProverInterface.Outcome outcome = ch.ReadOutcome();
parent.CurrentLocalVariables = null;
@@ -1135,10 +1136,10 @@ namespace VC { }
}
- public WaitHandle ProverDone {
+ public Task ProverTask {
get {
Contract.Assert(checker != null);
- return checker.ProverDone;
+ return checker.ProverTask;
}
}
@@ -1445,11 +1446,11 @@ namespace VC { remaining_cost = work.Peek().Cost;
}
- while (work.Count > 0 || currently_running.Count > 0) {
+ while (work.Any() || currently_running.Any()) {
bool prover_failed = false;
Split s;
- if (work.Count > 0 && currently_running.Count < cores) {
+ if (work.Any() && currently_running.Count < cores) {
s = work.Pop();
if (first_round && max_splits > 1) {
@@ -1473,11 +1474,9 @@ namespace VC { currently_running.Add(s);
}
} else {
- WaitHandle[] handles = new WaitHandle[currently_running.Count];
- for (int i = 0; i < currently_running.Count; ++i) {
- handles[i] = currently_running[i].ProverDone;
- }
- int index = WaitHandle.WaitAny(handles);
+ // 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);
|