changes in the parallel houdini script

2 files changed, 70 insertions, 31 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 9e4798a2..486f75bf 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -698,16 +698,15 @@ namespace Microsoft.Boogie.Houdini {
       this.NotifyFlushFinish();

     }

 

-    private List<RefutedAnnotation> ExchangeRefutedAnnotations(List<RefutedAnnotation> newlyRefuted)

+    private HashSet<RefutedAnnotation> ExchangeRefutedAnnotations(HashSet<RefutedAnnotation> newlyRefuted)

     {

-      List<RefutedAnnotation> result = newlyRefuted;

-//      List<string> knownRefutedInformation = new List<string>();

+      HashSet<RefutedAnnotation> result = newlyRefuted;

       string refutedInformation;

 

       if (CommandLineOptions.Clo.DebugParallelHoudini)

         Console.WriteLine("# refuted annotations before exchange: " + result.Count);

 

-      using (var fileStream = new FileStream(@"houdini.txt", FileMode.OpenOrCreate, FileAccess.ReadWrite, FileShare.ReadWrite))

+      using (var fileStream = new FileStream(@"houdini.csv", FileMode.OpenOrCreate, FileAccess.ReadWrite, FileShare.ReadWrite))

       using (var input = new StreamReader(fileStream))

       using (var output = new StreamWriter(fileStream)) {

         while ((refutedInformation = input.ReadLine()) != null) {

@@ -753,11 +752,8 @@ namespace Microsoft.Boogie.Houdini {
           Console.WriteLine("# refuted annotations after exchange: " + result.Count);

 

         foreach (RefutedAnnotation refAnnot in result) {

-//          string ri = refAnnot.Constant + "," + refAnnot.Kind + "," +

-//            refAnnot.CalleeProc + "," + currentHoudiniState.Implementation;

-//          if (!knownRefutedInformation.Contains(ri))

           output.WriteLine(refAnnot.Constant + "," + refAnnot.Kind + "," +

-                           refAnnot.CalleeProc + "," + currentHoudiniState.Implementation);

+                           refAnnot.CalleeProc + "," + refAnnot.RefutationSite);

         }

       }

 

@@ -802,7 +798,7 @@ namespace Microsoft.Boogie.Houdini {
               Contract.Assume(errors != null);

 

               if (CommandLineOptions.Clo.HoudiniOutputRefutedCandidates) {

-                  List<RefutedAnnotation> refutedAnnotations = new List<RefutedAnnotation>();

+                  HashSet<RefutedAnnotation> refutedAnnotations = new HashSet<RefutedAnnotation>();

                 

                   foreach (Counterexample error in errors) {

                       RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

@@ -1076,6 +1072,36 @@ namespace Microsoft.Boogie.Houdini {
       public static RefutedAnnotation BuildRefutedAssert(Variable constant, Implementation refutationSite) {

         return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null, refutationSite);

       }

+

+      public override int GetHashCode()

+      {

+        unchecked {

+          int hash = 17;

+          hash = hash * 23 + this.Constant.GetHashCode();

+          hash = hash * 23 + this.Kind.GetHashCode();

+          if (this.CalleeProc != null)

+            hash = hash * 23 + this.CalleeProc.GetHashCode();

+          hash = hash * 23 + this.RefutationSite.GetHashCode();

+          return hash;

+        }

+      }

+

+      public override bool Equals(object obj) {

+        bool result = true;

+        var other = obj as RefutedAnnotation;

+

+        if (other == null) {

+          result = false;

+        } else {

+          result = result && String.Equals(other.Constant, this.Constant);

+          result = result && String.Equals(other.Kind, this.Kind);

+          if (other.CalleeProc != null && this.CalleeProc != null)

+            result = result && String.Equals(other.CalleeProc, this.CalleeProc);

+          result = result && String.Equals(other.RefutationSite, this.RefutationSite);

+        }

+

+        return result;

+      }

     }

 

     private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {

diff --git a/Util/PortfolioSolver.py b/Util/PortfolioSolver.py
index d122eafe..d6bfc73a 100755
--- a/Util/PortfolioSolver.py
+++ b/Util/PortfolioSolver.py
@@ -36,18 +36,16 @@ exitHook.hook()
 class CommandLineOptions(object):
   sourceFiles = []
   boogieOptions = [ "/nologo",
+                    "/noinfer", 
                     "/typeEncoding:m", 
+                    "/vc:i",
                     "/useArrayTheory", 
                     "/doNotUseLabels", 
-                    "/noinfer", 
-                    "/contractInfer",
-                    "/outputRefuted",
-                    "/proverOpt:OPTIMIZE_FOR_BV=true"
+                    "/contractInfer"
                   ]
   workers = 1
-  inference = True
-  debugging = False
   verbose = False
+  keepTemps = False
   noSourceLocInfer = False
   time = False
   timeCSVLabel = None
@@ -62,23 +60,28 @@ class VerificationTask(multiprocessing.Process):
     """ This class is used to create a new thread and run a
     verification task on it.
     """
-    def __init__(self, taskID, queue, solver, errorLimit, timeout=0, timeoutErrorCode=None):
+    def __init__(self, taskID, queue, solver, trustFlag, errorLimit, loopUnwind, inlineDepth, timeout=0, timeoutErrorCode=None):
         super(VerificationTask, self).__init__()
         self.taskID = taskID
         self.queue = queue
         self.solver = solver
+        self.trust = trustFlag
         self.timeout = timeout
         self.timeoutErrorCode = timeoutErrorCode
-        self.options = [ "/outputRefuted",
-                         "/errorLimit:" + str(errorLimit)
-                       ]
-        
+        self.options = [ "/errorLimit:" + str(errorLimit) ]
         if (solver == "cvc4"):
           self.options += [ "/proverOpt:SOLVER=cvc4" ]
           self.options += [ "/cvc4exe:" + os.path.dirname(__file__) + os.sep + "../Binaries/cvc4.exe" ]
         elif (solver == "Z3"):
+          self.options += [ "/z3opt:SOLVER=true" ]
           self.options += [ "/z3exe:" + os.path.dirname(__file__) + os.sep + "../Binaries/z3.exe" ]
-          self.options += ["/z3opt:RELEVANCY=0", "/z3opt:SOLVER=true" ]
+          # self.options += [ "/z3opt:RELEVANCY=0" ]
+          self.options += [ "/z3opt:ARRAY_WEAK=true" ]
+          self.options += [ "/z3opt:ARRAY_EXTENSIONAL=false" ]
+        if (loopUnwind > 0):
+          self.options += ["/loopUnroll:" + str(loopUnwind) ]
+        if (inlineDepth > 0):
+          self.options += ["/inlineDepth:" + str(inlineDepth) ]
     
     def run(self):
         print "INFO:[Task-" + str(self.taskID) + "] running Boogie using the " + self.solver + " solver."
@@ -89,7 +92,7 @@ class VerificationTask(multiprocessing.Process):
             ErrorCodes.BOOGIE_ERROR,
             self.timeout,
             self.timeoutErrorCode)
-        self.queue.put(self.taskID)
+        if (self.trust): self.queue.put(self.taskID)
     
 class Timeout(Exception):
     pass
@@ -197,14 +200,15 @@ def showHelpAndExit():
   print "USAGE: PortfolioSolver.py [options] <inputs>"
   print ""
   print "GENERAL OPTIONS:"
-  print "  -h, --help              Display this message"
-  print "  -p, --processes=        Number of solvers to run in parallel"
+  print "  -h, --help              Display this message."
+  print "  -p, --processes=        Number of solvers to run in parallel."
   print "  --memout=X              Give Boogie a hard memory limit of X megabytes."
   print "                          A memout of 0 disables the memout. The default is " + str(CommandLineOptions.boogieMemout) + " megabytes."
-  print "  --time                  Show timing information"
+  print "  --time                  Show timing information."
   print "  --timeout=X             Allow Boogie to run for X seconds before giving up."
   print "                          A timeout of 0 disables the timeout. The default is " + str(CommandLineOptions.boogieTimeout) + " seconds."
-  print "  --verbose               Show commands to run and use verbose output"
+  print "  --verbose               Show commands to run and use verbose output."
+  print "  --keep-temps            Keep intermediate houdini output file."
   sys.exit(0)
 
 def PortfolioSolverError(msg, code):
@@ -263,6 +267,8 @@ def processOptions(opts, args):
           PortfolioSolverError("Invalid memout \"" + a + "\"", ErrorCodes.COMMAND_LINE_ERROR)
     if o == "--verbose":
       CommandLineOptions.verbose = True
+    if o == "--keep-temps":
+      CommandLineOptions.keepTemps = True
 
 def main(argv=None):
   if argv is None:
@@ -272,7 +278,7 @@ def main(argv=None):
   try:
     opts, args = getopt.gnu_getopt(argv[1:],'p:h', 
              ['help', 'processors=',
-              'verbose',
+              'verbose', 'keep-temps',
               'memout=',
               'no-source-loc-infer',
               'boogie-opt=',
@@ -290,7 +296,9 @@ def main(argv=None):
     CommandLineOptions.boogieOptions += [ "/noSourceLocInfer" ]
   if CommandLineOptions.boogieMemout > 0:
     CommandLineOptions.boogieOptions.append("/z3opt:-memory:" + str(CommandLineOptions.boogieMemout))
-
+  if CommandLineOptions.workers > 1:
+    CommandLineOptions.boogieOptions += [ "/outputRefuted" ]
+  
   timeoutArguments={}
   if CommandLineOptions.boogieTimeout > 0:
     timeoutArguments['timeout']= CommandLineOptions.boogieTimeout
@@ -304,9 +312,13 @@ def main(argv=None):
   
   for taskID in range(CommandLineOptions.workers):
     if (taskID == 0):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 8, **timeoutArguments)
+      task = VerificationTask(taskID + 1, taskQueue, "Z3", True, 20, 0, 2, **timeoutArguments)
     elif (taskID == 1):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, **timeoutArguments)
+      task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 20, 0, 0, **timeoutArguments)
+    elif (taskID == 2):
+      task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 4, 2, 0, **timeoutArguments)
+    elif (taskID == 3):
+      task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 4, 0, 1, **timeoutArguments)
     task.start()
     toolTasks.append(task)
   
@@ -319,7 +331,8 @@ def main(argv=None):
     print "INFO:[Task-" + str(taskResult) + "] finished (%.2f secs)." % timing
   else:
     print "INFO:[Task-" + str(taskResult) + "] finished."
-  os.remove("houdini.txt")
+  if (CommandLineOptions.workers > 1) and (not CommandLineOptions.keepTemps):
+    os.remove("houdini.csv")
 
   return 0