From 0c37d049e8ec31512a554d4304c6aa72c67fbda6 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Fri, 26 Jul 2013 15:58:02 +0100 Subject: parallel houdini prototype working --- Source/Core/CommandLineOptions.cs | 16 +++ Source/Houdini/Houdini.cs | 217 ++++++++++++++++++++++++++++++++------ 2 files changed, 202 insertions(+), 31 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index db7551ce..46f74004 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -397,6 +397,8 @@ namespace Microsoft.Boogie { public bool IntraproceduralInfer = true; public bool ContractInfer = false; public bool ExplainHoudini = false; + public bool HoudiniOutputRefutedCandidates = false; + public bool DebugParallelHoudini = false; public bool HoudiniUseCrossDependencies = false; public string StagedHoudini = null; public bool DebugStagedHoudini = false; @@ -1165,6 +1167,18 @@ namespace Microsoft.Boogie { } return true; + case "outputRefuted": + if (ps.ConfirmArgumentCount(0)) { + HoudiniOutputRefutedCandidates = true; + } + return true; + + case "debugParallelHoudini": + if (ps.ConfirmArgumentCount(0)) { + DebugParallelHoudini = true; + } + return true; + case "vcBrackets": ps.GetNumericArgument(ref BracketIdsInVC, 2); return true; @@ -1652,6 +1666,8 @@ namespace Microsoft.Boogie { /printInstrumented print Boogie program after it has been instrumented with invariants + /outputRefuted + Outputs the refuted candidates ---- Debugging and general tracing options --------------------------------- diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index afae3143..59a7d193 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -698,6 +698,121 @@ namespace Microsoft.Boogie.Houdini { this.NotifyFlushFinish(); } + private List ExchangeRefutedAnnotations(List newlyRefuted) + { + List result = newlyRefuted; +// List knownRefutedInformation = new List(); + string refutedInformation; + + if (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("# refuted annotations before exchange: " + result.Count); + + using (var fileStream = new FileStream(@"houdini.txt", FileMode.OpenOrCreate, FileAccess.ReadWrite, FileShare.ReadWrite)) + using (var input = new StreamReader(fileStream)) + using (var output = new StreamWriter(fileStream)) { + while ((refutedInformation = input.ReadLine()) != null) { +// knownRefutedInformation.Add(refutedInformation); + var ri = refutedInformation.Split(','); + + KeyValuePair kv = currentHoudiniState.Assignment.FirstOrDefault(entry => entry.Key.Name.Equals(ri[0]) && entry.Value); + + if (kv.Key != null) { + RefutedAnnotation ra = null; + Implementation refutationSite = null; + + foreach (var r in program.TopLevelDeclarations.OfType()) { + if (r.Name.Equals(ri[3])) { + refutationSite = r; + break; + } + } + Debug.Assert(refutationSite != null); + + if (ri[1].Equals("REQUIRES")) { + Procedure proc = null; + foreach (var p in program.TopLevelDeclarations.OfType()) { + if (p.Name.Equals(ri[2])) { + proc = p; + break; + } + } + Debug.Assert(proc != null); + ra = RefutedAnnotation.BuildRefutedRequires(kv.Key, proc, refutationSite); + } else if (ri[1].Equals("ENSURES")) + ra = RefutedAnnotation.BuildRefutedEnsures(kv.Key, refutationSite); + else if (ri[1].Equals("ASSERT")) + ra = RefutedAnnotation.BuildRefutedAssert(kv.Key, refutationSite); + Debug.Assert(ra != null); + + result.Add(ra); + if (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("(+) " + refutedInformation); + } + +// foreach (KeyValuePair entry in currentHoudiniState.Assignment) { +// if (entry.Key.Name.Equals(ri[0]) && entry.Value) { +// RefutedAnnotation ra = null; +// Implementation refutationSite = null; +// +// foreach (var r in program.TopLevelDeclarations.OfType()) { +// if (r.Name.Equals(ri[3])) { +// refutationSite = r; +// break; +// } +// } +// Debug.Assert(refutationSite != null); +// +// if (ri[1].Equals("REQUIRES")) { +// Procedure proc = null; +// foreach (var p in program.TopLevelDeclarations.OfType()) { +// if (p.Name.Equals(ri[2])) { +// proc = p; +// break; +// } +// } +// Debug.Assert(proc != null); +// ra = RefutedAnnotation.BuildRefutedRequires(entry.Key, proc, refutationSite); +// } else if (ri[1].Equals("ENSURES")) +// ra = RefutedAnnotation.BuildRefutedEnsures(entry.Key, refutationSite); +// else if (ri[1].Equals("ASSERT")) +// ra = RefutedAnnotation.BuildRefutedAssert(entry.Key, refutationSite); +// Debug.Assert(ra != null); +// +// //if (!result.Contains(ra)) { +// result.Add(ra); +// if (CommandLineOptions.Clo.DebugStagedHoudini) +// Console.WriteLine("(+) " + refutedInformation); +// //} +// +// break; +// } +// } + +// foreach (RefutedAnnotation refAnnot in newlyRefuted) { +// if (refAnnot.Constant != ra.Constant || refAnnot.Kind != ra.Kind || +// refAnnot.CalleeProc != ra.CalleeProc || refAnnot.RefutationSite != ra.RefutationSite) { +// result.Add(ra); +// if (CommandLineOptions.Clo.DebugStagedHoudini) +// Console.WriteLine("(+) " + knownRefutedInformation.LastOrDefault()); +// } +// } + } + + if (CommandLineOptions.Clo.DebugParallelHoudini) + Console.WriteLine("# refuted annotations after exchange: " + result.Count); + + foreach (RefutedAnnotation refAnnot in result) { +// string ri = refAnnot.Constant + "," + refAnnot.Kind + "," + +// refAnnot.CalleeProc + "," + currentHoudiniState.Implementation; +// if (!knownRefutedInformation.Contains(ri)) + output.WriteLine(refAnnot.Constant + "," + refAnnot.Kind + "," + + refAnnot.CalleeProc + "," + currentHoudiniState.Implementation); + } + } + + return result; + } + private void UpdateAssignment(RefutedAnnotation refAnnot) { if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Removing " + refAnnot.Constant); @@ -711,7 +826,7 @@ namespace Microsoft.Boogie.Houdini { private void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) { Contract.Assume(currentHoudiniState.Implementation != null); - foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, currentHoudiniState.Implementation)) { + foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, refutedAnnotation.RefutationSite)) { if (!currentHoudiniState.isBlackListed(implementation.Name)) { currentHoudiniState.WorkQueue.Enqueue(implementation); this.NotifyEnqueue(implementation); @@ -731,32 +846,67 @@ namespace Microsoft.Boogie.Houdini { case ProverInterface.Outcome.Valid: //yeah, dequeue break; + 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); + + if (CommandLineOptions.Clo.HoudiniOutputRefutedCandidates) { + List refutedAnnotations = new List(); + + foreach (Counterexample error in errors) { + RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); + if (refutedAnnotation != null) { // some candidate annotation removed + refutedAnnotations.Add(refutedAnnotation); + + #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); + } + } + #endregion + } + } + + refutedAnnotations = ExchangeRefutedAnnotations(refutedAnnotations); + + foreach (RefutedAnnotation refAnnot in refutedAnnotations) { + AddRelatedToWorkList(refAnnot); + UpdateAssignment(refAnnot); dequeue = false; - #region Extra debugging output - if (CommandLineOptions.Clo.Trace) - { - using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) + } + } else { + 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) { - 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(); + 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; @@ -946,11 +1096,13 @@ namespace Microsoft.Boogie.Houdini { private Variable _constant; private RefutedAnnotationKind _kind; private Procedure _callee; + private Implementation _refutationSite; - private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee) { + private RefutedAnnotation(Variable constant, RefutedAnnotationKind kind, Procedure callee, Implementation refutationSite) { this._constant = constant; this._kind = kind; this._callee = callee; + this._refutationSite = refutationSite; } public RefutedAnnotationKind Kind { get { return this._kind; } @@ -961,14 +1113,17 @@ namespace Microsoft.Boogie.Houdini { public Procedure CalleeProc { get { return this._callee; } } - public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee) { - return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee); + public Implementation RefutationSite { + get { return this._refutationSite; } + } + public static RefutedAnnotation BuildRefutedRequires(Variable constant, Procedure callee, Implementation refutationSite) { + return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee, refutationSite); } - public static RefutedAnnotation BuildRefutedEnsures(Variable constant) { - return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null); + public static RefutedAnnotation BuildRefutedEnsures(Variable constant, Implementation refutationSite) { + return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null, refutationSite); } - public static RefutedAnnotation BuildRefutedAssert(Variable constant) { - return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null); + public static RefutedAnnotation BuildRefutedAssert(Variable constant, Implementation refutationSite) { + return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null, refutationSite); } } @@ -1024,7 +1179,7 @@ namespace Microsoft.Boogie.Houdini { Requires failingRequires = callCounterexample.FailingRequires; if (MatchCandidate(failingRequires.Condition, out houdiniConstant)) { Contract.Assert(houdiniConstant != null); - return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure); + return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure, currentHoudiniState.Implementation); } } ReturnCounterexample returnCounterexample = error as ReturnCounterexample; @@ -1032,7 +1187,7 @@ namespace Microsoft.Boogie.Houdini { Ensures failingEnsures = returnCounterexample.FailingEnsures; if (MatchCandidate(failingEnsures.Condition, out houdiniConstant)) { Contract.Assert(houdiniConstant != null); - return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant); + return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant, currentHoudiniState.Implementation); } } AssertCounterexample assertCounterexample = error as AssertCounterexample; @@ -1040,7 +1195,7 @@ namespace Microsoft.Boogie.Houdini { AssertCmd failingAssert = assertCounterexample.FailingAssert; if (MatchCandidate(failingAssert.OrigExpr, out houdiniConstant)) { Contract.Assert(houdiniConstant != null); - return RefutedAnnotation.BuildRefutedAssert(houdiniConstant); + return RefutedAnnotation.BuildRefutedAssert(houdiniConstant, currentHoudiniState.Implementation); } } -- cgit v1.2.3