[ScopInfo] Simplify inbounds assumptions under domain constraints
Without this simplification for a loop nest:
void foo(long n1_a, long n1_b, long n1_c, long n1_d,
long p1_b, long p1_c, long p1_d,
float A_1[][p1_b][p1_c][p1_d]) {
for (long i = 0; i < n1_a; i++)
for (long j = 0; j < n1_b; j++)
for (long k = 0; k < n1_c; k++)
for (long l = 0; l < n1_d; l++)
A_1[i][j][k][l] += i + j + k + l;
}
the assumption:
n1_a <= 0 or (n1_a > 0 and n1_b <= 0) or
(n1_a > 0 and n1_b > 0 and n1_c <= 0) or
(n1_a > 0 and n1_b > 0 and n1_c > 0 and n1_d <= 0) or
(n1_a > 0 and n1_b > 0 and n1_c > 0 and n1_d > 0 and
p1_b >= n1_b and p1_c >= n1_c and p1_d >= n1_d)
is taken rather than the simpler assumption:
p9_b >= n9_b and p9_c >= n9_c and p9_d >= n9_d.
The former is less strict, as it allows arbitrary values of p1_* in case, the
loop is not executed at all. However, in practice these precise constraints
explode when combined across different accesses and loops. For now it seems
to make more sense to take less precise, but more scalable constraints by
default. In case we find a practical example where more precise constraints
are needed, we can think about allowing such precise constraints in specific
situations where they help.
This change speeds up the new test case from taking very long (waited at least
a minute, but it probably takes a lot more) to below a second.
llvm-svn: 296456
2017-02-28 17:45:54 +08:00
|
|
|
; RUN: opt %loadPolly -pass-remarks-analysis="polly-scops" -polly-scops \
|
|
|
|
|
; RUN: -polly-precise-inbounds -disable-output < %s 2>&1 | FileCheck %s
|
2015-11-12 11:25:01 +08:00
|
|
|
;
|
|
|
|
|
; CHECK: remark: <unknown>:0:0: SCoP begins here.
|
2016-05-10 22:00:57 +08:00
|
|
|
; CHECK-NEXT: remark: <unknown>:0:0: Use user assumption: [i, N, M] -> { : N <= i or (N > i and N >= 0) }
|
Model zext-extend instructions
A zero-extended value can be interpreted as a piecewise defined signed
value. If the value was non-negative it stays the same, otherwise it
is the sum of the original value and 2^n where n is the bit-width of
the original (or operand) type. Examples:
zext i8 127 to i32 -> { [127] }
zext i8 -1 to i32 -> { [256 + (-1)] } = { [255] }
zext i8 %v to i32 -> [v] -> { [v] | v >= 0; [256 + v] | v < 0 }
However, LLVM/Scalar Evolution uses zero-extend (potentially lead by a
truncate) to represent some forms of modulo computation. The left-hand side
of the condition in the code below would result in the SCEV
"zext i1 <false, +, true>for.body" which is just another description
of the C expression "i & 1 != 0" or, equivalently, "i % 2 != 0".
for (i = 0; i < N; i++)
if (i & 1 != 0 /* == i % 2 */)
/* do something */
If we do not make the modulo explicit but only use the mechanism described
above we will get the very restrictive assumption "N < 3", because for all
values of N >= 3 the SCEVAddRecExpr operand of the zero-extend would wrap.
Alternatively, we can make the modulo in the operand explicit in the
resulting piecewise function and thereby avoid the assumption on N. For the
example this would result in the following piecewise affine function:
{ [i0] -> [(1)] : 2*floor((-1 + i0)/2) = -1 + i0;
[i0] -> [(0)] : 2*floor((i0)/2) = i0 }
To this end we can first determine if the (immediate) operand of the
zero-extend can wrap and, in case it might, we will use explicit modulo
semantic to compute the result instead of emitting non-wrapping assumptions.
Note that operands with large bit-widths are less likely to be negative
because it would result in a very large access offset or loop bound after the
zero-extend. To this end one can optimistically assume the operand to be
positive and avoid the piecewise definition if the bit-width is bigger than
some threshold (here MaxZextSmallBitWidth).
We choose to go with a hybrid solution of all modeling techniques described
above. For small bit-widths (up to MaxZextSmallBitWidth) we will model the
wrapping explicitly and use a piecewise defined function. However, if the
bit-width is bigger than MaxZextSmallBitWidth we will employ overflow
assumptions and assume the "former negative" piece will not exist.
llvm-svn: 267408
2016-04-25 22:01:36 +08:00
|
|
|
; CHECK-NEXT: remark: <unknown>:0:0: Inbounds assumption: [i, N, M] -> { : N <= i or (N > i and M <= 100) }
|
2015-11-12 11:25:01 +08:00
|
|
|
; CHECK-NEXT: remark: <unknown>:0:0: SCoP ends here.
|
|
|
|
|
;
|
|
|
|
|
; void f(int *restrict A, int *restrict B, int i, int N, int M, int C[100][100]) {
|
|
|
|
|
; for (; i < N; i++) {
|
|
|
|
|
; __builtin_assume(N >= 0);
|
|
|
|
|
; for (int j = 0; j != M; j++) {
|
|
|
|
|
; __builtin_assume(N >= 0);
|
|
|
|
|
; C[i][j] += A[i * M + j] + B[i + j];
|
|
|
|
|
; }
|
|
|
|
|
; }
|
|
|
|
|
; }
|
|
|
|
|
;
|
2017-07-18 07:58:33 +08:00
|
|
|
|
|
|
|
|
|
|
|
|
|
; RUN: opt %loadPolly -pass-remarks-analysis="polly-scops" -polly-scops \
|
|
|
|
|
; RUN: -polly-precise-inbounds -disable-output < %s 2>&1 -pass-remarks-output=%t.yaml
|
|
|
|
|
; RUN: cat %t.yaml | FileCheck -check-prefix=YAML %s
|
|
|
|
|
; YAML: --- !Analysis
|
|
|
|
|
; YAML: Pass: polly-scops
|
|
|
|
|
; YAML: Name: ScopEntry
|
|
|
|
|
; YAML: Function: f
|
|
|
|
|
; YAML: Args:
|
|
|
|
|
; YAML: - String: SCoP begins here.
|
|
|
|
|
; YAML: ...
|
|
|
|
|
; YAML: --- !Analysis
|
|
|
|
|
; YAML: Pass: polly-scops
|
|
|
|
|
; YAML: Name: UserAssumption
|
|
|
|
|
; YAML: Function: f
|
|
|
|
|
; YAML: Args:
|
|
|
|
|
; YAML: - String: 'Use user assumption: '
|
|
|
|
|
; YAML: - String: '[i, N, M] -> { : N <= i or (N > i and N >= 0) }'
|
|
|
|
|
; YAML: ...
|
|
|
|
|
; YAML: --- !Analysis
|
|
|
|
|
; YAML: Pass: polly-scops
|
|
|
|
|
; YAML: Name: AssumpRestrict
|
|
|
|
|
; YAML: Function: f
|
|
|
|
|
; YAML: Args:
|
|
|
|
|
; YAML: - String: 'Inbounds assumption: [i, N, M] -> { : N <= i or (N > i and M <= 100) }'
|
|
|
|
|
; YAML: ...
|
|
|
|
|
; YAML: --- !Analysis
|
|
|
|
|
; YAML: Pass: polly-scops
|
|
|
|
|
; YAML: Name: ScopEnd
|
|
|
|
|
; YAML: Function: f
|
|
|
|
|
; YAML: Args:
|
|
|
|
|
; YAML: - String: SCoP ends here.
|
|
|
|
|
; YAML: ...
|
|
|
|
|
|
2015-11-12 11:25:01 +08:00
|
|
|
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
|
|
|
|
|
|
|
|
|
|
define void @f(i32* noalias %A, i32* noalias %B, i32 %i, i32 %N, i32 %M, [100 x i32]* %C) {
|
|
|
|
|
entry:
|
|
|
|
|
%tmp = zext i32 %M to i64
|
|
|
|
|
%tmp6 = sext i32 %i to i64
|
|
|
|
|
%tmp7 = sext i32 %N to i64
|
|
|
|
|
%tmp8 = sext i32 %M to i64
|
|
|
|
|
br label %for.cond
|
|
|
|
|
|
|
|
|
|
for.cond: ; preds = %for.inc.15, %entry
|
|
|
|
|
%indvars.iv3 = phi i64 [ %indvars.iv.next4, %for.inc.15 ], [ %tmp6, %entry ]
|
|
|
|
|
%cmp = icmp slt i64 %indvars.iv3, %tmp7
|
|
|
|
|
br i1 %cmp, label %for.body, label %for.end.17
|
|
|
|
|
|
|
|
|
|
for.body: ; preds = %for.cond
|
|
|
|
|
%cmp1 = icmp sgt i32 %N, -1
|
|
|
|
|
call void @llvm.assume(i1 %cmp1)
|
|
|
|
|
br label %for.cond.2
|
|
|
|
|
|
|
|
|
|
for.cond.2: ; preds = %for.inc, %for.body
|
|
|
|
|
%indvars.iv = phi i64 [ %indvars.iv.next, %for.inc ], [ 0, %for.body ]
|
|
|
|
|
%cmp3 = icmp eq i64 %indvars.iv, %tmp
|
|
|
|
|
br i1 %cmp3, label %for.end, label %for.body.4
|
|
|
|
|
|
|
|
|
|
for.body.4: ; preds = %for.cond.2
|
|
|
|
|
%tmp9 = mul nsw i64 %indvars.iv3, %tmp8
|
|
|
|
|
%tmp10 = add nsw i64 %tmp9, %indvars.iv
|
|
|
|
|
%arrayidx = getelementptr inbounds i32, i32* %A, i64 %tmp10
|
|
|
|
|
%tmp11 = load i32, i32* %arrayidx, align 4
|
|
|
|
|
%tmp12 = add nsw i64 %indvars.iv3, %indvars.iv
|
|
|
|
|
%arrayidx8 = getelementptr inbounds i32, i32* %B, i64 %tmp12
|
|
|
|
|
%tmp13 = load i32, i32* %arrayidx8, align 4
|
|
|
|
|
%add9 = add nsw i32 %tmp11, %tmp13
|
|
|
|
|
%arrayidx13 = getelementptr inbounds [100 x i32], [100 x i32]* %C, i64 %indvars.iv3, i64 %indvars.iv
|
|
|
|
|
%tmp14 = load i32, i32* %arrayidx13, align 4
|
|
|
|
|
%add14 = add nsw i32 %tmp14, %add9
|
|
|
|
|
store i32 %add14, i32* %arrayidx13, align 4
|
|
|
|
|
br label %for.inc
|
|
|
|
|
|
|
|
|
|
for.inc: ; preds = %for.body.4
|
|
|
|
|
%indvars.iv.next = add nuw nsw i64 %indvars.iv, 1
|
|
|
|
|
br label %for.cond.2
|
|
|
|
|
|
|
|
|
|
for.end: ; preds = %for.cond.2
|
|
|
|
|
br label %for.inc.15
|
|
|
|
|
|
|
|
|
|
for.inc.15: ; preds = %for.end
|
|
|
|
|
%indvars.iv.next4 = add nsw i64 %indvars.iv3, 1
|
|
|
|
|
br label %for.cond
|
|
|
|
|
|
|
|
|
|
for.end.17: ; preds = %for.cond
|
|
|
|
|
ret void
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
declare void @llvm.assume(i1) #1
|
|
|
|
|
|