[patch-axel-18] CMake stuff and QEMU stuff

.cmake-format.yaml

@@ -40,6 +40,12 @@ additional_commands:
     kwargs:
       CFILES: '*'
       PREFIX: '*'
+  find_in_map:
+    kwargs:
+      RESULT_VAR: '1'
+      KEY_VAR: '1'
+      DEFAULT: '1'
+      MAP: '1+'
   declare_default_headers:
     kwargs:
         TIMER_FREQUENCY: '*'

CMakeLists.txt

@@ -184,6 +184,9 @@ add_compile_options(
     -Wundef
     -Wpointer-arith
     -Wno-nonnull
+    -Wshadow
+    -Wconversion
+    -Wformat
     #-----------------------------------
     # Configure compiler settings.
     #-----------------------------------

config.cmake

@@ -129,15 +129,13 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
             "Provide an additional list of overlays to append to the selected KernelPlatform's \
         device tree during build time"
     )
-    if(NOT "${KernelCustomDTSOverlay}" STREQUAL "")
-        foreach(dts_entry IN ITEMS ${KernelCustomDTSOverlay})
-            if(NOT EXISTS ${dts_entry})
-                message(FATAL_ERROR "Can't open external overlay file '${dts_entry}'!")
-            endif()
-            list(APPEND KernelDTSList "${dts_entry}")
-            message(STATUS "Appending ${dts_entry} overlay")
-        endforeach()
-    endif()
+    foreach(dts_entry IN LISTS KernelCustomDTSOverlay)
+        if(NOT EXISTS ${dts_entry})
+            message(FATAL_ERROR "Can't open external overlay file '${dts_entry}'!")
+        endif()
+        list(APPEND KernelDTSList "${dts_entry}")
+        message(STATUS "Appending ${dts_entry} overlay")
+    endforeach()
 
     find_program(DTC_TOOL dtc)
     if("${DTC_TOOL}" STREQUAL "DTC_TOOL-NOTFOUND")
@@ -149,15 +147,15 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
     endif()
     mark_as_advanced(DTC_TOOL STAT_TOOL)
     # Generate final DTS based on Linux DTS + seL4 overlay[s]
-    foreach(entry ${KernelDTSList})
+    foreach(entry IN LISTS KernelDTSList)
         get_absolute_source_or_binary(dts_tmp ${entry})
         list(APPEND dts_list "${dts_tmp}")
     endforeach()
 
     check_outfile_stale(regen ${KernelDTBPath} dts_list ${CMAKE_CURRENT_BINARY_DIR}/dts.cmd)
     if(regen)
         file(REMOVE "${KernelDTSIntermediate}")
-        foreach(entry ${dts_list})
+        foreach(entry IN LISTS dts_list)
             file(READ ${entry} CONTENTS)
             file(APPEND "${KernelDTSIntermediate}" "${CONTENTS}")
         endforeach()

configs/seL4Config.cmake

@@ -170,20 +170,15 @@ foreach(file ${result})
     include("${file}")
 endforeach()
 
-# Verify that, as a minimum any variables that are used
-# to find other build files are actually defined at this
-# point. This means at least: KernelArch KernelWordSize
-
-if("${KernelArch}" STREQUAL "")
-    message(FATAL_ERROR "Variable 'KernelArch' is not set.")
-endif()
-
-if("${KernelWordSize}" STREQUAL "")
-    message(FATAL_ERROR "Variable 'KernelWordSize' is not set.")
-endif()
-
 config_choice(KernelPlatform PLAT "Select the platform" ${kernel_platforms})
 
+# Verify that a proper minimal configuration has been selected.
+foreach(var IN ITEMS KernelPlatform KernelSel4Arch KernelArch KernelWordSize)
+    if (NOT ${var})
+        message(FATAL_ERROR "Variable '${var}' is not set.")
+    endif()
+endforeach()
+
 # Now enshrine all the common variables in the config
 config_set(KernelArmCortexA7 ARM_CORTEX_A7 "${KernelArmCortexA7}")
 config_set(KernelArmCortexA8 ARM_CORTEX_A8 "${KernelArmCortexA8}")

include/arch/riscv/arch/sbi.h

@@ -55,14 +55,14 @@ static inline word_t sbi_call(word_t cmd,
                               word_t arg_1,
                               word_t arg_2)
 {
-    register word_t a0 asm("a0") = arg_0;
-    register word_t a1 asm("a1") = arg_1;
-    register word_t a2 asm("a2") = arg_2;
-    register word_t a7 asm("a7") = cmd;
+    register word_t reg_a0 asm("a0") = arg_0;
+    register word_t reg_a1 asm("a1") = arg_1;
+    register word_t reg_a2 asm("a2") = arg_2;
+    register word_t reg_a7 asm("a7") = cmd;
     register word_t result asm("a0");
     asm volatile("ecall"
                  : "=r"(result)
-                 : "r"(a0), "r"(a1), "r"(a2), "r"(a7)
+                 : "r"(reg_a0), "r"(reg_a1), "r"(reg_a2), "r"(reg_a7)
                  : "memory");
     return result;
 }

include/arch/x86/arch/kernel/cmdline.h

@@ -16,5 +16,5 @@ typedef struct cmdline_opt {
     bool_t   disable_iommu;
 } cmdline_opt_t;
 
-void cmdline_parse(const char *cmdline, cmdline_opt_t *cmdline_opt);
+void cmdline_parse(const char *cmdline, cmdline_opt_t *opt);
 

src/arch/riscv/kernel/vspace.c

@@ -1164,15 +1164,15 @@ void Arch_userStackTrace(tcb_t *tptr)
         return;
     }
 
-    word_t sp = getRegister(tptr, SP);
-    if (!IS_ALIGNED(sp, seL4_WordSizeBits)) {
-        printf("SP %p not aligned", (void *) sp);
+    word_t reg_sp = getRegister(tptr, SP);
+    if (!IS_ALIGNED(reg_sp, seL4_WordSizeBits)) {
+        printf("SP %p not aligned", (void *) reg_sp);
         return;
     }
 
     pte_t *vspace_root = PTE_PTR(pptr_of_cap(threadRoot));
     for (int i = 0; i < CONFIG_USER_STACK_TRACE_LENGTH; i++) {
-        word_t address = sp + (i * sizeof(word_t));
+        word_t address = reg_sp + (i * sizeof(word_t));
         lookupPTSlot_ret_t ret = lookupPTSlot(vspace_root, address);
         if (pte_ptr_get_valid(ret.ptSlot) && !isPTEPageTable(ret.ptSlot)) {
             pptr_t pptr = (pptr_t)(getPPtrFromHWPTE(ret.ptSlot));

src/arch/x86/kernel/boot_sys.c

@@ -54,7 +54,7 @@ boot_state_t boot_state;
 /* global variables (not covered by abstract specification) */
 
 BOOT_BSS
-cmdline_opt_t cmdline_opt;
+static cmdline_opt_t cmdline_opt;
 
 /* functions not modeled in abstract specification */
 

src/arch/x86/kernel/cmdline.c

@@ -103,7 +103,7 @@ static void UNUSED parse_uint16_array(char *str, uint16_t *array, int array_size
     }
 }
 
-void cmdline_parse(const char *cmdline, cmdline_opt_t *cmdline_opt)
+void cmdline_parse(const char *cmdline, cmdline_opt_t *opt)
 {
 #if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD)
     /* use BIOS data area to read serial configuration. The BDA is not
@@ -125,42 +125,42 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t *cmdline_opt)
 
 #ifdef CONFIG_PRINTING
     /* initialise to default or use BDA if available */
-    cmdline_opt->console_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8;
+    opt->console_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8;
 
     if (parse_opt(cmdline, "console_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
-        parse_uint16_array(cmdline_val, &cmdline_opt->console_port, 1);
+        parse_uint16_array(cmdline_val, &opt->console_port, 1);
     }
 
     /* initialise console ports to enable debug output */
-    if (cmdline_opt->console_port) {
-        serial_init(cmdline_opt->console_port);
-        x86KSconsolePort = cmdline_opt->console_port;
+    if (opt->console_port) {
+        serial_init(opt->console_port);
+        x86KSconsolePort = opt->console_port;
     }
 
     /* only start printing here after having parsed/set/initialised the console_port */
     printf("\nBoot config: parsing cmdline '%s'\n", cmdline);
 
-    if (cmdline_opt->console_port) {
-        printf("Boot config: console_port = 0x%x\n", cmdline_opt->console_port);
+    if (opt->console_port) {
+        printf("Boot config: console_port = 0x%x\n", opt->console_port);
     }
 #endif
 
 #if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD)
     /* initialise to default or use BDA if available */
-    cmdline_opt->debug_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8;
+    opt->debug_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8;
     if (parse_opt(cmdline, "debug_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
-        parse_uint16_array(cmdline_val, &cmdline_opt->debug_port, 1);
+        parse_uint16_array(cmdline_val, &opt->debug_port, 1);
     }
 
     /* initialise debug ports */
-    if (cmdline_opt->debug_port) {
-        serial_init(cmdline_opt->debug_port);
-        x86KSdebugPort = cmdline_opt->debug_port;
-        printf("Boot config: debug_port = 0x%x\n", cmdline_opt->debug_port);
+    if (opt->debug_port) {
+        serial_init(opt->debug_port);
+        x86KSdebugPort = opt->debug_port;
+        printf("Boot config: debug_port = 0x%x\n", opt->debug_port);
     }
 #pragma GCC diagnostic pop
 #endif
 
-    cmdline_opt->disable_iommu = parse_bool(cmdline, cmdline_str_disable_iommu);
-    printf("Boot config: disable_iommu = %s\n", cmdline_opt->disable_iommu ? "true" : "false");
+    opt->disable_iommu = parse_bool(cmdline, cmdline_str_disable_iommu);
+    printf("Boot config: disable_iommu = %s\n", opt->disable_iommu ? "true" : "false");
 }

src/kernel/boot.c

@@ -889,13 +889,13 @@ BOOT_CODE static bool_t check_available_memory(word_t n_available,
 
 
 BOOT_CODE static bool_t check_reserved_memory(word_t n_reserved,
-                                              const region_t *reserved)
+                                              const region_t *regs)
 {
     printf("reserved virt address space regions: %"SEL4_PRIu_word"\n",
            n_reserved);
     /* Force ordering and exclusivity of reserved regions. */
     for (word_t i = 0; i < n_reserved; i++) {
-        const region_t *r = &reserved[i];
+        const region_t *r = &regs[i];
         printf("  [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end);
 
         /* Reserved regions must be sane, the size is allowed to be zero. */
@@ -906,7 +906,7 @@ BOOT_CODE static bool_t check_reserved_memory(word_t n_reserved,
 
         /* Regions must be ordered and must not overlap. Regions are [start..end),
            so the == case is fine. Directly adjacent regions are allowed. */
-        if ((i > 0) && (r->start < reserved[i - 1].end)) {
+        if ((i > 0) && (r->start < regs[i - 1].end)) {
             printf("ERROR: reserved region %"SEL4_PRIu_word" in wrong order\n", i);
             return false;
         }
@@ -922,16 +922,16 @@ BOOT_BSS static region_t avail_reg[MAX_NUM_FREEMEM_REG];
  * Dynamically initialise the available memory on the platform.
  * A region represents an area of memory.
  */
-BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
-                              word_t n_reserved, const region_t *reserved,
+BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *regs_available,
+                              word_t n_reserved, const region_t *regs_reserved,
                               v_region_t it_v_reg, word_t extra_bi_size_bits)
 {
 
-    if (!check_available_memory(n_available, available)) {
+    if (!check_available_memory(n_available, regs_available)) {
         return false;
     }
 
-    if (!check_reserved_memory(n_reserved, reserved)) {
+    if (!check_reserved_memory(n_reserved, regs_reserved)) {
         return false;
     }
 
@@ -941,7 +941,7 @@ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
 
     /* convert the available regions to pptrs */
     for (word_t i = 0; i < n_available; i++) {
-        avail_reg[i] = paddr_to_pptr_reg(available[i]);
+        avail_reg[i] = paddr_to_pptr_reg(regs_available[i]);
         avail_reg[i].end = ceiling_kernel_window(avail_reg[i].end);
         avail_reg[i].start = ceiling_kernel_window(avail_reg[i].start);
     }
@@ -950,38 +950,38 @@ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
     word_t r = 0;
     /* Now iterate through the available regions, removing any reserved regions. */
     while (a < n_available && r < n_reserved) {
-        if (reserved[r].start == reserved[r].end) {
+        if (regs_reserved[r].start == regs_reserved[r].end) {
             /* reserved region is empty - skip it */
             r++;
         } else if (avail_reg[a].start >= avail_reg[a].end) {
             /* skip the entire region - it's empty now after trimming */
             a++;
-        } else if (reserved[r].end <= avail_reg[a].start) {
+        } else if (regs_reserved[r].end <= avail_reg[a].start) {
             /* the reserved region is below the available region - skip it */
-            reserve_region(pptr_to_paddr_reg(reserved[r]));
+            reserve_region(pptr_to_paddr_reg(regs_reserved[r]));
             r++;
-        } else if (reserved[r].start >= avail_reg[a].end) {
+        } else if (regs_reserved[r].start >= avail_reg[a].end) {
             /* the reserved region is above the available region - take the whole thing */
             insert_region(avail_reg[a]);
             a++;
         } else {
             /* the reserved region overlaps with the available region */
-            if (reserved[r].start <= avail_reg[a].start) {
+            if (regs_reserved[r].start <= avail_reg[a].start) {
                 /* the region overlaps with the start of the available region.
                  * trim start of the available region */
-                avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end);
-                reserve_region(pptr_to_paddr_reg(reserved[r]));
+                avail_reg[a].start = MIN(avail_reg[a].end, regs_reserved[r].end);
+                reserve_region(pptr_to_paddr_reg(regs_reserved[r]));
                 r++;
             } else {
-                assert(reserved[r].start < avail_reg[a].end);
+                assert(regs_reserved[r].start < avail_reg[a].end);
                 /* take the first chunk of the available region and move
                  * the start to the end of the reserved region */
                 region_t m = avail_reg[a];
-                m.end = reserved[r].start;
+                m.end = regs_reserved[r].start;
                 insert_region(m);
-                if (avail_reg[a].end > reserved[r].end) {
-                    avail_reg[a].start = reserved[r].end;
-                    reserve_region(pptr_to_paddr_reg(reserved[r]));
+                if (avail_reg[a].end > regs_reserved[r].end) {
+                    avail_reg[a].start = regs_reserved[r].end;
+                    reserve_region(pptr_to_paddr_reg(regs_reserved[r]));
                     r++;
                 } else {
                     a++;
@@ -991,8 +991,8 @@ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available,
     }
 
     for (; r < n_reserved; r++) {
-        if (reserved[r].start < reserved[r].end) {
-            reserve_region(pptr_to_paddr_reg(reserved[r]));
+        if (regs_reserved[r].start < regs_reserved[r].end) {
+            reserve_region(pptr_to_paddr_reg(regs_reserved[r]));
         }
     }