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 @@ -282,6 +282,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; void dump() const; 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 @@ -1610,7 +1610,29 @@ return Assignor.assign(CoS, NewConstraint); } + /// Handle expressions like: a % b == 0. + /// E.g., a % b != 0 implies that a != 0. + template + bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) { + if (Sym->getOpcode() != BO_Rem) + return true; + const SymExpr *LHS = Sym->getLHS(); + const llvm::APSInt &Zero = + Builder.getBasicValueFactory().getValue(0, LHS->getType()); + if (Constraint.containsZero()) + State = RCM.assumeSymEQ(State, LHS, Zero, Zero); + else + 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 handleRemainderOp(Sym, Constraint); + } inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym, RangeSet Constraint); @@ -1688,9 +1710,7 @@ if (Constraint.getConcreteValue()) return !Constraint.getConcreteValue()->isZero(); - APSIntType T{Constraint.getMinValue()}; - Const Zero = T.getZeroValue(); - if (!Constraint.contains(Zero)) + if (!Constraint.containsZero()) return true; return llvm::None; @@ -1734,6 +1754,9 @@ bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym, RangeSet Constraint) { + if (!handleRemainderOp(Sym, Constraint)) + return false; + Optional ConstraintAsBool = interpreteAsBool(Constraint); if (!ConstraintAsBool) 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,57 @@ +// 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_eq_zero(int x, int y) { + if (x % 3 != 0) // x % 3 == 0 -> x == 0 + return; + if (x * y == 0) // x * y != 0 -> contradiction + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} + +void rem_symbolic_rhs_eq_zero(int x, int y, int z) { + if (x % z != 0) // x % z == 0 -> x == 0 + return; + if (x * y == 0) // x * y != 0 -> contradiction + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} + +void rem_constant_rhs_ne_zero(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_ne_zero(int x, int y, int z) { + if (x % z == 0) // x % z != 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_eq_zero_nested(int w, int x, int y, int z) { + if (w % x % z != 0) // w % x % z == 0 -> w % x == 0 + return; + if (w % x * y == 0) // w % x * y != 0 -> contradiction + return; + clang_analyzer_warnIfReached(); // no-warning + (void)(w * x); // keep the constraints alive. +}