summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/GPUVerify/CommandLineOptions.cs23
-rw-r--r--Source/GPUVerify/ElementEncodingRaceInstrumenter.cs2
-rw-r--r--Source/GPUVerify/GPUVerifier.cs52
-rw-r--r--Source/GPUVerify/GPUVerify.csproj1
-rw-r--r--Source/GPUVerify/LoopInvariantGenerator.cs7
-rw-r--r--Source/GPUVerify/SetEncodingRaceInstrumenter.cs2
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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 00:59:37 +0000