summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/GPUVerify/GPUVerifier.cs5
-rw-r--r--Source/GPUVerify/IRaceInstrumenter.cs7
-rw-r--r--Source/GPUVerify/Main.cs3
-rw-r--r--Source/GPUVerify/NullRaceInstrumenter.cs4
-rw-r--r--Source/GPUVerify/RaceInstrumenter.cs114
5 files changed, 35 insertions, 98 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 9fad81f9..e07111e9 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -387,10 +387,7 @@ namespace GPUVerify
}
}
- if (RaceInstrumenter.AddRaceCheckingInstrumentation() == false)
- {
- return;
- }
+ RaceInstrumenter.AddRaceCheckingInstrumentation();
if (CommandLineOptions.ShowStages)
{
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index 63b1ea1a..5e5cca5c 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -11,12 +11,7 @@ namespace GPUVerify
void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region);
void AddKernelPrecondition();
- // Summary:
- // Returns whether we should continue.
- // E.g. if race checking code could not be added because
- // the specified accesses to check were read/read or did not exist,
- // this will return false.
- bool AddRaceCheckingInstrumentation();
+ void AddRaceCheckingInstrumentation();
void AddRaceCheckingDeclarations();
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index c6600d61..b11dfc6f 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -88,7 +88,7 @@ namespace GPUVerify
return null;
}
- public static bool doit(string filename, Variable v, int a1, int a2)
+/* public static bool doit(string filename, Variable v, int a1, int a2)
{
ResolutionContext rc;
Program newProgram = parse(out rc);
@@ -121,6 +121,7 @@ namespace GPUVerify
return !ri.failedToFindSecondAccess;
}
+ */
public static void parseProcessOutput()
{
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index acba7ca6..458481a0 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -19,9 +19,9 @@ namespace GPUVerify
}
- public bool AddRaceCheckingInstrumentation()
+ public void AddRaceCheckingInstrumentation()
{
- return true;
+
}
public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index 6d76c65e..d3032783 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -13,22 +13,8 @@ namespace GPUVerify {
public IKernelArrayInfo NonLocalStateToCheck;
- public int onlyLog1;
- public int onlyLog2;
- public bool failedToFindSecondAccess;
- public bool addedLogWrite;
- private int logAddCount;
-
private Dictionary<string, Procedure> logAccessProcedures = new Dictionary<string, Procedure>();
- public RaceInstrumenter() {
- onlyLog1 = -1;
- onlyLog2 = -1;
- failedToFindSecondAccess = false;
- addedLogWrite = false;
- logAddCount = 0;
- }
-
public void setVerifier(GPUVerifier verifier) {
this.verifier = verifier;
NonLocalStateToCheck = new KernelArrayInfoLists();
@@ -295,16 +281,7 @@ namespace GPUVerify {
}
}
- public bool AddRaceCheckingInstrumentation() {
-
- if (onlyLog1 != -1) {
- addedLogWrite = false;
- failedToFindSecondAccess = true;
- }
- else {
- addedLogWrite = true;
- failedToFindSecondAccess = false;
- }
+ public void AddRaceCheckingInstrumentation() {
foreach (Declaration d in verifier.Program.TopLevelDeclarations) {
if (d is Implementation) {
@@ -312,11 +289,6 @@ namespace GPUVerify {
}
}
- if (failedToFindSecondAccess || !addedLogWrite)
- return false;
-
- return true;
-
}
private void AddRaceCheckingDecsAndProcsForVar(Variable v) {
@@ -350,27 +322,6 @@ namespace GPUVerify {
impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
}
- private bool shouldAddLogCallAndIncr() {
- Contract.Assert(onlyLog1 >= -1);
- int oldLogAddCount = logAddCount;
- ++logAddCount;
-
- if (onlyLog1 == -1) {
- return true;
- }
-
- if (onlyLog1 + onlyLog2 == oldLogAddCount) {
- failedToFindSecondAccess = false;
- return true;
- }
-
- if (onlyLog1 == oldLogAddCount) {
- return true;
- }
-
- return false;
- }
-
private CmdSeq AddRaceCheckCalls(CmdSeq cs) {
var result = new CmdSeq();
foreach (Cmd c in cs) {
@@ -383,28 +334,26 @@ namespace GPUVerify {
rc.Visit(rhs);
if (rc.accesses.Count > 0) {
foreach (AccessRecord ar in rc.accesses) {
- if (shouldAddLogCallAndIncr()) {
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null) {
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null) {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null) {
- inParams.Add(ar.IndexX);
- }
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null) {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null) {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null) {
+ inParams.Add(ar.IndexX);
+ }
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
- logAccessCallCmd.Proc = logProcedure;
+ logAccessCallCmd.Proc = logProcedure;
- result.Add(logAccessCallCmd);
+ result.Add(logAccessCallCmd);
- }
}
}
@@ -414,30 +363,25 @@ namespace GPUVerify {
if (wc.GetAccess() != null) {
AccessRecord ar = wc.GetAccess();
- if (shouldAddLogCallAndIncr()) {
-
- ExprSeq inParams = new ExprSeq();
- if (ar.IndexZ != null) {
- inParams.Add(ar.IndexZ);
- }
- if (ar.IndexY != null) {
- inParams.Add(ar.IndexY);
- }
- if (ar.IndexX != null) {
- inParams.Add(ar.IndexX);
- }
-
- Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
+ ExprSeq inParams = new ExprSeq();
+ if (ar.IndexZ != null) {
+ inParams.Add(ar.IndexZ);
+ }
+ if (ar.IndexY != null) {
+ inParams.Add(ar.IndexY);
+ }
+ if (ar.IndexX != null) {
+ inParams.Add(ar.IndexX);
+ }
- CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
+ Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);
- logAccessCallCmd.Proc = logProcedure;
+ CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());
- result.Add(logAccessCallCmd);
+ logAccessCallCmd.Proc = logProcedure;
- addedLogWrite = true;
+ result.Add(logAccessCallCmd);
- }
}
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:09:13 +0000