vabridgers created this revision.
vabridgers added reviewers: steakhal, martong.
Herald added subscribers: manas, ASDenysPetrov, dkrupp, donat.nagy, Szelethus,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun.
vabridgers requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
This change fixes an assert that occurs in the SMT layer when refuting a
finding that uses pointers of two different sizes. This was found in a
downstream build that supports two different pointer sizes, The CString
Checker was attempting to compute an overlap for the 'to' and 'from'
pointers, where the pointers were of different sizes.
The problem was reproduced using a amdgcn target, and an upstreamable
test produced for the fix.
The assert seen is:
`*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same
sort!"'
Ack to steakhal for reviewing the fix, and creating the test case.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D118050
Files:
clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
clang/test/Analysis/cstring-checker-addressspace.c
Index: clang/test/Analysis/cstring-checker-addressspace.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/cstring-checker-addressspace.c
@@ -0,0 +1,21 @@
+// RUN: %clang_analyze_cc1 -triple amdgcn-unknown-unknown \
+// RUN: -analyze -analyzer-checker=core,alpha.unix.cstring \
+// RUN: -analyze -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_warnIfReached();
+
+#define DEVICE __attribute__((address_space(256)))
+_Static_assert(sizeof(int *) == 4, "");
+_Static_assert(sizeof(DEVICE int *) == 8, "");
+
+// Copy from host to device memory.
+DEVICE void *memcpy(DEVICE void *dst, const void *src, unsigned long len);
+
+void top(DEVICE int *dst, int *src, int len) {
+ memcpy(dst, src, len);
+
+ // Create a bugreport for triggering Z3 refutation.
+ clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}
Index: clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
@@ -449,6 +449,11 @@
ProgramStateRef stateTrue, stateFalse;
+ // Assume different address spaces cannot overlap.
+ if (First.Expression->getType()->getPointeeType().getAddressSpace() !=
+ Second.Expression->getType()->getPointeeType().getAddressSpace())
+ return state;
+
// Get the buffer values and make sure they're known locations.
const LocationContext *LCtx = C.getLocationContext();
SVal firstVal = state->getSVal(First.Expression, LCtx);
Index: clang/test/Analysis/cstring-checker-addressspace.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/cstring-checker-addressspace.c
@@ -0,0 +1,21 @@
+// RUN: %clang_analyze_cc1 -triple amdgcn-unknown-unknown \
+// RUN: -analyze -analyzer-checker=core,alpha.unix.cstring \
+// RUN: -analyze -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_warnIfReached();
+
+#define DEVICE __attribute__((address_space(256)))
+_Static_assert(sizeof(int *) == 4, "");
+_Static_assert(sizeof(DEVICE int *) == 8, "");
+
+// Copy from host to device memory.
+DEVICE void *memcpy(DEVICE void *dst, const void *src, unsigned long len);
+
+void top(DEVICE int *dst, int *src, int len) {
+ memcpy(dst, src, len);
+
+ // Create a bugreport for triggering Z3 refutation.
+ clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}
Index: clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
@@ -449,6 +449,11 @@
ProgramStateRef stateTrue, stateFalse;
+ // Assume different address spaces cannot overlap.
+ if (First.Expression->getType()->getPointeeType().getAddressSpace() !=
+ Second.Expression->getType()->getPointeeType().getAddressSpace())
+ return state;
+
// Get the buffer values and make sure they're known locations.
const LocationContext *LCtx = C.getLocationContext();
SVal firstVal = state->getSVal(First.Expression, LCtx);
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
