GPUVerify: construct BV*_AND and BV*_SUB using MakeBVFunctionCall

2 files changed, 10 insertions, 6 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 5d693fa4..6c874e86 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1300,7 +1300,9 @@ namespace GPUVerify
         private Expr MakeBVFunctionCall(string functionName, string smtName, Microsoft.Boogie.Type resultType, params Expr[] args)

         {

             Function f = GetOrCreateBVFunction(functionName, smtName, resultType, args.Select(a => a.Type).ToArray());

-            return new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));

+            var e = new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));

+            e.Type = resultType;

+            return e;

         }

 

         private Expr MakeBitVectorBinaryBoolean(string suffix, string smtName, Expr lhs, Expr rhs)

@@ -1317,6 +1319,9 @@ namespace GPUVerify
         internal Expr MakeBVSgt(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGT", "bvsgt", lhs, rhs); }

         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 MakeBVSub(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("SUB", "bvsub", lhs, 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[] { 

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 585ca433..30ba63b0 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -379,14 +379,14 @@ namespace GPUVerify
                 {

                     if (DoesNotReferTo(nary.Args[0], v))

                     {

-                        return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",

+                        return verifier.MakeBVSub(

                             InverseOfLinearFunctionOfVariable(nary.Args[1], v, offsetExpr),

                             nary.Args[0]);

                     }

                     else

                     {

                         Debug.Assert(DoesNotReferTo(nary.Args[1], v));

-                        return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",

+                        return verifier.MakeBVSub(

                             InverseOfLinearFunctionOfVariable(nary.Args[0], v, offsetExpr),

                             nary.Args[1]);

                     }

@@ -400,11 +400,10 @@ namespace GPUVerify
 

         private Expr ExprModPow2EqualsId(Expr expr, Expr powerOfTwoExpr, Expr threadIdExpr)

         {

-            Expr Pow2Minus1 = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB", powerOfTwoExpr, 

+            Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr, 

                             new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));

 

-            Expr Pow2Minus1BitAndExpr =

-                GPUVerifier.MakeBitVectorBinaryBitVector("BV32_AND", Pow2Minus1, expr);

+            Expr Pow2Minus1BitAndExpr = verifier.MakeBVAnd(Pow2Minus1, expr);

 

             return Expr.Eq(Pow2Minus1BitAndExpr, threadIdExpr);