martong created this revision.
martong added reviewers: steakhal, ASDenysPetrov, manas, NoQ, vsavchenko.
Herald added subscribers: 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.
The solver's symbol simplification mechanism was not able to handle cases
when a symbol is simplified to a concrete integer. This patch adds the
capability.
E.g., in the attached lit test case, the original symbol is `c + 1` and
it has a `[0, 0]` range associated with it. Then, a new condition `c == 0`
is assumed, so a new range constraint `[0, 0]` comes in for `c` and
simplification kicks in. `c + 1` becomes `0 + 1`, but the associated
range is `[0, 0]`, so now we are able to realize the contradiction.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D110913
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
clang/test/Analysis/solver-sym-simplification-concreteint.c
Index: clang/test/Analysis/solver-sym-simplification-concreteint.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-concreteint.c
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_to_concrete_int(int b, int c) {
+ if (b < 0 || b > 1) // b: [0,1]
+ return;
+ if (c < 0 || c > 1) // c: [0,1]
+ return;
+ if (c + b != 0) // c + b == 0
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1 == 0
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+ // c == 0 --> 0 + 1 == 0 contradiction
+ clang_analyzer_eval(c == 0); // expected-warning{{FALSE}}
+
+ // c == 1 --> 1 + 1 == 0 contradiction
+ clang_analyzer_eval(c != 0); // expected-warning{{FALSE}}
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -226,9 +226,13 @@
}
}
-SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym) {
SValBuilder &SVB = State->getStateManager().getSValBuilder();
- SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+ return SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+}
+
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
return SimplifiedSym;
return Sym;
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2096,7 +2096,19 @@
ProgramStateRef State, EquivalenceClass Class) {
SymbolSet ClassMembers = Class.getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
+
+ SymbolRef SimplifiedMemberSym = nullptr;
+ SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
+ if (const auto CI = SimplifiedMemberVal.getAs<nonloc::ConcreteInt>()) {
+ const llvm::APSInt &SV = CI->getValue();
+ const RangeSet *ClassConstraint = getConstraint(State, Class);
+ // We have found a contradiction.
+ if (ClassConstraint && !ClassConstraint->contains(SV))
+ return nullptr;
+ } else {
+ SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();
+ }
+
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
// The simplified symbol should be the member of the original Class,
// however, it might be in another existing class at the moment. We
Index:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
---
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -390,6 +390,9 @@
/// Try to simplify a given symbolic expression's associated value based on the
/// constraints in State. This is needed because the Environment bindings are
/// not getting updated when a new constraint is added to the State.
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+/// If the symbol is simplified to a constant then it returns the original
+/// symbol.
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
} // namespace ento
Index: clang/test/Analysis/solver-sym-simplification-concreteint.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-concreteint.c
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_to_concrete_int(int b, int c) {
+ if (b < 0 || b > 1) // b: [0,1]
+ return;
+ if (c < 0 || c > 1) // c: [0,1]
+ return;
+ if (c + b != 0) // c + b == 0
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1 == 0
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+ // c == 0 --> 0 + 1 == 0 contradiction
+ clang_analyzer_eval(c == 0); // expected-warning{{FALSE}}
+
+ // c == 1 --> 1 + 1 == 0 contradiction
+ clang_analyzer_eval(c != 0); // expected-warning{{FALSE}}
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -226,9 +226,13 @@
}
}
-SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym) {
SValBuilder &SVB = State->getStateManager().getSValBuilder();
- SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+ return SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+}
+
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
return SimplifiedSym;
return Sym;
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2096,7 +2096,19 @@
ProgramStateRef State, EquivalenceClass Class) {
SymbolSet ClassMembers = Class.getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
+
+ SymbolRef SimplifiedMemberSym = nullptr;
+ SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
+ if (const auto CI = SimplifiedMemberVal.getAs<nonloc::ConcreteInt>()) {
+ const llvm::APSInt &SV = CI->getValue();
+ const RangeSet *ClassConstraint = getConstraint(State, Class);
+ // We have found a contradiction.
+ if (ClassConstraint && !ClassConstraint->contains(SV))
+ return nullptr;
+ } else {
+ SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();
+ }
+
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
// The simplified symbol should be the member of the original Class,
// however, it might be in another existing class at the moment. We
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -390,6 +390,9 @@
/// Try to simplify a given symbolic expression's associated value based on the
/// constraints in State. This is needed because the Environment bindings are
/// not getting updated when a new constraint is added to the State.
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+/// If the symbol is simplified to a constant then it returns the original
+/// symbol.
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
} // namespace ento
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
