[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

Bal√°zs Benics via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Fri Apr 29 09:01:47 PDT 2022


steakhal added a comment.

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.



================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:93
   /// 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);
 
----------------
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.


================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h:293
                              ExplodedNode *Pred) {
-    return generateNodeImpl(PP, State, Pred, false);
+    return generateNodeImpl(PP, State, Pred, State->isInfeasible());
   }
----------------



================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:86
   GenericDataMap   GDM;      // Custom data stored by a client of this class.
+  bool Infeasible = false;
   unsigned refCount;
----------------
For the record, back then we had such flag. IDK when did we remove it, but we had it for sure.


================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:113-115
+  ProgramStateRef cloneAsInfeasible() const;
+  bool isInfeasible() const { return Infeasible; }
+
----------------
These should not be public. Make friends if required.


================
Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+    ProgramStateRef StFalse = assume(State, Cond, false);
+    if (!StFalse) { // both infeasible
+      ProgramStateRef Infeasible = State->cloneAsInfeasible();
----------------
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?


================
Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:52-54
+      ProgramStateRef Infeasible = State->cloneAsInfeasible();
+      assert(Infeasible->isInfeasible());
+      return ProgramStatePair(Infeasible, Infeasible);
----------------
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.


================
Comment at: clang/test/Analysis/sink-infeasible.c:37-48
+  /* 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
----------------
You could use a non-default check prefix.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D124674/new/

https://reviews.llvm.org/D124674



More information about the cfe-commits mailing list