Fixed bug with handling of return in GPUVerify.

2 files changed, 15 insertions, 4 deletions

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index 7f2b1d33..7fc0fcd3 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -348,7 +348,7 @@ namespace GPUVerify
                     // Add a new big block with just the assignment

                     AssignCmd assignToReturnPredicate = new AssignCmd(Token.NoToken,

                         new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, returnPredicate) }),

-                        new List<Expr>(new Expr[] { GetCurrentPredicate() }));

+                        new List<Expr>(new Expr[] { Expr.And(returnPredicate, Expr.Not(predicate.Peek ())) }));

 

                     result.Add(new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { assignToReturnPredicate }), null, null));

                     firstBigBlock.tc = null;

diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs
index 9a36233e..c910e64d 100644
--- a/Source/GPUVerify/UniformityAnalyser.cs
+++ b/Source/GPUVerify/UniformityAnalyser.cs
@@ -26,6 +26,8 @@ namespace GPUVerify
 

         private List<WhileCmd> loopStack;

 

+        private bool hitNonuniformReturn;

+

         public UniformityAnalyser(GPUVerifier verifier)

         {

             this.verifier = verifier;

@@ -113,6 +115,7 @@ namespace GPUVerify
                     {

                         if (D is Implementation)

                         {

+                            hitNonuniformReturn = false;

                             Implementation Impl = D as Implementation;

                             Analyse(Impl, uniformityInfo[Impl.Name].Key);

                         }

@@ -149,8 +152,10 @@ namespace GPUVerify
             Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);

         }

 

+

         private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)

         {

+            ControlFlowIsUniform &= !hitNonuniformReturn;

             foreach (BigBlock bb in stmtList.BigBlocks)

             {

                 Analyse(impl, bb, ControlFlowIsUniform);

@@ -159,6 +164,7 @@ namespace GPUVerify
 

         private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)

         {

+            ControlFlowIsUniform &= !hitNonuniformReturn;

             foreach (Cmd c in bb.simpleCmds)

             {

                 if (c is AssignCmd)

@@ -242,12 +248,17 @@ namespace GPUVerify
                 }

             }

 

-            if (bb.tc is ReturnCmd && !ControlFlowIsUniform && loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))

+            if (bb.tc is ReturnCmd && !ControlFlowIsUniform)

             {

-                SetNonUniform(impl.Name, loopStack[0]);

-                loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));

+                hitNonuniformReturn = true;

+                if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))

+                {

+                    SetNonUniform(impl.Name, loopStack[0]);

+                    loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));

+                }

             }

 

+

         }

 

         private int GetLoopId(WhileCmd wc)