Stream: git-cranelift

Topic: cranelift / Issue #145 Canonical, split-invariant CFG pos...

GitHub (Dec 19 2019 at 09:33):

bnjbvr closed Issue #145:

In e0fd5252d5c9d0fb0eaae5f33a2d55b197c33ad4 we landed the function DominatorTree::recompute_split_ebb() which updates the dominator tree and its cached CFG post-order after an EBB split. It looks like the way we repair the post order is not correct. Consider this example:

ebb0:
    brnz v1, ebb1
    brnz v2, ebb2
    brnz v3, ebb3
    brnz v4, ebb4
    jump ebb5

If we assume that all of ebb0's successors are not visited before ebb0 in the DFS, we get the following post order: ebb5, ebb4, ebb3, ebb2, ebb1, ebb0.

Now assume we split the EBB by inserting the ebb99 header:

ebb0:
    brnz v1, ebb1
    brnz v2, ebb2
    jump ebb99
ebb99
    brnz v3, ebb3
    brnz v4, ebb4
    jump ebb5

The post order is now: ebb5, ebb4, ebb3, ebb99, ebb2, ebb1, ebb0. Two claims:

1. The current implementation of recompute_split_ebb() is not correct because it inserts the new EBB adjacent to ebb0. As the example shows, that is not always the right insertion spot.
2. The post order currently computed by the dominator tree is split invariant. By this I mean that the effect on the post order of splitting an EBB is just to insert the new EBB header somewhere. The relative order of existing EBBs does not change. It would be good to prove this property more strictly.

Some implementation notes for fixing this:

• Assuming the post order really is split invariant, the strategy in recompute_split_ebb() of inserting the new EBB somewhere in the existing post order is correct. It is only the insertion position that needs to be fixed.
• The new EBB will always appear before the old EBB header in the post order.
• The successors to the old EBB (ebb0 in the example) do not necessarily come before the old EBB in the post order. It is possible for any of the to be visited before ebb0 along another CFG path, which would cause them to appear after ebb0 in the post order.
• If one of the successors after the split appear before ebb0 in the post order, the correct insertion point is after the first such successor.

Last updated: Dec 23 2024 at 13:07 UTC