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

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

Let me try to summarize some of the variables:

So, given an invocation like `MPI_Waitall(C, Requests, Statues)`:

- `MR` is `lval(Requests)`
- `ElementCount` is the number of elements `Requests` consist of.
- `ArrSize` is basically `ElementCount` but an APSInt.
- `MROffset` is the offset and allocated region of the `Requests` region.
- `Index` is ConcreteInt(0, ..., ArrSize)
- `Count` is `C`, which is likely a ConcreteInt.

Please note that I have no idea what this checker does.



================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:46-48
+    if (!ErrorNode)
+      return;
+
----------------
If these hunks are not closely related to the issue you intend to fix in this PR, I'd suggesst submitting it separately. That is a common API, and we wouldn't need tests for such defensive checks, as they rarely trigger.


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:185-188
+    CharUnits ElemSizeInChars = ASTCtx.getTypeSizeInChars(ElemType);
+    int64_t ElemSizeInBits =
+        (ElemSizeInChars.isZero() ? 1 : ElemSizeInChars.getQuantity()) *
+        ASTCtx.getCharWidth();
----------------
How can `ElemSizeInChar` be zero?
If it can be zero, could you demonstrate it by a test?


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:189-190
+        ASTCtx.getCharWidth();
+    const NonLoc MROffset =
+        SVB.makeArrayIndex(MR->getAsOffset().getOffset() / ElemSizeInBits);
 
----------------
What implies that `MR->getAsOffset()` succeeds, and also what implies that the `Offset` within that is not symbolic?
Also, how can you use this without also using the result region?
Without using that you don't know what is the anchor point, from which this offset represent anything.
ATM I believe the code assumes that `MR->getRegion()` equals to `SuperRegion`, which might not be always the case.
This could materialize a problem when you construct the element region later.


================
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;
----------------
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.


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:195
+      const NonLoc Idx = Ctx.getSValBuilder().makeArrayIndex(i);
+      auto CountReached = SVB.evalBinOp(State, BO_GE, Idx, Count, ASTCtx.BoolTy)
+                              .getAs<DefinedOrUnknownSVal>();
----------------
In C for example, we might not have a Boot type AFAIK.
Usually, we use `SVB.getConditionType()` in such cases.


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:200-202
+      auto ElementRegionIndex =
+          SVB.evalBinOp(State, BO_Add, Idx, MROffset, SVB.getArrayIndexType())
+              .getAs<NonLoc>();
----------------
My guess is that we only care about if `MROffset` is a concrete int, thus we could also just do this assidion in regular c++ and just transfer the result into the symbolic domain. 


================
Comment at: clang/lib/StaticAnalyzer/Checkers/MPI-Checker/MPIChecker.cpp:205
+        const ElementRegion *const ER = RegionManager.getElementRegion(
+            ElemType, *ElementRegionIndex, SuperRegion, Ctx.getASTContext());
+        ReqRegions.push_back(ER);
----------------
I believe you have a variable `ASTCtx` that you could use.


================
Comment at: clang/test/Analysis/mpichecker-crash-gh64647.cpp:5-13
+bool contains();
+void do_a() {
+  if (contains()) {
+    MPI_Request request_item;
+    MPI_Wait(&request_item, MPI_STATUS_IGNORE);
+    // expected-warning at -1 {{Request 'request_item' has no matching nonblocking call.}}
+  }
----------------
Unless you have a compelling reason creating this file, I'd suggest to append this to the end of the `test/Analysis/mpichecker.cpp`, and just leave a comment there like `// GithHub Issue 64647`.

On a side note, do we need this to be recursive? Is this the minimal case to reproduce the issue?


================
Comment at: clang/test/Analysis/mpichecker.cpp:286-288
+  for (int i = 0; i < 3; ++i)
+    MPI_Ireduce(MPI_IN_PLACE, &buf, 1, MPI_DOUBLE, MPI_SUM, 0, MPI_COMM_WORLD,
+                &rs.req[i]);
----------------
This loop here implicitly depends on the fact that we only unroll loops 4 times.
I'd prefer a simpler test where we don't even have a loop.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D158813