Merge

6 files changed, 76 insertions, 47 deletions

diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln
index 4fb930ef..a78d449e 100644
--- a/Source/GPUVerify.sln
+++ b/Source/GPUVerify.sln
@@ -53,26 +53,28 @@ Global
 		z3apidebug|x86 = z3apidebug|x86

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

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/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 7023a2b3..6956b973 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -61,6 +61,37 @@
     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'">

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <Optimize>true</Optimize>

+    <DebugType>pdbonly</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

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

-        }

-

     }

 }