From 819c1f07fe1e0244e14306ad1dee213a9a034f1e Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Thu, 15 Aug 2013 12:48:24 +0100 Subject: new option to disable checking for loop maintained invariants - this leads to an underapproximation that helps to speedup houdini refutation of candidates --- Source/Core/CommandLineOptions.cs | 10 ++++++ Source/ExecutionEngine/ExecutionEngine.cs | 1 - Source/Provers/SMTLib/SMTLibProverOptions.cs | 6 ++-- Source/VCGeneration/VC.cs | 7 +++- Util/PortfolioSolver.py | 49 +++++++++++++++++----------- 5 files changed, 50 insertions(+), 23 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 46f74004..22d48af0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -398,6 +398,7 @@ namespace Microsoft.Boogie { public bool ContractInfer = false; public bool ExplainHoudini = false; public bool HoudiniOutputRefutedCandidates = false; + public bool DisableLoopInvMaintainedAssert = false; public bool DebugParallelHoudini = false; public bool HoudiniUseCrossDependencies = false; public string StagedHoudini = null; @@ -1173,6 +1174,12 @@ namespace Microsoft.Boogie { } return true; + case "disableLoopInvMaintainedAssert": + if (ps.ConfirmArgumentCount(0)) { + DisableLoopInvMaintainedAssert = true; + } + return true; + case "debugParallelHoudini": if (ps.ConfirmArgumentCount(0)) { DebugParallelHoudini = true; @@ -1668,6 +1675,9 @@ namespace Microsoft.Boogie { invariants /outputRefuted Outputs the refuted candidates + /disableLoopInvMaintainedAssert + Disables the loop invariant check to maintain the invariant after iteration. + This is an under-approximation feature. ---- Debugging and general tracing options --------------------------------- diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index f81150b1..34a32dfd 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -686,7 +686,6 @@ namespace Microsoft.Boogie } } - /// /// Given a resolved and type checked Boogie program, infers invariants for the program /// and then attempts to verify it. Returns: diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 3f4ef5ac..0cfa65d8 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -87,15 +87,17 @@ namespace Microsoft.Boogie.SMTLib string SolverStr = null; if (ParseString(opt, "SOLVER", ref SolverStr)) { switch (SolverStr) { + case "Z3": case "z3": Solver = SolverKind.Z3; break; + case "CVC4": case "cvc4": Solver = SolverKind.CVC4; - if (Logic.Equals("")) Logic = "ALL_SUPPORTED"; + if (Logic.Equals("")) Logic = "ALL_SUPPORTED"; break; default: - ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'"); + ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4'"); return false; } return true; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index fd7a4f72..1aed2cba 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1944,7 +1944,12 @@ namespace VC { b.Attributes = c.Attributes; b.ErrorData = c.ErrorData; prefixOfPredicateCmdsInit.Add(b); - b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr); + + if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert) + b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True); + else + b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr); + b.Attributes = c.Attributes; b.ErrorData = c.ErrorData; prefixOfPredicateCmdsMaintained.Add(b); diff --git a/Util/PortfolioSolver.py b/Util/PortfolioSolver.py index d6bfc73a..61f0887d 100755 --- a/Util/PortfolioSolver.py +++ b/Util/PortfolioSolver.py @@ -44,13 +44,14 @@ class CommandLineOptions(object): "/contractInfer" ] workers = 1 + inlineDepth = 2 verbose = False keepTemps = False noSourceLocInfer = False time = False timeCSVLabel = None boogieMemout=0 - boogieTimeout=300 + boogieTimeout=0 def SplitFilenameExt(f): filename, ext = os.path.splitext(f) @@ -60,12 +61,14 @@ 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, trustFlag, errorLimit, loopUnwind, inlineDepth, timeout=0, timeoutErrorCode=None): + + isTrusted = True + + def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, loopUnwind, 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 = [ "/errorLimit:" + str(errorLimit) ] @@ -73,16 +76,17 @@ class VerificationTask(multiprocessing.Process): 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: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 (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." RunTool("boogie", @@ -92,7 +96,7 @@ class VerificationTask(multiprocessing.Process): ErrorCodes.BOOGIE_ERROR, self.timeout, self.timeoutErrorCode) - if (self.trust): self.queue.put(self.taskID) + if (self.isTrusted): self.queue.put(self.taskID) class Timeout(Exception): pass @@ -202,6 +206,7 @@ def showHelpAndExit(): 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." @@ -242,8 +247,11 @@ def processOptions(opts, args): CommandLineOptions.workers = int(a) except ValueError: PortfolioSolverError("non integer value '" + a + "' provided as argument to --processes", ErrorCodes.COMMAND_LINE_ERROR) - if o == "--boogie-opt": - CommandLineOptions.boogieOptions += str(a).split(" ") + 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": @@ -269,6 +277,8 @@ def processOptions(opts, args): 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: @@ -278,12 +288,12 @@ def main(argv=None): try: opts, args = getopt.gnu_getopt(argv[1:],'p:h', ['help', 'processors=', - 'verbose', 'keep-temps', - 'memout=', + 'inline-depth=', 'no-source-loc-infer', - 'boogie-opt=', 'time', 'time-as-csv=', - 'timeout=' + '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) @@ -303,7 +313,8 @@ def main(argv=None): 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 = [] @@ -312,13 +323,13 @@ def main(argv=None): for taskID in range(CommandLineOptions.workers): if (taskID == 0): - task = VerificationTask(taskID + 1, taskQueue, "Z3", True, 20, 0, 2, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 1, True, 0, **timeoutArguments) elif (taskID == 1): - task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 20, 0, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 2, True, 0, **timeoutArguments) elif (taskID == 2): - task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 4, 2, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, 0, **timeoutArguments) elif (taskID == 3): - task = VerificationTask(taskID + 1, taskQueue, "Z3", False, 4, 0, 1, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, 0, **timeoutArguments) task.start() toolTasks.append(task) -- cgit v1.2.3