[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

Compared with https://reviews.llvm.org/D28953, this revision fixes the test failure with `PR3991.m` with RangeConstraintManager, and a few other failures with Z3ConstraintManager. However, there's one remaining test failure in `range_casts.c` that I'm not sure how to resolve. For reference, this is the simplified code snippet from that testcase:

  void f15(long foo) {
    unsigned index = -1;
    if (index < foo) index = foo;
    unsigned int tmp = index + 1;
    if (tmp == 0)
      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
    else
      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  }

In debug mode, an assertion about the system being over-constrained is thrown from `ConstraintManager.h`. This is because the new `Simplifier::VisitSymbolCast` function will attempt to evaluate the cast `(unsigned int) (reg_$0<long foo>)`, which is suppressed by the call to `haveSameType()` in `SimpleSValBuilder::evalCastFromNonLoc` (https://reviews.llvm.org/D28955 fixes this, but only for Z3ConstraintManager), generating just the symbol `reg_$0<long foo>`. Subsequently, the analyzer will attempt to evaluate the expression `((reg_$0<long foo>) + 1U) == 0U` with the range `reg_$0<long foo> : { [4294967296, 9223372036854775807] }`, or `[UINT_MAX + 1, LONG_MAX]`. However, in the case where the assumption is true, RangeConstraintManager takes the intersection of the previous range with `[UINT_MAX, UINT_MAX]` and produces the empty set, and likewise where the assumption is false, the intersection with `[UINT_MAX - 1, 0]` again produces the empty set. As a result, both program states are NULL, triggering the assertion.

I'm now somewhat inclined to drop the addition of `Simplified::VisitSymbolCast()` and those associated testsuite changes, because ignoring type casts is clearly incorrect and will introduce both false negatives and false positives.


https://reviews.llvm.org/D35450