From 8475d1c1638235a89eba799ebd94d056aa49d582 Mon Sep 17 00:00:00 2001 From: Johannes Doerfert Date: Thu, 28 Apr 2016 14:32:58 +0000 Subject: [PATCH] [FIX] Correct assumption simplification Assumptions and restrictions can both be simplified with the domain of a statement but not the same way. After this patch we will correctly distinguish them. llvm-svn: 267885 --- polly/lib/Analysis/ScopInfo.cpp | 24 ++++++++++++++++++++---- polly/test/ScopInfo/simple_loop_unsigned.ll | 4 +++- polly/test/ScopInfo/simple_loop_unsigned_2.ll | 4 +++- 3 files changed, 26 insertions(+), 6 deletions(-) diff --git a/polly/lib/Analysis/ScopInfo.cpp b/polly/lib/Analysis/ScopInfo.cpp index 20084cd..2b0c182 100644 --- a/polly/lib/Analysis/ScopInfo.cpp +++ b/polly/lib/Analysis/ScopInfo.cpp @@ -3651,12 +3651,28 @@ void Scop::addRecordedAssumptions() { while (!RecordedAssumptions.empty()) { const Assumption &AS = RecordedAssumptions.pop_back_val(); - isl_set *S = AS.Set; + if (!AS.BB) { + addAssumption(AS.Kind, AS.Set, AS.Loc, AS.Sign); + continue; + } + // If a basic block was given use its domain to simplify the assumption. - if (AS.BB) - S = isl_set_params(isl_set_intersect(S, getDomainConditions(AS.BB))); + // In case of restrictions we know they only have to hold on the domain, + // thus we can intersect them with the domain of the block. However, for + // assumptions the domain has to imply them, thus: + // _ _____ + // Dom => S <==> A v B <==> A - B + // + // To avoid the complement we will register A - B as a restricton not an + // assumption. + isl_set *S = AS.Set; + isl_set *Dom = getDomainConditions(AS.BB); + if (AS.Sign == AS_RESTRICTION) + S = isl_set_params(isl_set_intersect(S, Dom)); + else /* (AS.Sign == AS_ASSUMPTION) */ + S = isl_set_params(isl_set_subtract(Dom, S)); - addAssumption(AS.Kind, S, AS.Loc, AS.Sign); + addAssumption(AS.Kind, S, AS.Loc, AS_RESTRICTION); } } diff --git a/polly/test/ScopInfo/simple_loop_unsigned.ll b/polly/test/ScopInfo/simple_loop_unsigned.ll index 0f451f2..dcd13dd 100644 --- a/polly/test/ScopInfo/simple_loop_unsigned.ll +++ b/polly/test/ScopInfo/simple_loop_unsigned.ll @@ -8,7 +8,9 @@ ; } ; CHECK: Assumed Context: -; CHECK-NEXT: [N] -> { : N >= 0 } +; CHECK-NEXT: [N] -> { : } +; CHECK-NEXT: Invalid Context: +; CHECK-NEXT: [N] -> { : N < 0 } ; ; CHECK: Domain := ; CHECK-NEXT: [N] -> { Stmt_bb[i0] : 0 <= i0 < N; Stmt_bb[0] : N <= 0 }; diff --git a/polly/test/ScopInfo/simple_loop_unsigned_2.ll b/polly/test/ScopInfo/simple_loop_unsigned_2.ll index 744bf27..8e7ef93 100644 --- a/polly/test/ScopInfo/simple_loop_unsigned_2.ll +++ b/polly/test/ScopInfo/simple_loop_unsigned_2.ll @@ -1,7 +1,9 @@ ; RUN: opt %loadPolly -polly-scops -analyze < %s | FileCheck %s ; CHECK: Assumed Context: -; CHECK-NEXT: [N] -> { : N > 0 } +; CHECK-NEXT: [N] -> { : } +; CHECK-NEXT: Invalid Context: +; CHECK-NEXT: [N] -> { : N <= 0 or N >= 1152921504606846976 } ; ; CHECK: Domain := ; CHECK-NEXT: [N] -> { Stmt_bb[i0] : 0 <= i0 < N; Stmt_bb[0] : N <= 0 }; -- 2.7.4