martong created this revision.
martong added reviewers: NoQ, vsavchenko, steakhal, Szelethus, ASDenysPetrov.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun,
whisperity.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
`a % b != 0` implies that `a != 0` for any `a` and `b`. This patch
extends the ConstraintAssignor to do just that. In fact, we could do
something similar with division and in case of multiplications we could
have some other inferences, but I'd like to keep these for future
patches.
Fixes https://bugs.llvm.org/show_bug.cgi?id=51940
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D110357
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constraint-assignor.c
Index: clang/test/Analysis/constraint-assignor.c
===================================================================
--- /dev/null
+++ 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.
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ 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<ConstraintAssignor> {
-public:
- template <class ClassOrSymbol>
- 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<ConstraintAssignor>;
-
- /// 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<ConstraintRange>();
- ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
-
- // 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<bool> 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<ConstraintAssignor> {
+public:
+ template <class ClassOrSymbol>
+ 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 <typename SymT>
+ 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<ConstraintAssignor>;
+
+ /// 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<ConstraintRange>();
+ ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
+
+ // 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<bool> 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<EquivalenceClass, 4> SimplifiedClasses;
@@ -1721,8 +1741,10 @@
bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
RangeSet Constraint) {
- Optional<bool> ConstraintAsBool = interpreteAsBool(Constraint);
+ if (!handleRem(Sym, Constraint))
+ return false;
+ Optional<bool> 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);
}
//===------------------------------------------------------------------------===
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ 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; }
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
