C++: Range analysis not picking up on condition because of implicit casts

[criemen]

Description of the issue

void test(unsigned long count) {
    for (int i = 0; i < count - 2; ++i) {
        sink(i);
    }
}

By looking at the code, we would expect a bound of the form i <= count -3 at the sink call.
However, because of the implicit conversion from int to unsigned long (which is not a safeCast),
the range analysis ignores the condition.

A case should be added to the RA that handles this.

[geoffw0]

Hi, if count = 0, the loop is entered with i = 0. In this case, i <= count - 3 evaluates to true as a C expression (due to the conversion), but it doesn't hold as a mathematical expression.

[criemen]

Thanks for the explanation!
So this is actually part of the behaviour that the RA doesn't model under/overflow.

Still, the slightly modified example of

void test19(unsigned long count) {
  if (count < 3) {
    return;
  }
  for (int i = 0; i < count - 2; ++i) {
      sink(i);
  }
}

shows that no "back-porting" of bounds on i (converted to unsigned long) happens to i (non-converted). I think if the RA can prove that count -2 >= 0, (i.e. no underflow occurs), it would be safe to have i <= count - 3.
The only soundness violation would be if the expression on the RHS is count +1 and there's overflow happening, but that is not handled in other parts of the RA, either.

[jbj]

These examples certainly show that handling type conversions is no trivial matter. Indeed it can be a source of security vulnerabilities. In your examples, if an attacker can set count to a sufficiently large number, then i will likely overflow before reaching it and lead to an infinite loop (actually undefined behaviour).