[analyzer] Indicate if a parent state is infeasible

[martong]

Summary

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

[martong]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

96–97

This statement is false because our constraint solver is not precise.

[steakhal]

Finally, we have this!

Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you proposed?
I find it more readable.

What performance hit will we suffer from this change?
Please do a differential analysis.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

93–96

I would leave a note here that these two states might be equal in a very rare case (*); but one should not depend on that.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h

293–295

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

88

For the record, back then we had such flag. IDK when did we remove it, but we had it for sure.

148–150

These should not be public. Make friends if required.

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

51

Should we mark this LLVM_UNLIKELY(cond)?
I would expect this function to be quite hot, and infeasible states rare.

Could we measure this one?

52–54

Add here some comments on why we return (Infeasible,Infeasible).
I would rather see StInfeasible to better discriminate what we are talking about. We already use StTrue and StFalse in this context though.

clang/test/Analysis/sink-infeasible.c

37–48 ↗

(On Diff #426061)

You could use a non-default check prefix.

[martong]

• Update according to review comments

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

51

Yes, it could be.

Let me come back with some measurement results soon. I am going to use llvm statistics macros to measure this, but that makes sense on top of D124758

clang/test/Analysis/sink-infeasible.c

37–48 ↗

(On Diff #426061)

No I can't, because this test code in the comment is meaningful only in the baseline, I cannot run both clang versions from lit.

So, actually there is no RUN line for these, it is here only to demonstrate what happens in the baseline.

[martong]

In D124674#3482765, @steakhal wrote:

Finally, we have this!

Thanks for the review.

Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you proposed?
I find it more readable.

Sure, I find it also more readable. I will update soon.

What performance hit will we suffer from this change?
Please do a differential analysis.

I am doing that with the dependent patch https://reviews.llvm.org/D124758

[steakhal]

I think I don't have anything left.
Let's see the numbers.

clang/test/Analysis/sink-infeasible.c

37–48 ↗

(On Diff #426061)

Okay, why don't we drop these if these are only applicable to the baseline?
Should we really introduce 'stale' comments?

[martong]

• Add a simpler test case

[martong]

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

51

This is what I use for the measurement, stay tuned for the results.

diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index ef98ed7d36e9..82097d67ec0f 100644
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -16,10 +16,16 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "llvm/ADT/Statistic.h"

 using namespace clang;
 using namespace ento;

+#define DEBUG_TYPE "CoreEngine"
+
+STATISTIC(NumInfeasible, "The # of infeasible states");
+STATISTIC(NumFeasible, "The # of feasible states");
+
 ConstraintManager::~ConstraintManager() = default;

 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
@@ -51,16 +57,20 @@ ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
     if (!StFalse) { // both infeasible
       ProgramStateRef Infeasible = State->cloneAsInfeasible();
       assert(Infeasible->isInfeasible());
+      ++NumInfeasible;
       return ProgramStatePair(Infeasible, Infeasible);
     }
+    ++NumFeasible;
     return ProgramStatePair(nullptr, StFalse);
   }

   ProgramStateRef StFalse = assumeInternal(State, Cond, false);
   if (!StFalse) {
+    ++NumFeasible;
     return ProgramStatePair(StTrue, nullptr);
   }

+  ++NumFeasible;
   return ProgramStatePair(StTrue, StFalse);
 }

[martong]

clang/test/Analysis/sink-infeasible.c

37–48 ↗

(On Diff #426061)

Ok, I can remove them if you insist, but I thought it might make it easier to understand what is changed.

[martong]

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

51

Ups, the purpose of the measure is to determine if UNLIKELY is justified, so this diff seems better, restarted the measurement with it.

--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -16,10 +16,16 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "llvm/ADT/Statistic.h"

 using namespace clang;
 using namespace ento;

+#define DEBUG_TYPE "CoreEngine"
+
+STATISTIC(NumInfeasible, "The # of infeasible states");
+STATISTIC(NumFeasible, "The # of feasible states");
+
 ConstraintManager::~ConstraintManager() = default;

 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
@@ -51,8 +57,10 @@ ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
     if (!StFalse) { // both infeasible
       ProgramStateRef Infeasible = State->cloneAsInfeasible();
       assert(Infeasible->isInfeasible());
+      ++NumInfeasible;
       return ProgramStatePair(Infeasible, Infeasible);
     }
+    ++NumFeasible;
     return ProgramStatePair(nullptr, StFalse);
   }

[martong]

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

51

This is indeed UNLIKELY. Seems like a good upper-bound for the ratio's order of magnitude is around 1000 / 10 million i.e. 0.0001.

[martong]

• Add LLVM_UNLIKELY

[martong]

@NoQ Could you please take a look? This change effects the very core of the analyzer.

[NoQ]

Yes, we've discussed this before, and I'm very much in favor of this change. This is assertion removal, and the assertion has been really useful back in the day, but the assertion doesn't seem to be realistic to maintain with all the new logic in the constraint solver coming in in recent years.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

88

The reader deserves a massive amount of explanation here. Normally infeasible states are just null states. We need to explain how these new infeasible states are different.

Maybe a longer name? IsPostOverconstrained or something like that.

[martong]

In D124674#3491710, @NoQ wrote:

Yes, we've discussed this before, and I'm very much in favor of this change. This is assertion removal, and the assertion has been really useful back in the day, but the assertion doesn't seem to be realistic to maintain with all the new logic in the constraint solver coming in in recent years.

Thanks for your review and support!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

88

Okay, I've added an essay that explains these differences.

Maybe a longer name? IsPostOverconstrained or something like that.

Yeah, I agree a longer name could reflect that this is something that requires special handling. I chose PosteriorlyOverconstrained.

[martong]

• Add explanatory comment, rename to PosteriorlyOverconstrained

[steakhal]

only a few typos

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

89–114

[martong]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

99

Yeah, thx, I've also found one more typo. That's the problem with long comments :D

[martong]

• Fix typos in essay

[thakis]

One of your 3 commits in https://github.com/llvm/llvm-project/compare/3d888b0491f8...34ac048aef29 broke check-clang on Windows: http://45.33.8.238/win/57870/step_7.txt

Please take a look, and revert for now if it takes a while to fix.

[thakis]

https://github.com/llvm/llvm-project/commit/21feafaeb85aad2847db44aa2208999b166ba4a9 fixed it, thanks!

[martong]

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

46

TODO We should have a very similar implementation for assumeInclusiveRangeDual! (Not that high prio, that is used only by the BoolAssignmentChecker).

[• galapoz1996]

This comment was removed by mehdi_amini.

[• Balazom]

This comment was removed by mehdi_amini.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

public:
   virtual ProgramStateRef assume(ProgramStateRef state,
                                  DefinedSVal Cond,
                                  bool Assumption) = 0;
 
   using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
 
   /// 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,
                                                const llvm::APSInt &From,
                                                const llvm::APSInt &To,
                                                bool InBound) = 0;
 
   virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,

clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h

public:
   }
 
   virtual ~NodeBuilder() = default;
 
   /// Generates a node in the ExplodedGraph.
   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.
   ///
   /// When a node is marked as sink, the exploration from the node is stopped -
   /// the node becomes the last node on the path and certain kinds of bugs are
   /// suppressed.
   ExplodedNode *generateSink(const ProgramPoint &PP,

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

public:
   typedef llvm::ImmutableMap<void*, void*>                 GenericDataMap;
 
 private:
   void operator=(const ProgramState& R) = delete;
 
   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
   ///  state with the exception of using the specified Store.
   ProgramStateRef makeWithStore(const StoreRef &store) const;
 
   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,
           StoreRef st, GenericDataMap gdm);
 
   /// Copy ctor - We must explicitly define this or else the "Next" ptr
   ///  in FoldingSetNode will also get copied.
   ProgramState(const ProgramState &RHS);
 
   ~ProgramState();
 
   int64_t getID() const;
 
   /// Return the ProgramStateManager associated with this state.
   ProgramStateManager &getStateManager() const {
     return *stateMgr;
   }
 
   AnalysisManager &getAnalysisManager() const;
 
   /// Return the ConstraintManager.
   ConstraintManager &getConstraintManager() const;
 
   /// getEnvironment - Return the environment associated with this state.
   ///  The environment is the mapping from expressions to values.
   const Environment& getEnvironment() const { return Env; }
 
   /// Return the store associated with this state.  The store
   ///  is a mapping from locations to values.
   Store getStore() const { return store; }
 
 
   /// getGDM - Return the generic data map associated with this state.
   GenericDataMap getGDM() const { return GDM; }
 
   void setGDM(GenericDataMap gdm) { GDM = gdm; }
 
   /// Profile - Profile the contents of a ProgramState object for use in a
   ///  FoldingSet.  Two ProgramState objects are considered equal if they
   ///  have the same Environment, Store, and GenericDataMap.
   static void Profile(llvm::FoldingSetNodeID& ID, const ProgramState *V) {
     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
   ///  in a FoldingSet.
   void Profile(llvm::FoldingSetNodeID& ID) const {
     Profile(ID, this);
   }
 

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
                                      : nonloc::SymbolVal(Sym);
   const ProgramStatePair &P = assumeDual(State, V);
   if (P.first && !P.second)
     return ConditionTruthVal(false);
   if (!P.first && P.second)
     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);
+}

clang/lib/StaticAnalyzer/Core/ProgramState.cpp

: stateMgr(mgr),
     store(st.getStore()),
     GDM(gdm),
     refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
 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);
 }
 
 ProgramState::~ProgramState() {
   if (store)
     stateMgr->getStoreManager().decrementReferenceCount(store);
 }
 

 }
 
 ProgramStateRef ProgramState::makeWithStore(const StoreRef &store) const {
   ProgramState NewSt(*this);
   NewSt.setStore(store);
   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)
     stateMgr->getStoreManager().incrementReferenceCount(newStoreStore);
   if (store)
     stateMgr->getStoreManager().decrementReferenceCount(store);
   store = newStoreStore;
 }

clang/test/Analysis/infeasible-sink.c

+// 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
+}