[clang] [analyzer][z3] Fix SMTConstraintManager.h removeDeadBindings (PR #215240)

[via cfe-commits]

https://github.com/rdevshp created https://github.com/llvm/llvm-project/pull/215240

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.

CC: @steakhal

Assisted-by: Codex

>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] [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}}
+  }
+}