Hi Zhongxing,
My plan was not to leave this mechanism in place for Pre/PostVisits. All I
care about right now is that it works for the nil-receiver check. It's not
meant to be an extension to the general API. It's a stop-gap for a better
solution where we can dispatch to Checker logic to handle the evaluation of the
entire message expression or function call. That would be something like
"EvalCall" or "EvalObjCMessageExpr". My thought is that we can dispatch to
such methods, much like we do in GRExprEngine::CheckerVisit(), except that we
stop walking through the chain of Checkers after one of them generates *any*
node. In other words, if a Checker knows how to handle a specific function or
message expression, it handles it, otherwise it passes it on to the next
checker. This might allow us to model "domain-specific" knowledge of specific
APIs, effects of functions, etc. For example, this approach could handle the
nil-receiver check as well as the OSAtomics logic (which is currentl!
y mangled into GRExprEngine directly). It's only a rough idea, and I'd like
to discuss it with you more offline.
On Nov 25, 2009, at 6:28 PM, Zhongxing Xu wrote:
> 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 <[email protected]>:
>> 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
>> [email protected]
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
>>
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
