Added uniform expression analysis, and started using it to do less predication.

1 files changed, 132 insertions, 132 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index f4dee6d3..cb9c511e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -33,9 +33,9 @@ namespace GPUVerify
         private const string LOCAL_ID_Y_STRING = "local_id_y";

         private const string LOCAL_ID_Z_STRING = "local_id_z";

 

-        private static Constant _X = null;

-        private static Constant _Y = null;

-        private static Constant _Z = null;

+        internal static Constant _X = null;

+        internal static Constant _Y = null;

+        internal static Constant _Z = null;

 

         private Constant _GROUP_SIZE_X = null;

         private Constant _GROUP_SIZE_Y = null;

@@ -63,6 +63,8 @@ namespace GPUVerify
 

         public IRaceInstrumenter RaceInstrumenter;

 

+        public UniformityAnalyser uniformityAnalyser;

+

         public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)

         {

         }

@@ -302,7 +304,7 @@ namespace GPUVerify
 

             DoLiveVariableAnalysis();

 

-            DoSensitivityAnalysis();

+            DoUniformityAnalysis();

 

             DoArrayControlFlowAnalysis();

 

@@ -419,9 +421,10 @@ namespace GPUVerify
             // TODO

         }

 

-        private void DoSensitivityAnalysis()

+        private void DoUniformityAnalysis()

         {

-            // TODO

+            uniformityAnalyser = new UniformityAnalyser(this);

+            uniformityAnalyser.Analyse();

         }

 

         private void DoLiveVariableAnalysis()

@@ -969,65 +972,113 @@ namespace GPUVerify
             {

                 WhileCmd wc = bb.ec as WhileCmd;

 

-                Debug.Assert(wc.Guard is NAryExpr);

-                Debug.Assert((wc.Guard as NAryExpr).Args.Length == 2);

-                Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);

-                string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;

+                AddBarrierDivergenceCandidates(LocalVars, Impl, wc);

 

-                LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));

+                RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);

 

-                AddCandidateInvariant(wc, Expr.Eq(

-                    // Int type used here, but it doesn't matter as we will print and then re-parse the program

-                    new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

-                    new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

-                ));

+                AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);

+

+                AddCandidateInvariants(wc.Body, LocalVars, UserSuppliedInvariants, Impl);

+            }

+            else if (bb.ec is IfCmd)

+            {

+                // We should have done predicated execution by now, so we won't have any if statements

+                Debug.Assert(false);

+            }

+            else

+            {

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

+            }

+        }

+

+        private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, WhileCmd wc)

+        {

 

-                foreach (Variable v in LocalVars)

+            if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)

+            {

+                if (!ContainsBarrierCall(wc.Body))

                 {

-                    string lv = StripThreadIdentifier(v.Name);

+                    return;

+                }

+            }

 

-                    if (IsPredicateOrTemp(lv))

-                    {

-                        continue;

-                    }

+            Debug.Assert(wc.Guard is NAryExpr);

+            Debug.Assert((wc.Guard as NAryExpr).Args.Length == 2);

+            Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);

+            string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;

 

+            LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));

 

-                    if (!ContainsNamedVariable(GetModifiedVariables(wc.Body), StripThreadIdentifier(v.Name)))

-                    {

-                        continue;

-                    }

+            AddCandidateInvariant(wc, Expr.Eq(

+                // Int type used here, but it doesn't matter as we will print and then re-parse the program

+                new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),

+                new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))

+            ));

 

-                    AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));

+            foreach (Variable v in LocalVars)

+            {

+                string lv = StripThreadIdentifier(v.Name);

 

-                    if (Impl != KernelImplementation)

-                    {

-                        AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));                    

-                    }

+                if (IsPredicateOrTemp(lv))

+                {

+                    continue;

                 }

 

-                if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)

+                if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)

                 {

-                    foreach (Variable v in NonLocalState.getAllNonLocalVariables())

+                    if (!ContainsNamedVariable(GetModifiedVariables(wc.Body), StripThreadIdentifier(v.Name)))

                     {

-                        AddEqualityCandidateInvariant(wc, LoopPredicate, v);

+                        continue;

                     }

                 }

 

-                RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);

+                AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));

 

-                AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);

+                if (Impl != KernelImplementation)

+                {

+                    AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));

+                }

+            }

 

-                AddCandidateInvariants(wc.Body, LocalVars, UserSuppliedInvariants, Impl);

+            if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)

+            {

+                foreach (Variable v in NonLocalState.getAllNonLocalVariables())

+                {

+                    AddEqualityCandidateInvariant(wc, LoopPredicate, v);

+                }

             }

-            else if (bb.ec is IfCmd)

+        }

+

+        private bool ContainsBarrierCall(StmtList stmtList)

+        {

+            foreach (BigBlock bb in stmtList.BigBlocks)

             {

-                // We should have done predicated execution by now, so we won't have any if statements

-                Debug.Assert(false);

+                if (ContainsBarrierCall(bb))

+                {

+                    return true;

+                }

             }

-            else

+            return false;

+        }

+

+        private bool ContainsBarrierCall(BigBlock bb)

+        {

+            foreach (Cmd c in bb.simpleCmds)

             {

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

+                if (c is CallCmd && ((c as CallCmd).Proc == BarrierProcedure))

+                {

+                    return true;

+                }

+            }

+

+            if (bb.ec is WhileCmd)

+            {

+                return ContainsBarrierCall((bb.ec as WhileCmd).Body);

             }

+

+            Debug.Assert(bb.ec == null || bb.ec is BreakCmd);

+

+            return false;

         }

 

         private bool ContainsNamedVariable(HashSet<Variable> variables, string name)

@@ -1240,7 +1291,7 @@ namespace GPUVerify
             return ExistentialBooleanConstant;

         }

 

-        private string StripThreadIdentifier(string p)

+        internal static string StripThreadIdentifier(string p)

         {

             return p.Substring(0, p.IndexOf("$"));

         }

@@ -1339,77 +1390,13 @@ namespace GPUVerify
                     continue;

                 }

 

-                EnsureDisabledThreadHasNoEffect(Impl);

-

-            }

-

-        }

-

-        private void EnsureDisabledThreadHasNoEffect(Implementation Impl)

-        {

-            foreach (IdentifierExpr iex in Impl.Proc.Modifies)

-            {

-                // For some reason, this does not work well with maps

-                if (iex.Decl.TypedIdent.Type is MapType)

-                {

-                    continue;

-                }

-

-                Expr NoEffectExpr = Expr.Imp(

-                        Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" + GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),

-                        Expr.Eq(iex, new OldExpr(iex.tok, iex))

-                    );

-

-                Impl.Proc.Ensures.Add(new Ensures(false,

-                    NoEffectExpr

-                ));

-

-                AddInvariantToAllLoops(NoEffectExpr, Impl.StructuredStmts);

-

-            }

-

-            AddEnablednessInvariantToAllLoops(Impl.StructuredStmts);

-        }

-

-        private void AddEnablednessInvariantToAllLoops(StmtList stmtList)

-        {

-            foreach (BigBlock bb in stmtList.BigBlocks)

-            {

-                AddEnablednessInvariantToAllLoops(bb);

-            }

-        }

-

-        private void AddEnablednessInvariantToAllLoops(BigBlock bb)

-        {

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd wc = bb.ec as WhileCmd;

-                Debug.Assert(wc.Guard is NAryExpr);

-                Debug.Assert((wc.Guard as NAryExpr).Fun is BinaryOperator);

-                Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);

-                string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;

-                LoopPredicate = StripThreadIdentifier(LoopPredicate);

-

-                wc.Invariants.Add(

-                    new AssertCmd(wc.tok,

-                        Expr.Imp(

-                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$1", Microsoft.Boogie.Type.Bool)))),

-                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Bool))))

-                    )));

+                new EnsureDisabledThreadHasNoEffectInstrumenter(this, Impl).instrument();

 

-                wc.Invariants.Add(

-                    new AssertCmd(wc.tok,

-                        Expr.Imp(

-                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))),

-                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Bool))))

-                    )));

-

-                AddEnablednessInvariantToAllLoops(wc.Body);

             }

 

         }

 

-        private void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)

+        internal static void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)

         {

             foreach (BigBlock bb in stmtList.BigBlocks)

             {

@@ -1417,7 +1404,7 @@ namespace GPUVerify
             }

         }

 

-        private void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)

+        internal static void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)

         {

             if (bb.ec is WhileCmd)

             {

@@ -1428,7 +1415,7 @@ namespace GPUVerify
             Debug.Assert(!(bb.ec is IfCmd));

         }

 

-        private int GetThreadSuffix(string p)

+        internal static int GetThreadSuffix(string p)

         {

             return Int32.Parse(p.Substring(p.IndexOf("$") + 1, p.Length - (p.IndexOf("$") + 1)));

         }

@@ -2309,40 +2296,47 @@ namespace GPUVerify
             {

                 if (d is Procedure)

                 {

-                    if (d != KernelProcedure)

+                    Procedure proc = d as Procedure;

+                    IdentifierExpr enabled = new IdentifierExpr(proc.tok,

+                        new LocalVariable(proc.tok, new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool)));

+                    Expr predicateExpr;

+                    if (!uniformityAnalyser.IsUniform(proc.Name))

                     {

                         // Add predicate to start of parameter list

-                        Procedure proc = d as Procedure;

                         VariableSeq NewIns = new VariableSeq();

-                        TypedIdent enabled = new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool);

-                        NewIns.Add(new LocalVariable(proc.tok, enabled));

+                        NewIns.Add(enabled.Decl);

                         foreach (Variable v in proc.InParams)

                         {

                             NewIns.Add(v);

                         }

                         proc.InParams = NewIns;

+                        predicateExpr = enabled;

+                    }

+                    else

+                    {

+                        predicateExpr = Expr.True;

+                    }

 

-                        RequiresSeq newRequires = new RequiresSeq();

-                        foreach (Requires r in proc.Requires)

-                        {

-                            newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, enabled)));

-                        }

-                        proc.Requires = newRequires;

-

-                        EnsuresSeq newEnsures = new EnsuresSeq();

-                        foreach (Ensures e in proc.Ensures)

-                        {

-                            newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, enabled)));

-                        }

-                        proc.Ensures = newEnsures;

-

+                    RequiresSeq newRequires = new RequiresSeq();

+                    foreach (Requires r in proc.Requires)

+                    {

+                        newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, predicateExpr)));

+                    }

+                    proc.Requires = newRequires;

 

+                    EnsuresSeq newEnsures = new EnsuresSeq();

+                    foreach (Ensures e in proc.Ensures)

+                    {

+                        newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, predicateExpr)));

                     }

+                    proc.Ensures = newEnsures;

 

                 }

                 else if (d is Implementation)

                 {

-                    new Predicator(this, d != KernelImplementation).transform(d as Implementation);

+                    Implementation impl = d as Implementation;

+                    new Predicator(this, !uniformityAnalyser.IsUniform(impl.Name)).transform

+                        (impl);

                 }

             }

 

@@ -2494,9 +2488,15 @@ namespace GPUVerify
                     ),

                     MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));

             }

-            else

+            else if(bb.ec is IfCmd)

             {

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

+                result.ec = new IfCmd(bb.ec.tok,

+                    Expr.And(new VariableDualiser(1).VisitExpr((bb.ec as IfCmd).Guard),

+                             new VariableDualiser(2).VisitExpr((bb.ec as IfCmd).Guard)),

+                             MakeDual((bb.ec as IfCmd).thn, HalfDualise),

+                             null,

+                             (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock, HalfDualise));

+

             }

 

             return result;