[cfe-commits] r89882 - /cfe/trunk/lib/Analysis/GRExprEngine.cpp

[Zhongxing Xu]

I think this is still not correct. And the whole 'early stop'
mechanism may not work. Consider this:
If the receiver is a symbolic value, the checker may bifurcate the
state, generating two states. In one state the receiver is constrained
to nil, in the other to non-nil. They are in the same set. This
mechanism have no way to continue to evaluate the non-nil one.

An alternative way is to let the transfer function (or other checker)
to decide if it is going to evaluate the node according to the state
itself. This is the code in CFRefCount.cpp does:

void CFRefCount::EvalObjCMessageExpr(ExplodedNodeSet& Dst,
                                     GRExprEngine& Eng,
                                     GRStmtNodeBuilder& Builder,
                                     ObjCMessageExpr* ME,
                                     ExplodedNode* Pred) {
  // FIXME: Since we moved the nil check into a checker, we could get nil
  // receiver here. Need a better way to check such case.
  if (Expr* Receiver = ME->getReceiver()) {
    const GRState *state = Pred->getState();
    DefinedOrUnknownSVal L=cast<DefinedOrUnknownSVal>(state->getSVal(Receiver));
    if (!state->Assume(L, true)) {
      Dst.Add(Pred);
      return;
    }
  }

2009/11/26 Ted Kremenek <kremenek at apple.com>:
> Author: kremenek
> Date: Wed Nov 25 15:40:22 2009
> New Revision: 89882
>
> URL: http://llvm.org/viewvc/llvm-project?rev=89882&view=rev
> Log:
> When dispatching to Checker objects in GRExprEngine::CheckerVisit(),
> only stop processing the checkers after all the nodes for a current
> check have been processed.  This (I believe) handles the case where
> PredSet (the input nodes) contains more than one node due to state
> bifurcation.  Zhongxing: can you review this?
>
> Modified:
>    cfe/trunk/lib/Analysis/GRExprEngine.cpp
>
> Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=89882&r1=89881&r2=89882&view=diff
>
> ==============================================================================
> --- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
> +++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Wed Nov 25 15:40:22 2009
> @@ -118,6 +118,7 @@
>
>   ExplodedNodeSet Tmp;
>   ExplodedNodeSet *PrevSet = &Src;
> +  bool stopProcessingAfterCurrentChecker = false;
>
>   for (CheckersOrdered::iterator I=Checkers.begin(),E=Checkers.end(); I!=E; ++I)
>   {
> @@ -127,20 +128,27 @@
>     CurrSet->clear();
>     void *tag = I->first;
>     Checker *checker = I->second;
> -
> +
>     for (ExplodedNodeSet::iterator NI = PrevSet->begin(), NE = PrevSet->end();
>          NI != NE; ++NI) {
>       // FIXME: Halting evaluation of the checkers is something we may
> -      // not support later.  The design is still evolving.
> +      // not support later.  The design is still evolving.
>       if (checker->GR_Visit(*CurrSet, *Builder, *this, S, *NI,
>                             tag, isPrevisit)) {
>         if (CurrSet != &Dst)
>           Dst.insert(*CurrSet);
> -        return true;
> +
> +        stopProcessingAfterCurrentChecker = true;
> +        continue;
>       }
> +      assert(stopProcessingAfterCurrentChecker == false &&
> +             "Inconsistent setting of 'stopProcessingAfterCurrentChecker'");
>     }
> +
> +    if (stopProcessingAfterCurrentChecker)
> +      return true;
>
> -    // Update which NodeSet is the current one.
> +    // Continue on to the next checker.  Update the current NodeSet.
>     PrevSet = CurrSet;
>   }
>
>
>
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
>