https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/215240
>From d757aeb0be9a88adecb5b689f5fc0dad58f0e818 Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Mon, 10 Aug 2026 09:53:58 +0000 Subject: [PATCH 1/3] [analyzer][z3] Fix SMTConstraintManager.h removeDeadBindings removeDeadBindings did not properly keep track of constraint dependencies, causing still-in-use constraints to be incorrectly removed. This PR treats constraints that are indirectly related to a live symbol as not dead. Assisted-by: Codex --- .../Core/PathSensitive/SMTConstraintManager.h | 39 +++++++++++++++++-- .../test/Analysis/z3/z3-constraint-liveness.c | 13 +++++++ 2 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 clang/test/Analysis/z3/z3-constraint-liveness.c diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 14c8411f24a1b..69fe99eab9641 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -19,6 +19,9 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h" #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +#include "llvm/ADT/BitVector.h" +#include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/DenseSet.h" #include <optional> typedef llvm::ImmutableSet< @@ -30,6 +33,7 @@ namespace clang { namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { + using ConstraintEntry = std::pair<SymbolRef, const llvm::SMTExpr *>; mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); public: @@ -224,10 +228,39 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SymbolReaper &SymReaper) override { auto CZ = State->get<ConstraintSMT>(); auto &CZFactory = State->get_context<ConstraintSMT>(); + llvm::SmallVector<ConstraintEntry> Constraints(CZ.begin(), CZ.end()); + llvm::DenseMap<SymbolRef, SmallVector<size_t>> ConstraintsBySym; + llvm::DenseSet<SymbolRef> TraversedSymbols; + SmallVector<SymbolRef> WorkList; + llvm::BitVector RelevantConstraints(Constraints.size()); + + for (size_t Idx = 0; Idx < Constraints.size(); ++Idx) { + for (auto Symbol : Constraints[Idx].first->symbols()) { + if (SymReaper.isLive(Symbol) && TraversedSymbols.insert(Symbol).second) + WorkList.push_back(Symbol); + ConstraintsBySym[Symbol].push_back(Idx); + } + } + + while (WorkList.size()) { + SymbolRef Item = WorkList.pop_back_val(); + auto &SymConstraints = ConstraintsBySym[Item]; + for (auto Idx : SymConstraints) { + if (RelevantConstraints.test(Idx)) + continue; + + RelevantConstraints.set(Idx); + + for (auto Symbol : Constraints[Idx].first->symbols()) { + if (TraversedSymbols.insert(Symbol).second) + WorkList.push_back(Symbol); + } + } + } - for (const auto &Entry : CZ) { - if (SymReaper.isDead(Entry.first)) - CZ = CZFactory.remove(CZ, Entry); + for (size_t Idx = 0; Idx < Constraints.size(); ++Idx) { + if (!RelevantConstraints.test(Idx)) + CZ = CZFactory.remove(CZ, Constraints[Idx]); } return State->set<ConstraintSMT>(CZ); diff --git a/clang/test/Analysis/z3/z3-constraint-liveness.c b/clang/test/Analysis/z3/z3-constraint-liveness.c new file mode 100644 index 0000000000000..d6302013dc8c4 --- /dev/null +++ b/clang/test/Analysis/z3/z3-constraint-liveness.c @@ -0,0 +1,13 @@ +// RUN: %clang_analyze_cc1 \ +// RUN: -analyzer-checker=core,debug.ExprInspection \ +// RUN: -analyzer-constraints=unsupported-z3 -verify %s +// REQUIRES: z3 + +void clang_analyzer_eval(int); + +void transitive_constraints(int a, int b, int c) { + if (a != b && b == c && c == 42) { + clang_analyzer_eval(b == 42); // expected-warning{{TRUE}} + clang_analyzer_eval(a != 42); // expected-warning{{TRUE}} + } +} >From 151e920a53fa9ef8ffd289e923e65a4b57de2f0d Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Mon, 10 Aug 2026 12:31:40 +0000 Subject: [PATCH 2/3] add llvm:: for llvm::SmallVector --- .../StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 69fe99eab9641..c476ed84f65f7 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -231,7 +231,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { llvm::SmallVector<ConstraintEntry> Constraints(CZ.begin(), CZ.end()); llvm::DenseMap<SymbolRef, SmallVector<size_t>> ConstraintsBySym; llvm::DenseSet<SymbolRef> TraversedSymbols; - SmallVector<SymbolRef> WorkList; + llvm::SmallVector<SymbolRef> WorkList; llvm::BitVector RelevantConstraints(Constraints.size()); for (size_t Idx = 0; Idx < Constraints.size(); ++Idx) { >From ee91b9cfb9b13f50b9abd3872deee61c10f9f4fa Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Tue, 11 Aug 2026 11:52:09 +0000 Subject: [PATCH 3/3] rename RelevantConstraints to RetainedConstraints --- .../Core/PathSensitive/SMTConstraintManager.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index c476ed84f65f7..4725beb9f5ef0 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -232,7 +232,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { llvm::DenseMap<SymbolRef, SmallVector<size_t>> ConstraintsBySym; llvm::DenseSet<SymbolRef> TraversedSymbols; llvm::SmallVector<SymbolRef> WorkList; - llvm::BitVector RelevantConstraints(Constraints.size()); + llvm::BitVector RetainedConstraints(Constraints.size()); for (size_t Idx = 0; Idx < Constraints.size(); ++Idx) { for (auto Symbol : Constraints[Idx].first->symbols()) { @@ -246,10 +246,10 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SymbolRef Item = WorkList.pop_back_val(); auto &SymConstraints = ConstraintsBySym[Item]; for (auto Idx : SymConstraints) { - if (RelevantConstraints.test(Idx)) + if (RetainedConstraints.test(Idx)) continue; - RelevantConstraints.set(Idx); + RetainedConstraints.set(Idx); for (auto Symbol : Constraints[Idx].first->symbols()) { if (TraversedSymbols.insert(Symbol).second) @@ -259,7 +259,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { } for (size_t Idx = 0; Idx < Constraints.size(); ++Idx) { - if (!RelevantConstraints.test(Idx)) + if (!RetainedConstraints.test(Idx)) CZ = CZFactory.remove(CZ, Constraints[Idx]); } _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
