Completed basic version of GPUVerify tool

4 files changed, 574 insertions, 36 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 812d9f20..ecbee795 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -14,6 +14,7 @@ namespace GPUVerify
         public static List<string> inputFiles = new List<string>();

 

         public static string outputFile = null;

+        public static string formulaSkeletonsFile = null;

 

         public static int Parse(string[] args)

         {

@@ -44,6 +45,17 @@ namespace GPUVerify
                         outputFile = afterColon;

                     break;

 

+                    case "-generateFormulaSkeletons":

+                    case "/generateFormulaSkeletons":

+                    if (!hasColonArgument)

+                    {

+                        Console.WriteLine("Error: filename expected after " + beforeColon + " argument");

+                        Environment.Exit(1);

+                    }

+                    Debug.Assert(afterColon != null);

+                    formulaSkeletonsFile = afterColon;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index f90e521e..8ea3cdfd 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -4,6 +4,7 @@ using System.Linq;
 using System.Text;

 using System.Diagnostics;

 using Microsoft.Boogie;

+using Microsoft.Basetypes;

 

 namespace GPUVerify

 {

@@ -21,9 +22,9 @@ namespace GPUVerify
 

         private HashSet<int> BarrierIds = new HashSet<int>();

 

-        private HashSet<Variable> ThreadLocalVariables = new HashSet<Variable>();

-        private HashSet<Variable> TileStaticVariables = new HashSet<Variable>();

-        private HashSet<Variable> GloalVariables = new HashSet<Variable>();

+        private List<Variable> ThreadLocalVariables = new List<Variable>();

+        private List<Variable> TileStaticVariables = new List<Variable>();

+        private List<Variable> GlobalVariables = new List<Variable>();

 

 

         public GPUVerifier(Program program)

@@ -36,6 +37,7 @@ namespace GPUVerify
             ReservedNames.Add("offset_x");

             ReservedNames.Add("offset_y");

             ReservedNames.Add("offset_z");

+            ReservedNames.Add("is_write");

             ReservedNames.Add("AT_BARRIER");

 

             CheckWellFormedness();

@@ -88,7 +90,7 @@ namespace GPUVerify
                 {

                     if (!ReservedNames.Contains((D as Variable).Name))

                     {

-                        GloalVariables.Add(D as Variable);

+                        GlobalVariables.Add(D as Variable);

                     }

                 }

             }

@@ -283,17 +285,17 @@ namespace GPUVerify
             return result;

         }

 

-        internal HashSet<Variable> GetGlobalVariables()

+        internal List<Variable> GetGlobalVariables()

         {

-            return GloalVariables;

+            return GlobalVariables;

         }

 

-        internal HashSet<Variable> GetTileStaticVariables()

+        internal List<Variable> GetTileStaticVariables()

         {

             return TileStaticVariables;

         }

 

-        internal HashSet<Variable> GetThreadLocalVariables()

+        internal List<Variable> GetThreadLocalVariables()

         {

             return ThreadLocalVariables;

         }

@@ -510,29 +512,39 @@ namespace GPUVerify
         }

 

 

-        private void ComputeBarrierToNextBarriersProcedure(Block B)

+        private void GenerateBarrierToNextBarriersProcedure(Block B)

         {

             SanityCheckKernel();

             Debug.Assert(IsBarrier(B));

 

-            String NewProcedureName = "Barrier_" + GetBarrierId(B) + "_to_next_barriers";

-            Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);

+            String NewProcedureName = MakeBarrierToNextBarriersProcedureName(B);

+            Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);

 

-            NewProcedure.Modifies.Add(MakeBaseVariable(B.tok));

-            NewProcedure.Modifies.Add(MakeOffsetXVariable(B.tok));

-            NewProcedure.Modifies.Add(MakeOffsetYVariable(B.tok));

-            NewProcedure.Modifies.Add(MakeOffsetZVariable(B.tok));

-            NewProcedure.Modifies.Add(MakeIsWriteVariable(B.tok));

+            AddTrackingVariablesToModifiesSet(B.tok, NewProcedure.Modifies);

+

+            AddInlineAttribute(NewProcedure);

 

             Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);

 

             InstrumentWithRaceDetection(NewImplementation);

 

+            AddBarrierTracking(NewImplementation);

+

             Program.TopLevelDeclarations.Add(NewProcedure);

             Program.TopLevelDeclarations.Add(NewImplementation);

 

         }

 

+        private string MakeBarrierToNextBarriersProcedureName(Block B)

+        {

+            return "Barrier_" + GetBarrierId(B) + "_to_next_barriers";

+        }

+

+        private string MakeBarrierAToBProcedureName(Block A, Block B)

+        {

+            return "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);

+        }

+

         private static CtorType MakeArrayBaseType(IToken tok)

         {

             return new CtorType(tok, new TypeCtorDecl(tok, "ArrayBase", 0), new TypeSeq());

@@ -617,15 +629,24 @@ namespace GPUVerify
             return InParams;

         }

 

-        private void ComputeBarrierAToBarrierBProcedure(Block A, Block B)

+        private void GenerateBarrierAToBarrierBProcedure(Block A, Block B)

         {

             Debug.Assert(IsBarrier(A));

             Debug.Assert(IsBarrier(B));

 

-            String NewProcedureName = "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);

-            Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);

+            if (!BarrierReachesBarrier(A, B))

+            {

+                return;

+            }

+

+            String NewProcedureName = MakeBarrierAToBProcedureName(A, B);

+            Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);

             Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, NewProcedureName);

 

+            AddInlineAttribute(NewProcedure);

+

+            NewProcedure.Modifies.Add(MakeAtBarrierVariable(B.tok));

+

             Block NewA = NewImplementation.Blocks[0];

             Block NewB = null;

             for (int i = 1; i < NewImplementation.Blocks.Count; i++)

@@ -636,11 +657,7 @@ namespace GPUVerify
                     break;

                 }

             }

-            if (NewB == null)

-            {

-                // No path between the barriers -- nothing to do

-                return;

-            }

+            Debug.Assert(NewB != null);

 

             NewImplementation.ComputePredecessorsForBlocks();

 

@@ -668,11 +685,116 @@ namespace GPUVerify
 

             NewImplementation.PruneUnreachableBlocks();

 

+            AddBarrierTracking(NewImplementation);

+

             Program.TopLevelDeclarations.Add(NewProcedure);

             Program.TopLevelDeclarations.Add(NewImplementation);

 

         }

 

+        private bool BarrierReachesBarrier(Block A, Block B)

+        {

+            Debug.Assert(IsBarrier(A));

+            Debug.Assert(IsBarrier(B));

+

+            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, "noname");

+

+            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

+            {

+                if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))

+                {

+                    return true;

+                }

+            }

+

+            return false;

+        }

+

+        private static void AddInlineAttribute(Procedure NewProcedure)

+        {

+            NewProcedure.AddAttribute("inline", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(1)) });

+        }

+

+        private Procedure CloneKernelProcedure(string NewProcedureName)

+        {

+            RequiresSeq NewRequiresSeq = new RequiresSeq();

+            foreach(Requires r in KernelProcedure.Requires)

+            {

+                NewRequiresSeq.Add(r);

+            }

+            EnsuresSeq NewEnsuresSeq = new EnsuresSeq();

+            foreach (Ensures e in KernelProcedure.Ensures)

+            {

+                NewEnsuresSeq.Add(e);

+            }

+            IdentifierExprSeq NewModifiesSeq = new IdentifierExprSeq();

+            foreach (IdentifierExpr ies in KernelProcedure.Modifies)

+            {

+                NewModifiesSeq.Add(ies);

+            }

+            return new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, NewRequiresSeq, NewModifiesSeq, NewEnsuresSeq);

+        }

+

+        private void AddBarrierTracking(Implementation Impl)

+        {

+            Debug.Assert(IsBarrier(Impl.Blocks[0]));

+            CmdSeq NewBlock0Commands = new CmdSeq();

+

+            NewBlock0Commands.Add(Impl.Blocks[0].Cmds[0]);

+

+            NewBlock0Commands.Add(MakeAssignToAtBarrier(Impl.Blocks[0].Cmds[0].tok, -1));

+

+            for (int i = 1; i < Impl.Blocks[0].Cmds.Length; i++)

+            {

+                NewBlock0Commands.Add(Impl.Blocks[0].Cmds[i]);

+            }

+

+            Impl.Blocks[0].Cmds = NewBlock0Commands;

+

+            for (int i = 1; i < Impl.Blocks.Count; i++)

+            {

+                if (IsBarrier(Impl.Blocks[i]))

+                {

+                    // At this stage, the barrier should be followed immediately by a return

+                    Debug.Assert(Impl.Blocks[i].Cmds.Length == 1);

+

+                    Impl.Blocks[i].Cmds.Add(MakeAssignToAtBarrier(Impl.Blocks[i].Cmds[0].tok, GetBarrierId(Impl.Blocks[i])));

+

+                }

+            }

+            

+

+

+

+        }

+

+        private AssignCmd MakeAssignToAtBarrier(IToken tok, int p)

+        {

+            List<AssignLhs> lhss = new List<AssignLhs>();

+            List<Expr> rhss = new List<Expr>();

+

+            List<Expr> indexes = new List<Expr>();

+            indexes.Add(MakeThreadIdExpr(tok, "i"));

+            lhss.Add(new MapAssignLhs(tok, new SimpleAssignLhs(tok, MakeAtBarrierVariable(tok)), indexes));

+            rhss.Add(new LiteralExpr(tok, BigNum.FromInt(p)));

+            return new AssignCmd(tok, lhss, rhss);

+        }

+

+        private NAryExpr MakeAtBarrierAccess(IToken tok, string ThreadIdName)

+        {

+            ExprSeq args = new ExprSeq();

+            args.Add(MakeAtBarrierVariable(tok));

+            args.Add(MakeThreadIdExpr(tok, ThreadIdName));

+            return new NAryExpr(tok, new MapSelect(tok, 1), args);

+        }

+

+        private IdentifierExpr MakeAtBarrierVariable(IToken tok)

+        {

+            TypeSeq IndexType = new TypeSeq();

+            IndexType.Add(ThreadIdType);

+            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "AT_BARRIER", new MapType(tok, new TypeVariableSeq(), IndexType, Microsoft.Boogie.Type.Int))));

+        }

+

         private static HashSet<Block> BlocksReaching(Block B)

         {

             HashSet<Block> Result = new HashSet<Block>();

@@ -843,18 +965,18 @@ namespace GPUVerify
             return KernelImplementation;

         }

 

-        internal void ComputeBarrierToNextBarriersProcedures()

+        internal void GenerateBarrierToNextBarriersProcedures()

         {

             foreach (Block B in KernelImplementation.Blocks)

             {

                 if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))

                 {

-                    ComputeBarrierToNextBarriersProcedure(B);

+                    GenerateBarrierToNextBarriersProcedure(B);

                 }

             }

         }

 

-        internal void ComputeBarrierToBarrierPairs()

+        internal void GenerateBarrierToBarrierPairProcedures()

         {

             foreach (Block A in KernelImplementation.Blocks)

             {

@@ -864,18 +986,22 @@ namespace GPUVerify
                     {

                         if (IsBarrier(B))

                         {

-                            ComputeBarrierAToBarrierBProcedure(A, B);

+                            GenerateBarrierAToBarrierBProcedure(A, B);

                         }

                     }

                 }

             }

         }

 

-        internal IdentifierExpr MakeThreadIdExpr(IToken tok)

+        internal IdentifierExpr MakeThreadIdExpr(IToken tok, string name)

         {

-            return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, ThreadIdParameterName, ThreadIdType)));

+            return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, name, ThreadIdType)));

         }

 

+        internal IdentifierExpr MakeThreadIdExpr(IToken tok)

+        {

+            return MakeThreadIdExpr(tok, ThreadIdParameterName);

+        }

 

 

         internal void AddArrayBaseDeclarations()

@@ -890,6 +1016,342 @@ namespace GPUVerify
                 Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));

             }

         }

+

+        internal void GenerateBarrierToNextBarriersVCs()

+        {

+            foreach (Block B in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))

+                {

+                    GenerateBarrierToNextBarriersVC(B);

+                }

+            }

+        }

+

+        private void GenerateBarrierToNextBarriersVC(Block B)

+        {

+            VariableSeq InParams = new VariableSeq();

+            InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "i", ThreadIdType)));

+            InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "j", ThreadIdType)));

+

+            VariableSeq OutParams = new VariableSeq();

+

+            IdentifierExprSeq Modifies = new IdentifierExprSeq();

+            foreach (IdentifierExpr ie in KernelProcedure.Modifies)

+            {

+                Modifies.Add(ie);

+            }

+

+            AddTrackingVariablesToModifiesSet(B.tok, Modifies);

+

+            RequiresSeq Requires = new RequiresSeq();

+            Requires.Add(new Requires(false, MakePreconditionExpr(B)));

+            AddDistinctSameTile(B.tok, Requires, "i", "j");

+            AddNothingInitiallyTracked(B.tok, Requires, "i", "j");

+

+

+            EnsuresSeq Ensures = new EnsuresSeq();

+            AddNoRace(B.tok, Ensures, "i", "j");

+            AddSameBarrier(B.tok, Ensures, "i", "j");

+

+            string BarrierIsRaceAndDivergenceFree = "Check_Barrier_" + GetBarrierId(B) + "_Race_And_Divergence_Free";

+

+            Procedure NewProcedure = new Procedure(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, Requires, Modifies, Ensures);

+

+            List<Block> Blocks = new List<Block>();

+

+            Blocks.Add(new Block());

+

+            Blocks[0].TransferCmd = new ReturnCmd(B.tok);

+

+            Blocks[0].Label = "entry";

+

+            Blocks[0].Cmds = new CmdSeq();

+

+            ExprSeq i = new ExprSeq();

+            i.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "i", ThreadIdType))));

+            Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), i, new IdentifierExprSeq()));

+

+            ExprSeq j = new ExprSeq();

+            j.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "j", ThreadIdType))));

+            Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), j, new IdentifierExprSeq()));

+

+            Implementation NewImplementation = new Implementation(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, new VariableSeq(), Blocks);

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+

+        }

+

+        private void AddNothingInitiallyTracked(IToken tok, RequiresSeq Requires, string i, string j)

+        {

+            Requires.Add(new Requires(false, Expr.And(BaseEqualsNothing(tok, i), BaseEqualsNothing(tok, j))));

+        }

+

+        private Expr BaseEqualsNothing(IToken tok, string i)

+        {

+            ExprSeq MapSelectArgs = new ExprSeq();

+            MapSelectArgs.Add(MakeBaseVariable(tok));

+            MapSelectArgs.Add(MakeThreadIdExpr(tok, i));

+            return Expr.Eq(new NAryExpr(tok, new MapSelect(tok, 1), MapSelectArgs), new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "nothing", MakeArrayBaseType(tok)))));

+        }

+

+        private void AddSameBarrier(IToken tok, EnsuresSeq Ensures, string i, string j)

+        {

+            ExprSeq args1 = new ExprSeq();

+            args1.Add(MakeAtBarrierVariable(tok));

+            args1.Add(MakeThreadIdExpr(tok, i));

+

+            ExprSeq args2 = new ExprSeq();

+            args2.Add(MakeAtBarrierVariable(tok));

+            args2.Add(MakeThreadIdExpr(tok, j));

+

+            Ensures.Add(new Ensures(false, Expr.Eq( new NAryExpr(tok, new MapSelect(tok, 1), args1), new NAryExpr(tok, new MapSelect(tok, 1), args2) ) ) );

+

+        }

+

+        private void AddNoRace(IToken tok, EnsuresSeq Ensures, string i, string j)

+        {

+            ExprSeq RaceArgs = new ExprSeq();

+            RaceArgs.Add(MakeBaseVariable(tok));

+            RaceArgs.Add(MakeOffsetZVariable(tok));

+            RaceArgs.Add(MakeOffsetYVariable(tok));

+            RaceArgs.Add(MakeOffsetXVariable(tok));

+            RaceArgs.Add(MakeIsWriteVariable(tok));

+            RaceArgs.Add(MakeThreadIdExpr(tok, i));

+            RaceArgs.Add(MakeThreadIdExpr(tok, j));

+

+            NAryExpr RaceExpr = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "race", Microsoft.Boogie.Type.Bool)), RaceArgs);

+            Ensures.Add(new Ensures(false, Expr.Not(RaceExpr)));

+        }

+

+        private void AddDistinctSameTile(IToken tok, RequiresSeq Requires, string i, string j)

+        {

+            ExprSeq args = new ExprSeq();

+            args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, i, ThreadIdType))));

+            args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, j, ThreadIdType))));

+            Requires.Add(new Requires(false, new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "distinct_same_tile", Microsoft.Boogie.Type.Bool)), args)));

+        }

+

+        private NAryExpr MakePreconditionExpr(Block B)

+        {

+            ExprSeq PreconditionArgs = new ExprSeq();

+            foreach (Variable v in MakeFormulaFunctionArguments(B.tok))

+            {

+                PreconditionArgs.Add(new IdentifierExpr(B.tok, v));

+            }

+

+            NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(B.tok, MakePreconditionName(B), Microsoft.Boogie.Type.Bool)), PreconditionArgs);

+            return nary;

+        }

+

+        private void AddTrackingVariablesToModifiesSet(IToken tok, IdentifierExprSeq Modifies)

+        {

+            Modifies.Add(MakeBaseVariable(tok));

+            Modifies.Add(MakeOffsetXVariable(tok));

+            Modifies.Add(MakeOffsetYVariable(tok));

+            Modifies.Add(MakeOffsetZVariable(tok));

+            Modifies.Add(MakeIsWriteVariable(tok));

+            Modifies.Add(MakeAtBarrierVariable(tok));

+        }

+

+        internal void GenerateBarrierToBarrierPairVCs()

+        {

+            foreach (Block A in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(A))

+                {

+                    foreach (Block B in KernelImplementation.Blocks)

+                    {

+                        if (IsBarrier(B) && BarrierReachesBarrier(A, B))

+                        {

+                            GenerateBarrierAToBarrierBVCs(A, B);

+                        }

+                    }

+                }

+            }

+        }

+

+        private void GenerateBarrierAToBarrierBVCs(Block A, Block B)

+        {

+            GenerateVC_AToBPreconditionA(A, B);

+            GenerateVC_AToBInduction(A, B);

+            GenerateVC_AToBPreconditionB(A, B);

+        }

+

+        private ForallExpr MakeAllAtBarrierExpr(Block A)

+        {

+            VariableSeq i = new VariableSeq();

+            i.Add(MakeThreadIdExpr(A.tok, "i").Decl);

+            Expr body = Expr.Eq(MakeAtBarrierAccess(A.tok, "i"), new LiteralExpr(A.tok, BigNum.FromInt(GetBarrierId(A))));

+            ForallExpr forallexpr = new ForallExpr(A.tok, i, body);

+            return forallexpr;

+        }

+

+        private string MakeIHName(Block A, Block B)

+        {

+            return "IH_" + GetBarrierId(A) + "_" + GetBarrierId(B);

+        }

+

+

+        private NAryExpr MakeIHExpr(Block A, Block B)

+        {

+            ExprSeq IHArgs = new ExprSeq();

+            foreach (Variable v in MakeFormulaFunctionArguments(B.tok))

+            {

+                IHArgs.Add(new IdentifierExpr(B.tok, v));

+            }

+

+            NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(A.tok, MakeIHName(A, B), Microsoft.Boogie.Type.Bool)), IHArgs);

+            return nary;

+        }

+

+        private Expr MakeThreadAtBarrierExpr(Block A, string p)

+        {

+            return Expr.Eq(MakeAtBarrierAccess(A.tok, "i"), new LiteralExpr(A.tok, BigNum.FromInt(GetBarrierId(A))));

+        }

+

+        private void GenerateVC_AToBPreconditionA(Block A, Block B)

+        {

+            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Precondition_" + GetBarrierId(A);

+

+            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            NewProcedure.Requires.Add(new Requires(false, MakePreconditionExpr(A)));

+            NewProcedure.Requires.Add(new Requires(false, MakeAllAtBarrierExpr(A)));

+            NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));

+

+            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+        }

+

+        private void GenerateVC_AToBInduction(Block A, Block B)

+        {

+            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Induction";

+

+            VariableSeq InParams = new VariableSeq();

+            InParams.Add(MakeThreadIdExpr(A.tok).Decl);

+

+            IdentifierExprSeq Modifies = new IdentifierExprSeq();

+            foreach (IdentifierExpr ie in KernelProcedure.Modifies)

+            {

+                Modifies.Add(ie);

+            }

+

+            AddTrackingVariablesToModifiesSet(A.tok, Modifies);

+

+            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new RequiresSeq(), Modifies, new EnsuresSeq());

+            NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));

+            NewProcedure.Requires.Add(new Requires(false, MakeThreadAtBarrierExpr(A, "i")));

+            NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));

+

+            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new VariableSeq(), new List<Block>());

+            NewImplementation.Blocks.Add(new Block());

+            NewImplementation.Blocks[0].Label = "entry";

+            NewImplementation.Blocks[0].TransferCmd = new ReturnCmd(A.tok);

+            NewImplementation.Blocks[0].Cmds = new CmdSeq();

+            ExprSeq i = new ExprSeq();

+            i.Add(MakeThreadIdExpr(A.tok));

+            NewImplementation.Blocks[0].Cmds.Add(new CallCmd(A.tok, MakeBarrierAToBProcedureName(A, B), i, new IdentifierExprSeq()));

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+        }

+

+        private void GenerateVC_AToBPreconditionB(Block A, Block B)

+        {

+            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Precondition_" + GetBarrierId(B);

+

+            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));

+            NewProcedure.Requires.Add(new Requires(false, MakeAllAtBarrierExpr(B)));

+            NewProcedure.Ensures.Add(new Ensures(false, MakePreconditionExpr(B)));

+

+            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+

+        }

+

+        internal void GenerateFormulaSkeletons(string filename)

+        {

+            Program FormulaSkeletons = new Program();

+

+            foreach (Block B in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(B))

+                {

+                    FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakePreconditionName(B)));

+                }

+            }

+

+            foreach (Block A in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(A))

+                {

+                    foreach (Block B in KernelImplementation.Blocks)

+                    {

+                        if (IsBarrier(B) && BarrierReachesBarrier(A, B))

+                        {

+                            FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakeIHName(A, B)));

+                        }

+                    }

+                }

+            }

+

+            using (TokenTextWriter writer = new TokenTextWriter(filename))

+            {

+                FormulaSkeletons.Emit(writer);

+            }

+

+

+        }

+

+        private string MakePreconditionName(Block B)

+        {

+            return "Pre_" + GetBarrierId(B);

+        }

+

+        private Function MakeSkeletonFormula(Block B, string FunctionName)

+        {

+

+            Function precondition = new Function(B.tok, FunctionName, MakeFormulaFunctionArguments(B.tok), MakeFunctionReturnTemp(B.tok));

+

+            precondition.AddAttribute("inline", new object[] { });

+

+            precondition.Body = new LiteralExpr(B.tok, true);

+            return precondition;

+        }

+

+        private Variable MakeFunctionReturnTemp(IToken tok)

+        {

+            return new LocalVariable(tok, new TypedIdent(tok, "result", Microsoft.Boogie.Type.Bool));

+        }

+

+        private VariableSeq MakeFormulaFunctionArguments(IToken tok)

+        {

+            VariableSeq arguments = new VariableSeq();

+

+            foreach (Variable v in ThreadLocalVariables)

+            {

+                arguments.Add(v);

+            }

+

+            foreach (Variable v in TileStaticVariables)

+            {

+                arguments.Add(v);

+            }

+

+            foreach (Variable v in GlobalVariables)

+            {

+                arguments.Add(v);

+            }

+

+            arguments.Add(MakeAtBarrierVariable(tok).Decl);

+            return arguments;

+        }

     }

 

 }

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index a0576f45..90524bb1 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -67,9 +67,21 @@ namespace GPUVerify
 

             verifier.SplitBlocksAtBarriers();

 

-            verifier.ComputeBarrierToNextBarriersProcedures();

 

-            verifier.ComputeBarrierToBarrierPairs();

+            if (CommandLineOptions.formulaSkeletonsFile != null)

+            {

+                Console.WriteLine("Generating skeleton formulas to \"" + CommandLineOptions.formulaSkeletonsFile + "\" and exiting");

+                verifier.GenerateFormulaSkeletons(CommandLineOptions.formulaSkeletonsFile);

+                Environment.Exit(0);

+            }

+

+            verifier.GenerateBarrierToNextBarriersProcedures();

+

+            verifier.GenerateBarrierToBarrierPairProcedures();

+

+            verifier.GenerateBarrierToNextBarriersVCs();

+

+            verifier.GenerateBarrierToBarrierPairVCs();

 

             verifier.AddArrayBaseDeclarations();

 

diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
index dda5ddcf..d81c0fc1 100644
--- a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
+++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
@@ -1,9 +1,61 @@
-echo off

+@ECHO OFF

 

-Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl

+set InputFile=""

+set SkeletonFile=""

 

+set ScriptDir=%~p0

+

+:Loop

+IF "%1"=="" GOTO Continue

+

+set temp=%1

+

+IF %temp:~0,26%==/generateFormulaSkeletons: GOTO SetSkeletonFile

+

+set InputFile=%1

+

+GOTO LastPartOfLoop

+

+:SetSkeletonFile

+

+set SkeletonFile=%temp:~26%

+

+:LastPartOfLoop

+

+SHIFT

+GOTO Loop

+:Continue

+

+IF %InputFile%=="" GOTO Error

+

+echo Preprocess

+Boogie /noVerify /printUnstructured /print:temp_unstructured.bpl %InputFile% %ScriptDir%..\BoogieLibrary\GPUVerifyLibrary.bpl

+

+IF %SkeletonFile%=="" GOTO Verify

+

+GOTO Generate

+

+

+

+

+:Verify

+echo Verify

 GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl

+Boogie temp_ready_to_verify.bpl formulas.bpl /prover:smtlib

+del temp_unstructured.bpl

+GOTO End

+

+:Generate

+echo Generate

+GPUVerify temp_unstructured.bpl /generateFormulaSkeletons:%SkeletonFile%

+del temp_unstructured.bpl

+GOTO End

+

+:Error

+echo Error: Bad command line specified for GPUVerify

+GOTO End

+

+

 

-Boogie temp_ready_to_verify.bpl /prover:smtlib

 

-del temp_instrumented.bpl

+:End
\ No newline at end of file