[clang] [clang][analyzer] Preserve symbolic-offset regions across pointer casts (PR #221213)

[Radovan Božić via cfe-commits]

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