baloghadamsoftware updated this revision to Diff 159012.
baloghadamsoftware edited the summary of this revision.
baloghadamsoftware added a comment.
Completely rewritten: works correctly for modular arithmetic (multiplication),
works correctly for truncation (division), only uses integers, no floats.
https://reviews.llvm.org/D49074
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
test/Analysis/multiplicative-folding.c
Index: test/Analysis/multiplicative-folding.c
===================================================================
--- test/Analysis/multiplicative-folding.c
+++ test/Analysis/multiplicative-folding.c
@@ -467,6 +467,1442 @@
}
}
+void signed_multiplication_lt_0(int32_t n) {
+ if (n * 2 < 3) {
+ int32_t U1 = 0x80000001,
+ L2 = 0xc0000000, U2 = 1,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 < 3);
+ assert(U1 * 2 < 3);
+ assert((U1 + 1) * 2 >= 3);
+ assert(L2 * 2 < 3);
+ assert((L2 - 1) * 2 >= 3);
+ assert(U2 * 2 < 3);
+ assert((U2 + 1) * 2 >= 3);
+ assert(L3 * 2 < 3);
+ assert((L3 - 1) * 2 >= 3);
+ assert(INT_MAX * 2 < 3);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2){
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_lt_1(int32_t n) {
+ if (n * 2 < 4) {
+ int32_t U1 = 0x80000001,
+ L2 = 0xc0000000, U2 = 1,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 < 4);
+ assert(U1 * 2 < 4);
+ assert((U1 + 1) * 2 >= 4);
+ assert(L2 * 2 < 4);
+ assert((L2 - 1) * 2 >= 4);
+ assert(U2 * 2 < 4);
+ assert((U2 + 1) * 2 >= 4);
+ assert(L3 * 2 < 4);
+ assert((L3 - 1) * 2 >= 4);
+ assert(INT_MAX * 2 < 4);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2){
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_lt_2(int32_t n) {
+ if (n * 2 < 5) {
+ int32_t U1 = 0x80000002,
+ L2 = 0xc0000000, U2 = 2,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 < 5);
+ assert(U1 * 2 < 5);
+ assert((U1 + 1) * 2 >= 5);
+ assert(L2 * 2 < 5);
+ assert((L2 - 1) * 2 >= 5);
+ assert(U2 * 2 < 5);
+ assert((U2 + 1) * 2 >= 5);
+ assert(L3 * 2 < 5);
+ assert((L3 - 1) * 2 >= 5);
+ assert(INT_MAX * 2 < 5);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2){
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_lt_3(int32_t n) {
+ if (n * 3 < 4) {
+ int32_t U1 = 0xaaaaaaab,
+ L2 = 0xd5555556, U2 = 1,
+ L3 = 0x2aaaaaab, U3 = 0x55555556;
+
+ assert(INT_MIN * 3 < 4);
+ assert(U1 * 3 < 4);
+ assert((U1 + 1) * 3 >= 4);
+ assert(L2 * 3 < 4);
+ assert((L2 - 1) * 3 >= 4);
+ assert(U2 * 3 < 4);
+ assert((U2 + 1) * 3 >= 4);
+ assert(L3 * 3 < 4);
+ assert((L3 - 1) * 3 >= 4);
+ assert(U3 * 3 < 4);
+ assert((U3 + 1) * 3 >= 4);
+
+ if (n < (int32_t) 0xc0000000) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x15555556) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_lt_4(int32_t n) {
+ if (n * 6 < -2) {
+ int32_t L1 = 0x95555556, U1 = 0xaaaaaaaa,
+ L2 = 0xc0000000, U2 = 0x55555554,
+ L3 = 0xeaaaaaab, U3 = -1,
+ L4 = 0x15555556, U4 = 0x2aaaaaaa,
+ L5 = 0x40000000, U5 = 0x55555554,
+ L6 = 0x6aaaaaab;
+
+ assert(L1 * 6 < -2);
+ assert((L1 - 1) * 6 >= -2);
+ assert(U1 * 6 < -2);
+ assert((U1 + 1) * 6 >= -2);
+ assert(L2 * 6 < -2);
+ assert((L2 - 1) * 6 >= -2);
+ assert(U2 * 6 < -2);
+ assert((U2 + 1) * 6 >= -2);
+ assert(L3 * 6 < -2);
+ assert((L3 - 1) * 6 >= -2);
+ assert(U3 * 6 < -2);
+ assert((U3 + 1) * 6 >= -2);
+ assert(L4 * 6 < -2);
+ assert((L4 - 1) * 6 >= -2);
+ assert(U4 * 6 < -2);
+ assert((U4 + 1) * 6 >= -2);
+ assert(L5 * 6 < -2);
+ assert((L5 - 1) * 6 >= -2);
+ assert(U5 * 6 < -2);
+ assert((U5 + 1) * 6 >= -2);
+ assert(L6 * 6 < -2);
+ assert((L6 - 1) * 6 >= -2);
+ assert(INT_MAX * 6 < -2);
+
+ if (n < (int32_t) 0xb5555555) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xdfffffff) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x0aaaaaaa) {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x35555555) {
+ clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x5fffffff) {
+ clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_division_lt_0(int32_t n) {
+ if (n / 4 < 0) {
+ const int32_t C = -4;
+
+ assert(C / 4 < 0);
+ assert((C + 1) / 4 >= 0);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_lt_1(int32_t n) {
+ if (n / 3 < 2) {
+ const int32_t C = 5;
+
+ assert(C / 3 < 2);
+ assert((C + 1) / 3 >= 2);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_lt_2(int32_t n) {
+ if (n / 5 < -7) {
+ const int32_t C = -40;
+
+ assert(C / 5 < -7);
+ assert((C + 1) / 5 >= -7);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_multiplication_lt_0(uint32_t n) {
+ if (n * 2 < 3) {
+ uint32_t U1 = 1,
+ L2 = 0x80000000, U2 = 0x80000001;
+
+ assert(U1 * 2 < 3);
+ assert((U1 + 1) * 2 >= 3);
+ assert(L2 * 2 < 3);
+ assert((L2 - 1) * 2 >= 3);
+ assert(U2 * 2 < 3);
+ assert((U2 + 1) * 2 >= 3);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_lt_1(uint32_t n) {
+ if (n * 2 < 4) {
+ uint32_t U1 = 1,
+ L2 = 0x80000000, U2 = 0x80000001;
+
+ assert(U1 * 2 < 4);
+ assert((U1 + 1) * 2 >= 4);
+ assert(L2 * 2 < 4);
+ assert((L2 - 1) * 2 >= 4);
+ assert(U2 * 2 < 4);
+ assert((U2 + 1) * 2 >= 4);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_lt_2(uint32_t n) {
+ if (n * 2 < 5) {
+ uint32_t U1 = 2,
+ L2 = 0x80000000, U2 = 0x80000002;
+
+ assert(U1 * 2 < 5);
+ assert((U1 + 1) * 2 >= 5);
+ assert(L2 * 2 < 5);
+ assert((L2 - 1) * 2 >= 5);
+ assert(U2 * 2 < 5);
+ assert((U2 + 1) * 2 >= 5);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_lt_3(uint32_t n) {
+ if (n * 3 < 4) {
+ uint32_t U1 = 1, C2 = 0x55555556, C3 = 0xaaaaaaab;
+
+ assert(U1 * 3 < 4);
+ assert((U1 + 1) * 3 >= 4);
+ assert(C2 * 3 < 4);
+ assert((C2 - 1) * 3 >= 4);
+ assert((C2 + 1) * 3 >= 4);
+ assert(C3 * 3 < 4);
+ assert((C3 - 1) * 3 >= 4);
+ assert((C3 + 1) * 3 >= 4);
+
+ if (n < 0x2aaaaaab) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < 0x80000000) {
+ clang_analyzer_eval(n < C2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n == C2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < C3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n == C3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C3); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_division_lt_0(uint32_t n) {
+ if (n / 3 < 2) {
+ const uint32_t C = 5;
+
+ assert(C / 3 < 2);
+ assert((C + 1) / 3 >= 2);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_multiplication_le_0(int32_t n) {
+ if (n * 2 <= 3) {
+ int32_t U1 = 0x80000001,
+ L2 = 0xc0000000, U2 = 1,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 <= 3);
+ assert(U1 * 2 <= 3);
+ assert((U1 + 1) * 2 > 3);
+ assert(L2 * 2 <= 3);
+ assert((L2 - 1) * 2 > 3);
+ assert(U2 * 2 <= 3);
+ assert((U2 + 1) * 2 > 3);
+ assert(L3 * 2 <= 3);
+ assert((L3 - 1) * 2 > 3);
+ assert(INT_MAX * 2 <= 3);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_le_1(int32_t n) {
+ if (n * 2 <= 4) {
+ int32_t U1 = 0x80000002,
+ L2 = 0xc0000000, U2 = 2,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 <= 4);
+ assert(U1 * 2 <= 4);
+ assert((U1 + 1) * 2 > 4);
+ assert(L2 * 2 <= 4);
+ assert((L2 - 1) * 2 > 4);
+ assert(U2 * 2 <= 4);
+ assert((U2 + 1) * 2 > 4);
+ assert(L3 * 2 <= 4);
+ assert((L3 - 1) * 2 > 4);
+ assert(INT_MAX * 2 <= 4);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2){
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_le_2(int32_t n) {
+ if (n * 2 <= 5) {
+ int32_t U1 = 0x80000002,
+ L2 = 0xc0000000, U2 = 2,
+ L3 = 0x40000000;
+
+ assert(INT_MIN * 2 <= 5);
+ assert(U1 * 2 <= 5);
+ assert((U1 + 1) * 2 > 5);
+ assert(L2 * 2 <= 5);
+ assert((L2 - 1) * 2 > 5);
+ assert(U2 * 2 <= 5);
+ assert((U2 + 1) * 2 > 5);
+ assert(L3 * 2 <= 5);
+ assert((L3 - 1) * 2 > 5);
+ assert(INT_MAX * 2 <= 5);
+
+ if (n < INT_MIN / 2) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_le_3(int32_t n) {
+ if (n * 3 <= 4) {
+ int32_t U1 = 0xaaaaaaac,
+ L2 = 0xd5555556, U2 = 1,
+ L3 = 0x2aaaaaab, U3 = 0x55555556;
+
+ assert(INT_MIN * 3 <= 4);
+ assert(U1 * 3 <= 4);
+ assert((U1 + 1) * 3 > 4);
+ assert(L2 * 3 <= 4);
+ assert((L2 - 1) * 3 > 4);
+ assert(U2 * 3 <= 4);
+ assert((U2 + 1) * 3 > 4);
+ assert(L3 * 3 <= 4);
+ assert((L3 - 1) * 3 > 4);
+ assert(U3 * 3 <= 4);
+ assert((U3 + 1) * 3 > 4);
+
+ if (n < (int32_t) 0xc0000001) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x15555556) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_le_4(int32_t n) {
+ if (n * 6 <= -2) {
+ int32_t L1 = 0x95555556, U1 = 0xaaaaaaaa,
+ L2 = 0xc0000000, U2 = 0x55555555,
+ L3 = 0xeaaaaaab, U3 = -1,
+ L4 = 0x15555556, U4 = 0x2aaaaaaa,
+ L5 = 0x40000000, U5 = 0x55555555,
+ L6 = 0x6aaaaaab;
+
+ assert(L1 * 6 <= -2);
+ assert((L1 - 1) * 6 > -2);
+ assert(U1 * 6 <= -2);
+ assert((U1 + 1) * 6 > -2);
+ assert(L2 * 6 <= -2);
+ assert((L2 - 1) * 6 > -2);
+ assert(U2 * 6 <= -2);
+ assert((U2 + 1) * 6 > -2);
+ assert(L3 * 6 <= -2);
+ assert((L3 - 1) * 6 > -2);
+ assert(U3 * 6 <= -2);
+ assert((U3 + 1) * 6 > -2);
+ assert(L4 * 6 <= -2);
+ assert((L4 - 1) * 6 > -2);
+ assert(U4 * 6 <= -2);
+ assert((U4 + 1) * 6 > -2);
+ assert(L5 * 6 <= -2);
+ assert((L5 - 1) * 6 > -2);
+ assert(U5 * 6 <= -2);
+ assert((U5 + 1) * 6 > -2);
+ assert(L6 * 6 <= -2);
+ assert((L6 - 1) * 6 > -2);
+ assert(INT_MAX * 6 <= -2);
+
+ if (n < (int32_t) 0xb5555555) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xe0000000) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x0aaaaaaa) {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x35555555) {
+ clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x60000000) {
+ clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_division_le_0(int32_t n) {
+ if (n / 4 <= 0) {
+ const int32_t C = 3;
+
+ assert(C / 4 <= 0);
+ assert((C + 1) / 4 > 0);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_le_1(int32_t n) {
+ if (n / 3 <= 2) {
+ const int32_t C = 8;
+
+ assert(C / 3 <= 2);
+ assert((C + 1) / 3 > 2);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_le_2(int32_t n) {
+ if (n / 5 <= -7) {
+ const int32_t C = -35;
+
+ assert(C / 5 <= -7);
+ assert((C + 1) / 5 > -7);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_multiplication_le_0(uint32_t n) {
+ if (n * 2 <= 3) {
+ uint32_t U1 = 1,
+ L2 = 0x80000000, U2 = 0x80000001;
+
+ assert(U1 * 2 <= 3);
+ assert((U1 + 1) * 2 > 3);
+ assert(L2 * 2 <= 3);
+ assert((L2 - 1) * 2 > 3);
+ assert(U2 * 2 <= 3);
+ assert((U2 + 1) * 2 > 3);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_le_1(uint32_t n) {
+ if (n * 2 <= 4) {
+ uint32_t U1 = 2,
+ L2 = 0x80000000, U2 = 0x80000002;
+
+ assert(U1 * 2 <= 4);
+ assert((U1 + 1) * 2 > 4);
+ assert(L2 * 2 <= 4);
+ assert((L2 - 1) * 2 > 4);
+ assert(U2 * 2 <= 4);
+ assert((U2 + 1) * 2 > 4);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_le_2(uint32_t n) {
+ if (n * 2 <= 5) {
+ uint32_t U1 = 2,
+ L2 = 0x80000000, U2 = 0x80000002;
+
+ assert(U1 * 2 <= 5);
+ assert((U1 + 1) * 2 > 5);
+ assert(L2 * 2 <= 5);
+ assert((L2 - 1) * 2 > 5);
+ assert(U2 * 2 <= 5);
+ assert((U2 + 1) * 2 > 5);
+
+ if (n < UINT_MAX / 2) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_multiplication_le_3(uint32_t n) {
+ if (n * 3 <= 4) {
+ uint32_t U1 = 1,
+ C2 = 0x55555556,
+ L3 = 0xaaaaaaab, U3 = 0xaaaaaaac;
+
+ assert(U1 * 3 <= 4);
+ assert((U1 + 1) * 3 > 4);
+ assert(C2 * 3 <= 4);
+ assert((C2 - 1) * 3 > 4);
+ assert((C2 + 1) * 3 > 4);
+ assert(L3 * 3 <= 4);
+ assert((L3 - 1) * 3 > 4);
+ assert(U3 * 3 <= 4);
+ assert((U3 + 1) * 3 > 4);
+
+ if (n < 0x2aaaaaab) {
+ clang_analyzer_eval(n == 0); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < 0x80000000) {
+ clang_analyzer_eval(n < C2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n == C2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void unsigned_division_le_0(uint32_t n) {
+ if (n / 4 <= 0) {
+ const uint32_t C = 3;
+
+ assert(C / 4 <= 0);
+ assert((C + 1) / 4 > 0);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_division_le_1(uint32_t n) {
+ if (n / 3 <= 2) {
+ const uint32_t C = 8;
+
+ assert(C / 3 <= 2);
+ assert((C + 1) / 3 > 2);
+
+ clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_multiplication_gt_0(int32_t n) {
+ if (n * 2 > 3) {
+ int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+ L2 = 2, U2 = 0x3fffffff;
+
+ assert(L1 * 2 > 3);
+ assert((L1 - 1) * 2 <= 3);
+ assert(U1 * 2 > 3);
+ assert((U1 + 1) * 2 <= 3);
+ assert(L2 * 2 > 3);
+ assert((L2 - 1) * 2 <= 3);
+ assert(U2 * 2 > 3);
+ assert((U2 + 1) * 2 <= 3);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_gt_1(int32_t n) {
+ if (n * 2 > 4) {
+ int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+ L2 = 3, U2 = 0x3fffffff;
+
+ assert(L1 * 2 > 4);
+ assert((L1 - 1) * 2 <= 4);
+ assert(U1 * 2 > 4);
+ assert((U1 + 1) * 2 <= 4);
+ assert(L2 * 2 > 4);
+ assert((L2 - 1) * 2 <= 4);
+ assert(U2 * 2 > 4);
+ assert((U2 + 1) * 2 <= 4);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_gt_2(int32_t n) {
+ if (n * 2 > 5) {
+ int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+ L2 = 3, U2 = 0x3fffffff;
+
+ assert(L1 * 2 > 5);
+ assert((L1 - 1) * 2 <= 5);
+ assert(U1 * 2 > 5);
+ assert((U1 + 1) * 2 <= 5);
+ assert(L2 * 2 > 5);
+ assert((L2 - 1) * 2 <= 5);
+ assert(U2 * 2 > 5);
+ assert((U2 + 1) * 2 <= 5);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_gt_3(int32_t n) {
+ if (n * 3 > 4) {
+ int32_t L1 = 0xaaaaaaad, U1 = 0xd5555555,
+ L2 = 2, U2 = 0x2aaaaaaa,
+ L3 = 0x55555557;
+
+ assert(L1 * 3 > 4);
+ assert((L1 - 1) * 3 <= 4);
+ assert(U1 * 3 > 4);
+ assert((U1 + 1) * 3 <= 4);
+ assert(L2 * 3 > 4);
+ assert((L2 - 1) * 3 <= 4);
+ assert(U2 * 3 > 4);
+ assert((U2 + 1) * 3 <= 4);
+ assert(L3 * 3 > 4);
+ assert((L3 - 1) * 3 <= 4);
+ assert(INT_MAX * 3 > 4);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_gt_4(int32_t n) {
+ if (n * 6 > -2) {
+ int32_t U1 = 0x95555555,
+ L2 = 0xaaaaaaab, U2 = 0xbfffffff,
+ L3 = 0xd5555556, U3 = 0xeaaaaaaa,
+ L4 = 0, U4 = 0x15555555,
+ L5 = 0x2aaaaaab, U5 = 0x3fffffff,
+ L6 = 0x55555556, U6 = 0x6aaaaaaa;
+
+ assert(INT_MIN * 6 > -2);
+ assert(U1 * 6 > -2);
+ assert((U1 + 1) * 6 <= -2);
+ assert(L2 * 6 > -2);
+ assert((L2 - 1) * 6 <= -2);
+ assert(U2 * 6 > -2);
+ assert((U2 + 1) * 6 <= -2);
+ assert(L3 * 6 > -2);
+ assert((L3 - 1) * 6 <= -2);
+ assert(U3 * 6 > -2);
+ assert((U3 + 1) * 6 <= -2);
+ assert(L4 * 6 > -2);
+ assert((L4 - 1) * 6 <= -2);
+ assert(U4 * 6 > -2);
+ assert((U4 + 1) * 6 <= -2);
+ assert(L5 * 6 > -2);
+ assert((L5 - 1) * 6 <= -2);
+ assert(U5 * 6 > -2);
+ assert((U5 + 1) * 6 <= -2);
+ assert(L6 * 6 > -2);
+ assert((L6 - 1) * 6 <= -2);
+ assert(U6 * 6 > -2);
+ assert((U6 + 1) * 6 <= -2);
+
+ if (n < (int32_t) 0xa0000000) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xcaaaaaaa) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xf5555555) {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x20000000) {
+ clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x4aaaaaaa) {
+ clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U6); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_division_gt_0(int32_t n) {
+ if (n / 4 > 0) {
+ const int32_t C = 4;
+
+ assert(C / 4 > 0);
+ assert((C - 1) / 4 <= 0);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_gt_1(int32_t n) {
+ if (n / 3 > 2) {
+ const int32_t C = 9;
+
+ assert(C / 3 > 2);
+ assert((C - 1) / 3 <= 2);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_gt_2(int32_t n) {
+ if (n / 5 > -7) {
+ const int32_t C = -34;
+
+ assert(C / 5 > -7);
+ assert((C - 1) / 5 <= -7);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_multiplication_gt_0(uint32_t n) {
+ if (n * 2 > 3) {
+ uint32_t L1 = 2, U1 = 0x7fffffff,
+ L2 = 0x80000002;
+
+ assert(L1 * 2 > 3);
+ assert((L1 - 1) * 2 <= 3);
+ assert(U1 * 2 > 3);
+ assert((U1 + 1) * 2 <= 3);
+ assert(L2 * 2 > 3);
+ assert((L2 - 1) * 2 <= 3);
+ assert(UINT_MAX * 2 > 3);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_gt_1(uint32_t n) {
+ if (n * 2 > 4) {
+ uint32_t L1 = 3, U1 = 0x7fffffff,
+ L2 = 0x80000003;
+
+ assert(L1 * 2 > 4);
+ assert((L1 - 1) * 2 <= 4);
+ assert(U1 * 2 > 4);
+ assert((U1 + 1) * 2 <= 4);
+ assert(L2 * 2 > 4);
+ assert((L2 - 1) * 2 <= 4);
+ assert(UINT_MAX * 2 > 4);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_gt_2(uint32_t n) {
+ if (n * 2 > 5) {
+ uint32_t L1 = 3, U1 = 0x7fffffff,
+ L2 = 0x80000003;
+
+ assert(L1 * 2 > 5);
+ assert((L1 - 1) * 2 <= 5);
+ assert(U1 * 2 > 5);
+ assert((U1 + 1) * 2 <= 5);
+ assert(L2 * 2 > 5);
+ assert((L2 - 1) * 2 <= 5);
+ assert(UINT_MAX * 2 > 5);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_gt_3(uint32_t n) {
+ if (n * 3 > 4) {
+ uint32_t L1 = 2, U1 = 0x55555555,
+ L2 = 0x55555557, U2 = 0xaaaaaaaa,
+ L3 = 0xaaaaaaad;
+
+ assert(L1 * 3 > 4);
+ assert((L1 - 1) * 3 <= 4);
+ assert(U1 * 3 > 4);
+ assert((U1 + 1) * 3 <= 4);
+ assert(L2 * 3 > 4);
+ assert((L2 - 1) * 3 <= 4);
+ assert(U2 * 3 > 4);
+ assert((U2 + 1) * 3 <= 4);
+ assert(L3 * 3 > 4);
+ assert((L3 - 1) * 3 <= 4);
+ assert(INT_MAX * 3 > 4);
+
+ if (n < UINT_MAX / 3 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < 2 * (UINT_MAX / 3 + 1)) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_division_gt_0(uint32_t n) {
+ if (n / 4 > 0) {
+ const uint32_t C = 4;
+
+ assert(C / 4 > 0);
+ assert((C - 1) / 4 <= 0);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_division_gt_1(uint32_t n) {
+ if (n / 3 > 2) {
+ const uint32_t C = 9;
+
+ assert(C / 3 > 2);
+ assert((C - 1) / 3 <= 2);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_multiplication_ge_0(int32_t n) {
+ if (n * 2 >= 3) {
+ int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+ L2 = 2, U2 = 0x3fffffff;
+
+ assert(L1 * 2 >= 3);
+ assert((L1 - 1) * 2 < 3);
+ assert(U1 * 2 >= 3);
+ assert((U1 + 1) * 2 < 3);
+ assert(L2 * 2 >= 3);
+ assert((L2 - 1) * 2 < 3);
+ assert(U2 * 2 >= 3);
+ assert((U2 + 1) * 2 < 3);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_ge_1(int32_t n) {
+ if (n * 2 >= 4) {
+ int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+ L2 = 2, U2 = 0x3fffffff;
+
+ assert(L1 * 2 >= 4);
+ assert((L1 - 1) * 2 < 4);
+ assert(U1 * 2 >= 4);
+ assert((U1 + 1) * 2 < 4);
+ assert(L2 * 2 >= 4);
+ assert((L2 - 1) * 2 < 4);
+ assert(U2 * 2 >= 4);
+ assert((U2 + 1) * 2 < 4);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_ge_2(int32_t n) {
+ if (n * 2 >= 5) {
+ int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+ L2 = 3, U2 = 0x3fffffff;
+
+ assert(L1 * 2 >= 5);
+ assert((L1 - 1) * 2 < 5);
+ assert(U1 * 2 >= 5);
+ assert((U1 + 1) * 2 < 5);
+ assert(L2 * 2 >= 5);
+ assert((L2 - 1) * 2 < 5);
+ assert(U2 * 2 >= 5);
+ assert((U2 + 1) * 2 < 5);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_multiplication_ge_3(int32_t n) {
+ if (n * 3 >= 4) {
+ int32_t L1 = 0xaaaaaaac, U1 = 0xd5555555,
+ L2 = 2, U2 = 0x2aaaaaaa,
+ L3 = 0x55555557;
+
+ assert(L1 * 3 >= 4);
+ assert((L1 - 1) * 3 < 4);
+ assert(U1 * 3 >= 4);
+ assert((U1 + 1) * 3 < 4);
+ assert(L2 * 3 >= 4);
+ assert((L2 - 1) * 3 < 4);
+ assert(U2 * 3 >= 4);
+ assert((U2 + 1) * 3 < 4);
+ assert(L3 * 3 >= 4);
+ assert((L3 - 1) * 3 < 4);
+ assert(INT_MAX * 3 >= 4);
+
+ if (n < 0) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < INT_MAX / 2) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == INT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void signed_multiplication_ge_4(int32_t n) {
+ if (n * 6 >= -2) {
+ int32_t U1 = 0x95555555,
+ L2 = 0xaaaaaaab, U2 = 0xbfffffff,
+ L3 = 0xd5555555, U3 = 0xeaaaaaaa,
+ L4 = 0, U4 = 0x15555555,
+ L5 = 0x2aaaaaab, U5 = 0x3fffffff,
+ L6 = 0x55555555, U6 = 0x6aaaaaaa;
+
+ assert(INT_MIN * 6 >= -2);
+ assert(U1 * 6 >= -2);
+ assert((U1 + 1) * 6 < -2);
+ assert(L2 * 6 >= -2);
+ assert((L2 - 1) * 6 < -2);
+ assert(U2 * 6 >= -2);
+ assert((U2 + 1) * 6 < -2);
+ assert(L3 * 6 >= -2);
+ assert((L3 - 1) * 6 < -2);
+ assert(U3 * 6 >= -2);
+ assert((U3 + 1) * 6 < -2);
+ assert(L4 * 6 >= -2);
+ assert((L4 - 1) * 6 < -2);
+ assert(U4 * 6 >= -2);
+ assert((U4 + 1) * 6 < -2);
+ assert(L5 * 6 >= -2);
+ assert((L5 - 1) * 6 < -2);
+ assert(U5 * 6 >= -2);
+ assert((U5 + 1) * 6 < -2);
+ assert(L6 * 6 >= -2);
+ assert((L6 - 1) * 6 < -2);
+ assert(U6 * 6 >= -2);
+ assert((U6 + 1) * 6 < -2);
+
+ if (n < (int32_t) 0xa0000000) {
+ clang_analyzer_eval(n == INT_MIN); //expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xcaaaaaaa) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0xf5555555) {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x20000000) {
+ clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+ } else if (n < (int32_t) 0x4aaaaaaa) {
+ clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U6); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U6); //expected-warning{{FALSE}}
+ }
+ }
+}
+
+void signed_division_ge_0(int32_t n) {
+ if (n / 4 >= 0) {
+ const int32_t C = -3;
+
+ assert(C / 4 >= 0);
+ assert((C - 1) / 4 < 0);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_ge_1(int32_t n) {
+ if (n / 3 >= 2) {
+ const int32_t C = 6;
+
+ assert(C / 3 >= 2);
+ assert((C - 1) / 3 < 2);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void signed_division_ge_2(int32_t n) {
+ if (n / 5 >= -7) {
+ const int32_t C = -39;
+
+ assert(C / 5 >= -7);
+ assert((C - 1) / 5 < -7);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
+void unsigned_multiplication_ge_0(uint32_t n) {
+ if (n * 2 >= 3) {
+ uint32_t L1 = 2, U1 = 0x7fffffff,
+ L2 = 0x80000002;
+
+ assert(L1 * 2 >= 3);
+ assert((L1 - 1) * 2 < 3);
+ assert(U1 * 2 >= 3);
+ assert((U1 + 1) * 2 < 3);
+ assert(L2 * 2 >= 3);
+ assert((L2 - 1) * 2 < 3);
+ assert(UINT_MAX * 2 >= 3);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_ge_1(uint32_t n) {
+ if (n * 2 >= 4) {
+ uint32_t L1 = 2, U1 = 0x7fffffff,
+ L2 = 0x80000002;
+
+ assert(L1 * 2 >= 4);
+ assert((L1 - 1) * 2 < 4);
+ assert(U1 * 2 >= 4);
+ assert((U1 + 1) * 2 < 4);
+ assert(L2 * 2 >= 4);
+ assert((L2 - 1) * 2 < 4);
+ assert(UINT_MAX * 2 >= 4);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_ge_2(uint32_t n) {
+ if (n * 2 >= 5) {
+ uint32_t L1 = 3, U1 = 0x7fffffff,
+ L2 = 0x80000003;
+
+ assert(L1 * 2 >= 5);
+ assert((L1 - 1) * 2 < 5);
+ assert(U1 * 2 >= 5);
+ assert((U1 + 1) * 2 < 5);
+ assert(L2 * 2 >= 5);
+ assert((L2 - 1) * 2 < 5);
+ assert(UINT_MAX * 2 >= 5);
+
+ if (n < UINT_MAX / 2 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_multiplication_ge_3(uint32_t n) {
+ if (n * 3 >= 4) {
+ uint32_t L1 = 2, U1 = 0x55555555,
+ L2 = 0x55555557, U2 = 0xaaaaaaaa,
+ L3 = 0xaaaaaaac;
+
+ assert(L1 * 3 >= 4);
+ assert((L1 - 1) * 3 < 4);
+ assert(U1 * 3 >= 4);
+ assert((U1 + 1) * 3 < 4);
+ assert(L2 * 3 >= 4);
+ assert((L2 - 1) * 3 < 4);
+ assert(U2 * 3 >= 4);
+ assert((U2 + 1) * 3 < 4);
+ assert(L3 * 3 >= 4);
+ assert((L3 - 1) * 3 < 4);
+ assert(INT_MAX * 3 >= 4);
+
+ if (n < UINT_MAX / 3 + 1) {
+ clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+ } else if (n < 2 * (UINT_MAX / 3 + 1)) {
+ clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+ clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n == UINT_MAX); //expected-warning{{UNKNOWN}}
+ }
+ }
+}
+
+void unsigned_division_ge_0(uint32_t n) {
+ if (n / 3 >= 2) {
+ const uint32_t C = 6;
+
+ assert(C / 3 >= 2);
+ assert((C - 1) / 3 < 2);
+
+ clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+ clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+ }
+}
+
void additive(int32_t n) {
if (n * 2 + 1 == 4) {
clang_analyzer_warnIfReached(); // no-warning
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -82,21 +82,27 @@
SymbolRef AdjustedSym = Sym;
computeAdjustment(AdjustedSym, Adjustment);
+ ScalingFactor Scale = {WraparoundType.getValue(1), false};
+ SymbolRef ScaledSym = AdjustedSym;
+ computeScale(ScaledSym, Scale);
+
// Convert the right-hand side integer as necessary.
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
llvm::APSInt ConvertedTo = ComparisonType.convert(To);
// Prefer unsigned comparisons.
if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
- ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+ ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) {
+ Scale.Val.setIsSigned(false);
Adjustment.setIsSigned(false);
+ }
if (InRange)
return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
- ConvertedTo, Adjustment);
+ ConvertedTo, Scale, Adjustment);
return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
- ConvertedTo, Adjustment);
+ ConvertedTo, Scale, Adjustment);
}
ProgramStateRef
@@ -157,9 +163,7 @@
// SimpleConstraintManager to handle the scaling.
ScalingFactor Scale = {WraparoundType.getValue(1), false};
- // FIXME: For now scaling only works for == and !=
- if (Op == BO_EQ || Op == BO_NE)
- computeScale(Sym, Scale);
+ computeScale(Sym, Scale);
// Convert the right-hand side integer as necessary.
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
@@ -183,16 +187,16 @@
return assumeSymNE(State, Sym, ConvertedInt, Scale, Adjustment);
case BO_GT:
- return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
+ return assumeSymGT(State, Sym, ConvertedInt, Scale, Adjustment);
case BO_GE:
- return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
+ return assumeSymGE(State, Sym, ConvertedInt, Scale, Adjustment);
case BO_LT:
- return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
+ return assumeSymLT(State, Sym, ConvertedInt, Scale, Adjustment);
case BO_LE:
- return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
+ return assumeSymLE(State, Sym, ConvertedInt, Scale, Adjustment);
} // end switch
}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -260,27 +260,33 @@
ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) override;
ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) override;
ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) override;
ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) override;
ProgramStateRef assumeSymWithinInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) override;
ProgramStateRef assumeSymOutsideInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) override;
private:
RangeSet::Factory F;
@@ -291,22 +297,28 @@
RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment);
RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment);
RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment);
RangeSet getSymLERange(llvm::function_ref<RangeSet()> RS,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment);
RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment);
bool rescale(llvm::APSInt &Int, const ScalingFactor &Scale,
- const llvm::APSInt &Index);
+ const llvm::APSInt &Index,
+ const ScalingFactor::RoundingMode Rounding);
};
} // end anonymous namespace
@@ -514,9 +526,11 @@
return nullptr;
}
-bool RangeConstraintManager::rescale(llvm::APSInt &Int,
- const ScalingFactor &Scale,
- const llvm::APSInt &Index) {
+bool
+RangeConstraintManager::rescale(llvm::APSInt &Int,
+ const ScalingFactor &Scale,
+ const llvm::APSInt &Index,
+ const ScalingFactor::RoundingMode Rounding) {
if (Scale.Val == 1)
return true;
@@ -544,7 +558,22 @@
llvm::APSInt Frac = Remainder + Index * PeriodFrac;
Int = Quotient + Index * PeriodInt + Frac / Scale.Val;
- return (Frac % Scale.Val).isNullValue();
+ switch(Rounding) {
+ default:
+ llvm_unreachable("Invalid rounding mode!");
+ case ScalingFactor::rmExact:
+ return (Frac % Scale.Val).isNullValue();
+ case ScalingFactor::rmDown:
+ if (Frac % Scale.Val < ScaleType.getZeroValue()) {
+ --Int;
+ }
+ return true;
+ case ScalingFactor::rmUp:
+ if (Frac % Scale.Val > ScaleType.getZeroValue()) {
+ ++Int;
+ }
+ return true;
+ }
}
}
@@ -579,7 +608,7 @@
I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
llvm::APSInt ScInt = AdjInt;
- if (!rescale(ScInt, Scale, I))
+ if (!rescale(ScInt, Scale, I, ScalingFactor::rmExact))
continue;
llvm::APSInt Lower = ScInt;
@@ -618,7 +647,7 @@
I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
llvm::APSInt ScInt = AdjInt;
- if (!rescale(ScInt, Scale, I))
+ if (!rescale(ScInt, Scale, I, ScalingFactor::rmExact))
continue;
llvm::APSInt Lower = ScInt;
@@ -641,6 +670,7 @@
RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
// Before we do any real work, see if the value can even show up.
APSIntType AdjustmentType(Adjustment);
@@ -659,24 +689,42 @@
if (ComparisonVal == Min)
return F.getEmptySet();
- llvm::APSInt Lower = Min - Adjustment;
- llvm::APSInt Upper = ComparisonVal - Adjustment;
- --Upper;
+ llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+ llvm::APSInt AdjMin = Min - Adjustment;
+ RangeSet New = F.getEmptySet();
+ for (llvm::APSInt I = AdjustmentType.getZeroValue();
+ I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+ llvm::APSInt Lower = AdjMin;
+ rescale(Lower, Scale, I, ScalingFactor::rmUp);
+ llvm::APSInt Upper = AdjCompVal;
+ rescale(Upper, Scale, I, ScalingFactor::rmUp);
+ Upper -= (Scale.Reciprocal && Upper <= 0) ? Scale.Val :
+ AdjustmentType.getValue(1);
+
+ if (Lower == Upper + AdjustmentType.getValue(1))
+ continue;
+
+ New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+ Upper));
+ }
- return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+ return New;
}
ProgramStateRef
RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
- RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
+ RangeSet New = getSymLTRange(St, Sym, Int, Scale, Adjustment);
return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
}
RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
// Before we do any real work, see if the value can even show up.
APSIntType AdjustmentType(Adjustment);
@@ -695,24 +743,42 @@
if (ComparisonVal == Max)
return F.getEmptySet();
- llvm::APSInt Lower = ComparisonVal - Adjustment;
- llvm::APSInt Upper = Max - Adjustment;
- ++Lower;
+ llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+ llvm::APSInt AdjMax = Max - Adjustment;
+ RangeSet New = F.getEmptySet();
+ for (llvm::APSInt I = AdjustmentType.getZeroValue();
+ I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+ llvm::APSInt Lower = AdjCompVal;
+ rescale(Lower, Scale, I, ScalingFactor::rmDown);
+ llvm::APSInt Upper = AdjMax;
+ rescale(Upper, Scale, I, ScalingFactor::rmDown);
+ Lower += (Scale.Reciprocal && Lower >= 0) ? Scale.Val :
+ AdjustmentType.getValue(1);
+
+ if (Lower == Upper + AdjustmentType.getValue(1))
+ continue;
+
+ New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+ Upper));
+ }
- return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+ return New;
}
ProgramStateRef
RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
- RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
+ RangeSet New = getSymGTRange(St, Sym, Int, Scale, Adjustment);
return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
}
RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
// Before we do any real work, see if the value can even show up.
APSIntType AdjustmentType(Adjustment);
@@ -732,23 +798,45 @@
return getRange(St, Sym);
llvm::APSInt Max = AdjustmentType.getMaxValue();
- llvm::APSInt Lower = ComparisonVal - Adjustment;
- llvm::APSInt Upper = Max - Adjustment;
- return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+ llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+ llvm::APSInt AdjMax = Max - Adjustment;
+ RangeSet New = F.getEmptySet();
+ for (llvm::APSInt I = AdjustmentType.getZeroValue();
+ I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+ llvm::APSInt Lower = AdjCompVal;
+ rescale(Lower, Scale, I, ScalingFactor::rmUp);
+ llvm::APSInt Upper = AdjMax;
+ rescale(Upper, Scale, I, ScalingFactor::rmDown);
+
+ if (Scale.Reciprocal && Lower <= 0) {
+ Lower -= Scale.Val - AdjustmentType.getValue(1);
+ }
+
+ if (Lower == Upper + AdjustmentType.getValue(1))
+ continue;
+
+ New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+ Upper));
+ }
+
+ return New;
}
ProgramStateRef
RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
- RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
+ RangeSet New = getSymGERange(St, Sym, Int, Scale, Adjustment);
return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
}
RangeSet RangeConstraintManager::getSymLERange(
llvm::function_ref<RangeSet()> RS,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
// Before we do any real work, see if the value can even show up.
APSIntType AdjustmentType(Adjustment);
@@ -768,42 +856,66 @@
return RS();
llvm::APSInt Min = AdjustmentType.getMinValue();
- llvm::APSInt Lower = Min - Adjustment;
- llvm::APSInt Upper = ComparisonVal - Adjustment;
- return RS().Intersect(getBasicVals(), F, Lower, Upper);
+ llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+ llvm::APSInt AdjMin = Min - Adjustment;
+ RangeSet New = F.getEmptySet();
+ for (llvm::APSInt I = AdjustmentType.getZeroValue();
+ I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+ llvm::APSInt Lower = AdjMin;
+ rescale(Lower, Scale, I, ScalingFactor::rmUp);
+ llvm::APSInt Upper = AdjCompVal;
+ rescale(Upper, Scale, I, ScalingFactor::rmDown);
+
+ if (Scale.Reciprocal && Upper >= 0) {
+ Upper += Scale.Val - AdjustmentType.getValue(1);
+ }
+
+ if (Lower == Upper + AdjustmentType.getValue(1))
+ continue;
+
+ New = New.addRange(F, RS().Intersect(getBasicVals(), F, Lower, Upper));
+ }
+
+ return New;
}
RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
- return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment);
+ return getSymLERange([&] { return getRange(St, Sym); }, Int, Scale,
+ Adjustment);
}
ProgramStateRef
RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) {
- RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
+ RangeSet New = getSymLERange(St, Sym, Int, Scale, Adjustment);
return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
}
ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
- RangeSet New = getSymGERange(State, Sym, From, Adjustment);
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) {
+ RangeSet New = getSymGERange(State, Sym, From, Scale, Adjustment);
if (New.isEmpty())
return nullptr;
- RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment);
+ RangeSet Out = getSymLERange([&] { return New; }, To, Scale, Adjustment);
return Out.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, Out);
}
ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
- RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
- RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) {
+ RangeSet RangeLT = getSymLTRange(State, Sym, From, Scale, Adjustment);
+ RangeSet RangeGT = getSymGTRange(State, Sym, To, Scale, Adjustment);
RangeSet New(RangeLT.addRange(F, RangeGT));
return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
}
Index: include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -161,6 +161,8 @@
struct ScalingFactor {
llvm::APSInt Val;
bool Reciprocal;
+
+ enum RoundingMode {rmExact, rmDown, rmUp};
};
/// Assume a constraint between a symbolic expression and a concrete integer.
@@ -187,27 +189,33 @@
virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) = 0;
virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) = 0;
virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) = 0;
virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &V,
+ const ScalingFactor &Scale,
const llvm::APSInt &Adjustment) = 0;
virtual ProgramStateRef assumeSymWithinInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) = 0;
virtual ProgramStateRef assumeSymOutsideInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+ const llvm::APSInt &To, const ScalingFactor &Scale,
+ const llvm::APSInt &Adjustment) = 0;
//===------------------------------------------------------------------===//
// Internal implementation.
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
