[PATCH] D103096: [analyzer] Implement cast for ranges of symbolic integers.

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

It sounds like you indeed solved a lot of problems that prevented us from enabling `SymbolCast`. But this still requires //massive// testing, a lot more than a typical constraint solver patch; extraordinary claims require extraordinary evidence. If it works out though, it might be the best thing to happen to the static analyzer in years.

With `SymbolCast`s in place our equations become much more complicated and therefore the constraint solver becomes much more likely to produce false positives in cases where it previously erred on the side of false negatives.

Another thing to test is our ability to explain bug paths. People are often careless about integral types and it may lead to bugs which your patch helps uncover. But it is worthless to uncover these bugs if the user can't understand them. I'm thinking of scenarios like this:

  01  void foo(long x) {
  02    if (x == 0)
  03      return;
  04
  05    bar(x, nullptr);
  06  }
  07
  08  void bar(int y, int *p) {
  09    if (y == 0)
  10      *p = 1; // warning: null dereference
  11  }

The user will discard this as false positive because "I checked for zero in foo(), it obviously can't be zero in bar() in this context". There needs to be a note that explains the implicit truncation of an interesting* symbol on line 5. Maybe even mention truncation on line 9 as well (not sure how to word that).

I also wonder if a lot of such reports will also be false positives simply because the presumption of potential overflow is baseless. On paper it looks like "if the user didn't want to pass large values, they'd just use `int` instead of `long`". But in practice there may be other reasons to use a larger integer type, such as API requirements (eg., how `isascii()` accepts an `int` but only uses 266 values). There's also the usual problem of overflow being impossible specifically on the current path; in this case we have to make sure that an appropriate `assert()` would actually suppress the warning (i.e., the constraint solver would be able to correctly solve the assert condition as well).

__
*In this case it's interesting as a control flow dependency of the bug location; it sounds like without @Szelethus's control flow dependency tracking this advancement would have been virtually impossible.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103096/new/

https://reviews.llvm.org/D103096