small cleanup

1 files changed, 0 insertions, 380 deletions

diff --git a/Util/PortfolioSolver.py b/Util/PortfolioSolver.py
deleted file mode 100755
index 0572987d..00000000
--- a/Util/PortfolioSolver.py
+++ /dev/null
@@ -1,380 +0,0 @@
-#!/usr/bin/env python2.7
-
-import atexit
-import getopt
-import os
-import signal
-import subprocess
-import sys
-import timeit
-import threading
-import multiprocessing 
-
-""" WindowsError is not defined on UNIX systems, this works around that """
-try:
-   WindowsError
-except NameError:
-   WindowsError = None
-
-""" Horrible hack: Patch sys.exit() so we can get the exitcode in atexit callbacks """
-class ExitHook(object):
-  def __init__(self):
-    self.code = None
-
-  def hook(self):
-    self.realExit = sys.exit
-    sys.exit = self.exit
-
-  def exit(self, code=0):
-    self.code = code
-    self.realExit(code)
-
-exitHook = ExitHook()
-exitHook.hook()
-
-""" Options for the tool """
-class CommandLineOptions(object):
-  sourceFiles = []
-  boogieOptions = [ "/nologo",
-                    "/noinfer", 
-                    "/typeEncoding:m", 
-                    "/vc:i",
-                    "/useArrayTheory", 
-                    "/doNotUseLabels", 
-                    "/contractInfer"
-                  ]
-  workers = 1
-  inlineDepth = 2
-  verbose = False
-  keepTemps = False
-  noSourceLocInfer = False
-  time = False
-  timeCSVLabel = None
-  boogieMemout=0
-  boogieTimeout=0
-
-def SplitFilenameExt(f):
-  filename, ext = os.path.splitext(f)
-  return filename, ext
-
-class VerificationTask(multiprocessing.Process):
-    """ This class is used to create a new thread and run a
-    verification task on it.
-    """
-    
-    isTrusted = True
-    
-    def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, reverseTopSort, loopUnwind, timeout=0, timeoutErrorCode=None):
-        super(VerificationTask, self).__init__()
-        self.taskID = taskID
-        self.queue = queue
-        self.solver = solver
-        self.timeout = timeout
-        self.timeoutErrorCode = timeoutErrorCode
-        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 += [ "/z3exe:" + os.path.dirname(__file__) + os.sep + "../Binaries/z3.exe" ]
-          self.options += [ "/z3opt:SOLVER=true" ]
-          # self.options += [ "/z3opt:RELEVANCY=0" ]
-          self.options += [ "/z3opt:ARRAY_WEAK=true" ]
-          self.options += [ "/z3opt:ARRAY_EXTENSIONAL=false" ]
-        if not checkForLMI:
-          self.options += [ "/disableLoopInvMaintainedAssert" ]
-          self.isTrusted = False
-        if reverseTopSort:
-          self.options += [ "/reverseTopologicalSorting" ]
-        if (loopUnwind > 0):
-          self.options += ["/loopUnroll:" + str(loopUnwind) ]
-        
-    def run(self):
-        print "INFO:[Task-" + str(self.taskID) + "] running Boogie using the " + self.solver + " solver."
-        RunTool("boogie",
-            (["mono"] if os.name == "posix" else []) +
-            [os.path.dirname(__file__) + os.sep + "../Binaries/Boogie.exe"] +
-            CommandLineOptions.boogieOptions + self.options,
-            ErrorCodes.BOOGIE_ERROR,
-            self.timeout,
-            self.timeoutErrorCode)
-        if (self.isTrusted): self.queue.put(self.taskID)
-    
-class Timeout(Exception):
-    pass
-
-class ToolWatcher(object):
-  """ This class is used by run() to implement a timeout.
-  It uses threading.Timer to implement the timeout and provides
-  a method for checking if the timeout occurred. It also provides a 
-  method for cancelling the timeout.
-
-  The class is reentrant
-  """
-
-  def __handleTimeOut(self):
-    if self.popenObject.poll() == None :
-      # Program is still running, let's kill it
-      self.__killed=True
-      self.popenObject.terminate()
-
-  """ Create a ToolWatcher instance with an existing "subprocess.Popen" instance
-      and timeout.
-  """
-  def __init__(self,popenObject,timeout):
-    """ Create ToolWatcher. This will start the timeout.
-    """
-    self.timeout=timeout
-    self.popenObject=popenObject
-    self.__killed=False
-
-    self.timer=threading.Timer(self.timeout, self.__handleTimeOut)
-    self.timer.start()
-
-  """ Returns True if the timeout occurred """
-  def timeOutOccured(self):
-    return self.__killed
-
-  """ Cancel the timeout. You must call this if your program wishes
-      to exit else exit() will block waiting for this class's Thread
-      (threading.Timer) to finish.
-  """
-  def cancelTimeout(self):
-    self.timer.cancel()
-
-def run(command,timeout=0):
-  """ Run a command with an optional timeout. A timeout of zero 
-      implies no timeout.
-  """
-  popenargs={}
-  if CommandLineOptions.verbose:
-    print " ".join(command)
-  else:
-    popenargs['bufsize']=0
-    popenargs['stdout']=subprocess.PIPE
-    popenargs['stderr']=subprocess.PIPE
-
-  killer=None
-  def cleanupKiller():
-    if killer!=None:
-      killer.cancelTimeout()
-
-  proc = subprocess.Popen(command,**popenargs)
-  if timeout > 0:
-    killer=ToolWatcher(proc,timeout)
-  try:
-    stdout, stderr = proc.communicate()
-    if killer != None and killer.timeOutOccured():
-      raise Timeout
-  except KeyboardInterrupt:
-    cleanupKiller()
-    proc.wait()
-    sys.exit(ErrorCodes.CTRL_C)
-  finally:
-    #Need to kill the timer if it exists else exit() will block until the timer finishes
-    cleanupKiller()
-
-  return stdout, stderr, proc.returncode
-
-class ErrorCodes(object):
-  SUCCESS = 0
-  COMMAND_LINE_ERROR = 1
-  BOOGIE_ERROR = 2
-  BOOGIE_TIMEOUT = 3
-  CTRL_C = 4
-
-def RunTool(ToolName, Command, ErrorCode,timeout=0,timeoutErrorCode=None):
-  """ Run a tool. 
-      If the timeout is set to 0 then there will no timeout.
-      If the timeout is > 0 then timeoutErrorCode MUST be set!
-  """
-  try:
-    stdout, stderr, returnCode = run(Command, timeout)
-  except Timeout:
-    PortfolioSolverError(ToolName + " timed out.  Use --timeout=N with N > " + str(timeout) + " to increase timeout, or --timeout=0 to disable timeout.", timeoutErrorCode)
-  except (OSError,WindowsError) as e:
-    PortfolioSolverError("While invoking " + ToolName + ": " + str(e),ErrorCode)
-
-  if returnCode != 0:
-    if stdout: print >> sys.stderr, stdout
-    if stderr: print >> sys.stderr, stderr
-    sys.exit(ErrorCode)
-
-def showHelpAndExit():
-  print "OVERVIEW: Portfolio Solver"
-  print ""
-  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 "  --inline-depth=X        Depth of inlining procedure calls."
-  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 "  --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 "  --keep-temps            Keep intermediate houdini output file."
-  sys.exit(0)
-
-def PortfolioSolverError(msg, code):
-  print >> sys.stderr, "PortfolioSolver: error: " + msg
-  sys.exit(code)
-
-def Verbose(msg):
-  if(CommandLineOptions.verbose):
-    print msg
-
-def getSourceFiles(args):
-  if len(args) == 0:
-    PortfolioSolverError("no .bpl files supplied", ErrorCodes.COMMAND_LINE_ERROR)
-  for a in args:
-    filename, ext = SplitFilenameExt(a)
-    if not ext == ".bpl":
-      PortfolioSolverError("'" + a + "' has unknown file extension, supported file extensions are .bpl (Boogie PL)", ErrorCodes.COMMAND_LINE_ERROR)
-    CommandLineOptions.sourceFiles.append(a)
-
-def showHelpIfRequested(opts):
-  for o, a in opts:
-    if o == "--help" or o == "-h":
-      showHelpAndExit()
-
-def processOptions(opts, args):
-  for o, a in opts:
-    if o == "--processes" or o == "-p":
-      try:
-        if int(a) < 0:
-          PortfolioSolverError("negative value " + a + " provided as argument to --processes", ErrorCodes.COMMAND_LINE_ERROR) 
-        CommandLineOptions.workers = int(a)
-      except ValueError:
-        PortfolioSolverError("non integer value '" + a + "' provided as argument to --processes", ErrorCodes.COMMAND_LINE_ERROR)
-    if o == "--inline-depth":
-      try:
-        CommandLineOptions.inlineDepth = int(a)
-      except ValueError:
-        PortfolioSolverError("non integer value '" + a + "' provided as argument to --inline-depth", ErrorCodes.COMMAND_LINE_ERROR)
-    if o == "--no-source-loc-infer":
-      CommandLineOptions.noSourceLocInfer = True
-    if o == "--time":
-      CommandLineOptions.time = True
-    if o == "--time-as-csv":
-      CommandLineOptions.time = True
-      CommandLineOptions.timeCSVLabel = a
-    if o == "--timeout":
-      try:
-        CommandLineOptions.boogieTimeout = int(a)
-        if CommandLineOptions.boogieTimeout < 0:
-          raise ValueError
-      except ValueError as e:
-          PortfolioSolverError("Invalid timeout \"" + a + "\"", ErrorCodes.COMMAND_LINE_ERROR)
-    if o == "--memout":
-      try:
-        CommandLineOptions.boogieMemout = int(a)
-        if CommandLineOptions.boogieMemout < 0:
-          raise ValueError
-      except ValueError as e:
-          PortfolioSolverError("Invalid memout \"" + a + "\"", ErrorCodes.COMMAND_LINE_ERROR)
-    if o == "--verbose":
-      CommandLineOptions.verbose = True
-    if o == "--keep-temps":
-      CommandLineOptions.keepTemps = True
-    if o == "--boogie-opt":
-      CommandLineOptions.boogieOptions += str(a).split(" ")
-
-def main(argv=None):
-  if argv is None:
-    argv = sys.argv
-  progname = argv[0]
-
-  try:
-    opts, args = getopt.gnu_getopt(argv[1:],'p:h', 
-             ['help', 'processors=',
-              'inline-depth=',
-              'no-source-loc-infer',
-              'time', 'time-as-csv=',
-              'memout=', 'timeout=',
-              'verbose', 'keep-temps',
-              'boogie-opt='
-             ])
-  except getopt.GetoptError as getoptError:
-    PortfolioSolverError(getoptError.msg + ".  Try --help for list of options", ErrorCodes.COMMAND_LINE_ERROR)
-
-  showHelpIfRequested(opts)
-  getSourceFiles(args)
-  processOptions(opts, args)
-  
-  if CommandLineOptions.noSourceLocInfer:
-    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
-    timeoutArguments['timeoutErrorCode']=ErrorCodes.BOOGIE_TIMEOUT
-  
-  CommandLineOptions.boogieOptions += [ "/inlineDepth:" + str(CommandLineOptions.inlineDepth) ]
-  CommandLineOptions.boogieOptions += [ CommandLineOptions.sourceFiles[0] ]
-  
-  toolTasks = []
-  taskQueue = multiprocessing.Queue()  
-  start = timeit.default_timer()
-  
-  for taskID in range(CommandLineOptions.workers):
-    if (taskID == 0):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments)
-    elif (taskID == 1):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, True, 0, **timeoutArguments)
-    elif (taskID == 2):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, False, 0, **timeoutArguments)
-    elif (taskID == 3):
-      task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments)
-    task.start()
-    toolTasks.append(task)
-  
-  taskResult = taskQueue.get()
-  end = timeit.default_timer()
-  for task in toolTasks:
-    task.terminate()
-  timing = end-start
-  if CommandLineOptions.time:
-    print "INFO:[Task-" + str(taskResult) + "] finished (%.2f secs)." % timing
-  else:
-    print "INFO:[Task-" + str(taskResult) + "] finished."
-  if (CommandLineOptions.workers > 1) and (not CommandLineOptions.keepTemps):
-    os.remove("houdini.csv")
-
-  return 0
-
-def showTiming():
-  label = CommandLineOptions.timeCSVLabel
-  times.append(timing)
-  row = [ '%.3f' % t for t in times ]
-  if len(label) > 0: row.insert(0, label)
-  if exitHook.code is ErrorCodes.SUCCESS:
-    row.append('PASS')
-    print ', '.join(row)
-  else:
-    row.append('FAIL(' + str(exitHook.code) + ')')
-    print >> sys.stderr, ', '.join(row)
-
-def killChildrenPosix():
-  def handler(signal,frame):
-    return
-  signal.signal(signal.SIGINT, handler)
-  os.killpg(0,signal.SIGINT)
-
-def exitHandler():
-  if CommandLineOptions.timeCSVLabel is not None:
-    showTiming()
-  sys.stderr.flush()
-  sys.stdout.flush()
-  if os.name == 'posix':
-    killChildrenPosix()
-
-if __name__ == '__main__':
-  atexit.register(exitHandler)
-  sys.exit(main())