diff options
| author |  Unknown <afd@afd-THINK.quadriga.com> | 2012-03-24 09:44:34 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.quadriga.com> | 2012-03-24 09:44:34 +0000 |
| commit | d386f4ea43b087f607f723238db0f73ac08f8d76 (patch) | |
| tree | 4cc89b621316b92e5a4ffc21ef556c8a72f748d5 | |
| parent | 15bf06fadd0009407ca8b20d2af844d804475b19 (diff) | |
Using uniform expression analysis in GPUVerify - also did some major refactoring to GPUVerify.
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/CrossThreadInvariantProcessor.cs | 87 | ||||
| -rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 50 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 634 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 403 | ||||
| -rw-r--r-- | Source/GPUVerify/LoopInvariantGenerator.cs | 265 | ||||
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 13 | ||||
| -rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 12 | ||||
| -rw-r--r-- | Source/GPUVerify/UniformExpressionAnalysisVisitor.cs | 11 | ||||
| -rw-r--r-- | Source/GPUVerify/UniformityAnalyser.cs | 77 | ||||
| -rw-r--r-- | Source/GPUVerify/VariableDualiser.cs | 17 |
12 files changed, 922 insertions, 651 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 78b3f51d..02598fa6 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -34,7 +34,7 @@ namespace GPUVerify public static bool AddDivergenceCandidatesOnlyToBarrierLoops = false;
public static bool ShowUniformityAnalysis = false;
- public static bool DoUniformityAnalysis = true;
+ public static bool DoUniformityAnalysis = false;
public static int Parse(string[] args)
{
diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs index c9b4c26c..4d215f24 100644 --- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs +++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs @@ -9,6 +9,14 @@ namespace GPUVerify {
class CrossThreadInvariantProcessor : StandardVisitor
{
+ private GPUVerifier verifier;
+ private string procName;
+
+ public CrossThreadInvariantProcessor(GPUVerifier verifier, string procName)
+ {
+ this.verifier = verifier;
+ this.procName = procName;
+ }
public override Expr VisitNAryExpr(NAryExpr node)
{
@@ -19,26 +27,27 @@ namespace GPUVerify if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))
{
- return Expr.Eq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));
+ return Expr.Eq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))
{
- return Expr.Neq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));
+ return Expr.Neq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__all"))
{
- return Expr.And(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));
+ return Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
if (call.Func.Name.Equals("__at_most_one"))
{
- return Expr.Not(Expr.And(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr)));
+ return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName)
+ .VisitExpr(node.Args[0].Clone() as Expr)));
}
@@ -48,6 +57,68 @@ namespace GPUVerify }
+ internal EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)
+ {
+ EnsuresSeq result = new EnsuresSeq();
+ foreach (Ensures e in ensuresSeq)
+ {
+ result.Add(new Ensures(e.Free, VisitExpr(e.Condition.Clone() as Expr)));
+ }
+ return result;
+ }
+
+ internal RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)
+ {
+ RequiresSeq result = new RequiresSeq();
+ foreach (Requires r in requiresSeq)
+ {
+ result.Add(new Requires(r.Free, VisitExpr(r.Condition.Clone() as Expr)));
+ }
+ return result;
+ }
+
+ internal void ProcessCrossThreadInvariants(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ ProcessCrossThreadInvariants(bb);
+ }
+ }
+
+ private void ProcessCrossThreadInvariants(BigBlock bb)
+ {
+ CmdSeq newCommands = new CmdSeq();
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is AssertCmd)
+ {
+ newCommands.Add(new AssertCmd(c.tok, VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));
+ }
+ else if (c is AssumeCmd)
+ {
+ newCommands.Add(new AssumeCmd(c.tok, VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));
+ }
+ else
+ {
+ newCommands.Add(c);
+ }
+ }
+
+ bb.simpleCmds = newCommands;
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd whileCmd = bb.ec as WhileCmd;
+ List<PredicateCmd> newInvariants = new List<PredicateCmd>();
+ foreach (PredicateCmd p in whileCmd.Invariants)
+ {
+ newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
+ }
+ whileCmd.Invariants = newInvariants;
+ ProcessCrossThreadInvariants(whileCmd.Body);
+ }
+ }
}
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 6d18c970..91b1edb6 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -172,8 +172,10 @@ namespace GPUVerify protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
{
- IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
- IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
+ IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok,
+ new VariableDualiser(1, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
+ IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok,
+ new VariableDualiser(2, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
@@ -206,30 +208,30 @@ namespace GPUVerify protected override Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType)
{
Expr RaceCondition = Expr.And(
- new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));
+ new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),
+ new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));
if (GPUVerifier.HasXDimension(v))
{
RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, SecondAccessType)))
+ new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, FirstAccessType))),
+ new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, SecondAccessType)))
));
}
if (GPUVerifier.HasYDimension(v))
{
RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, SecondAccessType)))
+ new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, FirstAccessType))),
+ new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, SecondAccessType)))
));
}
if (GPUVerifier.HasZDimension(v))
{
RaceCondition = Expr.And(RaceCondition, Expr.Eq(
- new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, FirstAccessType))),
- new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, SecondAccessType)))
+ new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, FirstAccessType))),
+ new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, SecondAccessType)))
));
}
@@ -246,7 +248,7 @@ namespace GPUVerify private static Expr MakeWrittenIndex(Variable v, int OneOrTwo)
{
- Expr result = new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(v.Clone() as Variable));
+ Expr result = new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(v.Clone() as Variable));
if (v.TypedIdent.Type is MapType)
{
@@ -254,7 +256,7 @@ namespace GPUVerify Debug.Assert(mt.Arguments.Length == 1);
result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, "WRITE"))) });
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, "WRITE"))) });
if (mt.Result is MapType)
{
@@ -263,7 +265,7 @@ namespace GPUVerify Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));
result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, "WRITE"))) });
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, "WRITE"))) });
if (mt2.Result is MapType)
{
@@ -273,7 +275,7 @@ namespace GPUVerify Debug.Assert(!(mt3.Result is MapType));
result = Expr.Select(result,
- new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });
+ new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });
}
}
@@ -290,10 +292,10 @@ namespace GPUVerify protected override void AddRequiresNoPendingAccess(Variable v)
{
- IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
- IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
- IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
- IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
+ IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
+ IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));
+ IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
+ IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
if (CommandLineOptions.Symmetry)
{
@@ -344,8 +346,8 @@ namespace GPUVerify if (GPUVerifier.HasZDimension(v) && verifier.KernelHasIdZ() && GPUVerifier.IndexTypeOfZDimension(v).Equals(verifier.GetTypeOfIdZ()))
{
expr = Expr.Imp(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread))));
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread))));
}
return expr;
}
@@ -365,8 +367,8 @@ namespace GPUVerify if (GPUVerifier.HasYDimension(v) && verifier.KernelHasIdY() && GPUVerifier.IndexTypeOfYDimension(v).Equals(verifier.GetTypeOfIdY()))
{
expr = Expr.Imp(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread))));
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread))));
}
return expr;
}
@@ -386,8 +388,8 @@ namespace GPUVerify if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
{
expr = Expr.Imp(
- new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
- Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
+ new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
+ Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
}
return expr;
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index cb9c511e..fe0fdeba 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -432,66 +432,6 @@ namespace GPUVerify // TODO
}
- private 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 HashSet<Variable> GetModifiedVariables(BigBlock bb)
- {
- HashSet<Variable> result = new HashSet<Variable>();
-
- foreach (Cmd c in bb.simpleCmds)
- {
- VariableSeq vars = new VariableSeq();
- c.AddAssignedVariables(vars);
- foreach (Variable v in vars)
- {
- result.Add(v);
- }
- }
-
- 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;
- }
private void ProcessAccessInvariants()
{
@@ -598,80 +538,18 @@ namespace GPUVerify if (d is Procedure)
{
Procedure p = d as Procedure;
- p.Requires = ProcessCrossThreadInvariants(p.Requires);
- p.Ensures = ProcessCrossThreadInvariants(p.Ensures);
+ p.Requires = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Requires);
+ p.Ensures = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Ensures);
}
if (d is Implementation)
{
Implementation i = d as Implementation;
- ProcessCrossThreadInvariants(i.StructuredStmts);
+ new CrossThreadInvariantProcessor(this, i.Name).ProcessCrossThreadInvariants(i.StructuredStmts);
}
}
}
- private EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)
- {
- EnsuresSeq result = new EnsuresSeq();
- foreach (Ensures e in ensuresSeq)
- {
- result.Add(new Ensures(e.Free, new CrossThreadInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr)));
- }
- return result;
- }
-
- private RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)
- {
- RequiresSeq result = new RequiresSeq();
- foreach (Requires r in requiresSeq)
- {
- result.Add(new Requires(r.Free, new CrossThreadInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr)));
- }
- return result;
- }
-
- private void ProcessCrossThreadInvariants(StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- ProcessCrossThreadInvariants(bb);
- }
- }
-
- private void ProcessCrossThreadInvariants(BigBlock bb)
- {
- CmdSeq newCommands = new CmdSeq();
-
- foreach (Cmd c in bb.simpleCmds)
- {
- if (c is AssertCmd)
- {
- newCommands.Add(new AssertCmd(c.tok, new CrossThreadInvariantProcessor().VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));
- }
- else if (c is AssumeCmd)
- {
- newCommands.Add(new AssumeCmd(c.tok, new CrossThreadInvariantProcessor().VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));
- }
- else
- {
- newCommands.Add(c);
- }
- }
-
- bb.simpleCmds = newCommands;
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd whileCmd = bb.ec as WhileCmd;
- List<PredicateCmd> newInvariants = new List<PredicateCmd>();
- foreach(PredicateCmd p in whileCmd.Invariants)
- {
- newInvariants.Add(new AssertCmd(p.tok, new CrossThreadInvariantProcessor().VisitExpr(p.Expr)));
- }
- whileCmd.Invariants = newInvariants;
- ProcessCrossThreadInvariants(whileCmd.Body);
- }
- }
private void emitProgram(string filename)
{
@@ -730,21 +608,7 @@ namespace GPUVerify List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants(Impl.Name);
- HashSet<Variable> LocalVars = new HashSet<Variable>();
- foreach (Variable v in Impl.LocVars)
- {
- LocalVars.Add(v);
- }
- foreach (Variable v in Impl.InParams)
- {
- LocalVars.Add(v);
- }
- foreach (Variable v in Impl.OutParams)
- {
- LocalVars.Add(v);
- }
-
- AddCandidateInvariants(Impl.StructuredStmts, LocalVars, UserSuppliedInvariants, Impl);
+ new LoopInvariantGenerator(this, Impl).instrument(UserSuppliedInvariants);
Procedure Proc = Impl.Proc;
@@ -829,8 +693,8 @@ namespace GPUVerify new IdentifierExpr(Proc.tok, new LocalVariable(Proc.tok, new TypedIdent(Proc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))
),
Expr.Eq(
- new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable))
)
));
}
@@ -839,8 +703,8 @@ namespace GPUVerify {
AddCandidateRequires(Proc,
Expr.Eq(
- new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable))
)
);
}
@@ -849,8 +713,8 @@ namespace GPUVerify {
AddCandidateEnsures(Proc,
Expr.Eq(
- new IdentifierExpr(Proc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(Proc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
+ new IdentifierExpr(Proc.tok, new VariableDualiser(1, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable)),
+ new IdentifierExpr(Proc.tok, new VariableDualiser(2, uniformityAnalyser, Proc.Name).VisitVariable(v.Clone() as Variable))
));
}
@@ -958,130 +822,7 @@ namespace GPUVerify return result;
}
- 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)
- {
- if (bb.ec is WhileCmd)
- {
- WhileCmd wc = bb.ec as WhileCmd;
-
- AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
-
- RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);
-
- 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)
- {
-
- if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)
- {
- if (!ContainsBarrierCall(wc.Body))
- {
- 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('$'));
-
- 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)))
- ));
-
- foreach (Variable v in LocalVars)
- {
- string lv = StripThreadIdentifier(v.Name);
-
- if (IsPredicateOrTemp(lv))
- {
- continue;
- }
-
- if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)
- {
- if (!ContainsNamedVariable(GetModifiedVariables(wc.Body), StripThreadIdentifier(v.Name)))
- {
- continue;
- }
- }
-
- AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
-
- if (Impl != KernelImplementation)
- {
- AddPredicatedEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv, Microsoft.Boogie.Type.Int)));
- }
- }
-
- if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)
- {
- foreach (Variable v in NonLocalState.getAllNonLocalVariables())
- {
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
- }
- }
- }
-
- private bool ContainsBarrierCall(StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- if (ContainsBarrierCall(bb))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool ContainsBarrierCall(BigBlock bb)
- {
- foreach (Cmd c in bb.simpleCmds)
- {
- 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)
+ internal static bool ContainsNamedVariable(HashSet<Variable> variables, string name)
{
foreach(Variable v in variables)
{
@@ -1093,30 +834,8 @@ namespace GPUVerify return false;
}
- private void AddEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
- {
- AddCandidateInvariant(wc,
- Expr.Eq(
- new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
- ));
- }
-
- private void AddPredicatedEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
- {
- AddCandidateInvariant(wc, 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)))
- ),
- Expr.Eq(
- new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable)),
- new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable))
- )));
- }
-
- private bool IsPredicateOrTemp(string lv)
+ internal static bool IsPredicateOrTemp(string lv)
{
return (lv.Length >= 2 && lv.Substring(0,2).Equals("_P")) ||
(lv.Length > 3 && lv.Substring(0,3).Equals("_LC")) ||
@@ -1125,21 +844,8 @@ namespace GPUVerify - private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)
- {
- foreach (Expr e in UserSuppliedInvariants)
- {
- wc.Invariants.Add(new AssertCmd(wc.tok, e));
- bool OK = ProgramIsOK(Impl);
- wc.Invariants.RemoveAt(wc.Invariants.Count - 1);
- if (OK)
- {
- AddCandidateInvariant(wc, e);
- }
- }
- }
- private bool ProgramIsOK(Declaration d)
+ internal bool ProgramIsOK(Declaration d)
{
Debug.Assert(d is Procedure || d is Implementation);
TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");
@@ -1275,15 +981,7 @@ namespace GPUVerify return _GROUP_SIZE_Z != null;
}
- public void AddCandidateInvariant(WhileCmd wc, Expr e)
- {
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(wc.tok);
- IdentifierExpr ExistentialBoolean = new IdentifierExpr(wc.tok, ExistentialBooleanConstant);
- wc.Invariants.Add(new AssertCmd(wc.tok, Expr.Imp(ExistentialBoolean, e)));
- Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
- }
-
- private Constant MakeExistentialBoolean(IToken tok)
+ internal Constant MakeExistentialBoolean(IToken tok)
{
Constant ExistentialBooleanConstant = new Constant(tok, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
invariantGenerationCounter++;
@@ -1624,8 +1322,8 @@ namespace GPUVerify private void HavocAndAssumeEquality(IToken tok, BigBlock bb, Variable v)
{
- IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable));
- IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable));
+ IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
+ IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
IdentifierExprSeq ModifiedVars = new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 });
bb.simpleCmds.Add(new HavocCmd(tok, ModifiedVars));
@@ -2164,35 +1862,9 @@ namespace GPUVerify if (d is Procedure)
{
- // DuplicateParameters
- Procedure proc = d as Procedure;
-
- bool HalfDualise = HalfDualisedProcedureNames.Contains(proc.Name);
-
- proc.Requires = DualiseRequires(proc.Requires);
- proc.Ensures = DualiseEnsures(proc.Ensures);
+ new KernelDualiser(this).DualiseProcedure(d as Procedure);
- proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise);
- proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise);
- IdentifierExprSeq NewModifies = new IdentifierExprSeq();
- foreach (IdentifierExpr v in proc.Modifies)
- {
- NewModifies.Add(new VariableDualiser(1).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
- }
-
- if (!HalfDualise)
- {
- foreach (IdentifierExpr v in proc.Modifies)
- {
- if (!CommandLineOptions.Symmetry || !HalfDualisedVariableNames.Contains(v.Name))
- {
- NewModifies.Add(new VariableDualiser(2).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
- }
- }
- }
- proc.Modifies = NewModifies;
-
- NewTopLevelDeclarations.Add(proc);
+ NewTopLevelDeclarations.Add(d as Procedure);
continue;
@@ -2200,17 +1872,10 @@ namespace GPUVerify if (d is Implementation)
{
- // DuplicateParameters
- Implementation impl = d as Implementation;
- bool HalfDualise = HalfDualisedProcedureNames.Contains(impl.Name);
+ new KernelDualiser(this).DualiseImplementation(d as Implementation);
- impl.InParams = DualiseVariableSequence(impl.InParams, HalfDualise);
- impl.OutParams = DualiseVariableSequence(impl.OutParams, HalfDualise);
- MakeDualLocalVariables(impl, HalfDualise);
- impl.StructuredStmts = MakeDual(impl.StructuredStmts, HalfDualise);
-
- NewTopLevelDeclarations.Add(impl);
+ NewTopLevelDeclarations.Add(d as Implementation);
continue;
@@ -2218,11 +1883,11 @@ namespace GPUVerify if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)))
{
- NewTopLevelDeclarations.Add(new VariableDualiser(1).VisitVariable((Variable)d.Clone()));
+ NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)d.Clone()));
if (!HalfDualisedVariableNames.Contains((d as Variable).Name))
{
- NewTopLevelDeclarations.Add(new VariableDualiser(2).VisitVariable((Variable)d.Clone()));
+ NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)d.Clone()));
}
continue;
@@ -2236,60 +1901,6 @@ namespace GPUVerify }
- private EnsuresSeq DualiseEnsures(EnsuresSeq ensuresSeq)
- {
- EnsuresSeq newEnsures = new EnsuresSeq();
- foreach (Ensures e in ensuresSeq)
- {
- newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1).VisitExpr(e.Condition.Clone() as Expr)));
- if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition))
- {
- newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2).VisitExpr(e.Condition.Clone() as Expr)));
- }
- }
- return newEnsures;
- }
-
- private RequiresSeq DualiseRequires(RequiresSeq requiresSeq)
- {
- RequiresSeq newRequires = new RequiresSeq();
- foreach (Requires r in requiresSeq)
- {
- newRequires.Add(new Requires(r.Free, new VariableDualiser(1).VisitExpr(r.Condition.Clone() as Expr)));
-
- if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition))
- {
- newRequires.Add(new Requires(r.Free, new VariableDualiser(2).VisitExpr(r.Condition.Clone() as Expr)));
- }
- }
- return newRequires;
- }
-
- private bool ContainsAsymmetricExpression(Expr expr)
- {
- AsymmetricExpressionFinder finder = new AsymmetricExpressionFinder();
- finder.VisitExpr(expr);
- return finder.foundAsymmetricExpr();
- }
-
- private static VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)
- {
- VariableSeq result = new VariableSeq();
- foreach (Variable v in seq)
- {
- result.Add(new VariableDualiser(1).VisitVariable((Variable)v.Clone()));
- }
-
- if (!HalfDualise)
- {
- foreach (Variable v in seq)
- {
- result.Add(new VariableDualiser(2).VisitVariable((Variable)v.Clone()));
- }
- }
- return result;
- }
-
private void MakeKernelPredicated()
{
foreach (Declaration d in Program.TopLevelDeclarations)
@@ -2342,199 +1953,6 @@ namespace GPUVerify }
- private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
- {
- Contract.Requires(stmtList != null);
-
- StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
-
- foreach (BigBlock bodyBlock in stmtList.BigBlocks)
- {
- result.BigBlocks.Add(MakeDual(bodyBlock, HalfDualise));
- }
-
- return result;
- }
-
- private BigBlock MakeDual(BigBlock bb, bool HalfDualise)
- {
- // Not sure what to do about the transfer command
-
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- foreach (Cmd c in bb.simpleCmds)
- {
- if (c is CallCmd)
- {
- CallCmd Call = c as CallCmd;
-
- List<Expr> newIns = new List<Expr>();
- foreach (Expr e in Call.Ins)
- {
- newIns.Add(new VariableDualiser(1).VisitExpr(e));
- }
- if (!HalfDualise && !HalfDualisedProcedureNames.Contains(Call.callee))
- {
- foreach (Expr e in Call.Ins)
- {
- newIns.Add(new VariableDualiser(2).VisitExpr(e));
- }
- }
-
- List<IdentifierExpr> newOuts = new List<IdentifierExpr>();
- foreach (IdentifierExpr ie in Call.Outs)
- {
- newOuts.Add(new VariableDualiser(1).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
- }
- if (!HalfDualise && !HalfDualisedProcedureNames.Contains(Call.callee))
- {
- foreach (IdentifierExpr ie in Call.Outs)
- {
- newOuts.Add(new VariableDualiser(2).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
- }
- }
-
- CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
-
- NewCallCmd.Proc = Call.Proc;
-
- result.simpleCmds.Add(NewCallCmd);
- }
- else if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
-
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- List<AssignLhs> newLhss = new List<AssignLhs>();
-
- newLhss.Add(new VariableDualiser(1).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
-
- if (!HalfDualise)
- {
- newLhss.Add(new VariableDualiser(2).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- }
-
- List<Expr> newRhss = new List<Expr>();
-
- newRhss.Add(new VariableDualiser(1).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
-
- if (!HalfDualise)
- {
- newRhss.Add(new VariableDualiser(2).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- }
-
- AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
-
- result.simpleCmds.Add(newAssign);
- }
- else if (c is HavocCmd)
- {
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
-
- HavocCmd newHavoc;
-
- if (HalfDualise)
- {
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
- }
- else
- {
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
- (IdentifierExpr)(new VariableDualiser(2).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
- }
- result.simpleCmds.Add(newHavoc);
- }
- else if (c is AssertCmd)
- {
- AssertCmd ass = c as AssertCmd;
- if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
- }
- }
- else if (c is AssumeCmd)
- {
- AssumeCmd ass = c as AssumeCmd;
- if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
- }
- }
- else
- {
- Debug.Assert(false);
- }
- }
-
- if (bb.ec is WhileCmd)
- {
- result.ec = new WhileCmd(bb.ec.tok,
- Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard),
- new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)
- ),
- MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
- }
- else if(bb.ec is IfCmd)
- {
- 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;
-
- }
-
- private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
- {
- List<PredicateCmd> result = new List<PredicateCmd>();
- foreach(PredicateCmd p in originalInvariants)
- {
- result.Add(new AssertCmd(p.tok, new VariableDualiser(1).VisitExpr(p.Expr.Clone() as Expr)));
- if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))
- {
- result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr)));
- }
- }
-
- return result;
- }
-
- private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
- {
- VariableSeq NewLocalVars = new VariableSeq();
-
- foreach (LocalVariable v in impl.LocVars)
- {
- NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$1", v.TypedIdent.Type)));
- if (!HalfDualise)
- {
- NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$2", v.TypedIdent.Type)));
- }
- }
-
- impl.LocVars = NewLocalVars;
- }
-
-
private void CheckKernelParameters()
{
if (KernelProcedure.OutParams.Length != 0)
@@ -2667,5 +2085,13 @@ namespace GPUVerify QKeyValue.FindBoolAttribute(variable.Attributes, LOCAL_ID_Z_STRING));
}
+ internal void AddCandidateInvariant(WhileCmd wc, Expr e)
+ {
+ Constant ExistentialBooleanConstant = MakeExistentialBoolean(wc.tok);
+ IdentifierExpr ExistentialBoolean = new IdentifierExpr(wc.tok, ExistentialBooleanConstant);
+ wc.Invariants.Add(new AssertCmd(wc.tok, Expr.Imp(ExistentialBoolean, e)));
+ Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
+ }
+
}
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 8590c6a5..c216d089 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,6 +108,8 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
+ <Compile Include="KernelDualiser.cs" />
+ <Compile Include="LoopInvariantGenerator.cs" />
<Compile Include="StructuredProgramVisitor.cs" />
<Compile Include="CrossThreadInvariantProcessor.cs" />
<Compile Include="EnabledToPredicateVisitor.cs" />
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs new file mode 100644 index 00000000..6f6d7184 --- /dev/null +++ b/Source/GPUVerify/KernelDualiser.cs @@ -0,0 +1,403 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class KernelDualiser
+ {
+ private GPUVerifier verifier;
+
+ public KernelDualiser(GPUVerifier verifier)
+ {
+ this.verifier = verifier;
+ }
+
+ private string procName = null;
+
+ internal void DualiseProcedure(Microsoft.Boogie.Procedure proc)
+ {
+ procName = proc.Name;
+
+ bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(proc.Name);
+
+ proc.Requires = DualiseRequires(proc.Requires);
+ proc.Ensures = DualiseEnsures(proc.Ensures);
+
+ proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise);
+ proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise);
+ IdentifierExprSeq NewModifies = new IdentifierExprSeq();
+ foreach (IdentifierExpr v in proc.Modifies)
+ {
+ NewModifies.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
+ }
+
+ if (!HalfDualise)
+ {
+ foreach (IdentifierExpr v in proc.Modifies)
+ {
+ if (!CommandLineOptions.Symmetry || !verifier.HalfDualisedVariableNames.Contains(v.Name))
+ {
+ NewModifies.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
+ }
+ }
+ }
+ proc.Modifies = NewModifies;
+
+ procName = null;
+ }
+
+ private RequiresSeq DualiseRequires(RequiresSeq requiresSeq)
+ {
+ RequiresSeq newRequires = new RequiresSeq();
+ foreach (Requires r in requiresSeq)
+ {
+ newRequires.Add(new Requires(r.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).
+ VisitExpr(r.Condition.Clone() as Expr)));
+
+ if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition))
+ && !verifier.uniformityAnalyser.IsUniform(procName, r.Condition))
+ {
+ newRequires.Add(new Requires(r.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).
+ VisitExpr(r.Condition.Clone() as Expr)));
+ }
+ }
+ return newRequires;
+ }
+
+ private EnsuresSeq DualiseEnsures(EnsuresSeq ensuresSeq)
+ {
+ EnsuresSeq newEnsures = new EnsuresSeq();
+ foreach (Ensures e in ensuresSeq)
+ {
+ newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).
+ VisitExpr(e.Condition.Clone() as Expr)));
+ if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition))
+ && !verifier.uniformityAnalyser.IsUniform(procName, e.Condition))
+ {
+ newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).
+ VisitExpr(e.Condition.Clone() as Expr)));
+ }
+ }
+ return newEnsures;
+ }
+
+
+ private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
+ {
+ Contract.Requires(stmtList != null);
+
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+
+ foreach (BigBlock bodyBlock in stmtList.BigBlocks)
+ {
+ result.BigBlocks.Add(MakeDual(bodyBlock, HalfDualise));
+ }
+
+ return result;
+ }
+
+ private BigBlock MakeDual(BigBlock bb, bool HalfDualise)
+ {
+ // Not sure what to do about the transfer command
+
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is CallCmd)
+ {
+ CallCmd Call = c as CallCmd;
+
+ List<Expr> uniformNewIns = new List<Expr>();
+ List<Expr> nonUniformNewIns = new List<Expr>();
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))
+ {
+ uniformNewIns.Add(Call.Ins[i]);
+ }
+ else
+ {
+ nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
+ }
+ }
+ if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))
+ {
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
+ {
+ nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
+ }
+ }
+ }
+
+ List<Expr> newIns = uniformNewIns;
+ newIns.AddRange(nonUniformNewIns);
+
+ List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();
+ List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();
+ for (int i = 0; i < Call.Outs.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))
+ {
+ uniformNewOuts.Add(Call.Outs[i]);
+ }
+ else
+ {
+ nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
+ }
+
+ }
+ if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))
+ {
+ for (int i = 0; i < Call.Outs.Count; i++)
+ {
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
+ {
+ nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
+ }
+ }
+ }
+
+ List<IdentifierExpr> newOuts = uniformNewOuts;
+ newOuts.AddRange(nonUniformNewOuts);
+
+ CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
+
+ NewCallCmd.Proc = Call.Proc;
+
+ result.simpleCmds.Add(NewCallCmd);
+ }
+ else if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+
+ if (assign.Lhss[0] is SimpleAssignLhs &&
+ verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ {
+ result.simpleCmds.Add(assign);
+ }
+ else
+ {
+ List<AssignLhs> newLhss = new List<AssignLhs>();
+ List<Expr> newRhss = new List<Expr>();
+
+ newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+
+ if (!HalfDualise)
+ {
+ newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ }
+
+ newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+
+ if (!HalfDualise)
+ {
+ newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ }
+
+ AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
+
+ result.simpleCmds.Add(newAssign);
+ }
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
+
+ HavocCmd newHavoc;
+
+ if (HalfDualise)
+ {
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
+ }
+ else
+ {
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
+ (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
+ }
+ result.simpleCmds.Add(newHavoc);
+ }
+ else if (c is AssertCmd)
+ {
+ AssertCmd ass = c as AssertCmd;
+ if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
+ {
+ result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
+ else
+ {
+ result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
+ }
+ }
+ else if (c is AssumeCmd)
+ {
+ AssumeCmd ass = c as AssumeCmd;
+ if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))
+ {
+ result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
+ else
+ {
+ result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
+ }
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ Expr NewGuard;
+ if (verifier.uniformityAnalyser.IsUniform(procName, (bb.ec as WhileCmd).Guard))
+ {
+ NewGuard = (bb.ec as WhileCmd).Guard;
+ }
+ else
+ {
+ NewGuard = Expr.Or(Dualise((bb.ec as WhileCmd).Guard, 1),
+ Dualise((bb.ec as WhileCmd).Guard, 2)
+ );
+ }
+ result.ec = new WhileCmd(bb.ec.tok,
+ NewGuard,
+ MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
+ }
+ else if (bb.ec is IfCmd)
+ {
+ Debug.Assert(verifier.uniformityAnalyser.IsUniform(procName, (bb.ec as IfCmd).Guard));
+ result.ec = new IfCmd(bb.ec.tok,
+ (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;
+
+ }
+
+ private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
+ {
+ List<PredicateCmd> result = new List<PredicateCmd>();
+ foreach (PredicateCmd p in originalInvariants)
+ {
+ result.Add(new AssertCmd(p.tok,
+ Dualise(p.Expr, 1)));
+ if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))
+ && !verifier.uniformityAnalyser.IsUniform(procName, p.Expr))
+ {
+ result.Add(new AssertCmd(p.tok, Dualise(p.Expr, 2)));
+ }
+ }
+
+ return result;
+ }
+
+ private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
+ {
+ VariableSeq NewLocalVars = new VariableSeq();
+
+ foreach (LocalVariable v in impl.LocVars)
+ {
+ if (verifier.uniformityAnalyser.IsUniform(procName, v.Name))
+ {
+ NewLocalVars.Add (v);
+ }
+ else
+ {
+ NewLocalVars.Add(
+ new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));
+ if (!HalfDualise)
+ {
+ NewLocalVars.Add(
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));
+ }
+ }
+ }
+
+ impl.LocVars = NewLocalVars;
+ }
+
+ private bool ContainsAsymmetricExpression(Expr expr)
+ {
+ AsymmetricExpressionFinder finder = new AsymmetricExpressionFinder();
+ finder.VisitExpr(expr);
+ return finder.foundAsymmetricExpr();
+ }
+
+ private VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)
+ {
+ VariableSeq uniform = new VariableSeq();
+ VariableSeq nonuniform = new VariableSeq();
+
+ foreach (Variable v in seq)
+ {
+ if (verifier.uniformityAnalyser.IsUniform(procName, v.Name))
+ {
+ uniform.Add(v);
+ }
+ else
+ {
+ nonuniform.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));
+ }
+ }
+
+ if (!HalfDualise)
+ {
+ foreach (Variable v in seq)
+ {
+ if (!verifier.uniformityAnalyser.IsUniform(procName, v.Name))
+ {
+ nonuniform.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));
+ }
+ }
+ }
+
+ VariableSeq result = uniform;
+ result.AddRange(nonuniform);
+ return result;
+ }
+
+
+ internal void DualiseImplementation(Implementation impl)
+ {
+ procName = impl.Name;
+
+ bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(impl.Name);
+
+ impl.InParams = DualiseVariableSequence(impl.InParams, HalfDualise);
+ impl.OutParams = DualiseVariableSequence(impl.OutParams, HalfDualise);
+ MakeDualLocalVariables(impl, HalfDualise);
+ impl.StructuredStmts = MakeDual(impl.StructuredStmts, HalfDualise);
+
+ procName = null;
+ }
+
+ private Expr Dualise(Expr expr, int thread)
+ {
+ return new VariableDualiser(thread, verifier.uniformityAnalyser, procName).VisitExpr(expr.Clone() as Expr);
+ }
+
+ }
+
+
+}
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs new file mode 100644 index 00000000..4ec6de6c --- /dev/null +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -0,0 +1,265 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class LoopInvariantGenerator
+ {
+ private GPUVerifier verifier;
+ private Implementation Impl;
+
+ public LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl)
+ {
+ this.verifier = verifier;
+ this.Impl = Impl;
+ }
+
+ internal void instrument(List<Expr> UserSuppliedInvariants)
+ {
+ HashSet<Variable> LocalVars = new HashSet<Variable>();
+ foreach (Variable v in Impl.LocVars)
+ {
+ LocalVars.Add(v);
+ }
+ foreach (Variable v in Impl.InParams)
+ {
+ LocalVars.Add(v);
+ }
+ foreach (Variable v in Impl.OutParams)
+ {
+ LocalVars.Add(v);
+ }
+
+ AddCandidateInvariants(Impl.StructuredStmts, LocalVars, UserSuppliedInvariants, Impl);
+
+ }
+
+ private void AddEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
+ {
+ verifier.AddCandidateInvariant(wc,
+ 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))
+ ));
+ }
+
+ private void AddPredicatedEqualityCandidateInvariant(WhileCmd wc, string LoopPredicate, Variable v)
+ {
+ verifier.AddCandidateInvariant(wc, 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)))
+ ),
+ 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))
+ )));
+ }
+
+
+ private void AddBarrierDivergenceCandidates(HashSet<Variable> LocalVars, Implementation Impl, WhileCmd wc)
+ {
+
+ if (CommandLineOptions.AddDivergenceCandidatesOnlyToBarrierLoops)
+ {
+ if (!ContainsBarrierCall(wc.Body))
+ {
+ 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('$'));
+
+ 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)))
+ ));
+
+ foreach (Variable v in LocalVars)
+ {
+ string lv = GPUVerifier.StripThreadIdentifier(v.Name);
+
+ if (GPUVerifier.IsPredicateOrTemp(lv))
+ {
+ continue;
+ }
+
+ if (CommandLineOptions.AddDivergenceCandidatesOnlyIfModified)
+ {
+ if (!GPUVerifier.ContainsNamedVariable(GetModifiedVariables(wc.Body),
+ GPUVerifier.StripThreadIdentifier(v.Name)))
+ {
+ continue;
+ }
+ }
+
+ AddEqualityCandidateInvariant(wc, LoopPredicate, new LocalVariable(wc.tok, new TypedIdent(wc.tok, 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 (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)
+ {
+ foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())
+ {
+ AddEqualityCandidateInvariant(wc, 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)
+ {
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+
+ AddBarrierDivergenceCandidates(LocalVars, Impl, wc);
+
+ verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(wc);
+
+ 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 AddUserSuppliedInvariants(WhileCmd wc, 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);
+ if (OK)
+ {
+ verifier.AddCandidateInvariant(wc, e);
+ }
+ }
+ }
+
+ private 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 HashSet<Variable> GetModifiedVariables(BigBlock bb)
+ {
+ HashSet<Variable> result = new HashSet<Variable>();
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ VariableSeq vars = new VariableSeq();
+ c.AddAssignedVariables(vars);
+ foreach (Variable v in vars)
+ {
+ result.Add(v);
+ }
+ }
+
+ 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;
+ }
+
+ private bool ContainsBarrierCall(StmtList stmtList)
+ {
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ if (ContainsBarrierCall(bb))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private bool ContainsBarrierCall(BigBlock bb)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is CallCmd && ((c as CallCmd).Proc == verifier.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;
+ }
+
+
+ }
+}
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index d94d7d56..a1938376 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -117,12 +117,21 @@ namespace GPUVerify Debug.Assert(havoc.Vars.Length == 1);
+ if (predicate.Peek().Equals(Expr.True))
+ {
+ result.Add(havoc);
+ return result;
+ }
+
Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
Debug.Assert(type != null);
RequiredHavocVariables.Add(type);
IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
+
+ verifier.uniformityAnalyser.AddNonUniform(impl.Name, HavocTempExpr.Decl.Name);
+
result.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
HavocTempExpr
})));
@@ -177,6 +186,8 @@ namespace GPUVerify LoopPredicate = "_LC" + WhileLoopCounter;
WhileLoopCounter++;
+ verifier.uniformityAnalyser.AddNonUniform(impl.Name, LoopPredicate);
+
TypedIdent LoopPredicateTypedIdent = new TypedIdent(whileCmd.tok, LoopPredicate, Microsoft.Boogie.Type.Bool);
PredicateExpr = new IdentifierExpr(whileCmd.tok, new LocalVariable(whileCmd.tok, LoopPredicateTypedIdent));
@@ -239,6 +250,8 @@ namespace GPUVerify string IfPredicate = "_P" + IfCounter;
IfCounter++;
+ verifier.uniformityAnalyser.AddNonUniform(impl.Name, IfPredicate);
+
IdentifierExpr PredicateExpr = new IdentifierExpr(IfCommand.tok,
new LocalVariable(IfCommand.tok, new TypedIdent(IfCommand.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
Expr GuardExpr = IfCommand.Guard;
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index d9f674da..bda8f01f 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -190,13 +190,13 @@ namespace GPUVerify protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
{
- IdentifierExpr AccessSet1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(
+ IdentifierExpr AccessSet1 = new IdentifierExpr(tok, new VariableDualiser(1, null, null).VisitVariable(
MakeAccessSetVariable(v, AccessType)));
IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();
VariablesToHavoc.Add(AccessSet1);
if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
{
- IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(
+ IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2, null, null).VisitVariable(
MakeAccessSetVariable(v, AccessType)));
VariablesToHavoc.Add(AccessSet2);
}
@@ -284,8 +284,8 @@ namespace GPUVerify {
VariableSeq DummyVarsAccess1;
VariableSeq DummyVarsAccess2;
- Expr IndexExpr1 = QuantifiedIndexExpr(v, new VariableDualiser(1).VisitVariable(v.Clone() as Variable), out DummyVarsAccess1);
- Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2).VisitVariable(v.Clone() as Variable), out DummyVarsAccess2);
+ Expr IndexExpr1 = QuantifiedIndexExpr(v, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess1);
+ Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess2);
Debug.Assert(DummyVarsAccess1.Length == DummyVarsAccess2.Length);
Debug.Assert(DummyVars1.Length == DummyVarsAccess1.Length);
for (int i = 0; i < DummyVars1.Length; i++)
@@ -341,7 +341,7 @@ namespace GPUVerify private static Expr AccessExpr(Variable v, String AccessType, int Thread, out VariableSeq DummyVars)
{
- return QuantifiedIndexExpr(v, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType)), out DummyVars);
+ return QuantifiedIndexExpr(v, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType)), out DummyVars);
}
private static Expr QuantifiedIndexExpr(Variable v, Variable AccessSetVariable, out VariableSeq DummyVars)
@@ -401,7 +401,7 @@ namespace GPUVerify private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)
{
- return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))));
+ return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType))));
}
diff --git a/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs b/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs index b5f0bb53..76f6b5de 100644 --- a/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs +++ b/Source/GPUVerify/UniformExpressionAnalysisVisitor.cs @@ -19,12 +19,13 @@ namespace GPUVerify public override Variable VisitVariable(Variable v)
{
- if (uniformityInfo.ContainsKey(v.Name))
+ if (!uniformityInfo.ContainsKey(v.Name))
{
- if (!uniformityInfo[v.Name])
- {
- isUniform = false;
- }
+ isUniform = isUniform && (v is Constant);
+ }
+ else if (!uniformityInfo[v.Name])
+ {
+ isUniform = false;
}
return v;
diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs index cbc067fe..cf09ed82 100644 --- a/Source/GPUVerify/UniformityAnalyser.cs +++ b/Source/GPUVerify/UniformityAnalyser.cs @@ -16,10 +16,16 @@ namespace GPUVerify private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
+ private Dictionary<string, List<string>> inParameters;
+
+ private Dictionary<string, List<string>> outParameters;
+
public UniformityAnalyser(GPUVerifier verifier)
{
this.verifier = verifier;
uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
+ inParameters = new Dictionary<string, List<string>>();
+ outParameters = new Dictionary<string, List<string>>();
}
internal void Analyse()
@@ -54,8 +60,11 @@ namespace GPUVerify }
}
+ inParameters[Impl.Name] = new List<string>();
+
foreach (Variable v in Impl.InParams)
{
+ inParameters[Impl.Name].Add(v.Name);
if (CommandLineOptions.DoUniformityAnalysis)
{
SetUniform(Impl.Name, v.Name);
@@ -66,8 +75,10 @@ namespace GPUVerify }
}
+ outParameters[Impl.Name] = new List<string>();
foreach (Variable v in Impl.OutParams)
{
+ outParameters[Impl.Name].Add(v.Name);
if (CommandLineOptions.DoUniformityAnalysis)
{
SetUniform(Impl.Name, v.Name);
@@ -101,6 +112,24 @@ namespace GPUVerify }
}
+ foreach (Declaration D in verifier.Program.TopLevelDeclarations)
+ {
+ if (D is Implementation)
+ {
+ Implementation Impl = D as Implementation;
+ if (!IsUniform (Impl.Name))
+ {
+ List<string> newIns = new List<String>();
+ newIns.Add("_P");
+ foreach (string s in inParameters[Impl.Name])
+ {
+ newIns.Add(s);
+ }
+ inParameters[Impl.Name] = newIns;
+ }
+ }
+ }
+
if (CommandLineOptions.ShowUniformityAnalysis)
{
dump();
@@ -249,7 +278,15 @@ namespace GPUVerify internal bool IsUniform(string procedureName, string v)
{
- Debug.Assert(uniformityInfo.ContainsKey(procedureName));
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+
+ if (!uniformityInfo[procedureName].Value.ContainsKey(v))
+ {
+ return false;
+ }
return uniformityInfo[procedureName].Value[v];
}
@@ -281,9 +318,47 @@ namespace GPUVerify Console.WriteLine(" " + v + ": " +
(uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
}
+ Console.Write("Ins [");
+ for (int i = 0; i < inParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
+ }
+ Console.WriteLine("]");
+ Console.Write("Outs [");
+ for (int i = 0; i < outParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
+ }
+ Console.WriteLine("]");
}
}
+
+ internal string GetInParameter(string procName, int i)
+ {
+ Console.WriteLine("proc: " + procName + " i " + i);
+ return inParameters[procName][i];
+ }
+
+ internal string GetOutParameter(string procName, int i)
+ {
+ return outParameters[procName][i];
+ }
+
+
+ internal bool knowsOf(string p)
+ {
+ return uniformityInfo.ContainsKey(p);
+ }
+
+ internal void AddNonUniform(string proc, string v)
+ {
+ if (uniformityInfo.ContainsKey(proc))
+ {
+ Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
+ uniformityInfo[proc].Value[v] = false;
+ }
+ }
}
}
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs index add50f08..7f637734 100644 --- a/Source/GPUVerify/VariableDualiser.cs +++ b/Source/GPUVerify/VariableDualiser.cs @@ -11,10 +11,17 @@ namespace GPUVerify class VariableDualiser : Duplicator
{
private int id;
+ private UniformityAnalyser uniformityAnalyser;
+ private string procName;
- public VariableDualiser(int id)
+ public VariableDualiser(int id, UniformityAnalyser uniformityAnalyser, string procName)
{
+ Debug.Assert((uniformityAnalyser == null && procName == null)
+ || (uniformityAnalyser != null && procName != null));
+
this.id = id;
+ this.uniformityAnalyser = uniformityAnalyser;
+ this.procName = procName;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node)
@@ -34,7 +41,13 @@ namespace GPUVerify private TypedIdent DualiseTypedIdent(Variable v)
{
- return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
+
+ if (uniformityAnalyser == null || !uniformityAnalyser.IsUniform(procName, v.Name))
+ {
+ return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
+ }
+
+ return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
}
public override Variable VisitVariable(Variable node)
|