[clang] 1c1c1e2 - [analyzer] Implement assume in terms of assumeDual
Gabor Marton via cfe-commits
cfe-commits at lists.llvm.org
Tue May 10 01:17:35 PDT 2022
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;
+}
More information about the cfe-commits
mailing list