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

Denys Petrov via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon May 31 06:02:51 PDT 2021


ASDenysPetrov added a comment.

@NoQ
This solution only intends to make correct calculations whenever cast occures. We can mark this as //alpha// or add an argument flag to turn cast reasoning on/off, or we can even disable any part of this patch with argument settings.

> But this still requires //massive// testing, a lot more than a typical constraint solver patch; extraordinary claims require extraordinary evidence.

What kind of tests do you think we need?

> If it works out though, it might be the best thing to happen to the static analyzer in years.

Thank you. I appreciate your possitive evaluation.

> 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.

My proposition is to design and describe a paper of:

- what cases shall be considered as erroneous and be reported;
- what cases shall be ignored or considered as exceptions (i.e. static_cast);
- what wordings shall we use in reports;
- how paths of those reports shall look like;
- //your options;//

> 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).

IMO this is great when we tell user that he/she should make sure of the value bounds before passing the arguments to such APIs.

> 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).

For example, this test easily passes.

  void test(int x) {
    assert(0 < x && x < 42);
    char c = x;
    clang_analyzer_eval(c <= 0); // expected-warning {{FALSE}}
    clang_analyzer_eval(c >= 42); // expected-warning {{FALSE}}
  }

Or you meant some other cases?

> __
> *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.

Can this tracking mechanism be adjusted then?

In the end, should we go further with this patch and make more adjustments in CSA or reject it in view of your concerns?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103096



More information about the cfe-commits mailing list