diff options
Diffstat (limited to 'contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp')
| -rw-r--r-- | contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp | 1114 |
1 files changed, 1023 insertions, 91 deletions
diff --git a/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index cb6f61e86ae3..a481bde1651b 100644 --- a/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -89,7 +89,7 @@ public: } TriStateKind getCmpOpState(BinaryOperatorKind CurrentOP, - BinaryOperatorKind QueriedOP) const { + BinaryOperatorKind QueriedOP) const { return CmpOpTable[getIndexFromOp(CurrentOP)][getIndexFromOp(QueriedOP)]; } @@ -364,6 +364,18 @@ RangeSet RangeSet::Negate(BasicValueFactory &BV, Factory &F) const { return newRanges; } +RangeSet RangeSet::Delete(BasicValueFactory &BV, Factory &F, + const llvm::APSInt &Point) const { + llvm::APSInt Upper = Point; + llvm::APSInt Lower = Point; + + ++Upper; + --Lower; + + // Notice that the lower bound is greater than the upper bound. + return Intersect(BV, F, Upper, Lower); +} + void RangeSet::print(raw_ostream &os) const { bool isFirst = true; os << "{ "; @@ -379,7 +391,315 @@ void RangeSet::print(raw_ostream &os) const { os << " }"; } +REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(SymbolSet, SymbolRef) + namespace { +class EquivalenceClass; +} // end anonymous namespace + +REGISTER_MAP_WITH_PROGRAMSTATE(ClassMap, SymbolRef, EquivalenceClass) +REGISTER_MAP_WITH_PROGRAMSTATE(ClassMembers, EquivalenceClass, SymbolSet) +REGISTER_MAP_WITH_PROGRAMSTATE(ConstraintRange, EquivalenceClass, RangeSet) + +REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(ClassSet, EquivalenceClass) +REGISTER_MAP_WITH_PROGRAMSTATE(DisequalityMap, EquivalenceClass, ClassSet) + +namespace { +/// This class encapsulates a set of symbols equal to each other. +/// +/// The main idea of the approach requiring such classes is in narrowing +/// and sharing constraints between symbols within the class. Also we can +/// conclude that there is no practical need in storing constraints for +/// every member of the class separately. +/// +/// Main terminology: +/// +/// * "Equivalence class" is an object of this class, which can be efficiently +/// compared to other classes. It represents the whole class without +/// storing the actual in it. The members of the class however can be +/// retrieved from the state. +/// +/// * "Class members" are the symbols corresponding to the class. This means +/// that A == B for every member symbols A and B from the class. Members of +/// each class are stored in the state. +/// +/// * "Trivial class" is a class that has and ever had only one same symbol. +/// +/// * "Merge operation" merges two classes into one. It is the main operation +/// to produce non-trivial classes. +/// If, at some point, we can assume that two symbols from two distinct +/// classes are equal, we can merge these classes. +class EquivalenceClass : public llvm::FoldingSetNode { +public: + /// Find equivalence class for the given symbol in the given state. + LLVM_NODISCARD static inline EquivalenceClass find(ProgramStateRef State, + SymbolRef Sym); + + /// Merge classes for the given symbols and return a new state. + LLVM_NODISCARD static inline ProgramStateRef + merge(BasicValueFactory &BV, RangeSet::Factory &F, ProgramStateRef State, + SymbolRef First, SymbolRef Second); + // Merge this class with the given class and return a new state. + LLVM_NODISCARD inline ProgramStateRef merge(BasicValueFactory &BV, + RangeSet::Factory &F, + ProgramStateRef State, + EquivalenceClass Other); + + /// Return a set of class members for the given state. + LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State); + /// Return true if the current class is trivial in the given state. + LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State); + /// Return true if the current class is trivial and its only member is dead. + LLVM_NODISCARD inline bool isTriviallyDead(ProgramStateRef State, + SymbolReaper &Reaper); + + LLVM_NODISCARD static inline ProgramStateRef + markDisequal(BasicValueFactory &BV, RangeSet::Factory &F, + ProgramStateRef State, SymbolRef First, SymbolRef Second); + LLVM_NODISCARD static inline ProgramStateRef + markDisequal(BasicValueFactory &BV, RangeSet::Factory &F, + ProgramStateRef State, EquivalenceClass First, + EquivalenceClass Second); + LLVM_NODISCARD inline ProgramStateRef + markDisequal(BasicValueFactory &BV, RangeSet::Factory &F, + ProgramStateRef State, EquivalenceClass Other) const; + LLVM_NODISCARD static inline ClassSet + getDisequalClasses(ProgramStateRef State, SymbolRef Sym); + LLVM_NODISCARD inline ClassSet + getDisequalClasses(ProgramStateRef State) const; + LLVM_NODISCARD inline ClassSet + getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const; + + LLVM_NODISCARD static inline Optional<bool> + areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second); + + /// Check equivalence data for consistency. + LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool + isClassDataConsistent(ProgramStateRef State); + + LLVM_NODISCARD QualType getType() const { + return getRepresentativeSymbol()->getType(); + } + + EquivalenceClass() = delete; + EquivalenceClass(const EquivalenceClass &) = default; + EquivalenceClass &operator=(const EquivalenceClass &) = delete; + EquivalenceClass(EquivalenceClass &&) = default; + EquivalenceClass &operator=(EquivalenceClass &&) = delete; + + bool operator==(const EquivalenceClass &Other) const { + return ID == Other.ID; + } + bool operator<(const EquivalenceClass &Other) const { return ID < Other.ID; } + bool operator!=(const EquivalenceClass &Other) const { + return !operator==(Other); + } + + static void Profile(llvm::FoldingSetNodeID &ID, uintptr_t CID) { + ID.AddInteger(CID); + } + + void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, this->ID); } + +private: + /* implicit */ EquivalenceClass(SymbolRef Sym) + : ID(reinterpret_cast<uintptr_t>(Sym)) {} + + /// This function is intended to be used ONLY within the class. + /// The fact that ID is a pointer to a symbol is an implementation detail + /// and should stay that way. + /// In the current implementation, we use it to retrieve the only member + /// of the trivial class. + SymbolRef getRepresentativeSymbol() const { + return reinterpret_cast<SymbolRef>(ID); + } + static inline SymbolSet::Factory &getMembersFactory(ProgramStateRef State); + + inline ProgramStateRef mergeImpl(BasicValueFactory &BV, RangeSet::Factory &F, + ProgramStateRef State, SymbolSet Members, + EquivalenceClass Other, + SymbolSet OtherMembers); + static inline void + addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints, + BasicValueFactory &BV, RangeSet::Factory &F, + ProgramStateRef State, EquivalenceClass First, + EquivalenceClass Second); + + /// This is a unique identifier of the class. + uintptr_t ID; +}; + +//===----------------------------------------------------------------------===// +// Constraint functions +//===----------------------------------------------------------------------===// + +LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State, + EquivalenceClass Class) { + return State->get<ConstraintRange>(Class); +} + +LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State, + SymbolRef Sym) { + return getConstraint(State, EquivalenceClass::find(State, Sym)); +} + +//===----------------------------------------------------------------------===// +// Equality/diseqiality abstraction +//===----------------------------------------------------------------------===// + +/// A small helper structure representing symbolic equality. +/// +/// Equality check can have different forms (like a == b or a - b) and this +/// class encapsulates those away if the only thing the user wants to check - +/// whether it's equality/diseqiality or not and have an easy access to the +/// compared symbols. +struct EqualityInfo { +public: + SymbolRef Left, Right; + // true for equality and false for disequality. + bool IsEquality = true; + + void invert() { IsEquality = !IsEquality; } + /// Extract equality information from the given symbol and the constants. + /// + /// This function assumes the following expression Sym + Adjustment != Int. + /// It is a default because the most widespread case of the equality check + /// is (A == B) + 0 != 0. + static Optional<EqualityInfo> extract(SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + // As of now, the only equality form supported is Sym + 0 != 0. + if (!Int.isNullValue() || !Adjustment.isNullValue()) + return llvm::None; + + return extract(Sym); + } + /// Extract equality information from the given symbol. + static Optional<EqualityInfo> extract(SymbolRef Sym) { + return EqualityExtractor().Visit(Sym); + } + +private: + class EqualityExtractor + : public SymExprVisitor<EqualityExtractor, Optional<EqualityInfo>> { + public: + Optional<EqualityInfo> VisitSymSymExpr(const SymSymExpr *Sym) const { + switch (Sym->getOpcode()) { + case BO_Sub: + // This case is: A - B != 0 -> disequality check. + return EqualityInfo{Sym->getLHS(), Sym->getRHS(), false}; + case BO_EQ: + // This case is: A == B != 0 -> equality check. + return EqualityInfo{Sym->getLHS(), Sym->getRHS(), true}; + case BO_NE: + // This case is: A != B != 0 -> diseqiality check. + return EqualityInfo{Sym->getLHS(), Sym->getRHS(), false}; + default: + return llvm::None; + } + } + }; +}; + +//===----------------------------------------------------------------------===// +// Intersection functions +//===----------------------------------------------------------------------===// + +template <class SecondTy, class... RestTy> +LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV, + RangeSet::Factory &F, RangeSet Head, + SecondTy Second, RestTy... Tail); + +template <class... RangeTy> struct IntersectionTraits; + +template <class... TailTy> struct IntersectionTraits<RangeSet, TailTy...> { + // Found RangeSet, no need to check any further + using Type = RangeSet; +}; + +template <> struct IntersectionTraits<> { + // We ran out of types, and we didn't find any RangeSet, so the result should + // be optional. + using Type = Optional<RangeSet>; +}; + +template <class OptionalOrPointer, class... TailTy> +struct IntersectionTraits<OptionalOrPointer, TailTy...> { + // If current type is Optional or a raw pointer, we should keep looking. + using Type = typename IntersectionTraits<TailTy...>::Type; +}; + +template <class EndTy> +LLVM_NODISCARD inline EndTy intersect(BasicValueFactory &BV, + RangeSet::Factory &F, EndTy End) { + // If the list contains only RangeSet or Optional<RangeSet>, simply return + // that range set. + return End; +} + +LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED inline Optional<RangeSet> +intersect(BasicValueFactory &BV, RangeSet::Factory &F, const RangeSet *End) { + // This is an extraneous conversion from a raw pointer into Optional<RangeSet> + if (End) { + return *End; + } + return llvm::None; +} + +template <class... RestTy> +LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV, + RangeSet::Factory &F, RangeSet Head, + RangeSet Second, RestTy... Tail) { + // Here we call either the <RangeSet,RangeSet,...> or <RangeSet,...> version + // of the function and can be sure that the result is RangeSet. + return intersect(BV, F, Head.Intersect(BV, F, Second), Tail...); +} + +template <class SecondTy, class... RestTy> +LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV, + RangeSet::Factory &F, RangeSet Head, + SecondTy Second, RestTy... Tail) { + if (Second) { + // Here we call the <RangeSet,RangeSet,...> version of the function... + return intersect(BV, F, Head, *Second, Tail...); + } + // ...and here it is either <RangeSet,RangeSet,...> or <RangeSet,...>, which + // means that the result is definitely RangeSet. + return intersect(BV, F, Head, Tail...); +} + +/// Main generic intersect function. +/// It intersects all of the given range sets. If some of the given arguments +/// don't hold a range set (nullptr or llvm::None), the function will skip them. +/// +/// Available representations for the arguments are: +/// * RangeSet +/// * Optional<RangeSet> +/// * RangeSet * +/// Pointer to a RangeSet is automatically assumed to be nullable and will get +/// checked as well as the optional version. If this behaviour is undesired, +/// please dereference the pointer in the call. +/// +/// Return type depends on the arguments' types. If we can be sure in compile +/// time that there will be a range set as a result, the returning type is +/// simply RangeSet, in other cases we have to back off to Optional<RangeSet>. +/// +/// Please, prefer optional range sets to raw pointers. If the last argument is +/// a raw pointer and all previous arguments are None, it will cost one +/// additional check to convert RangeSet * into Optional<RangeSet>. +template <class HeadTy, class SecondTy, class... RestTy> +LLVM_NODISCARD inline + typename IntersectionTraits<HeadTy, SecondTy, RestTy...>::Type + intersect(BasicValueFactory &BV, RangeSet::Factory &F, HeadTy Head, + SecondTy Second, RestTy... Tail) { + if (Head) { + return intersect(BV, F, *Head, Second, Tail...); + } + return intersect(BV, F, Second, Tail...); +} + +//===----------------------------------------------------------------------===// +// Symbolic reasoning logic +//===----------------------------------------------------------------------===// /// A little component aggregating all of the reasoning we have about /// the ranges of symbolic expressions. @@ -389,10 +709,11 @@ namespace { class SymbolicRangeInferrer : public SymExprVisitor<SymbolicRangeInferrer, RangeSet> { public: + template <class SourceType> static RangeSet inferRange(BasicValueFactory &BV, RangeSet::Factory &F, - ProgramStateRef State, SymbolRef Sym) { + ProgramStateRef State, SourceType Origin) { SymbolicRangeInferrer Inferrer(BV, F, State); - return Inferrer.infer(Sym); + return Inferrer.infer(Origin); } RangeSet VisitSymExpr(SymbolRef Sym) { @@ -442,37 +763,35 @@ private: } RangeSet infer(SymbolRef Sym) { - const RangeSet *AssociatedRange = State->get<ConstraintRange>(Sym); - - // If Sym is a difference of symbols A - B, then maybe we have range set - // stored for B - A. - const RangeSet *RangeAssociatedWithNegatedSym = - getRangeForMinusSymbol(State, Sym); - - // If we have range set stored for both A - B and B - A then calculate the - // effective range set by intersecting the range set for A - B and the - // negated range set of B - A. - if (AssociatedRange && RangeAssociatedWithNegatedSym) - return AssociatedRange->Intersect( - ValueFactory, RangeFactory, - RangeAssociatedWithNegatedSym->Negate(ValueFactory, RangeFactory)); - - if (AssociatedRange) - return *AssociatedRange; - - if (RangeAssociatedWithNegatedSym) - return RangeAssociatedWithNegatedSym->Negate(ValueFactory, RangeFactory); + if (Optional<RangeSet> ConstraintBasedRange = intersect( + ValueFactory, RangeFactory, getConstraint(State, Sym), + // If Sym is a difference of symbols A - B, then maybe we have range + // set stored for B - A. + // + // If we have range set stored for both A - B and B - A then + // calculate the effective range set by intersecting the range set + // for A - B and the negated range set of B - A. + getRangeForNegatedSub(Sym), getRangeForEqualities(Sym))) { + return *ConstraintBasedRange; + } // If Sym is a comparison expression (except <=>), // find any other comparisons with the same operands. // See function description. - const RangeSet CmpRangeSet = getRangeForComparisonSymbol(State, Sym); - if (!CmpRangeSet.isEmpty()) - return CmpRangeSet; + if (Optional<RangeSet> CmpRangeSet = getRangeForComparisonSymbol(Sym)) { + return *CmpRangeSet; + } return Visit(Sym); } + RangeSet infer(EquivalenceClass Class) { + if (const RangeSet *AssociatedConstraint = getConstraint(State, Class)) + return *AssociatedConstraint; + + return infer(Class.getType()); + } + /// Infer range information solely from the type. RangeSet infer(QualType T) { // Lazily generate a new RangeSet representing all possible values for the @@ -621,8 +940,7 @@ private: /// Return a range set subtracting zero from \p Domain. RangeSet assumeNonZero(RangeSet Domain, QualType T) { APSIntType IntType = ValueFactory.getAPSIntType(T); - return Domain.Intersect(ValueFactory, RangeFactory, - ++IntType.getZeroValue(), --IntType.getZeroValue()); + return Domain.Delete(ValueFactory, RangeFactory, IntType.getZeroValue()); } // FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to @@ -630,23 +948,26 @@ private: // symbol manually. This will allow us to support finding ranges of not // only negated SymSymExpr-type expressions, but also of other, simpler // expressions which we currently do not know how to negate. - const RangeSet *getRangeForMinusSymbol(ProgramStateRef State, SymbolRef Sym) { + Optional<RangeSet> getRangeForNegatedSub(SymbolRef Sym) { if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) { if (SSE->getOpcode() == BO_Sub) { QualType T = Sym->getType(); + + // Do not negate unsigned ranges + if (!T->isUnsignedIntegerOrEnumerationType() && + !T->isSignedIntegerOrEnumerationType()) + return llvm::None; + SymbolManager &SymMgr = State->getSymbolManager(); - SymbolRef negSym = + SymbolRef NegatedSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), T); - if (const RangeSet *negV = State->get<ConstraintRange>(negSym)) { - // Unsigned range set cannot be negated, unless it is [0, 0]. - if (T->isUnsignedIntegerOrEnumerationType() || - T->isSignedIntegerOrEnumerationType()) - return negV; + if (const RangeSet *NegatedRange = getConstraint(State, NegatedSym)) { + return NegatedRange->Negate(ValueFactory, RangeFactory); } } } - return nullptr; + return llvm::None; } // Returns ranges only for binary comparison operators (except <=>) @@ -659,18 +980,16 @@ private: // It covers all possible combinations (see CmpOpTable description). // Note that `x` and `y` can also stand for subexpressions, // not only for actual symbols. - RangeSet getRangeForComparisonSymbol(ProgramStateRef State, SymbolRef Sym) { - const RangeSet EmptyRangeSet = RangeFactory.getEmptySet(); - - auto SSE = dyn_cast<SymSymExpr>(Sym); + Optional<RangeSet> getRangeForComparisonSymbol(SymbolRef Sym) { + const auto *SSE = dyn_cast<SymSymExpr>(Sym); if (!SSE) - return EmptyRangeSet; + return llvm::None; BinaryOperatorKind CurrentOP = SSE->getOpcode(); // We currently do not support <=> (C++20). if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp)) - return EmptyRangeSet; + return llvm::None; static const OperatorRelationsTable CmpOpTable{}; @@ -679,10 +998,6 @@ private: QualType T = SSE->getType(); SymbolManager &SymMgr = State->getSymbolManager(); - const llvm::APSInt &Zero = ValueFactory.getValue(0, T); - const llvm::APSInt &One = ValueFactory.getValue(1, T); - const RangeSet TrueRangeSet(RangeFactory, One, One); - const RangeSet FalseRangeSet(RangeFactory, Zero, Zero); int UnknownStates = 0; @@ -693,7 +1008,7 @@ private: // Let's find an expression e.g. (x < y). BinaryOperatorKind QueriedOP = OperatorRelationsTable::getOpFromIndex(i); const SymSymExpr *SymSym = SymMgr.getSymSymExpr(LHS, QueriedOP, RHS, T); - const RangeSet *QueriedRangeSet = State->get<ConstraintRange>(SymSym); + const RangeSet *QueriedRangeSet = getConstraint(State, SymSym); // If ranges were not previously found, // try to find a reversed expression (y > x). @@ -701,7 +1016,7 @@ private: const BinaryOperatorKind ROP = BinaryOperator::reverseComparisonOp(QueriedOP); SymSym = SymMgr.getSymSymExpr(RHS, ROP, LHS, T); - QueriedRangeSet = State->get<ConstraintRange>(SymSym); + QueriedRangeSet = getConstraint(State, SymSym); } if (!QueriedRangeSet || QueriedRangeSet->isEmpty()) @@ -732,11 +1047,38 @@ private: continue; } - return (BranchState == OperatorRelationsTable::True) ? TrueRangeSet - : FalseRangeSet; + return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T) + : getFalseRange(T); + } + + return llvm::None; + } + + Optional<RangeSet> getRangeForEqualities(SymbolRef Sym) { + Optional<EqualityInfo> Equality = EqualityInfo::extract(Sym); + + if (!Equality) + return llvm::None; + + if (Optional<bool> AreEqual = EquivalenceClass::areEqual( + State, Equality->Left, Equality->Right)) { + if (*AreEqual == Equality->IsEquality) { + return getTrueRange(Sym->getType()); + } + return getFalseRange(Sym->getType()); } - return EmptyRangeSet; + return llvm::None; + } + + RangeSet getTrueRange(QualType T) { + RangeSet TypeRange = infer(T); + return assumeNonZero(TypeRange, T); + } + + RangeSet getFalseRange(QualType T) { + const llvm::APSInt &Zero = ValueFactory.getValue(0, T); + return RangeSet(RangeFactory, Zero); } BasicValueFactory &ValueFactory; @@ -744,6 +1086,10 @@ private: ProgramStateRef State; }; +//===----------------------------------------------------------------------===// +// Range-based reasoning about symbolic operations +//===----------------------------------------------------------------------===// + template <> RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS, QualType T) { @@ -904,6 +1250,10 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS, return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)}; } +//===----------------------------------------------------------------------===// +// Constraint manager implementation details +//===----------------------------------------------------------------------===// + class RangeConstraintManager : public RangedConstraintManager { public: RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB) @@ -915,7 +1265,11 @@ public: bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const override { - return S1->get<ConstraintRange>() == S2->get<ConstraintRange>(); + // NOTE: ClassMembers are as simple as back pointers for ClassMap, + // so comparing constraint ranges and class maps should be + // sufficient. + return S1->get<ConstraintRange>() == S2->get<ConstraintRange>() && + S1->get<ClassMap>() == S2->get<ClassMap>(); } bool canReasonAbout(SVal X) const override; @@ -971,6 +1325,7 @@ private: RangeSet::Factory F; RangeSet getRange(ProgramStateRef State, SymbolRef Sym); + RangeSet getRange(ProgramStateRef State, EquivalenceClass Class); RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, @@ -987,6 +1342,87 @@ private: RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment); + + //===------------------------------------------------------------------===// + // Equality tracking implementation + //===------------------------------------------------------------------===// + + ProgramStateRef trackEQ(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + return track<true>(NewConstraint, State, Sym, Int, Adjustment); + } + + ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + return track<false>(NewConstraint, State, Sym, Int, Adjustment); + } + + template <bool EQ> + ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + if (NewConstraint.isEmpty()) + // This is an infeasible assumption. + return nullptr; + + ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint); + if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { + // If the original assumption is not Sym + Adjustment !=/</> Int, + // we should invert IsEquality flag. + Equality->IsEquality = Equality->IsEquality != EQ; + return track(NewState, *Equality); + } + + return NewState; + } + + ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) { + if (ToTrack.IsEquality) { + return trackEquality(State, ToTrack.Left, ToTrack.Right); + } + return trackDisequality(State, ToTrack.Left, ToTrack.Right); + } + + ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS, + SymbolRef RHS) { + return EquivalenceClass::markDisequal(getBasicVals(), F, State, LHS, RHS); + } + + ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS, + SymbolRef RHS) { + return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS); + } + + LLVM_NODISCARD inline ProgramStateRef setConstraint(ProgramStateRef State, + EquivalenceClass Class, + RangeSet Constraint) { + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>(); + + // Add new constraint. + Constraints = CF.add(Constraints, Class, Constraint); + + // There is a chance that we might need to update constraints for the + // classes that are known to be disequal to Class. + // + // In order for this to be even possible, the new constraint should + // be simply a constant because we can't reason about range disequalities. + if (const llvm::APSInt *Point = Constraint.getConcreteValue()) + for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) { + RangeSet UpdatedConstraint = + getRange(State, DisequalClass).Delete(getBasicVals(), F, *Point); + Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint); + } + + return State->set<ConstraintRange>(Constraints); + } + + LLVM_NODISCARD inline ProgramStateRef + setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) { + return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint); + } }; } // end anonymous namespace @@ -997,6 +1433,372 @@ ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder()); } +ConstraintMap ento::getConstraintMap(ProgramStateRef State) { + ConstraintMap::Factory &F = State->get_context<ConstraintMap>(); + ConstraintMap Result = F.getEmptyMap(); + + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) { + EquivalenceClass Class = ClassConstraint.first; + SymbolSet ClassMembers = Class.getClassMembers(State); + assert(!ClassMembers.isEmpty() && + "Class must always have at least one member!"); + + SymbolRef Representative = *ClassMembers.begin(); + Result = F.add(Result, Representative, ClassConstraint.second); + } + + return Result; +} + +//===----------------------------------------------------------------------===// +// EqualityClass implementation details +//===----------------------------------------------------------------------===// + +inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State, + SymbolRef Sym) { + // We store far from all Symbol -> Class mappings + if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym)) + return *NontrivialClass; + + // This is a trivial class of Sym. + return Sym; +} + +inline ProgramStateRef EquivalenceClass::merge(BasicValueFactory &BV, + RangeSet::Factory &F, + ProgramStateRef State, + SymbolRef First, + SymbolRef Second) { + EquivalenceClass FirstClass = find(State, First); + EquivalenceClass SecondClass = find(State, Second); + + return FirstClass.merge(BV, F, State, SecondClass); +} + +inline ProgramStateRef EquivalenceClass::merge(BasicValueFactory &BV, + RangeSet::Factory &F, + ProgramStateRef State, + EquivalenceClass Other) { + // It is already the same class. + if (*this == Other) + return State; + + // FIXME: As of now, we support only equivalence classes of the same type. + // This limitation is connected to the lack of explicit casts in + // our symbolic expression model. + // + // That means that for `int x` and `char y` we don't distinguish + // between these two very different cases: + // * `x == y` + // * `(char)x == y` + // + // The moment we introduce symbolic casts, this restriction can be + // lifted. + if (getType() != Other.getType()) + return State; + + SymbolSet Members = getClassMembers(State); + SymbolSet OtherMembers = Other.getClassMembers(State); + + // We estimate the size of the class by the height of tree containing + // its members. Merging is not a trivial operation, so it's easier to + // merge the smaller class into the bigger one. + if (Members.getHeight() >= OtherMembers.getHeight()) { + return mergeImpl(BV, F, State, Members, Other, OtherMembers); + } else { + return Other.mergeImpl(BV, F, State, OtherMembers, *this, Members); + } +} + +inline ProgramStateRef +EquivalenceClass::mergeImpl(BasicValueFactory &ValueFactory, + RangeSet::Factory &RangeFactory, + ProgramStateRef State, SymbolSet MyMembers, + EquivalenceClass Other, SymbolSet OtherMembers) { + // Essentially what we try to recreate here is some kind of union-find + // data structure. It does have certain limitations due to persistence + // and the need to remove elements from classes. + // + // In this setting, EquialityClass object is the representative of the class + // or the parent element. ClassMap is a mapping of class members to their + // parent. Unlike the union-find structure, they all point directly to the + // class representative because we don't have an opportunity to actually do + // path compression when dealing with immutability. This means that we + // compress paths every time we do merges. It also means that we lose + // the main amortized complexity benefit from the original data structure. + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>(); + + // 1. If the merged classes have any constraints associated with them, we + // need to transfer them to the class we have left. + // + // Intersection here makes perfect sense because both of these constraints + // must hold for the whole new class. + if (Optional<RangeSet> NewClassConstraint = + intersect(ValueFactory, RangeFactory, getConstraint(State, *this), + getConstraint(State, Other))) { + // NOTE: Essentially, NewClassConstraint should NEVER be infeasible because + // range inferrer shouldn't generate ranges incompatible with + // equivalence classes. However, at the moment, due to imperfections + // in the solver, it is possible and the merge function can also + // return infeasible states aka null states. + if (NewClassConstraint->isEmpty()) + // Infeasible state + return nullptr; + + // No need in tracking constraints of a now-dissolved class. + Constraints = CRF.remove(Constraints, Other); + // Assign new constraints for this class. + Constraints = CRF.add(Constraints, *this, *NewClassConstraint); + + State = State->set<ConstraintRange>(Constraints); + } + + // 2. Get ALL equivalence-related maps + ClassMapTy Classes = State->get<ClassMap>(); + ClassMapTy::Factory &CMF = State->get_context<ClassMap>(); + + ClassMembersTy Members = State->get<ClassMembers>(); + ClassMembersTy::Factory &MF = State->get_context<ClassMembers>(); + + DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>(); + DisequalityMapTy::Factory &DF = State->get_context<DisequalityMap>(); + + ClassSet::Factory &CF = State->get_context<ClassSet>(); + SymbolSet::Factory &F = getMembersFactory(State); + + // 2. Merge members of the Other class into the current class. + SymbolSet NewClassMembers = MyMembers; + for (SymbolRef Sym : OtherMembers) { + NewClassMembers = F.add(NewClassMembers, Sym); + // *this is now the class for all these new symbols. + Classes = CMF.add(Classes, Sym, *this); + } + + // 3. Adjust member mapping. + // + // No need in tracking members of a now-dissolved class. + Members = MF.remove(Members, Other); + // Now only the current class is mapped to all the symbols. + Members = MF.add(Members, *this, NewClassMembers); + + // 4. Update disequality relations + ClassSet DisequalToOther = Other.getDisequalClasses(DisequalityInfo, CF); + if (!DisequalToOther.isEmpty()) { + ClassSet DisequalToThis = getDisequalClasses(DisequalityInfo, CF); + DisequalityInfo = DF.remove(DisequalityInfo, Other); + + for (EquivalenceClass DisequalClass : DisequalToOther) { + DisequalToThis = CF.add(DisequalToThis, DisequalClass); + + // Disequality is a symmetric relation meaning that if + // DisequalToOther not null then the set for DisequalClass is not + // empty and has at least Other. + ClassSet OriginalSetLinkedToOther = + *DisequalityInfo.lookup(DisequalClass); + + // Other will be eliminated and we should replace it with the bigger + // united class. + ClassSet NewSet = CF.remove(OriginalSetLinkedToOther, Other); + NewSet = CF.add(NewSet, *this); + + DisequalityInfo = DF.add(DisequalityInfo, DisequalClass, NewSet); + } + + DisequalityInfo = DF.add(DisequalityInfo, *this, DisequalToThis); + State = State->set<DisequalityMap>(DisequalityInfo); + } + + // 5. Update the state + State = State->set<ClassMap>(Classes); + State = State->set<ClassMembers>(Members); + + return State; +} + +inline SymbolSet::Factory & +EquivalenceClass::getMembersFactory(ProgramStateRef State) { + return State->get_context<SymbolSet>(); +} + +SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) { + if (const SymbolSet *Members = State->get<ClassMembers>(*this)) + return *Members; + + // This class is trivial, so we need to construct a set + // with just that one symbol from the class. + SymbolSet::Factory &F = getMembersFactory(State); + return F.add(F.getEmptySet(), getRepresentativeSymbol()); +} + +bool EquivalenceClass::isTrivial(ProgramStateRef State) { + return State->get<ClassMembers>(*this) == nullptr; +} + +bool EquivalenceClass::isTriviallyDead(ProgramStateRef State, + SymbolReaper &Reaper) { + return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol()); +} + +inline ProgramStateRef EquivalenceClass::markDisequal(BasicValueFactory &VF, + RangeSet::Factory &RF, + ProgramStateRef State, + SymbolRef First, + SymbolRef Second) { + return markDisequal(VF, RF, State, find(State, First), find(State, Second)); +} + +inline ProgramStateRef EquivalenceClass::markDisequal(BasicValueFactory &VF, + RangeSet::Factory &RF, + ProgramStateRef State, + EquivalenceClass First, + EquivalenceClass Second) { + return First.markDisequal(VF, RF, State, Second); +} + +inline ProgramStateRef +EquivalenceClass::markDisequal(BasicValueFactory &VF, RangeSet::Factory &RF, + ProgramStateRef State, + EquivalenceClass Other) const { + // If we know that two classes are equal, we can only produce an infeasible + // state. + if (*this == Other) { + return nullptr; + } + + DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>(); + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + + // 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); + + State = State->set<DisequalityMap>(DisequalityInfo); + State = State->set<ConstraintRange>(Constraints); + + return State; +} + +inline void EquivalenceClass::addToDisequalityInfo( + DisequalityMapTy &Info, ConstraintRangeTy &Constraints, + BasicValueFactory &VF, RangeSet::Factory &RF, ProgramStateRef State, + EquivalenceClass First, EquivalenceClass Second) { + + // 1. Get all of the required factories. + DisequalityMapTy::Factory &F = State->get_context<DisequalityMap>(); + ClassSet::Factory &CF = State->get_context<ClassSet>(); + ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>(); + + // 2. Add Second to the set of classes disequal to First. + const ClassSet *CurrentSet = Info.lookup(First); + ClassSet NewSet = CurrentSet ? *CurrentSet : CF.getEmptySet(); + NewSet = CF.add(NewSet, Second); + + Info = F.add(Info, First, NewSet); + + // 3. If Second is known to be a constant, we can delete this point + // from the constraint asociated with First. + // + // So, if Second == 10, it means that First != 10. + // At the same time, the same logic does not apply to ranges. + if (const RangeSet *SecondConstraint = Constraints.lookup(Second)) + if (const llvm::APSInt *Point = SecondConstraint->getConcreteValue()) { + + RangeSet FirstConstraint = SymbolicRangeInferrer::inferRange( + VF, RF, State, First.getRepresentativeSymbol()); + + FirstConstraint = FirstConstraint.Delete(VF, RF, *Point); + Constraints = CRF.add(Constraints, First, FirstConstraint); + } +} + +inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State, + SymbolRef FirstSym, + SymbolRef SecondSym) { + EquivalenceClass First = find(State, FirstSym); + EquivalenceClass Second = find(State, SecondSym); + + // The same equivalence class => symbols are equal. + if (First == Second) + return true; + + // Let's check if we know anything about these two classes being not equal to + // each other. + ClassSet DisequalToFirst = First.getDisequalClasses(State); + if (DisequalToFirst.contains(Second)) + return false; + + // It is not clear. + return llvm::None; +} + +inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State, + SymbolRef Sym) { + return find(State, Sym).getDisequalClasses(State); +} + +inline ClassSet +EquivalenceClass::getDisequalClasses(ProgramStateRef State) const { + return getDisequalClasses(State->get<DisequalityMap>(), + State->get_context<ClassSet>()); +} + +inline ClassSet +EquivalenceClass::getDisequalClasses(DisequalityMapTy Map, + ClassSet::Factory &Factory) const { + if (const ClassSet *DisequalClasses = Map.lookup(*this)) + return *DisequalClasses; + + return Factory.getEmptySet(); +} + +bool EquivalenceClass::isClassDataConsistent(ProgramStateRef State) { + ClassMembersTy Members = State->get<ClassMembers>(); + + for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair : Members) { + for (SymbolRef Member : ClassMembersPair.second) { + // Every member of the class should have a mapping back to the class. + if (find(State, Member) == ClassMembersPair.first) { + continue; + } + + return false; + } + } + + DisequalityMapTy Disequalities = State->get<DisequalityMap>(); + for (std::pair<EquivalenceClass, ClassSet> DisequalityInfo : Disequalities) { + EquivalenceClass Class = DisequalityInfo.first; + ClassSet DisequalClasses = DisequalityInfo.second; + + // There is no use in keeping empty sets in the map. + if (DisequalClasses.isEmpty()) + return false; + + // Disequality is symmetrical, i.e. for every Class A and B that A != B, + // B != A should also be true. + for (EquivalenceClass DisequalClass : DisequalClasses) { + const ClassSet *DisequalToDisequalClasses = + Disequalities.lookup(DisequalClass); + + // It should be a set of at least one element: Class + if (!DisequalToDisequalClasses || + !DisequalToDisequalClasses->contains(Class)) + return false; + } + } + + return true; +} + +//===----------------------------------------------------------------------===// +// RangeConstraintManager implementation +//===----------------------------------------------------------------------===// + bool RangeConstraintManager::canReasonAbout(SVal X) const { Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>(); if (SymVal && SymVal->isExpression()) { @@ -1045,7 +1847,7 @@ bool RangeConstraintManager::canReasonAbout(SVal X) const { ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, SymbolRef Sym) { - const RangeSet *Ranges = State->get<ConstraintRange>(Sym); + const RangeSet *Ranges = getConstraint(State, Sym); // If we don't have any information about this symbol, it's underconstrained. if (!Ranges) @@ -1069,28 +1871,148 @@ ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St, SymbolRef Sym) const { - const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym); + const RangeSet *T = getConstraint(St, Sym); return T ? T->getConcreteValue() : nullptr; } +//===----------------------------------------------------------------------===// +// Remove dead symbols from existing constraints +//===----------------------------------------------------------------------===// + /// Scan all symbols referenced by the constraints. If the symbol is not alive /// as marked in LSymbols, mark it as dead in DSymbols. ProgramStateRef RangeConstraintManager::removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) { - bool Changed = false; - ConstraintRangeTy CR = State->get<ConstraintRange>(); - ConstraintRangeTy::Factory &CRFactory = State->get_context<ConstraintRange>(); + ClassMembersTy ClassMembersMap = State->get<ClassMembers>(); + ClassMembersTy NewClassMembersMap = ClassMembersMap; + ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>(); + SymbolSet::Factory &SetFactory = State->get_context<SymbolSet>(); + + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + ConstraintRangeTy NewConstraints = Constraints; + ConstraintRangeTy::Factory &ConstraintFactory = + State->get_context<ConstraintRange>(); + + ClassMapTy Map = State->get<ClassMap>(); + ClassMapTy NewMap = Map; + ClassMapTy::Factory &ClassFactory = State->get_context<ClassMap>(); + + DisequalityMapTy Disequalities = State->get<DisequalityMap>(); + DisequalityMapTy::Factory &DisequalityFactory = + State->get_context<DisequalityMap>(); + ClassSet::Factory &ClassSetFactory = State->get_context<ClassSet>(); + + bool ClassMapChanged = false; + bool MembersMapChanged = false; + bool ConstraintMapChanged = false; + bool DisequalitiesChanged = false; + + auto removeDeadClass = [&](EquivalenceClass Class) { + // Remove associated constraint ranges. + Constraints = ConstraintFactory.remove(Constraints, Class); + ConstraintMapChanged = true; + + // Update disequality information to not hold any information on the + // removed class. + ClassSet DisequalClasses = + Class.getDisequalClasses(Disequalities, ClassSetFactory); + if (!DisequalClasses.isEmpty()) { + for (EquivalenceClass DisequalClass : DisequalClasses) { + ClassSet DisequalToDisequalSet = + DisequalClass.getDisequalClasses(Disequalities, ClassSetFactory); + // DisequalToDisequalSet is guaranteed to be non-empty for consistent + // disequality info. + assert(!DisequalToDisequalSet.isEmpty()); + ClassSet NewSet = ClassSetFactory.remove(DisequalToDisequalSet, Class); + + // No need in keeping an empty set. + if (NewSet.isEmpty()) { + Disequalities = + DisequalityFactory.remove(Disequalities, DisequalClass); + } else { + Disequalities = + DisequalityFactory.add(Disequalities, DisequalClass, NewSet); + } + } + // Remove the data for the class + Disequalities = DisequalityFactory.remove(Disequalities, Class); + DisequalitiesChanged = true; + } + }; + + // 1. Let's see if dead symbols are trivial and have associated constraints. + for (std::pair<EquivalenceClass, RangeSet> ClassConstraintPair : + Constraints) { + EquivalenceClass Class = ClassConstraintPair.first; + if (Class.isTriviallyDead(State, SymReaper)) { + // If this class is trivial, we can remove its constraints right away. + removeDeadClass(Class); + } + } + + // 2. We don't need to track classes for dead symbols. + for (std::pair<SymbolRef, EquivalenceClass> SymbolClassPair : Map) { + SymbolRef Sym = SymbolClassPair.first; - for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { - SymbolRef Sym = I.getKey(); if (SymReaper.isDead(Sym)) { - Changed = true; - CR = CRFactory.remove(CR, Sym); + ClassMapChanged = true; + NewMap = ClassFactory.remove(NewMap, Sym); } } - return Changed ? State->set<ConstraintRange>(CR) : State; + // 3. Remove dead members from classes and remove dead non-trivial classes + // and their constraints. + for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair : + ClassMembersMap) { + EquivalenceClass Class = ClassMembersPair.first; + SymbolSet LiveMembers = ClassMembersPair.second; + bool MembersChanged = false; + + for (SymbolRef Member : ClassMembersPair.second) { + if (SymReaper.isDead(Member)) { + MembersChanged = true; + LiveMembers = SetFactory.remove(LiveMembers, Member); + } + } + + // Check if the class changed. + if (!MembersChanged) + continue; + + MembersMapChanged = true; + + if (LiveMembers.isEmpty()) { + // The class is dead now, we need to wipe it out of the members map... + NewClassMembersMap = EMFactory.remove(NewClassMembersMap, Class); + + // ...and remove all of its constraints. + removeDeadClass(Class); + } else { + // We need to change the members associated with the class. + NewClassMembersMap = + EMFactory.add(NewClassMembersMap, Class, LiveMembers); + } + } + + // 4. Update the state with new maps. + // + // Here we try to be humble and update a map only if it really changed. + if (ClassMapChanged) + State = State->set<ClassMap>(NewMap); + + if (MembersMapChanged) + State = State->set<ClassMembers>(NewClassMembersMap); + + if (ConstraintMapChanged) + State = State->set<ConstraintRange>(Constraints); + + if (DisequalitiesChanged) + State = State->set<DisequalityMap>(Disequalities); + + assert(EquivalenceClass::isClassDataConsistent(State)); + + return State; } RangeSet RangeConstraintManager::getRange(ProgramStateRef State, @@ -1098,6 +2020,11 @@ RangeSet RangeConstraintManager::getRange(ProgramStateRef State, return SymbolicRangeInferrer::inferRange(getBasicVals(), F, State, Sym); } +RangeSet RangeConstraintManager::getRange(ProgramStateRef State, + EquivalenceClass Class) { + return SymbolicRangeInferrer::inferRange(getBasicVals(), F, State, Class); +} + //===------------------------------------------------------------------------=== // assumeSymX methods: protected interface for RangeConstraintManager. //===------------------------------------------------------------------------===/ @@ -1119,15 +2046,11 @@ RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) return St; - llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment; - llvm::APSInt Upper = Lower; - --Lower; - ++Upper; + llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment; - // [Int-Adjustment+1, Int-Adjustment-1] - // Notice that the lower bound is greater than the upper bound. - RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point); + + return trackNE(New, St, Sym, Int, Adjustment); } ProgramStateRef @@ -1142,7 +2065,8 @@ RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, // [Int-Adjustment, Int-Adjustment] llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + + return trackEQ(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St, @@ -1178,7 +2102,7 @@ RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymLTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St, @@ -1214,7 +2138,7 @@ RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymGTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St, @@ -1250,13 +2174,13 @@ RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymGERange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); } -RangeSet RangeConstraintManager::getSymLERange( - llvm::function_ref<RangeSet()> RS, - const llvm::APSInt &Int, - const llvm::APSInt &Adjustment) { +RangeSet +RangeConstraintManager::getSymLERange(llvm::function_ref<RangeSet()> RS, + const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); switch (AdjustmentType.testInRange(Int, true)) { @@ -1293,7 +2217,7 @@ RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymLERange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New); + return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); } ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange( @@ -1303,7 +2227,7 @@ ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange( if (New.isEmpty()) return nullptr; RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment); - return Out.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, Out); + return Out.isEmpty() ? nullptr : setConstraint(State, Sym, Out); } ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange( @@ -1312,7 +2236,7 @@ ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange( RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment); RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment); RangeSet New(RangeLT.addRange(F, RangeGT)); - return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New); + return New.isEmpty() ? nullptr : setConstraint(State, Sym, New); } //===----------------------------------------------------------------------===// @@ -1332,17 +2256,25 @@ void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State, ++Space; Out << '[' << NL; - for (ConstraintRangeTy::iterator I = Constraints.begin(); - I != Constraints.end(); ++I) { - Indent(Out, Space, IsDot) - << "{ \"symbol\": \"" << I.getKey() << "\", \"range\": \""; - I.getData().print(Out); - Out << "\" }"; - - if (std::next(I) != Constraints.end()) - Out << ','; - Out << NL; + bool First = true; + for (std::pair<EquivalenceClass, RangeSet> P : Constraints) { + SymbolSet ClassMembers = P.first.getClassMembers(State); + + // We can print the same constraint for every class member. + for (SymbolRef ClassMember : ClassMembers) { + if (First) { + First = false; + } else { + Out << ','; + Out << NL; + } + Indent(Out, Space, IsDot) + << "{ \"symbol\": \"" << ClassMember << "\", \"range\": \""; + P.second.print(Out); + Out << "\" }"; + } } + Out << NL; --Space; Indent(Out, Space, IsDot) << "]," << NL; |