GPUVerify: add a MakeDual for unstructured blocks

2 files changed, 16 insertions, 3 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 711e1625..e6cc992b 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1924,7 +1924,7 @@ namespace GPUVerify
                 if (d is Implementation)

                 {

 

-                    new KernelDualiser(this).DualiseImplementation(d as Implementation);

+                    new KernelDualiser(this).DualiseImplementation(d as Implementation, CommandLineOptions.Unstructured);

 

                     NewTopLevelDeclarations.Add(d as Implementation);

 

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 7aba8f3d..8d51e74e 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -267,6 +267,16 @@ namespace GPUVerify
 

         }

 

+        private Block MakeDual(Block b)

+        {

+            Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);

+            foreach (Cmd c in b.Cmds)

+            {

+                MakeDual(result.Cmds, c);

+            }

+            return result;

+        }

+

         private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)

         {

             List<PredicateCmd> result = new List<PredicateCmd>();

@@ -350,14 +360,17 @@ namespace GPUVerify
         }

 

 

-        internal void DualiseImplementation(Implementation impl)

+        internal void DualiseImplementation(Implementation impl, bool unstructured)

         {

             procName = impl.Name;

 

             impl.InParams = DualiseVariableSequence(impl.InParams);

             impl.OutParams = DualiseVariableSequence(impl.OutParams);

             MakeDualLocalVariables(impl);

-            impl.StructuredStmts = MakeDual(impl.StructuredStmts);

+            if (unstructured)

+                impl.Blocks = new List<Block>(impl.Blocks.Select(MakeDual));

+            else

+                impl.StructuredStmts = MakeDual(impl.StructuredStmts);

 

             procName = null;

         }