forked from OSchip/llvm-project
[Analyzer][Core] Make SValBuilder to better simplify svals with 3 symbols in the tree
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.) Differential Revision: https://reviews.llvm.org/D103317
This commit is contained in:
parent
f02c5f3478
commit
0a17896fe6
|
@ -1102,7 +1102,6 @@ const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
|
||||||
if (SymbolRef Sym = V.getAsSymbol())
|
if (SymbolRef Sym = V.getAsSymbol())
|
||||||
return state->getConstraintManager().getSymVal(state, Sym);
|
return state->getConstraintManager().getSymVal(state, Sym);
|
||||||
|
|
||||||
// FIXME: Add support for SymExprs.
|
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1134,6 +1133,24 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
|
||||||
return cache(Sym, SVB.makeSymbolVal(Sym));
|
return cache(Sym, SVB.makeSymbolVal(Sym));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Return the known const value for the Sym if available, or return Undef
|
||||||
|
// otherwise.
|
||||||
|
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 UndefinedVal();
|
||||||
|
}
|
||||||
|
|
||||||
|
SVal getConstOrVisit(SymbolRef Sym) {
|
||||||
|
const SVal Ret = getConst(Sym);
|
||||||
|
if (Ret.isUndef())
|
||||||
|
return Visit(Sym);
|
||||||
|
return Ret;
|
||||||
|
}
|
||||||
|
|
||||||
public:
|
public:
|
||||||
Simplifier(ProgramStateRef State)
|
Simplifier(ProgramStateRef State)
|
||||||
: State(State), SVB(State->getStateManager().getSValBuilder()) {}
|
: State(State), SVB(State->getStateManager().getSValBuilder()) {}
|
||||||
|
@ -1147,15 +1164,14 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
|
||||||
return SVB.makeSymbolVal(S);
|
return SVB.makeSymbolVal(S);
|
||||||
}
|
}
|
||||||
|
|
||||||
// TODO: Support SymbolCast. Support IntSymExpr when/if we actually
|
// TODO: Support SymbolCast.
|
||||||
// start producing them.
|
|
||||||
|
|
||||||
SVal VisitSymIntExpr(const SymIntExpr *S) {
|
SVal VisitSymIntExpr(const SymIntExpr *S) {
|
||||||
auto I = Cached.find(S);
|
auto I = Cached.find(S);
|
||||||
if (I != Cached.end())
|
if (I != Cached.end())
|
||||||
return I->second;
|
return I->second;
|
||||||
|
|
||||||
SVal LHS = Visit(S->getLHS());
|
SVal LHS = getConstOrVisit(S->getLHS());
|
||||||
if (isUnchanged(S->getLHS(), LHS))
|
if (isUnchanged(S->getLHS(), LHS))
|
||||||
return skip(S);
|
return skip(S);
|
||||||
|
|
||||||
|
@ -1187,9 +1203,10 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
|
||||||
if (I != Cached.end())
|
if (I != Cached.end())
|
||||||
return I->second;
|
return I->second;
|
||||||
|
|
||||||
SVal RHS = Visit(S->getRHS());
|
SVal RHS = getConstOrVisit(S->getRHS());
|
||||||
if (isUnchanged(S->getRHS(), RHS))
|
if (isUnchanged(S->getRHS(), RHS))
|
||||||
return skip(S);
|
return skip(S);
|
||||||
|
|
||||||
SVal LHS = SVB.makeIntVal(S->getLHS());
|
SVal LHS = SVB.makeIntVal(S->getLHS());
|
||||||
return cache(
|
return cache(
|
||||||
S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
|
S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
|
||||||
|
@ -1208,8 +1225,9 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
|
||||||
Loc::isLocType(S->getRHS()->getType()))
|
Loc::isLocType(S->getRHS()->getType()))
|
||||||
return skip(S);
|
return skip(S);
|
||||||
|
|
||||||
SVal LHS = Visit(S->getLHS());
|
SVal LHS = getConstOrVisit(S->getLHS());
|
||||||
SVal RHS = Visit(S->getRHS());
|
SVal RHS = getConstOrVisit(S->getRHS());
|
||||||
|
|
||||||
if (isUnchanged(S->getLHS(), LHS) && isUnchanged(S->getRHS(), RHS))
|
if (isUnchanged(S->getLHS(), LHS) && isUnchanged(S->getRHS(), RHS))
|
||||||
return skip(S);
|
return skip(S);
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,76 @@
|
||||||
|
// 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 SValBuilder is capable to simplify existing
|
||||||
|
// compound SVals (where there are at leaset 3 symbols in the tree) based on
|
||||||
|
// newly added constraints.
|
||||||
|
|
||||||
|
void clang_analyzer_eval(bool);
|
||||||
|
void clang_analyzer_warnIfReached();
|
||||||
|
|
||||||
|
void test_left_tree_constrained(int x, int y, int z) {
|
||||||
|
if (x + y + z != 0)
|
||||||
|
return;
|
||||||
|
if (x + y != 0)
|
||||||
|
return;
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_right_tree_constrained(int x, int y, int z) {
|
||||||
|
if (x + y * z != 0)
|
||||||
|
return;
|
||||||
|
if (y * z != 0)
|
||||||
|
return;
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_left_tree_constrained_minus(int x, int y, int z) {
|
||||||
|
if (x - y - z != 0)
|
||||||
|
return;
|
||||||
|
if (x - y != 0)
|
||||||
|
return;
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_SymInt_constrained(int x, int y, int z) {
|
||||||
|
if (x * y * z != 4)
|
||||||
|
return;
|
||||||
|
if (z != 2)
|
||||||
|
return;
|
||||||
|
if (x * y == 3) {
|
||||||
|
clang_analyzer_warnIfReached(); // no-warning
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
(void)(x * y * z);
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_SValBuilder_simplifies_IntSym(int x, int y, int z) {
|
||||||
|
// Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder.
|
||||||
|
// Division is one exception.
|
||||||
|
x = 77 / (y + z);
|
||||||
|
if (y + z != 1)
|
||||||
|
return;
|
||||||
|
clang_analyzer_eval(x == 77); // expected-warning{{TRUE}}
|
||||||
|
(void)(x * y * z);
|
||||||
|
}
|
||||||
|
|
||||||
|
void recurring_symbol(int b) {
|
||||||
|
if (b * b != b)
|
||||||
|
if ((b * b) * b * b != (b * b) * b)
|
||||||
|
if (b * b == 1) // no-crash (assert should not fire)
|
||||||
|
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
|
||||||
|
}
|
|
@ -59,7 +59,7 @@ void taintTracking(int x) {
|
||||||
int tty = xy.y; // expected-warning + {{tainted}}
|
int tty = xy.y; // expected-warning + {{tainted}}
|
||||||
}
|
}
|
||||||
|
|
||||||
void BitwiseOp(int in, char inn) {
|
void BitwiseOp(int in, char inn, int zz) {
|
||||||
// Taint on bitwise operations, integer to integer cast.
|
// Taint on bitwise operations, integer to integer cast.
|
||||||
int m;
|
int m;
|
||||||
int x = 0;
|
int x = 0;
|
||||||
|
@ -67,11 +67,12 @@ void BitwiseOp(int in, char inn) {
|
||||||
int y = (in << (x << in)) * 5;// expected-warning + {{tainted}}
|
int y = (in << (x << in)) * 5;// expected-warning + {{tainted}}
|
||||||
// The next line tests integer to integer cast.
|
// The next line tests integer to integer cast.
|
||||||
int z = y & inn; // expected-warning + {{tainted}}
|
int z = y & inn; // expected-warning + {{tainted}}
|
||||||
if (y == 5) // expected-warning + {{tainted}}
|
if (y == zz) { // expected-warning + {{tainted}}
|
||||||
m = z | z;// expected-warning + {{tainted}}
|
m = z | z;// expected-warning + {{tainted}}
|
||||||
|
}
|
||||||
else
|
else
|
||||||
m = inn;
|
m = inn;
|
||||||
int mm = m; // expected-warning + {{tainted}}
|
int mm = m; // expected-warning 1 {{tainted}}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Test getenv.
|
// Test getenv.
|
||||||
|
|
Loading…
Reference in New Issue