Author: Gabor Marton Date: 2021-10-27T17:14:34+02:00 New Revision: a8297ed994301dbf34f259690e9f5fa8fce96ea2
URL: https://github.com/llvm/llvm-project/commit/a8297ed994301dbf34f259690e9f5fa8fce96ea2 DIFF: https://github.com/llvm/llvm-project/commit/a8297ed994301dbf34f259690e9f5fa8fce96ea2.diff LOG: [Analyzer][solver] Handle adjustments in constraint assignor remainder We can reuse the "adjustment" handling logic in the higher level of the solver by calling `State->assume`. Differential Revision: https://reviews.llvm.org/D112296 Added: Modified: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp clang/test/Analysis/constraint-assignor.c Removed: ################################################################################ diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 77f97da4322b3..6e4ee6e337ce5 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1614,14 +1614,14 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> { 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; + SVal SymSVal = Builder.makeSymbolVal(Sym->getLHS()); + if (auto NonLocSymSVal = SymSVal.getAs<nonloc::SymbolVal>()) { + State = State->assume(*NonLocSymSVal, true); + if (!State) + return false; + } } return true; } diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp index 80f3054a5a37f..892d64ea4e4e2 100644 --- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -41,7 +41,12 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State, return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS()); } - } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) { + // Handle adjustment with non-comparison ops. + const llvm::APSInt &Zero = getBasicVals().getValue(0, SIE->getType()); + return assumeSymRel(State, SIE, (Assumption ? BO_NE : BO_EQ), Zero); + } + + if (const auto *SSE = dyn_cast<SymSymExpr>(Sym)) { BinaryOperator::Opcode Op = SSE->getOpcode(); assert(BinaryOperator::isComparisonOp(Op)); diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c index 1c041e3e0ce45..1b9e40e6bf649 100644 --- a/clang/test/Analysis/constraint-assignor.c +++ b/clang/test/Analysis/constraint-assignor.c @@ -3,9 +3,8 @@ // RUN: -analyzer-checker=debug.ExprInspection \ // RUN: -verify -// expected-no-diagnostics - void clang_analyzer_warnIfReached(); +void clang_analyzer_eval(int); void rem_constant_rhs_ne_zero(int x, int y) { if (x % 3 == 0) // x % 3 != 0 -> x != 0 @@ -67,3 +66,19 @@ void internal_unsigned_signed_mismatch(unsigned a) { if (d % 2 != 0) return; } + +void remainder_with_adjustment(int x) { + if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1 + return; + clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x != -1); // expected-warning{{TRUE}} + (void)x; // keep the constraints alive. +} + +void remainder_with_adjustment_of_composit_lhs(int x, int y) { + if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1 + return; + clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x + y != -1); // expected-warning{{TRUE}} + (void)(x * y); // keep the constraints alive. +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
