diff options
| author |  Peter Collingbourne <peter@pcc.me.uk> | 2012-06-07 21:02:03 +0100 |
|---|---|---|
| committer | Peter Collingbourne <peter@pcc.me.uk> | 2012-06-07 21:02:03 +0100 |
| commit | 281e96f18dcc95347dd5040fcc7f835975420398 (patch) | |
| tree | 1bc565a574e74e7af2862cd97ed370b8ab76457d /Source/GPUVerify | |
| parent | 42905d3eb4157d81c6176211dd6567b24484be8e (diff) | |
GPUVerify: refactor candidate invariant generators and analyses to use regions
The main goal of this change is to make the candidate invariant
generation code and various analyses capable of handling both
structured and unstructured programs. This is achieved using a
high level abstraction of "regions" -- a region may either be a
"root region" representing the entire implementation, or a natural
loop within that implementation. Note that this is a subset to the
term's meaning in the context of compilers, in which regions are also
used for conditional control flow. Each region consists of a set of
commands and a set of child regions.
This change also has the side effect of eliminating a large amount of
boilerplate code -- its net effect is to reduce the number of lines
of code by 88.
Diffstat (limited to 'Source/GPUVerify')
19 files changed, 413 insertions, 501 deletions
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 7b78f0f1..cdedfef0 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -195,16 +195,16 @@ namespace GPUVerify }
- protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc, expr, "accessed offset is global id");
+ verifier.AddCandidateInvariant(region, expr, "accessed offset is global id");
}
- protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc, expr, "accessed offset is local id");
+ verifier.AddCandidateInvariant(region, expr, "accessed offset is local id");
}
private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
@@ -247,10 +247,10 @@ namespace GPUVerify new IdentifierExpr(Token.NoToken, verifier.GetGroupSize(dimension)));
}
- protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc, expr, "accessed offset is flattened 2D local id");
+ verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D local id");
}
private Expr AccessedOffsetIsThreadFlattened2DLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
@@ -271,10 +271,10 @@ namespace GPUVerify return expr;
}
- protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
+ protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
{
Expr expr = AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc, expr, "accessed offset is flattened 2D global id");
+ verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D global id");
}
private Expr AccessedOffsetIsThreadFlattened2DGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)
@@ -295,10 +295,10 @@ namespace GPUVerify return expr;
}
- protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
+ protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
{
Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
}
@@ -329,10 +329,10 @@ namespace GPUVerify return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite)));
}
- protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)
+ protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
{
Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 090ddd51..27909c52 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -2158,13 +2158,13 @@ namespace GPUVerify return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);
}
- internal void AddCandidateInvariant(WhileCmd wc, Expr e, string tag)
+ internal void AddCandidateInvariant(IRegion region, Expr e, string tag)
{
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(wc.tok);
- IdentifierExpr ExistentialBoolean = new IdentifierExpr(wc.tok, ExistentialBooleanConstant);
- PredicateCmd invariant = new AssertCmd(wc.tok, Expr.Imp(ExistentialBoolean, e));
+ Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);
+ IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
+ PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);
- wc.Invariants.Add(invariant);
+ region.AddInvariant(invariant);
Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
@@ -2182,21 +2182,9 @@ namespace GPUVerify }
- internal bool ContainsBarrierCall(StmtList stmtList)
+ internal bool ContainsBarrierCall(IRegion loop)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- if (ContainsBarrierCall(bb))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool ContainsBarrierCall(BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in loop.Cmds())
{
if (c is CallCmd && ((c as CallCmd).Proc == BarrierProcedure))
{
@@ -2204,21 +2192,6 @@ namespace GPUVerify }
}
- if (bb.ec is WhileCmd)
- {
- return ContainsBarrierCall((bb.ec as WhileCmd).Body);
- }
-
- if (bb.ec is IfCmd)
- {
- Debug.Assert((bb.ec as IfCmd).elseIf == null);
- if (ContainsBarrierCall((bb.ec as IfCmd).thn))
- {
- return true;
- }
- return (bb.ec as IfCmd).elseBlock != null && ContainsBarrierCall((bb.ec as IfCmd).elseBlock);
- }
-
return false;
}
@@ -2248,6 +2221,14 @@ namespace GPUVerify new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))),
new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension)));
}
+
+ internal IRegion RootRegion(Implementation Impl)
+ {
+ if (CommandLineOptions.Unstructured)
+ return new UnstructuredRegion(Program, Impl);
+ else
+ return new StructuredRegion(Impl);
+ }
}
class ThreadIdentifierStripper : StandardVisitor
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 27b9abe5..376d67b5 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -109,6 +109,8 @@ <Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
<Compile Include="BlockPredicator.cs" />
+ <Compile Include="UnstructuredRegion.cs" />
+ <Compile Include="IRegion.cs" />
<Compile Include="GraphAlgorithms.cs" />
<Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
@@ -145,6 +147,7 @@ <Compile Include="UniformityAnalyser.cs" />
<Compile Include="VariableDualiser.cs" />
<Compile Include="VariablesOccurringInExpressionVisitor.cs" />
+ <Compile Include="StructuredRegion.cs" />
<Compile Include="WriteCollector.cs" />
</ItemGroup>
<ItemGroup>
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs index 65d2cc1b..4845a0c3 100644 --- a/Source/GPUVerify/IRaceInstrumenter.cs +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -8,7 +8,7 @@ namespace GPUVerify {
interface IRaceInstrumenter
{
- void AddRaceCheckingCandidateInvariants(Implementation impl, WhileCmd wc);
+ void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region);
void AddKernelPrecondition();
// Summary:
diff --git a/Source/GPUVerify/IRegion.cs b/Source/GPUVerify/IRegion.cs new file mode 100644 index 00000000..26adaa4e --- /dev/null +++ b/Source/GPUVerify/IRegion.cs @@ -0,0 +1,17 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+
+interface IRegion {
+ IEnumerable<Cmd> Cmds();
+ IEnumerable<object> CmdsChildRegions();
+ IEnumerable<IRegion> SubRegions();
+ Expr Guard();
+ void AddInvariant(PredicateCmd pc);
+}
+
+}
diff --git a/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs index 1bd66785..cb2a9f41 100644 --- a/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs +++ b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs @@ -16,7 +16,7 @@ namespace GPUVerify.InvariantGenerationRules this.verifier = verifier;
}
- public abstract void GenerateCandidates(Implementation Impl, WhileCmd wc);
+ public abstract void GenerateCandidates(Implementation Impl, IRegion region);
}
}
diff --git a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs index af5f8d71..f73bddb6 100644 --- a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs +++ b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs @@ -17,15 +17,15 @@ namespace GPUVerify.InvariantGenerationRules }
- public override void GenerateCandidates(Implementation Impl, WhileCmd wc)
+ public override void GenerateCandidates(Implementation Impl, IRegion region)
{
- if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name, region.Guard()))
{
VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();
- visitor.VisitExpr(wc.Guard);
+ visitor.VisitExpr(region.Guard());
foreach (Variable v in visitor.GetVariables())
{
- if (!verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), v.Name))
+ if (!verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(region), v.Name))
{
continue;
}
@@ -34,7 +34,7 @@ namespace GPUVerify.InvariantGenerationRules {
int BVWidth = (v.TypedIdent.Type as BvType).Bits;
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
verifier.MakeBVSge(
new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");
diff --git a/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs index 6b2bdc56..8b24bb0a 100644 --- a/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs +++ b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs @@ -17,7 +17,7 @@ namespace GPUVerify.InvariantGenerationRules }
- public override void GenerateCandidates(Implementation Impl, WhileCmd wc)
+ public override void GenerateCandidates(Implementation Impl, IRegion region)
{
foreach (Variable v in Impl.LocVars)
{
@@ -26,17 +26,17 @@ namespace GPUVerify.InvariantGenerationRules {
if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))
{
- if (verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), basicName))
+ if (verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(region), basicName))
{
- verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");
+ verifier.AddCandidateInvariant(region, MakePowerOfTwoExpr(v), "pow2 disjunction");
for (int i = (1 << 15); i > 0; i >>= 1)
{
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);
}
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
Expr.Neq(new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");
}
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs index ead78917..936d1c44 100644 --- a/Source/GPUVerify/LoopInvariantGenerator.cs +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -43,153 +43,131 @@ namespace GPUVerify LocalVars.Add(v);
}
- AddCandidateInvariants(Impl.StructuredStmts, LocalVars, UserSuppliedInvariants, Impl);
+ AddCandidateInvariants(verifier.RootRegion(Impl), LocalVars, UserSuppliedInvariants, Impl);
}
- private void AddEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
+ private void AddEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v)
{
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
Expr.Eq(
- new IdentifierExpr(wc.tok, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(wc.tok, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))
), "equality");
}
- private void AddPredicatedEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
+ private void AddPredicatedEqualityCandidateInvariant(IRegion region, string LoopPredicate, Variable v)
{
- verifier.AddCandidateInvariant(wc, Expr.Imp(
+ verifier.AddCandidateInvariant(region, Expr.Imp(
Expr.And(
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
+ new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
+ new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
),
Expr.Eq(
- new IdentifierExpr(wc.tok, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(wc.tok, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(1, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Token.NoToken, new VariableDualiser(2, verifier.uniformityAnalyser, Impl.Name).VisitVariable(v.Clone() as Variable))
)), "predicated equality");
}
- private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, WhileCmd wc)
+ private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, IRegion region)
{
if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)
{
- if (!verifier.ContainsBarrierCall(wc.Body))
+ if (!verifier.ContainsBarrierCall(region))
{
return;
}
}
- if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))
+ Expr guard = region.Guard();
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name, guard))
{
return;
}
- Debug.Assert(wc.Guard is NAryExpr);
- Debug.Assert((wc.Guard as NAryExpr).Args.Length == 2);
- Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);
- string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;
-
- LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));
+ if (guard is NAryExpr &&
+ (guard as NAryExpr).Args.Length == 2 &&
+ (guard as NAryExpr).Args[0] is IdentifierExpr)
+ {
+ string LoopPredicate = ((guard as NAryExpr).Args[0] as IdentifierExpr).Name;
- verifier.AddCandidateInvariant(wc, Expr.Eq(
- // Int type used here, but it doesn't matter as we will print and then re-parse the program
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
- new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
- ), "loop predicate equality");
+ LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));
- foreach (Variable v in LocalVars)
- {
+ verifier.AddCandidateInvariant(region, Expr.Eq(
+ // Int type used here, but it doesn't matter as we will print and then re-parse the program
+ new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$1", Microsoft.Boogie.Type.Int))),
+ new IdentifierExpr(Token.NoToken, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, LoopPredicate + "$2", Microsoft.Boogie.Type.Int)))
+ ), "loop predicate equality");
- if (verifier.uniformityAnalyser.IsUniform(Impl.Name, v.Name))
+ foreach (Variable v in LocalVars)
{
- continue;
- }
- string lv = GPUVerifier.StripThreadIdentifier(v.Name);
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name, v.Name))
+ {
+ continue;
+ }
- if (GPUVerifier.IsPredicateOrTemp(lv))
- {
- continue;
- }
+ string lv = GPUVerifier.StripThreadIdentifier(v.Name);
- if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)
- {
- if (!verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body),
- GPUVerifier.StripThreadIdentifier(v.Name)))
+ if (GPUVerifier.IsPredicateOrTemp(lv))
{
continue;
}
- }
- AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+ if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)
+ {
+ if (!verifier.ContainsNamedVariable(GetModifiedVariables(region),
+ GPUVerifier.StripThreadIdentifier(v.Name)))
+ {
+ continue;
+ }
+ }
+
+ AddEqualityCandidateInvariant(region, LoopPredicate, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lv, Microsoft.Boogie.Type.Int)));
- if (Impl != verifier.KernelImplementation)
- {
- AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+ if (Impl != verifier.KernelImplementation)
+ {
+ AddPredicatedEqualityCandidateInvariant(region, LoopPredicate, new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, lv, Microsoft.Boogie.Type.Int)));
+ }
}
- }
- if (CommandLineOptions.ArrayEqualities)
- {
- foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())
+ if (CommandLineOptions.ArrayEqualities)
{
- if (!verifier.ArrayModelledAdversarially(v))
+ foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())
{
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ AddEqualityCandidateInvariant(region, LoopPredicate, v);
+ }
}
}
}
}
- private void AddCandidateInvariants(StmtList stmtList, HashSet<Variable> LocalVars, List<Expr> UserSuppliedInvariants, Implementation Impl)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- AddCandidateInvariants(bb, LocalVars, UserSuppliedInvariants, Impl);
- }
- }
-
- private void AddCandidateInvariants(BigBlock bb, HashSet<Variable> LocalVars, List<Expr> UserSuppliedInvariants, Implementation Impl)
+ private void AddCandidateInvariants(IRegion region, HashSet<Variable> LocalVars, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
- if (bb.ec is WhileCmd)
+ foreach (IRegion subregion in region.SubRegions())
{
- WhileCmd wc = bb.ec as WhileCmd;
-
foreach (InvariantGenerationRule r in invariantGenerationRules)
{
- r.GenerateCandidates(Impl, wc);
+ r.GenerateCandidates(Impl, subregion);
}
- AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
-
- verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, wc);
+ AddBarrierDivergenceCandidates(LocalVars, Impl, subregion);
- AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);
-
- AddCandidateInvariants(wc.Body, LocalVars, UserSuppliedInvariants, Impl);
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd ifCmd = bb.ec as IfCmd;
- AddCandidateInvariants(ifCmd.thn, LocalVars, UserSuppliedInvariants, Impl);
- if (ifCmd.elseBlock != null)
- {
- AddCandidateInvariants(ifCmd.elseBlock, LocalVars, UserSuppliedInvariants, Impl);
- }
+ verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, subregion);
- }
- else
- {
- Debug.Assert(bb.ec == null);
+ AddUserSuppliedInvariants(subregion, UserSuppliedInvariants, Impl);
}
}
- private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)
+ private void AddUserSuppliedInvariants(IRegion region, List<Expr> UserSuppliedInvariants, Implementation Impl)
{
foreach (Expr e in UserSuppliedInvariants)
{
+ /*
wc.Invariants.Add(new AssertCmd(wc.tok, e));
bool OK = verifier.ProgramIsOK(Impl);
wc.Invariants.RemoveAt(wc.Invariants.Count - 1);
@@ -197,30 +175,16 @@ namespace GPUVerify {
verifier.AddCandidateInvariant(wc, e, "user supplied");
}
+ */
+ verifier.AddCandidateInvariant(region, e, "user supplied");
}
}
- internal static HashSet<Variable> GetModifiedVariables(StmtList stmtList)
- {
- HashSet<Variable> result = new HashSet<Variable>();
-
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- HashSet<Variable> resultForBlock = GetModifiedVariables(bb);
- foreach (Variable v in resultForBlock)
- {
- result.Add(v);
- }
- }
-
- return result;
- }
-
- private static HashSet<Variable> GetModifiedVariables(BigBlock bb)
+ internal static HashSet<Variable> GetModifiedVariables(IRegion region)
{
HashSet<Variable> result = new HashSet<Variable>();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
VariableSeq vars = new VariableSeq();
c.AddAssignedVariables(vars);
@@ -230,34 +194,6 @@ namespace GPUVerify }
}
- if (bb.ec is WhileCmd)
- {
- HashSet<Variable> modifiedByLoop = GetModifiedVariables((bb.ec as WhileCmd).Body);
- foreach (Variable v in modifiedByLoop)
- {
- result.Add(v);
- }
- }
- else if (bb.ec is IfCmd)
- {
- HashSet<Variable> modifiedByThen = GetModifiedVariables((bb.ec as IfCmd).thn);
- foreach (Variable v in modifiedByThen)
- {
- result.Add(v);
- }
-
- if ((bb.ec as IfCmd).elseBlock != null)
- {
- HashSet<Variable> modifiedByElse = GetModifiedVariables((bb.ec as IfCmd).elseBlock);
- foreach (Variable v in modifiedByElse)
- {
- result.Add(v);
- }
- }
-
- Debug.Assert((bb.ec as IfCmd).elseIf == null);
- }
-
return result;
}
diff --git a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs index 3d65ec61..ea9b85fa 100644 --- a/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs +++ b/Source/GPUVerify/MayBeFlattened2DTidOrGidAnalyser.cs @@ -92,20 +92,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -129,23 +121,6 @@ namespace GPUVerify }
}
}
-
- 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 void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs index 969e8935..f7d8c973 100644 --- a/Source/GPUVerify/MayBeGidAnalyser.cs +++ b/Source/GPUVerify/MayBeGidAnalyser.cs @@ -92,20 +92,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -129,23 +121,6 @@ namespace GPUVerify }
}
}
-
- 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 void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs index 579f6805..98e71179 100644 --- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs +++ b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs @@ -92,20 +92,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -129,23 +121,6 @@ namespace GPUVerify }
}
}
-
- 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 void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs index a8563dfa..a57f35ee 100644 --- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs +++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs @@ -79,21 +79,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -135,23 +126,6 @@ namespace GPUVerify }
}
}
-
- 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 string ConvertToString(Expr constantIncrement)
diff --git a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs index 506add7c..c0f00dda 100644 --- a/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs +++ b/Source/GPUVerify/MayBePowerOfTwoAnalyser.cs @@ -67,20 +67,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -102,23 +94,6 @@ namespace GPUVerify }
}
}
-
- 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)
diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs index 53efbea8..d445d422 100644 --- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs +++ b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs @@ -127,20 +127,12 @@ namespace GPUVerify private void Analyse(Implementation Impl)
{
- Analyse(Impl, Impl.StructuredStmts);
+ Analyse(Impl, verifier.RootRegion(Impl));
}
- private void Analyse(Implementation impl, StmtList stmtList)
+ private void Analyse(Implementation impl, IRegion region)
{
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb);
- }
- }
-
- private void Analyse(Implementation impl, BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -164,23 +156,6 @@ namespace GPUVerify }
}
}
-
- 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 void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs index 73f038fb..d38c57af 100644 --- a/Source/GPUVerify/NullRaceInstrumenter.cs +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -9,7 +9,7 @@ namespace GPUVerify class NullRaceInstrumenter : IRaceInstrumenter
{
- public void AddRaceCheckingCandidateInvariants(Implementation impl, Microsoft.Boogie.WhileCmd wc)
+ public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
{
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index a821af15..ad0fd9f6 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -48,7 +48,7 @@ namespace GPUVerify protected abstract void AddRequiresNoPendingAccess(Variable v);
- private void AddNoReadOrWriteCandidateInvariants(WhileCmd wc, Variable v)
+ private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v)
{
// Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the
// loop then there is no point adding an invariant
@@ -63,18 +63,18 @@ namespace GPUVerify //
// The same reasoning applies for WRITE
- if (verifier.ContainsBarrierCall(wc.Body))
+ if (verifier.ContainsBarrierCall(region))
{
if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))
+ LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))
{
- AddNoReadOrWriteCandidateInvariant(wc, v, "READ");
+ AddNoReadOrWriteCandidateInvariant(region, v, "READ");
}
if (verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))
+ LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))
{
- AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE");
+ AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");
}
}
}
@@ -91,47 +91,47 @@ namespace GPUVerify AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
}
- private void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)
+ private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
{
Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
- verifier.AddCandidateInvariant(wc, candidate, "no " + ReadOrWrite.ToLower());
+ verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());
}
- public void AddRaceCheckingCandidateInvariants(Implementation impl, WhileCmd wc)
+ public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
{
foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
- AddNoReadOrWriteCandidateInvariants(wc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, wc, v, "READ");
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, wc, v, "WRITE");
- AddGroupStrideAccessCandidateInvariants(impl, wc, v, "READ");
- AddGroupStrideAccessCandidateInvariants(impl, wc, v, "WRITE");
+ AddNoReadOrWriteCandidateInvariants(region, v);
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");
+ AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");
+ AddGroupStrideAccessCandidateInvariants(impl, region, v, "READ");
+ AddGroupStrideAccessCandidateInvariants(impl, region, v, "WRITE");
}
}
- private void AddGroupStrideAccessCandidateInvariants(Implementation impl, WhileCmd wc, Variable v, string accessKind)
+ private void AddGroupStrideAccessCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessKind)
{
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessKind))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessKind))
{
- if (TryGenerateCandidateForDirectStridedAccess(impl, wc, v, e, accessKind))
+ if (TryGenerateCandidateForDirectStridedAccess(impl, region, v, e, accessKind))
{
continue;
}
- if (!TryGenerateCandidateForReducedStrengthStrideVariable(impl, wc, v, e, accessKind))
+ if (!TryGenerateCandidateForReducedStrengthStrideVariable(impl, region, v, e, accessKind))
{
if (e is IdentifierExpr)
{
- foreach(Expr f in GetExpressionsFromWhichVariableIsAssignedInLoop(wc.Body, (e as IdentifierExpr).Decl))
+ foreach(Expr f in GetExpressionsFromWhichVariableIsAssignedInLoop(region, (e as IdentifierExpr).Decl))
{
- TryGenerateCandidateForReducedStrengthStrideVariable(impl, wc, v, f, accessKind);
+ TryGenerateCandidateForReducedStrengthStrideVariable(impl, region, v, f, accessKind);
}
}
}
}
}
- private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind)
+ private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)
{
if (!(e is NAryExpr))
{
@@ -157,7 +157,7 @@ namespace GPUVerify new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
modPow2Expr);
- AddAccessRelatedCandidateInvariant(wc, accessKind, candidateInvariantExpr, impl.Name, "direct stride local");
+ AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride local");
return true;
}
}
@@ -173,7 +173,7 @@ namespace GPUVerify new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
modPow2Expr);
- AddAccessRelatedCandidateInvariant(wc, accessKind, candidateInvariantExpr, impl.Name, "direct stride global");
+ AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride global");
return true;
}
}
@@ -182,10 +182,10 @@ namespace GPUVerify }
- private void AddAccessRelatedCandidateInvariant(WhileCmd wc, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
+ 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(wc, candidate, tag);
+ verifier.AddCandidateInvariant(region, candidate, tag);
}
private Expr IsIdPlusConstantMultiple(Expr arg1, Expr arg2, bool local, Implementation impl)
@@ -248,20 +248,20 @@ namespace GPUVerify return verifier.mayBeGidAnalyser.MayBe("x", impl.Name, mayBeId);
}
- private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind)
+ private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)
{
foreach (string w in
verifier.mayBeTidPlusConstantAnalyser.GetMayBeIdPlusConstantVars(impl.Name))
{
if (!verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), w))
+ LoopInvariantGenerator.GetModifiedVariables(region), w))
{
continue;
}
// Check also live
- if (GenerateModIdInvariants(impl, wc, v, e, accessKind, w, verifier.mayBeTidPlusConstantAnalyser))
+ if (GenerateModIdInvariants(impl, region, v, e, accessKind, w, verifier.mayBeTidPlusConstantAnalyser))
{
return true;
}
@@ -272,14 +272,14 @@ namespace GPUVerify verifier.mayBeGidPlusConstantAnalyser.GetMayBeIdPlusConstantVars(impl.Name))
{
if (!verifier.ContainsNamedVariable(
- LoopInvariantGenerator.GetModifiedVariables(wc.Body), w))
+ LoopInvariantGenerator.GetModifiedVariables(region), w))
{
continue;
}
// Check also live
- if (GenerateModIdInvariants(impl, wc, v, e, accessKind, w, verifier.mayBeGidPlusConstantAnalyser))
+ if (GenerateModIdInvariants(impl, region, v, e, accessKind, w, verifier.mayBeGidPlusConstantAnalyser))
{
return true;
}
@@ -290,7 +290,7 @@ namespace GPUVerify return false;
}
- private bool GenerateModIdInvariants(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind,
+ private bool GenerateModIdInvariants(Implementation impl, IRegion region, Variable v, Expr e, string accessKind,
string w, MayBeIdPlusConstantAnalyser mayBeIdPlusConstantAnalyser)
{
if (!IsLinearFunctionOfVariable(e, w))
@@ -300,17 +300,17 @@ namespace GPUVerify Debug.Assert(!verifier.uniformityAnalyser.IsUniform(impl.Name, w));
- Variable wVariable = new LocalVariable(wc.tok, new TypedIdent(wc.tok, w,
+ Variable wVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, w,
Microsoft.Boogie.Type.GetBvType(32)));
Expr indexModPow2EqualsId = ExprModPow2EqualsId(
- new IdentifierExpr(wc.tok, wVariable),
+ new IdentifierExpr(Token.NoToken, wVariable),
mayBeIdPlusConstantAnalyser.GetIncrement(impl.Name, w), mayBeIdPlusConstantAnalyser.MakeIdExpr());
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsId.Clone() as Expr),
"is " + mayBeIdPlusConstantAnalyser.idKind() + " plus constant multiple");
- verifier.AddCandidateInvariant(wc,
+ verifier.AddCandidateInvariant(region,
new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsId.Clone() as Expr),
"is " + mayBeIdPlusConstantAnalyser.idKind() + " plus constant multiple");
@@ -325,29 +325,16 @@ namespace GPUVerify new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
invertedOffsetModPow2EqualsId);
- AddAccessRelatedCandidateInvariant(wc, accessKind, candidateInvariantExpr, impl.Name, "accessed offset is "
+ AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "accessed offset is "
+ mayBeIdPlusConstantAnalyser.idKind() + " plus constant multiple");
return true;
}
- private HashSet<Expr> GetExpressionsFromWhichVariableIsAssignedInLoop(StmtList stmts, Variable variable)
+ private HashSet<Expr> GetExpressionsFromWhichVariableIsAssignedInLoop(IRegion region, Variable variable)
{
HashSet<Expr> result = new HashSet<Expr>();
- foreach (BigBlock bb in stmts.BigBlocks)
- {
- foreach (Expr e in GetExpressionsFromWhichVariableIsAssignedInLoop(bb, variable))
- {
- result.Add(e);
- }
- }
- return result;
- }
-
- private HashSet<Expr> GetExpressionsFromWhichVariableIsAssignedInLoop(BigBlock bb, Variable variable)
- {
- HashSet<Expr> result = new HashSet<Expr>();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is AssignCmd)
{
@@ -370,34 +357,6 @@ namespace GPUVerify }
}
- if (bb.ec is WhileCmd)
- {
- foreach (Expr e in GetExpressionsFromWhichVariableIsAssignedInLoop((bb.ec as WhileCmd).Body, variable))
- {
- result.Add(e);
- }
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd ifCmd = bb.ec as IfCmd;
-
- foreach (Expr e in GetExpressionsFromWhichVariableIsAssignedInLoop(ifCmd.thn, variable))
- {
- result.Add(e);
- }
-
- Debug.Assert(ifCmd.elseIf == null);
-
- if (ifCmd.elseBlock != null)
- {
- foreach (Expr e in GetExpressionsFromWhichVariableIsAssignedInLoop(ifCmd.elseBlock, variable))
- {
- result.Add(e);
- }
- }
-
- }
-
return result;
}
@@ -491,66 +450,66 @@ namespace GPUVerify return !visitor.found;
}
- private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, WhileCmd wc, Variable v, string accessType)
+ private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
{
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
{
- AddAccessedOffsetIsThreadLocalIdCandidateInvariant(wc, v, accessType);
+ AddAccessedOffsetIsThreadLocalIdCandidateInvariant(region, v, accessType);
// No point adding it multiple times
break;
}
}
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if (verifier.mayBeGidAnalyser.MayBe("x", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
{
- AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(wc, v, accessType);
+ AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(region, v, accessType);
// No point adding it multiple times
break;
}
}
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("local", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
{
- AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(wc, v, accessType);
+ AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(region, v, accessType);
// No point adding it multiple times
break;
}
}
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("global", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))
{
- AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(wc, v, accessType);
+ AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(region, v, accessType);
// No point adding it multiple times
break;
}
}
- KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(wc.Guard);
+ KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
if (iLessThanC.Key != null)
{
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if(HasFormIPlusLocalIdTimesC(e, iLessThanC, impl))
{
- AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(wc, v, iLessThanC.Value, accessType);
+ AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);
break;
}
}
- foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessType))
+ foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
{
if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl))
{
- AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(wc, v, iLessThanC.Value, accessType);
+ AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);
break;
}
}
@@ -721,17 +680,17 @@ namespace GPUVerify AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
}
- protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
- protected abstract void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
- protected abstract void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
- protected abstract void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);
- protected abstract void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
- protected abstract void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite);
+ protected abstract void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);
protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread);
@@ -1049,24 +1008,11 @@ namespace GPUVerify protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);
- private HashSet<Expr> GetOffsetsAccessed(StmtList stmts, Variable v, string AccessType)
- {
- HashSet<Expr> result = new HashSet<Expr> ();
- foreach (BigBlock bb in stmts.BigBlocks)
- {
- foreach (Expr e in GetOffsetsAccessed(bb, v, AccessType))
- {
- result.Add(e);
- }
- }
- return result;
- }
-
- private HashSet<Expr> GetOffsetsAccessed(BigBlock bb, Variable v, string AccessType)
+ private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType)
{
HashSet<Expr> result = new HashSet<Expr>();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in region.Cmds())
{
if (c is CallCmd)
{
@@ -1097,36 +1043,6 @@ namespace GPUVerify }
- if (bb.ec is WhileCmd)
- {
- HashSet<Expr> bodyResult = GetOffsetsAccessed((bb.ec as WhileCmd).Body, v, AccessType);
- foreach (Expr e in bodyResult)
- {
- result.Add(e);
- }
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd ifCmd = bb.ec as IfCmd;
-
- HashSet<Expr> thenResult = GetOffsetsAccessed(ifCmd.thn, v, AccessType);
- foreach (Expr e in thenResult)
- {
- result.Add(e);
- }
-
- Debug.Assert(ifCmd.elseIf == null);
-
- if(ifCmd.elseBlock != null)
- {
- HashSet<Expr> elseResult = GetOffsetsAccessed(ifCmd.elseBlock, v, AccessType);
- foreach (Expr e in elseResult)
- {
- result.Add(e);
- }
- }
- }
-
return result;
}
diff --git a/Source/GPUVerify/StructuredRegion.cs b/Source/GPUVerify/StructuredRegion.cs new file mode 100644 index 00000000..ff964c83 --- /dev/null +++ b/Source/GPUVerify/StructuredRegion.cs @@ -0,0 +1,117 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+
+class StructuredRegion : IRegion {
+ WhileCmd cmd;
+ StmtList stmts;
+
+ public StructuredRegion(WhileCmd cmd) {
+ this.cmd = cmd;
+ }
+
+ public StructuredRegion(StmtList stmts) {
+ this.stmts = stmts;
+ }
+
+ public StructuredRegion(Implementation impl) {
+ this.stmts = impl.StructuredStmts;
+ }
+
+ private IEnumerable<Cmd> Cmds(StmtList stmts) {
+ foreach (var bb in stmts.BigBlocks) {
+ foreach (Cmd c in bb.simpleCmds)
+ yield return c;
+
+ if (bb.ec is IfCmd) {
+ var ic = (IfCmd)bb.ec;
+ foreach (var c in Cmds(ic.thn))
+ yield return c;
+
+ if (ic.elseBlock != null)
+ foreach (var c in Cmds(ic.elseBlock))
+ yield return c;
+ } else if (bb.ec is WhileCmd) {
+ var wc = (WhileCmd)bb.ec;
+ foreach (var c in Cmds(wc.Body))
+ yield return c;
+ }
+ }
+ }
+
+ private IEnumerable<object> CmdsChildRegions(StmtList stmts) {
+ foreach (var bb in stmts.BigBlocks) {
+ foreach (Cmd c in bb.simpleCmds)
+ yield return c;
+
+ if (bb.ec is IfCmd) {
+ var ic = (IfCmd)bb.ec;
+ foreach (var c in Cmds(ic.thn))
+ yield return c;
+
+ if (ic.elseBlock != null)
+ foreach (var c in Cmds(ic.elseBlock))
+ yield return c;
+ } else if (bb.ec is WhileCmd) {
+ var wc = (WhileCmd)bb.ec;
+ yield return new StructuredRegion(wc);
+ }
+ }
+ }
+
+ private IEnumerable<IRegion> SubRegions(StmtList stmts) {
+ foreach (var bb in stmts.BigBlocks) {
+ if (bb.ec is IfCmd) {
+ var ic = (IfCmd)bb.ec;
+ foreach (var r in SubRegions(ic.thn))
+ yield return r;
+
+ if (ic.elseBlock != null)
+ foreach (var r in SubRegions(ic.elseBlock))
+ yield return r;
+ } else if (bb.ec is WhileCmd) {
+ var wc = (WhileCmd)bb.ec;
+ yield return new StructuredRegion(wc);
+ }
+ }
+ }
+
+ public IEnumerable<Cmd> Cmds() {
+ if (cmd != null)
+ return Cmds(cmd.Body);
+ else
+ return Cmds(stmts);
+ }
+
+ public IEnumerable<object> CmdsChildRegions() {
+ if (cmd != null)
+ return CmdsChildRegions(cmd.Body);
+ else
+ return CmdsChildRegions(stmts);
+ }
+
+ public IEnumerable<IRegion> SubRegions() {
+ if (cmd != null)
+ return SubRegions(cmd.Body);
+ else
+ return SubRegions(stmts);
+ }
+
+ public Expr Guard() {
+ if (cmd != null)
+ return cmd.Guard;
+ else
+ return null;
+ }
+
+ public void AddInvariant(PredicateCmd pc) {
+ if (cmd != null)
+ cmd.Invariants.Add(pc);
+ }
+}
+
+}
\ No newline at end of file diff --git a/Source/GPUVerify/UnstructuredRegion.cs b/Source/GPUVerify/UnstructuredRegion.cs new file mode 100644 index 00000000..607dc6d7 --- /dev/null +++ b/Source/GPUVerify/UnstructuredRegion.cs @@ -0,0 +1,93 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using Graphing;
+
+namespace GPUVerify {
+
+class UnstructuredRegion : IRegion {
+ Graph<Block> blockGraph;
+ Block header;
+ Dictionary<Block, HashSet<Block>> loopNodes = new Dictionary<Block, HashSet<Block>>();
+ Dictionary<Block, Block> innermostHeader = new Dictionary<Block, Block>();
+ Expr guard;
+
+ public UnstructuredRegion(Program p, Implementation impl) {
+ blockGraph = p.ProcessLoops(impl);
+ header = null;
+ foreach (var h in blockGraph.SortHeadersByDominance()) {
+ var loopNodes = new HashSet<Block>();
+ foreach (var b in blockGraph.BackEdgeNodes(h))
+ loopNodes.UnionWith(blockGraph.NaturalLoops(h, b));
+ this.loopNodes[h] = loopNodes;
+ foreach (var n in loopNodes)
+ if (n != h)
+ innermostHeader[n] = h;
+ }
+ guard = null;
+ }
+
+ private UnstructuredRegion(UnstructuredRegion r, Block h) {
+ blockGraph = r.blockGraph;
+ header = h;
+ loopNodes = r.loopNodes;
+ innermostHeader = r.innermostHeader;
+ guard = null;
+ }
+
+ private HashSet<Block> SubBlocks() {
+ if (header != null) {
+ return loopNodes[header];
+ } else {
+ return blockGraph.Nodes;
+ }
+ }
+
+ public IEnumerable<Cmd> Cmds() {
+ foreach (var b in SubBlocks())
+ foreach (Cmd c in b.Cmds)
+ yield return c;
+ }
+
+ public IEnumerable<object> CmdsChildRegions() {
+ foreach (var b in SubBlocks()) {
+ if (b == header)
+ foreach (Cmd c in b.Cmds)
+ yield return c;
+ else if (innermostHeader[b] == header) {
+ if (loopNodes.ContainsKey(b))
+ yield return new UnstructuredRegion(this, b);
+ else
+ foreach (Cmd c in b.Cmds)
+ yield return c;
+ }
+ }
+ }
+
+ public IEnumerable<IRegion> SubRegions() {
+ return SubBlocks().Intersect(loopNodes.Keys).Select(b => new UnstructuredRegion(this, b));
+ }
+
+ public Expr Guard() {
+ if (header == null)
+ return null;
+ if (guard == null) {
+ var backedges = blockGraph.BackEdgeNodes(header);
+ if (backedges.Count() != 1)
+ return null;
+ var assumes = backedges.Single().Cmds.Cast<Cmd>().OfType<AssumeCmd>();
+ if (assumes.Count() != 1)
+ return null;
+ guard = assumes.Single().Expr;
+ }
+ return guard;
+ }
+
+ public void AddInvariant(PredicateCmd pc) {
+ header.Cmds = new CmdSeq((new Cmd[] {pc}.Concat(header.Cmds.Cast<Cmd>())).ToArray());
+ }
+}
+
+}
\ No newline at end of file |