[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware added a comment. In https://reviews.llvm.org/D41938#1167639, @baloghadamsoftware wrote: > The flag is off by default. Except the rearrangement of additive operations. > Should we put it also behind the flag? I did it as a temporary quick fix: https://reviews.llvm.org/D49536. Repository: rL LLVM https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware added a comment. In https://reviews.llvm.org/D41938#1167313, @NoQ wrote: > There are still performance regressions coming in, and this time it doesn't > look like it's my fault: https://bugs.llvm.org/show_bug.cgi?id=38208 > > I suspect that this might be because we aren't enforcing complexity > thresholds over all the symbols we're constructing, but that's not certain, > we need to get to the bottom of it some day. > > I suggest reverting the patch or putting it behind an off-by-default flag > until we debug these cases. The flag is off by default. Except the rearrangement of additive operations. Should we put it also behind the flag? Repository: rL LLVM https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
NoQ added a comment. Herald added a subscriber: mikhail.ramalho. There are still performance regressions coming in, and this time it doesn't look like it's my fault: https://bugs.llvm.org/show_bug.cgi?id=38208 I suspect that this might be because we aren't enforcing complexity thresholds over all the symbols we're constructing, but that's not certain, we need to get to the bottom of it some day. I suggest reverting the patch or putting it behind an off-by-default flag until we debug these cases. Repository: rL LLVM https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
NoQ added a comment.
We've found a crash on our internal buildbot, would you like to have a look?:
**`$ cat repro.c`**
int foo(int x, int y) {
short a = x - 1U;
return a - y;
}
**`$ clang -cc1 -analyze -analyzer-checker=core repro.c`**
Assertion failed: (APSIntType(LInt) == BV.getAPSIntType(SymTy) && "Integers
are not of the same type as symbols!"), function doRearrangeUnchecked, file
/Users/adergachev/llvm/tools/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp,
line 383.
`1U` can be replaced with `1L` or `1UL`.
Repository:
rL LLVM
https://reviews.llvm.org/D41938
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
This revision was automatically updated to reflect the committed changes.
Closed by commit rL329780: [Analyzer] SValBuilder Comparison Rearrangement
(with Restrictions and Analyzer… (authored by baloghadamsoftware, committed by
).
Herald added a subscriber: llvm-commits.
Changed prior to commit:
https://reviews.llvm.org/D41938?vs=140061=141952#toc
Repository:
rL LLVM
https://reviews.llvm.org/D41938
Files:
cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
cfe/trunk/test/Analysis/conditional-path-notes.c
cfe/trunk/test/Analysis/explain-svals.cpp
cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
Index: cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
===
--- cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
+++ cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,931 @@
+// 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))
+
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+unsigned int __line, __const char *__function)
+ __attribute__ ((__noreturn__));
+#define assert(expr) \
+ ((expr) ? (void)(0) : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+
+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.
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -((int)INT_MAX / 4));
+ 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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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); //
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
george.karpenkov accepted this revision. george.karpenkov added a comment. LGTM. Sorry for the delay, I thought that a single acceptance was sufficient. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware marked an inline comment as done. baloghadamsoftware added a comment. George or Devin, please accept it or give me some feedback if not. Since this patch affects the core infrastructure I think it is wise to merge it only if at least two of you have accepted it. Artem is one, I need a second one as well. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware marked an inline comment as done. baloghadamsoftware added inline comments. Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:675-677 + /// 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. NoQ wrote: > I believe that we should mention that the integers are signed. Also the symbols were forgotten. They must be in the range as well and must also be signed integers. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware updated this revision to Diff 140061.
baloghadamsoftware marked an inline comment as done.
baloghadamsoftware added a comment.
Comment fixed.
https://reviews.llvm.org/D41938
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/conditional-path-notes.c
test/Analysis/explain-svals.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,931 @@
+// 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))
+
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+unsigned int __line, __const char *__function)
+ __attribute__ ((__noreturn__));
+#define assert(expr) \
+ ((expr) ? (void)(0) : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+
+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.
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -((int)INT_MAX / 4));
+ 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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_eval(x == y);
+ // expected-warning@-1{{TRUE}}
+}
+
+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_eval(x == y);
+ //
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.
This looks good with a super tiny nit regarding comments about signed integers.
George, are you happy with the changes? (:
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:675-677
+ /// 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.
I believe that we should mention that the integers are signed.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:330
+ nonloc::ConcreteInt(Max), SVB.getConditionType());
+ if (auto DV = IsCappedFromAbove.getAs()) {
+if (State->assume(*DV, false))
baloghadamsoftware wrote:
> george.karpenkov wrote:
> > 6 lines of branching is probably better expressed as
> >
> > ```
> > if (!isa(IsCappedFromAbove) ||
> > State->assume(*dyn_cast(IsCappedFromAbove), false))
> >return false
> > ```
> SVal is not a pointer, so isa<>() and dyn_cast<>() does not work here.
`.getAs<>()` would have been similar, but i'm not fond of double checks either.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:429
+ if (BinaryOperator::isComparisonOp(Op)) {
+// Prefer comparing to a non-negative number.
+// FIXME: Maybe it'd be better to have consistency in
george.karpenkov wrote:
> It seems that having a concrete positive RHS is a part of your rewrite rule.
> In that case, that should be documented in a high-level overview of the
> rewrite rules.
That's an invariant that we're maintaining in other places as well.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:774
+ if (Optional V = tryRearrange(state, op, lhs, rhs, resultTy))
+return *V;
george.karpenkov wrote:
> I would expect that checking the analyzer option would be performed here?
>
Nope, not yet. The flag is only for range-checked rearrangements.
https://reviews.llvm.org/D41938
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware marked 12 inline comments as done. baloghadamsoftware added inline comments. Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:326 + + llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4. + SVal IsCappedFromAbove = george.karpenkov wrote: > Would just division produce the same result? Also probably it's better to > make "4" a constant, at least with `#define` I changed it to division, but I am not sure if we a constant would be more readable here than 4. Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:337 + + llvm::APSInt Min = -Max; + SVal IsCappedFromBelow = george.karpenkov wrote: > 326-335 duplicates 338-346. > Perhaps we could have > > ``` > static bool isCappedFrom(bool Above, llvm::APSInt bound, ...) > ``` > > ? isInRelation(), because the opcode itself is passed instead of a bool. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware updated this revision to Diff 138954.
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/conditional-path-notes.c
test/Analysis/explain-svals.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,931 @@
+// 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))
+
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+unsigned int __line, __const char *__function)
+ __attribute__ ((__noreturn__));
+#define assert(expr) \
+ ((expr) ? (void)(0) : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+
+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.
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -((int)INT_MAX / 4));
+ 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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$9{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_$9{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_$9{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$9{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_eval(x == y);
+ // expected-warning@-1{{TRUE}}
+}
+
+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_eval(x == y);
+ // expected-warning@-1{{FALSE}}
+}
+
+void
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:330
+ nonloc::ConcreteInt(Max), SVB.getConditionType());
+ if (auto DV = IsCappedFromAbove.getAs()) {
+if (State->assume(*DV, false))
george.karpenkov wrote:
> 6 lines of branching is probably better expressed as
>
> ```
> if (!isa(IsCappedFromAbove) ||
> State->assume(*dyn_cast(IsCappedFromAbove), false))
>return false
> ```
SVal is not a pointer, so isa<>() and dyn_cast<>() does not work here.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:376
+ // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+ return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType()));
+}
george.karpenkov wrote:
> Is it beneficial to do this though? At the point where `decomposeSymbol` is
> called we are still checking whether the rearrangement could be performed, so
> maybe just returning a false flag would be better?
Failing to decompose a symbol does not mean the rearrangement could not be
performed. If we have just A on the left side instead of A+m or A-m, then we
regard it as A+0.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:432
+// "$x - $y" vs. "$y - $x" because those are solver's keys.
+if (LInt > RInt) {
+ ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
george.karpenkov wrote:
> I think this could be shortened and made more explicit by constructing the
> LHS and RHS first, and then reversing both and the comparison operator if RHS
> is negative.
Are you sure it would be shorter? Anyway, how to reverse a SymSymExpr?
https://reviews.llvm.org/D41938
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
NoQ added a comment.
George's style comments are usually super spot-on. Please feel free to improve
my code. Also it was only written as a proof-of-concept because i failed to
explain my approach with natural language, so it definitely needs polishing.
I'd let you know when i disagree with anything :)
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:472
+ if (BinaryOperator::isComparisonOp(Op) &&
+ Opts.shouldAggressivelySimplifyRelationalComparison()) {
+if (ResultTy != SVB.getConditionType())
george.karpenkov wrote:
> I am confused why the option `shouldAggressivelySimplifyRelationalComparison`
> is checked here. Do we rewrite cases where `Op` is additive even if the
> option is not checked? It's generally better to check the flag outside of the
> rearranging function, so that the high-level logic can be seen.
> Do we rewrite cases where `Op` is additive even if the option is not checked?
Yes. Because for additive ops the presumably-expensive clamped-by-max/4 check
is not necessary (and is indeed skipped below).
This should be documented though.
Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:19
+ if (x < -(((int)INT_MAX) / 4))
+exit(1);
+ return x;
george.karpenkov wrote:
> assert would express intent better
Yeah, but it's also a bit more painful to write in tests (i.e.
`__builtin_assert()` and macros).
Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:28
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
george.karpenkov wrote:
> Can we also have integration-like tests where rearrangement would affect
> observable behavior?
>
> Also, `clang_analyzer_dump` is a debugging function, and I am not sure
> whether we should rely on its output in tests.
Yeah, this test would be painful to maintain if we change the dump output. I
guess we definitely need more integration tests.
I still wish there were ways to write "this" sort of tests without relying on
dumps. Eg.:
```
clang_analyzer_denote(x, "$x");
clang_analyzer_denote(y, "$y");
clang_analyzer_express(x == y); // expected-warning{{($x - $y) == 0}}
```
It should be easy to make an `SValVisitor` that does that.
Given how painful this would be to actually update these numerous tests, i'm
fine with leaving a comment explaining the above, as a bit of technical debt -
for anyone who would need to update them in the future.
We still need more integration tests though.
Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:100
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
This one, for instance, is essentially an integration test. You can easily
replace the last dump with clang_analyzer_eval(x == y) and the test would still
test the same thing. All tests here that expect a concrete integer in the last
check should probably be just converted to clang_analyzer_eval tests.
https://reviews.llvm.org/D41938
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware added a comment. Thank you for your comments. Since the original author of this particular code is Artem, I think he will answer your questions. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
george.karpenkov added inline comments.
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:597
+ // than or equal to the quarter of the maximum value of that type.
+ bool shouldAggressivelySimplifyRelationalComparison();
+
High level comment: can you list all [[ https://en.wikipedia.org/wiki/Rewriting
| rewriting ]] rules you are applying in a formula explicitly in a comment?
From the phabricator discussion I see that you are applying
```
A + n >= B + m -> A - B >= n + m // A, B symbolic, n and m are integers
```
but from the code it seems that you are applying more canonicalization rules?
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:317
+// with simpler symbols on every recursive call.
+static bool isOverflowClampedBy4(SymbolRef Sym, ProgramStateRef State) {
+ SValBuilder = State->getStateManager().getSValBuilder();
Can we have a better function name here? I can't think of one straight away,
but "clamped" is not very self-descriptive. `isWithinConstantOverflowBounds`?
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:326
+
+ llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4.
+ SVal IsCappedFromAbove =
Would just division produce the same result? Also probably it's better to make
"4" a constant, at least with `#define`
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:330
+ nonloc::ConcreteInt(Max), SVB.getConditionType());
+ if (auto DV = IsCappedFromAbove.getAs()) {
+if (State->assume(*DV, false))
6 lines of branching is probably better expressed as
```
if (!isa(IsCappedFromAbove) ||
State->assume(*dyn_cast(IsCappedFromAbove), false))
return false
```
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:337
+
+ llvm::APSInt Min = -Max;
+ SVal IsCappedFromBelow =
326-335 duplicates 338-346.
Perhaps we could have
```
static bool isCappedFrom(bool Above, llvm::APSInt bound, ...)
```
?
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:352
+// Same for the concrete integers: see if I is within [min/4, max/4].
+static bool isOverflowClampedBy4(llvm::APSInt I) {
+ APSIntType AT(I);
Again, could we do better with a function name?
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:357
+
+ llvm::APSInt Max = AT.getMaxValue() >> 2;
+ if (I > Max)
I think you want
```
return (I <= Max) && (I >= -Max)
```
instead of 358-365
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:376
+ // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+ return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType()));
+}
Is it beneficial to do this though? At the point where `decomposeSymbol` is
called we are still checking whether the rearrangement could be performed, so
maybe just returning a false flag would be better?
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:403
+ if (LOp == BO_Sub)
+LInt = -LInt;
+ else
I think this is a separate rewrite, which is better performed in a separate
function.
If you move it to `decomposeSymbol` or to a separate function, you would get a
lot of simplifications:
1. This function would be performing only a single rewrite.
2. You would no longer need to take `Lop` and `Rop` as parameters
3. At that point, two separate cases would be clearly seen: `Op` is a
comparison operator, or `Op` is an additive operator.
I would separate those two rewrites in separate functions, distinguishing
between them at the callsite.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:429
+ if (BinaryOperator::isComparisonOp(Op)) {
+// Prefer comparing to a non-negative number.
+// FIXME: Maybe it'd be better to have consistency in
It seems that having a concrete positive RHS is a part of your rewrite rule. In
that case, that should be documented in a high-level overview of the rewrite
rules.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:432
+// "$x - $y" vs. "$y - $x" because those are solver's keys.
+if (LInt > RInt) {
+ ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
I think this could be shortened and made more explicit by constructing the LHS
and RHS first, and then reversing both and the comparison operator if RHS is
negative.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:472
+ if (BinaryOperator::isComparisonOp(Op) &&
+ Opts.shouldAggressivelySimplifyRelationalComparison()) {
+if (ResultTy != SVB.getConditionType())
I am confused why the option `shouldAggressivelySimplifyRelationalComparison`
is checked here. Do we rewrite cases where `Op` is
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
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
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
NoQ added a comment. I think it'd be fine to do the rearrangement for additive ops without the option check, as we discussed. I.e., rearrange when it's either an additive op, or both the flag is set and the values are overflow-clamped. And remove the clamp checks (which are presumably heavy) for the additive ops, as they're not needed. Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:591-596 + /// Returns true if SValBuilder should rearrange comparisons of symbolic + /// expressions which consists of the sum of a symbol and a concrete integer + /// into a format where symbols are on the left side and the integer on the + /// right. This is only done if both concrete integers are greter or equal to + /// the quarter of the minimum value of the type and less or equal to the + /// quarter of the maximum. Fixed some typos: ``` /// 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. ``` (line breaks might need fixing) Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:5 +void clang_analyzer_eval(int x); +void clang_analyzer_printState(); + I guess you're not going to need the printState thing once these tests are settled down. https://reviews.llvm.org/D41938 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
baloghadamsoftware created this revision.
baloghadamsoftware added reviewers: NoQ, dcoughlin.
Herald added subscribers: a.sidorin, szepet.
This patch is a "light" version of https://reviews.llvm.org/D35109:
Since the range-based constraint manager (default) is weak in handling
comparisons where symbols are on both sides it is wise to rearrange them to
have symbols only on the left side. Thus e.g. `A + n >= B + m` becomes `A - B
>= m - n` which enables the constraint manager to store a range `m - n ..
MAX_VALUE` for the symbolic expression `A - B`. This can be used later to check
whether e.g. `A + k == B + l` can be true, which is also rearranged to `A - B
== l - k` so the constraint manager can check whether `l - k` is in the range
(thus greater than or equal to `m - n`).
The restriction in this version is the the rearrangement happens only if the
concrete integers are within the range `[min/4 .. max/4]` where `min` and `max`
are the minimal and maximal values of their type.
The rearrangement is not enabled by default. It has to be enabled by using
`-analyzer-config aggressive-relational-comparison-simplification=true`.
Co-author of this patch is Artem Dergachev (NoQ).
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,928 @@
+// 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 clang_analyzer_printState();
+
+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;
+
