[PATCH] D35851: [Dominators] Include infinite loops in PostDominatorTree

[Jakub Kuderski via Phabricator via llvm-commits]

kuhar added a comment.

Tobias,

To quickly address some of the remaining points:

In https://reviews.llvm.org/D35851#829390, @grosser wrote:

> > but here’s what happens when you call .deleteEdge with my patch: it first performs the edge deletion and can then immediately makes an insertion from the virtual exit to the reverse-unreachable code. From the end user’s perspective, those two steps happen atomically, but in reality it performs two different operations with an intermediate result not observable from outside. If you consider these two internal steps in terms of the parent and sibling property, the first one holds after deletion and the second one after insertion.
>
> Interesting! Do I understand correctly that for  a normal compete (post)dominator tree these two steps fall together. Hence, both parent and sibling property hold always?


Yes, although you cannot assume that the .deleteEdge call doesn't affect the parent property, as internally may result in an insertion. Even then, both parent and sibling property hold the whole time -- between the internal deletion an insertion, and after the whole function ends.

> Thank you for explaining the above. Yes, verify is verifying under the assumption that no virtual edges are added. Without virtual edges, the properties certainly hold. This difference is again something interesting to point out.

The properties hold all the time -- the thing is that the set of virtual exit's predecessor is stored only in the tree, and if you were to compute it just looking at the CFG you get an answer that assumes that the insertion already happened. If we made it a special case of root finding, then calling .verifyRootf before the internal insertion would also work, and thus the whole .veirfy.

> I fully agree that post-dominance alone is not sufficient. This seems contrary to the impression @kuhar's reply made to me

I tried to point out that it's necessary but not sufficient by saying:

> ...  (assuming that we already proved that it is (fine) from other standpoints) ...


https://reviews.llvm.org/D35851