[polly] r267885 - [FIX] Correct assumption simplification

[Johannes Doerfert via llvm-commits]

Author: jdoerfert
Date: Thu Apr 28 09:32:58 2016
New Revision: 267885

URL: http://llvm.org/viewvc/llvm-project?rev=267885&view=rev
Log:
[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.

Modified:
    polly/trunk/lib/Analysis/ScopInfo.cpp
    polly/trunk/test/ScopInfo/simple_loop_unsigned.ll
    polly/trunk/test/ScopInfo/simple_loop_unsigned_2.ll

Modified: polly/trunk/lib/Analysis/ScopInfo.cpp
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/lib/Analysis/ScopInfo.cpp?rev=267885&r1=267884&r2=267885&view=diff
==============================================================================
--- polly/trunk/lib/Analysis/ScopInfo.cpp (original)
+++ polly/trunk/lib/Analysis/ScopInfo.cpp Thu Apr 28 09:32:58 2016
@@ -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);
   }
 }
 

Modified: polly/trunk/test/ScopInfo/simple_loop_unsigned.ll
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/test/ScopInfo/simple_loop_unsigned.ll?rev=267885&r1=267884&r2=267885&view=diff
==============================================================================
--- polly/trunk/test/ScopInfo/simple_loop_unsigned.ll (original)
+++ polly/trunk/test/ScopInfo/simple_loop_unsigned.ll Thu Apr 28 09:32:58 2016
@@ -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 };

Modified: polly/trunk/test/ScopInfo/simple_loop_unsigned_2.ll
URL: http://llvm.org/viewvc/llvm-project/polly/trunk/test/ScopInfo/simple_loop_unsigned_2.ll?rev=267885&r1=267884&r2=267885&view=diff
==============================================================================
--- polly/trunk/test/ScopInfo/simple_loop_unsigned_2.ll (original)
+++ polly/trunk/test/ScopInfo/simple_loop_unsigned_2.ll Thu Apr 28 09:32:58 2016
@@ -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 };