RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

riscv: fix CLZ and CTZ for riscv32 builds (#325)

Browse Source 
A previous commit (9ec5df5f) to provide more efficient CLZ (count
leading zeros) and CTZ (count trailing zeros) removed the `__clzsi2` and
`__ctzsi2` symbols, due to a misunderstanding of the types of these and
other library functions expected by GCC's intrinsics. 9ec5df5f broke the
riscv32 build.

This commit corrects the misunderstanding:
- `__clzsi2` and `__ctzsi2` are reinstated with correct types.
- The types of `__clzdi2` and `__ctzdi2` are corrected.
- `__clzti2` and `__ctzti2` are removed, since seL4 contains no compiler
  intrinsics that would require them.
- `clzl` and `ctzl` dispatch to the appropriate library functions based
  on the size of `unsigned long`.
- Configuration options are updated to ensure that the library functions
  are included in the kernel binary only when needed.

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell
2021-03-30 13:17:16 +11:00
committed by GitHub
parent 2ac4185381
commit 14f2ed7650
4 changed files with 70 additions and 53 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
config.cmake
View File

@@ -463,29 +463,25 @@ config_string(
)
config_option(
KernelClzlImpl CLZL_IMPL
"Define a __clzdi2 function to count leading zeros for unsigned long arguments. \
KernelClz32 CLZ_32 "Define a __clzsi2 function to count leading zeros for uint32_t arguments. \
Only needed on platforms which lack a builtin instruction."
DEFAULT OFF
)
config_option(
KernelClzllImpl CLZLL_IMPL
"Define a __clzti2 function to count leading zeros for unsigned long long arguments. \
KernelClz64 CLZ_64 "Define a __clzdi2 function to count leading zeros for uint64_t arguments. \
Only needed on platforms which lack a builtin instruction."
DEFAULT OFF
)
config_option(
KernelCtzlImpl CTZL_IMPL
"Define a __ctzdi2 function to count trailing zeros for unsigned long arguments. \
KernelCtz32 CTZ_32 "Define a __ctzsi2 function to count trailing zeros for uint32_t arguments. \
Only needed on platforms which lack a builtin instruction."
DEFAULT OFF
)
config_option(
KernelCtzllImpl CTZLL_IMPL
"Define a __ctzti2 function to count trailing zeros for unsigned long long arguments. \
KernelCtz64 CTZ_64 "Define a __ctzdi2 function to count trailing zeros for uint64_t arguments. \
Only needed on platforms which lack a builtin instruction."
DEFAULT OFF
)

20
include/util.h
View File

@@ -102,10 +102,10 @@ long PURE str_to_long(const char *str);
// GCC's builtins will emit calls to these functions when the platform
// does not provide suitable inline assembly.
// We only emit function definitions if CONFIG_CLZL_IMPL etc are set.
NO_INLINE CONST int __clzdi2(unsigned long x);
NO_INLINE CONST int __clzti2(unsigned long long x);
NO_INLINE CONST int __ctzdi2(unsigned long x);
NO_INLINE CONST int __ctzti2(unsigned long long x);
CONST int __clzsi2(uint32_t x);
CONST int __clzdi2(uint64_t x);
CONST int __ctzsi2(uint32_t x);
CONST int __ctzdi2(uint64_t x);
// Used for compile-time constants, so should always use the builtin.
#define CTZL(x) __builtin_ctzl(x)
@@ -133,7 +133,11 @@ static inline long
CONST clzl(unsigned long x)
{
#ifdef CONFIG_CLZ_NO_BUILTIN
#if CONFIG_WORD_SIZE == 32
return __clzsi2(x);
#else
return __clzdi2(x);
#endif
#else
return __builtin_clzl(x);
#endif
@@ -154,7 +158,7 @@ static inline long long
CONST clzll(unsigned long long x)
{
#ifdef CONFIG_CLZ_NO_BUILTIN
return __clzti2(x);
return __clzdi2(x);
#else
return __builtin_clzll(x);
#endif
@@ -181,7 +185,11 @@ CONST ctzl(unsigned long x)
// This is typically the fastest way to calculate ctzl on such platforms.
#ifdef CONFIG_CLZ_NO_BUILTIN
// Here, there are no builtins we can use, so call the library function.
#if CONFIG_WORD_SIZE == 32
return __ctzsi2(x);
#else
return __ctzdi2(x);
#endif
#else
// Here, we have __builtin_clzl, but no __builtin_ctzl.
if (unlikely(x == 0)) {
@@ -214,7 +222,7 @@ CONST ctzll(unsigned long long x)
#ifdef CONFIG_CTZ_NO_BUILTIN
// See comments on ctzl.
#ifdef CONFIG_CLZ_NO_BUILTIN
return __ctzti2(x);
return __ctzdi2(x);
#else
if (unlikely(x == 0)) {
return 8 * sizeof(unsigned long long);

17
src/arch/riscv/config.cmake
View File

@@ -28,14 +28,25 @@ config_option(
)
# Until RISC-V has instructions to count leading/trailing zeros, we provide
# library implementations.
# library implementations. Platforms that implement the bit manipulation
# extension can override these settings to remove the library functions from
# the image.
# In the verified configurations, we additionally define KernelClzNoBuiltin and
# KernelCtzNoBuiltin to expose the library implementations to verification.
# However, since the NoBuiltin options force the use of the library functions
# even when the platform has sutiable inline assembly, we do not make these the
# default.
set(KernelClzlImpl ON CACHE BOOL "")
set(KernelCtzlImpl ON CACHE BOOL "")
if(KernelWordSize EQUAL 32)
set(KernelClz32 ON CACHE BOOL "")
set(KernelCtz32 ON CACHE BOOL "")
if(KernelIsMCS)
# Used for long division in timer calculations.
set(KernelClz64 ON CACHE BOOL "")
endif()
elseif(KernelWordSize EQUAL 64)
set(KernelClz64 ON CACHE BOOL "")
set(KernelCtz64 ON CACHE BOOL "")
endif()
if(KernelSel4ArchRiscV32)
set(KernelPTLevels 2 CACHE STRING "" FORCE)

66
src/util.c
View File

@@ -162,11 +162,11 @@ long PURE str_to_long(const char *str)
// implementation. In any case, the compiler might convert this to a branching
// binary.
// Check some assumptions made by the CLZ and CTZ library functions:
// Check some assumptions made by the clzl, clzll, ctzl functions:
compile_assert(clz_ulong_32_or_64, sizeof(unsigned long) == 4 || sizeof(unsigned long) == 8);
compile_assert(clz_ullong_64, sizeof(unsigned long long) == 8);
compile_assert(clz_word_size, sizeof(unsigned long) * 8 == CONFIG_WORD_SIZE);
#ifdef CONFIG_CLZL_IMPL
// Count leading zeros.
// This implementation contains no branches. If the architecture provides an
// instruction to set a register to a boolean value on a comparison, then the
@@ -174,7 +174,11 @@ compile_assert(clz_ullong_64, sizeof(unsigned long long) == 8);
// preferable on architectures with deep pipelines, or when the maximum
// priority of runnable threads frequently varies. However, note that the
// compiler may choose to convert this to a branching implementation.
static CONST inline unsigned clz32(uint32_t x)
//
// These functions are potentially `UNUSED` because we want to always expose
// them to verification without necessarily linking them into the kernel
// binary.
static UNUSED CONST inline unsigned clz32(uint32_t x)
{
// Compiler builtins typically return int, but we use unsigned internally
// to reduce the number of guards we see in the proofs.
@@ -238,10 +242,8 @@ static CONST inline unsigned clz32(uint32_t x)
// count gives a result from [0, 1, 2, ..., 31].
return count - x;
}
#endif
#if defined(CONFIG_CLZL_IMPL) || defined (CONFIG_CLZLL_IMPL)
static CONST inline unsigned clz64(uint64_t x)
static UNUSED CONST inline unsigned clz64(uint64_t x)
{
unsigned count = 64;
uint64_t mask = UINT64_MAX;
@@ -295,26 +297,10 @@ static CONST inline unsigned clz64(uint64_t x)
return count - x;
}
#endif
#ifdef CONFIG_CLZL_IMPL
int __clzdi2(unsigned long x)
{
return sizeof(unsigned long) == 4 ? clz32(x) : clz64(x);
}
#endif
#ifdef CONFIG_CLZLL_IMPL
int __clzti2(unsigned long long x)
{
return clz64(x);
}
#endif
#ifdef CONFIG_CTZL_IMPL
// Count trailing zeros.
// See comments on clz32.
static CONST inline unsigned ctz32(uint32_t x)
static UNUSED CONST inline unsigned ctz32(uint32_t x)
{
unsigned count = (x == 0);
uint32_t mask = UINT32_MAX;
@@ -375,10 +361,8 @@ static CONST inline unsigned ctz32(uint32_t x)
return count;
}
#endif
#if defined(CONFIG_CTZL_IMPL) || defined (CONFIG_CTZLL_IMPL)
static CONST inline unsigned ctz64(uint64_t x)
static UNUSED CONST inline unsigned ctz64(uint64_t x)
{
unsigned count = (x == 0);
uint64_t mask = UINT64_MAX;
@@ -428,17 +412,35 @@ static CONST inline unsigned ctz64(uint64_t x)
return count;
}
#endif
#ifdef CONFIG_CTZL_IMPL
int __ctzdi2(unsigned long x)
// GCC's builtins will emit calls to these functions when the platform does
// not provide suitable inline assembly.
// These are only provided when the relevant config items are set.
// We define these separately from `ctz32` etc. so that we can verify all of
// `ctz32` etc. without necessarily linking them into the kernel binary.
#ifdef CONFIG_CLZ_32
CONST int __clzsi2(uint32_t x)
{
return sizeof(unsigned long) == 4 ? ctz32(x) : ctz64(x);
return clz32(x);
}
#endif
#ifdef CONFIG_CTZLL_IMPL
int __ctzti2(unsigned long long x)
#ifdef CONFIG_CLZ_64
CONST int __clzdi2(uint64_t x)
{
return clz64(x);
}
#endif
#ifdef CONFIG_CTZ_32
CONST int __ctzsi2(uint32_t x)
{
return ctz32(x);
}
#endif
#ifdef CONFIG_CTZ_64
CONST int __ctzdi2(uint64_t x)
{
return ctz64(x);
}