Some fixes to get GPUVerify close to working with OpenCL.

4 files changed, 58 insertions, 15 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 99cc4b97..f2842d8f 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -27,6 +27,8 @@ namespace GPUVerify
         public static bool Symmetry = false;

         public static bool SetEncoding = false;

 

+        public static bool ShowStages = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -111,6 +113,11 @@ namespace GPUVerify
                     Eager = true;

                     break;

 

+                    case "-showStages":

+                    case "/showStages":

+                    ShowStages = true;

+                    break;

+

                     case "-inference":

                     case "/inference":

                     Inference = true;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index f1d06590..def58982 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -12,7 +12,7 @@ namespace GPUVerify
 {

     class GPUVerifier : CheckingContext

     {

-        public string ouputFilename;

+        public string outputFilename;

         public Program Program;

 

         public Procedure KernelProcedure;

@@ -70,7 +70,7 @@ namespace GPUVerify
         public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter, bool skipCheck)

             : base((IErrorSink)null)

         {

-            this.ouputFilename = filename;

+            this.outputFilename = filename;

             this.Program = program;

             this.RaceInstrumenter = raceInstrumenter;

             if(!skipCheck)

@@ -314,17 +314,42 @@ namespace GPUVerify
 

             preProcess();

 

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_preprocessed");

+            }

+

             if (RaceInstrumenter.AddRaceCheckingInstrumentation() == false)

             {

                 return;

             }

 

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_instrumented");

+            }

+

             AbstractSharedState();

 

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_abstracted");

+            }

+

             MakeKernelPredicated();

 

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_predicated");

+            }

+

             MakeKernelDualised();

 

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_dualised");

+            }

+

             if (CommandLineOptions.Eager)

             {

                 AddEagerRaceChecking();

@@ -334,22 +359,23 @@ namespace GPUVerify
 

             GenerateKernelPrecondition();

 

-            if (CommandLineOptions.Inference)

+            if (CommandLineOptions.ShowStages)

             {

-                ComputeInvariant();

+                emitProgram(outputFilename + "_ready_to_verify");

             }

-            

 

-            using (TokenTextWriter writer = new TokenTextWriter(ouputFilename + ".bpl"))

+            if (CommandLineOptions.Inference)

             {

-                Program.Emit(writer);

+                ComputeInvariant();

             }

 

+            emitProgram(outputFilename);

+

 

             if (CommandLineOptions.DividedAccesses)

             {

 

-                Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { ouputFilename + ".bpl" }), true);

+                Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { outputFilename + ".bpl" }), true);

                 p.Resolve();

                 p.Typecheck();

 

@@ -370,7 +396,7 @@ namespace GPUVerify
                 Contract.Assert(opt.NumLogCalls() <= 2);

                 if (opt.NumLogCalls() == 2 && !opt.HasConflicting())

                 {

-                    FileInfo f = new FileInfo(ouputFilename);

+                    FileInfo f = new FileInfo(outputFilename);

                     

                     string newName = f.Directory.FullName + "\\" + "NO_CONFLICTS_" + f.Name + ".bpl";

                     //File.Delete(newName);

@@ -378,7 +404,7 @@ namespace GPUVerify
                     {

                         File.Delete(newName);

                     }

-                    File.Move(ouputFilename + ".bpl", newName);

+                    File.Move(outputFilename + ".bpl", newName);

                     //Console.WriteLine("Renamed " + ouputFilename + "; no conflicting accesses (that are not already tested by other output files).");

                 }

 

@@ -387,6 +413,14 @@ namespace GPUVerify
 

         }

 

+        private void emitProgram(string filename)

+        {

+            using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl"))

+            {

+                Program.Emit(writer);

+            }

+        }

+

         private void AddEagerRaceChecking()

         {

             foreach(Variable v in NonLocalState.getAllNonLocalVariables())

@@ -2149,10 +2183,6 @@ namespace GPUVerify
 

         private void CheckKernelParameters()

         {

-            if (KernelProcedure.InParams.Length != 0)

-            {

-                Error(KernelProcedure.tok, "Kernel should not take any parameters");

-            }

             if (KernelProcedure.OutParams.Length != 0)

             {

                 Error(KernelProcedure.tok, "Kernel should not take return anything");

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 1be30dc9..cf1aaf70 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -58,13 +58,15 @@ namespace GPUVerify
                 Environment.Exit(1);

             }

 

+            Microsoft.Boogie.CommandLineOptions.Clo.DoModSetAnalysis = true;

+

             int errorCount = program.Resolve();

             if (errorCount != 0)

             {

                 Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

                 Environment.Exit(1);

             }

-

+            

             errorCount = program.Typecheck();

 

             if (errorCount != 0)

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index cca89b52..a4174cbb 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -139,6 +139,10 @@ namespace GPUVerify
                     firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));

 

                 }

+                else if (c is AssertCmd)

+                {

+                    firstBigBlock.simpleCmds.Add(new AssertCmd(c.tok, Expr.Imp(IncomingPredicate, (c as AssertCmd).Expr)));

+                }

                 else

                 {

                     Debug.Assert(false);