full port of houdini project

1 files changed, 46 insertions, 62 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 661393ff..294f5d1b 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -9,35 +9,33 @@ using System.Collections.Generic;
 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Boogie.Simplify;

-using VC;

 using Microsoft.Boogie.Z3;

 using System.Collections;

 using System.IO;

 using System.Threading;

+using VC;

 

 namespace Microsoft.Boogie.Houdini {

-  public class HoudiniChecker {

+  class HoudiniChecker {

     private Stack<VCExpr> axioms = new Stack<VCExpr>();

     private Checker checker;

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

-        

-    internal HoudiniChecker(Checker checker) 

+

+    internal HoudiniChecker(Checker checker, string _descriptiveName, VCExpr _vc, ProverInterface.ErrorHandler _handler) 

     {

       Contract.Requires(checker.TheoremProver != null);

       Contract.Requires(checker.TheoremProver is Z3ProcessTheoremProver);

       this.checker = checker;

-    }

-    

-    public void PrepareCheck(string _descriptiveName, VCExpr _vc, ProverInterface.ErrorHandler _handler) 

-    {

       this.descriptiveName = _descriptiveName;

       this.conjecture = _vc;

       this.handler = _handler;

     }

-

-    public void PushAxiom(VCExpr vc) {

+    

+    public void PushAxiom(Axiom axiom) {

+      DeclFreeProverContext proverContext = (DeclFreeProverContext) checker.TheoremProver.Context;

+      VCExpr vc = proverContext.BoogieExprTranslator.Translate(axiom.Expr);

       axioms.Push(vc);

     }

 

@@ -53,7 +51,7 @@ namespace Microsoft.Boogie.Houdini {
         if (vc_axioms == null)

           vc_axioms = axiom;

         else

-          vc_axioms = checker.VCExprGen.And(vc_axioms,axiom);

+          vc_axioms = checker.VCExprGen.And(vc_axioms, axiom);

       }

       return vc_axioms;

     }

@@ -78,7 +76,6 @@ namespace Microsoft.Boogie.Houdini {
     }

    

     private ProverInterface.Outcome outcome;

-    private UnexpectedProverOutputException outputExn;

 

     public ProverInterface.Outcome ReadOutcome()

     {

@@ -93,73 +90,61 @@ namespace Microsoft.Boogie.Houdini {
 

   public class HoudiniVCGen : VCGen {

     private HoudiniChecker hdnChecker;

-    private VCExpressionGenerator gen;

-    CounterexampleCollector collector = new CounterexampleCollector();

-    

-    public HoudiniVCGen(Program program, string logFilePath, bool appendLogFile) 

-      : base(program, logFilePath, appendLogFile)

-    {

-    }

-    

-    public void VerifyImplementation(Implementation impl, Program program) {

+    CounterexampleCollector collector;

+

+    public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile)

+      : base(program, logFilePath, appendLogFile) {

+      collector = new CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

         throw new Exception("HoudiniVCGen does not support Soundness smoke test.");

       }

-      

+

       ConvertCFG2DAG(impl, program);

       ModelViewInfo mvInfo;

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

-	  Hashtable/*<int, Absy!>*/ label2absy;

-      Checker checker = new Checker(this, program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime); 

+      Hashtable/*<int, Absy!>*/ label2absy;

+      Checker checker = new Checker(this, program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);

       VCExpr vc = GenerateVC(impl, null, out label2absy, checker);

-              

+

       ErrorReporter reporter;

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-        reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, null, program);

-      } else {

-        reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, null, program);

+        reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);

+      }

+      else {

+        reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);

       }

-      this.gen = checker.VCExprGen;

       if (checker.TheoremProver is Z3ProcessTheoremProver)

-        this.hdnChecker = new HoudiniChecker(checker);

+        this.hdnChecker = new HoudiniChecker(checker, impl.Name, vc, reporter);

       else

         throw new Exception("HdnChecker only works with z3");

-      this.hdnChecker.PrepareCheck(impl.Name, vc, reporter);

-      this.hdnChecker.Check();

     }

-    

-    public void PushAxiom(Axiom axiom) 

-    {

-      Contract.Assume(hdnChecker != null);

-      Contract.Assume(gen != null);

-      //VCExpr vc = axiom.Expr.VCView(gen);

-      //this.hdnChecker.PushAxiom(vc);

+

+    public void PushAxiom(Axiom axiom) {

+      this.hdnChecker.PushAxiom(axiom);

     }

 

     public void Pop() {

-      Contract.Assume(hdnChecker!=null);

       hdnChecker.Pop();

     }

-    

-    public Outcome Verify(out List<Counterexample> errors)       

-  {

-      Contract.Assume (hdnChecker != null);

+

+    public Outcome Verify(out List<Counterexample> errors) {

       collector.examples.Clear();

       hdnChecker.Check();

       ProverInterface.Outcome proverOutcome;

       proverOutcome = hdnChecker.ReadOutcome();

       Outcome verifyOutcome = ReadOutcome(proverOutcome);

       if (verifyOutcome == Outcome.Errors) {

-        Contract.Assume (collector.examples != null);

+        Contract.Assume(collector.examples != null);

         if (collector.examples.Count == 0) {

-            string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));

-            if (memStr != null)

-                memStr = "?";

-            throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");

+          string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));

+          if (memStr != null)

+            memStr = "?";

+          throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");

         }

         errors = collector.examples;

-      } else {

+      }

+      else {

         errors = null;

       }

       return verifyOutcome;

@@ -167,20 +152,19 @@ namespace Microsoft.Boogie.Houdini {
 

     private Outcome ReadOutcome(ProverInterface.Outcome proverOutcome) {

       switch (proverOutcome) {

-          case ProverInterface.Outcome.Valid:

-            return Outcome.Correct;

-          case ProverInterface.Outcome.Invalid:

-            return Outcome.Errors;

-          case ProverInterface.Outcome.TimeOut:

-            return Outcome.TimedOut;

-          case ProverInterface.Outcome.Undetermined:

-            return Outcome.Inconclusive;

-          default:

-            throw new Exception("Unknown Prover Interface outcome while reading outcome.");

-        }

+        case ProverInterface.Outcome.Valid:

+          return Outcome.Correct;

+        case ProverInterface.Outcome.Invalid:

+          return Outcome.Errors;

+        case ProverInterface.Outcome.TimeOut:

+          return Outcome.TimedOut;

+        case ProverInterface.Outcome.Undetermined:

+          return Outcome.Inconclusive;

+        default:

+          throw new Exception("Unknown Prover Interface outcome while reading outcome.");

+      }

     }

 

   }

   

-  

 }
\ No newline at end of file