[clang] c4fa05f - [analyzer] Indicate if a parent state is infeasible
Gabor Marton via cfe-commits
cfe-commits at lists.llvm.org
Tue May 10 01:17:33 PDT 2022
Author: Gabor Marton
Date: 2022-05-10T10:16:55+02:00
New Revision: c4fa05f5f7783efa380c200d96cc1f756fa88c6c
URL: https://github.com/llvm/llvm-project/commit/c4fa05f5f7783efa380c200d96cc1f756fa88c6c
DIFF: https://github.com/llvm/llvm-project/commit/c4fa05f5f7783efa380c200d96cc1f756fa88c6c.diff
LOG: [analyzer] Indicate if a parent state is infeasible
In some cases a parent State is already infeasible, but we recognize
this only if an additonal constraint is added. This patch is the first
of a series to address this issue. In this patch `assumeDual` is changed
to clone the parent State but with an `Infeasible` flag set, and this
infeasible-parent is returned both for the true and false case. Then
when we add a new transition in the exploded graph and the destination
is marked as infeasible, the node will be a sink node.
Related bug:
https://github.com/llvm/llvm-project/issues/50883
Actually, this patch does not solve that bug in the solver, rather with
this patch we can handle the general parent-infeasible cases.
Next step would be to change the State API and require all checkers to
use the `assume*Dual` API and deprecate the simple `assume` calls.
Hopefully, the next patch will introduce `assumeInBoundDual` and will
solve the CRASH we have here:
https://github.com/llvm/llvm-project/issues/54272
Differential Revision: https://reviews.llvm.org/D124674
Added:
clang/test/Analysis/infeasible-sink.c
Modified:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/ProgramState.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 335536b6a3106..3beee3980c963 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -90,28 +90,10 @@ class ConstraintManager {
/// Returns a pair of states (StTrue, StFalse) where the given condition is
/// assumed to be true or false, respectively.
- ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
- ProgramStateRef StTrue = assume(State, Cond, true);
-
- // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
- // because the existing constraints already establish this.
- if (!StTrue) {
-#ifdef EXPENSIVE_CHECKS
- assert(assume(State, Cond, false) && "System is over constrained.");
-#endif
- return ProgramStatePair((ProgramStateRef)nullptr, State);
- }
-
- ProgramStateRef StFalse = assume(State, Cond, false);
- if (!StFalse) {
- // We are careful to return the original state, /not/ StTrue,
- // because we want to avoid having callers generate a new node
- // in the ExplodedGraph.
- return ProgramStatePair(State, (ProgramStateRef)nullptr);
- }
-
- return ProgramStatePair(StTrue, StFalse);
- }
+ /// (Note that these two states might be equal if the parent state turns out
+ /// to be infeasible. This may happen if the underlying constraint solver is
+ /// not perfectly precise and this may happen very rarely.)
+ ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
NonLoc Value,
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
index 9898b9b42f4b2..760dc1d3e96c1 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
@@ -290,7 +290,9 @@ class NodeBuilder {
ExplodedNode *generateNode(const ProgramPoint &PP,
ProgramStateRef State,
ExplodedNode *Pred) {
- return generateNodeImpl(PP, State, Pred, false);
+ return generateNodeImpl(
+ PP, State, Pred,
+ /*MarkAsSink=*/State->isPosteriorlyOverconstrained());
}
/// Generates a sink in the ExplodedGraph.
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
index cf285c1e1d557..0e283103f5c2e 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
@@ -78,11 +78,42 @@ class ProgramState : public llvm::FoldingSetNode {
friend class ProgramStateManager;
friend class ExplodedGraph;
friend class ExplodedNode;
+ friend class NodeBuilder;
+ friend class ConstraintManager;
ProgramStateManager *stateMgr;
Environment Env; // Maps a Stmt to its current SVal.
Store store; // Maps a location to its current value.
GenericDataMap GDM; // Custom data stored by a client of this class.
+
+ // A state is infeasible if there is a contradiction among the constraints.
+ // An infeasible state is represented by a `nullptr`.
+ // In the sense of `assumeDual`, a state can have two children by adding a
+ // new constraint and the negation of that new constraint. A parent state is
+ // over-constrained if both of its children are infeasible. In the
+ // mathematical sense, it means that the parent is infeasible and we should
+ // have realized that at the moment when we have created it. However, we
+ // could not recognize that because of the imperfection of the underlying
+ // constraint solver. We say it is posteriorly over-constrained because we
+ // recognize that a parent is infeasible only *after* a new and more specific
+ // constraint and its negation are evaluated.
+ //
+ // Example:
+ //
+ // x * x = 4 and x is in the range [0, 1]
+ // This is an already infeasible state, but the constraint solver is not
+ // capable of handling sqrt, thus we don't know it yet.
+ //
+ // Then a new constraint `x = 0` is added. At this moment the constraint
+ // solver re-evaluates the existing constraints and realizes the
+ // contradiction `0 * 0 = 4`.
+ // We also evaluate the negated constraint `x != 0`; the constraint solver
+ // deduces `x = 1` and then realizes the contradiction `1 * 1 = 4`.
+ // Both children are infeasible, thus the parent state is marked as
+ // posteriorly over-constrained. These parents are handled with special care:
+ // we do not allow transitions to exploded nodes with such states.
+ bool PosteriorlyOverconstrained = false;
+
unsigned refCount;
/// makeWithStore - Return a ProgramState with the same values as the current
@@ -91,6 +122,11 @@ class ProgramState : public llvm::FoldingSetNode {
void setStore(const StoreRef &storeRef);
+ ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
+ bool isPosteriorlyOverconstrained() const {
+ return PosteriorlyOverconstrained;
+ }
+
public:
/// This ctor is used when creating the first ProgramState object.
ProgramState(ProgramStateManager *mgr, const Environment& env,
@@ -135,6 +171,7 @@ class ProgramState : public llvm::FoldingSetNode {
V->Env.Profile(ID);
ID.AddPointer(V->store);
V->GDM.Profile(ID);
+ ID.AddBoolean(V->PosteriorlyOverconstrained);
}
/// Profile - Used to profile the contents of this object for inclusion
diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index d642c35302681..2b23fef6160b5 100644
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@ ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State,
return ConditionTruthVal(true);
return {};
}
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+ ProgramStateRef StTrue = assume(State, Cond, true);
+
+ if (!StTrue) {
+ ProgramStateRef StFalse = assume(State, Cond, false);
+ if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
+ ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
+ assert(StInfeasible->isPosteriorlyOverconstrained());
+ // Checkers might rely on the API contract that both returned states
+ // cannot be null. Thus, we return StInfeasible for both branches because
+ // it might happen that a Checker uncoditionally uses one of them if the
+ // other is a nullptr. This may also happen with the non-dual and
+ // adjacent `assume(true)` and `assume(false)` calls. By implementing
+ // assume in therms of assumeDual, we can keep our API contract there as
+ // well.
+ return ProgramStatePair(StInfeasible, StInfeasible);
+ }
+ return ProgramStatePair(nullptr, StFalse);
+ }
+
+ ProgramStateRef StFalse = assume(State, Cond, false);
+ if (!StFalse) {
+ return ProgramStatePair(StTrue, nullptr);
+ }
+
+ return ProgramStatePair(StTrue, StFalse);
+}
diff --git a/clang/lib/StaticAnalyzer/Core/ProgramState.cpp b/clang/lib/StaticAnalyzer/Core/ProgramState.cpp
index 8d4e0bbb7dec9..9d84b816c122f 100644
--- a/clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@ ProgramState::ProgramState(ProgramStateManager *mgr, const Environment& env,
ProgramState::ProgramState(const ProgramState &RHS)
: stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
- refCount(0) {
+ PosteriorlyOverconstrained(RHS.PosteriorlyOverconstrained), refCount(0) {
stateMgr->getStoreManager().incrementReferenceCount(store);
}
@@ -429,6 +429,12 @@ ProgramStateRef ProgramState::makeWithStore(const StoreRef &store) const {
return getStateManager().getPersistentState(NewSt);
}
+ProgramStateRef ProgramState::cloneAsPosteriorlyOverconstrained() const {
+ ProgramState NewSt(*this);
+ NewSt.PosteriorlyOverconstrained = true;
+ return getStateManager().getPersistentState(NewSt);
+}
+
void ProgramState::setStore(const StoreRef &newStore) {
Store newStoreStore = newStore.getStore();
if (newStoreStore)
diff --git a/clang/test/Analysis/infeasible-sink.c b/clang/test/Analysis/infeasible-sink.c
new file mode 100644
index 0000000000000..9cb66fcac0b6b
--- /dev/null
+++ b/clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 existing defects 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 some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+ if (x * x != 4)
+ return;
+ if (x < 0 || x > 1)
+ return;
+
+ // { x^2 == 4 and x:[0,1] }
+ // This state is already infeasible.
+
+ // Perfectly constraining 'x' will trigger constant folding,
+ // when we realize we were already infeasible.
+ // The same happens for the 'else' branch.
+ if (x == 0) {
+ clang_analyzer_warnIfReached(); // no-warning
+ } else {
+ clang_analyzer_warnIfReached(); // no-warning
+ }
+ clang_analyzer_warnIfReached(); // no-warning
+ (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+ 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
+}
More information about the cfe-commits
mailing list