Fix LeastCommonAncestor method in Graph module

Solves a problem with Uniformity Analysis in GPUVerify.

"The least common ancestor of two nodes u and v in a rooted tree T is a node w
that is an ancestor of both u and v and that has the greatest depth in T" (CLR).

This is needed when computing the control dependence relation of a CFG. In this
case, we need the least common ancestor of a pair of nodes in the dominator tree
so we can reuse the 'intersect' function given by Cooper et al in "A Simple,
Fast Dominance Algorithm."

The old code picked the ancestor of both u and v that has the *least* depth in
T. This caused uniformity analysis, in GPUVerify, to be imprecise (adding blocks
as non-uniform when they were infact uniform).

1 files changed, 2 insertions, 10 deletions

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 4d58cbe7..ac406bb6 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -330,17 +330,9 @@ namespace Microsoft.Boogie.GraphUtil {
 

     public Node LeastCommonAncestor(Node n1, Node n2)

     {

-        var nums = new HashSet<int>();

         int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2];

-

-        while (true)

-        {

-            if (!nums.Add(num1))

-                return postOrderNumberToNode[num1].Val;

-            if (!nums.Add(num2))

-                return postOrderNumberToNode[num2].Val;

-            num1 = doms[num1]; num2 = doms[num2];

-        }

+        int lca = intersect(num1, num2, this.doms);

+        return postOrderNumberToNode[lca].Val;

     }

   }