From 91acbf1e099bd3508f99ff5ec1b3bf4f6cd3050f Mon Sep 17 00:00:00 2001
From: Unknown <afd@afd-THINK.home>
Date: Tue, 28 Feb 2012 12:38:38 +0000
Subject: Added support for invariants in GPUVerify input.

---
 Source/GPUVerify/GPUVerifier.cs | 121 +++++++++++++++++++++-------------------
 1 file changed, 63 insertions(+), 58 deletions(-)

(limited to 'Source/GPUVerify/GPUVerifier.cs')

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 2f9be79b..52d55585 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -2138,7 +2138,11 @@ namespace GPUVerify
 
             if (bb.ec is WhileCmd)
             {
-                result.ec = new WhileCmd(bb.ec.tok, Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)), (bb.ec as WhileCmd).Invariants, MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
+                result.ec = new WhileCmd(bb.ec.tok, 
+                    Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), 
+                            new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)
+                    ),
+                    MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
             }
             else
             {
@@ -2149,6 +2153,18 @@ namespace GPUVerify
 
         }
 
+        private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
+        {
+            List<PredicateCmd> result = new List<PredicateCmd>();
+            foreach(PredicateCmd p in originalInvariants)
+            {
+                result.Add(new AssertCmd(p.tok, new VariableDualiser(1).VisitExpr(p.Expr.Clone() as Expr)));
+                result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr)));
+            }
+
+            return result;
+        }
+
         private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
         {
             VariableSeq NewLocalVars = new VariableSeq();
@@ -2222,83 +2238,72 @@ namespace GPUVerify
                 MissingKernelAttributeError("Kernel", GROUP_ID_X_STRING);
             }
 
-            if (KernelHasIdY() || KernelHasGroupSizeY() || KernelHasNumGroupsY() || KernelHasGroupIdY())
+            if (!KernelHasIdY())
             {
-
-                if (!KernelHasIdY())
-                {
-                    MissingKernelAttributeError("2D kernel", LOCAL_ID_Y_STRING);
-                }
-
-                if (!KernelHasGroupSizeY())
-                {
-                    MissingKernelAttributeError("2D kernel", GROUP_SIZE_Y_STRING);
-                }
-
-                if (!KernelHasNumGroupsY())
-                {
-                    MissingKernelAttributeError("2D kernel", NUM_GROUPS_Y_STRING);
-                }
-
-                if (!KernelHasGroupIdY())
-                {
-                    MissingKernelAttributeError("2D kernel", GROUP_ID_Y_STRING);
-                }
-
+                MissingKernelAttributeError("Kernel", LOCAL_ID_Y_STRING);
             }
 
-            if (KernelHasIdZ() || KernelHasGroupSizeZ() || KernelHasNumGroupsZ() || KernelHasGroupIdZ())
+            if (!KernelHasGroupSizeY())
             {
+                MissingKernelAttributeError("2D kernel", GROUP_SIZE_Y_STRING);
+            }
 
-                if (!KernelHasIdY())
-                {
-                    MissingKernelAttributeError("3D kernel", LOCAL_ID_Y_STRING);
-                }
+            if (!KernelHasNumGroupsY())
+            {
+                MissingKernelAttributeError("2D kernel", NUM_GROUPS_Y_STRING);
+            }
 
-                if (!KernelHasGroupSizeY())
-                {
-                    MissingKernelAttributeError("3D kernel", GROUP_SIZE_Y_STRING);
-                }
+            if (!KernelHasGroupIdY())
+            {
+                MissingKernelAttributeError(GROUP_ID_Y_STRING);
+            }
 
-                if (!KernelHasNumGroupsY())
-                {
-                    MissingKernelAttributeError("3D kernel", NUM_GROUPS_Y_STRING);
-                }
+            if (!KernelHasIdY())
+            {
+                MissingKernelAttributeError("3D kernel", LOCAL_ID_Y_STRING);
+            }
 
-                if (!KernelHasGroupIdY())
-                {
-                    MissingKernelAttributeError("3D kernel", GROUP_ID_Y_STRING);
-                }
+            if (!KernelHasGroupSizeY())
+            {
+                MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
+            }
 
-                if (!KernelHasIdZ())
-                {
-                    MissingKernelAttributeError("3D kernel", LOCAL_ID_Z_STRING);
-                }
+            if (!KernelHasNumGroupsY())
+            {
+                MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
+            }
 
-                if (!KernelHasGroupSizeZ())
-                {
-                    MissingKernelAttributeError("3D kernel", GROUP_SIZE_Z_STRING);
-                }
+            if (!KernelHasGroupIdY())
+            {
+                MissingKernelAttributeError(GROUP_ID_Y_STRING);
+            }
 
-                if (!KernelHasNumGroupsZ())
-                {
-                    MissingKernelAttributeError("3D kernel", NUM_GROUPS_Z_STRING);
-                }
+            if (!KernelHasIdZ())
+            {
+                MissingKernelAttributeError(LOCAL_ID_Z_STRING);
+            }
 
-                if (!KernelHasGroupIdZ())
-                {
-                    MissingKernelAttributeError("3D kernel", GROUP_ID_Z_STRING);
-                }
+            if (!KernelHasGroupSizeZ())
+            {
+                MissingKernelAttributeError(GROUP_SIZE_Z_STRING);
+            }
 
+            if (!KernelHasNumGroupsZ())
+            {
+                MissingKernelAttributeError(NUM_GROUPS_Z_STRING);
+            }
 
+            if (!KernelHasGroupIdZ())
+            {
+                MissingKernelAttributeError(GROUP_ID_Z_STRING);
             }
 
             return ErrorCount;
         }
 
-        private void MissingKernelAttributeError(string kindOfKernel, string attribute)
+        private void MissingKernelAttributeError(string attribute)
         {
-            Error(KernelProcedure.tok, kindOfKernel + " must declare global constant marked with attribute ':" + attribute + "'");
+            Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");
         }
 
         public static bool IsThreadLocalIdConstant(Variable variable)
-- 
cgit v1.2.3