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

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674