[clang] deed195 - [analyzer] Prune infeasible states related to concrete ints early to fix a crash (#210912)
via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 29 05:27:16 PDT 2026
Author: Arseniy Zaostrovnykh
Date: 2026-07-29T14:27:11+02:00
New Revision: deed195c31f0ece487aa5ef79c90633860f10b93
URL: https://github.com/llvm/llvm-project/commit/deed195c31f0ece487aa5ef79c90633860f10b93
DIFF: https://github.com/llvm/llvm-project/commit/deed195c31f0ece487aa5ef79c90633860f10b93.diff
LOG: [analyzer] Prune infeasible states related to concrete ints early to fix a crash (#210912)
RangedConstraintManager discards a simplified symbol if it reduces to a
concrete integer. This leads to delayed realization that some state
might be infeasible (because the concrete integer does not fit in the
assumed range), which might produce unexpected null pointers on the
following state splits.
PthreadLockChecker has fallen just into this trap. It assumes
`pthread_mutex_lock` is always called in a feasible state, which is was
not true.
In particular, in ZFS the analyzer crashes when runs in CTU mode because
it reaches `pthread_mutex_lock()` in over-constraint state (see the
reduced example in the first commit).
Checkers rely on the invariant that a state split can never result in
both `StateRef`s being null. To fix this violation of the invariant,
this patch helps RangedConstraintManager to realize a state is
infeasible and abort its exploration early so no follow-up state split
produce unexpected null-null pair.
Assisted by Claude Opus 4.8
--
CPP-8665
Added:
clang/test/Analysis/simplify-drops-concrete.c
Modified:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
clang/test/Analysis/pthreadlock.c
clang/test/Analysis/z3/z3-crosscheck.c
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
index 4ed4d3c738444..6b7b94cd3319c 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -478,20 +478,8 @@ class RangedConstraintManager : public SimpleConstraintManager {
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
};
-/// 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`).
+/// constraints in State.
SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
} // namespace ento
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 94dcdaf327689..fa385bd602070 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -20,10 +20,29 @@ namespace ento {
RangedConstraintManager::~RangedConstraintManager() {}
+/// Is \p Assumption (i.e. "the condition is non-zero") inconsistent with a
+/// symbol that simplified to the concrete integer \p V?
+static bool isConcreteInfeasible(const llvm::APSInt &V, bool Assumption) {
+ return (V != 0) ? !Assumption : Assumption;
+}
+
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ if (const auto *CI = SimplifiedVal.getAsInteger()) {
+ // The assumption might be incompatible with the concrete integer after the
+ // simplification.
+ if (isConcreteInfeasible(*CI, Assumption))
+ return nullptr;
+ // When the fold is feasible we deliberately do NOT return early: we fall
+ // through and record the constraint on the *original* symbol. That is not a
+ // no-op -- it is how the symbol-simplification fixpoint migrates a
+ // constraint onto a just-simplified symbol. See an example in
+ // symbol-simplification-fixpoint-two-iterations.cpp.
+ } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
+ Sym = SimplifiedSym;
+ }
// Handle SymbolData.
if (isa<SymbolData>(Sym))
@@ -102,7 +121,20 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, bool InRange) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ if (const auto *CI = SimplifiedVal.getAsInteger()) {
+ // The symbol folds to a concrete integer. Prune the path only when the
+ // concrete value proves it infeasible (mirroring
+ // SimpleConstraintManager::assumeInclusiveRangeInternal). If it is
+ // consistent, fall through so the existing machinery still runs it might
+ // trigger further simplification even if this assumption is trivial.
+ bool IsInRange = llvm::APSInt::compareValues(*CI, From) >= 0 &&
+ llvm::APSInt::compareValues(*CI, To) <= 0;
+ if (IsInRange != InRange)
+ return nullptr;
+ } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
+ Sym = SimplifiedSym;
+ }
// Get the type used for calculating wraparound.
BasicValueFactory &BVF = getBasicVals();
@@ -132,7 +164,17 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ if (const auto *CI = SimplifiedVal.getAsInteger()) {
+ // Prune only when the concrete fold contradicts the assumption. When it is
+ // consistent we fall through and record the constraint on the original
+ // symbol (assumeSymNE/EQ below) rather than returning early to continue
+ // constraint simplification.
+ if (isConcreteInfeasible(*CI, Assumption))
+ return nullptr;
+ } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
+ Sym = SimplifiedSym;
+ }
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
@@ -237,12 +279,5 @@ SVal simplifyToSVal(ProgramStateRef State, SymbolRef 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;
-}
-
} // end of namespace ento
} // end of namespace clang
diff --git a/clang/test/Analysis/pthreadlock.c b/clang/test/Analysis/pthreadlock.c
index e931569c45ab8..e235628799a5e 100644
--- a/clang/test/Analysis/pthreadlock.c
+++ b/clang/test/Analysis/pthreadlock.c
@@ -1,8 +1,8 @@
// RUN: %clang_analyze_cc1 \
-// RUN: -analyzer-checker=alpha.unix.PthreadLock \
+// RUN: -analyzer-checker=alpha.unix.PthreadLock,debug.ExprInspection \
// RUN: -verify %s
// RUN: %clang_analyze_cc1 \
-// RUN: -analyzer-checker=alpha.unix.PthreadLock \
+// RUN: -analyzer-checker=alpha.unix.PthreadLock,debug.ExprInspection \
// RUN: -analyzer-config alpha.unix.PthreadLock:WarnOnLockOrderReversal=true \
// RUN: -verify=expected,lor %s
@@ -18,6 +18,29 @@ lck_rw_t rw;
#define NULL 0
+void clang_analyzer_warnIfReached(void);
+long global_var;
+// The self-contradictory constraint below used to reach the lock call with an
+// internally inconsistent state and crash PthreadLockChecker on an assertion.
+// RangedConstraintManager now honors the concrete simplification of
+// `(global_var & 137) & 8` (== 0 when `(global_var & 137) == 2`), so the dead
+// branch is pruned before the lock and neither function warns or crashes.
+void noCrash(void) {
+ if (((global_var & 137) == 2) &&
+ ((global_var & 137) & 8)) {
+ clang_analyzer_warnIfReached(); // no-warning (dead branch, pruned)
+ pthread_mutex_lock(&mtx1); // no-warning
+ }
+}
+
+void noCrashTryLock(void) {
+ if (((global_var & 137) == 2) &&
+ ((global_var & 137) & 8)) {
+ clang_analyzer_warnIfReached(); // no-warning (dead branch, pruned)
+ pthread_mutex_trylock(&mtx1); // no-warning
+ }
+}
+
void
ok1(void)
{
diff --git a/clang/test/Analysis/simplify-drops-concrete.c b/clang/test/Analysis/simplify-drops-concrete.c
new file mode 100644
index 0000000000000..87e95c0fb6ba6
--- /dev/null
+++ b/clang/test/Analysis/simplify-drops-concrete.c
@@ -0,0 +1,88 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+//
+// This test guards a precision fix in RangedConstraintManager. Previously the
+// assume machinery simplified a symbol to an SVal but *discarded* the result
+// unless it was still a SymbolRef. When a symbol simplifies to a concrete
+// integer (e.g. the folded value of `(x & 137) & 8` once `(x & 137)` is pinned
+// to 2), the concrete was thrown away and the coarse, over-approximated range
+// of the original symbol was used instead, which kept a self-contradictory
+// path feasible. The assumeSym* entry points now decide feasibility directly
+// from the concrete simplification (via simplifyToSVal), so the dead paths
+// below are correctly pruned.
+//
+// Three assume entry points consumed the discarded simplification; each is
+// exercised below.
+
+void clang_analyzer_warnIfReached(void);
+void clang_analyzer_eval(int);
+
+long global_var;
+
+// (1) RangedConstraintManager::assumeSymUnsupported.
+//
+// A bare bitwise expression used as a branch condition is not a comparison, so
+// canReasonAbout() returns false and SimpleConstraintManager routes it to
+// assumeSymUnsupported() -> assumeSymNE(sym, 0). The symbol folds to the
+// concrete 0; previously that fold was discarded and assumeSymNE deleted the
+// point 0 from the *coarse* range [0, 2] of `(global_var & 137) & 8`, leaving
+// [1, 2], which looked feasible and (wrongly) entered the dead branch. The
+// concrete fold is now honored: 0 != 0 is false, so the branch is pruned.
+void assumeSymUnsupported_bitwise(void) {
+ if ((global_var & 137) == 2)
+ if ((global_var & 137) & 8)
+ clang_analyzer_warnIfReached(); // no-warning (dead: (2 & 8) == 0)
+}
+
+// (2) RangedConstraintManager::assumeSymInclusiveRange.
+//
+// A switch over a bitwise expression with a GNU case-range routes through
+// ExprEngine's assumeInclusiveRange() -> assumeSymInclusiveRange(). Same
+// story: the switch value folds to the concrete 0. 0 is not in [1, 100], so
+// the case is dead; honoring the concrete fold prunes it.
+void assumeSymInclusiveRange_switch(void) {
+ if ((global_var & 137) == 2)
+ switch ((global_var & 137) & 8) {
+ case 1 ... 100:
+ clang_analyzer_warnIfReached(); // no-warning (dead: 0 not in [1,100])
+ break;
+ }
+}
+
+// (3) RangedConstraintManager::assumeSym.
+//
+// assumeSym() is only reached for conditions canReasonAbout() accepts, i.e.
+// comparison (or +/-) symbolic expressions. Unlike the two cases above, the
+// discarded concrete here was already masked: an explicit comparison is folded
+// by simplifySVal() inside evalBinOp() at evaluation time (or collapses the
+// operand to a single concrete value, which triggers the assignSymExprToConst
+// cascade), so the contradiction was detected and the branch pruned regardless.
+// The evals below document that the analyzer knows the value is 0 on this path.
+void assumeSym_comparison(void) {
+ if ((global_var & 137) == 2) {
+ clang_analyzer_eval(((global_var & 137) & 8) == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(((global_var & 137) & 8) != 0); // expected-warning{{FALSE}}
+ // Consequently the comparison branch is correctly pruned (no warning):
+ if (((global_var & 137) & 8) > 0)
+ clang_analyzer_warnIfReached(); // no-warning (correctly unreachable)
+ }
+}
+
+void noCrashOnTypeMismatch(_Bool a) {
+ // Type mismatch (int vs. _Bool).
+ // A switch routes through ExprEngine::processSwitch -> assumeInclusiveRange
+ // -> assumeSymInclusiveRange. Since `a` is _Bool its range is {0,1}: after
+ // `case 1` is split off, the fall-through path pins the value to 0, so the
+ // switch symbol folds to a concrete integer inside assumeSymInclusiveRange.
+ // That concrete keeps the operand's _Bool (1-bit, unsigned) type, while the
+ // `case 0` label is a promoted `int` (32-bit, signed). The naive `V >= From
+ // && V <= To` used APSInt relational operators, which assert on the
+ // signedness/width mismatch; APSInt::compareValues() normalizes both.
+ switch (a) { // expected-warning {{switch condition has boolean value}}
+ case 1:
+ clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+ break;
+ case 0:
+ clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+ break;
+ }
+}
diff --git a/clang/test/Analysis/z3/z3-crosscheck.c b/clang/test/Analysis/z3/z3-crosscheck.c
index 6b467ce6982de..76a241014c645 100644
--- a/clang/test/Analysis/z3/z3-crosscheck.c
+++ b/clang/test/Analysis/z3/z3-crosscheck.c
@@ -4,10 +4,17 @@
void clang_analyzer_dump(float);
-int foo(int x)
+// The built-in range-based constraint manager reasons about each `%` / `/`
+// sub-expression as an independent, coarsely over-approximated symbol and
+// cannot relate two of them, so it wrongly enters these contradictory
+// branches and reports a null dereference. Z3, with exact modular/division
+// semantics, refutes the path -- which is exactly what the cross-check is for.
+
+int rem_parity(int x) // `x` even and `x + 1` even: impossible
{
int *z = 0;
- if ((x & 1) && ((x & 1) ^ 1))
+ if (x % 2 == 0)
+ if ((x + 1) % 2 == 0)
#ifdef NO_CROSSCHECK
return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
#else
@@ -16,16 +23,28 @@ int foo(int x)
return 0;
}
-int unary(int x, long l)
+int mul_parity(int x, int y) // `x == 2 * y` is even, yet assumed odd: impossible
{
int *z = 0;
- int y = l;
- if ((x & 1) && ((x & 1) ^ 1))
- if (-y)
+ if (x == 2 * y)
+ if (x % 2 != 0)
#ifdef NO_CROSSCHECK
- return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+ return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
#else
- return *z; // no-warning
+ return *z; // no-warning
+#endif
+ return 0;
+}
+
+int div_rem_identity(int x) // `(x / 10) * 10 + x % 10 == x` always holds
+{
+ int *z = 0;
+ if (x > 0 && x < 1000)
+ if ((x / 10) * 10 + (x % 10) != x)
+#ifdef NO_CROSSCHECK
+ return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+ return *z; // no-warning
#endif
return 0;
}
More information about the cfe-commits
mailing list