diff options
5 files changed, 153 insertions, 77 deletions
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index da8adc8b..5b0f7e3e 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,6 +108,9 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
+ <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
+ <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
<Compile Include="MayBeGlobalSizeAnalyser.cs" />
<Compile Include="MayBeFlattened2DTidOrGidAnalyser.cs" />
<Compile Include="MayBeGidAnalyser.cs" />
diff --git a/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs new file mode 100644 index 00000000..1bd66785 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs @@ -0,0 +1,22 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ abstract class InvariantGenerationRule
+ {
+ protected GPUVerifier verifier;
+
+ public InvariantGenerationRule(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ }
+
+ public abstract void GenerateCandidates(Implementation Impl, WhileCmd wc);
+ }
+
+}
diff --git a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs new file mode 100644 index 00000000..233b3b45 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs @@ -0,0 +1,54 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ class LoopVariableBoundsInvariantGenerator : InvariantGenerationRule
+ {
+
+ public LoopVariableBoundsInvariantGenerator(GPUVerifier verifier)
+ : base(verifier)
+ {
+
+ }
+
+ public override void GenerateCandidates(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(LoopInvariantGenerator.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)), "loop guard variable non-negative");
+ }
+ }
+ }
+ }
+
+ 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));
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs new file mode 100644 index 00000000..6b2bdc56 --- /dev/null +++ b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs @@ -0,0 +1,61 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+
+namespace GPUVerify.InvariantGenerationRules
+{
+ class PowerOfTwoInvariantGenerator : InvariantGenerationRule
+ {
+
+ public PowerOfTwoInvariantGenerator(GPUVerifier verifier)
+ : base(verifier)
+ {
+
+ }
+
+ public override void GenerateCandidates(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(LoopInvariantGenerator.GetModifiedVariables(wc.Body), basicName))
+ {
+ verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");
+ for (int i = (1 << 15); i > 0; i >>= 1)
+ {
+ verifier.AddCandidateInvariant(wc,
+ GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
+ new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);
+ }
+ verifier.AddCandidateInvariant(wc,
+ Expr.Neq(new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");
+ }
+ }
+ }
+ }
+ }
+
+ private Expr MakePowerOfTwoExpr(Variable v)
+ {
+ Expr result = null;
+ for (int i = 1 << 15; 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);
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs index 6411025d..ead78917 100644 --- a/Source/GPUVerify/LoopInvariantGenerator.cs +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -6,6 +6,8 @@ using Microsoft.Boogie; using Microsoft.Basetypes;
using System.Diagnostics;
+using GPUVerify.InvariantGenerationRules;
+
namespace GPUVerify
{
class LoopInvariantGenerator
@@ -13,10 +15,16 @@ namespace GPUVerify private GPUVerifier verifier;
private Implementation Impl;
+ private List<InvariantGenerationRule> invariantGenerationRules;
+
public LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl)
{
this.verifier = verifier;
this.Impl = Impl;
+
+ invariantGenerationRules = new List<InvariantGenerationRule>();
+ invariantGenerationRules.Add(new PowerOfTwoInvariantGenerator(verifier));
+ invariantGenerationRules.Add(new LoopVariableBoundsInvariantGenerator(verifier));
}
internal void instrument(List<Expr> UserSuppliedInvariants)
@@ -149,11 +157,12 @@ namespace GPUVerify {
WhileCmd wc = bb.ec as WhileCmd;
- AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
-
- AddLoopVariableBoundsCandidateInvariants(Impl, wc);
+ foreach (InvariantGenerationRule r in invariantGenerationRules)
+ {
+ r.GenerateCandidates(Impl, wc);
+ }
- AddPowerOfTwoCandidateInvariants(Impl, wc);
+ AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, wc);
@@ -177,79 +186,6 @@ 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), "pow2 disjunction");
- for (int i = (1 << 15); i > 0; i >>= 1)
- {
- verifier.AddCandidateInvariant(wc,
- GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
- new IdentifierExpr(v.tok, v),
- new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);
- }
- verifier.AddCandidateInvariant(wc,
- Expr.Neq(new IdentifierExpr(v.tok, v),
- new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");
- }
- }
- }
- }
- }
-
- private Expr MakePowerOfTwoExpr(Variable v)
- {
- Expr result = null;
- for (int i = 1 << 15; 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))
- {
- 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)), "loop guard variable non-negative");
- }
- }
- }
- }
-
- 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)
|