1 files changed, 81 insertions, 0 deletions
diff --git a/Test/GPUVerify/Feature/ModInvariants/local_direct.gbpl b/Test/GPUVerify/Feature/ModInvariants/local_direct.gbpl
new file mode 100644
index 00000000..70414947
--- /dev/null
+++ b/Test/GPUVerify/Feature/ModInvariants/local_direct.gbpl
@@ -0,0 +1,81 @@
+// RUN: GPUVerify -unstructured -inference -print:%t %s
+// RUN: fgrep '==> BV32_AND(BV32_SUB(' %t.bpl
+// RUN: Boogie -noVerify %t.bpl
+
+type {:datatype} ptr;
+type arrayId;
+function {:constructor} MKPTR(base: arrayId, offset: bv32) : ptr;
+function PTR_LT(lhs: ptr, rhs: ptr) : bool;
+
+type float;
+type double;
+
+var {:global} $$A : [bv32]bv8;
+const unique $arrayId$A : arrayId;
+
+var {:global} $$B : [bv32]bv8;
+const unique $arrayId$B : arrayId;
+
+var {:global} $$C : [bv32]bv8;
+const unique $arrayId$C : arrayId;
+
+const unique $arrayId$$null : arrayId;
+
+const {:group_size_x} group_size_x : bv32;
+const {:group_size_y} group_size_y : bv32;
+const {:group_size_z} group_size_z : bv32;
+const {:local_id_x} local_id_x : bv32;
+const {:num_groups_x} num_groups_x : bv32;
+const {:num_groups_y} num_groups_y : bv32;
+const {:num_groups_z} num_groups_z : bv32;
+function {:bvbuiltin "bvadd"} BV32_ADD(bv32, bv32) : bv32;
+function {:bvbuiltin "bvmul"} BV32_MUL(bv32, bv32) : bv32;
+function {:bvbuiltin "bvslt"} BV32_SLT(bv32, bv32) : bool;
+procedure {:kernel} $foo()
+{
+  var $i.0:bv32;
+  var v0:bool;
+  var v1:bv32;
+  var v4:bv8;
+  var v5:bv8;
+  var v2:bv8;
+  var v3:bv8;
+$entry:
+  $i.0 := 0bv32;
+  goto $for.cond;
+$for.cond:
+  v0 := BV32_SLT($i.0, 1024bv32);
+  goto $truebb, $falsebb;
+$for.body:
+  v1 := local_id_x;
+  $$A[BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32)] := v1[8:0];
+  $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 1bv32)] := v1[16:8];
+  $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 2bv32)] := v1[24:16];
+  $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 3bv32)] := v1[32:24];
+  v2 := $$A[BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32)];
+  v3 := $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 1bv32)];
+  v4 := $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 2bv32)];
+  v5 := $$A[BV32_ADD(BV32_MUL(BV32_ADD(BV32_MUL($i.0, 256bv32), local_id_x), 4bv32), 3bv32)];
+  $$B[BV32_MUL(BV32_ADD(local_id_x, BV32_MUL(256bv32, $i.0)), 4bv32)] := v2;
+  $$B[BV32_ADD(BV32_MUL(BV32_ADD(local_id_x, BV32_MUL(256bv32, $i.0)), 4bv32), 1bv32)] := v3;
+  $$B[BV32_ADD(BV32_MUL(BV32_ADD(local_id_x, BV32_MUL(256bv32, $i.0)), 4bv32), 2bv32)] := v4;
+  $$B[BV32_ADD(BV32_MUL(BV32_ADD(local_id_x, BV32_MUL(256bv32, $i.0)), 4bv32), 3bv32)] := v5;
+  goto $for.inc;
+$for.inc:
+  $i.0 := BV32_ADD($i.0, 1bv32);
+  goto $for.cond;
+$for.end:
+  return;
+$truebb:
+  assume v0;
+  goto $for.body;
+$falsebb:
+  assume !v0;
+  goto $for.end;
+}
+axiom (if group_size_y == 1bv32 then 1bv1 else 0bv1) != 0bv1;
+axiom (if group_size_z == 1bv32 then 1bv1 else 0bv1) != 0bv1;
+axiom (if num_groups_y == 1bv32 then 1bv1 else 0bv1) != 0bv1;
+axiom (if num_groups_z == 1bv32 then 1bv1 else 0bv1) != 0bv1;
+axiom (if group_size_x == 16bv32 then 1bv1 else 0bv1) != 0bv1;
+axiom (if num_groups_x == 8bv32 then 1bv1 else 0bv1) != 0bv1;