[clang] ac3edc5 - [analyzer][solver] Handle simplification to ConcreteInt
Gabor Marton via cfe-commits
cfe-commits at lists.llvm.org
Thu Oct 14 08:53:45 PDT 2021
Author: Gabor Marton
Date: 2021-10-14T17:53:29+02:00
New Revision: ac3edc5af09947210d8f8d25ddd7e42379ef6454
URL: https://github.com/llvm/llvm-project/commit/ac3edc5af09947210d8f8d25ddd7e42379ef6454
DIFF: https://github.com/llvm/llvm-project/commit/ac3edc5af09947210d8f8d25ddd7e42379ef6454.diff
LOG: [analyzer][solver] Handle simplification to ConcreteInt
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.
Differential Revision: https://reviews.llvm.org/D110913
Added:
clang/test/Analysis/solver-sym-simplification-concreteint.c
Modified:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
index c1d2b4665f1d3..599e4ec812a1b 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -389,11 +389,22 @@ class RangedConstraintManager : public SimpleConstraintManager {
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
};
-/// 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.
+/// Try to simplify a given symbolic expression 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. If the symbol is
+/// simplified to a non-symbol (e.g. to a constant) then the original symbol
+/// is returned. We use this function in the family of assumeSymNE/EQ/LT/../GE
+/// functions where we can work only with symbols. Use the other function
+/// (simplifyToSVal) if you are interested in a simplification that may yield
+/// a concrete constant value.
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
+/// Try to simplify a given symbolic expression's associated `SVal` based on the
+/// constraints in State. This is very similar to `simplify`, but this function
+/// always returns the simplified SVal. The simplified SVal might be a single
+/// constant (i.e. `ConcreteInt`).
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+
} // namespace ento
} // namespace clang
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 8299486938850..d1113569c59db 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2106,7 +2106,20 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
ProgramStateRef State, EquivalenceClass Class) {
SymbolSet ClassMembers = Class.getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
+
+ const SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
+ const SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();
+
+ // The symbol is collapsed to a constant, check if the current State is
+ // still feasible.
+ 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;
+ }
+
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
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index d227c025fb203..80f3054a5a37f 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -226,9 +226,13 @@ void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
}
}
-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;
diff --git a/clang/test/Analysis/solver-sym-simplification-concreteint.c b/clang/test/Analysis/solver-sym-simplification-concreteint.c
new file mode 100644
index 0000000000000..bfd25eb4f59e5
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-concreteint.c
@@ -0,0 +1,40 @@
+// 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_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_to_concrete_int_infeasible(int b, int c) {
+ if (c + b != 0) // c + b == 0
+ return;
+ if (b != 1) // b == 1 --> c + 1 == 0
+ return;
+ if (c != 1) // c == 1 --> 1 + 1 == 0 contradiction
+ return;
+ clang_analyzer_warnIfReached(); // no-warning
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
+
+void test_simplification_to_concrete_int_feasible(int b, int c) {
+ if (c + b != 0)
+ return;
+ // c + b == 0
+ if (b != 1)
+ return;
+ // b == 1 --> c + 1 == 0
+ if (c != -1)
+ return;
+ // c == -1 --> -1 + 1 == 0 OK
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ clang_analyzer_eval(c == -1); // expected-warning{{TRUE}}
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
More information about the cfe-commits
mailing list