martong created this revision.
martong added reviewers: vsavchenko, NoQ, steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy,
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware,
xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Add the capability to simplify more complex constraints where there are 3
symbols in the tree. In this change I extend simplifySVal to query constraints
of children sub-symbols in a symbol tree. (The constraint for the parent is
asked in `getKnownValue`.) This change makes the following cases to pass
(notice the 3rd check in each test-case).
This patch is the second step of a sequence of patches, and not intended to be
commited as a standalone change. The sequence of patches (and the plan) is
described here: https://reviews.llvm.org/D102696#2784624
int test_left_tree_constrained(int x, int y, int z) {
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}}
clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
x = y = z = 1;
return 0;
}
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D103317
Files:
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
clang/test/Analysis/simplify-complex-constraints.cpp
Index: clang/test/Analysis/simplify-complex-constraints.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/simplify-complex-constraints.cpp
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config eagerly-assume=false \
+// RUN: -verify
+
+// Here we test whether the analyzer is capable to simplify existing
+// constraints based on newly added constraints on a sub-expression.
+
+void clang_analyzer_eval(bool);
+
+int test_left_tree_constrained(int x, int y, int z) {
+ 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}}
+ clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
+ x = y = z = 1;
+ return 0;
+}
+
+int test_right_tree_constrained(int x, int y, int z) {
+ if (x + (y + z) != 0)
+ return 0;
+ if (y + z != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == 0); // expected-warning{{TRUE}}
+ return 0;
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -1107,7 +1107,6 @@
if (SymbolRef Sym = V.getAsSymbol())
return state->getConstraintManager().getSymVal(state, Sym);
- // FIXME: Add support for SymExprs.
return nullptr;
}
@@ -1139,6 +1138,15 @@
return cache(Sym, SVB.makeSymbolVal(Sym));
}
+ SVal getConst(SymbolRef Sym) {
+ const llvm::APSInt *Const =
+ State->getConstraintManager().getSymVal(State, Sym);
+ if (Const)
+ return Loc::isLocType(Sym->getType()) ? (SVal)SVB.makeIntLocVal(*Const)
+ : (SVal)SVB.makeIntVal(*Const);
+ return SVal();
+ }
+
public:
Simplifier(ProgramStateRef State)
: State(State), SVB(State->getStateManager().getSValBuilder()) {}
@@ -1152,15 +1160,16 @@
return SVB.makeSymbolVal(S);
}
- // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
- // start producing them.
+ // TODO: Support SymbolCast.
SVal VisitSymIntExpr(const SymIntExpr *S) {
auto I = Cached.find(S);
if (I != Cached.end())
return I->second;
- SVal LHS = Visit(S->getLHS());
+ SVal LHS = getConst(S->getLHS());
+ if (LHS.isUndef())
+ LHS = Visit(S->getLHS());
if (isUnchanged(S->getLHS(), LHS))
return skip(S);
@@ -1187,6 +1196,22 @@
S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
}
+ SVal VisitIntSymExpr(const IntSymExpr *S) {
+ auto I = Cached.find(S);
+ if (I != Cached.end())
+ return I->second;
+
+ SVal RHS = getConst(S->getRHS());
+ if (RHS.isUndef())
+ RHS = Visit(S->getRHS());
+ if (isUnchanged(S->getRHS(), RHS))
+ return skip(S);
+
+ SVal LHS = SVB.makeIntVal(S->getLHS());
+ return cache(
+ S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
+ }
+
SVal VisitSymSymExpr(const SymSymExpr *S) {
auto I = Cached.find(S);
if (I != Cached.end())
@@ -1200,8 +1225,13 @@
Loc::isLocType(S->getRHS()->getType()))
return skip(S);
- SVal LHS = Visit(S->getLHS());
- SVal RHS = Visit(S->getRHS());
+ SVal LHS = getConst(S->getLHS());
+ if (LHS.isUndef())
+ LHS = Visit(S->getLHS());
+ SVal RHS = getConst(S->getRHS());
+ if (RHS.isUndef())
+ RHS = Visit(S->getRHS());
+
if (isUnchanged(S->getLHS(), LHS) && isUnchanged(S->getRHS(), RHS))
return skip(S);
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
