diff options
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 23 | ||||
| -rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 52 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 1 | ||||
| -rw-r--r-- | Source/GPUVerify/LoopInvariantGenerator.cs | 7 | ||||
| -rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 2 |
6 files changed, 62 insertions, 25 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 59d2fd89..ae6b03a2 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -16,7 +16,8 @@ namespace GPUVerify public static string outputFile = null;
public static bool OnlyDivergence = false;
- public static bool FullAbstraction = false;
+ public static bool AdversarialAbstraction = false;
+ public static bool EqualityAbstraction = false;
public static bool Inference = false;
public static bool ArrayEqualities = false;
public static string invariantsFile = null;
@@ -39,6 +40,7 @@ namespace GPUVerify public static bool ShowMayBeTidAnalysis = false;
public static bool ShowMayBePowerOfTwoAnalysis = false;
public static bool ShowMayBeTidPlusConstantAnalysis = false;
+ public static bool ShowArrayControlFlowAnalysis = false;
public static int Parse(string[] args)
{
@@ -81,9 +83,15 @@ namespace GPUVerify break;
- case "-fullAbstraction":
- case "/fullAbstraction":
- FullAbstraction = true;
+ case "-adversarialAbstraction":
+ case "/adversarialAbstraction":
+ AdversarialAbstraction = true;
+
+ break;
+
+ case "-equalityAbstraction":
+ case "/equalityAbstraction":
+ EqualityAbstraction = true;
break;
@@ -175,6 +183,11 @@ namespace GPUVerify ShowMayBeTidPlusConstantAnalysis = true;
break;
+ case "-showArrayControlFlowAnalysis":
+ case "/showArrayControlFlowAnalysis":
+ ShowArrayControlFlowAnalysis = true;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
@@ -204,7 +217,7 @@ namespace GPUVerify where <option> is one of
/help : this message
- /fullAbstraction : apply full state abstraction
+ /adversarialAbstraction : apply full state abstraction
/onlyDivergence : only check for divergence-freedom, not race-freedom
/symmetry : apply symmetry breaking
/eager : check races eagerly, rather than waiting for barrier
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 91b1edb6..430378c9 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -235,7 +235,7 @@ namespace GPUVerify ));
}
- if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !CommandLineOptions.FullAbstraction)
+ if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))
{
RaceCondition = Expr.And(RaceCondition, Expr.Neq(
MakeWrittenIndex(v, 1),
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 078c3d10..03a9f647 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -68,6 +68,7 @@ namespace GPUVerify public MayBeTidPlusConstantAnalyser mayBeTidPlusConstantAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
public LiveVariableAnalyser liveVariableAnalyser;
+ public ArrayControlFlowAnalyser arrayControlFlowAnalyser;
public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)
{
@@ -453,7 +454,8 @@ namespace GPUVerify private void DoArrayControlFlowAnalysis()
{
- // TODO
+ arrayControlFlowAnalyser = new ArrayControlFlowAnalyser(this);
+ arrayControlFlowAnalyser.Analyse();
}
private void DoUniformityAnalysis()
@@ -1321,7 +1323,7 @@ namespace GPUVerify checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));
- if (!CommandLineOptions.OnlyDivergence || !CommandLineOptions.FullAbstraction)
+ if (!CommandLineOptions.OnlyDivergence)
{
List<BigBlock> returnbigblocks = new List<BigBlock>();
returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));
@@ -1334,15 +1336,14 @@ namespace GPUVerify bigblocks.Add(RaceInstrumenter.MakeRaceCheckingStatements(tok));
- if (!CommandLineOptions.FullAbstraction)
+ BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
+ bigblocks.Add(havocSharedState);
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
- BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
- bigblocks.Add(havocSharedState);
- foreach (Variable v in NonLocalState.getAllNonLocalVariables())
+ if (!ArrayModelledAdversarially(v))
{
HavocAndAssumeEquality(tok, havocSharedState, v);
}
-
}
StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
@@ -1411,16 +1412,11 @@ namespace GPUVerify private void AbstractSharedState()
{
- if (!CommandLineOptions.FullAbstraction)
- {
- return; // There's actually nothing to do here
- }
-
List<Declaration> NewTopLevelDeclarations = new List<Declaration>();
foreach (Declaration d in Program.TopLevelDeclarations)
{
- if (d is Variable && NonLocalState.Contains(d as Variable))
+ if (d is Variable && NonLocalState.Contains(d as Variable) && ArrayModelledAdversarially(d as Variable))
{
continue;
}
@@ -1449,7 +1445,7 @@ namespace GPUVerify foreach (IdentifierExpr e in proc.Modifies)
{
- if (!NonLocalState.Contains(e.Decl))
+ if (!NonLocalState.Contains(e.Decl) || !ArrayModelledAdversarially(e.Decl))
{
NewModifies.Add(e);
}
@@ -1504,7 +1500,18 @@ namespace GPUVerify Expr rhs = assign.Rhss[0];
ReadCollector rc = new ReadCollector(NonLocalState);
rc.Visit(rhs);
- if (rc.accesses.Count > 0)
+
+ bool foundAdversarial = false;
+ foreach (AccessRecord ar in rc.accesses)
+ {
+ if (ArrayModelledAdversarially(ar.v))
+ {
+ foundAdversarial = true;
+ break;
+ }
+ }
+
+ if (foundAdversarial)
{
Debug.Assert(lhs is SimpleAssignLhs);
result.simpleCmds.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
@@ -1513,7 +1520,7 @@ namespace GPUVerify WriteCollector wc = new WriteCollector(NonLocalState);
wc.Visit(lhs);
- if (wc.GetAccess() != null)
+ if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
{
continue; // Just remove the write
}
@@ -2200,5 +2207,18 @@ namespace GPUVerify }
+
+ internal bool ArrayModelledAdversarially(Variable v)
+ {
+ if (CommandLineOptions.AdversarialAbstraction)
+ {
+ return true;
+ }
+ if (CommandLineOptions.EqualityAbstraction)
+ {
+ return false;
+ }
+ return !arrayControlFlowAnalyser.MayAffectControlFlow(v.Name);
+ }
}
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 1109ebb7..91800a70 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -106,6 +106,7 @@ <Compile Include="AccessCollector.cs" />
<Compile Include="AccessInvariantProcessor.cs" />
<Compile Include="AccessRecord.cs" />
+ <Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="KernelDualiser.cs" />
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs index 732b24fa..7dafe20c 100644 --- a/Source/GPUVerify/LoopInvariantGenerator.cs +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -123,11 +123,14 @@ namespace GPUVerify }
}
- if (!CommandLineOptions.FullAbstraction && CommandLineOptions.ArrayEqualities)
+ if (CommandLineOptions.ArrayEqualities)
{
foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())
{
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ if (!verifier.ArrayModelledAdversarially(v))
+ {
+ AddEqualityCandidateInvariant(wc, LoopPredicate, v);
+ }
}
}
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index bda8f01f..2942bc01 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -280,7 +280,7 @@ namespace GPUVerify Expr AssertExpr = Expr.And(SetExpr1, SetExpr2);
- if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !CommandLineOptions.FullAbstraction)
+ if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))
{
VariableSeq DummyVarsAccess1;
VariableSeq DummyVarsAccess2;
|