1 files changed, 47 insertions, 18 deletions
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index d5d9917a..ce5f78ee 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -54,13 +54,18 @@ namespace GPUVerify
 
         private TypedIdent DualiseTypedIdent(Variable v)
         {
+          if (QKeyValue.FindBoolAttribute(v.Attributes, "global") ||
+              QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+            return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
+          }
 
-            if (uniformityAnalyser == null || !uniformityAnalyser.IsUniform(procName, v.Name))
-            {
-                return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
-            }
-
+          if (uniformityAnalyser != null && uniformityAnalyser.IsUniform(procName, v.Name))
+          {
             return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
+          }
+
+          return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
+
         }
 
         public override Variable VisitVariable(Variable node)
@@ -79,26 +84,50 @@ namespace GPUVerify
 
         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 MapSelect) {
+            Debug.Assert((node.Fun as MapSelect).Arity == 1);
+            Debug.Assert(node.Args[0] is IdentifierExpr);
+            var v = (node.Args[0] as IdentifierExpr).Decl;
+            if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+              return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+                new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 
+                  new ExprSeq(new Expr[] { node.Args[0], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));
+            }
+          }
 
-            if (node.Fun is FunctionCall)
+          // Avoid dualisation of certain special builtin functions that are cross-thread
+          if (node.Fun is FunctionCall)
+          {
+            FunctionCall call = node.Fun as FunctionCall;
+
+            if (otherFunctionNames.Contains(call.Func.Name))
             {
-                FunctionCall call = node.Fun as FunctionCall;
+              Debug.Assert(id == 1 || id == 2);
+              int otherId = id == 1 ? 2 : 1;
+              return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
+                  node.Args[0]);
+            }
 
-                if (otherFunctionNames.Contains(call.Func.Name))
-                {
-                    Debug.Assert(id == 1 || id == 2);
-                    int otherId = id == 1 ? 2 : 1;
-                    return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
-                        node.Args[0]);
-                }
+          }
 
-            }
+          return base.VisitNAryExpr(node);
+        }
 
-            return base.VisitNAryExpr(node);
+
+        public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
+
+          var v = node.DeepAssignedVariable;
+          if(QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+            return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,
+              new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
+
+          }
+          return base.VisitMapAssignLhs(node);
         }
 
+        private Expr GroupSharedIndexingExpr() {
+          return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();
+        }
 
     }