diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -90,28 +90,7 @@ /// 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); - } + 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 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h @@ -290,7 +290,7 @@ ExplodedNode *generateNode(const ProgramPoint &PP, ProgramStateRef State, ExplodedNode *Pred) { - return generateNodeImpl(PP, State, Pred, false); + return generateNodeImpl(PP, State, Pred, State->isInfeasible()); } /// 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 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h @@ -83,6 +83,7 @@ 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. + bool Infeasible = false; unsigned refCount; /// makeWithStore - Return a ProgramState with the same values as the current @@ -109,6 +110,9 @@ return *stateMgr; } + ProgramStateRef cloneAsInfeasible() const; + bool isInfeasible() const { return Infeasible; } + AnalysisManager &getAnalysisManager() const; /// Return the ConstraintManager. @@ -135,6 +139,7 @@ V->Env.Profile(ID); ID.AddPointer(V->store); V->GDM.Profile(ID); + ID.AddBoolean(V->Infeasible); } /// 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 --- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp @@ -41,3 +41,25 @@ 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 (!StFalse) { // both infeasible + ProgramStateRef Infeasible = State->cloneAsInfeasible(); + assert(Infeasible->isInfeasible()); + return ProgramStatePair(Infeasible, Infeasible); + } + 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 --- a/clang/lib/StaticAnalyzer/Core/ProgramState.cpp +++ b/clang/lib/StaticAnalyzer/Core/ProgramState.cpp @@ -55,7 +55,7 @@ ProgramState::ProgramState(const ProgramState &RHS) : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM), - refCount(0) { + Infeasible(RHS.Infeasible), refCount(0) { stateMgr->getStoreManager().incrementReferenceCount(store); } @@ -429,6 +429,12 @@ return getStateManager().getPersistentState(NewSt); } +ProgramStateRef ProgramState::cloneAsInfeasible() const { + ProgramState NewSt(*this); + NewSt.Infeasible = true; + return getStateManager().getPersistentState(NewSt); +} + void ProgramState::setStore(const StoreRef &newStore) { Store newStoreStore = newStore.getStore(); if (newStoreStore) diff --git a/clang/test/Analysis/sink-infeasible.c b/clang/test/Analysis/sink-infeasible.c new file mode 100644 --- /dev/null +++ b/clang/test/Analysis/sink-infeasible.c @@ -0,0 +1,59 @@ +// 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 +}