diff options
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 3 | ||||
| -rw-r--r-- | Source/Houdini/ConcurrentHoudini.cs | 243 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 173 | ||||
| -rw-r--r-- | Source/Houdini/StagedHoudini.cs | 23 | ||||
| -rw-r--r-- | Test/AbsHoudini/Answer | 8 |
5 files changed, 130 insertions, 320 deletions
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 0da1c5d9..ea891dd6 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -518,13 +518,10 @@ namespace Microsoft.Boogie.Houdini { {
Stage.AddCandidate(c);
}
- Console.Write(n.Count() + ", ");
AssignedToThisStage.Add(n);
}
}
- Console.WriteLine("total: " + Stage.Count());
-
foreach(var n in AssignedToThisStage) {
done[n] = Stage;
}
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index b92cb7bc..bfc96258 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -12,69 +12,19 @@ namespace Microsoft.Boogie.Houdini { public class ConcurrentHoudini : Houdini { - int id; + + protected int taskID; private static ConcurrentDictionary<string, RefutedAnnotation> refutedSharedAnnotations; public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnotations { get { return refutedSharedAnnotations; } } - public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { - Contract.Assert(id >= 0); - - this.id = id; + public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { + Contract.Assert(taskId >= 0); this.program = program; this.cexTraceFile = cexTraceFile; - - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Collecting existential constants..."); - this.houdiniConstants = CollectExistentialConstants(); - - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Building call graph..."); - this.callGraph = Program.BuildCallGraph(program); - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count); - - if (CommandLineOptions.Clo.HoudiniUseCrossDependencies) - { - if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ..."); - this.crossDependencies = new CrossDependencies(this.houdiniConstants); - this.crossDependencies.Visit(program); - } - - Inline(); - - 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, id); - - vcgenFailures = new HashSet<Implementation>(); - Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>(); - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Beginning VC generation for Houdini..."); - foreach (Implementation impl in callGraph.Nodes) { - try { - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Generating VC for {0}", impl.Name); - HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id); - houdiniSessions.Add(impl, session); - } - catch (VCGenException) { - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("VC generation failed"); - vcgenFailures.Add(impl); - } - } - this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions); - - if (CommandLineOptions.Clo.ExplainHoudini) - { - // Print results of ExplainHoudini to a dotty file - explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot"); - explainHoudiniDottyFile.WriteLine("digraph explainHoudini {"); - foreach (var constant in houdiniConstants) - explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name); - explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];"); - } + this.taskID = taskId; + Initialize(program, stats); } static ConcurrentHoudini() @@ -82,7 +32,7 @@ namespace Microsoft.Boogie.Houdini refutedSharedAnnotations = new ConcurrentDictionary<string, RefutedAnnotation>(); } - private bool ExchangeRefutedAnnotations() + protected override bool ExchangeRefutedAnnotations() { int count = 0; @@ -132,176 +82,23 @@ namespace Microsoft.Boogie.Houdini return count > 0 ? true : false; } - protected override bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, - List<Counterexample> errors) - { - Contract.Assume(currentHoudiniState.Implementation != null); - bool dequeue = true; - - switch (outcome) { - case ProverInterface.Outcome.Valid: - //yeah, dequeue - break; - - case ProverInterface.Outcome.Invalid: - Contract.Assume(errors != null); - - foreach (Counterexample error in errors) { - RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); - // some candidate annotation removed - if (refutedAnnotation != null) { - refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation); - AddRelatedToWorkList(refutedAnnotation); - UpdateAssignment(refutedAnnotation); - dequeue = false; - - #region Extra debugging output - if (CommandLineOptions.Clo.Trace) { - using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) { - cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant); - cexWriter.Write(error.ToString()); - cexWriter.WriteLine(); - using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter)) - foreach (Microsoft.Boogie.Block blk in error.Trace) - blk.Emit(writer, 15); - //cexWriter.WriteLine(); - } - } - #endregion - } - } - - if (ExchangeRefutedAnnotations()) dequeue = false; - - break; - default: - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name); - } - - HoudiniSession houdiniSession; - houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession); - - foreach (Variable v in houdiniSession.houdiniAssertConstants) { - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Removing " + v); - } - currentHoudiniState.Assignment.Remove(v); - currentHoudiniState.Assignment.Add(v, false); - this.NotifyConstant(v.Name); - } - - currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name); - break; - } - - return dequeue; + protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) { + refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation); } - - public override HoudiniOutcome PerformHoudiniInference(int stage = 0, - IEnumerable<int> completedStages = null, - Dictionary<string, bool> initialAssignment = null) - { - this.NotifyStart(program, houdiniConstants.Count); - - currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants)); - - if (initialAssignment != null) { - foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) { - currentHoudiniState.Assignment[v] = initialAssignment[v.Name]; - } - } - - if (refutedSharedAnnotations.Count > 0) { - foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) { - if (refutedSharedAnnotations.ContainsKey(v.Name)) { - currentHoudiniState.Assignment[v] = false; - } - } - } - - foreach (Implementation impl in vcgenFailures) { - currentHoudiniState.addToBlackList(impl.Name); - } - - while (currentHoudiniState.WorkQueue.Count > 0) { - this.NotifyIteration(); - - currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); - this.NotifyImplementation(currentHoudiniState.Implementation); - - HoudiniSession session; - this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); - HoudiniVerifyCurrent(session, stage, completedStages); - } - - this.NotifyEnd(true); - Dictionary<string, bool> assignment = new Dictionary<string, bool>(); - foreach (var x in currentHoudiniState.Assignment) - assignment[x.Key.Name] = x.Value; - currentHoudiniState.Outcome.assignment = assignment; - return currentHoudiniState.Outcome; +
+ protected override void ApplyRefutedSharedAnnotations() {
+ if (refutedSharedAnnotations.Count > 0) {
+ foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {
+ if (refutedSharedAnnotations.ContainsKey(v.Name)) {
+ currentHoudiniState.Assignment[v] = false;
+ }
+ }
+ }
} - protected override void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) - { - while (true) { - this.NotifyAssignment(currentHoudiniState.Assignment); - - //check the VC with the current assignment - List<Counterexample> errors; - ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors); - this.NotifyOutcome(outcome); - - DebugRefutedCandidates(currentHoudiniState.Implementation, errors); - - #region Explain Houdini - if (CommandLineOptions.Clo.ExplainHoudini && outcome == ProverInterface.Outcome.Invalid) - { - Contract.Assume(errors != null); - // make a copy of this variable - errors = new List<Counterexample>(errors); - var refutedAnnotations = new List<RefutedAnnotation>(); - foreach (Counterexample error in errors) - { - RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); - if (refutedAnnotation == null || refutedAnnotation.Kind == RefutedAnnotationKind.ASSERT) continue; - refutedAnnotations.Add(refutedAnnotation); - } - foreach (var refutedAnnotation in refutedAnnotations) - { - session.Explain(proverInterface, currentHoudiniState.Assignment, refutedAnnotation.Constant); - } - } - #endregion - - if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort - currentHoudiniState.WorkQueue.Dequeue(); - this.NotifyDequeue(); - FlushWorkList(stage, completedStages); - return; - } - else if (UpdateAssignmentWorkList(outcome, errors)) { - if (CommandLineOptions.Clo.UseUnsatCoreForContractInfer && outcome == ProverInterface.Outcome.Valid) - session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment); - currentHoudiniState.WorkQueue.Dequeue(); - this.NotifyDequeue(); - return; - } - } + protected override int GetTaskID() { + return taskID; } - protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) { - ProverInterface.Outcome outcome; - try { - outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id); - } - catch (UnexpectedProverOutputException upo) { - Contract.Assume(upo != null); - errors = null; - outcome = ProverInterface.Outcome.Undetermined; - } - return outcome; - } } } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 393c71eb..adb86598 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -322,28 +322,30 @@ namespace Microsoft.Boogie.Houdini { public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
this.program = program;
this.cexTraceFile = cexTraceFile;
+ Initialize(program, stats);
+ }
+ protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats) {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Collecting existential constants...");
this.houdiniConstants = CollectExistentialConstants();
-
+
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Building call graph...");
this.callGraph = Program.BuildCallGraph(program);
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
- if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
- {
- if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
- this.crossDependencies = new CrossDependencies(this.houdiniConstants);
- this.crossDependencies.Visit(program);
+ if (CommandLineOptions.Clo.HoudiniUseCrossDependencies) {
+ if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
+ this.crossDependencies = new CrossDependencies(this.houdiniConstants);
+ this.crossDependencies.Visit(program);
}
Inline();
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);
+ this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
vcgenFailures = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
@@ -353,10 +355,9 @@ namespace Microsoft.Boogie.Houdini { try {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Generating VC for {0}", impl.Name);
- HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats);
+ HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
houdiniSessions.Add(impl, session);
- }
- catch (VCGenException) {
+ } catch (VCGenException) {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("VC generation failed");
vcgenFailures.Add(impl);
@@ -364,14 +365,13 @@ namespace Microsoft.Boogie.Houdini { }
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
- if (CommandLineOptions.Clo.ExplainHoudini)
- {
- // Print results of ExplainHoudini to a dotty file
- explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
- explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
- foreach (var constant in houdiniConstants)
- explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
- explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
+ if (CommandLineOptions.Clo.ExplainHoudini) {
+ // Print results of ExplainHoudini to a dotty file
+ explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
+ explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
+ foreach (var constant in houdiniConstants)
+ explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
+ explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
}
}
@@ -720,71 +720,96 @@ namespace Microsoft.Boogie.Houdini { // Updates the worklist and current assignment
// @return true if the current function is dequeued
- protected virtual bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,
+ protected bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,
List<Counterexample> errors) {
Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;
- switch (outcome)
- {
- case ProverInterface.Outcome.Valid:
- //yeah, dequeue
- break;
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ //yeah, dequeue
+ break;
- case ProverInterface.Outcome.Invalid:
- Contract.Assume(errors != null);
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
- foreach (Counterexample error in errors)
- {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation != null)
- { // some candidate annotation removed
- AddRelatedToWorkList(refutedAnnotation);
- UpdateAssignment(refutedAnnotation);
- dequeue = false;
- #region Extra debugging output
- if (CommandLineOptions.Clo.Trace)
- {
- using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))
- {
- cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
- cexWriter.Write(error.ToString());
- cexWriter.WriteLine();
- using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
- foreach (Microsoft.Boogie.Block blk in error.Trace)
- blk.Emit(writer, 15);
- //cexWriter.WriteLine();
- }
+ foreach (Counterexample error in errors) {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null) {
+ // some candidate annotation removed
+ ShareRefutedAnnotation(refutedAnnotation);
+ AddRelatedToWorkList(refutedAnnotation);
+ UpdateAssignment(refutedAnnotation);
+ dequeue = false;
+ #region Extra debugging output
+ if (CommandLineOptions.Clo.Trace) {
+ using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) {
+ cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
+ cexWriter.Write(error.ToString());
+ cexWriter.WriteLine();
+ using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
+ foreach (Microsoft.Boogie.Block blk in error.Trace)
+ blk.Emit(writer, 15);
+ //cexWriter.WriteLine();
}
- #endregion
}
+ #endregion
}
+ }
- break;
- default:
- if (CommandLineOptions.Clo.Trace)
- {
- Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
- }
- HoudiniSession houdiniSession;
- houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
- foreach (Variable v in houdiniSession.houdiniAssertConstants)
- {
- if (CommandLineOptions.Clo.Trace)
- {
- Console.WriteLine("Removing " + v);
- }
- currentHoudiniState.Assignment.Remove(v);
- currentHoudiniState.Assignment.Add(v, false);
- this.NotifyConstant(v.Name);
- }
- currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
- break;
+ if (ExchangeRefutedAnnotations()) dequeue = false;
+
+ break;
+ default:
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
+ }
+ HoudiniSession houdiniSession;
+ houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
+ foreach (Variable v in houdiniSession.houdiniAssertConstants) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Removing " + v);
+ }
+ currentHoudiniState.Assignment.Remove(v);
+ currentHoudiniState.Assignment.Add(v, false);
+ this.NotifyConstant(v.Name);
+ }
+ currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
+ break;
}
return dequeue;
}
+ // This method is a hook used by ConcurrentHoudini to
+ // exchange refuted annotations with other Houdini engines.
+ // If the method returns true, this indicates that at least
+ // one new refutation was received from some other engine.
+ // In the base class we thus return false.
+ protected virtual bool ExchangeRefutedAnnotations() {
+ return false;
+ }
+
+ // This method is a hook used by ConcurrentHoudini to
+ // apply a set of existing refuted annotations at the
+ // start of inference.
+ protected virtual void ApplyRefutedSharedAnnotations() {
+ // Empty in base class; can be overridden.
+ }
+
+ // This method is a hook used by ConcurrentHoudini to
+ // broadcast to other Houdini engines the fact that an
+ // annotation was refuted.
+ protected virtual void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) {
+ // Empty in base class; can be overridden.
+ }
+
+ // Hook for ConcurrentHoudini, which requires a task id.
+ // Non-concurrent Houdini has -1 as a task id
+ protected virtual int GetTaskID() {
+ return -1;
+ }
+
public class WorkQueue {
private Queue<Implementation> queue;
private HashSet<Implementation> set;
@@ -857,7 +882,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- public virtual HoudiniOutcome PerformHoudiniInference(int stage = 0,
+ public HoudiniOutcome PerformHoudiniInference(int stage = 0,
IEnumerable<int> completedStages = null,
Dictionary<string, bool> initialAssignment = null) {
this.NotifyStart(program, houdiniConstants.Count);
@@ -870,6 +895,8 @@ namespace Microsoft.Boogie.Houdini { }
}
+ ApplyRefutedSharedAnnotations();
+
foreach (Implementation impl in vcgenFailures) {
currentHoudiniState.addToBlackList(impl.Name);
}
@@ -1059,7 +1086,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- protected RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
+ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
Variable houdiniConstant;
CallCounterexample callCounterexample = error as CallCounterexample;
if (callCounterexample != null) {
@@ -1090,10 +1117,10 @@ namespace Microsoft.Boogie.Houdini { return null;
}
- protected virtual ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+ private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
ProverInterface.Outcome outcome;
try {
- outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);
+ outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: GetTaskID());
}
catch (UnexpectedProverOutputException upo) {
Contract.Assume(upo != null);
@@ -1122,7 +1149,7 @@ namespace Microsoft.Boogie.Houdini { return result;
}
- protected virtual void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) {
+ private void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) {
while (true) {
this.NotifyAssignment(currentHoudiniState.Assignment);
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs index c306afd8..a3b02250 100644 --- a/Source/Houdini/StagedHoudini.cs +++ b/Source/Houdini/StagedHoudini.cs @@ -123,9 +123,7 @@ namespace Microsoft.Boogie.Houdini outcomes.Where(Item => plan.Contains(Item.Key)).
Select(Item => Item.Value).
Select(Item => Item.assignment).ToList();
- //outcomes.Values.Select(Item => Item.assignment).ToList();
completedStages = plan.GetDependences(s).Select(Item => Item.GetId());
- //completedStages = outcomes.Keys.Select(Item => Item.GetId());
}
if (relevantAssignments.Count() > 0)
@@ -158,23 +156,14 @@ namespace Microsoft.Boogie.Houdini private List<Houdini> AcquireHoudiniInstance()
{
- List<Houdini> h = null;
- do
- {
- foreach (var houdini in houdiniInstances)
- {
- if (Monitor.TryEnter(houdini))
- {
- h = houdini;
- break;
- }
- else
- {
- Thread.Sleep(20);
+ while(true) {
+ foreach (var houdini in houdiniInstances) {
+ if (Monitor.TryEnter(houdini)) {
+ return houdini;
}
+ Thread.Sleep(20);
}
- } while (h == null);
- return h;
+ }
}
private void EmitProgram(string filename)
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index db2f6631..f0136d80 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -236,11 +236,11 @@ function {:existential true} {:inline} b1(x: bool) : bool {
false
}
-fail1.bpl(14,3): Error BP5001: This assertion might not hold.
+fail1.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- fail1.bpl(9,3): anon0
- fail1.bpl(10,11): anon4_Then
- fail1.bpl(14,3): anon3
+ fail1.bpl(11,3): anon0
+ fail1.bpl(12,11): anon4_Then
+ fail1.bpl(16,3): anon3
Boogie program verifier finished with 0 verified, 1 error
.
|