github/sparrow-kata-full
1
0
Fork 0
mirror of https://github.com/AmbiML/sparrow-kata-full.git synced 2025-07-14 22:44:13 +00:00
Code Issues Projects Releases Wiki Activity

kata-os-common: improve portability & fix aarch64 platform

Browse Source 
A smorgasbord of chnages to sel4-sys and kata-os-model mostly in support
of the aarch64 platform. This is derived from Marcin's aarch64 work.

TODO(sleffler): seL4_Page_Map_Flush maybe belongs in sel4-sys

sel4-sys changes:
- hoist seL4_ObjectTypeCount out of arch
- make seL4_Page_Map for ARM honor the grant right to set the NX bit
- fill-in seL4_ObjectType & related impl's for ARM & X86
- import cfg-if crate to cleanup various tangled conditionals

kata-os-model changes:
- add seL4_Page_Map_Flush to encapsulate arch-specific work needed after
  an seL4_Page_Map call; this is kept separate to avoid changing the
  Page_Map api
- purge kobject_t and replace kobject_get_type with get_frame_type
- purge kobject_get_size (only use was to calculate the size of the
  SchedContext object which is arch-independent)
- redo CDL_ObjectType to work for all arch's
- various fixes for target_arch aarch64
- construct platform_gen.rs at build-time from seL4's platform_gen.h for
  seL4_Page_Map_Flush to do it's job
- get target_arch arm closer (esp needs vspace setup fixed)
- correct various "arm" & "x86" target_arch checks to cover both 32-
  and 64-bit arch's
- misc style changes (e.g. sort imports)

capdl changes:
- add arch-specific CDL_CapType entries

NB: seL4_Page_Map_Flush for ARM is overly conservative in invalidating
    the data cache; this could be improved by identifying whether the page
    has a pre-assigned paddr
Change-Id: I005cbbbd36ea6711feed66412391e3790dda2966
GitOrigin-RevId: b5c6893fa1c7f3297d88aa7f522a2792ac3b75c7
This commit is contained in:
Marcin Witkowski 2022-02-24 14:27:44 +01:00 committed by Sam Leffler
parent 84986b53d4
commit 2a1cf83ac5
21 changed files with 577 additions and 458 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
apps/system/components/kata-os-common/src/capdl/mod.rs
View File

@ -131,24 +131,6 @@ pub const CDL_TCB_TemporalFaultEP_Slot: seL4_Word = CDL_TCB_SC_Slot + 1;
// CONFIG_ARM_HYPERVISOR_SUPPORT || CONFIG_VTX
pub const CDL_TCB_VCPU_Slot: seL4_Word = CDL_TCB_TemporalFaultEP_Slot + 1;
#[derive(Debug, PartialEq, Eq)]
pub enum kobject_t {
KOBJECT_PAGE_DIRECTORY,
KOBJECT_PAGE_TABLE,
KOBJECT_FRAME,
KOBJECT_ARCH_NUM_TYPES,
KOBJECT_TCB,
KOBJECT_CNODE,
KOBJECT_CSLOT,
KOBJECT_UNTYPED,
KOBJECT_ENDPOINT,
KOBJECT_NOTIFICATION,
KOBJECT_REPLY,
KOBJECT_SCHED_CONTEXT,
NUM_KOBJECT_TYPES,
}
pub type CDL_ObjID = seL4_Word;
// NB: some object id's are written in the spec as -1
pub fn is_objid_valid(val: CDL_ObjID) -> bool {
@ -201,7 +183,19 @@ pub enum CDL_CapType {
CDL_PGDCap,
CDL_ASIDControlCap,
CDL_ASIDPoolCap,
// TODO(sleffler): missing arch-specific caps
#[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
CDL_IOPortsCap,
#[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
CDL_IOSpaceCap,
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
CDL_ARMIOSpaceCap,
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
CDL_SIDCap,
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
CDL_CBCap,
CDL_SCCap,
CDL_SchedControlCap,
CDL_RTReplyCap,
@ -366,13 +360,13 @@ impl CDL_Cap {
#[inline]
pub fn rights(&self) -> CDL_CapRights {
unsafe {
::core::mem::transmute::<u32, CDL_CapRights>(self._bitfield.get(4, 4) as u32)
::core::mem::transmute::<usize, CDL_CapRights>(self._bitfield.get(4, 4) as usize)
}
}
#[inline]
pub fn set_rights(&mut self, val: CDL_CapRights) {
unsafe {
let val: u32 = ::core::mem::transmute(val);
let val: usize = ::core::mem::transmute(val);
self._bitfield.set(4, 4, val as u64)
}
}
@ -415,28 +409,44 @@ impl<'a> CDL_CapMap {
}
}
// TODO(sleffler): values depend on config & arch, this works for riscv
// might be better to ditch the enum or move to arch
// Object tyype as found in the capdl input stream. This is partly defined
// in terms of the seL4_ObjectType and otherwise using seL4_LastObjectCount.
// The result is a mess and for zero gain (relative to just never reusing
// an enum member value).
#[repr(C)]
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
pub enum CDL_ObjectType {
CDL_Untyped = 0,
CDL_TCB,
CDL_Endpoint,
CDL_Notification,
CDL_CNode,
CDL_Endpoint = sel4_sys::seL4_EndpointObject as isize,
CDL_Notification = sel4_sys::seL4_NotificationObject as isize,
CDL_TCB = sel4_sys::seL4_TCBObject as isize,
CDL_CNode = sel4_sys::seL4_CapTableObject as isize,
CDL_Untyped = sel4_sys::seL4_UntypedObject as isize,
#[cfg(feature = "CONFIG_KERNEL_MCS")]
CDL_SchedContext,
CDL_SchedContext = sel4_sys::seL4_SchedContextObject as isize,
#[cfg(feature = "CONFIG_KERNEL_MCS")]
CDL_RTReply,
CDL_RTReply = sel4_sys::seL4_ReplyObject as isize,
// XXX these work for CONFIG_ARCH_RISCV
CDL_Frame,
CDL_Mega_Frame,
CDL_PT,
CDL_Frame = sel4_sys::seL4_SmallPageObject as isize,
CDL_PT = sel4_sys::seL4_PageTableObject as isize,
#[cfg(any(target_arch = "arm", target_arch = "aarch64", target_arch = "x86"))]
CDL_PD = sel4_sys::seL4_PageDirectoryObject as isize,
// NB: remainder are numbered relative to seL4_ObjectTypeCount
#[cfg(target_arch = "aarch64")]
CDL_PUD = sel4_sys::seL4_PageUpperDirectoryObject as isize,
#[cfg(target_arch = "aarch64")]
CDL_PGD = sel4_sys::seL4_PageGlobalDirectoryObject as isize,
#[cfg(any(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT", feature = "CONFIG_VTX"))]
CDL_VCPU = sel4_sys::seL4_VCPUObject as isize,
#[cfg(target_arch = "x86_64")]
CDL_PML4 = sel4_sys::seL4_PML4Object as isize,
#[cfg(target_arch = "x86_64")]
CDL_PDPT = sel4_sys::seL4_PDPTObject as isize,
// NB: the following are numbered relative to seL4_ObjectTypeCount,
// do not re-order!
CDL_ASIDPool = seL4_ObjectTypeCount + 1,
CDL_Interrupt,
CDL_IOPorts, // CONFIG_ARCH_X86
@ -458,6 +468,7 @@ pub enum CDL_ObjectType {
}
impl From<CDL_ObjectType> for seL4_ObjectType {
fn from(type_: CDL_ObjectType) -> seL4_ObjectType {
// TODO(sleffler): maybe assert type_ < seL4_ObjectTypeCount
unsafe { ::core::mem::transmute(type_) }
}
}

2
apps/system/components/kata-os-common/src/model/Cargo.toml
View File

@ -8,6 +8,8 @@ build = "build.rs"
[build-dependencies]
sel4-config = { path = "../sel4-config" }
serde = { version = "1.0", features = ["derive"] }
serde_yaml = "0.8"
[build-env]
SEL4_OUT_DIR = "${ROOTDIR}out/kata/kernel"

178
apps/system/components/kata-os-common/src/model/arch/aarch32.rs Normal file
View File

@ -0,0 +1,178 @@
// ARM aarch32 target support.
#![allow(non_camel_case_types)]
use static_assertions::assert_cfg;
assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
mod arm;
pub use arm::*;
use capdl::*;
use capdl::CDL_CapType::*;
use capdl::CDL_ObjectType::*;
use crate::KataOsModel;
use sel4_sys::seL4_CapInitThreadCNode;
use sel4_sys::seL4_CapIRQControl;
use sel4_sys::seL4_CPtr;
use sel4_sys::seL4_Error;
use sel4_sys::seL4_IRQControl_GetTrigger;
use sel4_sys::seL4_LargePageBits;
use sel4_sys::seL4_ObjectType::*;
use sel4_sys::seL4_ObjectType;
use sel4_sys::seL4_PageBits;
use sel4_sys::seL4_PageTableIndexBits;
use sel4_sys::seL4_Result;
use sel4_sys::seL4_UserContext;
use sel4_sys::seL4_Word;
use sel4_sys::seL4_WordBits;
const CDL_PT_NUM_LEVELS: usize = 2;
// TOOD(sleffler): levels really should be 0 & 1, the names are vestiges of 64-bit support
const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
match object_size {
seL4_PageBits => seL4_ARM_SmallPageObject,
seL4_LargePageBits => seL4_ARM_LargePageObject,
_ => panic!("Unexpected frame size {}", object_size),
}
}
pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
assert_eq!(obj.r#type(), CDL_ARMInterrupt);
// XXX seL4_IRQControl_GetTriggerCore for NUM_NODES > 1
unsafe {
seL4_IRQControl_GetTrigger(
seL4_CapIRQControl,
irq,
obj.armirq_trigger(),
/*root=*/ seL4_CapInitThreadCNode as usize,
/*index=*/ free_slot,
/*depth=*/ seL4_WordBits as u8,
)
}
}
pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_UserContext {
#[rustfmt::skip]
static mut regs: seL4_UserContext = seL4_UserContext {
pc: 0, sp: 0, cpsr: 0,
r0: 0, r1: 0, r8: 0, r9: 0, r10: 0, r11: 0, r12: 0,
r2: 0, r3: 0, r4: 0, r5: 0, r6: 0, r7: 0, r14: 0,
tpidrurw: 0, tpidruro: 0,
};
assert_eq!(cdl_tcb.r#type(), CDL_TCB);
unsafe {
regs.pc = cdl_tcb.tcb_pc();
regs.sp = sp; // NB: may be adjusted from cdl_tcb.tcb_sp()
let argv = core::slice::from_raw_parts(cdl_tcb.tcb_init(), cdl_tcb.tcb_init_sz());
regs.r0 = if argv.len() > 0 { argv[0] } else { 0 };
regs.r1 = if argv.len() > 1 { argv[1] } else { 0 };
regs.r2 = if argv.len() > 2 { argv[2] } else { 0 };
regs.r3 = if argv.len() > 3 { argv[3] } else { 0 };
// trace!("Start {} with pc {:#x} sp {:#x} argv {:?}", cdl_tcb.name(),
// regs.pc, regs.sp, argv);
&regs as *const seL4_UserContext
}
}
impl<'a> KataOsModel<'a> {
pub fn create_arch_object(
&mut self,
_obj: &CDL_Object,
_id: CDL_ObjID,
_free_slot: usize,
) -> Option<seL4_Error> {
// CDL_SID objects with CONFIG_ARM_SMU?
None
}
// TODO(sleffler): BLINDLY COPIED FROM RISCV, CONVERT
pub fn init_vspace(&mut self, obj_id: CDL_ObjID) -> seL4_Result {
self.init_level_2(obj_id, 0, obj_id)
}
fn init_level_3(
&mut self,
level_3_obj: CDL_ObjID,
level_0_obj: CDL_ObjID,
level_3_base: usize,
) -> seL4_Result {
for slot in self.get_object(level_3_obj).slots_slice() {
let frame_cap = &slot.cap;
self.map_page_frame(
frame_cap,
level_0_obj,
frame_cap.cap_rights().into(),
level_3_base + (slot.slot << seL4_PageBits),
)?;
}
Ok(())
}
fn init_level_2(
&mut self,
level_0_obj: CDL_ObjID,
level_2_base: usize,
level_2_obj: CDL_ObjID,
) -> seL4_Result {
for slot in self.get_object(level_2_obj).slots_slice() {
let base = level_2_base + (slot.slot << (CDL_PT_LEVEL_3_IndexBits + seL4_PageBits));
let level_3_cap = &slot.cap;
if level_3_cap.r#type() == CDL_FrameCap {
self.map_page_frame(
level_3_cap,
level_0_obj,
level_3_cap.cap_rights().into(),
base,
)?;
} else {
let level_3_obj = level_3_cap.obj_id;
self.map_page_table(level_3_cap, level_0_obj, base)?;
self.init_level_3(level_3_obj, level_0_obj, base)?;
}
}
Ok(())
}
pub fn get_cdl_frame_pt(&self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
self.get_cdl_frame_pt_recurse(pd, vaddr, 2)
}
/**
* Do a recursive traversal from the top to bottom of a page table structure to
* get the cap for a particular page table object for a certain vaddr at a certain
* level. The level variable treats level==CDL_PT_NUM_LEVELS as the root page table
* object, and level 0 as the bottom level 4k frames.
*/
fn get_cdl_frame_pt_recurse(
&self,
root: CDL_ObjID,
vaddr: usize,
level: usize,
) -> Option<&'a CDL_Cap> {
fn PT_LEVEL_SLOT(vaddr: usize, level: usize) -> usize {
(vaddr >> ((seL4_PageTableIndexBits * (level - 1)) + seL4_PageBits))
& MASK(seL4_PageTableIndexBits)
}
let obj_id = if level < CDL_PT_NUM_LEVELS {
self.get_cdl_frame_pt_recurse(root, vaddr, level + 1)?
.obj_id
} else {
root
};
self.get_object(obj_id)
.get_cap_at(PT_LEVEL_SLOT(vaddr, level))
}
}

98
apps/system/components/kata-os-common/src/model/arch/aarch64.rs
View File

@ -8,30 +8,32 @@ assert_cfg!(target_arch = "aarch64");
mod arm;
pub use arm::*;
use crate::KataOsModel;
use capdl::kobject_t::*;
use capdl::*;
use capdl::CDL_CapType::*;
use capdl::CDL_ObjectType::*;
use capdl::*;
use log::{error, trace};
use crate::KataOsModel;
use sel4_sys::seL4_ARM_PageDirectory_Map;
use sel4_sys::seL4_ARM_PageUpperDirectory_Map;
use sel4_sys::seL4_CapInitThreadCNode;
use sel4_sys::seL4_CapIRQControl;
use sel4_sys::seL4_CPtr;
use sel4_sys::seL4_Error;
use sel4_sys::seL4_IRQControl_Get;
use sel4_sys::seL4_HugePageBits;
use sel4_sys::seL4_IRQControl_GetTrigger;
use sel4_sys::seL4_LargePageBits;
use sel4_sys::seL4_ObjectType::*;
use sel4_sys::seL4_ObjectType;
use sel4_sys::seL4_PageBits;
use sel4_sys::seL4_PageDirIndexBits;
use sel4_sys::seL4_PageTableIndexBits;
use sel4_sys::seL4_PGDIndexBits;
use sel4_sys::seL4_PUDIndexBits;
use sel4_sys::seL4_Result;
use sel4_sys::seL4_UserContext;
use sel4_sys::seL4_VMAttributes;
use sel4_sys::seL4_Word;
pub use arm::PAGE_SIZE;
pub const STACK_ALIGNMENT_BYTES: usize = 16;
pub const REG_ARGS: seL4_Word = 4; // Number of regs for passing thread args
use sel4_sys::seL4_WordBits;
pub const CDL_PT_LEVEL_1_IndexBits: usize = seL4_PUDIndexBits;
pub const CDL_PT_LEVEL_2_IndexBits: usize = seL4_PageDirIndexBits;
@ -39,17 +41,21 @@ pub const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
pub fn PD_SLOT(vaddr: usize) -> usize {
(vaddr >> (seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PageDirIndexBits)
pub fn PGD_SLOT(vaddr: usize) -> usize {
(vaddr >> (seL4_PUDIndexBits + seL4_PageDirIndexBits + seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PGDIndexBits)
}
pub fn PUD_SLOT(vaddr: usize) -> usize {
(vaddr >> (seL4_PageDirIndexBits + seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PUDIndexBits)
}
// NB: used for tcb_args::maybe_spill_tcb_args
pub fn PT_SLOT(vaddr: usize) -> usize { (vaddr >> seL4_PageBits) & MASK(seL4_PageTableIndexBits) }
// Identifies IRQ objects that potentially need special processing.
pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_ARMInterrupt || type_ == CDL_Interrupt }
// Identifies objects that need to be instantiated.
pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
match object_size {
seL4_PageBits => seL4_ARM_SmallPageObject,
seL4_LargePageBits => seL4_ARM_LargePageObject,
seL4_HugePageBits => seL4_ARM_HugePageObject,
_ => panic!("Unexpected frame size {}", object_size),
}
}
pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
assert_eq!(obj.r#type(), CDL_ARMInterrupt);
@ -96,40 +102,6 @@ pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_User
}
}
pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
if t == KOBJECT_FRAME && object_size == seL4_HugePageBits {
return object_size;
}
if t == KOBJECT_PAGE_UPPER_DIRECTORY {
return seL4_PUDBits;
}
#[cfg(feature = "CONFIG_KERNEL_MCS")]
if t == KOBJECT_SCHED_CONTEXT {
return core::cmp::max(object_size, sel4_sys::seL4_MinSchedContextBits);
}
error!("Unexpected object: type {:?} size {}", t, object_size);
0
}
pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
match t {
KOBJECT_PAGE_GLOBAL_DIRECTORY => {
return seL4_ARM_PageGlobalDirectoryObject;
}
KOBJECT_PAGE_UPPER_DIRECTORY => {
return seL4_ARM_PageUpperDirectoryObject;
}
KOBJECT_FRAME => {
if object_size == seL4_HugePageBits {
return seL4_ARM_HugePageObject;
}
error!("Unexpected frame size {}", object_size);
}
_ => {}
}
error!("Unexpected object: type {:?} size {}", t, object_size);
seL4_InvalidObjectType
}
impl<'a> KataOsModel<'a> {
pub fn create_arch_object(
&mut self,
@ -214,11 +186,11 @@ impl<'a> KataOsModel<'a> {
base,
)?;
} else {
let level_3_obj = level_3_cap.obj_id;
self.map_page_dir(level_2_cap, level_0_obj, base)?;
self.init_level_2(level_0_obj, base, level_2_obj.obj_id)?;
self.init_level_2(level_0_obj, base, level_2_cap.obj_id)?;
}
}
Ok(())
}
fn map_page_dir(&self, page_cap: &CDL_Cap, pd_id: CDL_ObjID, vaddr: seL4_Word) -> seL4_Result {
@ -240,19 +212,19 @@ impl<'a> KataOsModel<'a> {
&mut self,
level_0_obj: CDL_ObjID,
level_0_base: usize,
level_0_obj: CDL_ObjID,
) -> Result<(), seL4_Error> {
_level_0_obj: CDL_ObjID,
) -> seL4_Result {
for slot in self.get_object(level_0_obj).slots_slice() {
let base = level_0_base
+ (slot.slot
let base = (level_0_base + slot.slot)
<< (CDL_PT_LEVEL_1_IndexBits
+ CDL_PT_LEVEL_2_IndexBits
+ CDL_PT_LEVEL_3_IndexBits
+ seL4_PageBits));
+ seL4_PageBits);
let level_1_cap = &slot.cap;
self.map_page_upper_dir(level_1_cap, level_0_obj, base)?;
self.init_level_1(level_0_obj, base, level_1_cap.obj_id)?;
}
Ok(())
}
fn map_page_upper_dir(
@ -277,7 +249,7 @@ impl<'a> KataOsModel<'a> {
pub fn get_cdl_frame_pt(&self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
let pd_cap = self.get_cdl_frame_pd(pd, vaddr)?;
self.get_spec_object(pd_cap.obj_id)
self.get_object(pd_cap.obj_id)
.get_cap_at(PD_SLOT(vaddr))
}
@ -286,15 +258,15 @@ impl<'a> KataOsModel<'a> {
feature = "CONFIG_ARM_HYPERVISOR_SUPPORT",
feature = "CONFIG_ARM_PA_SIZE_BITS_40"
)) {
self.get_spec_object(root).get_cap_at(PUD_SLOT(vaddr))
self.get_object(root).get_cap_at(PUD_SLOT(vaddr))
} else {
let pud_cap = self.get_cdl_frame_pud(root, vaddr)?;
self.get_spec_object(pud_cap.obj_id)
self.get_object(pud_cap.obj_id)
.get_cap_at(PUD_SLOT(vaddr))
}
}
fn get_cdl_frame_pud(&self, root: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
self.get_spec_object(root).get_cap_at(PGD_SLOT(vaddr))
self.get_object(root).get_cap_at(PGD_SLOT(vaddr))
}
}

278
apps/system/components/kata-os-common/src/model/arch/arm.rs
View File

@ -1,84 +1,71 @@
// ARM 32-bit target support.
// ARM common target support.
#![allow(non_camel_case_types)]
use static_assertions::assert_cfg;
assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
assert_cfg!(any(target_arch = "arm", target_arch = "aarch64"));
use crate::KataOsModel;
use capdl::kobject_t::*;
use capdl::CDL_CapType::*;
use capdl::CDL_ObjectType::*;
use capdl::*;
use log::{error, trace};
use sel4_sys::seL4_ARM_Page_CleanInvalidate_Data;
use sel4_sys::seL4_ARM_Page_Map;
use sel4_sys::seL4_ARM_Page_GetAddress;
use sel4_sys::seL4_ARM_Page_Unify_Instruction;
use sel4_sys::seL4_CapInitThreadCNode;
use sel4_sys::seL4_CapIRQControl;
use sel4_sys::seL4_CPtr;
use sel4_sys::seL4_Error;
use sel4_sys::seL4_IRQControl_Get;
use sel4_sys::seL4_ObjectType::*;
use sel4_sys::seL4_CapRights;
use sel4_sys::seL4_ObjectType;
use sel4_sys::seL4_Page;
use sel4_sys::seL4_PageBits;
use sel4_sys::seL4_PageDirIndexBits;
use sel4_sys::seL4_PageTableIndexBits;
use sel4_sys::seL4_PUDIndexBits;
use sel4_sys::seL4_Result;
use sel4_sys::seL4_UserContext;
use sel4_sys::seL4_VMAttributes;
use sel4_sys::seL4_Word;
pub const PAGE_SIZE: usize = 4096;
pub const STACK_ALIGNMENT_BYTES: usize = 16;
pub const REG_ARGS: seL4_Word = 4; // Number of regs for passing thread args
pub const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
include!(concat!(env!("OUT_DIR"), "/platform_gen.rs"));
// NB: this overrides what sel4_sys provides
pub fn seL4_Page_Map(
sel4_page: seL4_ARM_Page,
sel4_pd: seL4_ARM_PageTable,
vaddr: seL4_Word,
// When seL4 creates a new frame object it zeroes the associated memory
// through a cached kernel mapping. If we are configuring a cached
// mapping for the target, standard coherence protocols ensure
// everything works as expected. However, if we are configuring an
// uncached mapping for the target, the dirty zero data cached from the
// kernel's mapping is likely flushed to memory at some time in the
// future causing an unpleasant surprise for the target whose own
// uncached writes are mysteriously overwritten. To prevent this, we
// unify the mapping here, flushing the cached data from the kernel's
// mapping.
pub unsafe fn seL4_Page_Map_Flush(
page_type: seL4_ObjectType,
sel4_page: seL4_Page,
rights: seL4_CapRights,
vm_attribs: seL4_ARM_VMAttributes,
vm_attribs: seL4_VMAttributes,
) -> seL4_Result {
if !rights.get_capAllowGrant() {
vm_attribs |= seL4_ARM_ExecuteNever;
}
seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs)?;
// XXX lookup frame_size_bits & page
/* When seL4 creates a new frame object it zeroes the associated memory
* through a cached kernel mapping. If we are configuring a cached
* mapping for the target, standard coherence protocols ensure
* everything works as expected. However, if we are configuring an
* uncached mapping for the target, the dirty zero data cached from the
* kernel's mapping is likely flushed to memory at some time in the
* future causing an unpleasant surprise for the target whose own
* uncached writes are mysteriously overwritten. To prevent this, we
* unify the mapping here, flushing the cached data from the kernel's
* mapping.
*/
const CHAR_BIT: usize = 8; // XXX
assert!(frame_size_bits <= size_of::<usize>() * CHAR_BIT - 1, "illegal object size");
let addr = seL4_ARM_Page_GetAddress(sel4_page);
if addr.paddr >= memory_region[0].start && addr.paddr <= memory_region[0].end {
if !(vm_attribs & seL4_ARM_PageCacheable) && spec.objects[page].paddr() == 0 {
if MEMORY_REGIONS[0].start <= addr.paddr && addr.paddr <= MEMORY_REGIONS[0].end {
let frame_size_bits = page_type.size_bits().unwrap();
assert!(frame_size_bits <= (usize::BITS - 1) as usize,
"{:?}: illegal object size", page_type);
// NB: could minimize invalidations by checking page's paddr, but
// given the cost already incurred to lookup the page's paddr
// just always do it
if ((vm_attribs as u32) & sel4_sys::seL4_ARM_VMAttributes::PageCacheable as u32) == 0 {
seL4_ARM_Page_CleanInvalidate_Data(sel4_page, 0, BIT(frame_size_bits))?;
}
if rights.get_capAllowGrant() {
if rights.get_capAllowGrant() != 0 {
seL4_ARM_Page_Unify_Instruction(sel4_page, 0, BIT(frame_size_bits))?;
}
}
Ok(())
}
fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
fn BIT(bit_num: usize) -> usize { 1 << bit_num }
fn MASK(pow2_bits: usize) -> usize { BIT(pow2_bits) - 1 }
#[allow(dead_code)]
pub fn PD_SLOT(vaddr: usize) -> usize {
(vaddr >> (seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PageDirIndexBits)
}
@ -90,198 +77,3 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_ARMInterrupt || type
// Identifies objects that need to be instantiated.
pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Error {
let root = seL4_CapInitThreadCNode;
let index = free_slot;
let depth = seL4_WordBits as u8;
match obj.r#type() {
// XXX seL4_IRQControl_GetTriggerCore for NUM_NODES > 1
#[cfg(feature = "CONFIG_SMP_SUPPORT")]
CDL_ARMInterrupt => {
seL4_IRQControl_GetTriggerCore(
seL4_CapIRQControl,
irq,
obj.armirq_trigger(),
root,
index,
depth,
obj.armirq_target(),
)
}
#[cfg(not(feature = "CONFIG_SMP_SUPPORT"))]
CDL_ARMInterrupt => {
seL4_IRQControl_GetTrigger(
seL4_CapIRQControl,
irq,
obj.armirq_trigger(),
root,
index,
depth,
)
}
_ => seL4_IRQControl_Get(seL4_CapIRQControl, irq, root, index, depth),
}
}
pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_UserContext {
#[rustfmt::skip]
static mut regs: seL4_UserContext = seL4_UserContext {
pc: 0, sp: 0, spsr: 0,
x0: 0, x1: 0, x2: 0, x3: 0, x4: 0, x5: 0, x6: 0, x7: 0,
x8: 0, x9: 0, x10: 0, x11: 0, x12: 0, x13: 0, x14: 0, x15: 0,
x16: 0, x17: 0, x18: 0, x19: 0, x20: 0, x21: 0, x22: 0, x23: 0,
x24: 0, x25: 0, x26: 0, x27: 0, x28: 0, x29: 0, x30: 0,
tpidr_el0: 0, tpidrro_el0: 0,
};
assert_eq!(cdl_tcb.r#type(), CDL_TCB);
unsafe {
regs.pc = cdl_tcb.tcb_pc();
regs.sp = sp; // NB: may be adjusted from cdl_tcb.tcb_sp()
let argv = core::slice::from_raw_parts(cdl_tcb.tcb_init(), cdl_tcb.tcb_init_sz());
regs.x0 = if argv.len() > 0 { argv[0] } else { 0 };
regs.x1 = if argv.len() > 1 { argv[1] } else { 0 };
regs.x2 = if argv.len() > 2 { argv[2] } else { 0 };
regs.x3 = if argv.len() > 3 { argv[3] } else { 0 };
// trace!("Start {} with pc {:#x} sp {:#x} argv {:?}", cdl_tcb.name(),
// regs.pc, regs.sp, argv);
&regs as *const seL4_UserContext
}
}
pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
if t == KOBJECT_FRAME && object_size == seL4_HugePageBits {
return object_size;
}
if t == KOBJECT_PAGE_UPPER_DIRECTORY {
return seL4_PUDBits;
}
#[cfg(feature = "CONFIG_KERNEL_MCS")]
if t == KOBJECT_SCHED_CONTEXT {
return core::cmp::max(object_size, sel4_sys::seL4_MinSchedContextBits);
}
error!("Unexpected object: type {:?} size {}", t, object_size);
0
}
pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
match t {
KOBJECT_PAGE_GLOBAL_DIRECTORY => {
return seL4_ARM_PageGlobalDirectoryObject;
}
KOBJECT_PAGE_UPPER_DIRECTORY => {
return seL4_ARM_PageUpperDirectoryObject;
}
KOBJECT_FRAME => {
if object_size == seL4_HugePageBits {
return seL4_ARM_HugePageObject;
}
error!("Unexpected frame size {}", object_size);
}
_ => {}
}
error!("Unexpected object: type {:?} size {}", t, object_size);
seL4_InvalidObjectType
}
impl<'a> KataOsModel<'a> {
pub fn create_arch_object(
&mut self,
obj: &CDL_Object,
_id: CDL_ObjID,
free_slot: usize,
) -> Option<seL4_Error> {
match obj.r#type() {
#[cfg(feature = "CONFIG_ARM_SMMU")]
CDL_SID => {
/* There can be multiple sids per context bank, currently only 1
* sid per cb is implemented for the vms. When this gets extended
* we need to decide to add sid number -> cb number map into the
* haskell / python tool or generate the capdl spec so that the
* order remains correct here e.g a list a stream ids followed by
* the cb they are mapped to, the cb condition here (1***) will the
* reset the stream id number back to 0 for the next context bank.
*/
assert!(sid_number <= MAX_STREAM_IDS);
// XXX handle error
seL4_ARM_SIDControl_GetSID(
seL4_CapSMMUSIDControl,
self.sid_number,
seL4_CapInitThreadCNode,
free_slot,
seL4_WordBits as u8,
);
self.sid_number += 1;
Some(seL4_NoError)
}
#[cfg(feature = "CONFIG_ARM_SMMU")]
CDL_CB => {
self.sid_number = 0; //(1***)
Some(seL4_ARM_CBControl_GetCB(
seL4_CapSMMUCBControl,
obj.cb_bank(),
seL4_CapInitThreadCNode,
free_slot,
seL4_WordBits as u8,
))
}
_ => None,
}
}
pub fn init_vspace(&mut self, obj_id: CDL_ObjID) -> seL4_Result {
assert_eq!(self.get_object(obj_id).r#type(), CDL_PD);
// XXX C code does all PD's before PT's, not sure if this works
self.map_page_directory(obj_id)?;
self.map_page_directory_page_tables(obj_id)?;
Ok(())
}
fn map_page_directory(&self, pd_id: CDL_ObjID) {
fn map_page_directory_slot(pd_id: CDL_ObjID, pd_slot: &CDL_CapSlot) {
let page_cap = &pd_slot.cap;
let page_vaddr = pd_slot.slot << (seL4_PageTableIndexBits + seL4_PageBits);
self.map_page(page_cap, pd_id, page_cap.cap_rights(), page_vaddr);
}
for slot in self.spec.get_object(pd_id).slots_slice() {
map_page_directory_slot(pd_id, &slot);
}
}
fn map_page_directory_page_tables(&self, pd: CDL_ObjID) {
fn map_page_table_slots(pd: CDL_ObjID, pd_slot: &CDL_CapSlot) {
fn map_page_table_slot(
pd: CDL_ObjID,
pt: CDL_ObjID,
pt_vaddr: seL4_Word,
pt_slot: &CDL_CapSlot,
) {
let page_cap = &pt_slot.cap;
let page_vaddr = pt_vaddr + (pt_slot.slot << seL4_PageBits);
self.map_page(page_cap, pd, page_cap.cap_rights(), page_vaddr);
}
let page_cap = &pd_slot.cap;
if (page_cap.r#type() == CDL_PTCap) {
let page = page_cap.obj_id;
let page_vaddr = pd_slot.slot << (seL4_PageTableIndexBits + seL4_PageBits);
for slot in self.spec.get_object(page).slots_slice() {
self.map_page_table_slot(pd, page, page_vaddr, &slot);
}
}
}
for slot in self.spec.get_object(pd).slots_slice() {
self.map_page_table_slots(pd, &slot);
}
}
pub fn get_cdl_frame_pt(&mut self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a mut CDL_Cap> {
self.get_spec_object(pd).get_cap_at(PD_SLOT(vaddr))
}
}

12
apps/system/components/kata-os-common/src/model/arch/riscv.rs
View File

@ -9,9 +9,14 @@ assert_cfg!(any(target_arch = "riscv32", target_arch = "riscv64"));
use capdl::CDL_ObjectType::*;
use capdl::*;
use sel4_sys::seL4_CapRights;
use sel4_sys::seL4_ObjectType;
use sel4_sys::seL4_Page;
use sel4_sys::seL4_PageBits;
use sel4_sys::seL4_PageDirIndexBits;
use sel4_sys::seL4_PageTableIndexBits;
use sel4_sys::seL4_Result;
use sel4_sys::seL4_VMAttributes;
use sel4_sys::seL4_Word;
pub const PAGE_SIZE: usize = 4096; // Base page size
@ -34,3 +39,10 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_Interrupt }
// by architectures that have device objects that are not backed by
// untyped memory (i.e. that need creation).
pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
pub unsafe fn seL4_Page_Map_Flush(
_page_type: seL4_ObjectType,
_sel4_page: seL4_Page,
_rights: seL4_CapRights,
_vm_attribs: seL4_VMAttributes,
) -> seL4_Result { Ok(()) }

59
apps/system/components/kata-os-common/src/model/arch/riscv32.rs
View File

@ -8,12 +8,10 @@ assert_cfg!(target_arch = "riscv32");
mod riscv;
pub use riscv::*;
use crate::KataOsModel;
use capdl::kobject_t::*;
use capdl::*;
use capdl::CDL_CapType::*;
use capdl::CDL_ObjectType::*;
use capdl::*;
use log::error;
use crate::KataOsModel;
use sel4_sys::seL4_CapInitThreadCNode;
use sel4_sys::seL4_CapIRQControl;
@ -21,13 +19,12 @@ use sel4_sys::seL4_CPtr;
use sel4_sys::seL4_Error;
use sel4_sys::seL4_IRQControl_Get;
use sel4_sys::seL4_LargePageBits;
use sel4_sys::seL4_MinSchedContextBits;
use sel4_sys::seL4_ObjectType;
use sel4_sys::seL4_ObjectType::*;
use sel4_sys::seL4_PageBits;
use sel4_sys::seL4_PageTableBits;
use sel4_sys::seL4_PageTableIndexBits;
use sel4_sys::seL4_Result;
use sel4_sys::seL4_RISCV_4K_Page;
use sel4_sys::seL4_RISCV_Mega_Page;
use sel4_sys::seL4_UserContext;
use sel4_sys::seL4_Word;
use sel4_sys::seL4_WordBits;
@ -36,6 +33,14 @@ const CDL_PT_NUM_LEVELS: usize = 2;
// TOOD(sleffler): levels really should be 0 & 1, the names are vestiges of 64-bit support
const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
match object_size {
seL4_PageBits => seL4_RISCV_4K_Page,
seL4_LargePageBits => seL4_RISCV_Mega_Page,
_ => panic!("Unexpected frame size {}", object_size),
}
}
fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
pub fn create_irq_cap(irq: CDL_IRQ, _obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
@ -79,46 +84,6 @@ pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_User
}
}
pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
match t {
KOBJECT_FRAME => {
if object_size == seL4_PageBits || object_size == seL4_LargePageBits {
return object_size;
}
}
KOBJECT_PAGE_TABLE => {
return seL4_PageTableBits;
}
KOBJECT_SCHED_CONTEXT => {
return core::cmp::max(object_size, seL4_MinSchedContextBits);
}
_ => {}
}
error!("Unexpected object: type {:?} size {}", t, object_size);
object_size
}
pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
match t {
KOBJECT_PAGE_DIRECTORY => {
return seL4_RISCV_PageTableObject;
}
KOBJECT_PAGE_TABLE => {
return seL4_RISCV_PageTableObject;
}
KOBJECT_FRAME => {
if object_size == seL4_PageBits {
return seL4_RISCV_4K_Page;
}
if object_size == seL4_LargePageBits {
return seL4_RISCV_Mega_Page;
}
}
_ => {}
}
error!("Unexpected object: type {:?} size {}", t, object_size);
seL4_LastObjectType // XXX not right
}
impl<'a> KataOsModel<'a> {
pub fn create_arch_object(
&mut self,

16
apps/system/components/kata-os-common/src/model/arch/x86.rs
View File

@ -4,6 +4,7 @@ use static_assertions::assert_cfg;
assert_cfg!(target_arch = "x86");
use log::{debug, error, info, trace, warn};
use sel4_sys::seL4_Result;
pub const PAGE_SIZE: usize = 4096;
pub const STACK_ALIGNMENT_BYTES: usize = 16;
@ -24,6 +25,21 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool {
// Identifies objects that need to be instantiated.
pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
pub unsafe fn seL4_Page_Map_Flush(
_page_type: seL4_ObjectType,
_sel4_page: seL4_Page,
_rights: seL4_CapRights,
_vm_attribs: seL4_VMAttributes,
) -> seL4_Result { Ok(()) }
pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
match object_size {
seL4_PageBits => seL4_X86_4K,
seL4_LargePageBits => seL4_X86_LargePageObject,
_ => panic!("Unexpected frame size {}", object_size),
}
}
pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Error {
let root = seL4_CapInitThreadCNode;
let index = free_slot;

33
apps/system/components/kata-os-common/src/model/build.rs
View File

@ -1,5 +1,18 @@
extern crate sel4_config;
use std::env;
use std::fs;
use std::io::Write;
#[derive(serde::Deserialize)]
struct PlatformInfo {
memory: Vec<MemoryRange>,
}
#[derive(serde::Deserialize)]
struct MemoryRange {
start: u64,
end: u64,
}
fn main() {
// If SEL4_OUT_DIR is not set we expect the kernel build at a fixed
@ -18,4 +31,24 @@ fn main() {
for feature in features {
println!("cargo:rustc-cfg=feature=\"{}\"", feature);
}
// Some architectures need informations from platform_yaml.
let platform_yaml_path = format!("{}/gen_headers/plat/machine/platform_gen.yaml", sel4_out_dir);
if let Ok(platform_yaml) = fs::File::open(&platform_yaml_path) {
let platform_info: PlatformInfo = serde_yaml::from_reader(platform_yaml).expect("invalid yaml file");
let out_dir = env::var("OUT_DIR").unwrap();
let out_path = std::path::Path::new(&out_dir).join("platform_gen.rs");
let mut out_file = fs::File::create(&out_path).unwrap();
writeln!(&mut out_file,
"struct MemoryRegion {{
start: usize,
end: usize,
}}").unwrap();
writeln!(&mut out_file, "const MEMORY_REGIONS: [MemoryRegion; {}] = [", platform_info.memory.len()).unwrap();
for range in platform_info.memory {
writeln!(&mut out_file, " MemoryRegion {{ start: 0x{:X}, end: 0x{:X} }},", range.start, range.end).ok();
}
writeln!(&mut out_file, "];").ok();
}
}

16
apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs
View File

@ -1,11 +1,10 @@
// Dynamic Object Allocation.
use crate::KataOsModel;
use capdl::kobject_t::KOBJECT_FRAME;
use capdl::CDL_FrameFillType_t::*;
use capdl::CDL_FrameFill_BootInfoEnum_t::*;
use capdl::CDL_ObjectType::*;
use capdl::*;
use capdl::CDL_FrameFill_BootInfoEnum_t::*;
use capdl::CDL_FrameFillType_t::*;
use capdl::CDL_ObjectType::*;
use crate::KataOsModel;
use log::{debug, info, trace};
use smallvec::SmallVec;
@ -29,8 +28,7 @@ use sel4_sys::seL4_Untyped_Retype;
use sel4_sys::seL4_Word;
use sel4_sys::seL4_WordBits;
use crate::arch::kobject_get_type;
use crate::arch::requires_creation;
use crate::arch;
use static_assertions::assert_cfg;
assert_cfg!(not(feature = "CONFIG_CAPDL_LOADER_STATIC_ALLOC"));
@ -70,7 +68,7 @@ impl<'a> KataOsModel<'a> {
let mut free_slot_index = 0;
for (obj_id, obj) in self.spec.obj_slice().iter()
.enumerate()
.filter(|(_, obj)| requires_creation(obj.r#type()))
.filter(|(_, obj)| arch::requires_creation(obj.r#type()))
{
let free_slot = self.free_slot_start + free_slot_index;
@ -304,7 +302,7 @@ impl<'a> KataOsModel<'a> {
unsafe {
seL4_Untyped_Retype(
ut_slot,
kobject_get_type(KOBJECT_FRAME, seL4_PageBits).into(),
arch::get_frame_type(seL4_PageBits).into(),
seL4_PageBits,
seL4_CapInitThreadCNode,
0,

5
apps/system/components/kata-os-common/src/model/feature/spill_tcb_args.rs
View File

@ -13,6 +13,9 @@ use capdl::*;
use core::mem::size_of;
use core::ptr;
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
use sel4_sys::seL4_ARM_Page_Unify_Instruction;
use sel4_sys::seL4_CapInitThreadVSpace;
use sel4_sys::seL4_CapRights;
use sel4_sys::seL4_CPtr;
@ -109,7 +112,7 @@ impl<'a> KataOsModel<'a> {
};
}
#[cfg(target_arch = "arm")]
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
unsafe { seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE) }?;
unsafe { seL4_Page_Unmap(frame) }?;

10
apps/system/components/kata-os-common/src/model/feature/static_alloc.rs
View File

@ -1,14 +1,14 @@
// Static Object Allocation.
// Expect a statically-allocated capDL spec.
use crate::KataOsModel;
use capdl::CDL_ObjectType::*;
use capdl::*;
use capdl::CDL_ObjectType::*;
use crate::arch;
use crate::KataOsModel;
use log::debug;
use smallvec::SmallVec;
use crate::arch::seL4_ASIDControl_MakePool;
use sel4_sys::seL4_ASIDControl_MakePool;
use sel4_sys::seL4_CapASIDControl;
use sel4_sys::seL4_CapInitThreadCNode;
use sel4_sys::seL4_CPtr;
@ -94,7 +94,7 @@ impl<'a> KataOsModel<'a> {
let untyped_cptr = self.state.get_untyped_cptr(ut_index);
assert!(
!capdl_obj_type.requires_creation(),
!arch::requires_creation(capdl_obj_type),
"Object {} requires dynamic allocation",
obj.name()
);

27
apps/system/components/kata-os-common/src/model/mod.rs
View File

@ -7,7 +7,6 @@
#![allow(non_upper_case_globals)]
#![allow(non_snake_case)]
use capdl::kobject_t::*;
use capdl::CDL_CapType::*;
use capdl::CDL_FrameFillType_t::*;
use capdl::CDL_FrameFill_BootInfoEnum_t::*;
@ -31,7 +30,7 @@ use static_assertions::*;
#[cfg_attr(target_arch = "aarch64", path = "arch/aarch64.rs")]
#[cfg_attr(
all(target_arch = "arm", target_pointer_width = "32"),
path = "arch/arm.rs"
path = "arch/aarch32.rs"
)]
#[cfg_attr(target_arch = "riscv32", path = "arch/riscv32.rs")]
#[cfg_attr(target_arch = "x86", path = "arch/x86.rs")]
@ -40,6 +39,7 @@ mod arch;
use arch::is_irq;
use arch::PAGE_SIZE; // Base page size, typically 4KB
use arch::seL4_Page_Map_Flush; // XXX temp until moved to sel4_sys
// Allocation-specific support
#[cfg_attr(
@ -361,14 +361,14 @@ impl<'a> KataOsModel<'a> {
let arch_type: seL4_ObjectType = match obj.r#type() {
CDL_Frame => {
// Calculate the frame-size-specific cap.
arch::kobject_get_type(KOBJECT_FRAME, obj_size)
arch::get_frame_type(obj_size)
}
CDL_ASIDPool => {
obj_size = seL4_ASIDPoolBits;
seL4_UntypedObject
}
CDL_SchedContext => {
obj_size = arch::kobject_get_size(KOBJECT_SCHED_CONTEXT, obj_size);
obj_size = core::cmp::max(obj_size, seL4_MinSchedContextBits);
CDL_SchedContext.into()
}
obj_type => obj_type.into(),
@ -736,9 +736,13 @@ impl<'a> KataOsModel<'a> {
page_cap.vm_attribs());
// FIXME: Add support for super-pages.
// NB: arch::seL4_Page_Map handles arch-specific work like
// marking the NX bit and invalidating/flushing caches.
let mut result = unsafe { seL4_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs) };
// NB: seL4_Page_Map handles marking the NX bit, we explicitly
// call seL4_Page_Map_Flush to invalidate and/or flush caches.
let mut result = unsafe {
seL4_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs).and_then(|_|
seL4_Page_Map_Flush(self.get_object(page).r#type().into(), sel4_page, rights, vm_attribs)
)
};
#[cfg(feature = "CONFIG_CAPDL_SHARED_FRAMES")]
if result == Err(seL4_InvalidCapability) {
// Page is shared (and already mapped); clone a copy of the page
@ -963,7 +967,8 @@ impl<'a> KataOsModel<'a> {
let target_cap_rights = target_cap.cap_rights();
// For endpoint this is the badge, for cnodes, this is the (encoded) guard.
let target_cap_data = target_cap.cap_data();
#[allow(unused_mut)]
let mut target_cap_data = target_cap.cap_data();
/* To support moving original caps, we need a spec with a CDT (most don't).
* This shoud probably become a separate configuration option for when to
@ -986,13 +991,13 @@ impl<'a> KataOsModel<'a> {
// Use an original cap to reference the object to copy.
let src_root = seL4_CapInitThreadCNode;
let (move_cap, src_index) = match target_cap_type {
#[cfg(target_arch = "x86")]
#[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
CDL_IOSpaceCap => (false, seL4_CapIOSpace),
#[cfg(target_arch = "arm")]
#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
CDL_ARMIOSpaceCap => {
target_cap_data = 0;
(false, first_arm_iospace + target_cap_data)
(false, self.first_arm_iospace + target_cap_data)
}
CDL_IRQHandlerCap => (false, self.get_irq_cap(target_cap_irq)),

1
apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml
View File

@ -62,5 +62,6 @@ CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE = []
path = "lib.rs"
[dependencies]
cfg-if = "1.0"
static_assertions = "1.1"
serde = { version = "1.0", default-features = false, features = ["derive"] }

78
apps/system/components/kata-os-common/src/sel4-sys/arch/aarch32.rs
View File

@ -9,10 +9,21 @@
* @TAG(NICTA_BSD)
*/
use static_assertions::assert_cfg;
assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
use cfg_if::cfg_if;
pub const seL4_WordBits: usize = 32;
pub const seL4_PageBits: usize = 12;
pub const seL4_SlotBits: usize = 4;
pub const seL4_ASIDPoolBits: usize = 12;
pub const seL4_EndpointBits: usize = 4;
pub const seL4_IOPageTableBits: usize = 12;
pub const seL4_LargePageBits: usize = 16;
pub const seL4_PageDirBits: usize = 14;
#[cfg(all(
feature = "CONFIG_HAVE_FPU",
any(
@ -43,15 +54,33 @@ pub const seL4_TCBBits: usize = 10;
)))]
pub const seL4_TCBBits: usize = 9;
pub const seL4_EndpointBits: usize = 4;
cfg_if! {
if #[cfg(feature = "CONFIG_KERNEL_MCS")] {
pub const seL4_NotificationBits: usize = 5;
} else {
pub const seL4_NotificationBits: usize = 4;
}
}
#[cfg(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT")]
cfg_if! {
if #[cfg(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT")] {
pub const seL4_PageTableBits: usize = 12;
#[cfg(not(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT"))]
pub const seL4_PageTableEntryBits: usize = 3;
pub const seL4_PageTableIndexBits: usize = 9;
pub const seL4_SectionBits: usize = 21;
pub const seL4_SuperSectionBits: usize = 25;
pub const seL4_PageDirEntryBits: usize = 3;
pub const seL4_PageDirIndexBits: usize = 11;
} else {
pub const seL4_PageTableBits: usize = 10;
pub const seL4_PageDirBits: usize = 14;
pub const seL4_ASIDPoolBits: usize = 12;
pub const seL4_PageTableEntryBits: usize = 2;
pub const seL4_PageTableIndexBits: usize = 8;
pub const seL4_SectionBits: usize = 20;
pub const seL4_SuperSectionBits: usize = 24;
pub const seL4_PageDirEntryBits: usize = 2;
pub const seL4_PageDirIndexBits: usize = 12;
}
}
pub const seL4_Frame_Args: usize = 4;
pub const seL4_Frame_MRs: usize = 7;
@ -101,7 +130,7 @@ pub enum seL4_ARM_VMAttributes {
ExecuteNever = 4,
}
impl From<u32> for seL4_ARM_VMAttributes {
fn from(val: u32) -> seL4_RISCV_VMAttributes {
fn from(val: u32) -> seL4_ARM_VMAttributes {
unsafe { ::core::mem::transmute(val & 7) }
}
}
@ -109,7 +138,7 @@ pub const seL4_ARM_Default_VMAttributes: seL4_ARM_VMAttributes =
seL4_ARM_VMAttributes::Default;
#[repr(C)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum seL4_ObjectType {
seL4_UntypedObject = 0,
seL4_TCBObject,
@ -137,15 +166,42 @@ pub enum seL4_ObjectType {
seL4_LastObjectType,
}
impl seL4_ObjectType {
// Returns the log2 size of fixed-size objects; typically for use
// with seL4_Retype_Untyped. seL4_UntypedObject has no fixed-size,
// callers must specify a size. seL4_CapTableObject has a per-slot
// fixed-size that callers must scale by the #slots.
// seL4_SchedContextObject size must be in the range
// [seL4_MinSchedContextBits..seL4_MaxSchedContextBits].
pub fn size_bits(&self) -> Option<usize> {
match self {
seL4_TCBObject => Some(seL4_TCBBits),
seL4_EndpointObject => Some(seL4_EndpointBits),
seL4_NotificationObject => Some(seL4_NotificationBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_ReplyObject => Some(seL4_ReplyBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
// NB: caller must scale by #slots
seL4_CapTableObject => Some(seL4_SlotBits),
seL4_ARM_SmallPageObject => Some(seL4_PageBits),
seL4_ARM_LargePageObject => Some(seL4_LargePageBits),
seL4_ARM_SectionObject => Some(seL4_SectionBits),
seL4_ARM_SuperSectionObject => Some(seL4_SuperSectionBits),
seL4_ARM_PageTableObject => Some(seL4_PageTableBits),
seL4_ARM_PageDirectoryObject => Some(seL4_PageDirBits),
_ => None,
}
}
}
impl From<seL4_ObjectType> for seL4_Word {
fn from(type_: seL4_ObjectType) -> seL4_Word {
type_ as seL4_Word
}
}
// NB: capDL is defined using this (sigh)
pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
#[inline(always)]
pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
// Use magic external symbol setup by runtime once TLS is primed

99
apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
View File

@ -9,23 +9,48 @@
* @TAG(NICTA_BSD)
*/
pub const seL4_WordBits: usize = 32;
use static_assertions::assert_cfg;
assert_cfg!(target_arch = "aarch64");
use cfg_if::cfg_if;
pub const seL4_WordBits: usize = 64;
pub const seL4_PageBits: usize = 12;
pub const seL4_SlotBits: usize = 5;
pub const seL4_TCBBits: usize = 11;
#[cfg(feature = "CONFIG_KERNEL_MCS")]
pub const seL4_NotificationBits: usize = 6;
#[cfg(feature = "CONFIG_KERNEL_MCS")]
pub const seL4_ReplyBits: usize = 5;
#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
pub const seL4_NotificationBits: usize = 5;
pub const seL4_EndpointBits: usize = 4;
pub const seL4_PageTableBits: usize = 12;
pub const seL4_PageDirBits: usize = 12;
pub const seL4_ASIDPoolBits: usize = 12;
pub const seL4_EndpointBits: usize = 4;
pub const seL4_IOPageTableBits: usize = 12;
pub const seL4_HugePageBits: usize = 30;
pub const seL4_LargePageBits: usize = 21;
pub const seL4_PageDirBits: usize = 12;
pub const seL4_PageDirIndexBits: usize = 9;
pub const seL4_PageTableBits: usize = 12;
pub const seL4_PageTableIndexBits: usize = 9;
pub const seL4_ReplyBits: usize = 5;
pub const seL4_TCBBits: usize = 11;
cfg_if! {
if #[cfg(feature = "CONFIG_KERNEL_MCS")] {
pub const seL4_NotificationBits: usize = 6;
} else {
pub const seL4_NotificationBits: usize = 5;
}
}
cfg_if! {
if #[cfg(all(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT", feature = "CONFIG_ARM_PA_SIZE_BITS_40"))] {
pub const seL4_PUDIndexBits: usize = 10;
pub const seL4_PUDBits: usize = 13;
pub const seL4_PGDIndexBits: usize = 0;
pub const seL4_PGDBits: usize = 0;
} else {
pub const seL4_PUDIndexBits: usize = 9;
pub const seL4_PUDBits: usize = 12;
pub const seL4_PGDIndexBits: usize = 9;
pub const seL4_PGDBits: usize = 13;
}
}
pub const seL4_Frame_Args: usize = 4;
pub const seL4_Frame_MRs: usize = 7;
@ -42,6 +67,9 @@ pub type seL4_ARM_VSpace = seL4_CPtr;
#[cfg(feature = "arch_generic")]
include!("arm_generic.rs");
pub use seL4_ARM_PageUpperDirectoryObject as seL4_PageUpperDirectoryObject;
pub use seL4_ARM_PageGlobalDirectoryObject as seL4_PageGlobalDirectoryObject;
error_types!(u64);
#[repr(C)]
@ -94,7 +122,7 @@ pub enum seL4_ARM_VMAttributes {
ExecuteNever = 4,
}
impl From<u32> for seL4_ARM_VMAttributes {
fn from(val: u32) -> seL4_RISCV_VMAttributes {
fn from(val: u32) -> seL4_ARM_VMAttributes {
unsafe { ::core::mem::transmute(val & 7) }
}
}
@ -102,7 +130,7 @@ pub const seL4_ARM_Default_VMAttributes: seL4_ARM_VMAttributes =
seL4_ARM_VMAttributes::Default;
#[repr(C)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum seL4_ObjectType {
seL4_UntypedObject = 0,
seL4_TCBObject,
@ -115,6 +143,10 @@ pub enum seL4_ObjectType {
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_ReplyObject,
seL4_ARM_HugePageObject,
seL4_ARM_PageUpperDirectoryObject,
seL4_ARM_PageGlobalDirectoryObject,
seL4_ARM_SmallPageObject,
seL4_ARM_LargePageObject,
seL4_ARM_PageTableObject,
@ -125,6 +157,40 @@ pub enum seL4_ObjectType {
#[cfg(feature = "CONFIG_TK1_SMMU")]
seL4_ARM_IOPageTableObject,
seL4_LastObjectType,
}
impl seL4_ObjectType {
// Returns the log2 size of fixed-size objects; typically for use
// with seL4_Retype_Untyped. seL4_UntypedObject has no fixed-size,
// callers must specify a size. seL4_CapTableObject has a per-slot
// fixed-size that callers must scale by the #slots.
// seL4_SchedContextObject size must be in the range
// [seL4_MinSchedContextBits..seL4_MaxSchedContextBits].
pub fn size_bits(&self) -> Option<usize> {
match self {
seL4_TCBObject => Some(seL4_TCBBits),
seL4_EndpointObject => Some(seL4_EndpointBits),
seL4_NotificationObject => Some(seL4_EndpointBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_ReplyObject => Some(seL4_ReplyBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
// NB: caller must scale by #slots
seL4_CapTableObject => Some(seL4_SlotBits),
seL4_ARM_HugePageObject => Some(seL4_HugePageBits),
seL4_ARM_PageUpperDirectoryObject => Some(seL4_PUDBits),
seL4_ARM_PageGlobalDirectoryObject => Some(seL4_PGDBits),
seL4_ARM_SmallPageObject => Some(seL4_PageBits),
seL4_ARM_LargePageObject => Some(seL4_LargePageBits),
seL4_ARM_PageTableObject => Some(seL4_PageTableBits),
seL4_ARM_PageDirectoryObject => Some(seL4_PageDirBits),
_ => None,
}
}
}
impl From<seL4_ObjectType> for seL4_Word {
fn from(type_: seL4_ObjectType) -> seL4_Word {
@ -132,9 +198,6 @@ impl From<seL4_ObjectType> for seL4_Word {
}
}
// NB: capDL is defined using this (sigh)
// pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
#[inline(always)]
pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
// Use magic external symbol setup by runtime once TLS is primed

18
apps/system/components/kata-os-common/src/sel4-sys/arch/arm_generic.rs
View File

@ -17,5 +17,21 @@ pub use seL4_ARM_ASIDControl_MakePool as seL4_ASIDControl_MakePool;
pub use seL4_ARM_ASIDPool_Assign as seL4_ASIDPool_Assign;
pub use seL4_ARM_PageTable_Map as seL4_PageTable_Map;
pub use seL4_ARM_Page_GetAddress as seL4_Page_GetAddress;
pub use seL4_ARM_Page_Map as seL4_Page_Map;
// NB: seL4_Page_Map impl found below
pub use seL4_ARM_Page_Unmap as seL4_Page_Unmap;
pub unsafe fn seL4_Page_Map(
sel4_page: seL4_CPtr,
sel4_pd: seL4_CPtr,
vaddr: seL4_Word,
rights: seL4_CapRights,
vm_attribs: seL4_VMAttributes,
) -> seL4_Result {
if rights.get_capAllowGrant() != 0 {
// NB: executable
seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs)
} else {
seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights,
seL4_ARM_VMAttributes::ExecuteNever)
}
}

5
apps/system/components/kata-os-common/src/sel4-sys/arch/riscv32.rs
View File

@ -130,7 +130,9 @@ impl seL4_ObjectType {
seL4_TCBObject => Some(seL4_TCBBits),
seL4_EndpointObject => Some(seL4_EndpointBits),
seL4_NotificationObject => Some(seL4_EndpointBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_ReplyObject => Some(seL4_ReplyBits),
#[cfg(feature = "CONFIG_KERNEL_MCS")]
seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
// NB: caller must scale by #slots
seL4_CapTableObject => Some(seL4_SlotBits),
@ -152,9 +154,6 @@ impl From<seL4_ObjectType> for seL4_Word {
}
}
// NB: capDL is defined using this (sigh)
pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
#[inline(always)]
pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
// Use magic external symbol setup by runtime once TLS is primed

5
apps/system/components/kata-os-common/src/sel4-sys/arch/x86.rs
View File

@ -51,7 +51,7 @@ include!("x86_generic.rs");
error_types!(u32);
#[repr(C)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum seL4_ObjectType {
seL4_UntypedObject = 0,
seL4_TCBObject,
@ -91,9 +91,6 @@ impl From<seL4_ObjectType> for seL4_Word {
}
}
// NB: capDL is defined using this (sigh)
pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
#[repr(u32)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum seL4_X86_VMAttributes {

5
apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
View File

@ -53,7 +53,7 @@ include!("x86_generic.rs");
error_types!(u64);
#[repr(C)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum seL4_ObjectType {
seL4_UntypedObject = 0,
seL4_TCBObject,
@ -98,9 +98,6 @@ impl From<seL4_ObjectType> for seL4_Word {
}
}
// NB: capDL is defined using this (sigh)
pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
#[repr(u32)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum seL4_X86_VMAttributes {

3
apps/system/components/kata-os-common/src/sel4-sys/lib.rs
View File

@ -161,6 +161,9 @@ pub type seL4_Untyped = seL4_CPtr;
// TODO(sleffler): seL4 uses seL4_Uint64 but it's not defined for us
pub type seL4_Time = u64;
// NB: capDL CDL_ObjectType is defined using this (sigh)
pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
pub const seL4_MsgLengthBits: usize = 7;
pub const seL4_MsgMaxLength: usize = 120;
pub const seL4_MsgExtraCapBits: usize = 2;