C++: Support < reasoning for switch statements in Guards library

[MathiasVP]

This is the final PR we need to fully support switch statement support in the Guards library 🎉 This PR is the < version of #15958 that ensures that we can know the lower and upper bounds given by case statements such as:

switch(i) {
  case 0 ... 10:
    // i >= 0 and i < 11 in here
    break;
}

Commit-by-commit review recommended

[jketema]

switch(i) {
  case 0 ... 10:

I'm assuming case 0 ... 10 is something you see in the IR? Because it's not valid C++ as far as I know.

[MathiasVP]

I'm assuming case 0 ... 10 is something you see in the IR? Because it's not valid C++ as far as I know.

It's valid: https://ideone.com/uMpD6M 😄

[jketema]

Oh, it some gcc extension https://godbolt.org/z/Wvqc1ceTs

[jketema]

My head is starting to spin a bit 😅 This adds more cases that look very similar to the cases that were already there, so I tend to believe this is all correct, but it feels a bit subtle.

[MathiasVP]

My head is starting to spin a bit 😅 This adds more cases that look very similar to the cases that were already there, so I tend to believe this is all correct, but it feels a bit subtle.

That's very fair! Yeah, there are many predicates that does similar things in this file. Before my changes we had:

1. a collection of predicates to reason about "binary equalities" (i.e., e1 == e2 + k)
2. a collection of predicates to reason about "binary inequalities" (i.e., e1 < e2 + k)

and now that we're supporting switch statements and cases we also have:
a. a collection of predicates to reason about "unary equalities" (i.e., e == k)
b. a collection of predicates to reason about "unary inequalities" (i.e., e < k)

which means we basically have 4 groups that look very much the same, and have basically the same set of cases, but subtle differ in what the base cases does.

It may be possible to define a parameterized module to group some of 1. and 2. together and another parameterized module to group some of a. and b. together. Ideally, we'd want to group 1. and a. together, and 2. and b. together, but since they deal with different number of parameters (since one is "binary" and one is "unary") I'm not sure it'll be very easy 😢