summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Doomed/DoomCheck.cs1
-rw-r--r--Source/Doomed/VCDoomed.cs8
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs27
-rw-r--r--Source/Houdini/AbstractHoudini.cs4
-rw-r--r--Source/Houdini/Houdini.cs2
-rw-r--r--Source/VCGeneration/Check.cs61
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs72
-rw-r--r--Source/VCGeneration/FixedpointVC.cs4
-rw-r--r--Source/VCGeneration/StratifiedVC.cs12
-rw-r--r--Source/VCGeneration/VC.cs13
10 files changed, 131 insertions, 73 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 1b78afc3..7e2ec984 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -121,6 +121,7 @@ void ObjectInvariant()
try {
outcome = m_Checker.ReadOutcome();
+ m_Checker.GoBackToIdle();
} catch (UnexpectedProverOutputException e)
{
if (CommandLineOptions.Clo.TraceVerify) {
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index fadb2ea7..778ae767 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -34,8 +34,8 @@ namespace VC {
/// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
- public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program) {
+ public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, checkers) {
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -115,7 +115,7 @@ namespace VC {
//Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
- Checker checker = FindCheckerFor(impl, 1000);
+ Checker checker = FindCheckerFor(1000);
Contract.Assert(checker != null);
int assertionCount;
DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);
@@ -173,7 +173,7 @@ namespace VC {
if (restartTP)
{
checker.Close();
- checker = FindCheckerFor(impl, 1000);
+ checker = FindCheckerFor(1000);
dc.RespawnChecker(impl, checker);
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ab029cb0..71f8cee7 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -776,18 +776,19 @@ namespace Microsoft.Boogie
var outputCollector = new OutputCollector(stablePrioritizedImpls);
var outcome = PipelineOutcome.VerificationCompleted;
+ var checkers = new List<Checker>();
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);
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);
});
tasks[taskIndex] = t;
try
{
- Task.WaitAll(new Task[] { t });
+ Task.WaitAll(t);
}
catch (AggregateException ae)
{
@@ -804,6 +805,14 @@ namespace Microsoft.Boogie
});
}
}
+ lock (checkers)
+ {
+ foreach (Checker checker in checkers)
+ {
+ Contract.Assert(checker != null);
+ checker.Close();
+ }
+ }
cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
@@ -815,7 +824,7 @@ namespace Microsoft.Boogie
}
- private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector)
+ private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers)
{
Implementation impl = stablePrioritizedImpls[index];
VerificationResult verificationResult = null;
@@ -846,7 +855,7 @@ namespace Microsoft.Boogie
verificationResult.ImplementationName = impl.Name;
verificationResult.ImplementationToken = impl.tok;
- using (var vcgen = CreateVCGen(program))
+ using (var vcgen = CreateVCGen(program, checkers))
{
verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
verificationResult.Start = DateTime.UtcNow;
@@ -987,24 +996,24 @@ namespace Microsoft.Boogie
}
- private static ConditionGeneration CreateVCGen(Program program)
+ private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)
{
ConditionGeneration vcgen = null;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
{
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
}
else if (CommandLineOptions.Clo.FixedPointEngine != null)
{
- vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
}
else if (CommandLineOptions.Clo.StratifiedInlining > 0)
{
- vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
}
else
{
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
}
return vcgen;
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index a9fae923..24a3c708 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -98,7 +98,7 @@ namespace Microsoft.Boogie.Houdini {
Inline();
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
this.proverTime = TimeSpan.Zero;
@@ -2053,7 +2053,7 @@ namespace Microsoft.Boogie.Houdini {
if (CommandLineOptions.Clo.ProverKillTime > 0)
CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
this.reporter = new AbstractHoudiniErrorReporter();
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4dd985b4..abc5a7e8 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -349,7 +349,7 @@ namespace Microsoft.Boogie.Houdini {
Inline();
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
vcgenFailures = new HashSet<Implementation>();
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 0a1059fe..d214517a 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -18,6 +18,15 @@ using Microsoft.Basetypes;
using System.Threading.Tasks;
namespace Microsoft.Boogie {
+
+ enum CheckerStatus
+ {
+ Idle,
+ Ready,
+ Busy,
+ Closed
+ }
+
/// <summary>
/// Interface to the theorem prover specialized to Boogie.
///
@@ -38,18 +47,32 @@ namespace Microsoft.Boogie {
// state for the async interface
private volatile ProverInterface.Outcome outcome;
- private volatile bool busy;
private volatile bool hasOutput;
private volatile UnexpectedProverOutputException outputExn;
private DateTime proverStart;
private TimeSpan proverRunTime;
private volatile ProverInterface.ErrorHandler handler;
- private volatile bool closed;
+ private volatile CheckerStatus status;
+ public readonly Program Program;
+
+ public void GetReady()
+ {
+ Contract.Requires(status == CheckerStatus.Idle);
+
+ status = CheckerStatus.Ready;
+ }
+
+ public void GoBackToIdle()
+ {
+ Contract.Requires(IsBusy);
+
+ status = CheckerStatus.Idle;
+ }
public Task ProverTask { get; set; }
- public bool WillingToHandle(Implementation impl, int timeout) {
- return !closed && timeout == this.timeout;
+ public bool WillingToHandle(int timeout, Program prog) {
+ return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);
}
public VCExpressionGenerator VCExprGen {
@@ -107,6 +130,7 @@ namespace Microsoft.Boogie {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
+ this.Program = prog;
ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
@@ -195,9 +219,9 @@ namespace Microsoft.Boogie {
/// <summary>
/// Clean-up.
/// </summary>
- public void Close() {
- this.closed = true;
+ public void Close() {
thmProver.Close();
+ status = CheckerStatus.Closed;
}
/// <summary>
@@ -212,13 +236,21 @@ namespace Microsoft.Boogie {
public bool IsBusy {
get {
- return busy;
+ return status == CheckerStatus.Busy;
}
}
- public bool Closed {
+ public bool IsClosed {
get {
- return closed;
+ return status == CheckerStatus.Closed;
+ }
+ }
+
+ public bool IsIdle
+ {
+ get
+ {
+ return status == CheckerStatus.Idle;
}
}
@@ -259,7 +291,6 @@ namespace Microsoft.Boogie {
break;
}
- Contract.Assert(busy);
hasOutput = true;
proverRunTime = DateTime.UtcNow - proverStart;
}
@@ -268,10 +299,9 @@ namespace Microsoft.Boogie {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
+ Contract.Requires(status == CheckerStatus.Ready);
- Contract.Requires(!IsBusy);
- Contract.Assert(!busy);
- busy = true;
+ status = CheckerStatus.Busy;
hasOutput = false;
outputExn = null;
this.handler = handler;
@@ -280,16 +310,15 @@ namespace Microsoft.Boogie {
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
- ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); });
+ ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); }/* , TaskCreationOptions.LongRunning*/);
}
public ProverInterface.Outcome ReadOutcome() {
-
Contract.Requires(IsBusy);
Contract.Requires(HasOutput);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
hasOutput = false;
- busy = false;
if (outputExn != null) {
throw outputExn;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index bb2deb29..2fe32500 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -527,8 +527,8 @@ namespace VC {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
}
- public ConditionGenerationContracts(Program p)
- : base(p) {
+ public ConditionGenerationContracts(Program p, List<Checker> checkers)
+ : base(p, checkers) {
}
}
@@ -570,7 +570,7 @@ namespace VC {
public int CumulativeAssertionCount; // for statistics
- protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
+ protected readonly List<Checker>/*!>!*/ checkers;
private bool _disposed;
@@ -586,9 +586,10 @@ namespace VC {
public static List<Model> errorModelList;
- public ConditionGeneration(Program p) {
- Contract.Requires(p != null);
+ public ConditionGeneration(Program p, List<Checker> checkers) {
+ Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers));
program = p;
+ this.checkers = checkers;
}
/// <summary>
@@ -970,42 +971,57 @@ namespace VC {
#endregion
- protected Checker FindCheckerFor(Implementation impl, int timeout)
+ protected Checker FindCheckerFor(int timeout)
{
Contract.Ensures(Contract.Result<Checker>() != null);
- // Look for existing checker.
- for (int i = 0; i < checkers.Count; i++)
+ lock (checkers)
{
- if (checkers[i].Closed)
+ retry:
+ // Look for existing checker.
+ for (int i = 0; i < checkers.Count; i++)
{
- checkers.RemoveAt(i);
- continue;
+ var c = checkers.ElementAt(i);
+ lock (c)
+ {
+ if (c.WillingToHandle(timeout, program))
+ {
+ c.GetReady();
+ return c;
+ }
+ else if (c.IsIdle || c.IsClosed)
+ {
+ checkers.RemoveAt(i);
+ if (c.IsIdle)
+ {
+ c.Close();
+ }
+ continue;
+ }
+ }
}
- if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))
+
+ if (1 < checkers.Count)
{
- return checkers[i];
+ Monitor.Wait(checkers, 50);
+ goto retry;
}
- }
- // 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);
- return ch;
+ // 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);
+ ch.GetReady();
+ checkers.Add(ch);
+ return ch;
+ }
}
virtual public void Close() {
- foreach (Checker checker in checkers) {
- Contract.Assert(checker != null);
- checker.Close();
- }
}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 19feabe9..3299ef76 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -78,8 +78,8 @@ namespace Microsoft.Boogie
private static Checker old_checker = null;
- public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)
- : base(_program, logFilePath, appendLogFile)
+ public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(_program, logFilePath, appendLogFile, checkers)
{
switch (CommandLineOptions.Clo.FixedPointMode)
{
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 9e0dd798..b4db817f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -309,8 +309,8 @@ namespace VC {
public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public ProverInterface prover;
- public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile) {
+ public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers) {
implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
foreach (Declaration decl in program.TopLevelDeclarations) {
@@ -510,8 +510,8 @@ namespace VC {
public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree,
HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,
- Program program, string/*?*/ logFilePath, bool appendLogFile)
- : this(program, logFilePath, appendLogFile)
+ Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : this(program, logFilePath, appendLogFile, checkers)
{
this.procsToSkip = new HashSet<string>(procsToSkip);
this.extraRecBound = new Dictionary<string, int>(extraRecBound);
@@ -525,8 +525,8 @@ namespace VC {
}
}
- public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile) {
+ public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers) {
PersistCallTree = false;
useSummary = false;
procsThatReachedRecBound = new HashSet<string>();
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 121cab46..fdadafac 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -26,8 +26,8 @@ namespace VC {
/// Constructor. Initializes the theorem prover.
/// </summary>
[NotDelayed]
- public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program)
+ public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, checkers)
{
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -291,7 +291,7 @@ namespace VC {
ModelViewInfo mvInfo;
parent.PassifyImpl(impl, out mvInfo);
Hashtable label2Absy;
- Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
+ Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
var exprGen = ch.TheoremProver.Context.ExprGen;
@@ -315,6 +315,7 @@ namespace VC {
ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
ch.ProverTask.Wait();
ProverInterface.Outcome outcome = ch.ReadOutcome();
+ ch.GoBackToIdle();
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
@@ -1192,7 +1193,7 @@ namespace VC {
impl.Blocks = blocks;
- checker = parent.FindCheckerFor(impl, timeout);
+ checker = parent.FindCheckerFor(timeout);
Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
ProverInterface tp = checker.TheoremProver;
@@ -1201,7 +1202,7 @@ namespace VC {
bet.SetCodeExprConverter(
new CodeExprConverter(
delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {
- VCGen vcgen = new VCGen(new Program(), null, false);
+ VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
vcgen.CurrentLocalVariables = codeExpr.LocVars;
@@ -1507,6 +1508,8 @@ namespace VC {
break;
}
+ s.Checker.GoBackToIdle();
+
Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 03:50:21 +0000