Fix for PR15623. The patch eliminates unwanted ProgramState checker data propagation from an operand of the logical operation to operation result.

The patch also simplifies 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.) which improves precision overall.
https://reviews.llvm.org/D22862

llvm-svn: 290413
This commit is contained in:
Anton Yartsev 2016-12-23 03:31:00 +00:00
parent 00d734d89b
commit 1a2a9e3087
4 changed files with 43 additions and 18 deletions

View File

@ -665,23 +665,13 @@ void ExprEngine::VisitLogicalExpr(const BinaryOperator* B, ExplodedNode *Pred,
if (RHSVal.isUndef()) {
X = RHSVal;
} else {
DefinedOrUnknownSVal DefinedRHS = RHSVal.castAs<DefinedOrUnknownSVal>();
ProgramStateRef StTrue, StFalse;
std::tie(StTrue, StFalse) = N->getState()->assume(DefinedRHS);
if (StTrue) {
if (StFalse) {
// We can't constrain the value to 0 or 1.
// The best we can do is a cast.
X = getSValBuilder().evalCast(RHSVal, B->getType(), RHS->getType());
} else {
// The value is known to be true.
X = getSValBuilder().makeIntVal(1, B->getType());
}
} else {
// The value is known to be false.
assert(StFalse && "Infeasible path!");
X = getSValBuilder().makeIntVal(0, B->getType());
}
// We evaluate "RHSVal != 0" expression which result in 0 if the value is
// known to be false, 1 if the value is known to be true and a new symbol
// when the assumption is unknown.
nonloc::ConcreteInt Zero(getBasicVals().getValue(0, B->getType()));
X = evalBinOp(N->getState(), BO_NE,
svalBuilder.evalCast(RHSVal, B->getType(), RHS->getType()),
Zero, B->getType());
}
}
Bldr.generateNode(B, Pred, state->BindExpr(B, Pred->getLocationContext(), X));

View File

@ -254,6 +254,21 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
assert(BinaryOperator::isComparisonOp(Op) &&
"Non-comparison ops should be rewritten as comparisons to zero.");
SymbolRef Sym = LHS;
// Simplification: translate 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 into an assume of
// "exp comparison_op expr" to false.)
if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym)) {
BinaryOperator::Opcode Op = SE->getOpcode();
if (BinaryOperator::isComparisonOp(Op))
return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
}
}
// Get the type used for calculating wraparound.
BasicValueFactory &BVF = getBasicVals();
APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
@ -265,7 +280,6 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
// x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
// in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
// the subclasses of SimpleConstraintManager to handle the adjustment.
SymbolRef Sym = LHS;
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
computeAdjustment(Sym, Adjustment);

View File

@ -1763,6 +1763,17 @@ void testConstEscapeThroughAnotherField() {
constEscape(&(s.x)); // could free s->p!
} // no-warning
// PR15623
int testNoCheckerDataPropogationFromLogicalOpOperandToOpResult(void) {
char *param = malloc(10);
char *value = malloc(10);
int ok = (param && value);
free(param);
free(value);
// Previously we ended up with 'Use of memory after it is freed' on return.
return ok; // no warning
}
// ----------------------------------------------------------------------------
// False negatives.

View File

@ -191,3 +191,13 @@ static void PR16131(int x) {
clang_analyzer_eval(*ip == 42); // expected-warning{{TRUE}}
clang_analyzer_eval(*(int *)&v == 42); // expected-warning{{TRUE}}
}
// PR15623: Currently the analyzer doesn't handle symbolic expressions of the
// form "(exp comparison_op expr) != 0" very well. We perform a simplification
// translating 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.
void PR15623(int n) {
if ((n == 0) != 0) {
clang_analyzer_eval(n == 0); // expected-warning{{TRUE}}
}
}