[PATCH] [analyzer] [patch] Path-sensitive different.IntegerOverflow checker

[Anna Zaks]

Hi Julia,

Thanks for working on this!

In general, we prefer to get incremental patches rather than something that is close to the end-result. That way it is easier to get the guidance along the way and easier for a reviewer to review.

Here are some high level comments. 

The package name lacks description. 

It would be very helpful to differentiate the overflows that are considered undefined behavior from the ones that are defined. I would have 2 checkers for these, to allow users to turn them on/off independently. However, this might be a separate future improvement.

Could you add more documentation in doxygen style as well as a high level description of the algorithm? 

After briefly looking at the patch, I am still not sure how exactly "ExternalSym" is used. Looks like you are tracking symbols that the analyzer may not have values for (like globals). But that should not be needed: if a value is not known by the analyzer you can determine that when evaluating the overflow check. Specifically, State->assume() returns two states, which you can use to find out which situation you are dealing with:
 - there was an overflow
 - there was no overflow
 - under constrained or unknown - this would correspond to the case where both states are feasible.
There should be other posts on the mailing list describing this API as well as other uses of it throughout the analyzer.

Also, I did not notice tests that are testing these heuristics...

The error message seems to be constructed prematurely and I do not see any tests that test it fully.

Another checker that is somewhat related to this one is the String API checker. One reason why it is still in alpha is that it was very difficult to interpret the reports; most of which were due to overflows earlier on the path. It would be very interesting to see how this checker works on various codebases (with respect to bugs found vs false positives). 

Cheers,
Anna.

================
Comment at: lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp:35
@@ +34,3 @@
+  mutable std::unique_ptr<BuiltinBug> BT;
+
+  mutable std::set<SourceLocation> OverflowLoc;
----------------
Are you getting multiple reports on the same location? I don't think that should be happening - the bug reporting infrastructure should unique reports.

================
Comment at: lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp:349
@@ +348,3 @@
+
+// Don't track global variables and class members we can't reason about.
+bool
----------------
Need a better comment here - the function returns a bool.
Also, comments should be in doxygen form and added to the declarations.

================
Comment at: lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp:446
@@ +445,3 @@
+}
+
+ProgramStateRef
----------------
addGoodSink seem to add a symbol to a state. Looks like it's used to track symbols we are not supposed to diagnose - symbols with global state? Could you add a better comment/name here?

Sink has a very specific meaning in the analyzer - it's a node at which the simulation stops. Usually, it's used for unrecoverable error nodes.

================
Comment at: lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp:498
@@ +497,3 @@
+  addRangeInformation(Lhs, C, LValue);
+
+  if (makeGlobalsMembersHeuristics(Lhs, ExprLhs, C)) {
----------------
It looks like you are building an error message string before the issue is diagnosed..

http://reviews.llvm.org/D4066