[DA] Introduce domain for monotonicity #170684

kasuga-fj · 2025-12-04T16:26:06Z

This PR is a proposal that is derived from #162281, and not intended to be merged as is.

Current definition of monotonicity assumes its domain as [0, BTC_1] x [0, BTC_2] x ... x [0, BTC_n] without justification. In fact, the result of monotonicity check is incconsistent in the following cases:

When a loop doesn't have a predicable exact backedge-taken count.
When a loop-guard like i < 42 exists and the exact backedge-taken count of the i-loop is larger than 42.
- In this case, just checking nowrap properties of addrecs recursively is not sufficient.

To address these issues, this PR introduces a domain for monotonicity and modifies the definition of monotonicity accordingly. Also changes the interface of the monotonicity check function to explicitly take the domain as an argument. Currently the following domains are supported:

EntireDomain: [0, BTC_1] x [0, BTC_2] x ... x [0, BTC_n]
EffectiveDomain: [L_1, U_1] x [L_2, U_2] x ... x [L_n, U_n] which is a superset of the actual execution domain. Note that we don't know the actual values of L_k and U_k.
- More precisely, when we say "a function F is monotonic in EffectiveDomain", it means that there exists values L_k and U_k for all k such that
  - F is monotonic in [L_1, U_1] x [L_2, U_2] x ... x [L_n, U_n]
  - If F(i_1, i_2, ..., i_n) is actually evaluated, then L_k <= i_k <= U_k for all k.

As a first step, monotonicity checks are added in strongSIVtest and symbolicRDIVtest. In addition, independence tests that use an exact backedge-taken count have been rewritten to evaluate the addrecs at the first and last iterations, rather than relying on the existing inequality checks, which require additional overflow checks.

github-actions · 2025-12-04T16:59:48Z

🐧 Linux x64 Test Results

166750 tests passed
2909 tests skipped
4 tests failed

Failed Tests

(click on a test name to see its output)

LLVM

LLVM.Analysis/DDG/basic-b.ll

Exit Code: 1

Command Output (stdout):
--
# RUN: at line 1
/home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt < /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Analysis/DDG/basic-b.ll -disable-output "-passes=print<ddg>" 2>&1 | /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Analysis/DDG/basic-b.ll
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -disable-output '-passes=print<ddg>'
# note: command had no output on stdout or stderr
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Analysis/DDG/basic-b.ll
# .---command stderr------------
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Analysis/DDG/basic-b.ll:41:15: error: CHECK-NEXT: is not on the line after the previous match
# | ; CHECK-NEXT: Edges:
# |               ^
# | <stdin>:43:2: note: 'next' match was here
# |  Edges:
# |  ^
# | <stdin>:41:62: note: previous match ended here
# |  %arrayidx2 = getelementptr inbounds float, ptr %a, i64 %sub1
# |                                                              ^
# | <stdin>:42:1: note: non-matching line after previous match is here
# |  %1 = load float, ptr %arrayidx2, align 4
# | ^
# | 
# | Input file: <stdin>
# | Check file: /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Analysis/DDG/basic-b.ll
# | 
# | -dump-input=help explains the following input dump.
# | 
# | Input was:
# | <<<<<<
# |          .
# |          .
# |          .
# |         38: Node Address:0x33cc0360:multi-instruction 
# |         39:  Instructions: 
# |         40:  %sub1 = add i64 %i.02, -1 
# |         41:  %arrayidx2 = getelementptr inbounds float, ptr %a, i64 %sub1 
# |         42:  %1 = load float, ptr %arrayidx2, align 4 
# |         43:  Edges: 
# | next:41      !~~~~~  error: match on wrong line
# |         44:  [def-use] to 0x33cc04b0 
# |         45:  [memory] to 0x33cc0590 
# |         46:  
# |         47: Node Address:0x33cc0280:multi-instruction 
# |         48:  Instructions: 
# |          .
# |          .
# |          .
# | >>>>>>
# `-----------------------------
# error: command failed with exit status: 1

--

LLVM.Transforms/LoopFusion/da_separate_loops.ll

Exit Code: 1

Command Output (stdout):
--
# RUN: at line 3
/home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-fusion -da-disable-delinearization-checks -disable-output -stats < /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopFusion/da_separate_loops.ll 2>&1 | /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck -check-prefix=STAT /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopFusion/da_separate_loops.ll
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-fusion -da-disable-delinearization-checks -disable-output -stats
# note: command had no output on stdout or stderr
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck -check-prefix=STAT /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopFusion/da_separate_loops.ll
# .---command stderr------------
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopFusion/da_separate_loops.ll:4:9: error: STAT: expected string not found in input
# | ; STAT: 2 loop-fusion - DA checks passed
# |         ^
# | <stdin>:1:1: note: scanning from here
# | ===-------------------------------------------------------------------------===
# | ^
# | <stdin>:15:2: note: possible intended match here
# |  1 loop-fusion - DA checks passed
# |  ^
# | 
# | Input file: <stdin>
# | Check file: /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopFusion/da_separate_loops.ll
# | 
# | -dump-input=help explains the following input dump.
# | 
# | Input was:
# | <<<<<<
# |            1: ===-------------------------------------------------------------------------=== 
# | check:4'0     X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
# |            2:  ... Statistics Collected ... 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            3: ===-------------------------------------------------------------------------=== 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            4:  
# | check:4'0     ~
# |            5:  2 aa - Number of MayAlias results 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            6:  2 codemover-utils - Movement of PHINodes are not supported 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            .
# |            .
# |            .
# |           10:  4 da - Strong SIV successes 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           11:  4 da - Symbolic RDIV applications 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           12:  2 da - Array pairs tested 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           13:  1 loop-fusion - Loops fused 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           14:  2 loop-fusion - Dependencies prevent fusion 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           15:  1 loop-fusion - DA checks passed 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# | check:4'1      ?                                 possible intended match
# |           16:  4 loop-fusion - Number of candidates for loop fusion 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           17: 19 scalar-evolution - Number of loop exits with predictable exit counts 
# | check:4'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |           18:  
# | check:4'0     ~
# | >>>>>>
# `-----------------------------
# error: command failed with exit status: 1

--

LLVM.Transforms/LoopUnrollAndJam/dependencies.ll

Exit Code: 1

Command Output (stdout):
--
# RUN: at line 1
/home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-unroll-and-jam -allow-unroll-and-jam -unroll-and-jam-count=4 < /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll -S | /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-unroll-and-jam -allow-unroll-and-jam -unroll-and-jam-count=4 -S
# note: command had no output on stdout or stderr
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll
# .---command stderr------------
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll:8:10: error: CHECK: expected string not found in input
# | ; CHECK: %j.1 = phi
# |          ^
# | <stdin>:20:10: note: scanning from here
# |  %j = phi i32 [ %add6, %for.inner ], [ 0, %for.outer ]
# |          ^
# | <stdin>:21:2: note: possible intended match here
# |  %sum = phi i32 [ %add, %for.inner ], [ 0, %for.outer ]
# |  ^
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll:297:10: error: CHECK: expected string not found in input
# | ; CHECK: %j.1 = phi
# |          ^
# | <stdin>:523:10: note: scanning from here
# |  %j = phi i32 [ %add6, %for.inner ], [ 0, %for.outer ]
# |          ^
# | <stdin>:524:2: note: possible intended match here
# |  %sum = phi i32 [ %add, %for.inner ], [ 0, %for.outer ]
# |  ^
# | 
# | Input file: <stdin>
# | Check file: /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/dependencies.ll
# | 
# | -dump-input=help explains the following input dump.
# | 
# | Input was:
# | <<<<<<
# |              .
# |              .
# |              .
# |             15:  %arrayidx = getelementptr inbounds i32, ptr %A, i32 %i 
# |             16:  store i32 1, ptr %arrayidx, align 4 
# |             17:  br label %for.inner 
# |             18:  
# |             19: for.inner: ; preds = %for.inner, %for.outer 
# |             20:  %j = phi i32 [ %add6, %for.inner ], [ 0, %for.outer ] 
# | check:8'0                X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
# |             21:  %sum = phi i32 [ %add, %for.inner ], [ 0, %for.outer ] 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# | check:8'1        ?                                                       possible intended match
# |             22:  %arrayidx5 = getelementptr inbounds i32, ptr %B, i32 %j 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             23:  %0 = load i32, ptr %arrayidx5, align 4 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             24:  %mul = mul nsw i32 %0, %i 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             25:  %add = add nsw i32 %mul, %sum 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             26:  %add6 = add nuw nsw i32 %j, 1 
# | check:8'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |              .
# |              .
# |              .
# |            518: for.outer: ; preds = %for.outer.preheader, %for.latch 
# |            519:  %i = phi i32 [ %add7, %for.latch ], [ 0, %for.outer.preheader ] 
# |            520:  br label %for.inner 
# |            521:  
# |            522: for.inner: ; preds = %for.inner, %for.outer 
# |            523:  %j = phi i32 [ %add6, %for.inner ], [ 0, %for.outer ] 
# | check:297'0              X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
# |            524:  %sum = phi i32 [ %add, %for.inner ], [ 0, %for.outer ] 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# | check:297'1      ?                                                       possible intended match
# |            525:  %arrayidx5 = getelementptr inbounds i32, ptr %B, i32 %j 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            526:  %0 = load i32, ptr %arrayidx5, align 4 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            527:  %mul = mul nsw i32 %0, %i 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            528:  %add = add nsw i32 %mul, %sum 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |            529:  %add6 = add nuw nsw i32 %j, 1 
# | check:297'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |              .
# |              .
# |              .
# | >>>>>>
# `-----------------------------
# error: command failed with exit status: 1

--

LLVM.Transforms/LoopUnrollAndJam/unroll-and-jam.ll

Exit Code: 1

Command Output (stdout):
--
# RUN: at line 2
/home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-unroll-and-jam -allow-unroll-and-jam -unroll-and-jam-count=4 -unroll-remainder < /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll -S | /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/opt -passes=loop-unroll-and-jam -allow-unroll-and-jam -unroll-and-jam-count=4 -unroll-remainder -S
# note: command had no output on stdout or stderr
# executed command: /home/gha/actions-runner/_work/llvm-project/llvm-project/build/bin/FileCheck /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll
# .---command stderr------------
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll:193:15: error: CHECK-NEXT: expected string not found in input
# | ; CHECK-NEXT: [[TMP0:%.*]] = add i32 [[I]], -1
# |               ^
# | <stdin>:172:21: note: scanning from here
# | for.outer.preheader: ; preds = %entry
# |                     ^
# | <stdin>:172:21: note: with "I" equal to "%I"
# | for.outer.preheader: ; preds = %entry
# |                     ^
# | <stdin>:186:2: note: possible intended match here
# |  %add = add i32 %1, %sum
# |  ^
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll:705:15: error: CHECK-NEXT: expected string not found in input
# | ; CHECK-NEXT: [[TMP0:%.*]] = add i32 [[I]], -1
# |               ^
# | <stdin>:425:15: note: scanning from here
# | for.preheader: ; preds = %entry
# |               ^
# | <stdin>:425:15: note: with "I" equal to "%I"
# | for.preheader: ; preds = %entry
# |               ^
# | <stdin>:448:2: note: possible intended match here
# |  %add9 = add i32 %l1, %sum
# |  ^
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll:901:15: error: CHECK-NEXT: expected string not found in input
# | ; CHECK-NEXT: [[TMP0:%.*]] = add i32 [[I]], -1
# |               ^
# | <stdin>:467:15: note: scanning from here
# | for.preheader: ; preds = %entry
# |               ^
# | <stdin>:467:15: note: with "I" equal to "%I"
# | for.preheader: ; preds = %entry
# |               ^
# | <stdin>:488:2: note: possible intended match here
# |  %add9 = add i32 %l1, %sum
# |  ^
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll:1462:12: error: undefined variable: LOOP6
# | ; CHECK: [[LOOP6]] = distinct !{[[LOOP6]], [[META5]]}
# |            ^
# | /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll:1462:35: error: undefined variable: LOOP6
# | ; CHECK: [[LOOP6]] = distinct !{[[LOOP6]], [[META5]]}
# |                                   ^
# | <stdin>:822:36: note: with "META5" equal to "!5"
# | !5 = !{!"llvm.loop.unroll.disable"}
# |                                    ^
# | <stdin>:823:2: note: possible intended match here
# | !6 = distinct !{!6, !5}
# |  ^
# | 
# | Input file: <stdin>
# | Check file: /home/gha/actions-runner/_work/llvm-project/llvm-project/llvm/test/Transforms/LoopUnrollAndJam/unroll-and-jam.ll
# | 
# | -dump-input=help explains the following input dump.
# | 
# | Input was:
# | <<<<<<
# |               .
# |               .
# |               .
# |             167:  %cmp = icmp ne i32 %E, 0 
# |             168:  %cmp125 = icmp ne i32 %I, 0 
# |             169:  %or.cond = and i1 %cmp, %cmp125 
# |             170:  br i1 %or.cond, label %for.outer.preheader, label %for.end10 
# |             171:  
# |             172: for.outer.preheader: ; preds = %entry 
# | next:193'0                           X~~~~~~~~~~~~~~~~~ error: no match found
# | next:193'1                                              with "I" equal to "%I"
# |             173:  br label %for.outer 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~
# |             174:  
# | next:193'0       ~
# |             175: for.outer: ; preds = %for.latch, %for.outer.preheader 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             176:  %i = phi i32 [ %add9, %for.latch ], [ 0, %for.outer.preheader ] 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             177:  %arrayidx = getelementptr inbounds i32, ptr %A, i32 %i 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             181: for.inner: ; preds = %for.inner, %for.outer 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             182:  %j = phi i32 [ 0, %for.outer ], [ %inc, %for.inner ] 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             183:  %sum = phi i32 [ %0, %for.outer ], [ %add, %for.inner ] 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             184:  %arrayidx6 = getelementptr inbounds i32, ptr %B, i32 %j 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             185:  %1 = load i32, ptr %arrayidx6, align 4, !tbaa !0 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             186:  %add = add i32 %1, %sum 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~
# | next:193'2        ?                        possible intended match
# |             187:  %inc = add nuw i32 %j, 1 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             188:  %exitcond = icmp eq i32 %inc, %E 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             189:  br i1 %exitcond, label %for.latch, label %for.inner 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             190:  
# | next:193'0       ~
# |             191: for.latch: ; preds = %for.inner 
# | next:193'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             420:  %cmp = icmp ne i32 %E, 0 
# |             421:  %cmp128 = icmp ne i32 %I, 0 
# |             422:  %or.cond = and i1 %cmp128, %cmp 
# |             423:  br i1 %or.cond, label %for.preheader, label %for.end 
# |             424:  
# |             425: for.preheader: ; preds = %entry 
# | next:705'0                     X~~~~~~~~~~~~~~~~~ error: no match found
# | next:705'1                                        with "I" equal to "%I"
# |             426:  br label %for.outer 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~
# |             427:  
# | next:705'0       ~
# |             428: for.outer: ; preds = %for.latch, %for.preheader 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             429:  %i = phi i32 [ %add, %for.latch ], [ 0, %for.preheader ] 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             430:  %arrayidx = getelementptr inbounds i32, ptr %A, i32 %i 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             443: for.inner: ; preds = %for.inner, %for.outer 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             444:  %sum = phi i32 [ 0, %for.outer ], [ %add9, %for.inner ] 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             445:  %j = phi i32 [ 0, %for.outer ], [ %add10, %for.inner ] 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             446:  %arrayidx7 = getelementptr inbounds i32, ptr %B, i32 %j 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             447:  %l1 = load i32, ptr %arrayidx7, align 4, !tbaa !0 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             448:  %add9 = add i32 %l1, %sum 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~
# | next:705'2        ?                          possible intended match
# |             449:  %add10 = add nuw i32 %j, 1 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             450:  %exitcond = icmp eq i32 %add10, %E 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             451:  br i1 %exitcond, label %for.latch, label %for.inner 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             452:  
# | next:705'0       ~
# |             453: for.end.loopexit: ; preds = %for.latch 
# | next:705'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             462:  %cmp = icmp eq i32 %E, 0 
# |             463:  %cmp336 = icmp eq i32 %I, 0 
# |             464:  %or.cond = or i1 %cmp, %cmp336 
# |             465:  br i1 %or.cond, label %for.end, label %for.preheader 
# |             466:  
# |             467: for.preheader: ; preds = %entry 
# | next:901'0                     X~~~~~~~~~~~~~~~~~ error: no match found
# | next:901'1                                        with "I" equal to "%I"
# |             468:  br label %for.outest 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~
# |             469:  
# | next:901'0       ~
# |             470: for.outest: ; preds = %for.cleanup, %for.preheader 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             471:  %x.038 = phi i32 [ %inc, %for.cleanup ], [ 0, %for.preheader ] 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             472:  br label %for.outer 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             483: for.inner: ; preds = %for.inner, %for.outer 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             484:  %sum = phi i32 [ 0, %for.outer ], [ %add9, %for.inner ] 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             485:  %j = phi i32 [ 0, %for.outer ], [ %add10, %for.inner ] 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             486:  %arrayidx11 = getelementptr inbounds i32, ptr %B, i32 %j 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             487:  %l1 = load i32, ptr %arrayidx11, align 4, !tbaa !0 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             488:  %add9 = add i32 %l1, %sum 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~
# | next:901'2        ?                          possible intended match
# |             489:  %add10 = add nuw i32 %j, 1 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             490:  %exitcond = icmp eq i32 %add10, %E 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             491:  br i1 %exitcond, label %for.latch, label %for.inner 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             492:  
# | next:901'0       ~
# |             493: for.latch: ; preds = %for.inner 
# | next:901'0       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |               .
# |               .
# |               .
# |             817: !0 = !{!1, !1, i64 0} 
# |             818: !1 = !{!"int", !2, i64 0} 
# |             819: !2 = !{!"omnipotent char", !3, i64 0} 
# |             820: !3 = !{!"Simple C/C++ TBAA"} 
# |             821: !4 = distinct !{!4, !5} 
# |             822: !5 = !{!"llvm.loop.unroll.disable"} 
# | check:1462'0                                        X error: match failed for invalid pattern
# | check:1462'1                                          undefined variable: LOOP6
# | check:1462'2                                          undefined variable: LOOP6
# | check:1462'3                                          with "META5" equal to "!5"
# |             823: !6 = distinct !{!6, !5} 
# | check:1462'0     ~~~~~~~~~~~~~~~~~~~~~~~~
# | check:1462'4      ?                       possible intended match
# |             824: !7 = !{!8, !8, i64 0} 
# | check:1462'0     ~~~~~~~~~~~~~~~~~~~~~~
# |             825: !8 = !{!"short", !2, i64 0} 
# | check:1462'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# |             826: !9 = distinct !{!9, !5} 
# | check:1462'0     ~~~~~~~~~~~~~~~~~~~~~~~~
# |             827: !10 = distinct !{!10, !5} 
# | check:1462'0     ~~~~~~~~~~~~~~~~~~~~~~~~~~
# | >>>>>>
# `-----------------------------
# error: command failed with exit status: 1

--

If these failures are unrelated to your changes (for example tests are broken or flaky at HEAD), please open an issue at https://github.com/llvm/llvm-project/issues and add the infrastructure label.

kasuga-fj added 3 commits December 4, 2025 10:37

move monotonicity definition to header file

3dbf4fd

remove -da-enable-monotonicity-check

34b46d0

introduce domain for monotonicity

38c0bac

kasuga-fj requested review from Meinersbur, amehsan, sebpop and sjoerdmeijer December 4, 2025 16:26

kasuga-fj mentioned this pull request Dec 4, 2025

[DA] Add tests for nsw doesn't hold on entire iteration space (NFC) #162281

Open

kasuga-fj added 2 commits December 5, 2025 01:35

apply monotonicity check for strong siv

3fb1bd1

apply monotonicity check for symbolic rdiv

e54ced2

kasuga-fj force-pushed the da-propose-monotonicity-domain branch from c78fba0 to e54ced2 Compare December 4, 2025 16:35

fix ci error

74dbf4c

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[DA] Introduce domain for monotonicity #170684

[DA] Introduce domain for monotonicity #170684

Uh oh!

kasuga-fj commented Dec 4, 2025

Uh oh!

github-actions bot commented Dec 4, 2025 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

[DA] Introduce domain for monotonicity #170684

Are you sure you want to change the base?

[DA] Introduce domain for monotonicity #170684

Uh oh!

Conversation

kasuga-fj commented Dec 4, 2025

Uh oh!

github-actions bot commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🐧 Linux x64 Test Results

Failed Tests

LLVM

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions bot commented Dec 4, 2025 •

edited

Loading