diff options
author | 2011-11-15 16:56:43 +0000 | |
---|---|---|
committer | 2011-11-15 16:56:43 +0000 | |
commit | 8e1a19a4fc73dcde12f0d20d3f40fc5fb0146425 (patch) | |
tree | 6b86ca1c6cc9b027252bf9097264f902874ec090 | |
parent | e1d66ac9026c503d3723895faacdcb5bc68ed520 (diff) |
Some fixes for race checking contracts
-rw-r--r-- | Source/GPUVerify/ElementEncodingRaceInstrumenter.cs | 24 | ||||
-rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 4 | ||||
-rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 26 | ||||
-rw-r--r-- | Source/GPUVerify/SetEncodingRaceInstrumenter.cs | 16 |
4 files changed, 33 insertions, 37 deletions
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 74bdaa5e..b17ca60f 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -261,7 +261,7 @@ namespace GPUVerify verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
}
- private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
+ protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
{
Variable ReadOrWriteHasOccurred = ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
@@ -355,22 +355,12 @@ namespace GPUVerify AddReadOrWrittenZOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);
}
- protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
- protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
private void AddReadOrWrittenXOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
{
Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -379,7 +369,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -388,7 +378,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -397,7 +387,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
@@ -406,7 +396,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
@@ -415,7 +405,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 25974225..36881f88 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -597,7 +597,7 @@ namespace GPUVerify - private void AddCandidateRequires(Procedure Proc, Expr e)
+ internal void AddCandidateRequires(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
@@ -605,7 +605,7 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
- private void AddCandidateEnsures(Procedure Proc, Expr e)
+ internal void AddCandidateEnsures(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 0f5f8278..237c155e 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -81,10 +81,6 @@ namespace GPUVerify protected abstract void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo);
- protected abstract void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
-
- protected abstract void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
-
public void AddRaceCheckingCandidateInvariants(WhileCmd wc)
{
foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
@@ -154,7 +150,13 @@ namespace GPUVerify failedToFindSecondAccess = false;
}
- AddRaceCheckCalls(verifier.KernelImplementation);
+ foreach (Declaration d in verifier.Program.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ AddRaceCheckCalls(d as Implementation);
+ }
+ }
if (failedToFindSecondAccess || !addedLogWrite)
return false;
@@ -447,5 +449,19 @@ namespace GPUVerify }
}
+ private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);
+
+
+
}
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index 3b1f877e..b3104609 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -567,7 +567,7 @@ namespace GPUVerify verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
}
- private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
+ protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
{
int OneOrTwo = Int32.Parse(OneOrTwoString);
Expr expr = null;
@@ -756,7 +756,7 @@ namespace GPUVerify if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -766,19 +766,9 @@ namespace GPUVerify if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
- protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
- protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
}
}
|