diff options
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 26 | ||||
| -rw-r--r-- | Source/GPUVerify/EnabledToPredicateVisitor.cs | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/EnsureDisabledThreadHasNoEffectInstrumenter.cs | 94 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 264 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 3 | ||||
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 157 | ||||
| -rw-r--r-- | Source/GPUVerify/StructuredProgramVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/UniformExpressionAnalysisVisitor.cs | 38 | ||||
| -rw-r--r-- | Source/GPUVerify/UniformityAnalyser.cs | 289 |
9 files changed, 688 insertions, 193 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index f17efffe..78b3f51d 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -30,6 +30,12 @@ namespace GPUVerify public static bool ShowStages = false;
+ public static bool AddDivergenceCandidatesOnlyIfModified = false;
+ public static bool AddDivergenceCandidatesOnlyToBarrierLoops = false;
+
+ public static bool ShowUniformityAnalysis = false;
+ public static bool DoUniformityAnalysis = true;
+
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -135,6 +141,26 @@ namespace GPUVerify ArrayEqualities = true;
break;
+ case "-addDivergenceCandidatesOnlyIfModified":
+ case "/addDivergenceCandidatesOnlyIfModified":
+ AddDivergenceCandidatesOnlyIfModified = true;
+ break;
+
+ case "-addDivergenceCandidatesOnlyToBarrierLoops":
+ case "/addDivergenceCandidatesOnlyToBarrierLoops":
+ AddDivergenceCandidatesOnlyToBarrierLoops = true;
+ break;
+
+ case "-showUniformityAnalysis":
+ case "/showUniformityAnalysis":
+ ShowUniformityAnalysis = true;
+ break;
+
+ case "-noUniformityAnalysis":
+ case "/noUniformityAnalysis":
+ DoUniformityAnalysis = false;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
diff --git a/Source/GPUVerify/EnabledToPredicateVisitor.cs b/Source/GPUVerify/EnabledToPredicateVisitor.cs index 3cedd075..e004004f 100644 --- a/Source/GPUVerify/EnabledToPredicateVisitor.cs +++ b/Source/GPUVerify/EnabledToPredicateVisitor.cs @@ -10,13 +10,13 @@ namespace GPUVerify class EnabledToPredicateVisitor : StandardVisitor
{
- public EnabledToPredicateVisitor(TypedIdent currentPredicate)
+ public EnabledToPredicateVisitor(Expr currentPredicate)
{
this.currentPredicate = currentPredicate;
}
- private TypedIdent currentPredicate;
+ private Expr currentPredicate;
public override Expr VisitNAryExpr(NAryExpr node)
@@ -27,7 +27,7 @@ namespace GPUVerify if (call.Func.Name.Equals("__enabled"))
{
- return new IdentifierExpr(node.tok, new LocalVariable(node.tok, currentPredicate));
+ return currentPredicate;
}
}
diff --git a/Source/GPUVerify/EnsureDisabledThreadHasNoEffectInstrumenter.cs b/Source/GPUVerify/EnsureDisabledThreadHasNoEffectInstrumenter.cs new file mode 100644 index 00000000..32dde507 --- /dev/null +++ b/Source/GPUVerify/EnsureDisabledThreadHasNoEffectInstrumenter.cs @@ -0,0 +1,94 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class EnsureDisabledThreadHasNoEffectInstrumenter
+ {
+
+ private GPUVerifier verifier;
+ private Implementation Impl;
+
+ public EnsureDisabledThreadHasNoEffectInstrumenter(GPUVerifier verifier, Implementation Impl)
+ {
+ this.verifier = verifier;
+ this.Impl = Impl;
+ }
+
+ internal void instrument()
+ {
+
+ if (verifier.uniformityAnalyser.IsUniform(Impl.Name))
+ {
+ return;
+ }
+
+ foreach (IdentifierExpr iex in Impl.Proc.Modifies)
+ {
+ // For some reason, this does not work well with maps
+ if (iex.Decl.TypedIdent.Type is MapType)
+ {
+ continue;
+ }
+
+ Expr NoEffectExpr = Expr.Imp(
+ Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" +
+ GPUVerifier.GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),
+ Expr.Eq(iex, new OldExpr(iex.tok, iex))
+ );
+
+ Impl.Proc.Ensures.Add(new Ensures(false,
+ NoEffectExpr
+ ));
+
+ GPUVerifier.AddInvariantToAllLoops(NoEffectExpr, Impl.StructuredStmts);
+
+ }
+
+ AddEnablednessInvariantToAllLoops(Impl.StructuredStmts);
+ }
+
+ private void AddEnablednessInvariantToAllLoops(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ AddEnablednessInvariantToAllLoops(bb);
+ }
+ }
+
+ private void AddEnablednessInvariantToAllLoops(BigBlock bb)
+ {
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ Debug.Assert(wc.Guard is NAryExpr);
+ Debug.Assert((wc.Guard as NAryExpr).Fun is BinaryOperator);
+ Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);
+ string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;
+ LoopPredicate = GPUVerifier.StripThreadIdentifier(LoopPredicate);
+
+ wc.Invariants.Add(
+ new AssertCmd(wc.tok,
+ Expr.Imp(
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$1", Microsoft.Boogie.Type.Bool)))),
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Bool))))
+ )));
+
+ wc.Invariants.Add(
+ new AssertCmd(wc.tok,
+ Expr.Imp(
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))),
+ Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Bool))))
+ )));
+
+ AddEnablednessInvariantToAllLoops(wc.Body);
+ }
+
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index f4dee6d3..cb9c511e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -33,9 +33,9 @@ namespace GPUVerify private const string LOCAL_ID_Y_STRING = "local_id_y";
private const string LOCAL_ID_Z_STRING = "local_id_z";
- private static Constant _X = null;
- private static Constant _Y = null;
- private static Constant _Z = null;
+ internal static Constant _X = null;
+ internal static Constant _Y = null;
+ internal static Constant _Z = null;
private Constant _GROUP_SIZE_X = null;
private Constant _GROUP_SIZE_Y = null;
@@ -63,6 +63,8 @@ namespace GPUVerify public IRaceInstrumenter RaceInstrumenter;
+ public UniformityAnalyser uniformityAnalyser;
+
public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)
{
}
@@ -302,7 +304,7 @@ namespace GPUVerify DoLiveVariableAnalysis();
- DoSensitivityAnalysis();
+ DoUniformityAnalysis();
DoArrayControlFlowAnalysis();
@@ -419,9 +421,10 @@ namespace GPUVerify // TODO
}
- private void DoSensitivityAnalysis()
+ private void DoUniformityAnalysis()
{
- // TODO
+ uniformityAnalyser = new UniformityAnalyser(this);
+ uniformityAnalyser.Analyse();
}
private void DoLiveVariableAnalysis()
@@ -969,65 +972,113 @@ namespace GPUVerify {
WhileCmd wc = bb.ec as WhileCmd;
- 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;
+ AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
- LoopPredicate = LoopPredicate.Substring(0, LoopPredicate.IndexOf('$'));
+ RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);
- 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)))
- ));
+ AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);
+
+ AddCandidateInvariants(wc.Body, LocalVars, UserSuppliedInvariants, Impl);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ // We should have done predicated execution by now, so we won't have any if statements
+ Debug.Assert(false);
+ }
+ else
+ {
+ Debug.Assert(bb.ec == null);
+ }
+ }
+
+ private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, WhileCmd wc)
+ {
- foreach (Variable v in LocalVars)
+ if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)
+ {
+ if (!ContainsBarrierCall(wc.Body))
{
- string lv = StripThreadIdentifier(v.Name);
+ return;
+ }
+ }
- if (IsPredicateOrTemp(lv))
- {
- continue;
- }
+ 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 (!ContainsNamedVariable(GetModifiedVariables(wc.Body), StripThreadIdentifier(v.Name)))
- {
- continue;
- }
+ 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)))
+ ));
- AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+ foreach (Variable v in LocalVars)
+ {
+ string lv = StripThreadIdentifier(v.Name);
- if (Impl != KernelImplementation)
- {
- AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
- }
+ if (IsPredicateOrTemp(lv))
+ {
+ continue;
}
- if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)
+ if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)
{
- foreach (Variable v in NonLocalState.getAllNonLocalVariables())
+ if (!ContainsNamedVariable(GetModifiedVariables(wc.Body), StripThreadIdentifier(v.Name)))
{
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ continue;
}
}
- RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);
+ AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
- AddUserSuppliedInvariants(wc, UserSuppliedInvariants, Impl);
+ if (Impl != KernelImplementation)
+ {
+ AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
+ }
+ }
- AddCandidateInvariants(wc.Body, LocalVars, UserSuppliedInvariants, Impl);
+ if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)
+ {
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
+ {
+ AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ }
}
- else if (bb.ec is IfCmd)
+ }
+
+ private bool ContainsBarrierCall(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
{
- // We should have done predicated execution by now, so we won't have any if statements
- Debug.Assert(false);
+ if (ContainsBarrierCall(bb))
+ {
+ return true;
+ }
}
- else
+ return false;
+ }
+
+ private bool ContainsBarrierCall(BigBlock bb)
+ {
+ foreach (Cmd c in bb.simpleCmds)
{
- Debug.Assert(bb.ec == null);
+ if (c is CallCmd && ((c as CallCmd).Proc == BarrierProcedure))
+ {
+ return true;
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ return ContainsBarrierCall((bb.ec as WhileCmd).Body);
}
+
+ Debug.Assert(bb.ec == null || bb.ec is BreakCmd);
+
+ return false;
}
private bool ContainsNamedVariable(HashSet<Variable> variables, string name)
@@ -1240,7 +1291,7 @@ namespace GPUVerify return ExistentialBooleanConstant;
}
- private string StripThreadIdentifier(string p)
+ internal static string StripThreadIdentifier(string p)
{
return p.Substring(0, p.IndexOf("$"));
}
@@ -1339,77 +1390,13 @@ namespace GPUVerify continue;
}
- EnsureDisabledThreadHasNoEffect(Impl);
-
- }
-
- }
-
- private void EnsureDisabledThreadHasNoEffect(Implementation Impl)
- {
- foreach (IdentifierExpr iex in Impl.Proc.Modifies)
- {
- // For some reason, this does not work well with maps
- if (iex.Decl.TypedIdent.Type is MapType)
- {
- continue;
- }
-
- Expr NoEffectExpr = Expr.Imp(
- Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" + GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),
- Expr.Eq(iex, new OldExpr(iex.tok, iex))
- );
-
- Impl.Proc.Ensures.Add(new Ensures(false,
- NoEffectExpr
- ));
-
- AddInvariantToAllLoops(NoEffectExpr, Impl.StructuredStmts);
-
- }
-
- AddEnablednessInvariantToAllLoops(Impl.StructuredStmts);
- }
-
- private void AddEnablednessInvariantToAllLoops(StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- AddEnablednessInvariantToAllLoops(bb);
- }
- }
-
- private void AddEnablednessInvariantToAllLoops(BigBlock bb)
- {
- if (bb.ec is WhileCmd)
- {
- WhileCmd wc = bb.ec as WhileCmd;
- Debug.Assert(wc.Guard is NAryExpr);
- Debug.Assert((wc.Guard as NAryExpr).Fun is BinaryOperator);
- Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);
- string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;
- LoopPredicate = StripThreadIdentifier(LoopPredicate);
-
- wc.Invariants.Add(
- new AssertCmd(wc.tok,
- Expr.Imp(
- Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$1", Microsoft.Boogie.Type.Bool)))),
- Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Bool))))
- )));
+ new EnsureDisabledThreadHasNoEffectInstrumenter(this, Impl).instrument();
- wc.Invariants.Add(
- new AssertCmd(wc.tok,
- Expr.Imp(
- Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))),
- Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Bool))))
- )));
-
- AddEnablednessInvariantToAllLoops(wc.Body);
}
}
- private void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)
+ internal static void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)
{
foreach (BigBlock bb in stmtList.BigBlocks)
{
@@ -1417,7 +1404,7 @@ namespace GPUVerify }
}
- private void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)
+ internal static void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)
{
if (bb.ec is WhileCmd)
{
@@ -1428,7 +1415,7 @@ namespace GPUVerify Debug.Assert(!(bb.ec is IfCmd));
}
- private int GetThreadSuffix(string p)
+ internal static int GetThreadSuffix(string p)
{
return Int32.Parse(p.Substring(p.IndexOf("$") + 1, p.Length - (p.IndexOf("$") + 1)));
}
@@ -2309,40 +2296,47 @@ namespace GPUVerify {
if (d is Procedure)
{
- if (d != KernelProcedure)
+ Procedure proc = d as Procedure;
+ IdentifierExpr enabled = new IdentifierExpr(proc.tok,
+ new LocalVariable(proc.tok, new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool)));
+ Expr predicateExpr;
+ if (!uniformityAnalyser.IsUniform(proc.Name))
{
// Add predicate to start of parameter list
- Procedure proc = d as Procedure;
VariableSeq NewIns = new VariableSeq();
- TypedIdent enabled = new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool);
- NewIns.Add(new LocalVariable(proc.tok, enabled));
+ NewIns.Add(enabled.Decl);
foreach (Variable v in proc.InParams)
{
NewIns.Add(v);
}
proc.InParams = NewIns;
+ predicateExpr = enabled;
+ }
+ else
+ {
+ predicateExpr = Expr.True;
+ }
- RequiresSeq newRequires = new RequiresSeq();
- foreach (Requires r in proc.Requires)
- {
- newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, enabled)));
- }
- proc.Requires = newRequires;
-
- EnsuresSeq newEnsures = new EnsuresSeq();
- foreach (Ensures e in proc.Ensures)
- {
- newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, enabled)));
- }
- proc.Ensures = newEnsures;
-
+ RequiresSeq newRequires = new RequiresSeq();
+ foreach (Requires r in proc.Requires)
+ {
+ newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, predicateExpr)));
+ }
+ proc.Requires = newRequires;
+ EnsuresSeq newEnsures = new EnsuresSeq();
+ foreach (Ensures e in proc.Ensures)
+ {
+ newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, predicateExpr)));
}
+ proc.Ensures = newEnsures;
}
else if (d is Implementation)
{
- new Predicator(this, d != KernelImplementation).transform(d as Implementation);
+ Implementation impl = d as Implementation;
+ new Predicator(this, !uniformityAnalyser.IsUniform(impl.Name)).transform
+ (impl);
}
}
@@ -2494,9 +2488,15 @@ namespace GPUVerify ),
MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
}
- else
+ else if(bb.ec is IfCmd)
{
- Debug.Assert(bb.ec == null);
+ result.ec = new IfCmd(bb.ec.tok,
+ Expr.And(new VariableDualiser(1).VisitExpr((bb.ec as IfCmd).Guard),
+ new VariableDualiser(2).VisitExpr((bb.ec as IfCmd).Guard)),
+ MakeDual((bb.ec as IfCmd).thn, HalfDualise),
+ null,
+ (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock, HalfDualise));
+
}
return result;
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 66be025a..8590c6a5 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -107,6 +107,7 @@ <Compile Include="AccessInvariantProcessor.cs" />
<Compile Include="AccessRecord.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="StructuredProgramVisitor.cs" />
<Compile Include="CrossThreadInvariantProcessor.cs" />
<Compile Include="EnabledToPredicateVisitor.cs" />
@@ -126,6 +127,8 @@ <Compile Include="RaceInstrumenterBase.cs" />
<Compile Include="ReadCollector.cs" />
<Compile Include="SetEncodingRaceInstrumenter.cs" />
+ <Compile Include="UniformExpressionAnalysisVisitor.cs" />
+ <Compile Include="UniformityAnalyser.cs" />
<Compile Include="VariableDualiser.cs" />
<Compile Include="WriteCollector.cs" />
</ItemGroup>
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index 2cd43101..d94d7d56 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -15,7 +15,9 @@ namespace GPUVerify private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;
private Stack<Expr> predicate;
- private Stack<IdentifierExpr> enclosingLoopPredicate;
+ private Stack<Expr> enclosingLoopPredicate;
+
+ private Implementation impl = null;
internal Predicator(GPUVerifier verifier, bool AddPredicateParameter) : base(verifier)
{
@@ -24,11 +26,12 @@ namespace GPUVerify IfCounter = 0;
RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
predicate = new Stack<Expr>();
- enclosingLoopPredicate = new Stack<IdentifierExpr>();
+ enclosingLoopPredicate = new Stack<Expr>();
}
internal void transform(Implementation impl)
{
+ this.impl = impl;
Expr Predicate;
if (AddPredicateParameter)
@@ -49,11 +52,13 @@ namespace GPUVerify }
predicate.Push(Predicate);
- enclosingLoopPredicate.Push(null);
+ enclosingLoopPredicate.Push(Expr.True);
impl.StructuredStmts = VisitStmtList(impl.StructuredStmts);
- AddPredicateLocalVariables(impl);
+ AddPredicateLocalVariables(impl);
+
+ this.impl = null;
}
public override CmdSeq VisitCmd(Cmd c)
@@ -70,7 +75,11 @@ namespace GPUVerify public override CmdSeq VisitCallCmd(CallCmd Call)
{
List<Expr> NewIns = new List<Expr>();
- NewIns.Add(predicate.Peek());
+
+ if (!verifier.uniformityAnalyser.IsUniform(Call.callee))
+ {
+ NewIns.Add(predicate.Peek());
+ }
foreach (Expr e in Call.Ins)
{
@@ -158,37 +167,54 @@ namespace GPUVerify {
WhileCmd whileCmd = bb.ec as WhileCmd;
- string LoopPredicate = "_LC" + WhileLoopCounter;
- WhileLoopCounter++;
+ Expr PredicateExpr;
+ Expr NewGuard;
+ string LoopPredicate = null;
+ List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
- TypedIdent LoopPredicateTypedIdent = new TypedIdent(whileCmd.tok, LoopPredicate, Microsoft.Boogie.Type.Bool);
+ if (!enclosingLoopPredicate.Peek().Equals(Expr.True) || !verifier.uniformityAnalyser.IsUniform(impl.Name, whileCmd.Guard))
+ {
+ LoopPredicate = "_LC" + WhileLoopCounter;
+ WhileLoopCounter++;
- IdentifierExpr PredicateExpr = new IdentifierExpr(whileCmd.tok, new LocalVariable(whileCmd.tok, LoopPredicateTypedIdent));
- Expr GuardExpr = whileCmd.Guard;
+ TypedIdent LoopPredicateTypedIdent = new TypedIdent(whileCmd.tok, LoopPredicate, Microsoft.Boogie.Type.Bool);
- List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
- WhilePredicateLhss.Add(new SimpleAssignLhs(whileCmd.tok, PredicateExpr));
+ PredicateExpr = new IdentifierExpr(whileCmd.tok, new LocalVariable(whileCmd.tok, LoopPredicateTypedIdent));
- List<Expr> WhilePredicateRhss = new List<Expr>();
- WhilePredicateRhss.Add(predicate.Peek().Equals(Expr.True) ? GuardExpr : Expr.And(predicate.Peek(), GuardExpr));
+ WhilePredicateLhss.Add(new SimpleAssignLhs(whileCmd.tok, PredicateExpr as IdentifierExpr));
- firstBigBlock.simpleCmds.Add(new AssignCmd(whileCmd.tok, WhilePredicateLhss, WhilePredicateRhss));
+ List<Expr> WhilePredicateRhss = new List<Expr>();
+ WhilePredicateRhss.Add(predicate.Peek().Equals(Expr.True) ?
+ whileCmd.Guard : Expr.And(predicate.Peek(), whileCmd.Guard));
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(whileCmd.tok, WhilePredicateLhss, WhilePredicateRhss));
+
+ NewGuard = PredicateExpr;
+ }
+ else
+ {
+ PredicateExpr = enclosingLoopPredicate.Peek();
+ NewGuard = whileCmd.Guard;
+ }
predicate.Push(PredicateExpr);
enclosingLoopPredicate.Push(PredicateExpr);
- WhileCmd NewWhile = new WhileCmd(whileCmd.tok, PredicateExpr,
- VisitWhileInvariants(whileCmd.Invariants),
+ WhileCmd NewWhile = new WhileCmd(whileCmd.tok, NewGuard,
+ VisitWhileInvariants(whileCmd.Invariants, NewGuard),
VisitStmtList(whileCmd.Body));
enclosingLoopPredicate.Pop();
predicate.Pop();
- List<Expr> UpdatePredicateRhss = new List<Expr>();
- UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));
+ if (!enclosingLoopPredicate.Peek().Equals(Expr.True) || !verifier.uniformityAnalyser.IsUniform(impl.Name, whileCmd.Guard))
+ {
+ List<Expr> UpdatePredicateRhss = new List<Expr>();
+ UpdatePredicateRhss.Add(Expr.And(PredicateExpr, whileCmd.Guard));
- CmdSeq updateCmd = new CmdSeq();
- updateCmd.Add(new AssignCmd(whileCmd.tok, WhilePredicateLhss, UpdatePredicateRhss));
+ CmdSeq updateCmd = new CmdSeq();
+ updateCmd.Add(new AssignCmd(whileCmd.tok, WhilePredicateLhss, UpdatePredicateRhss));
- NewWhile.Body.BigBlocks.Add(new BigBlock(whileCmd.tok, "update_" + LoopPredicate, updateCmd, null, null));
+ NewWhile.Body.BigBlocks.Add(new BigBlock(whileCmd.tok, "update_" + LoopPredicate, updateCmd, null, null));
+ }
firstBigBlock.ec = NewWhile;
@@ -197,50 +223,68 @@ namespace GPUVerify {
IfCmd IfCommand = bb.ec as IfCmd;
- string IfPredicate = "_P" + IfCounter;
- IfCounter++;
-
- IdentifierExpr PredicateExpr = new IdentifierExpr(IfCommand.tok,
- new LocalVariable(IfCommand.tok, new TypedIdent(IfCommand.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
- Expr GuardExpr = IfCommand.Guard;
+ if (IfCommand.elseIf != null)
+ {
+ throw new InvalidOperationException();
+ }
- List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
- IfPredicateLhss.Add(new SimpleAssignLhs(IfCommand.tok, PredicateExpr));
+ if (predicate.Peek().Equals(Expr.True) && verifier.uniformityAnalyser.IsUniform(impl.Name, IfCommand.Guard))
+ {
+ firstBigBlock.ec =
+ new IfCmd(IfCommand.tok, IfCommand.Guard, VisitStmtList(IfCommand.thn),
+ null, IfCommand.elseBlock == null ? null : VisitStmtList(IfCommand.elseBlock));
+ }
+ else
+ {
+ string IfPredicate = "_P" + IfCounter;
+ IfCounter++;
- List<Expr> IfPredicateRhss = new List<Expr>();
- IfPredicateRhss.Add(GuardExpr);
+ IdentifierExpr PredicateExpr = new IdentifierExpr(IfCommand.tok,
+ new LocalVariable(IfCommand.tok, new TypedIdent(IfCommand.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
+ Expr GuardExpr = IfCommand.Guard;
- firstBigBlock.simpleCmds.Add(new AssignCmd(IfCommand.tok, IfPredicateLhss, IfPredicateRhss));
+ List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
+ IfPredicateLhss.Add(new SimpleAssignLhs(IfCommand.tok, PredicateExpr));
- Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
+ List<Expr> IfPredicateRhss = new List<Expr>();
+ IfPredicateRhss.Add(GuardExpr);
- predicate.Push(Expr.And(predicate.Peek(), PredicateExpr));
- StmtList PredicatedThen = VisitStmtList(IfCommand.thn);
- predicate.Pop();
- result.AddRange(PredicatedThen.BigBlocks);
+ firstBigBlock.simpleCmds.Add(new AssignCmd(IfCommand.tok, IfPredicateLhss, IfPredicateRhss));
- if(IfCommand.elseIf != null)
- {
- throw new InvalidOperationException();
- }
+ Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
- if (IfCommand.elseBlock != null)
- {
- predicate.Push(Expr.And(predicate.Peek(), Expr.Not(PredicateExpr)));
- StmtList PredicatedElse = VisitStmtList(IfCommand.elseBlock);
+ predicate.Push(Expr.And(predicate.Peek(), PredicateExpr));
+ StmtList PredicatedThen = VisitStmtList(IfCommand.thn);
predicate.Pop();
- result.AddRange(PredicatedElse.BigBlocks);
+ result.AddRange(PredicatedThen.BigBlocks);
+
+ if (IfCommand.elseBlock != null)
+ {
+ predicate.Push(Expr.And(predicate.Peek(), Expr.Not(PredicateExpr)));
+ StmtList PredicatedElse = VisitStmtList(IfCommand.elseBlock);
+ predicate.Pop();
+ result.AddRange(PredicatedElse.BigBlocks);
+ }
}
}
else if (bb.ec is BreakCmd)
{
- firstBigBlock.simpleCmds.Add(new AssignCmd(bb.tok,
- new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(bb.tok, enclosingLoopPredicate.Peek()) }),
- new List<Expr>(new Expr[] { new NAryExpr(bb.tok, new IfThenElse(bb.tok), new ExprSeq(
- new Expr[] { predicate.Peek(), Expr.False, enclosingLoopPredicate.Peek() })) })
- ));
- firstBigBlock.ec = null;
+ if (enclosingLoopPredicate.Equals(Expr.True))
+ {
+ firstBigBlock.ec = bb.ec;
+ }
+ else
+ {
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(bb.tok,
+ new List<AssignLhs>(new AssignLhs[] {
+ new SimpleAssignLhs(bb.tok, enclosingLoopPredicate.Peek() as IdentifierExpr) }),
+ new List<Expr>(new Expr[] { new NAryExpr(bb.tok, new IfThenElse(bb.tok), new ExprSeq(
+ new Expr[] { predicate.Peek(), Expr.False, enclosingLoopPredicate.Peek() })) })
+ ));
+ firstBigBlock.ec = null;
+ }
}
else if (bb.ec != null)
{
@@ -266,19 +310,20 @@ namespace GPUVerify throw new InvalidOperationException();
}
- public override List<PredicateCmd> VisitWhileInvariants(List<PredicateCmd> invariants)
+ public override List<PredicateCmd> VisitWhileInvariants(List<PredicateCmd> invariants, Expr WhileGuard)
{
List<PredicateCmd> result = new List<PredicateCmd>();
foreach (PredicateCmd cmd in invariants)
{
- result.Add(new AssertCmd(cmd.tok, ProcessEnabledIntrinsics(cmd.Expr, enclosingLoopPredicate.Peek().Decl.TypedIdent)));
+ result.Add(new AssertCmd(cmd.tok, ProcessEnabledIntrinsics(
+ cmd.Expr, WhileGuard)));
}
return result;
}
- internal static Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate)
+ internal static Expr ProcessEnabledIntrinsics(Expr expr, Expr currentPredicate)
{
return new EnabledToPredicateVisitor(currentPredicate).VisitExpr(expr);
}
diff --git a/Source/GPUVerify/StructuredProgramVisitor.cs b/Source/GPUVerify/StructuredProgramVisitor.cs index c01bf9c8..8ed5a926 100644 --- a/Source/GPUVerify/StructuredProgramVisitor.cs +++ b/Source/GPUVerify/StructuredProgramVisitor.cs @@ -77,7 +77,7 @@ namespace GPUVerify public virtual WhileCmd VisitWhileCmd(WhileCmd whileCmd)
{
return new WhileCmd(whileCmd.tok,
- VisitWhileGuard(whileCmd.Guard), VisitWhileInvariants(whileCmd.Invariants), VisitStmtList(whileCmd.Body));
+ VisitWhileGuard(whileCmd.Guard), VisitWhileInvariants(whileCmd.Invariants, whileCmd.Guard), VisitStmtList(whileCmd.Body));
}
public virtual BreakCmd VisitBreakCmd(BreakCmd breakCmd)
@@ -86,7 +86,7 @@ namespace GPUVerify }
- public virtual List<PredicateCmd> VisitWhileInvariants(List<PredicateCmd> invariants)
+ public virtual List<PredicateCmd> VisitWhileInvariants(List<PredicateCmd> invariants, Expr WhileGuard)
{
return invariants;
}
diff --git a/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs b/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs new file mode 100644 index 00000000..b5f0bb53 --- /dev/null +++ b/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs @@ -0,0 +1,38 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class UniformExpressionAnalysisVisitor : StandardVisitor
+ {
+
+ private bool isUniform = true;
+ private Dictionary<string, bool> uniformityInfo;
+
+ public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo)
+ {
+ this.uniformityInfo = uniformityInfo;
+ }
+
+ public override Variable VisitVariable(Variable v)
+ {
+ if (uniformityInfo.ContainsKey(v.Name))
+ {
+ if (!uniformityInfo[v.Name])
+ {
+ isUniform = false;
+ }
+ }
+
+ return v;
+ }
+
+ internal bool IsUniform()
+ {
+ return isUniform;
+ }
+ }
+}
diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs new file mode 100644 index 00000000..cbc067fe --- /dev/null +++ b/Source/GPUVerify/UniformityAnalyser.cs @@ -0,0 +1,289 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+
+ class UniformityAnalyser
+ {
+ private GPUVerifier verifier;
+
+ private Dictionary<string, bool> ProcedureChanged = null;
+
+ private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
+
+ public UniformityAnalyser(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
+ }
+
+ internal void Analyse()
+ {
+ ProcedureChanged = new Dictionary<string, bool>();
+
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if(D is Implementation)
+ {
+ bool uniformProcedure =
+ (D == verifier.KernelImplementation
+ || CommandLineOptions.DoUniformityAnalysis);
+
+ Implementation Impl = D as Implementation;
+ uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool> ()));
+
+ SetNonUniform(Impl.Name, GPUVerifier._X.Name);
+ SetNonUniform(Impl.Name, GPUVerifier._Y.Name);
+ SetNonUniform(Impl.Name, GPUVerifier._Z.Name);
+
+ foreach (Variable v in Impl.LocVars)
+ {
+ if (CommandLineOptions.DoUniformityAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ foreach (Variable v in Impl.InParams)
+ {
+ if (CommandLineOptions.DoUniformityAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ foreach (Variable v in Impl.OutParams)
+ {
+ if (CommandLineOptions.DoUniformityAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ ProcedureChanged[Impl.Name] = true;
+ }
+ }
+
+ if (CommandLineOptions.DoUniformityAnalysis)
+ {
+ while (SomeProcedureRequiresAnalysis())
+ {
+
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ if (ProcedureChanged[Impl.Name])
+ {
+ Analyse(Impl, uniformityInfo[Impl.Name].Key);
+ }
+ }
+ }
+ }
+ }
+
+ if (CommandLineOptions.ShowUniformityAnalysis)
+ {
+ dump();
+ }
+ }
+
+
+ private bool SomeProcedureRequiresAnalysis()
+ {
+ foreach (string procedureName in ProcedureChanged.Keys)
+ {
+ if (ProcedureChanged[procedureName])
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
+ {
+ ProcedureChanged[Impl.Name] = false;
+ Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);
+ }
+
+ private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ Analyse(impl, bb, ControlFlowIsUniform);
+ }
+ }
+
+ private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assignCmd = c as AssignCmd;
+ Debug.Assert(assignCmd.Lhss.Count == 1);
+ Debug.Assert(assignCmd.Rhss.Count == 1);
+ if (assignCmd.Lhss[0] is SimpleAssignLhs)
+ {
+ SimpleAssignLhs lhs = assignCmd.Lhss[0] as SimpleAssignLhs;
+ Expr rhs = assignCmd.Rhss[0];
+
+ if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
+ (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
+ {
+ SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
+ }
+
+ }
+ }
+ else if (c is CallCmd)
+ {
+ CallCmd callCmd = c as CallCmd;
+
+ if (callCmd.callee != verifier.BarrierProcedure.Name)
+ {
+
+ if (!ControlFlowIsUniform)
+ {
+ if (IsUniform(callCmd.callee))
+ {
+ SetNonUniform(callCmd.callee);
+ }
+ }
+ Implementation CalleeImplementation = GetImplementation(callCmd.callee);
+ for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ {
+ if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
+ && !IsUniform(impl.Name, callCmd.Ins[i]))
+ {
+ SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
+ }
+ }
+
+ for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ {
+ if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+ && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
+ {
+ SetNonUniform(impl.Name, callCmd.Outs[i].Name);
+ }
+ }
+
+ }
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard));
+ }
+ else if (bb.ec is IfCmd)
+ {
+ IfCmd ifCmd = bb.ec as IfCmd;
+ Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+ if (ifCmd.elseBlock != null)
+ {
+ Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+ }
+ Debug.Assert(ifCmd.elseIf == null);
+ }
+
+ }
+
+ private Implementation GetImplementation(string procedureName)
+ {
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation && ((D as Implementation).Name == procedureName))
+ {
+ return D as Implementation;
+ }
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private void SetNonUniform(string procedureName)
+ {
+ uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
+ (false, uniformityInfo[procedureName].Value);
+ RecordProcedureChanged(procedureName);
+ }
+
+ internal bool IsUniform(string procedureName)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+ return uniformityInfo[procedureName].Key;
+ }
+
+ internal bool IsUniform(string procedureName, Expr expr)
+ {
+ UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
+ visitor.VisitExpr(expr);
+ return visitor.IsUniform();
+ }
+
+ internal bool IsUniform(string procedureName, string v)
+ {
+ Debug.Assert(uniformityInfo.ContainsKey(procedureName));
+ return uniformityInfo[procedureName].Value[v];
+ }
+
+ private void SetUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = true;
+ RecordProcedureChanged(procedureName);
+ }
+
+ private void RecordProcedureChanged(string procedureName)
+ {
+ ProcedureChanged[procedureName] = true;
+ }
+
+ private void SetNonUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = false;
+ RecordProcedureChanged(procedureName);
+ }
+
+ private void dump()
+ {
+ foreach (string p in uniformityInfo.Keys)
+ {
+ Console.WriteLine("Procedure " + p + ": "
+ + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
+ foreach (string v in uniformityInfo[p].Value.Keys)
+ {
+ Console.WriteLine(" " + v + ": " +
+ (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
+ }
+ }
+ }
+
+ }
+
+}
|