martong updated this revision to Diff 379189.
martong marked 3 inline comments as done.
martong added a comment.
- Fix logic error
- Add more test cases
- Use SymbolRef
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,93 @@
+// 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.
+}
+
+void rem_constant_rhs_eq_zero_early_contradiction(int x, int y) {
+ if (x == 0) // x != 0
+ return;
+ if (x % 3 != 0) // x % 3 == 0 -> x == 0 -> contradiction
+ return;
+ clang_analyzer_warnIfReached(); // no-warning
+ (void)x; // keep the constraints alive.
+}
+
+void rem_symbolic_rhs_eq_zero_early_contradiction(int x, int y, int z) {
+ if (x == 0) // x != 0
+ return;
+ if (x % z != 0) // x % z == 0 -> x == 0 -> contradiction
+ return;
+ clang_analyzer_warnIfReached(); // no-warning
+ (void)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.
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1610,7 +1610,35 @@
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, LHS->getType());
+ const llvm::APSInt *ConcreteValue = Constraint.getConcreteValue();
+ // a % b == 0 implies that a == 0.
+ if (ConcreteValue && *ConcreteValue == Zero) {
+ State = RCM.assumeSymEQ(State, LHS, Zero, Zero);
+ if (!State)
+ return false;
+ }
+ // 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 +1716,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 +1760,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
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
