GPUVerify: implement generic stride constraint generation

3 files changed, 142 insertions, 81 deletions

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index cb880767..ddc51368 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -259,10 +259,10 @@ namespace GPUVerify
 

         private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)

         {

-            Expr CTimesLocalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr, 

+            Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr, 

                 new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

 

-            Expr CTimesLocalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

                 new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

 

             Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));

@@ -293,10 +293,10 @@ namespace GPUVerify
 

         private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)

         {

-            Expr CTimesGlobalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,

                 GlobalIdExpr("X", Thread));

 

-            Expr CTimesGlobalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

                 GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

 

             Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 6c874e86..e3d94fcc 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1320,7 +1320,10 @@ namespace GPUVerify
         internal Expr MakeBVSge(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGE", "bvsge", lhs, rhs); }

 

         internal Expr MakeBVAnd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("AND", "bvand", lhs, rhs); }

+        internal Expr MakeBVAdd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("ADD", "bvadd", lhs, rhs); }

         internal Expr MakeBVSub(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("SUB", "bvsub", lhs, rhs); }

+        internal Expr MakeBVMul(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("MUL", "bvmul", lhs, rhs); }

+        internal Expr MakeBVURem(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("UREM", "bvurem", lhs, rhs); }

 

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

         {

@@ -1338,6 +1341,42 @@ namespace GPUVerify
             }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.GetBvType(32))))), new ExprSeq(new Expr[] { lhs, rhs }));

         }

 

+        private static bool IsBVFunctionCall(Expr e, string smtName, out ExprSeq args)

+        {

+            args = null;

+            var ne = e as NAryExpr;

+            if (ne == null)

+                return false;

+

+            var fc = ne.Fun as FunctionCall;

+            if (fc == null)

+                return false;

+

+            string bvBuiltin = QKeyValue.FindStringAttribute(fc.Func.Attributes, "bvbuiltin");

+            if (bvBuiltin == smtName)

+            {

+                args = ne.Args;

+                return true;

+            }

+

+            return false;

+        }

+

+        private static bool IsBVFunctionCall(Expr e, string smtName, out Expr lhs, out Expr rhs)

+        {

+            ExprSeq es;

+            if (IsBVFunctionCall(e, smtName, out es))

+            {

+                lhs = es[0]; rhs = es[1];

+                return true;

+            }

+            lhs = null; rhs = null;

+            return false;

+        }

+

+        internal static bool IsBVAdd(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvadd", out lhs, out rhs); }

+        internal static bool IsBVMul(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvmul", out lhs, out rhs); }

+

         internal Constant GetGroupSize(string dimension)

         {

             Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));

@@ -2299,7 +2338,7 @@ namespace GPUVerify
 

         internal Expr GlobalIdExpr(string dimension)

         {

-            return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",

+            return MakeBVAdd(MakeBVMul(

                             new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))),

                                 new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension)));

         }

@@ -2418,8 +2457,6 @@ namespace GPUVerify
             return IsGivenConstant(maybeGroupId, GetGroupIdConst(dim)) &&

                    IsGivenConstant(maybeGroupSize, GetGroupSizeConst(dim));

         }

-

-

     }

 

 }

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 30ba63b0..5a75fa21 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -131,121 +131,145 @@ namespace GPUVerify
             }

         }

 

-        private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

+        private class StrideConstraint {}

+        private class EqStrideConstraint : StrideConstraint {

+            public EqStrideConstraint(Expr eq) { this.eq = eq; }

+            public Expr eq;

+        }

+        private class ModStrideConstraint : StrideConstraint {

+            public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }

+            public Expr mod, modEq;

+        }

+

+        private StrideConstraint BuildBottomStrideConstraint(Expr e)

         {

-            if (!(e is NAryExpr))

-            {

-                return false;

-            }

+            int width = e.Type.BvBits;

+            return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),

+                                           new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));

+        }

 

-            NAryExpr nary = e as NAryExpr;

+        private bool IsBottomStrideConstraint(StrideConstraint sc)

+        {

+            var msc = sc as ModStrideConstraint;

+            if (msc == null)

+                return false;

 

-            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))

-            {

+            var le = msc.mod as LiteralExpr;

+            if (le == null)

                 return false;

-            }

 

-            {

-                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], true, impl);

-                if (constant != null)

-                {

-                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

-                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, new IdentifierExpr(Token.NoToken,

-                        verifier.MakeThreadId(Token.NoToken, "X")));

+            var bvc = le.Val as BvConst;

+            if (bvc == null)

+                return false;

 

-                    Expr candidateInvariantExpr = Expr.Imp(

-                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

-                            modPow2Expr);

+            return bvc.Value.InInt32 && bvc.Value.ToInt == 1;

+        }

 

-                    AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride local");

-                    return true;

-                }

+        private StrideConstraint BuildAddStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)

+        {

+            if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)

+            {

+                return new EqStrideConstraint(e);

             }

 

-            {

-                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], false, impl);

-                if (constant != null)

-                {

-                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

-                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, verifier.GlobalIdExpr("X"));

+            if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)

+                return BuildAddStrideConstraint(e, rhsc, lhsc);

 

-                    Expr candidateInvariantExpr = Expr.Imp(

-                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

-                            modPow2Expr);

+            if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)

+            {

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsec = (EqStrideConstraint)rhsc;

 

-                    AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride global");

-                    return true;

-                }

+                return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));

             }

 

-            return false;

+            if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint)

+            {

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsmc = (ModStrideConstraint)rhsc;

 

-        }

+                if (lhsmc.mod == rhsmc.mod)

+                    return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));

+            }

 

-        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

-        {

-            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

-            verifier.AddCandidateInvariant(region, candidate, tag);

+            return BuildBottomStrideConstraint(e);

         }

 

-        private Expr IsIdPlusConstantMultiple(Expr arg1, Expr arg2, bool local, Implementation impl)

+        private StrideConstraint BuildMulStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)

         {

+            if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)

             {

-                Expr constant = IsConstantMultiple(arg2);

-                if (constant != null && IsId(arg1, local, impl))

-                {

-                    return constant;

-                }

+                return new EqStrideConstraint(e);

             }

 

+            if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)

+                return BuildMulStrideConstraint(e, rhsc, lhsc);

+

+            if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)

             {

-                Expr constant = IsConstantMultiple(arg1);

-                if (constant != null && IsId(arg2, local, impl))

-                {

-                    return constant;

-                }

-            }

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsec = (EqStrideConstraint)rhsc;

 

-            return null;

+                return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),

+                                               verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));

+            }

 

+            return BuildBottomStrideConstraint(e);

         }

 

-        private Expr IsConstantMultiple(Expr e)

+        private StrideConstraint BuildStrideConstraint(Implementation impl, Expr e)

         {

-            if (!(e is NAryExpr))

-            {

-                return null;

-            }

+            if (e is LiteralExpr || (e is IdentifierExpr && ((IdentifierExpr)e).Decl is Constant))

+                return new EqStrideConstraint(e);

 

-            NAryExpr nary = e as NAryExpr;

+            Expr lhs, rhs;

 

-            if (!(nary.Fun.FunctionName.Equals("BV32_MUL")))

+            if (GPUVerifier.IsBVAdd(e, out lhs, out rhs))

             {

-                return null;

+                var lhsc = BuildStrideConstraint(impl, lhs);

+                var rhsc = BuildStrideConstraint(impl, rhs);

+                return BuildAddStrideConstraint(e, lhsc, rhsc);

             }

 

-            if (IsConstant(nary.Args[0]))

+            if (GPUVerifier.IsBVMul(e, out lhs, out rhs))

             {

-                return nary.Args[0];

+                var lhsc = BuildStrideConstraint(impl, lhs);

+                var rhsc = BuildStrideConstraint(impl, rhs);

+                return BuildMulStrideConstraint(e, lhsc, rhsc);

             }

 

-            if (IsConstant(nary.Args[1]))

-            {

-                return nary.Args[1];

-            }

-

-            return null;

-

+            return BuildBottomStrideConstraint(e);

         }

 

-        private bool IsId(Expr mayBeId, bool local, Implementation impl)

+        private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

         {

-            if (local)

+            bool isConstant;

+            e = verifier.varDefAnalyses[impl].SubstDefinitions(e, impl.Name, out isConstant);

+            if (isConstant)

+                return false;

+

+            var sc = BuildStrideConstraint(impl, e);

+            var msc = sc as ModStrideConstraint;

+            if (msc != null && !IsBottomStrideConstraint(msc))

             {

-                return verifier.IsLocalId(mayBeId, 0, impl);

+                Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

+                Expr modEqExpr = Expr.Eq(verifier.MakeBVURem(offsetExpr, msc.mod), verifier.MakeBVURem(msc.modEq, msc.mod));

+

+                Expr candidateInvariantExpr = Expr.Imp(

+                        new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

+                        modEqExpr);

+

+                AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride");

+                return true;

             }

 

-            return verifier.IsGlobalId(mayBeId, 0, impl);

+            return false;

+        }

+

+        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

+        {

+            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

+            verifier.AddCandidateInvariant(region, candidate, tag);

         }

 

         private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)