fix(flow): handle lesser array length guards

[lewis6991]

Problem

Array length guards using < or <= did not narrow arrays on their
complementary false branches. Explicit empty else blocks also dropped the
reachable branch, so guarded indexes remained nullable.

Solution

• reuse the existing lower-bound narrowing for complementary less-than branches
• preserve condition flow through explicit empty else blocks
• clamp exclusive array bounds at i64::MAX to avoid inference overflow

Fixes #1207

[github-actions]

I'll analyze this code change for potential issues:

Issues Found

1. Logic Error in OpLt and OpLe Handling (Critical)

In binary_flow.rs, the handling for OpLt and OpLe appears incorrect:

// Current code:
BinaryOperator::OpLt => try_get_at_array_len_expr(
    ...
    condition_flow.invert(),
    0,  // This should be 1 for `>` equivalent
),

BinaryOperator::OpLe => try_get_at_array_len_expr(
    ...
    condition_flow.invert(),
    1,  // This should be 0 for `>=` equivalent
),

The comments say "The false branches are equivalent to >= and > respectively", but:

• OpLt inverted (false branch) should be equivalent to >=, which requires max_adjustment = 0
• OpLe inverted (false branch) should be equivalent to >, which requires max_adjustment = 1

The current code has these swapped, which could lead to off-by-one errors in array length narrowing.

2. Potential Overflow Issue in max_adjustment

In mod.rs, the code uses saturating_add to handle overflow:

let max_len = i.saturating_add(*max_adjustment);

This is good, but consider that max_adjustment could be negative in future use cases. The function signature allows i64, but currently only passes 0 or 1. If negative values are passed in the future, saturating_add would clamp to i64::MIN, which might not be the intended behavior.

3. Incomplete Test Coverage

The tests added don't cover:

• The OpLt and OpLe cases (only <= and < are tested)
• The swapped adjustment values mentioned in issue #1
• Edge cases with negative array lengths

4. Naming Consistency

The function renamed from try_get_at_gt_or_ge_expr to try_get_at_array_len_expr is more accurate, but the parameter max_adjustment could be better named as exclusive_bound_adjustment or similar to clarify its purpose.

5. Potential Issue with has_else_clause Removal

In engine.rs, the removal of has_else_clause and the unconditional add_antecedent call:

// Before:
if !has_else_clause {
    self.binder.add_antecedent(post_if, else_label);
}

// After:
self.binder.add_antecedent(post_if, else_label);

This change means the antecedent is always added, even when there's an else clause. This could potentially affect flow analysis when there's an else block, as the else_label might not be properly connected. The test test_issue_1207_empty_else_preserves_array_length_guard covers an empty else, but not a non-empty else block.

Recommendations

1. Fix the swapped adjustments for OpLt and OpLe:

BinaryOperator::OpLt => try_get_at_array_len_expr(
    ...
    condition_flow.invert(),
    0,  // For `>=` equivalent
),
BinaryOperator::OpLe => try_get_at_array_len_expr(
    ...
    condition_flow.invert(),
    1,  // For `>` equivalent
),

2. Add tests for:

   • if #a > 1 then and if #a >= 1 then cases
   • Non-empty else blocks to verify the has_else_clause removal doesn't break flow analysis

3. Consider documenting the max_adjustment parameter's semantics (0 for inclusive bounds, 1 for exclusive bounds)

4. Add validation or assertions that max_adjustment is only 0 or 1 if that's the intended usage