llvm-project/clang/test/Analysis/constraint_manager_conditions.cpp
Gabor Marton 792be5df92 [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
2021-10-06 18:28:03 +02:00

228 lines
12 KiB
C++

// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
void clang_analyzer_eval(int);
void comparison_lt(int x, int y) {
if (x < y) {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
}
}
void comparison_gt(int x, int y) {
if (x > y) {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
clang_analyzer_eval(x <= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
}
}
void comparison_le(int x, int y) {
if (x <= y) {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
clang_analyzer_eval(x <= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
}
}
void comparison_ge(int x, int y) {
if (x >= y) {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
}
}
void comparison_eq(int x, int y) {
if (x == y) {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
clang_analyzer_eval(x != y); // expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
}
}
void comparison_ne(int x, int y) {
if (x != y) {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
} else {
clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
clang_analyzer_eval(x != y); // expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
}
}
void comparison_le_ne(int x, int y) {
if (x <= y)
if (x != y) {
clang_analyzer_eval(x < y); // expected-warning{{TRUE}}
clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
clang_analyzer_eval(x >= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
}
}
void comparison_ge_ne(int x, int y) {
if (x >= y)
if (x != y) {
clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
clang_analyzer_eval(x <= y); // expected-warning{{FALSE}}
clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
}
}
void comparison_le_ge(int x, int y) {
if (x <= y)
if (x >= y) {
clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
clang_analyzer_eval(x != y); // expected-warning{{FALSE}}
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
}
}
// Test 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}}
}
}