ContinueTargetStructurallyDominatesBackEdge axiom slightly too strong?

[johnwickerson]

Consider the ContinueTargetStructurallyDominatesBackEdge axiom here. Explanation as follows:

• ~continue.~backEdge gives us the set of pairs (A,B) where A is the continue target of some loop header and there is a back-edge from B to that loop header.
• When we add StructurallyReachableBlock <: ... we are saying that A is structurally reachable.
• The predicate asserts that under these circumstances, A must structually dominate B.
• We add the condition that A is structurally reachable because we only wish to impose this rule on blocks in the CFG that are structurally reachable.
• But we are only insisting that A is structurally reachable. We are not requiring B or the loop header to be structurally reachable too, and the arrows are pointing the wrong way to make the inference that B is structurally reachable too.
• So it seems possible that the axiom is slightly too strong. Perhaps there could be a situation where A is structurally reachable and B is not, but we are nonetheless insisting that A structurally dominates B.

Possible fix: require that B is structurally reachable. (From this, it follows that A is structurally reachable too.) That is, change

pred ContinueTargetStructurallyDominatesBackEdge 
{
    StructurallyReachableBlock <: (~continue.~backEdge) in structurallyDominates
}

to

pred ContinueTargetStructurallyDominatesBackEdge 
{
    (~continue.~backEdge) :> StructurallyReachableBlock in structurallyDominates
}

or

pred ContinueTargetStructurallyDominatesBackEdge 
{
    StructurallyReachableBlock <: (backEdge.continue) in ~structurallyDominates
}

[vili-1]

But in my solution, constraining that A is structurally reachable and that A structurally dominates B, it implies that B is structurally reachable, too (structural dominance implies structural reachability).

Your alternatives work, too, but are not orthogonal. When you say:

require that B is structurally reachable. (From this, it follows that A is structurally reachable too.)

the conclusion derives from other rules like: BackEdgesBranchToLoopHeader

[johnwickerson]

Hmm, I'm not sure... the thing is, the fact about A structurally dominating B is on the other side of the implication.

To be concrete: suppose I have a graph that looks like this.

                    EntryPoint
                        |
                      jump
                        |
                        v
B -jump-> H -continue-> A

The current ContinueTargetStructurallyDominatesBackEdge predicate does not hold for this graph. But my reformulated predicate does hold.

There are presumably other predicates that do not hold for this graph, making my point a bit moot. But still, it means that the current definition of this predicate is a little hard to explain in isolation.

[vili-1]

Now that the tennis game ended I can see you are right :) Our formulations disagree between them when there are structurally unreachable blocks in the graph.

[johnwickerson]

I'm glad we agree :).

In which case, I think I'll write about a different predicate in the paper (maybe BackEdgeStructurallyPostDominatesContinueTarget, which doesn't have this problem). That way, the paper-writing isn't blocked by needing to fix the ContinueTargetStructurallyDominatesBackEdge predicate.

In due course, I think the neater of my two proposed ways to fix the ContinueTargetStructurallyDominatesBackEdge predicate is the second one, StructurallyReachableBlock <: (backEdge.continue) in ~structurallyDominates.