Adding support for annotations written in the OpenCL/CUDA kernels.

4 files changed, 83 insertions, 2 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index b9e9d664..7432c823 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -336,6 +336,13 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_dualised");

             }

 

+            ProcessCrossThreadInvariants();

+

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_cross_thread_invariants");

+            }

+

             if (CommandLineOptions.Eager)

             {

                 AddEagerRaceChecking();

@@ -399,6 +406,35 @@ namespace GPUVerify
 

         }

 

+        private void ProcessCrossThreadInvariants()

+        {

+            foreach (Declaration d in Program.TopLevelDeclarations)

+            {

+                if (d is Procedure)

+                {

+                    // TODO: requires and ensures

+                }

+                if (d is Implementation)

+                {

+                    Implementation i = d as Implementation;

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

+                    foreach (Block b in i.Blocks)

+                    {

+                        Console.WriteLine("Before");

+                        Console.WriteLine(b.Cmds);

+                        Block newBlock = new CrossThreadInvariantProcessor().VisitBlock(b);

+                        Console.WriteLine("After");

+                        Console.WriteLine(newBlock.Cmds);

+

+

+                        newBlocks.Add(newBlock);

+                    }

+                    i.Blocks = newBlocks;

+                }

+

+            }

+        }

+

         private void emitProgram(string filename)

         {

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

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 6956b973..204ffabe 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -105,6 +105,8 @@
   <ItemGroup>

     <Compile Include="AccessCollector.cs" />

     <Compile Include="AccessRecord.cs" />

+    <Compile Include="CrossThreadInvariantProcessor.cs" />

+    <Compile Include="EnabledToPredicateVisitor.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="ElementEncodingraceInstrumenter.cs" />

     <Compile Include="GPUVerifier.cs" />

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index e2af8185..1ade15c9 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -158,7 +158,9 @@ namespace GPUVerify
                 string LoopPredicate = "_LC" + WhileLoopCounter;

                 WhileLoopCounter++;

 

-                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));

+                TypedIdent LoopPredicateTypedIdent = new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool);

+

+                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, LoopPredicateTypedIdent));

                 Expr GuardExpr = (b.ec as WhileCmd).Guard;

 

                 List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();

@@ -169,7 +171,9 @@ namespace GPUVerify
 

                 firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));

 

-                WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));

+                WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, 

+                    ProcessEnabledIntrinsics((b.ec as WhileCmd).Invariants, LoopPredicateTypedIdent), 

+                    MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));

 

                 List<Expr> UpdatePredicateRhss = new List<Expr>();

                 UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));

@@ -242,6 +246,23 @@ namespace GPUVerify
             return result;

         }

 

+        private List<PredicateCmd> ProcessEnabledIntrinsics(List<PredicateCmd> invariants, TypedIdent currentPredicate)

+        {

+            List<PredicateCmd> result = new List<PredicateCmd>();

+

+            foreach (PredicateCmd cmd in invariants)

+            {

+                result.Add(new AssertCmd(cmd.tok, ProcessEnabledIntrinsics(cmd.Expr, currentPredicate)));

+            }

+

+            return result;

+        }

+

+        private Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate)

+        {

+            return new EnabledToPredicateVisitor(currentPredicate).VisitExpr(expr);

+        }

+

 

         private void AddPredicateLocalVariables(Implementation impl)

         {

diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index 5cbfed99..1b1bf46e 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -49,6 +49,28 @@ namespace GPUVerify
             return base.VisitVariable(node);

         }

 

+

+        public override Expr VisitNAryExpr(NAryExpr node)

+        {

+            // The point of this override is to avoid dualisation of certain special

+            // intrinsics that are cross-thread

+

+            if (node.Fun is FunctionCall)

+            {

+                FunctionCall call = node.Fun as FunctionCall;

+

+                if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool") ||

+                    call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))

+                {

+                    return node;

+                }

+

+            }

+

+            return base.VisitNAryExpr(node);

+        }

+

+

     }

 

 }