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