From 99945de38ce51bcc7e2370bffdd00f2f8a203345 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Fri, 27 Sep 2013 21:10:44 +0100 Subject: refactoring + new class ConcurrentHoudini --- Source/Houdini/ConcurrentHoudini.cs | 215 ++++++++++++++++++++++++++++++++++++ Source/Houdini/Houdini.cs | 93 +++++----------- Source/Houdini/Houdini.csproj | 19 +++- 3 files changed, 254 insertions(+), 73 deletions(-) create mode 100644 Source/Houdini/ConcurrentHoudini.cs (limited to 'Source/Houdini') diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs new file mode 100644 index 00000000..ab5fbdcf --- /dev/null +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -0,0 +1,215 @@ +using System; +using System.IO; +using System.Collections.Generic; +using System.Collections.Concurrent; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using System.Text.RegularExpressions; +using System.Linq; + +namespace Microsoft.Boogie.Houdini +{ + public class ConcurrentHoudini : Houdini + { + int id; + +// private static ConcurrentDictionary refutedSharedAnnotations; + private static ConcurrentDictionary refutedSharedAnnotations; + + public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") + : base(program, stats, cexTraceFile) + { + this.id = id; + } + + static ConcurrentHoudini() + { + refutedSharedAnnotations = new ConcurrentDictionary(); + } + + public ConcurrentDictionary RefutedSharedAnnotations { get { return refutedSharedAnnotations; } } + + private bool ExchangeRefutedAnnotations() + { + int count = 0; + + foreach (string key in refutedSharedAnnotations.Keys) { + KeyValuePair kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key) && entry.Value); + RefutedAnnotation ra = refutedSharedAnnotations[key]; + + if (kv.Key != null) { + if (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite); + + AddRelatedToWorkList(ra); + UpdateAssignment(ra); + count++; + } + } + + if (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("# refuted annotations received from the shared exchanging set: " + count); + + 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) { + if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) + 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 (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("# exchange set size: " + refutedSharedAnnotations.Count); + + if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) + 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; + } + + 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]; + } + } + + foreach (Implementation impl in vcgenFailures) { + currentHoudiniState.addToBlackList(impl.Name); + } + + while (currentHoudiniState.WorkQueue.Count > 0) { + this.NotifyIteration(); + + if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) + ExchangeRefutedAnnotations(); + + 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 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); + Console.WriteLine("***ERROR with id {0} --- {1}***", id, errors.Count); + 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; + } + } + } + } +} diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6310c894..60ab6a25 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -6,7 +6,6 @@ using System; using System.Diagnostics.Contracts; using System.Collections.Generic; -using System.Collections.Concurrent; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using VC; @@ -18,7 +17,7 @@ using System.Diagnostics; namespace Microsoft.Boogie.Houdini { - class ReadOnlyDictionary { + internal class ReadOnlyDictionary { private Dictionary dictionary; public ReadOnlyDictionary(Dictionary dictionary) { this.dictionary = dictionary; @@ -306,19 +305,17 @@ namespace Microsoft.Boogie.Houdini { } public class Houdini : ObservableHoudini { - private Program program; - private HashSet houdiniConstants; - private ReadOnlyDictionary houdiniSessions; - private VCGen vcgen; - private ProverInterface proverInterface; - private Graph callGraph; - private HashSet vcgenFailures; - private HoudiniState currentHoudiniState; - private CrossDependencies crossDependencies; - - private static ConcurrentDictionary refutedSharedAnnotations; - - private string cexTraceFile; + protected Program program; + protected HashSet houdiniConstants; + protected VCGen vcgen; + protected ProverInterface proverInterface; + protected Graph callGraph; + protected HashSet vcgenFailures; + protected HoudiniState currentHoudiniState; + protected CrossDependencies crossDependencies; + internal ReadOnlyDictionary houdiniSessions; + + protected string cexTraceFile; public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } } @@ -380,10 +377,6 @@ namespace Microsoft.Boogie.Houdini { } } - static Houdini() { - refutedSharedAnnotations = new ConcurrentDictionary(); - } - private void Inline() { if (CommandLineOptions.Clo.InlineDepth < 0) return; @@ -503,7 +496,7 @@ namespace Microsoft.Boogie.Houdini { public Dictionary> assumedInImpl { get; private set; } } - private WorkQueue BuildWorkList(Program program) { + protected WorkQueue BuildWorkList(Program program) { // adding implementations to the workqueue from the bottom of the call graph upwards WorkQueue queue = new WorkQueue(); StronglyConnectedComponents sccs = @@ -641,7 +634,7 @@ namespace Microsoft.Boogie.Houdini { return null; } - private Dictionary BuildAssignment(HashSet constants) { + protected Dictionary BuildAssignment(HashSet constants) { Dictionary initial = new Dictionary(); foreach (var constant in constants) initial.Add(constant, true); @@ -666,7 +659,7 @@ namespace Microsoft.Boogie.Houdini { // Record most current non-candidate errors found // Return true if there was at least one non-candidate error - private bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome, + protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome, Implementation implementation, ProverInterface.Outcome outcome, List errors) { @@ -684,7 +677,7 @@ namespace Microsoft.Boogie.Houdini { return nonCandidateErrors.Count > 0; } - private void FlushWorkList(int stage, IEnumerable completedStages) { + protected void FlushWorkList(int stage, IEnumerable completedStages) { this.NotifyFlushStart(); while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); @@ -705,30 +698,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyFlushFinish(); } - private bool ExchangeRefutedAnnotations() - { - int count = 0; - - foreach (RefutedAnnotation key in refutedSharedAnnotations.Keys) { - KeyValuePair kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(key.Constant.Name) && entry.Value); - - if (kv.Key != null) { - if (CommandLineOptions.Clo.DebugParallelHoudini) - Console.WriteLine("(+) " + key.Constant + "," + key.Kind + "," + key.CalleeProc + "," + key.RefutationSite); - - AddRelatedToWorkList(key); - UpdateAssignment(key); - count++; - } - } - - if (CommandLineOptions.Clo.DebugParallelHoudini) - Console.WriteLine("# refuted annotations received from the shared exchanging set: " + count); - - return count > 0 ? true : false; - } - - private void UpdateAssignment(RefutedAnnotation refAnnot) { + protected void UpdateAssignment(RefutedAnnotation refAnnot) { if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Removing " + refAnnot.Constant); using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) @@ -739,7 +709,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyConstant(refAnnot.Constant.Name); } - private void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) { + protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) { Contract.Assume(currentHoudiniState.Implementation != null); foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, refutedAnnotation.RefutationSite)) { if (!currentHoudiniState.isBlackListed(implementation.Name)) { @@ -751,7 +721,7 @@ namespace Microsoft.Boogie.Houdini { // Updates the worklist and current assignment // @return true if the current function is dequeued - private bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, + protected virtual bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, List errors) { Contract.Assume(currentHoudiniState.Implementation != null); bool dequeue = true; @@ -770,8 +740,6 @@ namespace Microsoft.Boogie.Houdini { RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); if (refutedAnnotation != null) { // some candidate annotation removed - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - refutedSharedAnnotations.TryAdd (refutedAnnotation, 0); AddRelatedToWorkList(refutedAnnotation); UpdateAssignment(refutedAnnotation); dequeue = false; @@ -792,12 +760,6 @@ namespace Microsoft.Boogie.Houdini { #endregion } } - - if (CommandLineOptions.Clo.DebugParallelHoudini) - Console.WriteLine("# exchange set size: " + refutedSharedAnnotations.Count); - - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - if (ExchangeRefutedAnnotations()) dequeue = false; break; default: @@ -889,7 +851,7 @@ namespace Microsoft.Boogie.Houdini { } } - public HoudiniOutcome PerformHoudiniInference(int stage = 0, + public virtual HoudiniOutcome PerformHoudiniInference(int stage = 0, IEnumerable completedStages = null, Dictionary initialAssignment = null) { this.NotifyStart(program, houdiniConstants.Count); @@ -909,9 +871,6 @@ namespace Microsoft.Boogie.Houdini { while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - ExchangeRefutedAnnotations(); - currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); this.NotifyImplementation(currentHoudiniState.Implementation); @@ -983,9 +942,9 @@ namespace Microsoft.Boogie.Houdini { return implementations; } - private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT }; + public enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT }; - private class RefutedAnnotation { + public class RefutedAnnotation { private Variable _constant; private RefutedAnnotationKind _kind; private Procedure _callee; @@ -1074,7 +1033,7 @@ namespace Microsoft.Boogie.Houdini { } } - private void DebugRefutedCandidates(Implementation curFunc, List errors) { + protected void DebugRefutedCandidates(Implementation curFunc, List errors) { XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted; if (xmlRefuted != null && errors != null) { DateTime start = DateTime.UtcNow; @@ -1094,7 +1053,7 @@ namespace Microsoft.Boogie.Houdini { } } - private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) { + protected RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) { Variable houdiniConstant; CallCounterexample callCounterexample = error as CallCounterexample; if (callCounterexample != null) { @@ -1125,7 +1084,7 @@ namespace Microsoft.Boogie.Houdini { return null; } - private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable completedStages, out List errors) { + protected 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); @@ -1157,7 +1116,7 @@ namespace Microsoft.Boogie.Houdini { return result; } - private void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable completedStages) { + protected virtual void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable completedStages) { while (true) { this.NotifyAssignment(currentHoudiniState.Assignment); diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 6c98c2a8..140d40aa 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -54,12 +54,18 @@ False False False - - - - - - + + + + + + + + + + + + False Full Build @@ -85,6 +91,7 @@ + -- cgit v1.2.3