diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 12 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 7 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 23 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 9 | ||||
| -rwxr-xr-x | Util/PortfolioSolver.py | 12 |
6 files changed, 52 insertions, 15 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 22d48af0..2240c201 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -399,6 +399,7 @@ namespace Microsoft.Boogie { public bool ExplainHoudini = false;
public bool HoudiniOutputRefutedCandidates = false;
public bool DisableLoopInvMaintainedAssert = false;
+ public bool ReverseTopologicalSorting = false;
public bool DebugParallelHoudini = false;
public bool HoudiniUseCrossDependencies = false;
public string StagedHoudini = null;
@@ -1180,6 +1181,12 @@ namespace Microsoft.Boogie { }
return true;
+ case "reverseTopologicalSorting":
+ if (ps.ConfirmArgumentCount(0)) {
+ ReverseTopologicalSorting = true;
+ }
+ return true;
+
case "debugParallelHoudini":
if (ps.ConfirmArgumentCount(0)) {
DebugParallelHoudini = true;
@@ -1677,7 +1684,10 @@ namespace Microsoft.Boogie { Outputs the refuted candidates
/disableLoopInvMaintainedAssert
Disables the loop invariant check to maintain the invariant after iteration.
- This is an under-approximation feature.
+ This is an under-approximation feature
+ /reverseTopologicalSorting
+ Reverses the order that roots are found in the Topological Sorting algorithm.
+ Can be used to potentially change the order that Houdini refutes candidates
---- Debugging and general tracing options ---------------------------------
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 9d20c15e..86a3e599 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -372,7 +372,12 @@ namespace Microsoft.Boogie { }
}
- IEnumerable<Block> sortedNodes = dag.TopologicalSort();
+ IEnumerable<Block> sortedNodes;
+ if (CommandLineOptions.Clo.ReverseTopologicalSorting) {
+ sortedNodes = dag.TopologicalSort(true);
+ } else {
+ sortedNodes = dag.TopologicalSort();
+ }
foreach (Block/*!*/ block in sortedNodes) {
Contract.Assert(block != null);
HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index b6fe8cfc..4a78c27f 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -522,14 +522,14 @@ namespace Microsoft.Boogie.GraphUtil { return dominees == null ? new List<Node>() : dominees;
}
- public IEnumerable<Node/*?*/> TopologicalSort() {
+ public IEnumerable<Node/*?*/> TopologicalSort(bool reversed = false) {
bool acyclic;
List<Node> sortedList;
- this.TarjanTopSort(out acyclic, out sortedList);
+ this.TarjanTopSort(out acyclic, out sortedList, reversed);
return acyclic ? sortedList : new List<Node>();
}
// From Tarjan 1972
- public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes) {
+ public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes, bool reversed = false) {
int n = this.Nodes.Count;
if (n == 0) {
acyclic = true;
@@ -558,10 +558,19 @@ namespace Microsoft.Boogie.GraphUtil { while (sortedIndex < n) {
// find a root (i.e., its index)
int rootIndex = -1;
- for (int i = 0; i < n; i++) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
+ if (reversed) {
+ for (int i = n-1; i >= 0; i--) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
+ }
+ } else {
+ for (int i = 0; i < n; i++) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
}
}
if (rootIndex == -1) {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 486f75bf..23967f02 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -822,7 +822,11 @@ namespace Microsoft.Boogie.Houdini { }
}
+ int start = Environment.TickCount;
refutedAnnotations = ExchangeRefutedAnnotations(refutedAnnotations);
+ int duration = Environment.TickCount - start;
+ if (CommandLineOptions.Clo.DebugParallelHoudini)
+ Console.WriteLine("*** Exchange of Refuted Candidates: " + duration + " ms ***");
foreach (RefutedAnnotation refAnnot in refutedAnnotations) {
AddRelatedToWorkList(refAnnot);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 36b8fbe5..e3991f93 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1342,7 +1342,14 @@ namespace VC { }
}
}
- IEnumerable sortedNodes = dag.TopologicalSort();
+
+ IEnumerable sortedNodes;
+ if (CommandLineOptions.Clo.ReverseTopologicalSorting) {
+ sortedNodes = dag.TopologicalSort(true);
+ } else {
+ sortedNodes = dag.TopologicalSort();
+ }
+
Contract.Assert(sortedNodes != null);
#endregion
diff --git a/Util/PortfolioSolver.py b/Util/PortfolioSolver.py index 61f0887d..de004981 100755 --- a/Util/PortfolioSolver.py +++ b/Util/PortfolioSolver.py @@ -64,7 +64,7 @@ class VerificationTask(multiprocessing.Process): isTrusted = True - def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, loopUnwind, timeout=0, timeoutErrorCode=None): + def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, reverseTopSort, loopUnwind, timeout=0, timeoutErrorCode=None): super(VerificationTask, self).__init__() self.taskID = taskID self.queue = queue @@ -84,6 +84,8 @@ class VerificationTask(multiprocessing.Process): if not checkForLMI: self.options += [ "/disableLoopInvMaintainedAssert" ] self.isTrusted = False + if reverseTopSort: + self.options += [ "/reverseTopologicalSorting" ] if (loopUnwind > 0): self.options += ["/loopUnroll:" + str(loopUnwind) ] @@ -323,13 +325,13 @@ def main(argv=None): for taskID in range(CommandLineOptions.workers): if (taskID == 0): - task = VerificationTask(taskID + 1, taskQueue, "Z3", 1, True, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments) elif (taskID == 1): - task = VerificationTask(taskID + 1, taskQueue, "Z3", 2, True, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, False, False, 0, **timeoutArguments) elif (taskID == 2): - task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, False, 0, **timeoutArguments) elif (taskID == 3): - task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, 0, **timeoutArguments) + task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments) task.start() toolTasks.append(task) |