[clang] 3085bda - [analyzer][solver] Fix infeasible constraints (PR49642)
Valeriy Savchenko via cfe-commits
cfe-commits at lists.llvm.org
Mon Mar 22 01:02:26 PDT 2021
Author: Valeriy Savchenko
Date: 2021-03-22T11:02:02+03:00
New Revision: 3085bda2b348f6a8b4e0bd1d230af4e9c900c9c4
URL: https://github.com/llvm/llvm-project/commit/3085bda2b348f6a8b4e0bd1d230af4e9c900c9c4
DIFF: https://github.com/llvm/llvm-project/commit/3085bda2b348f6a8b4e0bd1d230af4e9c900c9c4.diff
LOG: [analyzer][solver] Fix infeasible constraints (PR49642)
Additionally, this patch puts an assertion checking for feasible
constraints in every place where constraints are assigned to states.
Differential Revision: https://reviews.llvm.org/D98948
Added:
clang/test/Analysis/PR49642.c
Modified:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
Removed:
################################################################################
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 95e61f9c8c61..6ae80b3ae773 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -448,12 +448,12 @@ class EquivalenceClass : public llvm::FoldingSetNode {
EquivalenceClass Other);
/// Return a set of class members for the given state.
- LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State);
+ LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State) const;
/// Return true if the current class is trivial in the given state.
- LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State);
+ LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State) const;
/// Return true if the current class is trivial and its only member is dead.
LLVM_NODISCARD inline bool isTriviallyDead(ProgramStateRef State,
- SymbolReaper &Reaper);
+ SymbolReaper &Reaper) const;
LLVM_NODISCARD static inline ProgramStateRef
markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
@@ -521,7 +521,7 @@ class EquivalenceClass : public llvm::FoldingSetNode {
ProgramStateRef State, SymbolSet Members,
EquivalenceClass Other,
SymbolSet OtherMembers);
- static inline void
+ static inline bool
addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
BasicValueFactory &BV, RangeSet::Factory &F,
ProgramStateRef State, EquivalenceClass First,
@@ -535,6 +535,15 @@ class EquivalenceClass : public llvm::FoldingSetNode {
// Constraint functions
//===----------------------------------------------------------------------===//
+LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED bool
+areFeasible(ConstraintRangeTy Constraints) {
+ return llvm::none_of(
+ Constraints,
+ [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
+ return ClassConstraint.second.isEmpty();
+ });
+}
+
LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
EquivalenceClass Class) {
return State->get<ConstraintRange>(Class);
@@ -1397,15 +1406,6 @@ class RangeConstraintManager : public RangedConstraintManager {
return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
}
- LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
- areFeasible(ConstraintRangeTy Constraints) {
- return llvm::none_of(
- Constraints,
- [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
- return ClassConstraint.second.isEmpty();
- });
- }
-
LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
EquivalenceClass Class,
RangeSet Constraint) {
@@ -1428,7 +1428,7 @@ class RangeConstraintManager : public RangedConstraintManager {
getRange(State, DisequalClass).Delete(getBasicVals(), F, *Point);
// If we end up with at least one of the disequal classes to be
- // constrainted with an empty range-set, the state is infeasible.
+ // constrained with an empty range-set, the state is infeasible.
if (UpdatedConstraint.isEmpty())
return nullptr;
@@ -1574,6 +1574,9 @@ EquivalenceClass::mergeImpl(BasicValueFactory &ValueFactory,
// Assign new constraints for this class.
Constraints = CRF.add(Constraints, *this, *NewClassConstraint);
+ assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+ "a state with infeasible constraints");
+
State = State->set<ConstraintRange>(Constraints);
}
@@ -1644,7 +1647,7 @@ EquivalenceClass::getMembersFactory(ProgramStateRef State) {
return State->get_context<SymbolSet>();
}
-SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) {
+SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) const {
if (const SymbolSet *Members = State->get<ClassMembers>(*this))
return *Members;
@@ -1654,12 +1657,12 @@ SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) {
return F.add(F.getEmptySet(), getRepresentativeSymbol());
}
-bool EquivalenceClass::isTrivial(ProgramStateRef State) {
+bool EquivalenceClass::isTrivial(ProgramStateRef State) const {
return State->get<ClassMembers>(*this) == nullptr;
}
bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
- SymbolReaper &Reaper) {
+ SymbolReaper &Reaper) const {
return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol());
}
@@ -1694,10 +1697,14 @@ EquivalenceClass::markDisequal(BasicValueFactory &VF, RangeSet::Factory &RF,
// Disequality is a symmetric relation, so if we mark A as disequal to B,
// we should also mark B as disequalt to A.
- addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, *this,
- Other);
- addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, Other,
- *this);
+ if (!addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, *this,
+ Other) ||
+ !addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, Other,
+ *this))
+ return nullptr;
+
+ assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+ "a state with infeasible constraints");
State = State->set<DisequalityMap>(DisequalityInfo);
State = State->set<ConstraintRange>(Constraints);
@@ -1705,7 +1712,7 @@ EquivalenceClass::markDisequal(BasicValueFactory &VF, RangeSet::Factory &RF,
return State;
}
-inline void EquivalenceClass::addToDisequalityInfo(
+inline bool EquivalenceClass::addToDisequalityInfo(
DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
BasicValueFactory &VF, RangeSet::Factory &RF, ProgramStateRef State,
EquivalenceClass First, EquivalenceClass Second) {
@@ -1734,8 +1741,16 @@ inline void EquivalenceClass::addToDisequalityInfo(
VF, RF, State, First.getRepresentativeSymbol());
FirstConstraint = FirstConstraint.Delete(VF, RF, *Point);
+
+ // If the First class is about to be constrained with an empty
+ // range-set, the state is infeasible.
+ if (FirstConstraint.isEmpty())
+ return false;
+
Constraints = CRF.add(Constraints, First, FirstConstraint);
}
+
+ return true;
}
inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
diff --git a/clang/test/Analysis/PR49642.c b/clang/test/Analysis/PR49642.c
new file mode 100644
index 000000000000..af691d6afd6f
--- /dev/null
+++ b/clang/test/Analysis/PR49642.c
@@ -0,0 +1,24 @@
+// RUN: %clang_analyze_cc1 -w -verify %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=apiModeling.StdCLibraryFunctions
+
+// expected-no-diagnostics
+
+typedef ssize_t;
+b;
+
+unsigned c;
+int write(int, const void *, unsigned long);
+
+a() {
+ d();
+ while (c > 0) {
+ b = write(0, d, c);
+ if (b)
+ c -= b;
+ b < 1;
+ }
+ if (c && c) {
+ // ^ no-crash
+ }
+}
More information about the cfe-commits
mailing list