[PATCH] D158813: [analyzer] MPIChecker: MPI_Waitall should respect count arg

[Ding Fei via Phabricator via cfe-commits]

danix800 added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:192-198
+    SVal Count = CE.getArgSVal(0);
+    for (size_t i = 0; i < ArrSize; ++i) {
+      const NonLoc Idx = Ctx.getSValBuilder().makeArrayIndex(i);
+      auto CountReached = SVB.evalBinOp(State, BO_GE, Idx, Count, ASTCtx.BoolTy)
+                              .getAs<DefinedOrUnknownSVal>();
+      if (CountReached && State->assume(*CountReached, true))
+        break;
----------------
steakhal wrote:
> It's suspicious to me to compare stuff in the symbolic domain, such as `Idx >= Count` here.
> And let me elaborate on why I think so.
> 
> I'd assume that the first argument of `MPI_Waitall` is usually just a number literal, thus it's gonna be a ConcreteInt, so now we have `Count`.
> The `Index` you just created, obviously is just a ConcreteInt.
> After this, we could simply unwrap them and do the comparison without doing it in the symbolic domain.
> 
> ---
> 
> As a sidenote, `State->assume(*CountReached, true)` would return a state in two cases:
>  1) We can prove that the assumption holds.
>  2) We cannot disprove the assumption, thus it might hold, so we assume it holds.
> This is probably not what you wanted in the first place, but it's probably irrelelevant anyway.
I'll restrict this checker to handle `ConcreteInt` count only.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D158813