KernelFWholeProgram=On

CMakeLists.txt

@@ -250,10 +250,13 @@ endif()
 
 if(KernelFWholeProgram)
     # KernelFWholeProgram is still an experimental feature and disabled by
-    # default. Clarify if the linker step via GCC actually cares about this
-    # parameter. There are also the options -flto and -fuse-linker-plugin that
-    # might be a more modern approach.
-    KernelCommonFlags(-fwhole-program)
+    # default. The option is supported by GCC only, not by Clang. Clarify if the
+    # linker step via GCC actually cares about this parameter. There are also
+    # the options -flto and -fuse-linker-plugin that might be a more modern
+    # approach.
+    if(CMAKE_C_COMPILER_ID STREQUAL "GNU")
+        KernelCommonFlags(-fwhole-program)
+    endif()
 endif()
 
 if(KernelDebugBuild)

config.cmake

@@ -511,7 +511,7 @@ config_option(
     KernelFWholeProgram KERNEL_FWHOLE_PROGRAM
     "Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which \
     are not uncommon with -fwhole-program. Consider this feature experimental!"
-    DEFAULT OFF
+    DEFAULT ON
     DEPENDS "NOT KernelBinaryVerificationBuild"
 )
 

include/util.h

@@ -148,10 +148,9 @@ long PURE str_to_long(const char *str);
  * the implementation choices for the sizes of `unsigned int`. Instead, it
  * appears that `si` always signifies a 32-bit argument and `di` always
  * signifies a 64-bit argument. Tests with __builtin_clzl() on RISC-V have shown
- * that if 'unsigned long' is 32 bits __builtin_clzl() uses __clzsi2() and if
- * the type is 64 bits __builtin_clzl() uses __clzdi2(). Thus using the types
- * uint32_t and uint64_t from stdint.h in the signatures below is considered the
- * semantically correct way.
+ * than __clzsi2() is used if 'unsigned long' is 32 bits, and __clzdi2() if it
+ * is 64 bits.. Thus, using the types uint32_t and uint64_t from stdint.h in the
+ * signatures below is considered the semantically correct way.
  * Note that we only emit actual function implementations for these functions if
  * CONFIG_CLZ_32 etc. are set. Otherwise, the compiler's internal implementation
  * may get used or compilation fails if there is no machine instruction.

src/arch/riscv/config.cmake

@@ -59,6 +59,12 @@ elseif(KernelWordSize EQUAL 64)
     set(KernelCtz64 ON CACHE BOOL "")
 endif()
 
+message("KernelClz32: ${KernelClz32}")
+message("KernelCtz32: ${KernelCtz32}")
+message("KernelClz64: ${KernelClz64}")
+message("KernelCtz64: ${KernelCtz64}")
+
+
 if(KernelSel4ArchRiscV32)
     set(KernelPTLevels 2 CACHE STRING "" FORCE)
 endif()

src/util.c

@@ -178,11 +178,11 @@ compile_assert(clz_word_size, sizeof(unsigned long) * 8 == CONFIG_WORD_SIZE);
 // 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)
+static inline CONST int 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.
-    unsigned count = 32;
+    unsigned int count = 32;
     uint32_t mask = UINT32_MAX;
 
     // Each iteration i (counting backwards) considers the least significant
@@ -243,9 +243,9 @@ static UNUSED CONST inline unsigned clz32(uint32_t x)
     return count - x;
 }
 
-static UNUSED CONST inline unsigned clz64(uint64_t x)
+static inline CONST unsigned int clz64(uint64_t x)
 {
-    unsigned count = 64;
+    unsigned int count = 64;
     uint64_t mask = UINT64_MAX;
 
     // Although we could implement this using clz32, we spell out the
@@ -300,9 +300,9 @@ static UNUSED CONST inline unsigned clz64(uint64_t x)
 
 // Count trailing zeros.
 // See comments on clz32.
-static UNUSED CONST inline unsigned ctz32(uint32_t x)
+static inline CONST unsigned int ctz32(uint32_t x)
 {
-    unsigned count = (x == 0);
+    unsigned int count = (x == 0);
     uint32_t mask = UINT32_MAX;
 
     // Each iteration i (counting backwards) considers the least significant
@@ -362,9 +362,9 @@ static UNUSED CONST inline unsigned ctz32(uint32_t x)
     return count;
 }
 
-static UNUSED CONST inline unsigned ctz64(uint64_t x)
+static inline CONST unsigned int ctz64(uint64_t x)
 {
-    unsigned count = (x == 0);
+    unsigned int count = (x == 0);
     uint64_t mask = UINT64_MAX;
 
     if (1) {
@@ -413,35 +413,76 @@ static UNUSED CONST inline unsigned ctz64(uint64_t x)
     return count;
 }
 
-// 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.
+//
+// /usr/bin/riscv64-unknown-elf-gcc
+//    --sysroot=/home/codasip.com/axel.heider/projects/cheri/hobgoblin/build-sel4_hello_world-qemu-riscv-virt
+//    -D__KERNEL_64__
+//    -march=rv64imac
+//    -mabi=lp64
+//    -O2
+//    -g
+//    -DNDEBUG
+//    -D__KERNEL_64__
+//    -march=rv64imac
+//    -mabi=lp64
+//    -static
+//    -Wl,--build-id=none
+//    -Wl,-n
+//    -O2
+//    -nostdlib
+//    -fno-pic
+//    -fno-pie
+//    -fwhole-program
+//    -DDEBUG
+//    -g
+//    -ggdb
+//    -mcmodel=medany
+//    -msmall-data-limit=1024
+//    -Wl,-T /home/codasip.com/axel.heider/projects/cheri/hobgoblin/build-sel4_hello_world-qemu-riscv-virt/kernel/linker.lds_pp
+//    kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj
+//    kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/traps.S.obj
+//    kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
+//    -o kernel/kernel.elf
+//
+
+// The compiler 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. Explicitly using 'VISIBLE' is required for
+// CONFIG_KERNEL_FWHOLE_PROGRAM, otherwise the symbols are removed due to
+// inlining, which leads to linking failures evenutally.
+
+#if defined(CONFIG_KERNEL_FWHOLE_PROGRAM) && !defined(__clang__)
+#define CxZxi2_VISIBLE  VISIBLE
+#else
+#define CxZxi2_VISIBLE
+#endif
+
 #ifdef CONFIG_CLZ_32
-CONST int __clzsi2(uint32_t x)
+CONST int CxZxi2_VISIBLE __clzsi2(uint32_t x)
 {
-    return clz32(x);
+    return (int)clz32(x);
 }
 #endif
 
 #ifdef CONFIG_CLZ_64
-CONST int __clzdi2(uint64_t x)
+CONST int CxZxi2_VISIBLE __clzdi2(uint64_t x)
 {
-    return clz64(x);
+    return (int)clz64(x);
 }
 #endif
 
 #ifdef CONFIG_CTZ_32
-CONST int __ctzsi2(uint32_t x)
+CONST int CxZxi2_VISIBLE __ctzsi2(uint32_t x)
 {
-    return ctz32(x);
+    return (int)ctz32(x);
 }
 #endif
 
 #ifdef CONFIG_CTZ_64
-CONST int __ctzdi2(uint64_t x)
+CONST int CxZxi2_VISIBLE __ctzdi2(uint64_t x)
 {
-    return ctz64(x);
+    return (int)ctz64(x);
 }
 #endif