Unstructured and smart predication are now default options for GPUVerify.

The executable produced by building the project is now GPUVerifyVCGen.
Refactored the way "other" functions are handled to make this more easily
extensible.

3 files changed, 13 insertions, 10 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 85d559d0..f28535c2 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -35,8 +35,8 @@ namespace GPUVerify
 

         public static bool NoLoopPredicateInvariants = false;

 

-        public static bool Unstructured = false;

-        public static bool SmartPredication = false;

+        public static bool Unstructured = true;

+        public static bool SmartPredication = true;

 

         public static bool OnlyIntraGroupRaceChecking = false;

 

@@ -161,14 +161,14 @@ namespace GPUVerify
                     NoLoopPredicateInvariants = true;

                     break;

 

-                    case "-unstructured":

-                    case "/unstructured":

-                    Unstructured = true;

+                    case "-structured":

+                    case "/structured":

+                    Unstructured = false;

                     break;

 

-                    case "-smartPredication":

-                    case "/smartPredication":

-                    SmartPredication = true;

+                    case "-noSmartPredication":

+                    case "/noSmartPredication":

+                    SmartPredication = false;

                     break;

 

                     case "-onlyIntraGroupRaceChecking":

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 342c0539..4cb24f2c 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -9,7 +9,7 @@
     <OutputType>Exe</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>GPUVerify</RootNamespace>

-    <AssemblyName>GPUVerify</AssemblyName>

+    <AssemblyName>GPUVerifyVCGen</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <FileAlignment>512</FileAlignment>

diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index 6e375945..110e6a17 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -10,6 +10,9 @@ namespace GPUVerify
 {

     class VariableDualiser : Duplicator

     {

+      static HashSet<string> otherFunctionNames =

+        new HashSet<string>(new string[] { "__other_bool", "__other_bv32", "__other_arrayId" });

+

         private int id;

         private UniformityAnalyser uniformityAnalyser;

         private string procName;

@@ -78,7 +81,7 @@ namespace GPUVerify
             {

                 FunctionCall call = node.Fun as FunctionCall;

 

-                if (call.Func.Name.Equals("__other_bool") || call.Func.Name.Equals("__other_bv32"))

+                if (otherFunctionNames.Contains(call.Func.Name))

                 {

                     Debug.Assert(id == 1 || id == 2);

                     int otherId = id == 1 ? 2 : 1;