Some fixes for race checking contracts

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

-        }

-

     }

 }