Added support for break and return.

5 files changed, 187 insertions, 19 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index c0987296..078c3d10 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -290,6 +290,8 @@ namespace GPUVerify
 

         internal void preProcess()

         {

+            RemoveRedundantReturns();

+

             RemoveElseIfs();

 

             AddStartAndEndBarriers();

@@ -539,7 +541,9 @@ namespace GPUVerify
 

             foreach (PredicateCmd p in invariants)

             {

-                result.Add(new AssertCmd(p.tok, new AccessInvariantProcessor().VisitExpr(p.Expr.Clone() as Expr)));

+                PredicateCmd newP = new AssertCmd(p.tok, new AccessInvariantProcessor().VisitExpr(p.Expr.Clone() as Expr));

+                newP.Attributes = p.Attributes;

+                result.Add(newP);

             }

 

             return result;

@@ -1674,6 +1678,17 @@ namespace GPUVerify
             }

         }

 

+        private void RemoveRedundantReturns()

+        {

+            foreach (Declaration d in Program.TopLevelDeclarations)

+            {

+                if (d is Implementation)

+                {

+                    RemoveRedundantReturns((d as Implementation).StructuredStmts);

+                }

+            }

+        }

+

         private StmtList RemoveElseIfs(StmtList stmtList)

         {

             Contract.Requires(stmtList != null);

@@ -1688,6 +1703,18 @@ namespace GPUVerify
             return result;

         }

 

+        private void RemoveRedundantReturns(StmtList stmtList)

+        {

+            Contract.Requires(stmtList != null);

+

+            BigBlock bb = stmtList.BigBlocks[stmtList.BigBlocks.Count - 1];

+

+            if (bb.tc is ReturnCmd)

+            {

+                bb.tc = null;

+            }

+        }

+

         private BigBlock RemoveElseIfs(BigBlock bb)

         {

             BigBlock result = bb;

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 6f6d7184..41546a84 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -290,6 +290,14 @@ namespace GPUVerify
                              (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock, HalfDualise));

 

             }

+            else if (bb.ec is BreakCmd)

+            {

+                result.ec = bb.ec;

+            }

+            else

+            {

+                Debug.Assert(bb.ec == null);

+            }

 

             return result;

 

@@ -300,12 +308,18 @@ namespace GPUVerify
             List<PredicateCmd> result = new List<PredicateCmd>();

             foreach (PredicateCmd p in originalInvariants)

             {

-                result.Add(new AssertCmd(p.tok, 

-                    Dualise(p.Expr, 1)));

+                {

+                    PredicateCmd newP = new AssertCmd(p.tok,

+                        Dualise(p.Expr, 1));

+                    newP.Attributes = p.Attributes;

+                    result.Add(newP);

+                }

                 if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))

                     && !verifier.uniformityAnalyser.IsUniform(procName, p.Expr))

                 {

-                    result.Add(new AssertCmd(p.tok, Dualise(p.Expr, 2)));

+                    PredicateCmd newP = new AssertCmd(p.tok, Dualise(p.Expr, 2));

+                    newP.Attributes = p.Attributes;

+                    result.Add(newP);

                 }

             }

 

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index 4dab448b..7f2b1d33 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -17,6 +17,9 @@ namespace GPUVerify
         private Stack<Expr> predicate;

         private Stack<Expr> enclosingLoopPredicate;

 

+        private IdentifierExpr returnPredicate;

+        private bool hitNonuniformReturn;

+

         private Implementation impl = null;

 

         internal Predicator(GPUVerifier verifier, bool AddPredicateParameter) : base(verifier)

@@ -54,16 +57,36 @@ namespace GPUVerify
             predicate.Push(Predicate);

             enclosingLoopPredicate.Push(Expr.True);

 

+            Variable ReturnPredicateVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "_R", Microsoft.Boogie.Type.Bool));

+            returnPredicate = new IdentifierExpr(Token.NoToken, ReturnPredicateVariable);

+            hitNonuniformReturn = false;

+

             impl.StructuredStmts = VisitStmtList(impl.StructuredStmts);

 

             AddPredicateLocalVariables(impl);

 

+            if (hitNonuniformReturn)

+            {

+                impl.LocVars.Add(ReturnPredicateVariable);

+                verifier.uniformityAnalyser.AddNonUniform(impl.Name, ReturnPredicateVariable.Name);

+

+                CmdSeq newSimpleCmds = new CmdSeq();

+                newSimpleCmds.Add(new AssignCmd(Token.NoToken,

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

+                    new List<Expr>(new Expr[] { Expr.True })));

+                foreach (Cmd c in impl.StructuredStmts.BigBlocks[0].simpleCmds)

+                {

+                    newSimpleCmds.Add(c);

+                }

+                impl.StructuredStmts.BigBlocks[0].simpleCmds = newSimpleCmds;

+            }

+

             this.impl = null;

         }

 

         public override CmdSeq VisitCmd(Cmd c)

         {

-            if (c is CallCmd || !predicate.Peek().Equals(Expr.True))

+            if (c is CallCmd || !GetCurrentPredicate().Equals(Expr.True))

             {

                 return base.VisitCmd(c);

             }

@@ -78,7 +101,7 @@ namespace GPUVerify
 

             if (!verifier.uniformityAnalyser.IsUniform(Call.callee))

             {

-                NewIns.Add(predicate.Peek());

+                NewIns.Add(GetCurrentPredicate());

             }

 

             foreach (Expr e in Call.Ins)

@@ -99,7 +122,7 @@ namespace GPUVerify
             Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

 

             ExprSeq iteArgs = new ExprSeq();

-            iteArgs.Add(predicate.Peek());

+            iteArgs.Add(GetCurrentPredicate());

             iteArgs.Add(assign.Rhss.ElementAt(0));

             iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);

             NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);

@@ -117,7 +140,7 @@ namespace GPUVerify
 

             Debug.Assert(havoc.Vars.Length == 1);

 

-            if (predicate.Peek().Equals(Expr.True))

+            if (GetCurrentPredicate().Equals(Expr.True))

             {

                 result.Add(havoc);

                 return result;

@@ -144,7 +167,7 @@ namespace GPUVerify
 

             List<Expr> rhss = new List<Expr>();

             rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(

-                new Expr[] { predicate.Peek(), HavocTempExpr, havoc.Vars[0] })));

+                new Expr[] { GetCurrentPredicate(), HavocTempExpr, havoc.Vars[0] })));

 

             result.Add(new AssignCmd(havoc.tok, lhss, rhss));

 

@@ -155,14 +178,14 @@ namespace GPUVerify
         public override CmdSeq VisitAssertCmd(AssertCmd assert)

         {

             return new CmdSeq(new Cmd[] {

-                new AssertCmd(assert.tok, Expr.Imp(predicate.Peek(), assert.Expr))

+                new AssertCmd(assert.tok, Expr.Imp(GetCurrentPredicate(), assert.Expr))

             });

         }

 

         public override CmdSeq VisitAssumeCmd(AssumeCmd assume)

         {

             return new CmdSeq(new Cmd[] {

-                new AssumeCmd(assume.tok, Expr.Imp(predicate.Peek(), assume.Expr))

+                new AssumeCmd(assume.tok, Expr.Imp(GetCurrentPredicate(), assume.Expr))

             });

         }

 

@@ -179,12 +202,19 @@ namespace GPUVerify
             {

                 WhileCmd whileCmd = bb.ec as WhileCmd;

 

+                if (!hitNonuniformReturn && verifier.uniformityAnalyser.HasNonuniformReturn(impl.Name, whileCmd))

+                {

+                    hitNonuniformReturn = true;

+                }

+

                 Expr PredicateExpr;

                 Expr NewGuard;

                 string LoopPredicate = null;

                 List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();

 

-                if (!enclosingLoopPredicate.Peek().Equals(Expr.True) || !verifier.uniformityAnalyser.IsUniform(impl.Name, whileCmd.Guard))

+                if (!enclosingLoopPredicate.Peek().Equals(Expr.True) || 

+                    !verifier.uniformityAnalyser.IsUniform(impl.Name, whileCmd.Guard) ||

+                    !verifier.uniformityAnalyser.IsUniform(impl.Name, whileCmd))

                 {

                     LoopPredicate = "_LC" + WhileLoopCounter;

                     WhileLoopCounter++;

@@ -198,8 +228,8 @@ namespace GPUVerify
                     WhilePredicateLhss.Add(new SimpleAssignLhs(whileCmd.tok, PredicateExpr as IdentifierExpr));

 

                     List<Expr> WhilePredicateRhss = new List<Expr>();

-                    WhilePredicateRhss.Add(predicate.Peek().Equals(Expr.True) ? 

-                        whileCmd.Guard : Expr.And(predicate.Peek(), whileCmd.Guard));

+                    WhilePredicateRhss.Add(GetCurrentPredicate().Equals(Expr.True) ? 

+                        whileCmd.Guard : Expr.And(GetCurrentPredicate(), whileCmd.Guard));

 

                     firstBigBlock.simpleCmds.Add(new AssignCmd(whileCmd.tok, WhilePredicateLhss, WhilePredicateRhss));

 

@@ -242,7 +272,7 @@ namespace GPUVerify
                     throw new InvalidOperationException();

                 }

 

-                if (predicate.Peek().Equals(Expr.True) && verifier.uniformityAnalyser.IsUniform(impl.Name, IfCommand.Guard))

+                if (GetCurrentPredicate().Equals(Expr.True) && verifier.uniformityAnalyser.IsUniform(impl.Name, IfCommand.Guard))

                 {

                     firstBigBlock.ec = 

                         new IfCmd(IfCommand.tok, IfCommand.Guard, VisitStmtList(IfCommand.thn),

@@ -286,18 +316,17 @@ namespace GPUVerify
             }

             else if (bb.ec is BreakCmd)

             {

-                if (enclosingLoopPredicate.Equals(Expr.True))

+                if (enclosingLoopPredicate.Peek().Equals(Expr.True))

                 {

                     firstBigBlock.ec = bb.ec;

                 }

                 else

                 {

-

                     firstBigBlock.simpleCmds.Add(new AssignCmd(bb.tok,

                         new List<AssignLhs>(new AssignLhs[] { 

                             new SimpleAssignLhs(bb.tok, enclosingLoopPredicate.Peek() as IdentifierExpr) }),

                         new List<Expr>(new Expr[] { new NAryExpr(bb.tok, new IfThenElse(bb.tok), new ExprSeq(

-                            new Expr[] { predicate.Peek(), Expr.False, enclosingLoopPredicate.Peek() })) })

+                            new Expr[] { GetCurrentPredicate(), Expr.False, enclosingLoopPredicate.Peek() })) })

                         ));

                     firstBigBlock.ec = null;

                 }

@@ -307,10 +336,47 @@ namespace GPUVerify
                 throw new InvalidOperationException();

             }

 

+            if (bb.tc is ReturnCmd)

+            {

+                if (!GetCurrentPredicate().Equals(Expr.True))

+                {

+                    hitNonuniformReturn = true;

+                }

+

+                if (hitNonuniformReturn)

+                {

+                    // 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() }));

+

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

+                    firstBigBlock.tc = null;

+                }

+

+            }

+

+            result[result.Count - 1].tc = firstBigBlock.tc;

+

+            if (result.Count > 1)

+            {

+                firstBigBlock.tc = null;

+            }

+

             return result;

 

         }

 

+        private Expr GetCurrentPredicate()

+        {

+            if (!hitNonuniformReturn)

+            {

+                return predicate.Peek();

+            }

+

+            return Expr.And(predicate.Peek(), returnPredicate);

+        }

+

         public override IfCmd VisitIfCmd(IfCmd ifCmd)

         {

             throw new InvalidOperationException();

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 47591c1b..b380a595 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -804,6 +804,10 @@ namespace GPUVerify
                     AddNoRaceInvariants((bb.ec as IfCmd).elseBlock);

                 }

             }

+            else if (bb.ec is BreakCmd)

+            {

+                // Do nothing

+            }

             else

             {

                 Debug.Assert(bb.ec == null);

diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs
index 072688a0..9a36233e 100644
--- a/Source/GPUVerify/UniformityAnalyser.cs
+++ b/Source/GPUVerify/UniformityAnalyser.cs
@@ -16,16 +16,25 @@ namespace GPUVerify
 

         private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;

 

+        private Dictionary<string, HashSet<int>> nonUniformLoops;

+

+        private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;

+

         private Dictionary<string, List<string>> inParameters;

 

         private Dictionary<string, List<string>> outParameters;

 

+        private List<WhileCmd> loopStack;

+

         public UniformityAnalyser(GPUVerifier verifier)

         {

             this.verifier = verifier;

             uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();

+            nonUniformLoops = new Dictionary<string, HashSet<int>>();

+            loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();

             inParameters = new Dictionary<string, List<string>>();

             outParameters = new Dictionary<string, List<string>>();

+            loopStack = new List<WhileCmd>();

         }

 

         internal void Analyse()

@@ -42,6 +51,9 @@ namespace GPUVerify
                     uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>

                         (uniformProcedure, new Dictionary<string, bool> ()));

 

+                    nonUniformLoops.Add(Impl.Name, new HashSet<int>());

+                    loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());

+

                     SetNonUniform(Impl.Name, GPUVerifier._X.Name);

                     SetNonUniform(Impl.Name, GPUVerifier._Y.Name);

                     SetNonUniform(Impl.Name, GPUVerifier._Z.Name);

@@ -207,7 +219,10 @@ namespace GPUVerify
             if (bb.ec is WhileCmd)

             {

                 WhileCmd wc = bb.ec as WhileCmd;

-                Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard));

+                loopStack.Add(wc);

+                Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) && 

+                    !nonUniformLoops[impl.Name].Contains(GetLoopId(wc)));

+                loopStack.RemoveAt(loopStack.Count - 1);

             }

             else if (bb.ec is IfCmd)

             {

@@ -219,7 +234,27 @@ namespace GPUVerify
                 }

                 Debug.Assert(ifCmd.elseIf == null);

             }

+            else if (bb.ec is BreakCmd)

+            {

+                if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1])))

+                {

+                    SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]);

+                }

+            }

+

+            if (bb.tc is ReturnCmd && !ControlFlowIsUniform && 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)

+        {

+            AssertCmd inv = wc.Invariants[0] as AssertCmd;

+            Debug.Assert(inv.Attributes.Key.Contains("loophead_"));

+            return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));

         }

 

         private void SetNonUniform(string procedureName)

@@ -229,6 +264,12 @@ namespace GPUVerify
             RecordProcedureChanged();

         }

 

+        private void SetNonUniform(string procedureName, WhileCmd wc)

+        {

+            nonUniformLoops[procedureName].Add(GetLoopId(wc));

+            RecordProcedureChanged();

+        }

+

         internal bool IsUniform(string procedureName)

         {

             if (!uniformityInfo.ContainsKey(procedureName))

@@ -299,6 +340,12 @@ namespace GPUVerify
                     Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);

                 }

                 Console.WriteLine("]");

+                Console.Write("Non-uniform loops:");

+                foreach (int l in nonUniformLoops[p])

+                {

+                    Console.Write(" " + l);

+                }

+                Console.WriteLine();

             }

         }

 

@@ -327,6 +374,16 @@ namespace GPUVerify
                 uniformityInfo[proc].Value[v] = false;

             }

         }

+

+        internal bool IsUniform(string proc, WhileCmd wc)

+        {

+            return !nonUniformLoops[proc].Contains(GetLoopId(wc));

+        }

+

+        internal bool HasNonuniformReturn(string proc, WhileCmd whileCmd)

+        {

+            return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd));

+        }

     }

 

 }