[PATCH] D22862: [analyzer] Fix for PR15623: eliminate unwanted ProgramState checker data propagation.

[Devin Coughlin via cfe-commits]

dcoughlin added a comment.

As PR15623 shows, returning the existing cast is not correct. But rather than replace it with an unknown, here is a proposal for how to address this without regressing in precision.

Instead of using `assumeDual()` in `ExprEngine::VisitLogicalExpr()` on the `RHSVal` and returning 0, 1, or `Unknown()` depending on whether the true and false states are empty, we can return a symbolic expression representing "RHSVal != 0":

  nonloc::ConcreteInt Zero(getBasicVals().getValue(0, B->getType()));
  X = evalBinOp(N->getState(), BO_NE, getSValBuilder().evalCast(RHSVal, B->getType(), RHS->getType()), Zero, B->getType());

Now, `evalBinOp()` is ultimately doing its own `assumeDual()` under the hood, so at a high level this should do the same thing as we had before for the 0 and 1 cases -- and it will return a new symbol rather than the casted RHSVal (which is what causing the false positive leaks) when the assumption is unknown.

Unfortunately, this can easily create symbolic expressions of the form "((reg_$1<n>) == 0U) != 0", which the analyzer currently doesn't handle very well. Right now when assumed, that symbolic expression gets translated into a range constraint saying the symbol (reg_$1<n>) == 0U) is in [1, UINTMAX] rather than a range constraint saying that reg_$1<n> is in [0,0] as we might expect. This means that we lose precision in cases like:

  if ((n == 0) != 0) {
    clang_analyzer_eval(n == 0); // This should be TRUE but we really currently get UNKNOWN
  }

So my proposal is to teach `SimpleConstraintManager::assumeSymRel()` to simplify an assume of a constraint of the form: "(exp comparison_op expr) != 0" to true into an assume of "exp comparison_op expr" to true. (And similarly, an assume of the form  "(exp comparison_op expr) == 0" to true as an assume of `exp comparison_op expr` to false.) This should be quite a small change.

This approach would improve precision overall, simplify `ExprEngine::VisitLogicalExpr()`, and avoid the leak false positive from PR15623 without causing the regression in misc-ps-region-store.m that Anna is worried about.

Does this seem reasonable?


https://reviews.llvm.org/D22862