martong created this revision.
martong added reviewers: NoQ, steakhal, ASDenysPetrov.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, Szelethus,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun.
Herald added a reviewer: Szelethus.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
By evaluating both children states, now we are capable of discovering
infeasible parent states. In this patch, `assume` is implemented in the terms
of `assumeDual`. 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
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D124758
Files:
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
clang/test/Analysis/infeasible-crash.c
clang/test/Analysis/infeasible-sink.c
clang/test/Analysis/sink-infeasible.c
Index: clang/test/Analysis/sink-infeasible.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/sink-infeasible.c
@@ -1,59 +0,0 @@
-// RUN: %clang_analyze_cc1 %s \
-// RUN: -analyzer-checker=core \
-// RUN: -analyzer-checker=debug.ExprInspection \
-// RUN: -analyzer-config eagerly-assume=false \
-// RUN: -verify
-
-// Here we test that if it turns out that the parent state is infeasible then
-// both children States (more precisely the ExplodedNodes) are marked as a
-// Sink.
-// We rely on an existing defect of the underlying constraint solver. However,
-// in the future we might strengthen the solver to discover the infeasibility
-// right when we create the parent state. At that point this test will fail,
-// and either we shall find another solver weakness to have this test case
-// functioning, or we shall simply remove this test.
-
-void clang_analyzer_warnIfReached();
-void clang_analyzer_eval(int);
-
-int a, b, c, d, e;
-void f() {
-
- if (a == 0)
- return;
-
- if (e != c)
- return;
-
- d = e - c;
- b = d;
- a -= d;
-
- if (a != 0)
- return;
-
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
-
- /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
- // The parent state is already infeasible, look at this contradiction:
- clang_analyzer_eval(b > 0); // expected-wrning{{FALSE}}
- clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
- // Crashes with expensive checks.
- if (b > 0) {
- clang_analyzer_warnIfReached(); // no-warning, OK
- return;
- }
- // Should not be reachable.
- clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
- */
-
- // The parent state is already infeasible, but we realize that only if b is
- // constrained.
- clang_analyzer_eval(b > 0); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
- if (b > 0) {
- clang_analyzer_warnIfReached(); // no-warning
- return;
- }
- clang_analyzer_warnIfReached(); // no-warning
-}
Index: clang/test/Analysis/infeasible-crash.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/infeasible-crash.c
@@ -0,0 +1,38 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=alpha.unix.cstring.OutOfBounds,alpha.unix.cstring.UninitializedRead \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// 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;
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -22,9 +22,9 @@
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 @@
}
case nonloc::LocAsIntegerKind:
- return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
- Assumption);
+ return assumeInternal(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
+ Assumption);
} // end switch
}
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -44,10 +44,10 @@
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 (!StFalse) { // both infeasible
ProgramStateRef Infeasible = State->cloneAsInfeasible();
assert(Infeasible->isInfeasible());
@@ -56,10 +56,16 @@
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;
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
@@ -36,8 +36,8 @@
/// 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,
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -82,9 +82,8 @@
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>;
@@ -158,6 +157,9 @@
/// 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
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
