From 06f2d60e945568d91ff1d2fdd41c85c38fd7c365 Mon Sep 17 00:00:00 2001
From: Sam Leffler <sleffler@google.com>
Date: Sat, 13 Nov 2021 20:10:29 +0000
Subject: [PATCH] sel4-sys: fix seL4_BootInfo definitions

- do not pack struct's, the C code does not
- replace the explicit padding in seL4_UntypedDesc (which was wrong) with the rust alignment idiom
- correct initThreadCNodeSizeBits type
- add extended header defs

Change-Id: I4a3fcbe470dd0a18b3c9b1ccf8af9634076e89fb
GitOrigin-RevId: f99eeed563d2d430381f0ad1a5fbe096a13c68f0
---
 .../kata-os-common/src/sel4-sys/lib.rs        | 55 +++++++++++--------
 1 file changed, 33 insertions(+), 22 deletions(-)

diff --git a/apps/system/components/kata-os-common/src/sel4-sys/lib.rs b/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
index 8893ee2..a6922f0 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
@@ -238,7 +238,7 @@ pub const seL4_CapBootInfoFrame: seL4_Word = 9; // bootinfo frame
 pub const seL4_CapInitThreadIPCBuffer: seL4_Word = 10; // initial thread's IPC buffer frame
 pub const seL4_CapDomain: seL4_Word = 11; // global domain controller
 
-#[repr(C, packed)]
+#[repr(C)]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 /// A half-open [start..end) range of slots
 pub struct seL4_SlotRegion {
@@ -248,17 +248,19 @@ pub struct seL4_SlotRegion {
     pub end: seL4_Word, /* first CNode slot position AFTER region */
 }
 
-#[repr(C, packed)]
+// NB: C definition is not packed; this explicitly aligns to an
+// seL4_Word using the Rust idiom.
+#[repr(C)]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub struct seL4_UntypedDesc {
     /// Physical address corresponding of the untyped object's backing memory
     pub paddr: seL4_Word,
-    pub padding1: u8,
-    pub padding2: u8,
     /// log2 size of the region of memory backing the untyped object
     pub sizeBits: u8,
     /// Whether the backing memory corresponds to some device memory
     pub isDevice: u8,
+    // Align to seL4_Word
+    align: [seL4_Word; 0],
 }
 impl seL4_UntypedDesc {
     pub fn is_device(&self) -> bool { self.isDevice != 0 }
@@ -268,12 +270,12 @@ impl seL4_UntypedDesc {
 // explicitly *not* Copy. the array at the end is tricky to handle.
 // #[derive]` can't be used on a `#[repr(packed)]` struct that does not derive Copy (error E0133)
 
-#[repr(C, packed)]
+#[repr(C)]
 pub struct seL4_BootInfo {
     /// Length of any additional bootinfo information
     pub extraLen: seL4_Word,
     /// ID [0..numNodes-1] of the current node (0 if uniprocessor)
-    pub nodeID: seL4_Word,
+    pub nodeID: seL4_NodeId,
     /// Number of seL4 nodes (1 if uniprocessor)
     pub numNodes: seL4_Word,
     /// Number of IOMMU PT levels (0 if no IOMMU support)
@@ -293,9 +295,9 @@ pub struct seL4_BootInfo {
     /// Caps fr anypages used to back the additional bootinfo information
     pub extraBIPages: seL4_SlotRegion,
     /// log2 size of root task's CNode
-    pub initThreadCNodeSizeBits: u8,
+    pub initThreadCNodeSizeBits: seL4_Word,
     /// Root task's domain ID
-    pub initThreadDomain: u32,
+    pub initThreadDomain: seL4_Domain,
 
     #[cfg(feature = "SEL4_CONFIG_KERNEL_MCS")]
     // Caps to sched_control for each node
@@ -305,20 +307,11 @@ pub struct seL4_BootInfo {
     pub untyped: seL4_SlotRegion,
     /// Information about each untyped cap
     ///
-    /// *Note*! This is actually an array! The actual length depends on kernel configuration which
-    /// we have no way of knowing at this point. Use the `untyped_descs` method.
-    pub untypedList: seL4_UntypedDesc,
+    /// *Note*! The actual length depends on kernel configuration that is
+    /// unavailable at compile time. Use the `untyped_descs` method to get
+    /// access to the descriptors.
+    pub untypedList: [seL4_UntypedDesc; 1],
 }
-
-#[repr(C, packed)]
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub struct seL4_BootInfoHeader {
-    /// Identifier of the following chunk
-    pub id: seL4_Word,
-    /// Length of the chunk
-    pub len: seL4_Word,
-}
-
 impl seL4_BootInfo {
     /// This is safe if you don't mutate the `untyped` field and corrupt its length.
     pub unsafe fn untyped_descs(&self) -> &[seL4_UntypedDesc] {
@@ -328,6 +321,24 @@ impl seL4_BootInfo {
             len <= (4096 - size_of::<seL4_BootInfo>() + size_of::<seL4_UntypedDesc>())
                 / size_of::<seL4_UntypedDesc>()
         );
-        core::slice::from_raw_parts(&self.untypedList, len)
+        core::slice::from_raw_parts(&self.untypedList[0], len)
     }
 }
+
+#[repr(C)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub struct seL4_BootInfoHeader {
+    /// Identifier of the following chunk
+    pub id: seL4_Word,
+    /// Length of the chunk
+    pub len: seL4_Word,
+}
+
+pub const SEL4_BOOTINFO_HEADER_PADDING: usize = 0;
+pub const SEL4_BOOTINFO_HEADER_X86_VBE: usize = 1;
+pub const SEL4_BOOTINFO_HEADER_X86_MBMMAP: usize = 2;
+pub const SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP: usize = 3;
+pub const SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER: usize = 4;
+pub const SEL4_BOOTINFO_HEADER_X86_TSC_FREQ: usize = 5;
+pub const SEL4_BOOTINFO_HEADER_FDT: usize = 6;
+pub const SEL4_BOOTINFO_HEADER_NUM: usize = SEL4_BOOTINFO_HEADER_FDT + 1;