Author: Gabor Marton Date: 2022-05-10T10:16:55+02:00 New Revision: 1c1c1e25f94fd1bb10fdbfe96dc14ffc655db5df
URL: https://github.com/llvm/llvm-project/commit/1c1c1e25f94fd1bb10fdbfe96dc14ffc655db5df DIFF: https://github.com/llvm/llvm-project/commit/1c1c1e25f94fd1bb10fdbfe96dc14ffc655db5df.diff LOG: [analyzer] Implement assume in terms of assumeDual Summary: By evaluating both children states, now we are capable of discovering infeasible parent states. In this patch, `assume` is implemented in the terms of `assumeDuali`. This might be suboptimal (e.g. where there are adjacent assume(true) and assume(false) calls, next patches addresses that). This patch fixes a real CRASH. Fixes https://github.com/llvm/llvm-project/issues/54272 Differential Revision: https://reviews.llvm.org/D124758 Added: clang/test/Analysis/infeasible-crash.c Modified: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Removed: ################################################################################ diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h index 3beee3980c96..f0dbcfd7dbff 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -82,9 +82,8 @@ class ConstraintManager { virtual bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const = 0; - virtual ProgramStateRef assume(ProgramStateRef state, - DefinedSVal Cond, - bool Assumption) = 0; + ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, + bool Assumption); using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>; @@ -161,6 +160,9 @@ class ConstraintManager { /// but not thread-safe. bool NotifyAssumeClients = true; + virtual ProgramStateRef assumeInternal(ProgramStateRef state, + DefinedSVal Cond, bool Assumption) = 0; + /// canReasonAbout - Not all ConstraintManagers can accurately reason about /// all SVal values. This method returns true if the ConstraintManager can /// reasonably handle a given SVal value. This is typically queried by diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h index 87e927f5b480..50206f6883ad 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h @@ -36,8 +36,8 @@ class SimpleConstraintManager : public ConstraintManager { /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by /// creating boolean casts to handle Loc's. - ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, - bool Assumption) override; + ProgramStateRef assumeInternal(ProgramStateRef State, DefinedSVal Cond, + bool Assumption) override; ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp index 2b23fef6160b..c29b3ab50a3c 100644 --- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp @@ -44,10 +44,10 @@ ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State, ConstraintManager::ProgramStatePair ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) { - ProgramStateRef StTrue = assume(State, Cond, true); + ProgramStateRef StTrue = assumeInternal(State, Cond, true); if (!StTrue) { - ProgramStateRef StFalse = assume(State, Cond, false); + ProgramStateRef StFalse = assumeInternal(State, Cond, false); if (LLVM_UNLIKELY(!StFalse)) { // both infeasible ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained(); assert(StInfeasible->isPosteriorlyOverconstrained()); @@ -63,10 +63,16 @@ ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) { return ProgramStatePair(nullptr, StFalse); } - ProgramStateRef StFalse = assume(State, Cond, false); + ProgramStateRef StFalse = assumeInternal(State, Cond, false); if (!StFalse) { return ProgramStatePair(StTrue, nullptr); } return ProgramStatePair(StTrue, StFalse); } + +ProgramStateRef ConstraintManager::assume(ProgramStateRef State, + DefinedSVal Cond, bool Assumption) { + ConstraintManager::ProgramStatePair R = assumeDual(State, Cond); + return Assumption ? R.first : R.second; +} diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp index f96974f97dcc..0a9814a17860 100644 --- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -22,9 +22,9 @@ namespace ento { SimpleConstraintManager::~SimpleConstraintManager() {} -ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State, - DefinedSVal Cond, - bool Assumption) { +ProgramStateRef SimpleConstraintManager::assumeInternal(ProgramStateRef State, + DefinedSVal Cond, + bool Assumption) { // If we have a Loc value, cast it to a bool NonLoc first. if (Optional<Loc> LV = Cond.getAs<Loc>()) { SValBuilder &SVB = State->getStateManager().getSValBuilder(); @@ -86,8 +86,8 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State, } case nonloc::LocAsIntegerKind: - return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(), - Assumption); + return assumeInternal(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(), + Assumption); } // end switch } diff --git a/clang/test/Analysis/infeasible-crash.c b/clang/test/Analysis/infeasible-crash.c new file mode 100644 index 000000000000..66ea77f0a86f --- /dev/null +++ b/clang/test/Analysis/infeasible-crash.c @@ -0,0 +1,37 @@ +// RUN: %clang_analyze_cc1 %s \ +// RUN: -analyzer-checker=core \ +// RUN: -analyzer-checker=alpha.unix.cstring.OutOfBounds,alpha.unix.cstring.UninitializedRead \ +// RUN: -analyzer-config eagerly-assume=false \ +// RUN: -verify + +// expected-no-diagnostics + +void *memmove(void *, const void *, unsigned long); + +typedef struct { + char a[1024]; +} b; +int c; +b *invalidate(); +int d() { + b *a = invalidate(); + if (c < 1024) + return 0; + int f = c & ~3, g = f; + g--; + if (g) + return 0; + + // Parent state is already infeasible. + // clang_analyzer_printState(); + // "constraints": [ + // { "symbol": "(derived_$3{conj_$0{int, LC1, S728, #1},c}) & -4", "range": "{ [1, 1] }" }, + // { "symbol": "derived_$3{conj_$0{int, LC1, S728, #1},c}", "range": "{ [1024, 2147483647] }" } + // ], + + // This sould not crash! + // It crashes in baseline, since there both true and false states are nullptr! + memmove(a->a, &a->a[f], c - f); + + return 0; +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
