baloghadamsoftware updated this revision to Diff 109117.
baloghadamsoftware added a comment.
Overflow scenarios skipped.
https://reviews.llvm.org/D35109
Files:
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/svalbuilder-rearrange-comparisons.c
Index: test/Analysis/svalbuilder-rearrange-comparisons.c
===================================================================
--- /dev/null
+++ test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,163 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_dump(int x);
+void clang_analyzer_eval(int x);
+void clang_analyzer_printState();
+
+int f();
+
+void compare_different_symbol() {
+ int x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int() {
+ int x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int() {
+ int x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int() {
+ int x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int() {
+ int x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int() {
+ int x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int() {
+ int x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int() {
+ int x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int() {
+ int x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol() {
+ int x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int() {
+ int x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int() {
+ int x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_right_int() {
+ int x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_right_int() {
+ int x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int() {
+ int x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int() {
+ int x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int() {
+ int x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int() {
+ int x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void overflow(signed char n, signed char m) {
+ if (n + 0 >= m + 0) {
+ clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}}
+ }
+}
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -554,6 +554,93 @@
if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
+ // If comparing two symbolic expressions of the format S, S+n or S-n
+ // rearrange the comparison by moving symbols to the left side and the
+ // concrete integer to the right. This enables the range based constraint
+ // manager to handle these comparisons.
+ if (BinaryOperator::isComparisonOp(op) &&
+ rhs.getSubKind() == nonloc::SymbolValKind) {
+ SymbolRef rSym = rhs.castAs<nonloc::SymbolVal>().getSymbol();
+ if (Sym->getType() == rSym->getType() &&
+ Sym->getType()->isSignedIntegerOrEnumerationType()) {
+ // FIXME: Support unsigned types using signed differences
+ const llvm::APSInt *lInt = nullptr, *rInt = nullptr;
+ BinaryOperator::Opcode lop, rop;
+
+ // Type of n in S+n or S-n is the same as the type of S+n or S-n.
+ // Since they are equal on both sides, no need to convert them.
+ if (const SymIntExpr *lSymIntExpr = dyn_cast<SymIntExpr>(Sym)) {
+ lop = lSymIntExpr->getOpcode();
+ if (BinaryOperator::isAdditiveOp(lop)) {
+ lInt = &lSymIntExpr->getRHS();
+ Sym = lSymIntExpr->getLHS();
+ }
+ }
+ if (const SymIntExpr *rSymIntExpr = dyn_cast<SymIntExpr>(rSym)) {
+ rop = rSymIntExpr->getOpcode();
+ if (BinaryOperator::isAdditiveOp(rop)) {
+ rInt = &rSymIntExpr->getRHS();
+ rSym = rSymIntExpr->getLHS();
+ }
+ }
+
+ bool reverse; // Avoid negative numbers in case of unsigned types
+ bool overflow = false;
+ const llvm::APSInt *newRhs;
+ if (lInt && rInt) {
+ int64_t newRhsExt;
+ if (lop != rop) {
+ newRhsExt = lInt->getExtValue() + rInt->getExtValue();
+ reverse = (lop == BO_Add);
+ } else {
+ if (*lInt >= *rInt) {
+ newRhsExt = lInt->getExtValue() - rInt->getExtValue();
+ reverse = (lop == BO_Add);
+ } else {
+ newRhsExt = rInt->getExtValue() - lInt->getExtValue();
+ reverse = (lop == BO_Sub);
+ }
+ }
+ newRhs = &BasicVals.getValue(newRhsExt, Sym->getType());
+ overflow =
+ (newRhsExt >
+ BasicVals.getAPSIntType(Sym->getType()).getMaxValue()) ||
+ (newRhsExt <
+ BasicVals.getAPSIntType(Sym->getType()).getMinValue());
+ // FIXME: Extend the type of the difference in case of overflow.
+ // Now we just skip this scenario.
+ } else if (lInt) {
+ newRhs = lInt;
+ reverse = (lop == BO_Add);
+ } else if (rInt) {
+ newRhs = rInt;
+ reverse = (rop == BO_Sub);
+ } else {
+ newRhs = &BasicVals.getValue(0, Sym->getType());
+ reverse = false;
+ }
+
+ if (!overflow) {
+ // If the two symbols are equal, compare only the integers and
+ // return the concrete result. If they are different, return the
+ // rearranged expression.
+ if (Sym == rSym) {
+ return nonloc::ConcreteInt(*BasicVals.evalAPSInt(
+ op, BasicVals.getValue(0, Sym->getType()), *newRhs));
+ } else {
+ if (reverse) {
+ op = BinaryOperator::reverseComparisonOp(op);
+ }
+ const SymExpr *newLhs =
+ reverse
+ ? SymMgr.getSymSymExpr(rSym, BO_Sub, Sym, Sym->getType())
+ : SymMgr.getSymSymExpr(Sym, BO_Sub, rSym, Sym->getType());
+ return makeNonLoc(newLhs, op, *newRhs, resultTy);
+ }
+ }
+ }
+ }
+
// Give up -- this is not a symbolic expression we can handle.
return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
