cmake: make calculation arch specific

- KernelMaxNumNodes is always defined, it's at lest 1
- CONFIGURE_NUM_PPI might be defined

Signed-off-by: Axel Heider <[email protected]>

config.cmake

@@ -51,15 +51,19 @@ if(DEFINED CALLED_declare_default_headers)
     # calculate the irq cnode size based on MAX_NUM_IRQ
     if(KernelArchRiscV)
         math(EXPR MAX_NUM_IRQ "${CONFIGURE_PLIC_MAX_NUM_INT} + 2")
-    else()
-        if(DEFINED KernelMaxNumNodes AND CONFIGURE_NUM_PPI GREATER "0" AND KernelArchARM)
+    elseif(KernelArchARM)
+        set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
+        if(DEFINED CONFIGURE_NUM_PPI)
+            # The PPIs are a part of CONFIGURE_MAX_IRQ, but they are separate
+            # for each core.
             math(
                 EXPR MAX_NUM_IRQ
-                "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
+                "${MAX_NUM_IRQ} + ((${KernelMaxNumNodes} - 1) * ${CONFIGURE_NUM_PPI})"
             )
-        else()
-            set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
         endif()
+    else()
+        # Don't make any assumption about other architectures.
+        message(FATAL_ERROR "unsupported architecture: '${KernelArch}'")
     endif()
     set(BITS "0")
     while(MAX_NUM_IRQ GREATER "0")

configs/seL4Config.cmake

@@ -124,6 +124,19 @@ macro(declare_default_headers)
         ""
         ${ARGN}
     )
+
+    if(NOT KernelArchARM AND DEFINED CONFIGURE_NUM_PPI)
+        message(FATAL_ERROR "NUM_PPI is for ARM only")
+    endif()
+
+    if(KernelArchRiscV)
+        if(DEFINED CONFIGURE_MAX_IRQ)
+            message(FATAL_ERROR "Use PLIC_MAX_NUM_INT instead MAX_IRQ on RISC-V")
+        endif()
+    elseif(DEFINED CONFIGURE_PLIC_MAX_NUM_INT)
+        message(FATAL_ERROR "PLIC_MAX_NUM_INT is for RISC-V only")
+    endif()
+
     set(CALLED_declare_default_headers 1)
 endmacro()