Added "may be power of two" analysis.

5 files changed, 296 insertions, 0 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index e775689c..81e61569 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -37,6 +37,7 @@ namespace GPUVerify
         public static bool DoUniformityAnalysis = true;

 

         public static bool ShowMayBeTidAnalysis = false;

+        public static bool ShowMayBePowerOfTwoAnalysis = false;

 

         public static int Parse(string[] args)

         {

@@ -163,6 +164,11 @@ namespace GPUVerify
                     ShowMayBeTidAnalysis = true;

                     break;

 

+                    case "-showMayBePowerOfTwoAnalysis":

+                    case "/showMayBePowerOfTwoAnalysis":

+                    ShowMayBePowerOfTwoAnalysis = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 48935806..070095ea 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -65,6 +65,7 @@ namespace GPUVerify
 

         public UniformityAnalyser uniformityAnalyser;

         public MayBeTidAnalyser mayBeTidAnalyser;

+        public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;

 

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

         {

@@ -309,6 +310,8 @@ namespace GPUVerify
 

             DoMayBeTidAnalysis();

 

+            DoMayBePowerOfTwoAnalysis();

+

             DoArrayControlFlowAnalysis();

 

             if (CommandLineOptions.ShowStages)

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

         }

 

+        private void DoMayBePowerOfTwoAnalysis()

+        {

+            mayBePowerOfTwoAnalyser = new MayBePowerOfTwoAnalyser(this);

+            mayBePowerOfTwoAnalyser.Analyse();

+        }

+

         private void DoMayBeTidAnalysis()

         {

             mayBeTidAnalyser = new MayBeTidAnalyser(this);

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 4b996908..f6353895 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="MayBePowerOfTwoAnalyser.cs" />

     <Compile Include="MayBeTidAnalyser.cs" />

     <Compile Include="StructuredProgramVisitor.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs
index c3851a29..b763852b 100644
--- a/Source/GPUVerify/LoopInvariantGenerator.cs
+++ b/Source/GPUVerify/LoopInvariantGenerator.cs
@@ -150,6 +150,8 @@ namespace GPUVerify
 

                 AddLoopVariableBoundsCandidateInvariants(Impl, wc);

 

+                AddPowerOfTwoCandidateInvariants(Impl, wc);

+

                 verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);

 

                 AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);

@@ -167,6 +169,43 @@ namespace GPUVerify
             }

         }

 

+        private void AddPowerOfTwoCandidateInvariants(Implementation Impl, WhileCmd wc)

+        {

+            foreach (Variable v in Impl.LocVars)

+            {

+                string basicName = GPUVerifier.StripThreadIdentifier(v.Name);

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

+                {

+                    if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))

+                    {

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

+                        {

+                            verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v));

+                            for (int i = (1 << 30); i > 0; i >>= 1)

+                            {

+                                verifier.AddCandidateInvariant(wc, 

+                                    GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",

+                                    new IdentifierExpr(v.tok, v),

+                                    new LiteralExpr(v.tok, BigNum.FromInt(i), 32)));

+                            }

+                        }

+                    }

+                }

+            }

+        }

+

+        private Expr MakePowerOfTwoExpr(Variable v)

+        {

+            Expr result = null;

+            for (int i = 1 << 30; i > 0; i >>= 1)

+            {

+                Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));

+                result = (result == null ? eq : Expr.Or(eq, result));

+            }

+

+            return Expr.Or(Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), result);

+        }

+

         private void AddLoopVariableBoundsCandidateInvariants(Implementation Impl, WhileCmd wc)

         {

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

diff --git a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs
new file mode 100644
index 00000000..a00462c8
--- /dev/null
+++ b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs
@@ -0,0 +1,241 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using Microsoft.Basetypes;

+

+namespace GPUVerify

+{

+    class MayBePowerOfTwoAnalyser

+    {

+        private GPUVerifier verifier;

+

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

+

+        public MayBePowerOfTwoAnalyser(GPUVerifier verifier)

+        {

+            this.verifier = verifier;

+            mayBePowerOfTwoInfo = 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;

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

+

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

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

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

+

+                    foreach (Variable v in Impl.LocVars)

+                    {

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

+                    }

+

+                    foreach (Variable v in Impl.InParams)

+                    {

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

+                    }

+

+                    foreach (Variable v in Impl.OutParams)

+                    {

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

+                    }

+

+                    // Fixpoint not required - this is just syntactic

+                    Analyse(Impl);

+

+                }

+            }

+

+            if (CommandLineOptions.ShowMayBePowerOfTwoAnalysis)

+            {

+                dump();

+            }

+        }

+

+        private void SetNotPowerOfTwo(string p, string v)

+        {

+            mayBePowerOfTwoInfo[p][v] = false;

+        }

+

+        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 assign = c as AssignCmd;

+                    assign = c as AssignCmd;

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

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

+

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

+                    {

+                        Variable v = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;

+                        if (mayBePowerOfTwoInfo[impl.Name].ContainsKey(v.Name))

+                        {

+                            if (isPowerOfTwoOperation(v, assign.Rhss[0]))

+                            {

+                                mayBePowerOfTwoInfo[impl.Name][v.Name] = true;

+                            }

+                        }

+                    }

+                }

+            }

+

+            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 bool isPowerOfTwoOperation(Variable v, Expr expr)

+        {

+            if (!(

+                v.TypedIdent.Type.Equals(

+                Microsoft.Boogie.Type.GetBvType(8))

+                ||

+                v.TypedIdent.Type.Equals(

+                Microsoft.Boogie.Type.GetBvType(16))

+                ||

+                v.TypedIdent.Type.Equals(

+                Microsoft.Boogie.Type.GetBvType(32))

+                ))

+            {

+                return false;

+            }

+

+            Microsoft.Boogie.Type bvType = v.TypedIdent.Type as BvType;

+

+            if (!(expr is NAryExpr))

+            {

+                return false;

+            }

+

+            NAryExpr nary = expr as NAryExpr;

+

+            string bvPrefix = "BV" + bvType.BvBits + "_";

+

+            if (nary.Fun.FunctionName.Equals(bvPrefix + "MUL"))

+            {

+                Debug.Assert(nary.Args.Length == 2);

+                return

+                   (

+                    (IsVariable(nary.Args[0], v) || IsVariable(nary.Args[1], v)) &&

+                    (IsConstant(nary.Args[0], 2) || IsConstant(nary.Args[1], 2))

+                    );

+            }

+

+            if (nary.Fun.FunctionName.Equals(bvPrefix + "DIV"))

+            {

+                Debug.Assert(nary.Args.Length == 2);

+                return

+                   (

+                    IsVariable(nary.Args[0], v) && IsConstant(nary.Args[1], 2)

+                    );

+            }

+

+            if (nary.Fun.FunctionName.Equals(bvPrefix + "SHL"))

+            {

+                return

+                   (

+                    IsVariable(nary.Args[0], v) && IsConstant(nary.Args[1], 1)

+                    );

+            }

+

+            if (nary.Fun.FunctionName.Equals(bvPrefix + "ASHR"))

+            {

+                return

+                   (

+                    IsVariable(nary.Args[0], v) && IsConstant(nary.Args[1], 1)

+                    );

+            }

+

+            return false;

+        }

+

+        private bool IsConstant(Expr expr, int x)

+        {

+            if (!(expr is LiteralExpr))

+            {

+                return false;

+            }

+

+            LiteralExpr lit = expr as LiteralExpr;

+

+            if (!(lit.Val is BvConst))

+            {

+                return false;

+            }

+

+            return (lit.Val as BvConst).Value.ToInt == x;

+        }

+

+        private bool IsVariable(Expr expr, Variable v)

+        {

+            return expr is IdentifierExpr && ((expr as IdentifierExpr).Decl.Name.Equals(v.Name));

+        }

+

+        private void dump()

+        {

+            foreach (string p in mayBePowerOfTwoInfo.Keys)

+            {

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

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

+                {

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

+                        (mayBePowerOfTwoInfo[p][v] ? "may be power of two" : "likely not power of two"));

+                }

+            }

+

+        }

+

+

+        internal bool MayBePowerOfTwo(string p, string v)

+        {

+            if (!mayBePowerOfTwoInfo.ContainsKey(p))

+            {

+                return false;

+            }

+

+            if (!mayBePowerOfTwoInfo[p].ContainsKey(v))

+            {

+                return false;

+            }

+

+            return mayBePowerOfTwoInfo[p][v];

+        }

+    }

+}