Author: rdevshp Date: 2026-08-20T00:04:49-04:00 New Revision: c4e241160b4a2305da6cf47af2bb22e91cda9785
URL: https://github.com/llvm/llvm-project/commit/c4e241160b4a2305da6cf47af2bb22e91cda9785 DIFF: https://github.com/llvm/llvm-project/commit/c4e241160b4a2305da6cf47af2bb22e91cda9785.diff LOG: [analyzer][z3] Fix SMTConstraintManager.h removeDeadBindings (#215240) removeDeadBindings did not properly keep track of constraint dependencies, causing still-in-use constraints to be incorrectly removed. This PR stops constraints that are indirectly related to a live symbol from being removed by removeDeadBindings. Assisted-by: Codex Added: clang/test/Analysis/z3/z3-constraint-liveness.c Modified: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Removed: ################################################################################ diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 14c8411f24a1b..9ddf982657d9b 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: @@ -222,12 +226,40 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override { - auto CZ = State->get<ConstraintSMT>(); - auto &CZFactory = State->get_context<ConstraintSMT>(); + ConstraintSMTType CZ = State->get<ConstraintSMT>(); + ConstraintSMTType::Factory &CZFactory = State->get_context<ConstraintSMT>(); + llvm::SmallVector<ConstraintEntry> Constraints(CZ.begin(), CZ.end()); + llvm::DenseMap<SymbolRef, SmallVector<size_t>> ConstraintsBySym; + llvm::DenseSet<SymbolRef> TraversedSymbols; + llvm::SmallVector<SymbolRef> WorkList; + llvm::BitVector RetainedConstraints(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(); + for (auto Idx : ConstraintsBySym[Item]) { + if (RetainedConstraints.test(Idx)) + continue; + + RetainedConstraints.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 (!RetainedConstraints.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..79388c3e5ee7f --- /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 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}} + } +} _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
