martong updated this revision to Diff 379988.
martong added a comment.
- Remove the wrong inferrence of `a % b == 0 implies that a == 0` and related
test cases.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D110357/new/
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,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;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1610,7 +1610,28 @@
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 @@
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::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
RangeSet Constraint) {
+ if (!handleRemainderOp(Sym, Constraint))
+ return false;
+
Optional<bool> ConstraintAsBool = interpreteAsBool(Constraint);
if (!ConstraintAsBool)
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
@@ -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;
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
