Added "may be tid" analysis.

8 files changed, 344 insertions, 31 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 78b3f51d..e775689c 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -30,12 +30,14 @@ namespace GPUVerify
 

         public static bool ShowStages = false;

 

-        public static bool AddDivergenceCandidatesOnlyIfModified = false;

-        public static bool AddDivergenceCandidatesOnlyToBarrierLoops = false;

+        public static bool AddDivergenceCandidatesOnlyIfModified = true;

+        public static bool AddDivergenceCandidatesOnlyToBarrierLoops = true;

 

         public static bool ShowUniformityAnalysis = false;

         public static bool DoUniformityAnalysis = true;

 

+        public static bool ShowMayBeTidAnalysis = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -141,14 +143,9 @@ namespace GPUVerify
                     ArrayEqualities = true;

                     break;

 

-                    case "-addDivergenceCandidatesOnlyIfModified":

-                    case "/addDivergenceCandidatesOnlyIfModified":

-                    AddDivergenceCandidatesOnlyIfModified = true;

-                    break;

-

-                    case "-addDivergenceCandidatesOnlyToBarrierLoops":

-                    case "/addDivergenceCandidatesOnlyToBarrierLoops":

-                    AddDivergenceCandidatesOnlyToBarrierLoops = true;

+                    case "-alwaysAddDivergenceCandidates":

+                    AddDivergenceCandidatesOnlyIfModified = false;

+                    AddDivergenceCandidatesOnlyToBarrierLoops = false;

                     break;

 

                     case "-showUniformityAnalysis":

@@ -161,6 +158,11 @@ namespace GPUVerify
                     DoUniformityAnalysis = false;

                     break;

 

+                    case "-showMayBeTidAnalysis":

+                    case "/showMayBeTidAnalysis":

+                    ShowMayBeTidAnalysis = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index fe0fdeba..48935806 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -64,6 +64,7 @@ namespace GPUVerify
         public IRaceInstrumenter RaceInstrumenter;

 

         public UniformityAnalyser uniformityAnalyser;

+        public MayBeTidAnalyser mayBeTidAnalyser;

 

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

         {

@@ -306,6 +307,8 @@ namespace GPUVerify
 

             DoUniformityAnalysis();

 

+            DoMayBeTidAnalysis();

+

             DoArrayControlFlowAnalysis();

 

             if (CommandLineOptions.ShowStages)

@@ -416,6 +419,12 @@ namespace GPUVerify
 

         }

 

+        private void DoMayBeTidAnalysis()

+        {

+            mayBeTidAnalyser = new MayBeTidAnalyser(this);

+            mayBeTidAnalyser.Analyse();

+        }

+

         private void DoArrayControlFlowAnalysis()

         {

             // TODO

@@ -822,7 +831,7 @@ namespace GPUVerify
             return result;

         }

 

-        internal static bool ContainsNamedVariable(HashSet<Variable> variables, string name)

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

         {

             foreach(Variable v in variables)

             {

@@ -991,7 +1000,11 @@ namespace GPUVerify
 

         internal static string StripThreadIdentifier(string p)

         {

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

+            if (p.Contains("$"))

+            {

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

+            }

+            return p;

         }

 

         private void AddStartAndEndBarriers()

@@ -1181,7 +1194,7 @@ namespace GPUVerify
             AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);

         }

 

-        private Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)

+        internal static Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)

         {

             return new NAryExpr(lhs.tok, new FunctionCall(new Function(lhs.tok, functionName, new VariableSeq(new Variable[] { 

                 new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "arg1", Microsoft.Boogie.Type.GetBvType(32))),

@@ -2093,5 +2106,18 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

         }

 

+        internal Implementation GetImplementation(string procedureName)

+        {

+            foreach (Declaration D in Program.TopLevelDeclarations)

+            {

+                if (D is Implementation && ((D as Implementation).Name == procedureName))

+                {

+                    return D as Implementation;

+                }

+            }

+            Debug.Assert(false);

+            return null;

+        }

+

     }

 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index c216d089..4b996908 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -110,6 +110,7 @@
     <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />

     <Compile Include="KernelDualiser.cs" />

     <Compile Include="LoopInvariantGenerator.cs" />

+    <Compile Include="MayBeTidAnalyser.cs" />

     <Compile Include="StructuredProgramVisitor.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

     <Compile Include="EnabledToPredicateVisitor.cs" />

@@ -132,6 +133,7 @@
     <Compile Include="UniformExpressionAnalysisVisitor.cs" />

     <Compile Include="UniformityAnalyser.cs" />

     <Compile Include="VariableDualiser.cs" />

+    <Compile Include="VariablesOccurringInExpressionVisitor.cs" />

     <Compile Include="WriteCollector.cs" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs
index 4ec6de6c..c3851a29 100644
--- a/Source/GPUVerify/LoopInvariantGenerator.cs
+++ b/Source/GPUVerify/LoopInvariantGenerator.cs
@@ -3,6 +3,7 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Text;

 using Microsoft.Boogie;

+using Microsoft.Basetypes;

 using System.Diagnostics;

 

 namespace GPUVerify

@@ -72,6 +73,11 @@ namespace GPUVerify
                 }

             }

 

+            if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))

+            {

+                return;

+            }

+

             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);

@@ -87,6 +93,12 @@ namespace GPUVerify
 

             foreach (Variable v in LocalVars)

             {

+

+                if (verifier.uniformityAnalyser.IsUniform(Impl.Name, v.Name))

+                {

+                    continue;

+                }

+

                 string lv = GPUVerifier.StripThreadIdentifier(v.Name);

 

                 if (GPUVerifier.IsPredicateOrTemp(lv))

@@ -96,7 +108,7 @@ namespace GPUVerify
 

                 if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)

                 {

-                    if (!GPUVerifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), 

+                    if (!verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), 

                         GPUVerifier.StripThreadIdentifier(v.Name)))

                     {

                         continue;

@@ -136,6 +148,8 @@ namespace GPUVerify
 

                 AddBarrierDivergenceCandidates(LocalVars, Impl, wc);

 

+                AddLoopVariableBoundsCandidateInvariants(Impl, wc);

+

                 verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);

 

                 AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);

@@ -153,6 +167,39 @@ namespace GPUVerify
             }

         }

 

+        private void AddLoopVariableBoundsCandidateInvariants(Implementation Impl, WhileCmd wc)

+        {

+            if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))

+            {

+                VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();

+                visitor.VisitExpr(wc.Guard);

+                foreach (Variable v in visitor.GetVariables())

+                {

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

+                    {

+                        continue;

+                    }

+

+                    if (IsBVType (v.TypedIdent.Type))

+                    {

+                        int BVWidth = (v.TypedIdent.Type as BvType).Bits;

+

+                        verifier.AddCandidateInvariant(wc,

+                                GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",

+                                new IdentifierExpr(v.tok, v),

+                                new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)));

+                    }

+                }

+            }

+        }

+

+        private bool IsBVType(Microsoft.Boogie.Type type)

+        {

+            return type.Equals(Microsoft.Boogie.Type.GetBvType(32))

+                || type.Equals(Microsoft.Boogie.Type.GetBvType(16))

+                || type.Equals(Microsoft.Boogie.Type.GetBvType(8));

+        }

+

         private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)

         {

             foreach (Expr e in UserSuppliedInvariants)

diff --git a/Source/GPUVerify/MayBeTidAnalyser.cs b/Source/GPUVerify/MayBeTidAnalyser.cs
new file mode 100644
index 00000000..990559c2
--- /dev/null
+++ b/Source/GPUVerify/MayBeTidAnalyser.cs
@@ -0,0 +1,220 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class MayBeTidAnalyser

+    {

+

+        private GPUVerifier verifier;

+

+        private bool ProcedureChanged;

+

+        private Dictionary<string, Dictionary<string, bool>> mayBeTidInfo;

+

+        public MayBeTidAnalyser(GPUVerifier verifier)

+        {

+            this.verifier = verifier;

+            mayBeTidInfo = new Dictionary<string, Dictionary<string, bool>>();

+        }

+

+        internal void Analyse()

+        {

+            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

+            {

+                if(D is Implementation)

+                {

+                    Implementation Impl = D as Implementation;

+                    mayBeTidInfo.Add(Impl.Name, new Dictionary<string, bool> ());

+

+                    SetMayBeTid(Impl.Name, GPUVerifier._X.Name);

+                    SetNotTid(Impl.Name, GPUVerifier._Y.Name);

+                    SetNotTid(Impl.Name, GPUVerifier._Z.Name);

+

+                    foreach (Variable v in Impl.LocVars)

+                    {

+                        SetMayBeTid(Impl.Name, v.Name);

+                    }

+

+                    foreach (Variable v in Impl.InParams)

+                    {

+                        SetMayBeTid(Impl.Name, v.Name);

+                    }

+

+                    foreach (Variable v in Impl.OutParams)

+                    {

+                        SetMayBeTid(Impl.Name, v.Name);

+                    }

+

+                    ProcedureChanged = true;

+                }

+            }

+

+            while (ProcedureChanged)

+            {

+                ProcedureChanged = false;

+

+                foreach (Declaration D in verifier.Program.TopLevelDeclarations)

+                {

+                    if (D is Implementation)

+                    {

+                        Implementation Impl = D as Implementation;

+                        Analyse(Impl);

+                    }

+                }

+            }

+

+            if (CommandLineOptions.ShowMayBeTidAnalysis)

+            {

+                dump();

+            }

+        }

+

+        private void Analyse(Implementation Impl)

+        {

+            Analyse(Impl, Impl.StructuredStmts);

+        }

+

+        private void Analyse(Implementation impl, StmtList stmtList)

+        {

+            foreach (BigBlock bb in stmtList.BigBlocks)

+            {

+                Analyse(impl, bb);

+            }

+        }

+

+        private void Analyse(Implementation impl, BigBlock bb)

+        {

+            foreach (Cmd c in bb.simpleCmds)

+            {

+                if (c is AssignCmd)

+                {

+                    AssignCmd assignCmd = c as AssignCmd;

+                    Debug.Assert(assignCmd.Lhss.Count == 1);

+                    Debug.Assert(assignCmd.Rhss.Count == 1);

+                    if (assignCmd.Lhss[0] is SimpleAssignLhs)

+                    {

+                        SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;

+                        Expr rhs = assignCmd.Rhss[0];

+

+                        if (MayBeTid (impl.Name, lhs.AssignedVariable.Name)

+                            && !MayBeTid(impl.Name, rhs))

+                        {

+                            SetNotTid (impl.Name, lhs.AssignedVariable.Name);

+                        }

+

+                    }

+                }

+                else if (c is CallCmd)

+                {

+                    CallCmd callCmd = c as CallCmd;

+

+                    if (callCmd.callee != verifier.BarrierProcedure.Name)

+                    {

+

+                        Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

+                        for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

+                        {

+                            if (MayBeTid(callCmd.callee, CalleeImplementation.InParams[i].Name)

+                                && !MayBeTid(impl.Name, callCmd.Ins[i]))

+                            {

+                                SetNotTid(callCmd.callee, CalleeImplementation.InParams[i].Name);

+                            }

+                        }

+

+                        for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)

+                        {

+                            if (MayBeTid(impl.Name, callCmd.Outs[i].Name)

+                                && !MayBeTid(callCmd.callee, CalleeImplementation.OutParams[i].Name))

+                            {

+                                SetNotTid(impl.Name, callCmd.Outs[i].Name);

+                            }

+                        }

+

+                    }

+                    else if (c is HavocCmd)

+                    {

+                        HavocCmd havoc = c as HavocCmd;

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

+

+                        if (MayBeTid(impl.Name, havoc.Vars[0].Decl.Name))

+                        {

+                            SetNotTid(impl.Name, havoc.Vars[0].Decl.Name);

+                        }

+                    }

+                }

+            }

+

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd wc = bb.ec as WhileCmd;

+                Analyse(impl, wc.Body);

+            }

+            else if (bb.ec is IfCmd)

+            {

+                IfCmd ifCmd = bb.ec as IfCmd;

+                Analyse(impl, ifCmd.thn);

+                if (ifCmd.elseBlock != null)

+                {

+                    Analyse(impl, ifCmd.elseBlock);

+                }

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

+            }

+

+        }

+

+        private void SetNotTid(string proc, string v)

+        {

+            mayBeTidInfo[proc][v] = false;

+            ProcedureChanged = true;

+        }

+

+        private void SetMayBeTid(string proc, string v)

+        {

+            mayBeTidInfo[proc][v] = true;

+        }

+

+        internal bool MayBeTid(string proc, string v)

+        {

+            if (!mayBeTidInfo.ContainsKey(proc))

+            {

+                return false;

+            }

+

+            if (!mayBeTidInfo[proc].ContainsKey(v))

+            {

+                return false;

+            }

+

+            return mayBeTidInfo[proc][v];

+        }

+

+        internal bool MayBeTid(string proc, Expr e)

+        {

+            if (e is IdentifierExpr)

+            {

+                return MayBeTid(proc, (e as IdentifierExpr).Decl.Name);

+            }

+            return false;

+        }

+

+        private void dump()

+        {

+            foreach (string p in mayBeTidInfo.Keys)

+            {

+                Console.WriteLine("Procedure " + p);

+                foreach (string v in mayBeTidInfo[p].Keys)

+                {

+                    Console.WriteLine("  " + v + ": " +

+                        (mayBeTidInfo[p][v] ? "may be tid" : "likely not tid"));

+                }

+            }

+

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index a1938376..4dab448b 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -126,11 +126,14 @@ namespace GPUVerify
             Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;

             Debug.Assert(type != null);

 

-            RequiredHavocVariables.Add(type);

-

             IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));

 

-            verifier.uniformityAnalyser.AddNonUniform(impl.Name, HavocTempExpr.Decl.Name);

+            if (!RequiredHavocVariables.Contains(type))

+            {

+                verifier.uniformityAnalyser.AddNonUniform(impl.Name, HavocTempExpr.Decl.Name);

+            }

+

+            RequiredHavocVariables.Add(type);

 

             result.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

                         HavocTempExpr 

diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs
index e65e9197..072688a0 100644
--- a/Source/GPUVerify/UniformityAnalyser.cs
+++ b/Source/GPUVerify/UniformityAnalyser.cs
@@ -181,7 +181,7 @@ namespace GPUVerify
                                 SetNonUniform(callCmd.callee);

                             }

                         }

-                        Implementation CalleeImplementation = GetImplementation(callCmd.callee);

+                        Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

                         for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

                         {

                             if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)

@@ -222,19 +222,6 @@ namespace GPUVerify
 

         }

 

-        private Implementation GetImplementation(string procedureName)

-        {

-            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-            {

-                if (D is Implementation && ((D as Implementation).Name == procedureName))

-                {

-                    return D as Implementation;

-                }

-            }

-            Debug.Assert(false);

-            return null;

-        }

-

         private void SetNonUniform(string procedureName)

         {

             uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>

diff --git a/Source/GPUVerify/VariablesOccurringInExpressionVisitor.cs b/Source/GPUVerify/VariablesOccurringInExpressionVisitor.cs
new file mode 100644
index 00000000..9c46db38
--- /dev/null
+++ b/Source/GPUVerify/VariablesOccurringInExpressionVisitor.cs
@@ -0,0 +1,26 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class VariablesOccurringInExpressionVisitor : StandardVisitor

+    {

+        private HashSet<Variable> variables = new HashSet<Variable>();

+

+        internal IEnumerable<Microsoft.Boogie.Variable> GetVariables()

+        {

+            return variables;

+        }

+

+        public override Variable VisitVariable(Variable node)

+        {

+            variables.Add(node);

+            return base.VisitVariable(node);

+        }

+

+    }

+}