[PATCH] D78933: RangeConstraintManager optimizations in comparison expressions

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov updated this revision to Diff 260331.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D78933/new/

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

Index: clang/test/Analysis/constraint_manager_conditions.cpp
===
--- /dev/null
+++ clang/test/Analysis/constraint_manager_conditions.cpp
@@ -0,0 +1,133 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+//reversed
+
+void comparison_reversed_gt(int x, int y) {
+  if (x > y)
+clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_ge(int x, int y) {
+  if (x >= y)
+clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_lt(int x, int y) {
+  if (x < y)
+clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_le(int x, int y) {
+  if (x <= y)
+clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_eq(int x, int y) {
+  if (x == y)
+clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_ne(int x, int y) {
+  if (x != y)
+clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
+}
+
+//opposite
+
+void comparison_opposite_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{{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}}
+  } else {
+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}}
+  }
+}
+
+void comparison_opposite_ge(int x, int y) {
+  if (x >= y) {
+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}}
+clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+  }
+}
+
+void comparison_opposite_lt(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{{FALSE}}
+clang_analyzer_eval(y == x); // 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{{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}}
+  }
+}
+
+void comparison_opposite_le(int x, int y) {
+  if (x <= y) {
+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}}
+clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
+  }
+}
+
+void comparison_opposite_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{{FALSE}}
+clang_analyzer_eval(y != x); // 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{{TRUE}}
+clang_analyzer_eval(y > x);  // expected-warning{{TRUE}}
+clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+

[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 
.
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 
 and F11810762: after.html 
 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

Index: clang/test/Analysis/constraint_manager_conditions.cpp
===
--- /dev/null
+++ clang/test/Analysis/constraint_manager_conditions.cpp
@@ -0,0 +1,109 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+//reversed
+
+void comparison_reversed_gt(int x, int y) {
+  if (x > y)
+clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_ge(int x, int y) {
+  if (x >= y)
+clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_lt(int x, int y) {
+  if (x < y)
+clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_le(int x, int y) {
+  if (x <= y)
+clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_eq(int x, int y) {
+  if (x == y)
+clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+}
+
+void comparison_reversed_ne(int x, int y) {
+  if (x != y)
+clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+  else
+clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
+}
+
+//opposite
+
+void comparison_opposite_gt(int x, int y) {
+  if (x > y) {
+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}}
+clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+  }
+}
+
+void comparison_opposite_ge(int x, int y) {
+  if (x >= y) {
+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}}
+clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+  }
+}
+
+void comparison_opposite_lt(int x, int y) {
+  if (x < y) {
+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}}
+clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+  }
+}
+
+void comparison_opposite_le(int x, int y) {
+  if (x <= y) {
+clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+