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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
