[clang] 888af47 - [Analyzer][solver] Simplification: reorganize equalities with adjustment
Gabor Marton via cfe-commits
cfe-commits at lists.llvm.org
Wed Oct 27 07:49:12 PDT 2021
Author: Gabor Marton
Date: 2021-10-27T16:48:55+02:00
New Revision: 888af47095d5a7121c1d78566df59c292f30ceaf
URL: https://github.com/llvm/llvm-project/commit/888af47095d5a7121c1d78566df59c292f30ceaf
DIFF: https://github.com/llvm/llvm-project/commit/888af47095d5a7121c1d78566df59c292f30ceaf.diff
LOG: [Analyzer][solver] Simplification: reorganize equalities with adjustment
Initiate the reorganization of the equality information during symbol
simplification. E.g., if we bump into `c + 1 == 0` during simplification
then we'd like to express that `c == -1`. It makes sense to do this only
with `SymIntExpr`s.
Reviewed By: steakhal
Differential Revision: https://reviews.llvm.org/D111642
Added:
clang/test/Analysis/solver-sym-simplification-adjustment.c
Modified:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
Removed:
################################################################################
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index e75a207ee86ab..77f97da4322b3 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -602,10 +602,9 @@ class EquivalenceClass : public llvm::FoldingSetNode {
areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
/// Iterate over all symbols and try to simplify them.
- LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
- RangeSet::Factory &F,
- ProgramStateRef State,
- EquivalenceClass Class);
+ LLVM_NODISCARD static inline ProgramStateRef
+ simplify(SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM,
+ ProgramStateRef State, EquivalenceClass Class);
void dumpToStream(ProgramStateRef State, raw_ostream &os) const;
LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
@@ -1729,7 +1728,8 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
ClassMembersTy Members = State->get<ClassMembers>();
for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
EquivalenceClass Class = ClassToSymbolSet.first;
- State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+ State =
+ EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
if (!State)
return false;
SimplifiedClasses.insert(Class);
@@ -1743,7 +1743,8 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
EquivalenceClass Class = ClassConstraint.first;
if (SimplifiedClasses.count(Class)) // Already simplified.
continue;
- State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+ State =
+ EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
if (!State)
return false;
}
@@ -2126,9 +2127,9 @@ inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
// class to this class. This way, we simplify not just the symbols but the
// classes as well: we strive to keep the number of the classes to be the
// absolute minimum.
-LLVM_NODISCARD ProgramStateRef
-EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
- ProgramStateRef State, EquivalenceClass Class) {
+LLVM_NODISCARD ProgramStateRef EquivalenceClass::simplify(
+ SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM,
+ ProgramStateRef State, EquivalenceClass Class) {
SymbolSet ClassMembers = Class.getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
@@ -2149,9 +2150,30 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
// The simplified symbol should be the member of the original Class,
// however, it might be in another existing class at the moment. We
// have to merge these classes.
+ ProgramStateRef OldState = State;
State = merge(F, State, MemberSym, SimplifiedMemberSym);
if (!State)
return nullptr;
+ // No state change, no merge happened actually.
+ if (OldState == State)
+ continue;
+
+ // Initiate the reorganization of the equality information. E.g., if we
+ // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+ // sense to do this only with `SymIntExpr`s.
+ // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+ // them.
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SimplifiedMemberSym)) {
+ if (const RangeSet *ClassConstraint = getConstraint(State, Class)) {
+ // Overestimate the individual Ranges with the RangeSet' lowest and
+ // highest values.
+ State = RCM.assumeSymInclusiveRange(
+ State, SIE, ClassConstraint->getMinValue(),
+ ClassConstraint->getMaxValue(), /*InRange=*/true);
+ if (!State)
+ return nullptr;
+ }
+ }
}
}
return State;
diff --git a/clang/test/Analysis/solver-sym-simplification-adjustment.c b/clang/test/Analysis/solver-sym-simplification-adjustment.c
new file mode 100644
index 0000000000000..f83e9a4f1fcd1
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-adjustment.c
@@ -0,0 +1,111 @@
+// 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_adjustment_concrete_int(int b, int c) {
+ if (b < 0 || b > 1) // b: [0,1]
+ return;
+ if (c < -1 || c > 1) // c: [-1,1]
+ return;
+ if (c + b != 0) // c + b == 0
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1 == 0 --> c == -1
+ return;
+ 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;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+ if (b < 0 || b > 1) // b: [0,1]
+ return;
+ if (c < -1 || c > 1) // c: [-1,1]
+ return;
+ if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1]
+ return;
+ // c: [-2,-1] is intersected with the
+ // already associated range which is [-1,1],
+ // thus we get c: [-1,-1]
+ 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;
+}
+
+void test_simplification_adjustment_to_infeasible_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 --> c == -1 contradiction
+ clang_analyzer_eval(b == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(c == 0); // expected-warning{{TRUE}}
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+ }
+ clang_analyzer_warnIfReached(); // no warning
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(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 < -1 || c + b > 0) // c + b: [-1,0]
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+ return;
+ clang_analyzer_warnIfReached(); // no warning
+
+ // Keep the symbols and the constraints! alive.
+ (void)(b * c);
+ return;
+}
+
+void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
+ if (a == b) // a != b
+ return;
+ if (c != 0) // c == 0
+ return;
+
+ if (b != 0) // b == 0
+ return;
+ // The above simplification of `b == 0` could result in an infinite loop
+ // unless we detect that the State is unchanged.
+ // The loop:
+ // 1) Simplification of the trivial equivalence class
+ // "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }"
+ // results in
+ // "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" }
+ // which in turn creates a non-trivial equivalence class
+ // [ "(reg_$0<int a>) == (reg_$1<int b>)", "(reg_$0<int a>) == 0" ]
+ // 2) We call assumeSymInclusiveRange("(reg_$0<int a>) == 0")
+ // and that calls **simplify** on the associated non-trivial equivalence
+ // class. During the simplification the State does not change, we reached
+ // the fixpoint.
+
+ (void)(a * b * c);
+}
More information about the cfe-commits
mailing list