diff options
author | Gabor Marton <gabor.marton@ericsson.com> | 2021-09-30 23:26:22 +0200 |
---|---|---|
committer | Gabor Marton <gabor.marton@ericsson.com> | 2021-10-06 18:28:03 +0200 |
commit | 792be5df92e8d068ca32444383bc4e9e7f024bd8 (patch) | |
tree | 3017498977a251edd6710d2f2dc4b3cb3b5c3ba4 /llvm/lib/Analysis/BasicAliasAnalysis.cpp | |
parent | b2c906da19a74fe93baff7c52eafa02b6613b473 (diff) | |
download | llvm-792be5df92e8d068ca32444383bc4e9e7f024bd8.zip llvm-792be5df92e8d068ca32444383bc4e9e7f024bd8.tar.gz llvm-792be5df92e8d068ca32444383bc4e9e7f024bd8.tar.bz2 |
[analyzer][solver] Fix CmpOpTable handling bug
There is an error in the implementation of the logic of reaching the `Unknonw` tristate in CmpOpTable.
```
void cmp_op_table_unknownX2(int x, int y, int z) {
if (x >= y) {
// x >= y [1, 1]
if (x + z < y)
return;
// x + z < y [0, 0]
if (z != 0)
return;
// x < y [0, 0]
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
}
}
```
We miss the `FALSE` warning because the false branch is infeasible.
We have to exploit simplification to discover the bug. If we had `x < y`
as the second condition then the analyzer would return the parent state
on the false path and the new constraint would not be part of the State.
But adding `z` to the condition makes both paths feasible.
The root cause of the bug is that we reach the `Unknown` tristate
twice, but in both occasions we reach the same `Op` that is `>=` in the
test case. So, we reached `>=` twice, but we never reached `!=`, thus
querying the `Unknonw2x` column with `getCmpOpStateForUnknownX2` is
wrong.
The solution is to ensure that we reached both **different** `Op`s once.
Differential Revision: https://reviews.llvm.org/D110910
Diffstat (limited to 'llvm/lib/Analysis/BasicAliasAnalysis.cpp')
0 files changed, 0 insertions, 0 deletions