martong updated this revision to Diff 346966.
martong added a comment.
- Add test case for commutativity
- Add test case for Valeriy's case
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D102696/new/
https://reviews.llvm.org/D102696
Files:
clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
clang/test/Analysis/find-binop-constraints.cpp
Index: clang/test/Analysis/find-binop-constraints.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/find-binop-constraints.cpp
@@ -0,0 +1,117 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config eagerly-assume=false \
+// RUN: -verify
+
+void clang_analyzer_eval(bool);
+
+int test_legacy_behavior(int x, int y) {
+ if (y != 0)
+ return 0;
+ if (x + y != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return y / (x + y); // expected-warning{{Division by zero}}
+}
+
+int test_rhs_further_constrained(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_lhs_further_constrained(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (x != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_lhs_and_rhs_further_constrained(int x, int y) {
+ if (x % y != 1)
+ return 0;
+ if (x != 1)
+ return 0;
+ if (y != 1)
+ return 0;
+ clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 1); // expected-warning{{TRUE}}
+ return 0;
+}
+
+// Docement that we fail in this case: "y + x" should be zero if "x + y" is
+// constrainted.
+int test_commutativity(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(y + x == 0); // expected-warning{{UNKNOWN}} FIXME!
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
+ switch (a) {
+ case 1: {
+ if (x + y + z != 0)
+ return 0;
+ if (z != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 2: {
+ if (x + y + z != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 3: {
+ if (x + y + z != 0)
+ return 0;
+ if (x != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 4: {
+ if (x + y + z != 0)
+ return 0;
+ if (x + y != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 5: {
+ if (z != 0)
+ return 0;
+ if (x + y + z != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ break;
+ }
+
+ }
+ return 0;
+}
Index: clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -10,8 +10,9 @@
//
//===----------------------------------------------------------------------===//
-#include "clang/AST/ExprCXX.h"
#include "clang/AST/DeclCXX.h"
+#include "clang/AST/ExprCXX.h"
+#include "clang/AST/StmtVisitor.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
@@ -37,10 +38,47 @@
return Symbol;
}
+// This class is responsible to build such an SVal for a BinOp expression where
+// all constituent SVals are representing an LValue expression. We use it to
+// query constraints that are attached directly to the BinOp.
+class LValueSValBuilder : public ConstStmtVisitor<LValueSValBuilder, SVal> {
+ QualType T;
+ const LocationContext *LCtx;
+ ProgramStateRef State;
+ SValBuilder &SvalBuilder;
+
+public:
+ LValueSValBuilder(QualType T, const LocationContext *LCtx,
+ ProgramStateRef State, SValBuilder &SvalBuilder)
+ : T(T), LCtx(LCtx), State(State), SvalBuilder(SvalBuilder) {}
+
+ SVal VisitImplicitCastExpr(const ImplicitCastExpr *E) {
+ if (E->getCastKind() == CK_LValueToRValue) {
+ SVal LValue = State->getSVal(E->getSubExpr(), LCtx); // LValue.
+ if (Optional<Loc> LValueLoc = LValue.getAs<Loc>())
+ return State->getRawSVal(*LValueLoc, T);
+ }
+ return SVal();
+ }
+ SVal VisitBinaryOperator(const BinaryOperator *B) {
+ SVal L = Visit(B->getLHS());
+ SVal R = Visit(B->getRHS());
+ if (L.isUndef() || R.isUndef())
+ return SVal();
+ Optional<NonLoc> LNL = L.getAs<NonLoc>();
+ Optional<NonLoc> RNL = R.getAs<NonLoc>();
+ if (!LNL || !RNL)
+ return SVal();
+ SVal SymSym =
+ SvalBuilder.makeSymExprValNN(B->getOpcode(), *LNL, *RNL, B->getType());
+ return SymSym;
+ }
+ SVal VisitExpr(const Expr *E) { return SVal(); }
+};
+
void ExprEngine::VisitBinaryOperator(const BinaryOperator* B,
ExplodedNode *Pred,
ExplodedNodeSet &Dst) {
-
Expr *LHS = B->getLHS()->IgnoreParens();
Expr *RHS = B->getRHS()->IgnoreParens();
@@ -95,9 +133,19 @@
if (B->getOpcode() == BO_PtrMemD)
state = createTemporaryRegionIfNeeded(state, LCtx, LHS);
- // Process non-assignments except commas or short-circuited
- // logical expressions (LAnd and LOr).
- SVal Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
+ SVal Result;
+ // Query any constraint that may be directly attached to the BinOp.
+ SVal LValueSymExpr =
+ LValueSValBuilder(B->getType(), LCtx, state, svalBuilder).Visit(B);
+ const llvm::APSInt *KnownInt =
+ state->getStateManager().getConstraintManager().getSymVal(
+ state, LValueSymExpr.getAsSymbol());
+ if (KnownInt)
+ Result = svalBuilder.makeIntVal(*KnownInt);
+ // Fall-back to the constant folding mechanism.
+ if (Result.isUndef())
+ Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
+
if (!Result.isUnknown()) {
state = state->BindExpr(B, LCtx, Result);
} else {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
