summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/GPUVerify/GPUVerifier.cs22
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)