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@-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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
