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,
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,
// 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);
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) {
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;
// 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);
}
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;
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());
}
// 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);
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) {
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,