llvmorg-github-actions[bot] wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang Author: rdevshp (rdevshp) <details> <summary>Changes</summary> 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 --- Full diff: https://github.com/llvm/llvm-project/pull/215240.diff 2 Files Affected: - (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+36-3) - (added) clang/test/Analysis/z3/z3-constraint-liveness.c (+13) ``````````diff 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}} + } +} `````````` </details> https://github.com/llvm/llvm-project/pull/215240 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
