GPUVerify: merge blocks into predecessors before and after predication

Because predication produces straight line control flow, merging
after predication can dramatically reduce the number of blocks to 1
plus 2-3 per loop.  We also merge before predication, which reduces
VC complexity by reducing the number of possible values for cur.

1 files changed, 19 insertions, 3 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index fdefdebd..62f39f76 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -339,9 +339,11 @@ namespace GPUVerify
             PullOutNonLocalAccesses();

         }

 

-        

-

-        

+        private void MergeBlocksIntoPredecessors()

+        {

+            foreach (var impl in Program.TopLevelDeclarations.OfType<Implementation>())

+                VC.VCGen.MergeBlocksIntoPredecessors(Program, impl);

+        }

 

         internal void doit()

         {

@@ -401,6 +403,13 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_abstracted");

             }

 

+            MergeBlocksIntoPredecessors();

+

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_merged_pre_predication");

+            }

+

             MakeKernelPredicated();

 

             if (CommandLineOptions.ShowStages)

@@ -408,6 +417,13 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_predicated");

             }

 

+            MergeBlocksIntoPredecessors();

+

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_merged_post_predication");

+            }

+

             MakeKernelDualised();

 

             if (CommandLineOptions.ShowStages)