diff options
| author |  Peter Collingbourne <peter@pcc.me.uk> | 2012-06-21 21:05:10 +0100 |
|---|---|---|
| committer | Peter Collingbourne <peter@pcc.me.uk> | 2012-06-21 21:05:10 +0100 |
| commit | 1d9b5adb6ef27c26d39c9e1a8a0cb5fcc84467a3 (patch) | |
| tree | 578ccdd29e85eb9c4addc79eb12c47bc9dbbe94a /Source/GPUVerify | |
| parent | b7a2d48041e494ceaa542c468f82c86278b59988 (diff) | |
GPUVerify: construct BV*_AND and BV*_SUB using MakeBVFunctionCall
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 9 |
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);
|