[clang] [analyzer][z3] Fix SMTConstraintManager.h removeDeadBindings (PR #215240)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Aug 11 05:38:03 PDT 2026
https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/215240
>From d757aeb0be9a88adecb5b689f5fc0dad58f0e818 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 10 Aug 2026 09:53:58 +0000
Subject: [PATCH 1/4] [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 <rdevshp at gmail.com>
Date: Mon, 10 Aug 2026 12:31:40 +0000
Subject: [PATCH 2/4] 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 <rdevshp at gmail.com>
Date: Tue, 11 Aug 2026 11:52:09 +0000
Subject: [PATCH 3/4] 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]);
}
>From 843e481e80d783c15c196051ea6b3a7e3ce34a29 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Tue, 11 Aug 2026 12:37:00 +0000
Subject: [PATCH 4/4] rename the test function in z3-constraint-liveness.c
---
clang/test/Analysis/z3/z3-constraint-liveness.c | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/clang/test/Analysis/z3/z3-constraint-liveness.c b/clang/test/Analysis/z3/z3-constraint-liveness.c
index d6302013dc8c4..79388c3e5ee7f 100644
--- a/clang/test/Analysis/z3/z3-constraint-liveness.c
+++ b/clang/test/Analysis/z3/z3-constraint-liveness.c
@@ -5,7 +5,7 @@
void clang_analyzer_eval(int);
-void transitive_constraints(int a, int b, int c) {
+void indirect_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}}
More information about the cfe-commits
mailing list