unsat core for houdini

1 files changed, 87 insertions, 17 deletions

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++;

     }

 

   }