summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Houdini/Houdini.cs2
-rwxr-xr-xUtil/PortfolioSolver.py380
2 files changed, 0 insertions, 382 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4b533e5b..c3575800 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -712,8 +712,6 @@ namespace Microsoft.Boogie.Houdini {
}
protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) {
- if (refutedAnnotation == null) Console.WriteLine("TEEEEEST!!!");
-
Contract.Assume(currentHoudiniState.Implementation != null);
foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, refutedAnnotation.RefutationSite)) {
if (!currentHoudiniState.isBlackListed(implementation.Name)) {
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())
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 06:00:17 +0000