From 5438a42e68bde8ef0b860d28af25acb33c9532e3 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 13 Aug 2012 17:38:01 +0100 Subject: Some more code cleanup related to removal of the "divided" option. --- Source/GPUVerify/GPUVerifier.cs | 5 +- Source/GPUVerify/IRaceInstrumenter.cs | 7 +- Source/GPUVerify/Main.cs | 3 +- Source/GPUVerify/NullRaceInstrumenter.cs | 4 +- Source/GPUVerify/RaceInstrumenter.cs | 114 ++++++++----------------------- 5 files changed, 35 insertions(+), 98 deletions(-) (limited to 'Source') 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 logAccessProcedures = new Dictionary(); - 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); - } } } } -- cgit v1.2.3