Author: Gabor Marton Date: 2021-10-22T10:47:25+02:00 New Revision: 5f8dca023504ed21490a40ddc3a0241029782910
URL: https://github.com/llvm/llvm-project/commit/5f8dca023504ed21490a40ddc3a0241029782910 DIFF: https://github.com/llvm/llvm-project/commit/5f8dca023504ed21490a40ddc3a0241029782910.diff LOG: [Analyzer] Extend ConstraintAssignor to handle remainder op Summary: `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 Reviewers: noq, vsavchenko, steakhal, szelethus, asdenyspetrov Subscribers: Differential Revision: https://reviews.llvm.org/D110357 Added: clang/test/Analysis/constraint-assignor.c Modified: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Removed: ################################################################################ diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h index 599e4ec812a1b..153b8a732166f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -282,6 +282,11 @@ class RangeSet { /// 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 index 7df9027b373d9..e75a207ee86ab 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1610,7 +1610,28 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> { return Assignor.assign(CoS, NewConstraint); } + /// Handle expressions like: a % b != 0. + template <typename SymT> + bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) { + if (Sym->getOpcode() != BO_Rem) + return true; + const SymbolRef LHS = Sym->getLHS(); + const llvm::APSInt &Zero = + Builder.getBasicValueFactory().getValue(0, Sym->getType()); + // a % b != 0 implies that a != 0. + if (!Constraint.containsZero()) { + 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 +1709,7 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> { 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 +1753,9 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym, RangeSet Constraint) { + if (!handleRemainderOp(Sym, Constraint)) + return false; + Optional<bool> 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 index 0000000000000..1c041e3e0ce45 --- /dev/null +++ b/clang/test/Analysis/constraint-assignor.c @@ -0,0 +1,69 @@ +// 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_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_ne_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 + return; + if (y != 1) // y == 1 -> w % x == 0 + return; + clang_analyzer_warnIfReached(); // no-warning + (void)(w * x); // keep the constraints alive. +} + +void rem_constant_rhs_ne_zero_early_contradiction(int x, int y) { + if ((x + y) != 0) // (x + y) == 0 + return; + if ((x + y) % 3 == 0) // (x + y) % 3 != 0 -> (x + y) != 0 -> contradiction + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} + +void rem_symbolic_rhs_ne_zero_early_contradiction(int x, int y, int z) { + if ((x + y) != 0) // (x + y) == 0 + return; + if ((x + y) % z == 0) // (x + y) % z != 0 -> (x + y) != 0 -> contradiction + return; + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} + +void internal_unsigned_signed_mismatch(unsigned a) { + int d = a; + // Implicit casts are not handled, thus the analyzer models `d % 2` as + // `(reg_$0<unsigned int a>) % 2` + // However, this should not result in internal signedness mismatch error when + // we assign new constraints below. + if (d % 2 != 0) + return; +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
