Skip to content

Commit 9ba5fa2

Browse files
authored
[Delinearization] Add test for inferred array size exceeds integer range (NFC) (#169048)
Add test cases where the delinearized arrays may not satisfy the following "common" property: `&A[I_1][I_2]...[I_n] == &A[J_1][J_2]...[J_n]` iff `(I_1, I_2, ..., I_n) == (J_1, J_2, ..., J_n)` The root cause of this issue is that the inferred array size is too large and the offset calculation overflows. Such results should be discarded during validation. This will be fixed by #169902 .
1 parent 3098bfe commit 9ba5fa2

File tree

1 file changed

+140
-0
lines changed

1 file changed

+140
-0
lines changed
Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
; NOTE: Assertions have been autogenerated by utils/update_analyze_test_checks.py UTC_ARGS: --version 6
2+
; RUN: opt < %s -passes='print<delinearization>' --delinearize-use-fixed-size-array-heuristic -disable-output 2>&1 | FileCheck %s
3+
4+
; FIXME: As for array accesses, the following property should hold (without
5+
; out-of-bound accesses):
6+
;
7+
; &A[I_1][I_2]...[I_n] == &A[J_1][J_2]...[J_n] iff
8+
; (I_1, I_2, ..., I_n) == (J_1, J_2, ..., J_n)
9+
;
10+
; Currently, delinearization doesn't guarantee this property, especially when
11+
; the inferred array size is very large so that the product of dimensions may
12+
; overflow. The delinearization validation should consider such cases as
13+
; invalid.
14+
15+
; for (i = 0; i < (1ULL << 60); i++)
16+
; for (j = 0; j < 256; j++)
17+
; A[i*256 + j] = 0;
18+
;
19+
; The store will be delinearized to `A[i][j]` with its size `[][256]`. Since
20+
; `i` can be very large, the mapping from subscripts to addresses is not
21+
; injective. E.g., `&A[0][j] = &A[2^56][j] = ...`.
22+
;
23+
define void @large_size_fixed(ptr %A) {
24+
; CHECK-LABEL: 'large_size_fixed'
25+
; CHECK-NEXT: Inst: store i8 0, ptr %gep, align 1
26+
; CHECK-NEXT: AccessFunction: {{\{\{}}0,+,256}<%for.i.header>,+,1}<nsw><%for.j>
27+
; CHECK-NEXT: Base offset: %A
28+
; CHECK-NEXT: ArrayDecl[UnknownSize][256] with elements of 1 bytes.
29+
; CHECK-NEXT: ArrayRef[{0,+,1}<nuw><nsw><%for.i.header>][{0,+,1}<nuw><nsw><%for.j>]
30+
; CHECK-NEXT: Delinearization validation: Succeeded
31+
;
32+
entry:
33+
br label %for.i.header
34+
35+
for.i.header:
36+
%i = phi i64 [ 0, %entry ], [ %i.inc, %for.i.latch ]
37+
%i.mul = mul i64 %i, 256
38+
br label %for.j
39+
40+
for.j:
41+
%j = phi i64 [ 0, %for.i.header ], [ %j.inc, %for.j ]
42+
%offset = add nsw i64 %i.mul, %j
43+
%gep = getelementptr i8, ptr %A, i64 %offset
44+
store i8 0, ptr %gep
45+
%j.inc = add i64 %j, 1
46+
%ec.j = icmp eq i64 %j.inc, 256
47+
br i1 %ec.j, label %for.i.latch, label %for.j
48+
49+
for.i.latch:
50+
%i.inc = add i64 %i, 1
51+
%ec.i = icmp eq i64 %i.inc, 1152921504606846976
52+
br i1 %ec.i, label %exit, label %for.i.header
53+
54+
exit:
55+
ret void
56+
}
57+
58+
; for (i = 0; i < n; i++)
59+
; for (j = 0; j < m; j++)
60+
; for (k = 0; k < o; k++)
61+
; if (i < 5 && j < 5 && k < 5)
62+
; A[i*m*o + j*o + k] = 0;
63+
;
64+
; The product (%m * %o) can overflow, e.g., (%m, %o) = (2^32 - 1, 2^32). In
65+
; this case, the delinearization `A[%i][%j][%k]` with its size `[][%m][%o]`
66+
; should be considered invalid, because the address calculation will be:
67+
;
68+
; A[%i][%j][%k] = %A + %i*%m*%o + %j*%o + %k
69+
; = %A - 2^32*%i + %j*2^32 + %k
70+
; = %A + 2^32*(%j - %i) + %k
71+
;
72+
; It means `&A[0][0][%k]` = `&A[1][1][%k]` = ..., which implies that the
73+
; mapping from subscripts to addresses is not injective.
74+
;
75+
define void @large_size_parametric(i64 %n, i64 %m, i64 %o, ptr %A) {
76+
; CHECK-LABEL: 'large_size_parametric'
77+
; CHECK-NEXT: Inst: store i8 0, ptr %gep, align 1
78+
; CHECK-NEXT: AccessFunction: {{\{\{\{}}0,+,(%m * %o)}<%for.i.header>,+,%o}<%for.j.header>,+,1}<nw><%for.k.header>
79+
; CHECK-NEXT: Base offset: %A
80+
; CHECK-NEXT: ArrayDecl[UnknownSize][%m][%o] with elements of 1 bytes.
81+
; CHECK-NEXT: ArrayRef[{0,+,1}<nuw><nsw><%for.i.header>][{0,+,1}<nuw><nsw><%for.j.header>][{0,+,1}<nuw><nsw><%for.k.header>]
82+
; CHECK-NEXT: Delinearization validation: Succeeded
83+
;
84+
entry:
85+
%guard.i = icmp sgt i64 %n, 0
86+
%m_o = mul i64 %m, %o
87+
br i1 %guard.i, label %for.i.header, label %exit
88+
89+
for.i.header:
90+
%i = phi i64 [ 0, %entry ], [ %i.inc, %for.i.latch ]
91+
%i_m_o = mul i64 %i, %m_o
92+
br label %for.j.preheader
93+
94+
for.j.preheader:
95+
%guard.j = icmp sgt i64 %m, 0
96+
br i1 %guard.j, label %for.j.header, label %for.i.latch
97+
98+
for.j.header:
99+
%j = phi i64 [ 0, %for.j.preheader ], [ %j.inc, %for.j.latch ]
100+
%j_o = mul i64 %j, %o
101+
br label %for.k.preheader
102+
103+
for.k.preheader:
104+
%guard.k = icmp sgt i64 %o, 0
105+
br i1 %guard.k, label %for.k.header, label %for.j.latch
106+
107+
for.k.header:
108+
%k = phi i64 [ 0, %for.k.preheader ], [ %k.inc, %for.k.latch ]
109+
%cond.i = icmp slt i64 %i, 5
110+
%cond.j = icmp slt i64 %j, 5
111+
%cond.k = icmp slt i64 %k, 5
112+
%cond.ij = and i1 %cond.i, %cond.j
113+
%cond = and i1 %cond.ij, %cond.k
114+
br i1 %cond, label %if.then, label %for.k.latch
115+
116+
if.then:
117+
%offset.tmp = add i64 %i_m_o, %j_o
118+
%offset = add i64 %offset.tmp, %k
119+
%gep = getelementptr i8, ptr %A, i64 %offset
120+
store i8 0, ptr %gep, align 1
121+
br label %for.k.latch
122+
123+
for.k.latch:
124+
%k.inc = add nsw i64 %k, 1
125+
%ec.k = icmp eq i64 %k.inc, %o
126+
br i1 %ec.k, label %for.j.latch, label %for.k.header
127+
128+
for.j.latch:
129+
%j.inc = add nsw i64 %j, 1
130+
%ec.j = icmp eq i64 %j.inc, %m
131+
br i1 %ec.j, label %for.i.latch, label %for.j.header
132+
133+
for.i.latch:
134+
%i.inc = add nsw i64 %i, 1
135+
%ec.i = icmp eq i64 %i.inc, %n
136+
br i1 %ec.i, label %exit, label %for.i.header
137+
138+
exit:
139+
ret void
140+
}

0 commit comments

Comments
 (0)