From c29422d07a638a502b8529dbe9c53667266ff781 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 9 Dec 2011 20:12:41 +0000 Subject: Some fixes to get GPUVerify close to working with OpenCL. --- Source/GPUVerify/CommandLineOptions.cs | 7 ++++ Source/GPUVerify/GPUVerifier.cs | 58 ++++++++++++++++++++++++++-------- Source/GPUVerify/Main.cs | 4 ++- Source/GPUVerify/Predicator.cs | 4 +++ 4 files changed, 58 insertions(+), 15 deletions(-) (limited to 'Source/GPUVerify') 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(new string[] { ouputFilename + ".bpl" }), true); + Program p = GPUVerify.ParseBoogieProgram(new List(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); -- cgit v1.2.3