cleaned up houdini options

5 files changed, 49 insertions, 59 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 88d8bdaa..35c0832a 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -429,6 +429,11 @@ namespace Microsoft.Boogie {
       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

       Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

 

+      if (CommandLineOptions.Clo.ContractInfer) {

+        Houdini.Houdini houdini = new Houdini.Houdini(program, true);

+        houdini.PerformHoudiniInference();

+      }

+

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 95078433..52714dc9 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -172,6 +172,10 @@
       <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Houdini\Houdini.csproj">

+      <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

+      <Name>Houdini</Name>

+    </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 56116601..e1136150 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -299,7 +299,6 @@ namespace Microsoft.Boogie {
     public int VcsCores = 1;

     public bool VcsDumpSplits = false;

 

-    public bool houdiniEnabled = false;

     public bool DebugRefuted = false;

 

     public XmlSink XmlRefuted {

@@ -401,7 +400,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true));

       Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true));

       Contract.Invariant(Ai != null);

-      Contract.Invariant(houdiniFlags != null);

     }

 

     [Rep]

@@ -441,13 +439,6 @@ namespace Microsoft.Boogie {
     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

-    public class HoudiniFlags {

-      public bool continueAtError = false;

-      public bool incremental = false;

-    }

-

-    public HoudiniFlags/*!*/ houdiniFlags = new HoudiniFlags();

-

     [Verify(false)]

     private CommandLineOptions() {

       // this is just to suppress verification.

@@ -979,8 +970,6 @@ namespace Microsoft.Boogie {
           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

-            TheProverFactory = ProverFactory.Load("ContractInference");

-            ProverName = "ContractInference".ToUpper();

             break;

 

           case "-subsumption":

@@ -1367,28 +1356,6 @@ namespace Microsoft.Boogie {
             }

             break;

 

-          case "-Houdini":

-          case "/Houdini":

-            this.houdiniEnabled = true;

-            if (ps.hasColonArgument) {

-              if (ps.ConfirmArgumentCount(1)) {

-                foreach (char c in cce.NonNull(args[ps.i])) {

-                  switch (c) {

-                    case 'c':

-                      houdiniFlags.continueAtError = true;

-                      break;

-                    case 'i':

-                      houdiniFlags.incremental = true;

-                      break;

-                    default:

-                      ps.Error("Unknown houdini flag: " + c + "\n");

-                      break;

-                  }

-                }

-              }

-            }

-            break;

-

           case "-z3exe":

           case "/z3exe":

             if (ps.ConfirmArgumentCount(1)) {

@@ -2172,10 +2139,6 @@ namespace Microsoft.Boogie {
                          of every block

   /printInstrumented : print Boogie program after it has been

                    instrumented with invariants

-  /Houdini[:<flags>] : perform procedure Houdini

-                     c = continue when an error found

-                     i = use incremental queries

-  /dbgRefuted    : log refuted Houdini candidates to XmlSink

 

   ---- Debugging and general tracing options ---------------------------------

 

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index c3b302e7..1efc0e91 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -7,6 +7,7 @@ using System;
 using System.Diagnostics.Contracts;

 using System.Collections.Generic;

 using Microsoft.Boogie;

+using Microsoft.Boogie.VCExprAST;

 using Microsoft.Boogie.Simplify;

 using VC;

 using Microsoft.Boogie.Z3;

@@ -256,30 +257,34 @@ namespace Microsoft.Boogie.Houdini {
 

     public Houdini(Program program, bool continueAtError) {

       this.program = program;

-      this.callGraph = BuildCallGraph(program);

+      this.callGraph = BuildCallGraph();

       this.continueAtError = continueAtError;

-      this.houdiniConstants = CollectExistentialConstants(program);

-      this.vcgenSessions = PrepareVCGenSessions(program);

+      this.houdiniConstants = CollectExistentialConstants();

+      this.vcgenSessions = PrepareVCGenSessions();

     }

 

-    private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions(Program program) {

+    private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {

+      HashSet<Implementation> impls = new HashSet<Implementation>();

       Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

         if (impl != null) {

-          // make a different simplify log file for each function

-          String simplifyLog = null;

-          if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {

-            simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;

-          }

-          HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

-          vcgenSessions.Add(impl, vcgen);

+          impls.Add(impl);

+        }

+      }

+      foreach (Implementation impl in impls) {

+        // make a different simplify log file for each function

+        String simplifyLog = null;

+        if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {

+          simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;

         }

+        HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgenSessions.Add(impl, vcgen);

       }

       return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);

     }

 

-    private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants(Program program) {

+    private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {

       Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Constant constant = decl as Constant;

@@ -294,7 +299,7 @@ namespace Microsoft.Boogie.Houdini {
       return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);

     }

 

-    private Graph<Implementation> BuildCallGraph(Program program) {

+    private Graph<Implementation> BuildCallGraph() {

       Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

@@ -345,17 +350,21 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

-    private Axiom BuildAxiom(Dictionary<string, bool> currentAssignment) {

-      Expr axiom = new LiteralExpr(Token.NoToken, true);

+    private Axiom BuildAxiom(Dictionary<string, bool> currentAssignment, Boogie2VCExprTranslator exprTranslator) {

+      Expr expr = new LiteralExpr(Token.NoToken, true);

+      expr.Type = Type.Bool;

       foreach (KeyValuePair<string, bool> kv in currentAssignment) {

         IdentifierExpr constantExpr;

         houdiniConstants.TryGetValue(kv.Key, out constantExpr);

         Contract.Assume(constantExpr != null);

         Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value);

+        valueExpr.Type = Type.Bool;

         Expr constantAssignment = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.Eq, constantExpr, valueExpr);

-        axiom = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.And, axiom, constantAssignment);

+        constantAssignment.Type = Type.Bool;

+        expr = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.And, expr, constantAssignment);

+        expr.Type = Type.Bool;

       }

-      return new Axiom(Token.NoToken, axiom);

+      return new Axiom(Token.NoToken, expr);

     }

 

     private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {

@@ -659,14 +668,14 @@ namespace Microsoft.Boogie.Houdini {
       PrintBadList("Errors", errors);

     }

 

-    public HoudiniOutcome VerifyProgram(Program program) {

-      HoudiniOutcome outcome = VerifyProgramSameFuncFirst(program);

+    public HoudiniOutcome VerifyProgram() {

+      HoudiniOutcome outcome = VerifyProgramSameFuncFirst();

       PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);

       return outcome;

     }

 

     // Old main loop

-    public HoudiniOutcome VerifyProgramUnorderedWork(Program program) {

+    public HoudiniOutcome VerifyProgramUnorderedWork() {

       HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

       this.NotifyStart(program, houdiniConstants.Keys.Count);

 

@@ -699,7 +708,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     // New main loop

-    public HoudiniOutcome VerifyProgramSameFuncFirst(Program program) {

+    public HoudiniOutcome VerifyProgramSameFuncFirst() {

       HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

       this.NotifyStart(program, houdiniConstants.Keys.Count);

 

@@ -738,7 +747,7 @@ namespace Microsoft.Boogie.Houdini {
     //Aborts when there is a violation of non-candidate assertion

     //This can be used in eager mode (continueAfterError) by simply making

     //all non-candidate annotations as unchecked (free requires/ensures, assumes)

-    public HoudiniOutcome PerformHoudiniInference(Program program) {

+    public HoudiniOutcome PerformHoudiniInference() {

       HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

       this.NotifyStart(program, houdiniConstants.Keys.Count);

 

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 5e910e03..9c006396 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -30,6 +30,12 @@
     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

   </PropertyGroup>

+  <PropertyGroup>

+    <SignAssembly>true</SignAssembly>

+  </PropertyGroup>

+  <PropertyGroup>

+    <AssemblyOriginatorKeyFile>InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

@@ -88,6 +94,9 @@
   <ItemGroup>

     <Folder Include="Properties\" />

   </ItemGroup>

+  <ItemGroup>

+    <None Include="InterimKey.snk" />

+  </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

        Other similar extension points exist, see Microsoft.Common.targets.