Conflict over overflowing the integer

I’m kinda playin with clang static analyzer. I got this interesting case .
int var = INT_MAX + 1;
okay I got the expected warning for this .
But for this, I don’t !

int var = INT_MAX ;
var++;

I’m assuming , they might be different at low level in some aspects but not sure . Pls tell me about this unusal behavior.

Are you sure that the warning you got for “int var = INT_MAX + 1;” was generated by the Static Analyzer and not a compiler warning?
As far as I am aware, there are no SA checkers that detect integer overflows/underflows.

How did you invoke the static analyzer? Did you use scan-build, code checker or clang directly?

Ya , I got it now that there is not integer overflow checker in csa . I wasn’t aware of that. By the way Did you know any tool that captures this behavior? And I used clang --analyze, afair!.

Okay , I think I missed something , warning is not by the analyzer, it is by the undefined sanitizer but again this thing is not catched by the sanitizer , int c = __INT_MAX__ ; and then ++c;

Yea, well. This is either a bug or a feature. I’m not sure right now which exactly.
One should try to fix it and see how the analysis changes, and which tests get broken.

That being said, the ExprEngine will dispatch using the VisitBinOp() (or smth similar) to interpret the operation in the symbolic domain. Which will eventually call probably SValBuilder::evalBinOpNN() which in turn correctly recognizes that an overflow would happen and wraps around; so returns some nonloc::ConcreteInt wrapping the wrapped value. It should have returned UndefinedVal, since the result of the signed overflow is undefined behavior, which will be caught by some checker enforcing that a BinOp operands should not be undefined.

If you decide to experiment with fixing this, you should not only produce UndefinedVal in that case, but also provide the mechanisms explaining what produced that offending value. But I won’t express those steps here right now.

Thanks for looking it. I’ll surely look into the codebase but yeah maybe it’s more like a bug for the normal users. I was trying to doing the same thing in the rust

fn main() {
let mut max = std::u32::MAX;
max+=1;
}

In rust there is no increment and decrement operator , so with max+=1, the compiler is throwing the expected error , this

error: this arithmetic operation will overflow
 --> src/main.rs:5:1
  |
 | max+=1;
  | ^^^^^^ attempt to compute `u32::MAX + 1_u32`, which would overflow
  |

I think we should try something similar with clang.

I’m not saying that it’s impossible. But right now it’s that easy to emit reports from the ExprEngine, which internally the SValBuilder constructs the symbolic representation of the calculation.

Let’s take a very similar warning: division by zero.
ExprEngine::VisitBinaryOperator() evaluates the BO_Div, with delegates the computation to the
SValBuilder::evalBinOp(), which itself cannot/shouldn’t emit reports.
We could probably follow something that the UndefResultChecker does.
check::PostStmt<BinOp>, early return if the result of the operation is not Undef.
If it turns out to be Undef, we should inspect that none of the operands were previously Undef, thus this binop resulted in UB, and now comes the hard part:
figuring out why did the Engine/SVB associated Undef with the operator.
To do this, we would implement basically the same logic that resides in the SValBuilder - at least on the paths where it returns Undef.

What we could do instead is to make SValBuilder possible to report the reason why did something result in Undef. Possibly by adding an additional (defaulted) parameter
for an output parameter in some form.
However, it would require consensus and a strong foundation for doing so.

My personal opinion is that we should have preserved the cause of the Undef in some way or another. Implementing this sort of backward reasoning/reverse-engineering and finding/guessing on how a given Undef was produced simply won’t scale.