Author: Gabor Marton Date: 2020-09-21T16:59:18+02:00 New Revision: 0c4f91f84b2efe8975848a7a13c08d7479abe752
URL: https://github.com/llvm/llvm-project/commit/0c4f91f84b2efe8975848a7a13c08d7479abe752 DIFF: https://github.com/llvm/llvm-project/commit/0c4f91f84b2efe8975848a7a13c08d7479abe752.diff LOG: [analyzer][solver] Fix issue with symbol non-equality tracking We should track non-equivalency (disequality) in case of greater-then or less-then assumptions. Differential Revision: https://reviews.llvm.org/D88019 Added: Modified: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp clang/test/Analysis/equality_tracking.c Removed: ################################################################################ diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 32766d796add..a481bde1651b 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1347,27 +1347,35 @@ class RangeConstraintManager : public RangedConstraintManager { // Equality tracking implementation //===------------------------------------------------------------------===// - ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &Int, + ProgramStateRef trackEQ(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { - if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { - // Extract function assumes that we gave it Sym + Adjustment != Int, - // so the result should be opposite. - Equality->invert(); - return track(State, *Equality); - } - - return State; + return track<true>(NewConstraint, State, Sym, Int, Adjustment); } - ProgramStateRef trackNE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &Int, + ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { + return track<false>(NewConstraint, State, Sym, Int, Adjustment); + } + + template <bool EQ> + ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + if (NewConstraint.isEmpty()) + // This is an infeasible assumption. + return nullptr; + + ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint); if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { - return track(State, *Equality); + // If the original assumption is not Sym + Adjustment !=/</> Int, + // we should invert IsEquality flag. + Equality->IsEquality = Equality->IsEquality != EQ; + return track(NewState, *Equality); } - return State; + return NewState; } ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) { @@ -2042,12 +2050,7 @@ RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point); - if (New.isEmpty()) - // this is infeasible assumption - return nullptr; - - ProgramStateRef NewState = setConstraint(St, Sym, New); - return trackNE(NewState, Sym, Int, Adjustment); + return trackNE(New, St, Sym, Int, Adjustment); } ProgramStateRef @@ -2063,12 +2066,7 @@ RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); - if (New.isEmpty()) - // this is infeasible assumption - return nullptr; - - ProgramStateRef NewState = setConstraint(St, Sym, New); - return trackEQ(NewState, Sym, Int, Adjustment); + return trackEQ(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St, @@ -2104,7 +2102,7 @@ RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymLTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St, @@ -2140,7 +2138,7 @@ RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymGTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St, diff --git a/clang/test/Analysis/equality_tracking.c b/clang/test/Analysis/equality_tracking.c index 3103e8516dcd..086db1070c64 100644 --- a/clang/test/Analysis/equality_tracking.c +++ b/clang/test/Analysis/equality_tracking.c @@ -185,3 +185,37 @@ void avoidInfeasibleConstraintsForClasses(int a, int b) { } } } + +void avoidInfeasibleConstraintforGT(int a, int b) { + int c = b - a; + if (c <= 0) + return; + // c > 0 + // b - a > 0 + // b > a + if (a != b) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + return; + } + clang_analyzer_warnIfReached(); // no warning + // a == b + if (c < 0) + ; +} + +void avoidInfeasibleConstraintforLT(int a, int b) { + int c = b - a; + if (c >= 0) + return; + // c < 0 + // b - a < 0 + // b < a + if (a != b) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + return; + } + clang_analyzer_warnIfReached(); // no warning + // a == b + if (c < 0) + ; +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
