baloghadamsoftware updated this revision to Diff 130403.
baloghadamsoftware added a comment.
Updated according to the comments.
https://reviews.llvm.org/D41938
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/svalbuilder-rearrange-comparisons.c
Index: test/Analysis/svalbuilder-rearrange-comparisons.c
===================================================================
--- /dev/null
+++ test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,927 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_dump(int x);
+void clang_analyzer_eval(int x);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+int g();
+int f() {
+ int x = g();
+ // Assert that no overflows occur in this test file.
+ // Assuming that concrete integers are also within that range.
+ if (x > ((int)INT_MAX / 4))
+ exit(1);
+ if (x < -(((int)INT_MAX) / 4))
+ exit(1);
+ return x;
+}
+
+void compare_different_symbol_equal() {
+ int x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal() {
+ int x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal() {
+ int x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal() {
+ int x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal() {
+ int x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal() {
+ int x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal() {
+ int x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal() {
+ int x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal() {
+ int x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol_equal() {
+ int x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_equal() {
+ int x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_equal() {
+ int x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_equal() {
+ int x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_equal() {
+ int x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal() {
+ int x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal() {
+ int x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal() {
+ int x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal() {
+ int x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_or_equal() {
+ int x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal() {
+ int x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal() {
+ int x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal() {
+ int x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal() {
+ int x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal() {
+ int x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal() {
+ int x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal() {
+ int x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal() {
+ int x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal() {
+ int x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal() {
+ int x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal() {
+ int x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal() {
+ int x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal() {
+ int x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal() {
+ int x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal() {
+ int x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal() {
+ int x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal() {
+ int x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less() {
+ int x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less() {
+ int x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less() {
+ int x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less() {
+ int x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less() {
+ int x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less() {
+ int x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less() {
+ int x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less() {
+ int x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less() {
+ int x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_same_symbol_less() {
+ int x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less() {
+ int x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_less() {
+ int x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_less() {
+ int x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_less() {
+ int x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less() {
+ int x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less() {
+ int x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less() {
+ int x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less() {
+ int x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_different_symbol_equal_unsigned() {
+ unsigned x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal_unsigned() {
+ unsigned x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal_unsigned() {
+ unsigned x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal_unsigned() {
+ unsigned x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal_unsigned() {
+ unsigned x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() {
+ unsigned x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() {
+ unsigned x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() {
+ unsigned x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() {
+ unsigned x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol_equal_unsigned() {
+ unsigned x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_equal_unsigned() {
+ unsigned x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_equal_unsigned() {
+ unsigned x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_or_equal_unsigned() {
+ unsigned x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal_unsigned() {
+ unsigned x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal_unsigned() {
+ unsigned x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal_unsigned() {
+ unsigned x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+ unsigned x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x <= y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_unsigned() {
+ unsigned x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_unsigned() {
+ unsigned x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_unsigned() {
+ unsigned x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_unsigned() {
+ unsigned x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_unsigned() {
+ unsigned x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_unsigned() {
+ unsigned x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_unsigned() {
+ unsigned x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_unsigned() {
+ unsigned x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_unsigned() {
+ unsigned x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_same_symbol_less_unsigned() {
+ unsigned x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_unsigned() {
+ unsigned x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_unsigned() {
+ unsigned x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_unsigned() {
+ unsigned x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_unsigned() {
+ unsigned x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_unsigned() {
+ unsigned x = f(), y = x+1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_unsigned() {
+ unsigned x = f(), y = x-1;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_unsigned() {
+ unsigned x = f(), y = x+1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_unsigned() {
+ unsigned x = f(), y = x-1;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x < y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void overflow(signed char n, signed char m) {
+ if (n + 0 > m + 0) {
+ clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}}
+ }
+}
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -12,8 +12,10 @@
//===----------------------------------------------------------------------===//
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
using namespace clang;
@@ -307,6 +309,216 @@
return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
}
+// See if Sym is known to be within [min/4, max/4], where min and max
+// are the bounds of the symbol's integral type. With such symbols,
+// some manipulations can be performed without the risk of overflow.
+// assume() doesn't cause infinite recursion because we should be dealing
+// with simpler symbols on every recursive call.
+static bool isOverflowClampedBy4(SymbolRef Sym, ProgramStateRef State) {
+ SValBuilder &SVB = State->getStateManager().getSValBuilder();
+ BasicValueFactory &BV = SVB.getBasicValueFactory();
+
+ QualType T = Sym->getType();
+ assert(T->isSignedIntegerOrEnumerationType() &&
+ "This only works with signed integers!");
+ APSIntType AT = BV.getAPSIntType(T);
+
+ llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4.
+ SVal IsCappedFromAbove =
+ SVB.evalBinOpNN(State, BO_LE, nonloc::SymbolVal(Sym),
+ nonloc::ConcreteInt(Max), SVB.getConditionType());
+ if (auto DV = IsCappedFromAbove.getAs<DefinedSVal>()) {
+ if (State->assume(*DV, false))
+ return false;
+ } else {
+ return false;
+ }
+
+ llvm::APSInt Min = -Max;
+ SVal IsCappedFromBelow =
+ SVB.evalBinOpNN(State, BO_GE, nonloc::SymbolVal(Sym),
+ nonloc::ConcreteInt(Min), SVB.getConditionType());
+ if (auto DV = IsCappedFromBelow.getAs<DefinedSVal>()) {
+ if (State->assume(*DV, false))
+ return false;
+ } else {
+ return false;
+ }
+
+ return true;
+}
+
+// Same for the concrete integers: see if I is within [min/4, max/4].
+static bool isOverflowClampedBy4(llvm::APSInt I) {
+ APSIntType AT(I);
+ assert(!AT.isUnsigned() &&
+ "This only works with signed integers!");
+
+ llvm::APSInt Max = AT.getMaxValue() >> 2;
+ if (I > Max)
+ return false;
+
+ llvm::APSInt Min = -Max;
+ if (I < Min)
+ return false;
+
+ return true;
+}
+
+std::tuple<SymbolRef, BinaryOperator::Opcode, llvm::APSInt>
+decomposeSymbol(SymbolRef Sym, BasicValueFactory &BV) {
+ if (const auto *SymInt = dyn_cast<SymIntExpr>(Sym))
+ if (BinaryOperator::isAdditiveOp(SymInt->getOpcode()))
+ return std::make_tuple(SymInt->getLHS(), SymInt->getOpcode(),
+ SymInt->getRHS());
+
+ // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+ return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType()));
+}
+
+// Simplify "(LSym LOp LInt) Op (RSym ROp RInt)" assuming all values are of the
+// same signed integral type and no overflows occur (which should be checked
+// by the caller).
+static NonLoc doRearrangeUnchecked(ProgramStateRef State,
+ BinaryOperator::Opcode Op,
+ SymbolRef LSym, BinaryOperator::Opcode LOp,
+ llvm::APSInt LInt,
+ SymbolRef RSym, BinaryOperator::Opcode ROp,
+ llvm::APSInt RInt) {
+ SValBuilder &SVB = State->getStateManager().getSValBuilder();
+ BasicValueFactory &BV = SVB.getBasicValueFactory();
+ SymbolManager &SymMgr = SVB.getSymbolManager();
+
+ QualType SymTy = LSym->getType();
+ assert(SymTy == RSym->getType() &&
+ "Symbols are not of the same type!");
+ assert(APSIntType(LInt) == BV.getAPSIntType(SymTy) &&
+ "Integers are not of the same type as symbols!");
+ assert(APSIntType(RInt) == BV.getAPSIntType(SymTy) &&
+ "Integers are not of the same type as symbols!");
+
+ // Change "$x - a" into "$x + (-a)". We'd bring back this cosmetic difference
+ // after we're done with our operations.
+ if (LOp == BO_Sub)
+ LInt = -LInt;
+ else
+ assert(LOp == BO_Add && "Unexpected operation!");
+ if (ROp == BO_Sub)
+ RInt = -RInt;
+ else
+ assert(ROp == BO_Add && "Unexpected operation!");
+
+ QualType ResultTy;
+ if (BinaryOperator::isComparisonOp(Op))
+ ResultTy = SVB.getConditionType();
+ else if (BinaryOperator::isAdditiveOp(Op))
+ ResultTy = SymTy;
+ else
+ llvm_unreachable("Operation not suitable for unchecked rearrangement!");
+
+ // FIXME: Can we use assume() without getting into an infinite recursion?
+ if (LSym == RSym)
+ return SVB.evalBinOpNN(State, Op, nonloc::ConcreteInt(LInt),
+ nonloc::ConcreteInt(RInt), ResultTy)
+ .castAs<NonLoc>();
+
+ SymbolRef ResultSym = nullptr;
+ BinaryOperator::Opcode ResultOp;
+ llvm::APSInt ResultInt;
+ if (BinaryOperator::isComparisonOp(Op)) {
+ // Prefer comparing to a non-negative number.
+ // FIXME: Maybe it'd be better to have consistency in
+ // "$x - $y" vs. "$y - $x" because those are solver's keys.
+ if (LInt > RInt) {
+ ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
+ ResultOp = BinaryOperator::reverseComparisonOp(Op);
+ ResultInt = LInt - RInt; // Opposite order!
+ } else {
+ ResultSym = SymMgr.getSymSymExpr(LSym, BO_Sub, RSym, SymTy);
+ ResultOp = Op;
+ ResultInt = RInt - LInt; // Opposite order!
+ }
+ } else {
+ ResultSym = SymMgr.getSymSymExpr(LSym, Op, RSym, SymTy);
+ ResultInt = (Op == BO_Add) ? (LInt + RInt) : (LInt - RInt);
+ ResultOp = BO_Add;
+ // Bring back the cosmetic difference.
+ if (ResultInt < 0) {
+ ResultInt = -ResultInt;
+ ResultOp = BO_Sub;
+ } else if (ResultInt == 0) {
+ // Shortcut: Simplify "$x + 0" to "$x".
+ return nonloc::SymbolVal(ResultSym);
+ }
+ }
+ const llvm::APSInt &PersistentResultInt = BV.getValue(ResultInt);
+ return nonloc::SymbolVal(
+ SymMgr.getSymIntExpr(ResultSym, ResultOp, PersistentResultInt, ResultTy));
+}
+
+static Optional<NonLoc> tryRearrange(ProgramStateRef State,
+ BinaryOperator::Opcode Op, NonLoc Lhs,
+ NonLoc Rhs, QualType ResultTy) {
+ ProgramStateManager &StateMgr = State->getStateManager();
+ SValBuilder &SVB = StateMgr.getSValBuilder();
+
+ // We expect everything to be of the same type - this type.
+ QualType SingleTy;
+
+ auto &Opts =
+ StateMgr.getOwningEngine()->getAnalysisManager().getAnalyzerOptions();
+
+ if (BinaryOperator::isComparisonOp(Op) &&
+ Opts.shouldAggressivelySimplifyRelationalComparison()) {
+ if (ResultTy != SVB.getConditionType())
+ return None;
+ // Initialize SingleTy later with a symbol's type.
+ } else if (BinaryOperator::isAdditiveOp(Op)) {
+ SingleTy = ResultTy;
+ } else {
+ // Don't rearrange other operations.
+ return None;
+ }
+
+ SymbolRef LSym = Lhs.getAsSymbol();
+ if (!LSym)
+ return None;
+
+ if (BinaryOperator::isAdditiveOp(Op)) {
+ if (SingleTy != ResultTy)
+ return None;
+ } else {
+ SingleTy = LSym->getType();
+ }
+
+ assert(!SingleTy.isNull() && "We should have figured out the type by now!");
+
+ // Substracting unsigned integers is a nightmare.
+ if (!SingleTy->isSignedIntegerOrEnumerationType())
+ return None;
+
+ SymbolRef RSym = Rhs.getAsSymbol();
+ if (!RSym || RSym->getType() != SingleTy)
+ return None;
+
+ BasicValueFactory &BV = State->getBasicVals();
+ llvm::APSInt LInt, RInt;
+ BinaryOperator::Opcode LOp, ROp;
+ std::tie(LSym, LOp, LInt) = decomposeSymbol(LSym, BV);
+ if (LSym->getType() != SingleTy ||
+ !isOverflowClampedBy4(LSym, State) || !isOverflowClampedBy4(LInt))
+ return None;
+
+ std::tie(RSym, ROp, RInt) = decomposeSymbol(RSym, BV);
+ if (RSym->getType() != SingleTy ||
+ (BinaryOperator::isComparisonOp(Op) &&
+ (!isOverflowClampedBy4(RSym, State) || !isOverflowClampedBy4(RInt))))
+ return None;
+
+ // We know that no overflows can occur anymore.
+ return doRearrangeUnchecked(State, Op, LSym, LOp, LInt, RSym, ROp, RInt);
+}
+
SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
BinaryOperator::Opcode op,
NonLoc lhs, NonLoc rhs,
@@ -559,6 +771,9 @@
if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
+ if (Optional<NonLoc> V = tryRearrange(state, op, lhs, rhs, resultTy))
+ return *V;
+
// Give up -- this is not a symbolic expression we can handle.
return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
}
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -392,3 +392,11 @@
getBooleanOption("notes-as-events", /*Default=*/false);
return DisplayNotesAsEvents.getValue();
}
+
+bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {
+ if (!AggressiveRelationalComparisonSimplification.hasValue())
+ AggressiveRelationalComparisonSimplification =
+ getBooleanOption("aggressive-relational-comparison-simplification",
+ /*Default=*/false);
+ return AggressiveRelationalComparisonSimplification.getValue();
+}
Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -284,6 +284,9 @@
/// \sa shouldDisplayNotesAsEvents
Optional<bool> DisplayNotesAsEvents;
+ /// \sa shouldAggressivelySimplifyRelationalComparison
+ Optional<bool> AggressiveRelationalComparisonSimplification;
+
/// A helper function that retrieves option for a given full-qualified
/// checker name.
/// Options for checkers can be specified via 'analyzer-config' command-line
@@ -585,6 +588,14 @@
/// to false when unset.
bool shouldDisplayNotesAsEvents();
+ /// Returns true if SValBuilder should rearrange comparisons of symbolic
+ /// expressions which consist of a sum of a symbol and a concrete integer
+ /// into the format where symbols are on the left-hand side and the integer
+ /// is on the right. This is only done if both concrete integers are greater
+ /// than or equal to the quarter of the minimum value of the type and less
+ // than or equal to the quarter of the maximum value of that type.
+ bool shouldAggressivelySimplifyRelationalComparison();
+
public:
AnalyzerOptions() :
AnalysisStoreOpt(RegionStoreModel),
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
