diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-08-20 22:04:10 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-08-20 22:04:10 -0700 |
| commit | d8b239c0c3bd5d33f683eafb735aef41dac28760 (patch) | |
| tree | ef4ec99f794ae60458af330f57e5ba61dfda24f4 /Source/Core | |
| parent | 54c75d7af7051fdaebcb4140560ed9a7f5d4060c (diff) | |
added code to handle irreducible graphs
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 58 |
1 files changed, 50 insertions, 8 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 3a80a2ea..92005e08 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -704,13 +704,52 @@ namespace Microsoft.Boogie { foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
- impl.PruneUnreachableBlocks();
- Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
- g.ComputeLoops();
- if (!g.Reducible) {
- throw new Exception("Irreducible flow graphs are unsupported.");
+ while (true) {
+ impl.PruneUnreachableBlocks();
+ impl.ComputePredecessorsForBlocks();
+ Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
+ g.ComputeLoops();
+ if (g.Reducible) {
+ CreateProceduresForLoops(impl, g, loopImpls, fullMap);
+ break;
+ }
+
+ System.Diagnostics.Debug.Assert(g.SplitCandidates.Count > 0);
+ Block splitCandidate = null;
+ foreach (Block b in g.SplitCandidates) {
+ if (b.Predecessors.Length > 1) {
+ splitCandidate = b;
+ break;
+ }
+ }
+ System.Diagnostics.Debug.Assert(splitCandidate != null);
+ int count = 0;
+ foreach (Block b in splitCandidate.Predecessors) {
+ GotoCmd gotoCmd = (GotoCmd)b.TransferCmd;
+ gotoCmd.labelNames.Remove(splitCandidate.Label);
+ gotoCmd.labelTargets.Remove(splitCandidate);
+
+ CodeCopier codeCopier = new CodeCopier(new Hashtable(), new Hashtable());
+ CmdSeq newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);
+ TransferCmd newTransferCmd;
+ GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd;
+ if (splitGotoCmd == null) {
+ newTransferCmd = new ReturnCmd(splitCandidate.tok);
+ }
+ else {
+ StringSeq newLabelNames = new StringSeq();
+ newLabelNames.AddRange(splitGotoCmd.labelNames);
+ BlockSeq newLabelTargets = new BlockSeq();
+ newLabelTargets.AddRange(splitGotoCmd.labelTargets);
+ newTransferCmd = new GotoCmd(splitCandidate.tok, newLabelNames, newLabelTargets);
+ }
+ Block copy = new Block(splitCandidate.tok, splitCandidate.Label + count++, newCmdSeq, newTransferCmd);
+
+ impl.Blocks.Add(copy);
+ gotoCmd.AddTarget(copy);
+ copy.Predecessors.Add(b);
+ }
}
- CreateProceduresForLoops(impl, g, loopImpls, fullMap);
}
}
foreach (Implementation/*!*/ loopImpl in loopImpls) {
@@ -2697,7 +2736,7 @@ namespace Microsoft.Boogie { /// </summary>
override public void ComputeStronglyConnectedComponents() {
if (!this.BlockPredecessorsComputed)
- ComputedPredecessorsForBlocks();
+ ComputePredecessorsForBlocks();
Adjacency<Block/*!*/> next = new Adjacency<Block/*!*/>(Successors);
Adjacency<Block/*!*/> prev = new Adjacency<Block/*!*/>(Predecessors);
@@ -2759,7 +2798,10 @@ namespace Microsoft.Boogie { /// <summary>
/// Compute the predecessor informations for the blocks
/// </summary>
- private void ComputedPredecessorsForBlocks() {
+ public void ComputePredecessorsForBlocks() {
+ foreach (Block b in this.Blocks) {
+ b.Predecessors = new BlockSeq();
+ }
foreach (Block b in this.Blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
if (gtc != null) {
|