Some fixes to get GPUVerify close to working with OpenCL.

1 files changed, 44 insertions, 14 deletions

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