Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[analyzer][solver] Handle UnarySymExpr in RangeConstraintSolver
Fixes #55241 Differential Revision: https://reviews.llvm.org/D125395
- Loading branch information
Gabor Marton
committed
May 26, 2022
1 parent
b5b2aec
commit 88abc50
Showing
5 changed files
with
214 additions
and
69 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,113 @@ | ||
// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin \ | ||
// RUN: -analyzer-config eagerly-assume=false \ | ||
// RUN: -verify %s | ||
|
||
void clang_analyzer_eval(int); | ||
void clang_analyzer_dump(int); | ||
|
||
void exit(int); | ||
|
||
#define UINT_MIN (0U) | ||
#define UINT_MAX (~UINT_MIN) | ||
#define UINT_MID (UINT_MAX / 2 + 1) | ||
#define INT_MAX (UINT_MAX & (UINT_MAX >> 1)) | ||
#define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1)) | ||
|
||
extern void abort() __attribute__((__noreturn__)); | ||
#define assert(expr) ((expr) ? (void)(0) : abort()) | ||
|
||
void negate_positive_range(int a) { | ||
assert(-a > 0); | ||
// -a: [1, INT_MAX] | ||
// a: [INT_MIN + 1, -1] | ||
clang_analyzer_eval(a < 0); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(a > INT_MIN); // expected-warning{{TRUE}} | ||
} | ||
|
||
void negate_positive_range2(int a) { | ||
assert(a > 0); | ||
// a: [1, INT_MAX] | ||
// -a: [INT_MIN + 1, -1] | ||
clang_analyzer_eval(-a < 0); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a > INT_MIN); // expected-warning{{TRUE}} | ||
} | ||
|
||
// INT_MIN equals 0b100...00. | ||
// Its two's compelement is 0b011...11 + 1 = 0b100...00 (itself). | ||
_Static_assert(INT_MIN == -INT_MIN, ""); | ||
void negate_int_min(int a) { | ||
assert(a == INT_MIN); | ||
clang_analyzer_eval(-a == INT_MIN); // expected-warning{{TRUE}} | ||
} | ||
|
||
void negate_mixed(int a) { | ||
assert(a > 0 || a == INT_MIN); | ||
clang_analyzer_eval(-a <= 0); // expected-warning{{TRUE}} | ||
} | ||
|
||
void effective_range(int a) { | ||
assert(a >= 0); | ||
assert(-a >= 0); | ||
clang_analyzer_eval(a == 0); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a == 0); // expected-warning{{TRUE}} | ||
} | ||
|
||
_Static_assert(-INT_MIN == INT_MIN, ""); | ||
void effective_range_2(int a) { | ||
assert(a <= 0); | ||
assert(-a <= 0); | ||
clang_analyzer_eval(a == 0 || a == INT_MIN); // expected-warning{{TRUE}} | ||
} | ||
|
||
void negate_symexpr(int a, int b) { | ||
assert(3 <= a * b && a * b <= 5); | ||
clang_analyzer_eval(-(a * b) >= -5); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-(a * b) <= -3); // expected-warning{{TRUE}} | ||
} | ||
|
||
void negate_unsigned_min(unsigned a) { | ||
assert(a == UINT_MIN); | ||
clang_analyzer_eval(-a == UINT_MIN); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a != UINT_MIN); // expected-warning{{FALSE}} | ||
clang_analyzer_eval(-a > UINT_MIN); // expected-warning{{FALSE}} | ||
clang_analyzer_eval(-a < UINT_MIN); // expected-warning{{FALSE}} | ||
} | ||
|
||
_Static_assert(7u - 3u != 3u - 7u, ""); | ||
_Static_assert(-4u == UINT_MAX - 3u, ""); | ||
void negate_unsigned_4(unsigned a) { | ||
assert(a == 4u); | ||
clang_analyzer_eval(-a == 4u); // expected-warning{{FALSE}} | ||
clang_analyzer_eval(-a != 4u); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a == UINT_MAX - 3u); // expected-warning{{TRUE}} | ||
} | ||
|
||
// UINT_MID equals 0b100...00. | ||
// Its two's compelement is 0b011...11 + 1 = 0b100...00 (itself). | ||
_Static_assert(UINT_MID == -UINT_MID, ""); | ||
void negate_unsigned_mid(unsigned a) { | ||
assert(a == UINT_MID); | ||
clang_analyzer_eval(-a == UINT_MID); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a != UINT_MID); // expected-warning{{FALSE}} | ||
} | ||
|
||
void negate_unsigned_mid2(unsigned a) { | ||
assert(UINT_MIN < a && a < UINT_MID); | ||
// a: [UINT_MIN+1, UINT_MID-1] | ||
// -a: [UINT_MID+1, UINT_MAX] | ||
clang_analyzer_eval(-a > UINT_MID); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a <= UINT_MAX); // expected-warning{{TRUE}} | ||
} | ||
|
||
_Static_assert(1u - 2u == UINT_MAX, ""); | ||
_Static_assert(2u - 1u == 1, ""); | ||
void negate_unsigned_max(unsigned a) { | ||
assert(a == UINT_MAX); | ||
clang_analyzer_eval(-a == 1); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a != 1); // expected-warning{{FALSE}} | ||
} | ||
void negate_unsigned_one(unsigned a) { | ||
assert(a == 1); | ||
clang_analyzer_eval(-a == UINT_MAX); // expected-warning{{TRUE}} | ||
clang_analyzer_eval(-a < UINT_MAX); // expected-warning{{FALSE}} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
// RUN: %clang_analyze_cc1 %s \ | ||
// RUN: -analyzer-checker=core,debug.ExprInspection \ | ||
// RUN: -analyzer-config eagerly-assume=false \ | ||
// RUN: -analyzer-config support-symbolic-integer-casts=false \ | ||
// RUN: -verify | ||
|
||
// RUN: %clang_analyze_cc1 %s \ | ||
// RUN: -analyzer-checker=core,debug.ExprInspection \ | ||
// RUN: -analyzer-config eagerly-assume=false \ | ||
// RUN: -analyzer-config support-symbolic-integer-casts=true \ | ||
// RUN: -verify | ||
|
||
// expected-no-diagnostics | ||
|
||
void clang_analyzer_eval(int); | ||
void clang_analyzer_dump(int); | ||
|
||
void crash(int b, long c) { | ||
b = c; | ||
if (b > 0) | ||
if(-b) // should not crash here | ||
; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters