[clang] [StaticAnalyzer] Fix state update in VisitObjCForCollectionStmt (PR #124477)

[Ziqing Luo via cfe-commits]

================
@@ -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