================
@@ -627,7 +628,7 @@ int f29(int i, int j, int k, int l, int m) {
clang_analyzer_eval(m29[i].s3[1] == 1); // expected-warning{{UNKNOWN}}
clang_analyzer_eval(m29[i].s3[2] == 1); // expected-warning{{UNKNOWN}}
clang_analyzer_eval(m29[i].s3[3] == 1); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(m29[j].s3[k] == 1); // expected-warning{{TRUE}}
+ clang_analyzer_eval(m29[j].s3[k] == 1); // expected-warning{{UNKNOWN}}
----------------
bozicrHT wrote:
I got stuck on this example, so I did some analysis with Codex. These are the
findings:
Before the patch, the cast follows: `VisitCast → handleLValueBitCast() →
SValBuilder::evalCast() → StoreManager::castRegion():`
- `castRegion()` calls `ElementRegion::getAsArrayOffset()`. Because `l` is
symbolic, the offset cannot be flattened, so the cast becomes `UnknownVal`
([`Store.cpp:174`](https://github.com/llvm/llvm-project/blob/main/clang/lib/StaticAnalyzer/Core/Store.cpp#L174),
[`MemRegion.cpp:1514`](https://github.com/llvm/llvm-project/blob/main/clang/lib/StaticAnalyzer/Core/MemRegion.cpp#L1514)).
- `VisitDeclStmt()` then replaces this unknown initializer with a fresh
conjured pointer
([`ExprEngineC.cpp:600`](https://github.com/llvm/llvm-project/blob/main/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp#L600)).
Consequently, `l29` is no longer connected to `m29[l]`.
The write through `l29` and the subsequent `memcpy` therefore affect only this
unrelated conjured region. The existing binding `m29[j].s3[k] = 1` survives.
`getBindingForElement()` retrieves that `1`, the comparison is folded to `1 ==
1`, and `ExprInspectionChecker` reports `TRUE`.
The debug output confirms this. Before the patch:
```c
&m29[l] -> &Element{m29, l, struct mm}
(struct ll *)&m29[l] -> UNKNOWN
l29 -> &SymRegion{conj_...}
j == l branch -> REACHABLE
&m29[j] == &m29[l] -> TRUE
dump(m29[j].s3[k]) -> 1
m29[j].s3[k] == 1 -> TRUE // incorrect
```
With the patch:
```c
(struct ll *)&m29[l] -> &Element{Element{m29, l, struct mm}, 0, struct ll}
l29 -> &Element{Element{m29, l, struct mm}, 0, struct ll}
j == l branch -> REACHABLE
&m29[j] == &m29[l] -> TRUE
dump(m29[j].s3[k]) -> UNKNOWN
m29[j].s3[k] == 1 -> UNKNOWN
```
Why does it become `UNKNOWN` rather than `FALSE`?
The patch restores the alias relationship, but
`CStringChecker::evalCopyCommon()` does not model `memcpy` by copying the
concrete source bytes. It conservatively invalidates the destination instead
([`CStringChecker.cpp:1576`](https://github.com/llvm/llvm-project/blob/3c63fcb246f3bf5c2717ec6bd567a46cd65a4c25/clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp#L1576)).
Because the destination is now rooted at symbolic `m29[l]`, `RegionStore`
cannot identify one concrete element and invalidates the enclosing `m29` region
([`RegionStore.cpp:1343`](https://github.com/llvm/llvm-project/blob/3c63fcb246f3bf5c2717ec6bd567a46cd65a4c25/clang/lib/StaticAnalyzer/Core/RegionStore.cpp#L1343)).
This removes the binding to `1` and replaces it with a conjured default value
([`RegionStore.cpp:1223`](https://github.com/llvm/llvm-project/blob/3c63fcb246f3bf5c2717ec6bd567a46cd65a4c25/clang/lib/StaticAnalyzer/Core/RegionStore.cpp#L1223),
[`RegionStore.cpp:1386`](https://github.com/llvm/llvm-project/blob/3c63fcb246f3bf5c2717ec6bd567a46cd65a4c25/clang/lib/StaticAnalyzer/Core/RegionStore.cpp#L1386)).
Thus, inside the `j == l` branch, the analyzer knows that the addresses alias,
but it does not know what value `memcpy` wrote. The concrete result is `FALSE`,
while the analyzer reports the sound but imprecise result `UNKNOWN`.
https://github.com/llvm/llvm-project/pull/221213
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
