================
@@ -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 think I finally understood this after comparing the exploded-graph
transitions.
Before the patch, the cast loses the alias with `m29`, so `l29` points to an
unrelated conjured region. Consequently, `memcpy` invalidates that region:
```diff
- SymRegion{conj_$6{...}} None 2 S8b
+ SymRegion{conj_$6{...}} 0 (Default) conj_$11{...}
```
Reads through `l29` therefore see fresh unknown contents, but the binding
`m29[j].s3[k] = 1` incorrectly survives. **After** the patch, `l29` correctly
aliases `m29[l]`: `&Element{Element{m29, l, struct mm}, 0, struct ll}`. The
`memcpy` invalidation now reaches the actual `m29` object. Because `l` is
symbolic, `RegionStore` cannot identify one concrete element and conservatively
invalidates the enclosing `m29` cluster:
```diff
- m29 None 1 S8b
+ m29 0 (Default) conj_$9{struct mm, ...}
```
The subsequent load no longer has a direct binding. Since its symbolic `j/k`
offset cannot be flattened, `RegionStore` returns `UnknownVal`.
Thus, the old `TRUE` came from a **stale binding** caused by lost aliasing. The
new `UNKNOWN` is sound but imprecise: the analyzer invalidates the destination
but does not model the concrete bytes copied by `memcpy`. **The gain** from the
patch is that writes through `l29` can no longer leave stale `m29` bindings
behind.
This is the example I used for analysis:
```c
typedef __typeof(sizeof(int)) size_t;
void *memcpy(void *, const void *, size_t);
void clang_analyzer_eval(int);
void clang_analyzer_dump(int);
void clang_analyzer_warnIfReached(void);
struct ll {
char s1[4];
char *s2;
};
struct mm {
char s3[4];
char *s4;
};
void f29(int j, int k, int l, int m) {
struct mm m29[2];
m29[j].s3[k] = 1;
struct ll *l29 = (struct ll *)&m29[l];
l29->s1[m] = 2;
char input[] = {'a', 'b', 'c', 'd'};
memcpy(l29->s1, input, 4);
if (j == l) {
clang_analyzer_warnIfReached();
clang_analyzer_eval(&m29[j] == &m29[l]);
clang_analyzer_dump(m29[j].s3[k]);
clang_analyzer_eval(m29[j].s3[k] == 1);
}
}
```
https://github.com/llvm/llvm-project/pull/221213
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
