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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
