[all-commits] [llvm/llvm-project] 792be5: [analyzer][solver] Fix CmpOpTable handling bug

Gabor Marton via All-commits all-commits at lists.llvm.org
Wed Oct 6 09:28:24 PDT 2021


  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 792be5df92e8d068ca32444383bc4e9e7f024bd8
      https://github.com/llvm/llvm-project/commit/792be5df92e8d068ca32444383bc4e9e7f024bd8
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2021-10-06 (Wed, 06 Oct 2021)

  Changed paths:
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    M clang/test/Analysis/constraint_manager_conditions.cpp

  Log Message:
  -----------
  [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




More information about the All-commits mailing list