[SCEV] Compute symbolic exit count for 'and' conditions

[mkazantsev]

Summary

If loop exits by condition like A < B && X < Y, and at least one of symbolic max
exit counts for these conditions is known, it can be used as estimate of symbolic
max exit count for whole branch. If both are known, then we can use their umin
as the estimate.

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

9006

This looks fishy to me, but one of tests is failing without this. It looks like we can make an improvement somewhere else to get rid of two checks above, but I haven't figured how it happens.

[nikic]

llvm/lib/Analysis/ScalarEvolution.cpp

8718

Why the new condition here?

llvm/test/Analysis/ScalarEvolution/widenable-condition.ll

27 ↗

(On Diff #480380)

I don't really get why this patch introduces these changes (i.e. why this wasn't the result previously). Aren't we already assigning the constant max to the symbol max if there is no exact?

[nikic]

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

227

I'm missing a test for the case where we actually produce a umin_seq.

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

8718

The old logic was: put to ExitCounts whenever an exact count is known. Then, when we request loop's exact exit count, we traverse through them and take umin.

Now in the test symbolic_max_exit_count.ll exact is not known. But we still want to put it into this vector to be able to request symbolic exit count.

That's why now we put it if either exact or symbolic is known. I think we can relax it to just symbolic (exact always implies it).

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

227

In fact we have it in test/Analysis/ScalarEvolution/exit-count-select-safe.ll. This patch preserves current behavior, however if I remove /*IsSequential*/ true, it changes. Is it enough or you want a new one specifically for this?

llvm/test/Analysis/ScalarEvolution/widenable-condition.ll

27 ↗

(On Diff #480380)

This is indeed strange. I will investigate.

[mkazantsev]

Planned separation into 2 pieces.

llvm/test/Analysis/ScalarEvolution/widenable-condition.ll

27 ↗

(On Diff #480380)

Funny thing, it happened exactly because I've added this

if (EL.ExactNotTaken != getCouldNotCompute() ||
    EL.SymbolicMaxNotTaken != getCouldNotCompute())

The story is simple: symbolic exit count was exaluated as constant, but then ExitCount simply wasn't added to the array because Exact was missing.

I will split it off into a separate fix.

[mkazantsev]

Now this is duing purely what it claims to do.

[nikic]

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

227

If I understand correctly, the tests in exit-count-select-safe.ll cover the case where we have an exact (but umin_seq) exit count. I think it still makes sense to have a test for the case where we don't have an exact count, but do have a symbolic umin_seq count.

We probably also want to use umin or umin_seq depending on isa<BinaryOperator>(ExitCond), same as is done for the ExactNotTaken case a few lines before the new code.

[mkazantsev]

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

227

Good point, I'll try to wright such a test.

[mkazantsev]

I've added a test which I think should end up with umin_seq, but it's umin. I don't know why, maybe a bug?

[nikic]

In D139403#3977959, @mkazantsev wrote:

I've added a test which I think should end up with umin_seq, but it's umin. I don't know why, maybe a bug?

Indeed, we were missing a umin_seq when computing the symbolic max BE count. Fixed in https://github.com/llvm/llvm-project/commit/4d97a914d7aef6c95cd95669f99e5d32899e165a.

However, this indicates that this test is still not covering the right code path: I think what you need is a nested (A1 and A2) and (B1 and B2) structure where we get symbolic counts C1 and C2 from the inner ands and then those get combined. That will give you the umin from the new code path.

[mkazantsev]

In D139403#3978183, @nikic wrote:

In D139403#3977959, @mkazantsev wrote:

I've added a test which I think should end up with umin_seq, but it's umin. I don't know why, maybe a bug?

Indeed, we were missing a umin_seq when computing the symbolic max BE count. Fixed in https://github.com/llvm/llvm-project/commit/4d97a914d7aef6c95cd95669f99e5d32899e165a.

However, this indicates that this test is still not covering the right code path: I think what you need is a nested (A1 and A2) and (B1 and B2) structure where we get symbolic counts C1 and C2 from the inner ands and then those get combined. That will give you the umin from the new code path.

Will do, but I don't quite get why. In my example, if %start_1 is 0, we will bail on 1st exit and never use %start_2. So there is no UB if start_1 = 0 and start_2 = poison. As far as I understood what umin_seq is, it's trying to address exactly this case.

[mkazantsev]

Rebased on top of more tests with combined arith and logical AND conditions.

As far as I understand the topic, it should be umin in test_two_phis_arithmetic_and and umin_seq in test_two_phis_logical_and. In practice it's umin_seq in the former case and nothing in the later.

Do we really want to block the patch on this? Looks like umin_seq requires a lot of work to apply where it's really needed.

[nikic]

llvm/lib/Analysis/ScalarEvolution.cpp

8988

This should pass !isa<BinaryOperator>(ExitCond) as in the ExactNotTaken case above.

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

560

This should be select i1 %c1, i1 %c2, i1 false. You made this an or rather than an and.

[mkazantsev]

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

560

You're right, what I've done is OR... /facepalm

Let me fix that.

[mkazantsev]

llvm/lib/Analysis/ScalarEvolution.cpp

8988

I missed that one, thanks for reminding!

[mkazantsev]

Fixed umin(seq)

[nikic]

LGTM

llvm/lib/Analysis/ScalarEvolution.cpp

for (unsigned i = 0, e = ExitingBlocks.size(); i != e; ++i) {
 
     // 1. For each exit that can be computed, add an entry to ExitCounts.
     // CouldComputeBECount is true only if all exits can be computed.
     if (EL.ExactNotTaken == getCouldNotCompute())
       // We couldn't compute an exact value for this exit, so
       // we won't be able to compute an exact value for the loop.
       CouldComputeBECount = false;
     // Remember exit count if either exact or symbolic is known. Because
     // Exact always implies symbolic, only check symbolic.
     if (EL.SymbolicMaxNotTaken != getCouldNotCompute())
       ExitCounts.emplace_back(ExitBB, EL);
     else
       assert(EL.ExactNotTaken == getCouldNotCompute() &&
              "Exact is known but symbolic isn't?");
 
     // 2. Derive the loop's MaxBECount from each exit's max number of
     // non-exiting iterations. Partition the loop exits into two kinds:
ScalarEvolution::computeExitLimitFromCondFromBinOp(
   const Constant *NeutralElement = ConstantInt::get(ExitCond->getType(), IsAnd);
   if (isa<ConstantInt>(Op1))
     return Op1 == NeutralElement ? EL0 : EL1;
   if (isa<ConstantInt>(Op0))
     return Op0 == NeutralElement ? EL1 : EL0;
 
   const SCEV *BECount = getCouldNotCompute();
   const SCEV *ConstantMaxBECount = getCouldNotCompute();
+  const SCEV *SymbolicMaxBECount = getCouldNotCompute();
   if (EitherMayExit) {
+    bool UseSequentialUMin = !isa<BinaryOperator>(ExitCond);
     // Both conditions must be same for the loop to continue executing.
     // Choose the less conservative count.
     if (EL0.ExactNotTaken != getCouldNotCompute() &&
         EL1.ExactNotTaken != getCouldNotCompute()) {
-      BECount = getUMinFromMismatchedTypes(
-          EL0.ExactNotTaken, EL1.ExactNotTaken,
-          /*Sequential=*/!isa<BinaryOperator>(ExitCond));
+      BECount = getUMinFromMismatchedTypes(EL0.ExactNotTaken, EL1.ExactNotTaken,
+                                           UseSequentialUMin);
     }
     if (EL0.ConstantMaxNotTaken == getCouldNotCompute())
       ConstantMaxBECount = EL1.ConstantMaxNotTaken;
     else if (EL1.ConstantMaxNotTaken == getCouldNotCompute())
       ConstantMaxBECount = EL0.ConstantMaxNotTaken;
     else
       ConstantMaxBECount = getUMinFromMismatchedTypes(EL0.ConstantMaxNotTaken,
                                                       EL1.ConstantMaxNotTaken);
+    if (EL0.SymbolicMaxNotTaken == getCouldNotCompute())
+      SymbolicMaxBECount = EL1.SymbolicMaxNotTaken;
+    else if (EL1.SymbolicMaxNotTaken == getCouldNotCompute())
+      SymbolicMaxBECount = EL0.SymbolicMaxNotTaken;
+    else
+      SymbolicMaxBECount = getUMinFromMismatchedTypes(
+          EL0.SymbolicMaxNotTaken, EL1.SymbolicMaxNotTaken, UseSequentialUMin);
   } else {
     // Both conditions must be same at the same time for the loop to exit.
     // For now, be conservative.
     if (EL0.ExactNotTaken == EL1.ExactNotTaken)
       BECount = EL0.ExactNotTaken;
   }
 
   // There are cases (e.g. PR26207) where computeExitLimitFromCond is able
   // to be more aggressive when computing BECount than when computing
   // ConstantMaxBECount.  In these cases it is possible for EL0.ExactNotTaken
   // and
   // EL1.ExactNotTaken to match, but for EL0.ConstantMaxNotTaken and
   // EL1.ConstantMaxNotTaken to not.
   if (isa<SCEVCouldNotCompute>(ConstantMaxBECount) &&
       !isa<SCEVCouldNotCompute>(BECount))
     ConstantMaxBECount = getConstant(getUnsignedRangeMax(BECount));
-  const SCEV *SymbolicMaxBECount =
+  if (isa<SCEVCouldNotCompute>(SymbolicMaxBECount))
+    SymbolicMaxBECount =
         isa<SCEVCouldNotCompute>(BECount) ? ConstantMaxBECount : BECount;
   return ExitLimit(BECount, ConstantMaxBECount, SymbolicMaxBECount, false,
                    { &EL0.Predicates, &EL1.Predicates });
 }
 
 ScalarEvolution::ExitLimit
 ScalarEvolution::computeExitLimitFromICmp(const Loop *L,
                                           ICmpInst *ExitCond,
                                           bool ExitIfTrue,

llvm/test/Analysis/ScalarEvolution/symbolic_max_exit_count.ll

 
 failed_1:
   ret i32 -1
 
 failed_2:
   ret i32 -2
 }
 
-; TODO: Symbolic max can be %start
 define i32 @test_litter_conditions(i32 %start, i32 %len) {
 ; CHECK-LABEL: 'test_litter_conditions'
 ; CHECK-NEXT:  Classifying expressions for: @test_litter_conditions
 ; CHECK-NEXT:    %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
 ; CHECK-NEXT:    --> {%start,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %fake_1 = call i1 @cond()
 ; CHECK-NEXT:    --> %fake_1 U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:    %and_1 = and i1 %zero_check, %fake_1

 ; CHECK-NEXT:    %loop_cond = call i1 @cond()
 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_litter_conditions
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is %start
+; CHECK-NEXT:    symbolic max exit count for loop: %start
 ; CHECK-NEXT:    symbolic max exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop:

 
 failed_1:
   ret i32 -1
 
 failed_2:
   ret i32 -2
 }
 
-; TODO: Symbolic max can be %start
 define i32 @test_litter_conditions_bad_context(i32 %start, i32 %len) {
 ; CHECK-LABEL: 'test_litter_conditions_bad_context'
 ; CHECK-NEXT:  Classifying expressions for: @test_litter_conditions_bad_context
 ; CHECK-NEXT:    %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
 ; CHECK-NEXT:    --> {%start,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %fake_1 = call i1 @cond()
 ; CHECK-NEXT:    --> %fake_1 U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:    %and_1 = and i1 %zero_check, %fake_1

 ; CHECK-NEXT:    %loop_cond = call i1 @cond()
 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_litter_conditions_bad_context
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is %start
+; CHECK-NEXT:    symbolic max exit count for loop: %start
 ; CHECK-NEXT:    symbolic max exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop:

 
 failed_1:
   ret i32 -1
 
 failed_2:
   ret i32 -2
 }
 
-; TODO: Symbolic max can be %start
 define i32 @test_and_conditions(i32 %start, i32 %len) {
 ; CHECK-LABEL: 'test_and_conditions'
 ; CHECK-NEXT:  Classifying expressions for: @test_and_conditions
 ; CHECK-NEXT:    %iv = phi i32 [ %start, %entry ], [ %iv.next, %backedge ]
 ; CHECK-NEXT:    --> {%start,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %iv.minus.1 = add i32 %iv, -1
 ; CHECK-NEXT:    --> {(-1 + %start),+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %both_checks = and i1 %zero_check, %range_check
 ; CHECK-NEXT:    --> (%range_check umin %zero_check) U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:    %iv.next = add i32 %iv, -1
 ; CHECK-NEXT:    --> {(-1 + %start),+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %loop_cond = call i1 @cond()
 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_and_conditions
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is %start
+; CHECK-NEXT:    symbolic max exit count for loop: %start
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop:
   %iv = phi i32 [%start, %entry], [%iv.next, %backedge]
   %zero_check = icmp ne i32 %iv, 0
   %iv.minus.1 = add i32 %iv, -1
   %range_check = icmp ult i32 %iv.minus.1, %len
   %both_checks = and i1 %zero_check, %range_check
   br i1 %both_checks, label %backedge, label %failed
 
 backedge:
   %iv.next = add i32 %iv, -1
   %loop_cond = call i1 @cond()
   br i1 %loop_cond, label %done, label %loop
 
 done:
   ret i32 %iv
 
 failed:
   ret i32 -3
 }
 
 define i32 @test_mixup_constant_symbolic(i32 %end, i32 %len) {
 ; CHECK-LABEL: 'test_mixup_constant_symbolic'
 ; CHECK-NEXT:  Classifying expressions for: @test_mixup_constant_symbolic
 ; CHECK-NEXT:    %iv = phi i32 [ 0, %entry ], [ %iv.next, %backedge ]
 ; CHECK-NEXT:    --> {0,+,1}<%loop> U: [0,1001) S: [0,1001) Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %iv.next = add i32 %iv, 1
 ; CHECK-NEXT:    --> {1,+,1}<%loop> U: [1,1002) S: [1,1002) Exits: <<Unknown>> LoopDispositions: { %loop: Computable }

 
 done:
   ret i32 %iv
 
 failed_1:
   ret i32 -1
 }
 
-; TODO: Symbolic max can be start1 umin_seq start2
 define i32 @test_two_phis(i32 %start_1, i32 %start_2, i32 %len) {
 ; CHECK-LABEL: 'test_two_phis'
 ; CHECK-NEXT:  Classifying expressions for: @test_two_phis
 ; CHECK-NEXT:    %iv_1 = phi i32 [ %start_1, %entry ], [ %iv_1.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_1,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %iv_2 = phi i32 [ %start_2, %entry ], [ %iv_2.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_2,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %scam_1 = call i1 @cond()

 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_two_phis
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for zero_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
-; CHECK-NEXT:    symbolic max exit count for zero_check_block: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is (%start_1 umin_seq %start_2)
+; CHECK-NEXT:    symbolic max exit count for loop: %start_1
+; CHECK-NEXT:    symbolic max exit count for zero_check_block: %start_2
 ; CHECK-NEXT:    symbolic max exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop:
backedge:
   %iv_1.next = add i32 %iv_1, -1
   %iv_2.next = add i32 %iv_2, -1
   br i1 %zero_check_2, label %loop, label %exit
 
 exit:
   ret i32 0
 }
 
-; TODO: Symbolic max can be start1 umin start2
 define i32 @test_two_phis_arithmetic_and(i32 %start_1, i32 %start_2, i32 %len) {
 ; CHECK-LABEL: 'test_two_phis_arithmetic_and'
 ; CHECK-NEXT:  Classifying expressions for: @test_two_phis_arithmetic_and
 ; CHECK-NEXT:    %iv_1 = phi i32 [ %start_1, %entry ], [ %iv_1.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_1,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %iv_2 = phi i32 [ %start_2, %entry ], [ %iv_2.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_2,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %scam_1 = call i1 @cond()

 ; CHECK-NEXT:    %loop_cond = call i1 @cond()
 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_two_phis_arithmetic_and
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is (%start_1 umin %start_2)
+; CHECK-NEXT:    symbolic max exit count for loop: (%start_1 umin %start_2)
 ; CHECK-NEXT:    symbolic max exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop:
loop:
   %iv_1 = phi i32 [%start_1, %entry], [%iv_1.next, %backedge]
   %iv_2 = phi i32 [%start_2, %entry], [%iv_2.next, %backedge]
   %scam_1 = call i1 @cond()
   %zero_check_1 = icmp ne i32 %iv_1, 0
   %c1 = and i1 %zero_check_1, %scam_1
   %scam_2 = call i1 @cond()
   %zero_check_2 = icmp ne i32 %iv_2, 0
   %c2 = and i1 %zero_check_2, %scam_2
   %merged_cond = select i1 %c1, i1 true, i1 %c2
   br i1 %merged_cond, label %range_check_block, label %failed_1
 
 range_check_block:
   %iv.minus.1 = add i32 %iv_1, -1
   %range_check = icmp ult i32 %iv.minus.1, %len
   br i1 %range_check, label %backedge, label %failed_2
 
 backedge:
   %iv_1.next = add i32 %iv_1, -1
   %iv_2.next = add i32 %iv_2, -1
   %loop_cond = call i1 @cond()
   br i1 %loop_cond, label %done, label %loop
 
 done:
   ret i32 %iv_2
 
 failed_1:
   ret i32 -1
 
 failed_2:
   ret i32 -2
 }
 
-; TODO: Symbolic max can be start1 umin_seq start2
 define i32 @test_two_phis_logical_and(i32 %start_1, i32 %start_2, i32 %len) {
 ; CHECK-LABEL: 'test_two_phis_logical_and'
 ; CHECK-NEXT:  Classifying expressions for: @test_two_phis_logical_and
 ; CHECK-NEXT:    %iv_1 = phi i32 [ %start_1, %entry ], [ %iv_1.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_1,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %iv_2 = phi i32 [ %start_2, %entry ], [ %iv_2.next, %backedge ]
 ; CHECK-NEXT:    --> {%start_2,+,-1}<%loop> U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Computable }
 ; CHECK-NEXT:    %scam_1 = call i1 @cond()

 ; CHECK-NEXT:    %loop_cond = call i1 @cond()
 ; CHECK-NEXT:    --> %loop_cond U: full-set S: full-set Exits: <<Unknown>> LoopDispositions: { %loop: Variant }
 ; CHECK-NEXT:  Determining loop execution counts for: @test_two_phis_logical_and
 ; CHECK-NEXT:  Loop %loop: <multiple exits> Unpredictable backedge-taken count.
 ; CHECK-NEXT:    exit count for loop: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: constant max backedge-taken count is -1
-; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is -1
-; CHECK-NEXT:    symbolic max exit count for loop: -1
+; CHECK-NEXT:  Loop %loop: symbolic max backedge-taken count is (%start_1 umin_seq %start_2)
+; CHECK-NEXT:    symbolic max exit count for loop: (%start_1 umin_seq %start_2)
 ; CHECK-NEXT:    symbolic max exit count for range_check_block: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:    symbolic max exit count for backedge: ***COULDNOTCOMPUTE***
 ; CHECK-NEXT:  Loop %loop: Unpredictable predicated backedge-taken count.
 ;
 entry:
   br label %loop
 
 loop: