Fixed issue with uniformity analysis and block merging. Uniformity analysis

now enabled by default.

5 files changed, 28 insertions, 11 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 5f6f0066..2f9ed792 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -25,7 +25,7 @@ namespace GPUVerify
         public static bool ShowStages = false;

 

         public static bool ShowUniformityAnalysis = false;

-        public static bool DoUniformityAnalysis = false;

+        public static bool DoUniformityAnalysis = true;

 

         public static bool ShowMayBePowerOfTwoAnalysis = false;

         public static bool ShowArrayControlFlowAnalysis = false;

@@ -116,9 +116,9 @@ namespace GPUVerify
                     ShowUniformityAnalysis = true;

                     break;

 

-                    case "-uniformityAnalysis":

-                    case "/uniformityAnalysis":

-                    DoUniformityAnalysis = true;

+                    case "-noUniformityAnalysis":

+                    case "/noUniformityAnalysis":

+                    DoUniformityAnalysis = false;

                     break;

 

                     case "-showMayBePowerOfTwoAnalysis":

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 94c460fe..f94cf5ef 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -383,8 +383,8 @@ namespace GPUVerify
         private void MergeBlocksIntoPredecessors()
         {
             foreach (var impl in Program.TopLevelDeclarations.OfType<Implementation>())
-                VC.VCGen.MergeBlocksIntoPredecessors(Program, impl);
-        }
+                VC.VCGen.MergeBlocksIntoPredecessors(Program, impl, uniformityAnalyser);
+        }

 
         internal void doit()
         {
diff --git a/Source/VCGeneration/SmartBlockPredicator.cs b/Source/VCGeneration/SmartBlockPredicator.cs
index 9dada1a5..b4f5a3df 100644
--- a/Source/VCGeneration/SmartBlockPredicator.cs
+++ b/Source/VCGeneration/SmartBlockPredicator.cs
@@ -371,7 +371,7 @@ public class SmartBlockPredicator {
 
         if (n.Item2) {
           var backedgeBlock = new Block();
-          newBlocks.Add(backedgeBlock);
+          newBlocks.Add(backedgeBlock);

 
           backedgeBlock.Label = n.Item1.Label + ".backedge";
           backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
@@ -384,7 +384,12 @@ public class SmartBlockPredicator {
 
           tailBlock.Label = n.Item1.Label + ".tail";
           tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
-                                               Expr.Not(pExpr)));
+                                               Expr.Not(pExpr)));

+

+          if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {

+            uni.AddNonUniform(impl.Name, backedgeBlock);

+            uni.AddNonUniform(impl.Name, tailBlock);

+          }
 
           if (prevBlock != null)
             prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/VCGeneration/UniformityAnalyser.cs
index e5647a21..849333b3 100644
--- a/Source/VCGeneration/UniformityAnalyser.cs
+++ b/Source/VCGeneration/UniformityAnalyser.cs
@@ -520,6 +520,13 @@ namespace Microsoft.Boogie
                 Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
                 uniformityInfo[proc].Value[v] = false;
             }
+        }

+

+        public void AddNonUniform(string proc, Block b) {

+          if (nonUniformBlocks.ContainsKey(proc)) {

+            Debug.Assert(!nonUniformBlocks[proc].Contains(b));

+            nonUniformBlocks[proc].Add(b);

+          }

         }
 
         public bool IsUniform(string proc, WhileCmd wc)
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 2ac8dc83..e7f5999a 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3042,15 +3042,20 @@ namespace VC {
     /// <summary>

     /// Simplifies the CFG of the given implementation impl by merging each

     /// basic block with a single predecessor into that predecessor if the

-    /// predecessor has a single successor.

+    /// predecessor has a single successor.  If a uniformity analyser is

+    /// being used then block will only be merged if they are both uniform

+    /// or both non-uniform

     /// </summary>

-    public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl) {

+    public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni) {

       var blockGraph = prog.ProcessLoops(impl);

       var predMap = new Dictionary<Block, Block>();

       foreach (var block in blockGraph.Nodes) {

         try {

           var pred = blockGraph.Predecessors(block).Single();

-          if (blockGraph.Successors(pred).Single() == block) {

+          if (blockGraph.Successors(pred).Single() == block &&

+              (uni == null || 

+              (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||

+              (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block)))) {

             Block predMapping;

             while (predMap.TryGetValue(pred, out predMapping))

               pred = predMapping;