================
@@ -124,24 +124,26 @@ void ExprEngine::VisitObjCForCollectionStmt(const 
ObjCForCollectionStmt *S,
 
   bool isContainerNull = state->isNull(collectionV).isConstrainedTrue();
 
-  ExplodedNodeSet dstLocation;
-  evalLocation(dstLocation, S, elem, Pred, state, elementV, false);
----------------
ziqingluo-90 wrote:

To elaborate the issue, suppose `evalLocation` alters the `Pred` state and 
populates the new states in `dstLocation`. (This name `dstLocation` is a bit 
confusing IMO, let's call those new states `NewPreds` instead.)  However,  the 
`StmtNodeBuilder` below still takes `Pred` as the source state (old line 131) 
while the next transitions computed in `populateObjCForDestinationSet` are 
computed from `NewPreds` (old line 134 & 138).

The confusion here is that there suppose to be transitions:
`Pred --evalLocation--> NewPreds --populateObjCForDestinationSet--> Dest`
but the `StmtNodeBuilder` used for the second transition above assumes the 
source state is `Pred` instead of `NewPreds`.   This is what's wrong with this 
function `VisitObjCForCollectionStmt`.

Then how does the bug lead to a crash?

The way `StmtNodeBuilder` works is that it maintains a `Frontier` set---the set 
of states to be explored next.   After initialization (old line 131),  
`Frontier = {Pred}`.    In `populateObjCForDestinationSet`, `StmtNodeBuilder` 
is used to generate `Dest` and remove source state from the set.  Note that 
`NewPreds` are passed to `populateObjCForDestinationSet` as source states.  So 
`StmtNodeBuilder` attempts to remove `NewPreds` from the set, which does not 
change the set.   Finally, `Frontier = {Pred, Dest}`.

Starting from this ill-formed `Frontier` set, the engine executes 
[`hasMoreIterations`](https://github.com/llvm/llvm-project/blob/e8e75e08c9214fe25b56535fc26f5435a875a137/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp#L2709C1-L2714C2)
 on them.   The assertion fails on the state `Pred` because it has never been 
set the `ObjCForHasMoreIterations` map. `Dest` has the map set.  This is what 
`populateObjCForDestinationSet` does.   (If assertions are disabled, there is a 
segmentation fault.) 




https://github.com/llvm/llvm-project/pull/124477
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to