From 5715e950f0bbfa08760f5da3c0b1c8028be82984 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Wed, 28 May 2014 09:36:48 +0100 Subject: Refactored ConcurrentHoudini and Houdini to (significantly) reduce duplication of code --- Source/Houdini/ConcurrentHoudini.cs | 243 +++--------------------------------- 1 file changed, 20 insertions(+), 223 deletions(-) (limited to 'Source/Houdini/ConcurrentHoudini.cs') 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 refutedSharedAnnotations; public static ConcurrentDictionary 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()); - this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id); - - vcgenFailures = new HashSet(); - Dictionary houdiniSessions = new Dictionary(); - 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(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(); } - 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 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 completedStages = null, - Dictionary 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 assignment = new Dictionary(); - 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 completedStages) - { - while (true) { - this.NotifyAssignment(currentHoudiniState.Assignment); - - //check the VC with the current assignment - List 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(errors); - var refutedAnnotations = new List(); - 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 completedStages, out List 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; - } } } -- cgit v1.2.3