1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
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;
|
