diff options
| -rw-r--r-- | Source/Graph/Graph.cs | 32 | ||||
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 2 |
2 files changed, 26 insertions, 8 deletions
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 4a78c27f..8e5479e3 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -956,8 +956,12 @@ namespace Microsoft.Boogie.GraphUtil { }
var successors = new List<int>[n];
+ var predecessors = new List<int>[n];
int[] incomingEdges = new int[n];
+ for (int i = 0; i < n; i++)
+ predecessors[i] = new List<int>();
+
foreach (var e in g.Edges)
{
Contract.Assert(e.Item1 != null);
@@ -970,33 +974,47 @@ namespace Microsoft.Boogie.GraphUtil { successors[source].Add(target);
incomingEdges[target]++;
}
+ predecessors[target].Add(source);
}
var sortedNodes = new List<Tuple<Node, bool>>();
+ var sortedNodesInternal = new List<int>();
var regionStack = new Stack<Tuple<Node, List<int>>>();
regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
while (regionStack.Count != 0)
{
- int rootIndex = -1;
+ var rootIndexes = new List<int>();
foreach (var i in regionStack.Peek().Item2)
{
if (incomingEdges[i] == 0)
- {
- rootIndex = i;
- break;
- }
+ rootIndexes.Add(i);
}
- if (rootIndex == -1)
+ if (rootIndexes.Count() == 0)
{
var region = regionStack.Pop();
- if (regionStack.Count != 0)
+ if (regionStack.Count != 0) {
sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+ sortedNodesInternal.Add(nodeToNumber[region.Item1]);
+ }
continue;
}
+ int rootIndex = rootIndexes[0];
+ int maxPredIndex = -1;
+ foreach (var i in rootIndexes) {
+ foreach (var p in predecessors[i]) {
+ int predIndex =
+ sortedNodesInternal.FindLastIndex(x => x == p);
+ if (predIndex > maxPredIndex) {
+ rootIndex = i;
+ maxPredIndex = predIndex;
+ }
+ }
+ }
incomingEdges[rootIndex] = -1;
sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+ sortedNodesInternal.Add(rootIndex);
if (successors[rootIndex] != null)
foreach (int s in successors[rootIndex])
incomingEdges[s]--;
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 5222061f..ea526591 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -429,7 +429,7 @@ public class SmartBlockPredicator { var oldCmdSeq = block.Cmds;
block.Cmds = new List<Cmd>();
newBlocks.Add(block);
- if (prevBlock != null) {
+ if (prevBlock != null && !((prevBlock.TransferCmd is ReturnCmd) && uni != null && uni.IsUniform(impl.Name, block))) {
prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
}
|