diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -281,6 +281,11 @@ /// where N = size(this) bool contains(llvm::APSInt Point) const { return containsImpl(Point); } + bool containsZero() const { + APSIntType T{getMinValue()}; + return contains(T.getZeroValue()); + } + void dump(raw_ostream &OS) const; bool operator==(const RangeSet &Other) const { return *Impl == *Other.Impl; } diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1468,121 +1468,6 @@ #undef ASSIGN }; -/// A little component aggregating all of the reasoning we have about -/// assigning new constraints to symbols. -/// -/// The main purpose of this class is to associate constraints to symbols, -/// and impose additional constraints on other symbols, when we can imply -/// them. -/// -/// It has a nice symmetry with SymbolicRangeInferrer. When the latter -/// can provide more precise ranges by looking into the operands of the -/// expression in question, ConstraintAssignor looks into the operands -/// to see if we can imply more from the new constraint. -class ConstraintAssignor : public ConstraintAssignorBase { -public: - template - LLVM_NODISCARD static ProgramStateRef - assign(ProgramStateRef State, SValBuilder &Builder, RangeSet::Factory &F, - ClassOrSymbol CoS, RangeSet NewConstraint) { - if (!State || NewConstraint.isEmpty()) - return nullptr; - - ConstraintAssignor Assignor{State, Builder, F}; - return Assignor.assign(CoS, NewConstraint); - } - - inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint); - inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym, - RangeSet Constraint); - -private: - ConstraintAssignor(ProgramStateRef State, SValBuilder &Builder, - RangeSet::Factory &F) - : State(State), Builder(Builder), RangeFactory(F) {} - using Base = ConstraintAssignorBase; - - /// Base method for handling new constraints for symbols. - LLVM_NODISCARD ProgramStateRef assign(SymbolRef Sym, RangeSet NewConstraint) { - // All constraints are actually associated with equivalence classes, and - // that's what we are going to do first. - State = assign(EquivalenceClass::find(State, Sym), NewConstraint); - if (!State) - return nullptr; - - // And after that we can check what other things we can get from this - // constraint. - Base::assign(Sym, NewConstraint); - return State; - } - - /// Base method for handling new constraints for classes. - LLVM_NODISCARD ProgramStateRef assign(EquivalenceClass Class, - RangeSet NewConstraint) { - // 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 = NewConstraint.getConcreteValue()) { - - ConstraintRangeTy Constraints = State->get(); - ConstraintRangeTy::Factory &CF = State->get_context(); - - // Add new constraint. - Constraints = CF.add(Constraints, Class, NewConstraint); - - for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) { - RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange( - RangeFactory, State, DisequalClass); - - UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point); - - // If we end up with at least one of the disequal classes to be - // constrained with an empty range-set, the state is infeasible. - if (UpdatedConstraint.isEmpty()) - return nullptr; - - Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint); - } - assert(areFeasible(Constraints) && "Constraint manager shouldn't produce " - "a state with infeasible constraints"); - - return setConstraints(State, Constraints); - } - - return setConstraint(State, Class, NewConstraint); - } - - ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS, - SymbolRef RHS) { - return EquivalenceClass::markDisequal(RangeFactory, State, LHS, RHS); - } - - ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS, - SymbolRef RHS) { - return EquivalenceClass::merge(RangeFactory, State, LHS, RHS); - } - - LLVM_NODISCARD Optional interpreteAsBool(RangeSet Constraint) { - assert(!Constraint.isEmpty() && "Empty ranges shouldn't get here"); - - if (Constraint.getConcreteValue()) - return !Constraint.getConcreteValue()->isNullValue(); - - APSIntType T{Constraint.getMinValue()}; - Const Zero = T.getZeroValue(); - if (!Constraint.contains(Zero)) - return true; - - return llvm::None; - } - - ProgramStateRef State; - SValBuilder &Builder; - RangeSet::Factory &RangeFactory; -}; - //===----------------------------------------------------------------------===// // Constraint manager implementation details //===----------------------------------------------------------------------===// @@ -1690,6 +1575,141 @@ const llvm::APSInt &Adjustment); }; +/// A little component aggregating all of the reasoning we have about +/// assigning new constraints to symbols. +/// +/// The main purpose of this class is to associate constraints to symbols, +/// and impose additional constraints on other symbols, when we can imply +/// them. +/// +/// It has a nice symmetry with SymbolicRangeInferrer. When the latter +/// can provide more precise ranges by looking into the operands of the +/// expression in question, ConstraintAssignor looks into the operands +/// to see if we can imply more from the new constraint. +class ConstraintAssignor : public ConstraintAssignorBase { +public: + template + LLVM_NODISCARD static ProgramStateRef + assign(ProgramStateRef State, RangeConstraintManager *RCM, + SValBuilder &Builder, RangeSet::Factory &F, ClassOrSymbol CoS, + RangeSet NewConstraint) { + if (!State || NewConstraint.isEmpty()) + return nullptr; + + ConstraintAssignor Assignor{State, RCM, Builder, F}; + return Assignor.assign(CoS, NewConstraint); + } + + template + bool handleRem(const SymT *Sym, RangeSet Constraint) { + // a % b != 0 implies that a != 0. + if (Sym->getOpcode() != BO_Rem) + return true; + if (!Constraint.containsZero()) { + const SymExpr *LHS = Sym->getLHS(); + const llvm::APSInt &Zero = + Builder.getBasicValueFactory().getValue(0, LHS->getType()); + State = RCM->assumeSymNE(State, LHS, Zero, Zero); + if (!State) + return false; + } + return true; + } + + inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint); + inline bool assignSymIntExprToRangeSet(const SymIntExpr *Sym, + RangeSet Constraint) { + return handleRem(Sym, Constraint); + } + inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym, + RangeSet Constraint); + +private: + ConstraintAssignor(ProgramStateRef State, RangeConstraintManager *RCM, + SValBuilder &Builder, RangeSet::Factory &F) + : State(State), RCM(RCM), Builder(Builder), RangeFactory(F) {} + using Base = ConstraintAssignorBase; + + /// Base method for handling new constraints for symbols. + LLVM_NODISCARD ProgramStateRef assign(SymbolRef Sym, RangeSet NewConstraint) { + // All constraints are actually associated with equivalence classes, and + // that's what we are going to do first. + State = assign(EquivalenceClass::find(State, Sym), NewConstraint); + if (!State) + return nullptr; + + // And after that we can check what other things we can get from this + // constraint. + Base::assign(Sym, NewConstraint); + return State; + } + + /// Base method for handling new constraints for classes. + LLVM_NODISCARD ProgramStateRef assign(EquivalenceClass Class, + RangeSet NewConstraint) { + // 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 = NewConstraint.getConcreteValue()) { + + ConstraintRangeTy Constraints = State->get(); + ConstraintRangeTy::Factory &CF = State->get_context(); + + // Add new constraint. + Constraints = CF.add(Constraints, Class, NewConstraint); + + for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) { + RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange( + RangeFactory, State, DisequalClass); + + UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point); + + // If we end up with at least one of the disequal classes to be + // constrained with an empty range-set, the state is infeasible. + if (UpdatedConstraint.isEmpty()) + return nullptr; + + Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint); + } + assert(areFeasible(Constraints) && "Constraint manager shouldn't produce " + "a state with infeasible constraints"); + + return setConstraints(State, Constraints); + } + + return setConstraint(State, Class, NewConstraint); + } + + ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS, + SymbolRef RHS) { + return EquivalenceClass::markDisequal(RangeFactory, State, LHS, RHS); + } + + ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS, + SymbolRef RHS) { + return EquivalenceClass::merge(RangeFactory, State, LHS, RHS); + } + + LLVM_NODISCARD Optional interpreteAsBool(RangeSet Constraint) { + assert(!Constraint.isEmpty() && "Empty ranges shouldn't get here"); + + if (Constraint.getConcreteValue()) + return !Constraint.getConcreteValue()->isNullValue(); + + if (!Constraint.containsZero()) + return true; + + return llvm::None; + } + + ProgramStateRef State; + RangeConstraintManager *RCM; + SValBuilder &Builder; + RangeSet::Factory &RangeFactory; +}; + bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, const llvm::APSInt &Constraint) { llvm::SmallSet SimplifiedClasses; @@ -1721,8 +1741,10 @@ bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym, RangeSet Constraint) { - Optional ConstraintAsBool = interpreteAsBool(Constraint); + if (!handleRem(Sym, Constraint)) + return false; + Optional ConstraintAsBool = interpreteAsBool(Constraint); if (!ConstraintAsBool) return true; @@ -2396,7 +2418,8 @@ ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State, SymbolRef Sym, RangeSet Range) { - return ConstraintAssignor::assign(State, getSValBuilder(), F, Sym, Range); + return ConstraintAssignor::assign(State, this, getSValBuilder(), F, Sym, + Range); } //===------------------------------------------------------------------------=== diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c new file mode 100644 --- /dev/null +++ b/clang/test/Analysis/constraint-assignor.c @@ -0,0 +1,30 @@ +// RUN: %clang_analyze_cc1 %s \ +// RUN: -analyzer-checker=core \ +// RUN: -analyzer-checker=debug.ExprInspection \ +// RUN: -verify + +// expected-no-diagnostics + +void clang_analyzer_warnIfReached(); + +void rem_constant_rhs(int x, int y) { + if (x % 3 == 0) // x % 3 != 0 -> x != 0 + return; + if (x * y != 0) // x * y == 0 + return; + if (y != 1) // y == 1 -> x == 0 + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} + +void rem_symbolic_rhs(int x, int y, int z) { + if (x % z == 0) // x % 3 != 0 -> x != 0 + return; + if (x * y != 0) // x * y == 0 + return; + if (y != 1) // y == 1 -> x == 0 + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +}