[polly] 68a9cd3 - [Polly] Detect preconditions of cached user assumption translations (#226204)

[via llvm-commits]

Author: Timur Baidusenov
Date: 2026-09-25T14:06:08+02:00
New Revision: 68a9cd31fd277f9f6b8a8ab95e18d00a786e7c12

URL: https://github.com/llvm/llvm-project/commit/68a9cd31fd277f9f6b8a8ab95e18d00a786e7c12
DIFF: https://github.com/llvm/llvm-project/commit/68a9cd31fd277f9f6b8a8ab95e18d00a786e7c12.diff

LOG: [Polly] Detect preconditions of cached user assumption translations (#226204)

`addUserAssumptions` detected preconditions of a user assumption by
checking whether building its condition recorded new assumptions, but
`SCEVAffinator` caches translated expressions, so a precondition shared
with an earlier assumption (e.g. the same truncation) was missed and the
assumption went into the context, removing the runtime check it relied
on. For example, with `__builtin_assume((signed char)n >= 0)` and
`__builtin_assume((signed char)n < 10)`, the `n >= 128` check was
dropped, although `n = 261` satisfies both assumptions. Instead, check
the invalid domain of each assumption, which is also cached, and if it
is non-empty, add the assumption to the defined behavior context as in
#189350.

Assisted-by: Claude (Anthropic)

Added: 
    polly/test/ScopInfo/user-assumption-cached-precondition.ll

Modified: 
    polly/lib/Analysis/ScopBuilder.cpp

Removed: 
    


################################################################################
diff  --git a/polly/lib/Analysis/ScopBuilder.cpp b/polly/lib/Analysis/ScopBuilder.cpp
index 5f8c6dc8ccd38..7a52ee3481817 100644
--- a/polly/lib/Analysis/ScopBuilder.cpp
+++ b/polly/lib/Analysis/ScopBuilder.cpp
@@ -1441,17 +1441,31 @@ void ScopBuilder::addUserAssumptions(
       NewParams.insert(Param);
     }
 
-    size_t NumAssumptions = RecordedAssumptions.size();
     SmallVector<isl_set *, 2> ConditionSets;
     auto *TI = InScop ? CI->getParent()->getTerminator() : nullptr;
     BasicBlock *BB = InScop ? CI->getParent() : R.getEntry();
     auto *Dom = InScop ? isl_set_copy(scop->getDomainConditions(BB).get())
                        : isl_set_copy(scop->getContext().get());
     assert(Dom && "Cannot propagate a nullptr.");
-    bool Valid = buildConditionSets(BB, Val, TI, L, Dom, InvalidDomainMap,
-                                    ConditionSets);
+
+    // Collect the invalid domain of this assumption on its own to determine
+    // whether its translation depends on preconditions (such as a truncation
+    // not overflowing). Checking for newly recorded assumptions is not
+    // sufficient: SCEVAffinator caches translated expressions, so a
+    // precondition shared with an earlier assumption is only recorded once.
+    isl::set BBInvalidDomain = InvalidDomainMap[BB];
+    assert(!BBInvalidDomain.is_null() && "Cannot propagate a nullptr.");
+    DenseMap<BasicBlock *, isl::set> AssumptionInvalidDomainMap;
+    AssumptionInvalidDomainMap[BB] =
+        isl::set::empty(BBInvalidDomain.get_space());
+    bool Valid = buildConditionSets(BB, Val, TI, L, Dom,
+                                    AssumptionInvalidDomainMap, ConditionSets);
     isl_set_free(Dom);
 
+    isl::set AssumptionInvalidDomain = AssumptionInvalidDomainMap[BB];
+    bool HasPreconditions = !AssumptionInvalidDomain.is_empty();
+    InvalidDomainMap[BB] = BBInvalidDomain.unite(AssumptionInvalidDomain);
+
     if (!Valid)
       continue;
 
@@ -1487,7 +1501,7 @@ void ScopBuilder::addUserAssumptions(
     // correctness of AssumptionCtx. Using DefinedBehaviorContext which does not
     // gist the other contexts.
     // TODO: Use recordAssumption() for adding context/assumptions
-    if (NumAssumptions == RecordedAssumptions.size()) {
+    if (!HasPreconditions) {
       isl::set newContext =
           scop->getContext().intersect(isl::manage(AssumptionCtx));
       scop->setContext(newContext);

diff  --git a/polly/test/ScopInfo/user-assumption-cached-precondition.ll b/polly/test/ScopInfo/user-assumption-cached-precondition.ll
new file mode 100644
index 0000000000000..43c1e444c641b
--- /dev/null
+++ b/polly/test/ScopInfo/user-assumption-cached-precondition.ll
@@ -0,0 +1,63 @@
+; RUN: opt %loadNPMPolly '-passes=polly-custom<scops>' -polly-print-scops -disable-output < %s 2>&1 | FileCheck %s
+; RUN: opt %loadNPMPolly '-passes=polly-custom<ast>' -polly-print-ast -disable-output < %s 2>&1 | FileCheck %s --check-prefix=AST
+;
+; Both user assumptions are derived from (trunc i64 %n to i8), which is only
+; modeled correctly if the truncation does not overflow. SCEVAffinator caches
+; the translation of the truncation, so the precondition is recorded only for
+; the first assumption. The second assumption must nevertheless not be added
+; to the context: this would remove the 'n >= 128' runtime check from the
+; invalid context and the 'n <= 9' condition from the domain of Stmt_then.
+; For n = 261, both assumptions hold but Stmt_then must not be executed.
+;
+; void f(int *A, long n) {
+;   __builtin_assume((signed char)n >= 0);
+;   __builtin_assume((signed char)n < 10);
+;   for (long i = 0; i < 4; i++)
+;     if (n < 10)
+;       A[i] = 1;
+; }
+
+; CHECK:      Context:
+; CHECK-NEXT:   [n] -> {  : -9223372036854775808 <= n <= 9223372036854775807 }
+; CHECK:      Invalid Context:
+; CHECK-NEXT:   [n] -> {  : n <= -129 or n >= 128 }
+; CHECK:      Defined Behavior Context:
+; CHECK-NEXT:   [n] -> {  : 0 <= n <= 9 }
+; CHECK:      Domain :=
+; CHECK-NEXT:   [n] -> { Stmt_then[i0] : n <= 9 and 0 <= i0 <= 3 };
+
+; AST:      if (1 && 0 == (n <= -129 || n >= 128))
+; AST-EMPTY:
+; AST-NEXT:     if (n <= 9)
+; AST-NEXT:       for (int c0 = 0; c0 <= 3; c0 += 1)
+; AST-NEXT:         Stmt_then(c0);
+
+define void @f(ptr %A, i64 %n) {
+entry:
+  %t = trunc i64 %n to i8
+  %c1 = icmp sge i8 %t, 0
+  call void @llvm.assume(i1 %c1)
+  %c2 = icmp slt i8 %t, 10
+  call void @llvm.assume(i1 %c2)
+  br label %for
+
+for:
+  %i = phi i64 [ 0, %entry ], [ %i.next, %latch ]
+  %small = icmp slt i64 %n, 10
+  br i1 %small, label %then, label %latch
+
+then:
+  %gep = getelementptr inbounds i32, ptr %A, i64 %i
+  store i32 1, ptr %gep
+  br label %latch
+
+latch:
+  %i.next = add nuw nsw i64 %i, 1
+  %cmp = icmp slt i64 %i.next, 4
+  br i1 %cmp, label %for, label %exit
+
+exit:
+  ret void
+}
+
+declare void @llvm.assume(i1)