Merge "processmanger: fix release builds"

GitOrigin-RevId: 18bd5b9b85ab3b264c5816327d34b0ba3d645204

apps/system/components/DebugConsole/kata-shell/Cargo.toml

@@ -3,6 +3,17 @@ name = "kata-shell"
 version = "0.1.0"
 authors = ["Matt Harvey <mattharvey@google.com>"]
 edition = "2018"
+build = "build.rs"
+
+[build-dependencies]
+sel4-config = { path = "../../kata-os-common/src/sel4-config" }
+
+[build-env]
+SEL4_OUT_DIR = "${ROOTDIR}out/kata/kernel"
+
+[features]
+default = []
+CONFIG_DEBUG_BUILD = []
 
 [dependencies]
 crc = { version = "1.4.0", default_features = false }

apps/system/components/DebugConsole/kata-shell/build.rs

@@ -0,0 +1,21 @@
+//extern crate sel4_config;
+use std::env;
+
+fn main() {
+    // If SEL4_OUT_DIR is not set we expect the kernel build at a fixed
+    // location relative to the ROOTDIR env variable.
+    println!("SEL4_OUT_DIR {:?}", env::var("SEL4_OUT_DIR"));
+    let sel4_out_dir = env::var("SEL4_OUT_DIR").unwrap_or_else(
+        |_| format!("{}/out/kata/kernel", env::var("ROOTDIR").unwrap())
+    );
+    println!("sel4_out_dir {}", sel4_out_dir);
+
+    // Dredge seL4 kernel config for settings we need as features to generate
+    // correct code: e.g. CONFIG_KERNEL_MCS enables MCS support which changes
+    // the system call numbering.
+    let features = sel4_config::get_sel4_features(&sel4_out_dir);
+    println!("features={:?}", features);
+    for feature in features {
+        println!("cargo:rustc-cfg=feature=\"{}\"", feature);
+    }
+}

apps/system/components/DebugConsole/kata-shell/src/lib.rs

@@ -10,7 +10,6 @@ use log;
 
 use kata_io as io;
 use kata_line_reader::LineReader;
-use kata_os_common::sel4_sys::seL4_DebugDumpScheduler;
 use kata_proc_interface::kata_pkg_mgmt_install;
 use kata_proc_interface::kata_pkg_mgmt_uninstall;
 use kata_proc_interface::kata_proc_ctrl_get_running_bundles;
@@ -110,7 +109,7 @@ fn dispatch_command(cmdline: &str, input: &mut dyn io::BufRead, output: &mut dyn
                 "install" => install_command(&mut args, output),
                 "loglevel" => loglevel_command(&mut args, output),
                 "rz" => rz_command(input, output),
-                "ps" => ps_command(),
+                "ps" => ps_command(output),
                 "scecho" => scecho_command(cmdline, output),
                 "start" => start_command(&mut args, output),
                 "stop" => stop_command(&mut args, output),
@@ -214,13 +213,19 @@ fn rz_command(
 }
 
 /// Implements a "ps" command that dumps seL4 scheduler state to the console.
-fn ps_command() -> Result<(), CommandError> {
+#[cfg(feature = "CONFIG_DEBUG_BUILD")]
+fn ps_command(_output: &mut dyn io::Write) -> Result<(), CommandError> {
     unsafe {
-        seL4_DebugDumpScheduler();
+        kata_os_common::sel4_sys::seL4_DebugDumpScheduler();
     }
     Ok(())
 }
 
+#[cfg(not(feature = "CONFIG_DEBUG_BUILD"))]
+fn ps_command(output: &mut dyn io::Write) -> Result<(), CommandError> {
+    Ok(writeln!(output, "Kernel support not configured!")?)
+}
+
 /// Implements a binary float addition command.
 ///
 /// This is a toy to demonstrate that the CLI can operate on some very basic

apps/system/components/OpenTitanUARTDriver/src/driver.c

@@ -7,6 +7,7 @@
  * SPDX-License-Identifier: Apache-2.0
  */
 
+#include <assert.h>
 #include <camkes.h>
 #include <sel4/syscalls.h>
 #include <stdbool.h>
@@ -17,6 +18,13 @@
 #include "opentitan/uart.h"
 #include "uart_driver_error.h"
 
+// NB: KATA_ASSERTs preserve expr when not checking
+#ifdef CONFIG_DEBUG_BUILD
+#define KATA_ASSERT(expr) assert(expr)
+#else
+#define KATA_ASSERT(expr) ((void)(expr))
+#endif
+
 // Referenced by macros in the generated file opentitan/uart.h.
 #define UART0_BASE_ADDR (void *)mmio_region
 
@@ -47,8 +55,8 @@
   ((value & UART_##regname##_##subfield##_MASK)     \
    << UART_##regname##_##subfield##_OFFSET)
 
-#define LOCK(lockname) seL4_Assert(lockname##_lock() == 0)
-#define UNLOCK(lockname) seL4_Assert(lockname##_unlock() == 0)
+#define LOCK(lockname) KATA_ASSERT(lockname##_lock() == 0)
+#define UNLOCK(lockname) KATA_ASSERT(lockname##_unlock() == 0)
 #define ASSERT_OR_RETURN(x)            \
   if (!(bool)(x)) {                    \
     return UARTDriver_AssertionFailed; \
@@ -117,10 +125,10 @@ void pre_init() {
 
   // Computes NCO value corresponding to baud rate.
   // nco = 2^20 * baud / fclk  (assuming NCO width is 16-bit)
-  seL4_CompileTimeAssert(UART_CTRL_NCO_MASK == 0xffff);
+  compile_time_assert(NCO, UART_CTRL_NCO_MASK == 0xffff);
   uint64_t baud = 115200ull;
   uint64_t ctrl_nco = ((uint64_t)baud << 20) / CLK_FIXED_FREQ_HZ;
-  seL4_Assert(ctrl_nco < 0xffff);
+  assert(ctrl_nco < 0xffff);
 
   // Sets baud rate and enables TX and RX.
   REG(CTRL) = MASK_AND_SHIFT_UP(ctrl_nco, CTRL, NCO) | BIT(UART_CTRL_TX) |
@@ -178,13 +186,13 @@ int read_read(size_t limit) {
   LOCK(rx_mutex);
   while (circular_buffer_empty(&rx_buf)) {
     UNLOCK(rx_mutex);
-    seL4_Assert(rx_nonempty_semaphore_wait() == 0);
+    KATA_ASSERT(rx_nonempty_semaphore_wait() == 0);
     LOCK(rx_mutex);
   }
   while (cursor < cursor_limit) {
     if (!circular_buffer_pop_front(&rx_buf, cursor)) {
       // The buffer is empty.
-      seL4_Assert(rx_empty_semaphore_post() == 0);
+      KATA_ASSERT(rx_empty_semaphore_post() == 0);
       break;
     }
     ++cursor;
@@ -256,7 +264,7 @@ void tx_watermark_handle(void) {
   // flushed out.
   REG(INTR_STATE) = BIT(UART_INTR_STATE_TX_WATERMARK);
 
-  seL4_Assert(tx_watermark_acknowledge() == 0);
+  KATA_ASSERT(tx_watermark_acknowledge() == 0);
 }
 
 // Handles an rx_watermark interrupt.
@@ -274,20 +282,20 @@ void rx_watermark_handle(void) {
       // RX FIFO is empty, since the rx_watermark interrupt will not fire again
       // until the RX FIFO level crosses from 0 to 1. Therefore we unblock any
       // pending reads and wait for enough reads to consume all of rx_buf.
-      seL4_Assert(rx_nonempty_semaphore_post() == 0);
+      KATA_ASSERT(rx_nonempty_semaphore_post() == 0);
       UNLOCK(rx_mutex);
-      seL4_Assert(rx_empty_semaphore_wait() == 0);
+      KATA_ASSERT(rx_empty_semaphore_wait() == 0);
       LOCK(rx_mutex);
       continue;
     }
-    seL4_Assert(circular_buffer_push_back(&rx_buf, uart_getchar()));
+    KATA_ASSERT(circular_buffer_push_back(&rx_buf, uart_getchar()));
   }
-  seL4_Assert(rx_nonempty_semaphore_post() == 0);
+  KATA_ASSERT(rx_nonempty_semaphore_post() == 0);
   UNLOCK(rx_mutex);
 
   // Clears INTR_STATE for rx_watermark. (INTR_STATE is write-1-to-clear.)
   REG(INTR_STATE) = BIT(UART_INTR_STATE_RX_WATERMARK);
-  seL4_Assert(rx_watermark_acknowledge() == 0);
+  KATA_ASSERT(rx_watermark_acknowledge() == 0);
 }
 
 // Handles a tx_empty interrupt.
@@ -307,5 +315,5 @@ void tx_empty_handle(void) {
     REG(INTR_STATE) = BIT(UART_INTR_STATE_TX_EMPTY);
   }
   UNLOCK(tx_mutex);
-  seL4_Assert(tx_empty_acknowledge() == 0);
+  KATA_ASSERT(tx_empty_acknowledge() == 0);
 }

easy-settings.cmake

@@ -3,6 +3,7 @@ set(CAMKES_APP "system" CACHE STRING "The one and only CAmkES application in thi
 set(PLATFORM "sparrow" CACHE STRING "The one and only seL4 platform for Sparrow")
 set(KernelSel4Arch "riscv32" CACHE STRING "Specifies 32-bit branch of the seL4 spike platform")
 set(KernelIsMCS ON CACHE BOOL "Enable seL4 MCS support")
+set(KernelPrinting ON CACHE BOOL "Enable seL4 console output support")
 
 set(LibUtilsDefaultZfLogLevel 5 CACHE STRING "seL4 internal logging level (0-5).")
 set(SIMULATION ON CACHE BOOL "Whether to build simulate script")