summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/CommandLineOptions.cs10
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs1
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs6
-rw-r--r--Source/VCGeneration/VC.cs7
-rwxr-xr-xUtil/PortfolioSolver.py49
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
}
}
-
/// <summary>
/// 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 09:09:02 +0000