Some more code cleanup related to removal of the "divided" option.

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);

 

-              }

             }

           }

         }