[PATCH] D78933: RangeConstraintManager optimizations in comparison expressions

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov created this revision.
ASDenysPetrov added reviewers: NoQ, baloghadamsoftware, steakhal, xazax.hun.
ASDenysPetrov added a project: clang.
Herald added subscribers: cfe-commits, martong, Charusso, rnkovacs.

I got an idea how to make RangeConstraintManager​ more sofisticated.
I want you speak out, share your vision about this idea.

The idea came to me as a thing which resolves this bug PR13426 <https://bugs.llvm.org/show_bug.cgi?id=13426>.
Let's consider the next snippet:

  int foo(int y, int x) {
      int x;
      if (y == z) {
          x = 0;
      }
      if (y != z) {
          x = 1;
      }
      return x;
  }

Obviously that `x` will be initialized, but CSA reports next:

  warning: Undefined or garbage value returned to caller
        [core.uninitialized.UndefReturn]
          return x;

It happenes because CSA does not take into account that `y == z` and `y != z` are just two **opposites**, as if it was:

  if (y == z) {
      x = 0;
  } else {
      x = 1;
  }

So my improvments is in handling case above and similar ones.
This patch covers next:

- Consider comparisons such as `x > y` and `y < x` as **reversed** copy and generates a //true// branch only. Applies to `< > <= >= == !=`.
- Consider comparisons such as `x > y` and `x < y`, `x <= y`, `x == y`,  `y > x`,  `y >= x`,  `y == x` as **opposites** and generates a //false// branch only. Applies to `< > <= >= == !=`.

As a result of processing an example below, we have F11810767: before.html <https://reviews.llvm.org/F11810767> and F11810762: after.html <https://reviews.llvm.org/F11810762> exploded graphs.

  void foo(int y, int x) {
      int z;
      if (x > y) {
          if (y > x) {
              z = 1;
          }
          if (y >= x) {
              z = 2;
          }
          if (y == x) {
              z = 3;
          }
      }
      else{
          if (y > x) {
              z = 1;
          }
          if (y >= x) {
              z = 2;
          }
          if (y == x) {
              z = 3;
          }
  }


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D78933

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/constraint_manager_conditions.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D78933.260302.patch
Type: text/x-patch
Size: 11594 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200427/919dc094/attachment-0001.bin>