From bcb6fdad0da726bbee87f1a62c921a8190a4931a Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 27 Apr 2012 20:21:47 -0700 Subject: unsat core for houdini --- Source/BoogieDriver/BoogieDriver.cs | 6 ++- Source/Core/CommandLineOptions.cs | 2 + Source/Houdini/Checker.cs | 104 ++++++++++++++++++++++++++++++------ Source/Houdini/Houdini.cs | 98 ++++++++++++++++----------------- 4 files changed, 144 insertions(+), 66 deletions(-) (limited to 'Source') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index ed70f14e..0459c2ea 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -616,7 +616,8 @@ namespace Microsoft.Boogie { Console.WriteLine(x.Key + " = " + x.Value); } } - if (CommandLineOptions.Clo.Trace) { + if (CommandLineOptions.Clo.Trace) + { int numTrueAssigns = 0; foreach (var x in outcome.assignment) { if (x.Value) @@ -625,7 +626,10 @@ namespace Microsoft.Boogie { Console.WriteLine("Number of true assignments = " + numTrueAssigns); Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns)); Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime); + Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime); Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries); + Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries); + Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings); } foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) { diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 1827b12e..6e5617cf 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -389,6 +389,7 @@ namespace Microsoft.Boogie { public int /*(0:3)*/ ErrorTrace = 1; public bool IntraproceduralInfer = true; public bool ContractInfer = false; + public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; public int InlineDepth = -1; public bool UseUncheckedContracts = false; @@ -1231,6 +1232,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || + ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ) { diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index b837e61a..1a7cd1cf 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -15,22 +15,67 @@ using System.Threading; using VC; namespace Microsoft.Boogie.Houdini { + public class ExistentialConstantCollector : StandardVisitor { + public static HashSet CollectHoudiniConstants(Houdini houdini, Implementation impl) { + ExistentialConstantCollector collector = new ExistentialConstantCollector(houdini); + collector.VisitImplementation(impl); + return collector.houdiniConstants; + } + private ExistentialConstantCollector(Houdini houdini) { + this.houdini = houdini; + this.houdiniConstants = new HashSet(); + } + private Houdini houdini; + private HashSet houdiniConstants; + public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertRequiresCmd(node); + } + public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertEnsuresCmd(node); + } + public override Cmd VisitAssertCmd(AssertCmd node) { + AddHoudiniConstant(node); + return base.VisitAssertCmd(node); + } + public override Cmd VisitAssumeCmd(AssumeCmd node) { + AddHoudiniConstant(node); + return base.VisitAssumeCmd(node); + } + private void AddHoudiniConstant(PredicateCmd node) { + Variable houdiniConstant; + if (houdini.MatchCandidate(node.Expr, out houdiniConstant)) + houdiniConstants.Add(houdiniConstant); + } + } + public class HoudiniSession { public static double proverTime = 0; public static int numProverQueries = 0; + public static double unsatCoreProverTime = 0; + public static int numUnsatCoreProverQueries = 0; + public static int numUnsatCorePrunings = 0; + public string descriptiveName; private VCExpr conjecture; private ProverInterface.ErrorHandler handler; ConditionGeneration.CounterexampleCollector collector; HashSet unsatCoreSet; + HashSet houdiniConstants; + Houdini houdini; + Implementation implementation; public bool InUnsatCore(Variable constant) { if (unsatCoreSet == null) return true; - return unsatCoreSet.Contains(constant); + if (unsatCoreSet.Contains(constant)) + return true; + numUnsatCorePrunings++; + return false; } - public HoudiniSession(VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) { + public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) { descriptiveName = impl.Name; collector = new ConditionGeneration.CounterexampleCollector(); collector.OnProgress("HdnVCGen", 0, 0, 0.0); @@ -38,11 +83,13 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl, program); ModelViewInfo mvInfo; Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo); - Hashtable/**/ label2absy; + + houdiniConstants = ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl); var exprGen = proverInterface.Context.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - + + Hashtable/**/ label2absy; conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context); if (!CommandLineOptions.Clo.UseLabels) { VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); @@ -60,6 +107,9 @@ namespace Microsoft.Boogie.Houdini { else { handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, proverInterface.Context, program); } + + this.houdini = houdini; + this.implementation = impl; } private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary currentAssignment) { @@ -68,6 +118,7 @@ namespace Microsoft.Boogie.Houdini { VCExpressionGenerator exprGen = proverInterface.VCExprGen; VCExpr expr = VCExpressionGenerator.True; + foreach (KeyValuePair kv in currentAssignment) { Variable constant = kv.Key; VCExprVar exprVar = exprTranslator.LookupVariable(constant); @@ -78,22 +129,47 @@ namespace Microsoft.Boogie.Houdini { expr = exprGen.And(expr, exprGen.Not(exprVar)); } } + + /* + foreach (Variable constant in this.houdiniConstants) { + VCExprVar exprVar = exprTranslator.LookupVariable(constant); + if (currentAssignment[constant]) { + expr = exprGen.And(expr, exprVar); + } + else { + expr = exprGen.And(expr, exprGen.Not(exprVar)); + } + } + */ return expr; } public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary assignment, out List errors) { collector.examples.Clear(); - VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture); if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Verifying " + descriptiveName); } DateTime now = DateTime.UtcNow; + VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture); proverInterface.BeginCheck(descriptiveName, vc, handler); ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler); -#if UNSAT_CORE + double queryTime = (DateTime.UtcNow - now).TotalSeconds; + proverTime += queryTime; + numProverQueries++; + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Time taken = " + queryTime); + } + + errors = collector.examples; + return proverOutcome; + } + + public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary assignment) { + DateTime now = DateTime.UtcNow; + Boogie2VCExprTranslator exprTranslator = proverInterface.Context.BoogieExprTranslator; proverInterface.Push(); proverInterface.Assert(conjecture, false); @@ -109,22 +185,16 @@ namespace Microsoft.Boogie.Houdini { assumptionExprs.Add(exprTranslator.LookupVariable(v)); } List unsatCore; - ProverInterface.Outcome proverOutcome = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler); + ProverInterface.Outcome tmp = proverInterface.CheckAssumptions(assumptionExprs, out unsatCore, handler); + System.Diagnostics.Debug.Assert(tmp == ProverInterface.Outcome.Valid); unsatCoreSet = new HashSet(); foreach (int i in unsatCore) unsatCoreSet.Add(assumptionVars[i]); proverInterface.Pop(); -#endif - - double queryTime = (DateTime.UtcNow - now).TotalSeconds; - proverTime += queryTime; - numProverQueries++; - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Time taken = " + queryTime); - } - errors = collector.examples; - return proverOutcome; + double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds; + unsatCoreProverTime += unsatCoreQueryTime; + numUnsatCoreProverQueries++; } } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 5f60feff..53c49e02 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -309,7 +309,9 @@ namespace Microsoft.Boogie.Houdini { private ProverInterface proverInterface; private Graph callGraph; private HashSet vcgenFailures; + private HoudiniState currentHoudiniState; + public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } } private ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) { Contract.Requires(prog != null); @@ -395,7 +397,7 @@ namespace Microsoft.Boogie.Houdini { try { if (CommandLineOptions.Clo.Trace) Console.WriteLine("Generating VC for {0}", impl.Name); - HoudiniSession session = new HoudiniSession(vcgen, proverInterface, program, impl); + HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl); houdiniSessions.Add(impl, session); } catch (VCGenException) { @@ -405,6 +407,7 @@ namespace Microsoft.Boogie.Houdini { } } this.houdiniSessions = new ReadOnlyDictionary(houdiniSessions); + currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants)); } private void Inline() { @@ -531,7 +534,7 @@ namespace Microsoft.Boogie.Houdini { */ } - private bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) { + public bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) { candidateConstant = null; IExpr antecedent; IExpr expr = boogieExpr as IExpr; @@ -588,41 +591,41 @@ namespace Microsoft.Boogie.Houdini { return nonCandidateErrors.Count > 0; } - private void FlushWorkList(HoudiniState current) { + private void FlushWorkList() { this.NotifyFlushStart(); - while (current.WorkQueue.Count > 0) { + while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); - current.Implementation = current.WorkQueue.Peek(); - this.NotifyImplementation(current.Implementation); + currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); + this.NotifyImplementation(currentHoudiniState.Implementation); HoudiniSession session; - houdiniSessions.TryGetValue(current.Implementation, out session); + houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); List errors; - ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors); - UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors); + ProverInterface.Outcome outcome = TryCatchVerify(session, out errors); + UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors); this.NotifyOutcome(outcome); - current.WorkQueue.Dequeue(); + currentHoudiniState.WorkQueue.Dequeue(); this.NotifyDequeue(); } this.NotifyFlushFinish(); } - private void UpdateAssignment(HoudiniState current, RefutedAnnotation refAnnot) { + private void UpdateAssignment(RefutedAnnotation refAnnot) { if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Removing " + refAnnot.Constant); } - current.Assignment.Remove(refAnnot.Constant); - current.Assignment.Add(refAnnot.Constant, false); + currentHoudiniState.Assignment.Remove(refAnnot.Constant); + currentHoudiniState.Assignment.Add(refAnnot.Constant, false); this.NotifyConstant(refAnnot.Constant.Name); } - private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) { - Contract.Assume(current.Implementation != null); - foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { - if (!current.isBlackListed(implementation.Name)) { - current.WorkQueue.Enqueue(implementation); + private void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) { + Contract.Assume(currentHoudiniState.Implementation != null); + foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, currentHoudiniState.Implementation)) { + if (!currentHoudiniState.isBlackListed(implementation.Name)) { + currentHoudiniState.WorkQueue.Enqueue(implementation); this.NotifyEnqueue(implementation); } } @@ -630,10 +633,9 @@ namespace Microsoft.Boogie.Houdini { // Updates the worklist and current assignment // @return true if the current function is dequeued - private bool UpdateAssignmentWorkList(HoudiniState current, - ProverInterface.Outcome outcome, + private bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, List errors) { - Contract.Assume(current.Implementation != null); + Contract.Assume(currentHoudiniState.Implementation != null); bool dequeue = true; switch (outcome) { @@ -645,21 +647,21 @@ namespace Microsoft.Boogie.Houdini { foreach (Counterexample error in errors) { RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); if (refutedAnnotation != null) { // some candidate annotation removed - AddRelatedToWorkList(current, refutedAnnotation); - UpdateAssignment(current, refutedAnnotation); + AddRelatedToWorkList(refutedAnnotation); + UpdateAssignment(refutedAnnotation); dequeue = false; } } break; default: - current.addToBlackList(current.Implementation.Name); + currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name); break; } return dequeue; } - private class WorkQueue { + public class WorkQueue { private Queue queue; private HashSet set; public WorkQueue() { @@ -688,7 +690,7 @@ namespace Microsoft.Boogie.Houdini { } } - private class HoudiniState { + public class HoudiniState { private WorkQueue _workQueue; private HashSet blackList; private Dictionary _assignment; @@ -725,28 +727,27 @@ namespace Microsoft.Boogie.Houdini { } public HoudiniOutcome PerformHoudiniInference() { - HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants)); this.NotifyStart(program, houdiniConstants.Count); foreach (Implementation impl in vcgenFailures) { - current.addToBlackList(impl.Name); + currentHoudiniState.addToBlackList(impl.Name); } - while (current.WorkQueue.Count > 0) { + while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); - current.Implementation = current.WorkQueue.Peek(); - this.NotifyImplementation(current.Implementation); + currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); + this.NotifyImplementation(currentHoudiniState.Implementation); HoudiniSession session; - this.houdiniSessions.TryGetValue(current.Implementation, out session); - HoudiniVerifyCurrent(session, current); + this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); + HoudiniVerifyCurrent(session); } this.NotifyEnd(true); Dictionary assignment = new Dictionary(); - foreach (var x in current.Assignment) + foreach (var x in currentHoudiniState.Assignment) assignment[x.Key.Name] = x.Value; - current.Outcome.assignment = assignment; - return current.Outcome; + currentHoudiniState.Outcome.assignment = assignment; + return currentHoudiniState.Outcome; } private List FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) { @@ -806,7 +807,6 @@ namespace Microsoft.Boogie.Houdini { public static RefutedAnnotation BuildRefutedAssert(Variable constant) { return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null); } - } private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) { @@ -884,10 +884,10 @@ namespace Microsoft.Boogie.Houdini { return null; } - private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, Dictionary assignment, out List errors) { + private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, out List errors) { ProverInterface.Outcome outcome; try { - outcome = session.Verify(proverInterface, assignment, out errors); + outcome = session.Verify(proverInterface, currentHoudiniState.Assignment, out errors); } catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); @@ -897,25 +897,27 @@ namespace Microsoft.Boogie.Houdini { return outcome; } - private void HoudiniVerifyCurrent(HoudiniSession session, HoudiniState current) { + private void HoudiniVerifyCurrent(HoudiniSession session) { while (true) { - this.NotifyAssignment(current.Assignment); + this.NotifyAssignment(currentHoudiniState.Assignment); //check the VC with the current assignment List errors; - ProverInterface.Outcome outcome = TryCatchVerify(session, current.Assignment, out errors); + ProverInterface.Outcome outcome = TryCatchVerify(session, out errors); this.NotifyOutcome(outcome); - DebugRefutedCandidates(current.Implementation, errors); + DebugRefutedCandidates(currentHoudiniState.Implementation, errors); - if (UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors)) { // abort - current.WorkQueue.Dequeue(); + if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort + currentHoudiniState.WorkQueue.Dequeue(); this.NotifyDequeue(); - FlushWorkList(current); + FlushWorkList(); return; } - else if (UpdateAssignmentWorkList(current, outcome, errors)) { - current.WorkQueue.Dequeue(); + else if (UpdateAssignmentWorkList(outcome, errors)) { + if (CommandLineOptions.Clo.UseUnsatCoreForContractInfer && outcome == ProverInterface.Outcome.Valid) + session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment); + currentHoudiniState.WorkQueue.Dequeue(); this.NotifyDequeue(); return; } -- cgit v1.2.3