[clang] [analyzer] Fix null-pointer dereference in PthreadLockChecker (PR #210912)
Arseniy Zaostrovnykh via cfe-commits
cfe-commits at lists.llvm.org
Thu Jul 23 07:32:04 PDT 2026
https://github.com/necto updated https://github.com/llvm/llvm-project/pull/210912
>From e9e747a0cad3ff0ca74a2b035fca1eacd492f168 Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Mon, 20 Jul 2026 13:20:00 +0200
Subject: [PATCH 1/7] Crashing test case
---
clang/test/Analysis/pthreadlock.c | 26 ++++++++++++++++++++++++--
1 file changed, 24 insertions(+), 2 deletions(-)
diff --git a/clang/test/Analysis/pthreadlock.c b/clang/test/Analysis/pthreadlock.c
index e931569c45ab8..426070ae3012a 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,28 @@ lck_rw_t rw;
#define NULL 0
+void clang_analyzer_warnIfReached(void);
+long global_var;
+void noCrash(void) {
+ // Produce a complicated self-contradictory constraint
+ if (((global_var & 137) == 2) &&
+ ((global_var & 137) & 8)) {
+ // This branch is actually dead, but the analyzer does not realize that yet.
+ clang_analyzer_warnIfReached();
+ pthread_mutex_lock(&mtx1); // no-warning
+ }
+}
+
+void noCrashTryLock(void) {
+ // Produce a complicated self-contradictory constraint
+ if (((global_var & 137) == 2) &&
+ ((global_var & 137) & 8)) {
+ // This branch is actually dead, but the analyzer does not realize that yet.
+ clang_analyzer_warnIfReached();
+ pthread_mutex_trylock(&mtx1); // no-warning
+ }
+}
+
void
ok1(void)
{
>From 36eca8abce0f944aab2b3cd5b7b40b60764d2eab Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Tue, 21 Jul 2026 10:39:09 +0200
Subject: [PATCH 2/7] Fix PthreadLockChecker
---
.../Checkers/PthreadLockChecker.cpp | 17 ++++++++++++++---
clang/test/Analysis/pthreadlock.c | 4 ++--
2 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
index 6a1c7a93fb773..c3540ddc32e3a 100644
--- a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -493,8 +493,11 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
default:
llvm_unreachable("Unknown tryLock locking semantics");
}
- assert(lockFail && lockSucc);
- C.addTransition(lockFail);
+ // The state where the lock failed can be infeasible if the constraint
+ // solver only now discovers a contradiction in the accumulated
+ // constraints; only take that transition when it is feasible.
+ if (lockFail)
+ C.addTransition(lockFail);
}
// We might want to handle the case when the mutex lock function was inlined
// and returned an Unknown or Undefined value.
@@ -505,7 +508,9 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
// FIXME: If the lock function was inlined and returned true,
// we need to behave sanely - at least generate sink.
lockSucc = state->assume(*DefinedRetVal, false);
- assert(lockSucc);
+ // `lockSucc` can be null here if the constraint solver only now detects
+ // a contradiction in the accumulated constraints; the shared guard below
+ // prunes this infeasible path.
}
// We might want to handle the case when the mutex lock function was inlined
// and returned an Unknown or Undefined value.
@@ -515,6 +520,12 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
lockSucc = state;
}
+ // If the constraint solver determined the lock-acquired path is infeasible
+ // (which can surface here when it only now detects a contradiction in the
+ // accumulated constraints), prune this path.
+ if (!lockSucc)
+ return;
+
// Record that the lock was acquired.
lockSucc = lockSucc->add<LockSet>(lockR);
lockSucc = lockSucc->set<LockMap>(lockR, LockState::getLocked());
diff --git a/clang/test/Analysis/pthreadlock.c b/clang/test/Analysis/pthreadlock.c
index 426070ae3012a..49b83cab031a0 100644
--- a/clang/test/Analysis/pthreadlock.c
+++ b/clang/test/Analysis/pthreadlock.c
@@ -25,7 +25,7 @@ void noCrash(void) {
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
// This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached();
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
pthread_mutex_lock(&mtx1); // no-warning
}
}
@@ -35,7 +35,7 @@ void noCrashTryLock(void) {
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
// This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached();
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
pthread_mutex_trylock(&mtx1); // no-warning
}
}
>From 934cd3ccc7fd2a33bae8c17c9335a92fd634271d Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Wed, 22 Jul 2026 16:05:50 +0200
Subject: [PATCH 3/7] Revert "Fix PthreadLockChecker"
This reverts commit 36eca8abce0f944aab2b3cd5b7b40b60764d2eab.
---
.../Checkers/PthreadLockChecker.cpp | 17 +++--------------
clang/test/Analysis/pthreadlock.c | 4 ++--
2 files changed, 5 insertions(+), 16 deletions(-)
diff --git a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
index c3540ddc32e3a..6a1c7a93fb773 100644
--- a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -493,11 +493,8 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
default:
llvm_unreachable("Unknown tryLock locking semantics");
}
- // The state where the lock failed can be infeasible if the constraint
- // solver only now discovers a contradiction in the accumulated
- // constraints; only take that transition when it is feasible.
- if (lockFail)
- C.addTransition(lockFail);
+ assert(lockFail && lockSucc);
+ C.addTransition(lockFail);
}
// We might want to handle the case when the mutex lock function was inlined
// and returned an Unknown or Undefined value.
@@ -508,9 +505,7 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
// FIXME: If the lock function was inlined and returned true,
// we need to behave sanely - at least generate sink.
lockSucc = state->assume(*DefinedRetVal, false);
- // `lockSucc` can be null here if the constraint solver only now detects
- // a contradiction in the accumulated constraints; the shared guard below
- // prunes this infeasible path.
+ assert(lockSucc);
}
// We might want to handle the case when the mutex lock function was inlined
// and returned an Unknown or Undefined value.
@@ -520,12 +515,6 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
lockSucc = state;
}
- // If the constraint solver determined the lock-acquired path is infeasible
- // (which can surface here when it only now detects a contradiction in the
- // accumulated constraints), prune this path.
- if (!lockSucc)
- return;
-
// Record that the lock was acquired.
lockSucc = lockSucc->add<LockSet>(lockR);
lockSucc = lockSucc->set<LockMap>(lockR, LockState::getLocked());
diff --git a/clang/test/Analysis/pthreadlock.c b/clang/test/Analysis/pthreadlock.c
index 49b83cab031a0..426070ae3012a 100644
--- a/clang/test/Analysis/pthreadlock.c
+++ b/clang/test/Analysis/pthreadlock.c
@@ -25,7 +25,7 @@ void noCrash(void) {
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
// This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ clang_analyzer_warnIfReached();
pthread_mutex_lock(&mtx1); // no-warning
}
}
@@ -35,7 +35,7 @@ void noCrashTryLock(void) {
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
// This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ clang_analyzer_warnIfReached();
pthread_mutex_trylock(&mtx1); // no-warning
}
}
>From 1ae1e1dc5b8de08663883840adfc1d335de4b2b3 Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Wed, 22 Jul 2026 17:25:01 +0200
Subject: [PATCH 4/7] Add a test case demonstrating missed simplification
---
clang/test/Analysis/simplify-drops-concrete.c | 77 +++++++++++++++++++
1 file changed, 77 insertions(+)
create mode 100644 clang/test/Analysis/simplify-drops-concrete.c
diff --git a/clang/test/Analysis/simplify-drops-concrete.c b/clang/test/Analysis/simplify-drops-concrete.c
new file mode 100644
index 0000000000000..7046c9016a25c
--- /dev/null
+++ b/clang/test/Analysis/simplify-drops-concrete.c
@@ -0,0 +1,77 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+//
+// This test documents an imprecision in RangedConstraintManager: the helper
+//
+// SymbolRef simplify(ProgramStateRef, SymbolRef)
+//
+// (clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp) simplifies a
+// symbol to an SVal but then *discards* the result unless it is 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 is
+// thrown away and the coarse, over-approximated range of the original symbol
+// is used instead. That keeps a self-contradictory path feasible.
+//
+// The helper is called from three places; each is exercised below.
+
+void clang_analyzer_warnIfReached(void);
+void clang_analyzer_eval(int);
+
+long global_var;
+
+// (1) simplify() call inside 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). simplify() folds the symbol
+// to the concrete 0 but discards it; assumeSymNE then deletes the point 0 from
+// the *coarse* range [0, 2] of `(global_var & 137) & 8`, leaving [1, 2], which
+// looks feasible. The dead branch is therefore (incorrectly) entered.
+//
+// FIXME: This branch is dead ((2 & 8) == 0), so it should NOT be reachable.
+// The REACHABLE expectation below encodes the current (buggy) behavior and
+// should be removed once simplify() preserves concrete simplifications.
+void assumeSymUnsupported_bitwise(void) {
+ if ((global_var & 137) == 2)
+ if ((global_var & 137) & 8)
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+// (2) simplify() call inside RangedConstraintManager::assumeSymInclusiveRange.
+//
+// A switch over a bitwise expression with a GNU case-range routes through
+// ExprEngine's assumeInclusiveRange() -> assumeSymInclusiveRange(). Same
+// story: simplify() folds the switch value to 0 but discards it, and the
+// coarse range [0, 2] intersected with the case range [1, 100] yields the
+// non-empty [1, 2], so the (dead) case is entered.
+//
+// FIXME: 0 is not in [1, 100], so this case is dead and should be unreachable.
+void assumeSymInclusiveRange_switch(void) {
+ if ((global_var & 137) == 2)
+ switch ((global_var & 137) & 8) {
+ case 1 ... 100:
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ break;
+ }
+}
+
+// (3) simplify() call inside 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 is 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 is detected and the branch is pruned
+// regardless of what simplify() returns. We therefore cannot demonstrate a
+// spurious *reachable* branch through assumeSym; the discard here is only
+// wasted work. The evals below document that the analyzer already 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)
+ }
+}
>From dcb89e17978a56dc04f4ad390f7abc55593cab35 Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Thu, 23 Jul 2026 13:35:32 +0200
Subject: [PATCH 5/7] Fix the simplification blind spot for concrete integers
---
.../PathSensitive/RangedConstraintManager.h | 17 +---
.../Core/RangedConstraintManager.cpp | 85 ++++++++++++++++---
clang/test/Analysis/pthreadlock.c | 13 +--
clang/test/Analysis/simplify-drops-concrete.c | 63 ++++++--------
clang/test/Analysis/z3/z3-crosscheck.c | 17 ++--
5 files changed, 120 insertions(+), 75 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
index 4ed4d3c738444..455668b48eafc 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -478,20 +478,11 @@ 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. This is needed because the Environment bindings are
+/// not getting updated when a new constraint is added to the State. The
+/// simplified SVal might be a single constant (i.e. `ConcreteInt`), which
+/// callers in the assumeSym* family use to decide feasibility directly.
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..8045e107c960a 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -20,10 +20,46 @@ namespace ento {
RangedConstraintManager::~RangedConstraintManager() {}
+// Is `Assumption` (i.e. "the condition is non-zero") consistent with a symbol
+// that simplified to the concrete integer `V`? Mirrors the nonloc::ConcreteInt
+// handling in SimpleConstraintManager::assumeAux.
+static bool isConcreteFeasible(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);
+ // Note: a loc::ConcreteInt is not possible here. This callsite is only ever
+ // reached with non-loc-typed symbols (SimpleConstraintManager::assumeAux's
+ // nonloc::SymbolVal case and assumeSymRel's comparison-to-zero rewrite), and
+ // simplifyToSVal() -> makeSymbolVal() only produces a Loc for pointer-typed
+ // symbols -- so the fold can only ever be a nonloc::ConcreteInt.
+ if (auto CI = SimplifiedVal.getAs<nonloc::ConcreteInt>()) {
+ // The symbol folds to a concrete integer. If the assumption contradicts it
+ // the path is infeasible and must be pruned; otherwise a self-contradictory
+ // state would stay feasible and could crash checkers downstream.
+ if (!isConcreteFeasible(*CI->getValue(), Assumption))
+ return nullptr;
+ // When the fold is consistent 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. Concretely, in
+ // symbol-simplification-fixpoint-two-iterations.cpp, once `b == 0` rewrites
+ // `c + b` (constrained to 0) into the bare symbol `c`, the classes merge and
+ // reAssume() calls assume(c, false); here `c` folds to the concrete 0, and
+ // falling through to assumeSymUnsupported()/assumeSymEQ() records `c == 0`.
+ // That recorded fact is what lets the *next* iteration rewrite `a + c` into
+ // `a`. Returning State here skips the recording and the class stays stuck at
+ // `(a + c) != d`, regressing that test. (EquivalenceClass::simplify ->
+ // reAssume -> State->assume is the loop this participates in.)
+ } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
+ // A symbolic fold replaces the symbol so we reason about the simpler form.
+ // Any other SVal shape (Unknown, ...) keeps the original symbol -- matching
+ // the pre-existing behavior of the old simplify() helper.
+ Sym = SimplifiedSym;
+ }
// Handle SymbolData.
if (isa<SymbolData>(Sym))
@@ -102,7 +138,28 @@ 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);
+ // Note: unlike assumeSym(), this callsite can receive a pointer-typed Sym
+ // (assumeInclusiveRangeInternal's nonloc::LocAsInteger case, e.g. a case-range
+ // switch over `(intptr_t)ptr`), so simplifyToSVal() could in principle yield a
+ // loc::ConcreteInt. In practice it never does: that fold requires the pointer
+ // pinned to a single concrete address, and once it is, `(intptr_t)ptr` folds
+ // eagerly to a nonloc::ConcreteInt and is handled before ever reaching a
+ // symbol here. Hence only the nonloc::ConcreteInt case needs handling.
+ if (auto CI = SimplifiedVal.getAs<nonloc::ConcreteInt>()) {
+ // The symbol folds to a concrete integer. Prune the path only when the
+ // concrete value proves it infeasible (mirroring
+ // SimpleConstraintManager::assumeInclusiveRangeInternal; APSInt comparison
+ // handles differing widths/signedness, so no explicit conversion needed).
+ // If it is consistent, fall through so the existing machinery still runs
+ // (see the note in assumeSym for why the fall-through is load-bearing).
+ const llvm::APSInt &V = *CI->getValue();
+ bool IsInRange = V >= From && V <= To;
+ 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 +189,22 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ // Note: like assumeSym(), this never receives a pointer-typed Sym -- its
+ // callers (assumeSym()'s fall-through and assumeAux()'s !canReasonAbout
+ // branch, where getAsSymbol() yields the integer-typed bitwise/comparison
+ // expression) only pass non-loc symbols -- so the fold is always a
+ // nonloc::ConcreteInt.
+ if (auto CI = SimplifiedVal.getAs<nonloc::ConcreteInt>()) {
+ // 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; see the note
+ // in assumeSym for why the fall-through is load-bearing.
+ if (!isConcreteFeasible(*CI->getValue(), Assumption))
+ return nullptr;
+ } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
+ Sym = SimplifiedSym;
+ }
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
@@ -237,12 +309,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 426070ae3012a..e235628799a5e 100644
--- a/clang/test/Analysis/pthreadlock.c
+++ b/clang/test/Analysis/pthreadlock.c
@@ -20,22 +20,23 @@ lck_rw_t rw;
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) {
- // Produce a complicated self-contradictory constraint
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
- // This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached();
+ clang_analyzer_warnIfReached(); // no-warning (dead branch, pruned)
pthread_mutex_lock(&mtx1); // no-warning
}
}
void noCrashTryLock(void) {
- // Produce a complicated self-contradictory constraint
if (((global_var & 137) == 2) &&
((global_var & 137) & 8)) {
- // This branch is actually dead, but the analyzer does not realize that yet.
- clang_analyzer_warnIfReached();
+ clang_analyzer_warnIfReached(); // no-warning (dead branch, pruned)
pthread_mutex_trylock(&mtx1); // no-warning
}
}
diff --git a/clang/test/Analysis/simplify-drops-concrete.c b/clang/test/Analysis/simplify-drops-concrete.c
index 7046c9016a25c..26322436f5fc9 100644
--- a/clang/test/Analysis/simplify-drops-concrete.c
+++ b/clang/test/Analysis/simplify-drops-concrete.c
@@ -1,71 +1,62 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
//
-// This test documents an imprecision in RangedConstraintManager: the helper
+// 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.
//
-// SymbolRef simplify(ProgramStateRef, SymbolRef)
-//
-// (clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp) simplifies a
-// symbol to an SVal but then *discards* the result unless it is 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 is
-// thrown away and the coarse, over-approximated range of the original symbol
-// is used instead. That keeps a self-contradictory path feasible.
-//
-// The helper is called from three places; each is exercised below.
+// 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) simplify() call inside RangedConstraintManager::assumeSymUnsupported.
+// (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). simplify() folds the symbol
-// to the concrete 0 but discards it; assumeSymNE then deletes the point 0 from
-// the *coarse* range [0, 2] of `(global_var & 137) & 8`, leaving [1, 2], which
-// looks feasible. The dead branch is therefore (incorrectly) entered.
-//
-// FIXME: This branch is dead ((2 & 8) == 0), so it should NOT be reachable.
-// The REACHABLE expectation below encodes the current (buggy) behavior and
-// should be removed once simplify() preserves concrete simplifications.
+// 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(); // expected-warning{{REACHABLE}}
+ clang_analyzer_warnIfReached(); // no-warning (dead: (2 & 8) == 0)
}
-// (2) simplify() call inside RangedConstraintManager::assumeSymInclusiveRange.
+// (2) RangedConstraintManager::assumeSymInclusiveRange.
//
// A switch over a bitwise expression with a GNU case-range routes through
// ExprEngine's assumeInclusiveRange() -> assumeSymInclusiveRange(). Same
-// story: simplify() folds the switch value to 0 but discards it, and the
-// coarse range [0, 2] intersected with the case range [1, 100] yields the
-// non-empty [1, 2], so the (dead) case is entered.
-//
-// FIXME: 0 is not in [1, 100], so this case is dead and should be unreachable.
+// 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(); // expected-warning{{REACHABLE}}
+ clang_analyzer_warnIfReached(); // no-warning (dead: 0 not in [1,100])
break;
}
}
-// (3) simplify() call inside RangedConstraintManager::assumeSym.
+// (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 is masked: an explicit comparison is folded by
-// simplifySVal() inside evalBinOp() at evaluation time (or collapses 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 is detected and the branch is pruned
-// regardless of what simplify() returns. We therefore cannot demonstrate a
-// spurious *reachable* branch through assumeSym; the discard here is only
-// wasted work. The evals below document that the analyzer already knows the
-// value is 0 on this path.
+// 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}}
diff --git a/clang/test/Analysis/z3/z3-crosscheck.c b/clang/test/Analysis/z3/z3-crosscheck.c
index 41ecaee5529e0..f1e7eee67a491 100644
--- a/clang/test/Analysis/z3/z3-crosscheck.c
+++ b/clang/test/Analysis/z3/z3-crosscheck.c
@@ -4,15 +4,16 @@
void clang_analyzer_dump(float);
+// `(x & 1) && ((x & 1) ^ 1)` is self-contradictory: the second conjunct is
+// `1 ^ 1 == 0` whenever the first holds. The range-based constraint manager
+// now folds the concrete simplification of `(x & 1) ^ 1` and prunes the dead
+// branch on its own, so the null dereference is unreachable in *both*
+// configurations -- the Z3 cross-check is no longer needed to refute it.
int foo(int x)
{
int *z = 0;
if ((x & 1) && ((x & 1) ^ 1))
-#ifdef NO_CROSSCHECK
- return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
-#else
- return *z; // no-warning
-#endif
+ return *z; // no-warning (dead branch pruned by the range solver)
return 0;
}
@@ -22,11 +23,7 @@ int unary(int x, long l)
int y = l;
if ((x & 1) && ((x & 1) ^ 1))
if (-y)
-#ifdef NO_CROSSCHECK
- return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
-#else
- return *z; // no-warning
-#endif
+ return *z; // no-warning (dead branch pruned by the range solver)
return 0;
}
>From 96bdb09b678ab77074bd340bd3e079771b118ad1 Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Thu, 23 Jul 2026 13:38:35 +0200
Subject: [PATCH 6/7] Restore meaningful z3-crosscheck.c test
---
clang/test/Analysis/z3/z3-crosscheck.c | 48 +++++++++++++++++++-------
1 file changed, 35 insertions(+), 13 deletions(-)
diff --git a/clang/test/Analysis/z3/z3-crosscheck.c b/clang/test/Analysis/z3/z3-crosscheck.c
index f1e7eee67a491..c5500efa23c33 100644
--- a/clang/test/Analysis/z3/z3-crosscheck.c
+++ b/clang/test/Analysis/z3/z3-crosscheck.c
@@ -4,26 +4,48 @@
void clang_analyzer_dump(float);
-// `(x & 1) && ((x & 1) ^ 1)` is self-contradictory: the second conjunct is
-// `1 ^ 1 == 0` whenever the first holds. The range-based constraint manager
-// now folds the concrete simplification of `(x & 1) ^ 1` and prunes the dead
-// branch on its own, so the null dereference is unreachable in *both*
-// configurations -- the Z3 cross-check is no longer needed to refute it.
-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 % 2 == 0)
+ if ((x + 1) % 2 == 0)
+#ifdef NO_CROSSCHECK
+ return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+ return *z; // no-warning
+#endif
+ return 0;
+}
+
+int mul_parity(int x, int y) // `x == 2 * y` is even, yet assumed odd: impossible
{
int *z = 0;
- if ((x & 1) && ((x & 1) ^ 1))
- return *z; // no-warning (dead branch pruned by the range solver)
+ if (x == 2 * y)
+ if (x % 2 != 0)
+#ifdef NO_CROSSCHECK
+ return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+ return *z; // no-warning
+#endif
return 0;
}
-int unary(int x, long l)
+int div_rem_identity(int x) // `(x / 10) * 10 + x % 10 == x` always holds
{
int *z = 0;
- int y = l;
- if ((x & 1) && ((x & 1) ^ 1))
- if (-y)
- return *z; // no-warning (dead branch pruned by the range solver)
+ 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;
}
>From 055b84f81fc63f6358ffb66a482b47f3f0c0152c Mon Sep 17 00:00:00 2001
From: Arseniy Zaostrovnykh <necto.ne at gmail.com>
Date: Thu, 23 Jul 2026 16:31:31 +0200
Subject: [PATCH 7/7] [NFC] Apply clang format
---
.../Core/RangedConstraintManager.cpp | 24 ++++++++++---------
1 file changed, 13 insertions(+), 11 deletions(-)
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 8045e107c960a..db31b8855b5db 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -47,11 +47,12 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
// no-op -- it is how the symbol-simplification fixpoint migrates a
// constraint onto a just-simplified symbol. Concretely, in
// symbol-simplification-fixpoint-two-iterations.cpp, once `b == 0` rewrites
- // `c + b` (constrained to 0) into the bare symbol `c`, the classes merge and
- // reAssume() calls assume(c, false); here `c` folds to the concrete 0, and
- // falling through to assumeSymUnsupported()/assumeSymEQ() records `c == 0`.
- // That recorded fact is what lets the *next* iteration rewrite `a + c` into
- // `a`. Returning State here skips the recording and the class stays stuck at
+ // `c + b` (constrained to 0) into the bare symbol `c`, the classes merge
+ // and reAssume() calls assume(c, false); here `c` folds to the concrete 0,
+ // and falling through to assumeSymUnsupported()/assumeSymEQ() records `c ==
+ // 0`. That recorded fact is what lets the *next* iteration rewrite `a + c`
+ // into `a`. Returning State here skips the recording and the class stays
+ // stuck at
// `(a + c) != d`, regressing that test. (EquivalenceClass::simplify ->
// reAssume -> State->assume is the loop this participates in.)
} else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
@@ -140,12 +141,13 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
SVal SimplifiedVal = simplifyToSVal(State, Sym);
// Note: unlike assumeSym(), this callsite can receive a pointer-typed Sym
- // (assumeInclusiveRangeInternal's nonloc::LocAsInteger case, e.g. a case-range
- // switch over `(intptr_t)ptr`), so simplifyToSVal() could in principle yield a
- // loc::ConcreteInt. In practice it never does: that fold requires the pointer
- // pinned to a single concrete address, and once it is, `(intptr_t)ptr` folds
- // eagerly to a nonloc::ConcreteInt and is handled before ever reaching a
- // symbol here. Hence only the nonloc::ConcreteInt case needs handling.
+ // (assumeInclusiveRangeInternal's nonloc::LocAsInteger case, e.g. a
+ // case-range switch over `(intptr_t)ptr`), so simplifyToSVal() could in
+ // principle yield a loc::ConcreteInt. In practice it never does: that fold
+ // requires the pointer pinned to a single concrete address, and once it is,
+ // `(intptr_t)ptr` folds eagerly to a nonloc::ConcreteInt and is handled
+ // before ever reaching a symbol here. Hence only the nonloc::ConcreteInt case
+ // needs handling.
if (auto CI = SimplifiedVal.getAs<nonloc::ConcreteInt>()) {
// The symbol folds to a concrete integer. Prune the path only when the
// concrete value proves it infeasible (mirroring
More information about the cfe-commits
mailing list