unsat core for houdini

4 files changed, 144 insertions, 66 deletions

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<Variable> 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<Variable>();

+    }

+    private Houdini houdini;

+    private HashSet<Variable> 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<Variable> unsatCoreSet;

+    HashSet<Variable> 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/*<int, Absy!>*/ label2absy;

+

+      houdiniConstants = ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl);

 

       var exprGen = proverInterface.Context.ExprGen;

       VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

-      

+

+      Hashtable/*<int, Absy!>*/ 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<Variable, bool> currentAssignment) {

@@ -68,6 +118,7 @@ namespace Microsoft.Boogie.Houdini {
       VCExpressionGenerator exprGen = proverInterface.VCExprGen;

 

       VCExpr expr = VCExpressionGenerator.True;

+

       foreach (KeyValuePair<Variable, bool> 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<Variable, bool> assignment, out List<Counterexample> 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<Variable, bool> 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<int> 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<Variable>();

       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<Implementation> callGraph;

     private HashSet<Implementation> 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<Implementation, HoudiniSession>(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<Counterexample> 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<Counterexample> 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<Implementation> queue;

       private HashSet<Implementation> set;

       public WorkQueue() {

@@ -688,7 +690,7 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private class HoudiniState {

+    public class HoudiniState {

       private WorkQueue _workQueue;

       private HashSet<string> blackList;

       private Dictionary<Variable, bool> _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<string, bool> assignment = new Dictionary<string, bool>();

-      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<Implementation> 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<Variable, bool> assignment, out List<Counterexample> errors) {

+    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, out List<Counterexample> 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<Counterexample> 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;

         }