From c4fa05f5f7783efa380c200d96cc1f756fa88c6c Mon Sep 17 00:00:00 2001 From: Gabor Marton Date: Tue, 3 May 2022 12:11:49 +0200 Subject: [PATCH] [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 --- .../Core/PathSensitive/ConstraintManager.h | 26 ++----- .../StaticAnalyzer/Core/PathSensitive/CoreEngine.h | 4 +- .../Core/PathSensitive/ProgramState.h | 37 ++++++++++ .../lib/StaticAnalyzer/Core/ConstraintManager.cpp | 29 ++++++++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp | 8 ++- clang/test/Analysis/infeasible-sink.c | 80 ++++++++++++++++++++++ 6 files changed, 160 insertions(+), 24 deletions(-) create mode 100644 clang/test/Analysis/infeasible-sink.c diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h index 335536b..3beee39 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -90,28 +90,10 @@ public: /// 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 9898b9b..760dc1d 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h @@ -290,7 +290,9 @@ public: 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 cf285c1e..0e28310 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h @@ -78,11 +78,42 @@ private: 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 @@ private: 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 @@ public: 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 d642c35..2b23fef 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 8d4e0bb..9d84b81 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 0000000..9cb66fc --- /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 +} -- 2.7.4