diff options
Diffstat (limited to 'Test/GPUVerify/Feature/ModInvariants/local_reduce_strength.gbpl')
-rw-r--r-- | Test/GPUVerify/Feature/ModInvariants/local_reduce_strength.gbpl | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/Test/GPUVerify/Feature/ModInvariants/local_reduce_strength.gbpl b/Test/GPUVerify/Feature/ModInvariants/local_reduce_strength.gbpl new file mode 100644 index 00000000..181ad1ef --- /dev/null +++ b/Test/GPUVerify/Feature/ModInvariants/local_reduce_strength.gbpl @@ -0,0 +1,80 @@ +// RUN: GPUVerify -unstructured -inference -print:%t %s +// RUN: grep 'assert.*WRITE_HAS_OCCURRED.*==> BV32_AND(BV32_SUB(' %t.bpl +// RUN: grep 'assert {:tag "variable \$i\.0 is strided"}.*\$i\.0\$1.*group_size_x.*local_id_x\$1' %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_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 v1:bv32; + var v2:bv32; + var v3:bv32; + var v0:bool; +$entry: + $i.0 := local_id_x; + goto $for.cond; +$for.cond: + v0 := BV32_SLT($i.0, 1024bv32); + goto $truebb, $falsebb; +$for.body: + v1 := local_id_x; + $$A[BV32_MUL($i.0, 4bv32)] := v1[8:0]; + $$A[BV32_ADD(BV32_MUL($i.0, 4bv32), 1bv32)] := v1[16:8]; + $$A[BV32_ADD(BV32_MUL($i.0, 4bv32), 2bv32)] := v1[24:16]; + $$A[BV32_ADD(BV32_MUL($i.0, 4bv32), 3bv32)] := v1[32:24]; + v2 := local_id_x; + $$B[BV32_MUL(BV32_ADD($i.0, 10bv32), 4bv32)] := v2[8:0]; + $$B[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 10bv32), 4bv32), 1bv32)] := v2[16:8]; + $$B[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 10bv32), 4bv32), 2bv32)] := v2[24:16]; + $$B[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 10bv32), 4bv32), 3bv32)] := v2[32:24]; + v3 := local_id_x; + $$C[BV32_MUL(BV32_ADD($i.0, 20bv32), 4bv32)] := v3[8:0]; + $$C[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 20bv32), 4bv32), 1bv32)] := v3[16:8]; + $$C[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 20bv32), 4bv32), 2bv32)] := v3[24:16]; + $$C[BV32_ADD(BV32_MUL(BV32_ADD($i.0, 20bv32), 4bv32), 3bv32)] := v3[32:24]; + goto $for.inc; +$for.inc: + $i.0 := BV32_ADD($i.0, group_size_x); + 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; |