40cc4379cd
Before this commit the LIT test framework of the static analyzer had a
file called `analyzer_test.py` which implemented a tricky system for
selecting the constraint manager:
- (A) Test files without `REQUIRES: z3` were executed with the default
range-based constraint manager.
- (B) If clang was built with Z3 support _and_ `USE_Z3_SOLVER=1` was
passed to the test run, the test was executed with Z3 as the
constraint manager.
(There was support for executing the same RUN line twice if both
conditions were satisfied.)
Unfortunately, using Z3 as the constraint manager does not work in
practice (very slow and causes many crashes), so the (B) pathway became
unused (or was never truly used?) and became broken due to bit rot. (In
the CI bots the analyzer is built without Z3 support, so only the
pathway (A) is used.)
This commit removes `analyzer_test.py` (+ related logic in other build
files + the test `z3/enabled.c` which just tested that
`analyzer_test.py` is active), because it tries to implement a feature
that we don't need (only one constraint manager is functional) and its
code is so complicated and buggy that it isn't useful as a starting
point for future development.
The fact that this logic was broken implied that tests with `REQUIRES:
z3` were not executed during normal testing, so they were also affected
by bit rot. Unfortunately this also affected the tests of the
`z3-crosscheck` mode (aka Z3 refutation) which also depends on Z3 but
uses Z3 in a different way which is actually stable and functional.
In this commit I'm fixing most of the `REQUIRES: z3` tests that were
broken by straightforward issues. Two test files, `PR37855.c` and
`z3-crosscheck.c` were affected by more complex issues, so I marked them
as `XFAIL` for now. We're planning to fix them with follow-up commits in
the foreseeable future.
For additional background information see also the discourse thread
https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689
64 lines
2.5 KiB
C
64 lines
2.5 KiB
C
// RUN: %clang_analyze_cc1 -triple amdgcn-unknown-unknown \
|
|
// RUN: -analyzer-checker=core,alpha.unix.cstring,debug.ExprInspection \
|
|
// RUN: -analyzer-config crosscheck-with-z3=true -verify %s \
|
|
// RUN: -Wno-incompatible-library-redeclaration
|
|
// REQUIRES: z3
|
|
|
|
void clang_analyzer_warnIfReached();
|
|
|
|
// From https://llvm.org/docs/AMDGPUUsage.html#address-spaces,
|
|
// select address space 3 (local), since the pointer size is
|
|
// different than Generic.
|
|
#define DEVICE __attribute__((address_space(3)))
|
|
_Static_assert(sizeof(int *) == 8, "");
|
|
_Static_assert(sizeof(DEVICE int *) == 4, "");
|
|
_Static_assert(sizeof(void *) == 8, "");
|
|
_Static_assert(sizeof(DEVICE void *) == 4, "");
|
|
|
|
// Copy from host to device memory. Note this is specialized
|
|
// since one of the parameters is assigned an address space such
|
|
// that the sizeof the the pointer is different than the other.
|
|
//
|
|
// Some downstream implementations may have specialized memcpy
|
|
// routines that copy from one address space to another. In cases
|
|
// like that, the address spaces are assumed to not overlap, so the
|
|
// cstring overlap check is not needed. When a static analysis report
|
|
// is generated in as case like this, SMTConv may attempt to create
|
|
// a refutation to Z3 with different bitwidth pointers which lead to
|
|
// a crash. This is not common in directly used upstream compiler builds,
|
|
// but can be seen in specialized downstrean implementations. This case
|
|
// covers those specific instances found and debugged.
|
|
//
|
|
// Since memcpy is a builtin, a specialized builtin instance named like
|
|
// 'memcpy_special' will hit in cstring, triggering this behavior. The
|
|
// best we can do for an upstream test is use the same memcpy function name.
|
|
DEVICE void *memcpy(DEVICE void *dst, const void *src, unsigned long len);
|
|
|
|
void top1(DEVICE void *dst, void *src, int len) {
|
|
memcpy(dst, src, len);
|
|
|
|
// Create a bugreport for triggering Z3 refutation.
|
|
clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
|
|
}
|
|
|
|
void top2(DEVICE int *dst, void *src, int len) {
|
|
memcpy(dst, src, len);
|
|
|
|
// Create a bugreport for triggering Z3 refutation.
|
|
clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
|
|
}
|
|
|
|
void top3(DEVICE int *dst, int *src, int len) {
|
|
memcpy(dst, src, len);
|
|
|
|
// Create a bugreport for triggering Z3 refutation.
|
|
clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
|
|
}
|
|
|
|
void top4() {
|
|
memcpy((DEVICE void *)1, (const void *)1, 1);
|
|
|
|
// Create a bugreport for triggering Z3 refutation.
|
|
clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
|
|
}
|