sparse: add an address space and a __sparse_force annotation

We want to use a sparse address space to identify invalid conversions
between cached and uncached address aliases. This patch adds a
__sparse_cache sparse annotation for that. Where those conversions
must be done that has to be supported by using the __sparse_force
sparse attribute. To avoid compiler complains about unknown
attributes we add a -Wno-attributes flag when building with sparse
support.

Signed-off-by: Guennadi Liakhovetski <[email protected]>

Author: lyakh

CMakeLists.txt

@@ -269,6 +269,8 @@ endif()
 
 if("${SPARSE}" STREQUAL "y")
   list(APPEND TOOLCHAIN_C_FLAGS -D__CHECKER__)
+  # Avoid compiler "attribute directive ignored" warnings
+  list(APPEND TOOLCHAIN_C_FLAGS -Wno-attributes)
 endif()
 
 zephyr_compile_options(

include/zephyr/arch/xtensa/cache.h

@@ -8,6 +8,7 @@
 #include <xtensa/config/core-isa.h>
 #include <toolchain.h>
 #include <sys/util.h>
+#include <debug/sparse.h>
 
 #ifdef __cplusplus
 extern "C" {
@@ -127,11 +128,11 @@ static ALWAYS_INLINE uint32_t z_xtrpoflip(uint32_t addr, uint32_t rto, uint32_t
  * @param ptr A pointer to a valid C object
  * @return A pointer to the same object via the L1 dcache
  */
-static inline void *arch_xtensa_cached_ptr(void *ptr)
+static inline void __sparse_cache *arch_xtensa_cached_ptr(void *ptr)
 {
-	return (void *)z_xtrpoflip((uint32_t) ptr,
-				   CONFIG_XTENSA_CACHED_REGION,
-				   CONFIG_XTENSA_UNCACHED_REGION);
+	return (__sparse_force void __sparse_cache *)z_xtrpoflip((uint32_t) ptr,
+						CONFIG_XTENSA_CACHED_REGION,
+						CONFIG_XTENSA_UNCACHED_REGION);
 }
 
 /**
@@ -152,7 +153,7 @@ static inline void *arch_xtensa_cached_ptr(void *ptr)
  * @param ptr A pointer to a valid C object
  * @return A pointer to the same object bypassing the L1 dcache
  */
-static inline void *arch_xtensa_uncached_ptr(void *ptr)
+static inline void *arch_xtensa_uncached_ptr(void __sparse_cache *ptr)
 {
 	return (void *)z_xtrpoflip((uint32_t) ptr,
 				   CONFIG_XTENSA_UNCACHED_REGION,

include/zephyr/debug/sparse.h

@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) 2022 Intel Corporation
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+#ifndef ZEPHYR_INCLUDE_DEBUG_SPARSE_H
+#define ZEPHYR_INCLUDE_DEBUG_SPARSE_H
+
+#if defined(__CHECKER__)
+#define __sparse_cache __attribute__((address_space(__cache)))
+#define __sparse_force __attribute__((force))
+#else
+#define __sparse_cache
+#define __sparse_force
+#endif
+
+#endif