diff --git a/tool/microkit/__main__.py b/tool/microkit/__main__.py index a4359307..601c73ff 100644 --- a/tool/microkit/__main__.py +++ b/tool/microkit/__main__.py @@ -108,7 +108,7 @@ SEL4_OBJECT_TYPE_NAMES, ) from microkit.sysxml import ProtectionDomain, xml2system, SystemDescription, PlatformDescription -from microkit.sysxml import SysMap, SysMemoryRegion # This shouldn't be needed here as such +from microkit.sysxml import SysMap, SysMemoryRegion # This shouldn't be needed here as such from microkit.loader import Loader # This is a workaround for: https://github.com/indygreg/PyOxidizer/issues/307 @@ -120,9 +120,10 @@ default_platform_description = PlatformDescription( - page_sizes = (0x1_000, 0x200_000) + page_sizes=(0x1_000, 0x200_000) ) + @dataclass class MonitorConfig: untyped_info_symbol_name: str @@ -135,6 +136,7 @@ class MonitorConfig: def max_untyped_objects(self, symbol_size: int) -> int: return (symbol_size - self.untyped_info_header_struct.size) // self.untyped_info_object_struct.size + # The monitor config is fixed (unless the monitor C code # changes the definitions of struct, or the name. # While this is fixed, we dynamically determine the @@ -142,12 +144,12 @@ def max_untyped_objects(self, symbol_size: int) -> int: # to allow for minor changes in the C code without requiring # rework of this tool MONITOR_CONFIG = MonitorConfig( - untyped_info_symbol_name = "untyped_info", - untyped_info_header_struct = Struct(" int: def end(self) -> int: return self.untyped_object.region.end + class KernelObjectAllocator: """Allocator for kernel objects. @@ -213,6 +216,7 @@ class KernelObjectAllocator: as the allocations are made. """ + def __init__(self, kernel_boot_info: KernelBootInfo) -> None: self._allocation_idx = 0 self._untyped = [] @@ -287,14 +291,13 @@ def overlaps(range1: Tuple[int, int], range2: Tuple[int, int]) -> bool: if base1 >= base2 + size2: # range1 is completely above range2 return False - if base1 + size1 <= base2: + if base1 + size1 <= base2: # range1 is completely below range2 return False # otherwise there is some overlap return True - def phys_mem_regions_from_elf(elf: ElfFile, alignment: int) -> List[MemoryRegion]: """Determine the physical memory regions for an ELF file with a given alignment. @@ -369,6 +372,7 @@ def __str__(self) -> str: def __contains__(self, address: int) -> bool: return self._ut.region.base <= address < self._ut.region.end + @dataclass(frozen=True, eq=True) class KernelObject: """Represents an allocated kernel object. @@ -431,16 +435,16 @@ def human_size_strict(size: int) -> str: class InitSystem: def __init__( - self, - kernel_config: KernelConfig, - cnode_cap: int, - cnode_mask: int, - first_available_cap_slot: int, - kernel_object_allocator: KernelObjectAllocator, - kernel_boot_info: KernelBootInfo, - invocations: List[Sel4Invocation], - cap_address_names: Dict[int, str], - ): + self, + kernel_config: KernelConfig, + cnode_cap: int, + cnode_mask: int, + first_available_cap_slot: int, + kernel_object_allocator: KernelObjectAllocator, + kernel_boot_info: KernelBootInfo, + invocations: List[Sel4Invocation], + cap_address_names: Dict[int, str], + ): self._cnode_cap = cnode_cap self._cnode_mask = cnode_mask self._kernel_config = kernel_config @@ -465,7 +469,6 @@ def reserve(self, allocations: List[Tuple[UntypedObject, int]]) -> None: ut.watermark = alloc_phys_addr - def allocate_fixed_objects(self, phys_address: int, object_type: int, count: int, names: List[str]) -> List[KernelObject]: """ @@ -511,28 +514,28 @@ def allocate_fixed_objects(self, phys_address: int, object_type: int, count: int for sz in padding_sizes: self._invocations.append(Sel4UntypedRetype( - ut._ut.cap, - SEL4_UNTYPED_OBJECT, - int(log2(sz)), - self._cnode_cap, - 1, - 1, - self._cap_slot, - 1 + ut._ut.cap, + SEL4_UNTYPED_OBJECT, + int(log2(sz)), + self._cnode_cap, + 1, + 1, + self._cap_slot, + 1 )) self._cap_slot += 1 object_cap = self._cap_slot self._cap_slot += 1 self._invocations.append(Sel4UntypedRetype( - ut._ut.cap, - object_type, - 0, - self._cnode_cap, - 1, - 1, - object_cap, - 1 + ut._ut.cap, + object_type, + 0, + self._cnode_cap, + 1, + 1, + object_cap, + 1 )) ut.watermark = phys_address + alloc_size @@ -564,14 +567,14 @@ def allocate_objects(self, object_type: int, names: List[str], size: Optional[in while to_alloc: call_count = min(to_alloc, self._kernel_config.fan_out_limit) self._invocations.append(Sel4UntypedRetype( - allocation.untyped_cap_address, - object_type, - api_size, - self._cnode_cap, - 1, - 1, - alloc_cap_slot, - call_count + allocation.untyped_cap_address, + object_type, + api_size, + self._cnode_cap, + 1, + 1, + alloc_cap_slot, + call_count )) to_alloc -= call_count alloc_cap_slot += call_count @@ -629,14 +632,14 @@ def _get_full_path(filename: Path, search_paths: List[Path]) -> Path: def build_system( - kernel_config: KernelConfig, - kernel_elf: ElfFile, - monitor_elf: ElfFile, - system: SystemDescription, - invocation_table_size: int, - system_cnode_size: int, - search_paths: List[Path], - ) -> BuiltSystem: + kernel_config: KernelConfig, + kernel_elf: ElfFile, + monitor_elf: ElfFile, + system: SystemDescription, + invocation_table_size: int, + system_cnode_size: int, + search_paths: List[Path], +) -> BuiltSystem: """Build system as description by the inputs, with a 'BuiltSystem' object as the output.""" assert is_power_of_two(system_cnode_size) assert invocation_table_size % kernel_config.minimum_page_size == 0 @@ -656,17 +659,16 @@ def build_system( # Emulate kernel boot - ## Determine physical memory region used by the monitor + # Determine physical memory region used by the monitor initial_task_size = phys_mem_region_from_elf(monitor_elf, kernel_config.minimum_page_size).size - ## Get the elf files for each pd: + # Get the elf files for each pd: pd_elf_files = { pd: ElfFile.from_path(_get_full_path(pd.program_image, search_paths)) for pd in system.protection_domains } - ### Here we should validate that ELF files - ## Determine physical memory region for 'reserved' memory. + # Determine physical memory region for 'reserved' memory. # # The 'reserved' memory region will not be touched by seL4 during boot # and allows the monitor (initial task) to create memory regions @@ -736,7 +738,6 @@ def build_system( # pd.maps.append(mp) pd_elf_regions[pd] = tuple(elf_regions) - # 1.3 With both the initial task region and reserved region determined the kernel # boot can be emulated. This provides the boot info information which is needed # for the next steps @@ -792,7 +793,7 @@ def build_system( # slot 1: our main system cnode root_cnode_bits = 1 root_cnode_allocation = kao.alloc((1 << root_cnode_bits) * (1 << SLOT_BITS)) - root_cnode_cap = kernel_boot_info.first_available_cap + root_cnode_cap = kernel_boot_info.first_available_cap cap_address_names[root_cnode_cap] = "CNode: root" # 2.1.2: Allocate the *system* CNode. It is the cnodes that @@ -808,14 +809,14 @@ def build_system( bootstrap_invocations: List[Sel4Invocation] = [] bootstrap_invocations.append(Sel4UntypedRetype( - root_cnode_allocation.untyped_cap_address, - SEL4_CNODE_OBJECT, - root_cnode_bits, - INIT_CNODE_CAP_ADDRESS, - 0, - 0, - root_cnode_cap, - 1 + root_cnode_allocation.untyped_cap_address, + SEL4_CNODE_OBJECT, + root_cnode_bits, + INIT_CNODE_CAP_ADDRESS, + 0, + 0, + root_cnode_cap, + 1 )) # 2.1.4: Now insert a cap to the initial Cnode into slot zero of the newly @@ -899,7 +900,7 @@ def build_system( # page size. It would be good in the future to use super pages (when # it makes sense to - this would reduce memory usage, and the number of # invocations required to set up the address space - pages_required= invocation_table_size // kernel_config.minimum_page_size + pages_required = invocation_table_size // kernel_config.minimum_page_size remaining_pages = pages_required invocation_table_allocations = [] phys_addr = invocation_table_region.base @@ -913,14 +914,14 @@ def build_system( retype_page_count = min(ut_pages, remaining_pages) assert retype_page_count <= kernel_config.fan_out_limit bootstrap_invocations.append(Sel4UntypedRetype( - ut.cap, - SEL4_SMALL_PAGE_OBJECT, - 0, - root_cnode_cap, - 1, - 1, - cap_slot, - retype_page_count + ut.cap, + SEL4_SMALL_PAGE_OBJECT, + 0, + root_cnode_cap, + 1, + 1, + cap_slot, + retype_page_count )) remaining_pages -= retype_page_count @@ -947,14 +948,14 @@ def build_system( assert page_tables_required <= kernel_config.fan_out_limit bootstrap_invocations.append(Sel4UntypedRetype( - page_table_allocation.untyped_cap_address, - SEL4_PAGE_TABLE_OBJECT, - 0, - root_cnode_cap, - 1, - 1, - cap_slot, - page_tables_required + page_table_allocation.untyped_cap_address, + SEL4_PAGE_TABLE_OBJECT, + 0, + root_cnode_cap, + 1, + 1, + cap_slot, + page_tables_required )) cap_slot += page_tables_required @@ -970,7 +971,6 @@ def build_system( invocation.repeat(pages_required, page=1, vaddr=kernel_config.minimum_page_size) bootstrap_invocations.append(invocation) - # 3. Now we can start setting up the system based on the information # the user provided in the system xml. # @@ -989,7 +989,6 @@ def build_system( # Page table structs: # as needed by protection domains based on mappings required - phys_addr_next = reserved_base + invocation_table_size # Now we create additional MRs (and mappings) for the ELF files. regions: List[Region] = [] @@ -1043,7 +1042,7 @@ def build_system( if mr.phys_addr is not None: continue page_size_human = human_size_strict(mr.page_size) - page_names_by_size[mr.page_size] += [f"Page({page_size_human}): MR={mr.name} #{idx}" for idx in range(mr.page_count)] + page_names_by_size[mr.page_size] += [f"Page({page_size_human}): MR={mr.name} #{idx}" for idx in range(mr.page_count)] page_objects: Dict[int, List[KernelObject]] = {} @@ -1066,7 +1065,7 @@ def build_system( # First we need to find all the requested pages and sorted them fixed_pages = [] - for mr in all_mrs: #system.memory_regions: + for mr in all_mrs: # system.memory_regions: if mr.phys_addr is None: continue phys_addr = mr.phys_addr @@ -1096,7 +1095,7 @@ def build_system( schedcontext_caps = [sc.cap_addr for sc in schedcontext_objects] pp_protection_domains = [pd for pd in system.protection_domains if pd.pp] endpoint_names = ["EP: Monitor Fault"] + [f"EP: PD={pd.name}" for pd in pp_protection_domains] - reply_names = ["Reply: Monitor"]+ [f"Reply: PD={pd.name}" for pd in system.protection_domains] + reply_names = ["Reply: Monitor"] + [f"Reply: PD={pd.name}" for pd in system.protection_domains] reply_objects = init_system.allocate_objects(SEL4_REPLY_OBJECT, reply_names) reply_object = reply_objects[0] # FIXME: Probably only need reply objects for PPs @@ -1206,7 +1205,7 @@ def build_system( for pd_idx, pd in enumerate(system.protection_domains): for mp in (pd.maps + pd_extra_maps[pd]): vaddr = mp.vaddr - mr = all_mr_by_name[mp.mr] #system.mr_by_name[mp.mr] + mr = all_mr_by_name[mp.mr] # system.mr_by_name[mp.mr] rights = 0 attrs = SEL4_ARM_PARITY_ENABLED if "r" in mp.perms: @@ -1268,7 +1267,7 @@ def build_system( final_cap_slot = cap_slot - ## Minting in the address space + # Minting in the address space for pd, notification_obj, cnode_obj in zip(system.protection_domains, notification_objects, cnode_objects): obj = pp_ep_endpoint_objects[pd] if pd.pp else notification_obj assert INPUT_CAP_IDX < PD_CAP_SIZE @@ -1289,13 +1288,13 @@ def build_system( invocation.repeat(len(system.protection_domains), cnode=1, src_obj=1) system_invocations.append(invocation) - ## Mint access to the vspace cap + # Mint access to the vspace cap assert VSPACE_CAP_IDX < PD_CAP_SIZE invocation = Sel4CnodeMint(cnode_objects[0].cap_addr, VSPACE_CAP_IDX, PD_CAP_BITS, root_cnode_cap, vspace_objects[0].cap_addr, kernel_config.cap_address_bits, SEL4_RIGHTS_ALL, 0) invocation.repeat(len(system.protection_domains), cnode=1, src_obj=1) system_invocations.append(invocation) - ## Mint access to interrupt handlers in the PD Cspace + # Mint access to interrupt handlers in the PD Cspace for cnode_obj, pd in zip(cnode_objects, system.protection_domains): for sysirq, irq_cap_address in zip(pd.irqs, irq_cap_addresses[pd]): cap_idx = BASE_IRQ_CAP + sysirq.id_ @@ -1335,7 +1334,7 @@ def build_system( root_cnode_cap, pd_b_notification_obj.cap_addr, kernel_config.cap_address_bits, - SEL4_RIGHTS_ALL, # FIXME: Check rights + SEL4_RIGHTS_ALL, # FIXME: Check rights pd_a_badge) ) @@ -1351,7 +1350,7 @@ def build_system( root_cnode_cap, pd_a_notification_obj.cap_addr, kernel_config.cap_address_bits, - SEL4_RIGHTS_ALL, # FIXME: Check rights + SEL4_RIGHTS_ALL, # FIXME: Check rights pd_b_badge) ) @@ -1370,7 +1369,7 @@ def build_system( root_cnode_cap, pd_b_endpoint_obj.cap_addr, kernel_config.cap_address_bits, - SEL4_RIGHTS_ALL, # FIXME: Check rights + SEL4_RIGHTS_ALL, # FIXME: Check rights pd_a_badge) ) @@ -1388,7 +1387,7 @@ def build_system( root_cnode_cap, pd_a_endpoint_obj.cap_addr, kernel_config.cap_address_bits, - SEL4_RIGHTS_ALL, # FIXME: Check rights + SEL4_RIGHTS_ALL, # FIXME: Check rights pd_b_badge) ) @@ -1396,14 +1395,14 @@ def build_system( for idx, (cnode_obj, pd) in enumerate(zip(cnode_objects, system.protection_domains), 1): if pd.passive: system_invocations.append(Sel4CnodeMint( - cnode_obj.cap_addr, - MONITOR_EP_CAP_IDX, - PD_CAP_BITS, - root_cnode_cap, - fault_ep_endpoint_object.cap_addr, - kernel_config.cap_address_bits, - SEL4_RIGHTS_ALL, - idx)) + cnode_obj.cap_addr, + MONITOR_EP_CAP_IDX, + PD_CAP_BITS, + root_cnode_cap, + fault_ep_endpoint_object.cap_addr, + kernel_config.cap_address_bits, + SEL4_RIGHTS_ALL, + idx)) # All minting is complete at this point # Associate badges @@ -1412,7 +1411,6 @@ def build_system( for irq_cap_address, badged_notification_cap_address in zip(irq_cap_addresses[pd], badged_irq_caps[pd]): system_invocations.append(Sel4IrqHandlerSetNotification(irq_cap_address, badged_notification_cap_address)) - # Initialise the VSpaces -- assign them all the the initial asid pool. for map_cls, descriptors, objects in [ (Sel4PageUpperDirectoryMap, uds, ud_objects), @@ -1486,7 +1484,7 @@ def build_system( Sel4TcbWriteRegisters( tcb_obj.cap_addr, False, - 0, # no flags on ARM + 0, # no flags on ARM Sel4Aarch64Regs(pc=pd_elf_files[pd].entry) ) ) @@ -1509,7 +1507,6 @@ def build_system( for system_invocation in system_invocations: system_invocation_data += system_invocation._get_raw_invocation() - for pd in system.protection_domains: # Could use pd.elf_file.write_symbol here to update variables if required. pd_elf_files[pd].write_symbol("microkit_name", pack("<16s", pd.name.encode("utf8"))) @@ -1532,22 +1529,22 @@ def build_system( raise Exception(f"Unable to patch variable '{setvar.symbol}' in protection domain: '{pd.name}': variable not found.") return BuiltSystem( - number_of_system_caps = final_cap_slot, #init_system._cap_slot, - invocation_data_size = len(system_invocation_data), - bootstrap_invocations = bootstrap_invocations, - system_invocations = system_invocations, - kernel_boot_info = kernel_boot_info, - reserved_region = reserved_region, - fault_ep_cap_address = fault_ep_endpoint_object.cap_addr, - reply_cap_address = reply_object.cap_addr, - cap_lookup = cap_address_names, - tcb_caps = tcb_caps, - sched_caps = schedcontext_caps, - ntfn_caps = notification_caps, - regions = regions, - kernel_objects = init_system._objects, - initial_task_phys_region = initial_task_phys_region, - initial_task_virt_region = initial_task_virt_region, + number_of_system_caps=final_cap_slot, # init_system._cap_slot, + invocation_data_size=len(system_invocation_data), + bootstrap_invocations=bootstrap_invocations, + system_invocations=system_invocations, + kernel_boot_info=kernel_boot_info, + reserved_region=reserved_region, + fault_ep_cap_address=fault_ep_endpoint_object.cap_addr, + reply_cap_address=reply_object.cap_addr, + cap_lookup=cap_address_names, + tcb_caps=tcb_caps, + sched_caps=schedcontext_caps, + ntfn_caps=notification_caps, + regions=regions, + kernel_objects=init_system._objects, + initial_task_phys_region=initial_task_phys_region, + initial_task_virt_region=initial_task_virt_region, ) @@ -1622,11 +1619,11 @@ def main() -> int: # FIXME: The kernel config should be an output of the kernel # build step (or embedded into the kernel elf file in some manner kernel_config = KernelConfig( - word_size = 64, - minimum_page_size = kb(4), - paddr_user_device_top = (1 << 40), - kernel_frame_size = (1 << 12), - init_cnode_bits = 12, + word_size=64, + minimum_page_size=kb(4), + paddr_user_device_top=(1 << 40), + kernel_frame_size=(1 << 12), + init_cnode_bits=12, cap_address_bits=64, fan_out_limit=256 ) @@ -1649,8 +1646,8 @@ def main() -> int: search_paths, ) print(f"BUILT: {system_cnode_size=} {built_system.number_of_system_caps=} {invocation_table_size=} {built_system.invocation_data_size=}") - if (built_system.number_of_system_caps <= system_cnode_size and - built_system.invocation_data_size <= invocation_table_size): + if (built_system.number_of_system_caps <= system_cnode_size + and built_system.invocation_data_size <= invocation_table_size): break # Recalculate the sizes for the next iteration @@ -1674,9 +1671,9 @@ def main() -> int: if len(built_system.kernel_boot_info.untyped_objects) > max_untyped_objects: raise Exception(f"Too many untyped objects: monitor ({monitor_elf_path}) supports {max_untyped_objects:,d} regions. System has {len(built_system.kernel_boot_info.untyped_objects):,d} objects.") untyped_info_header = MONITOR_CONFIG.untyped_info_header_struct.pack( - built_system.kernel_boot_info.untyped_objects[0].cap, - built_system.kernel_boot_info.untyped_objects[-1].cap + 1 - ) + built_system.kernel_boot_info.untyped_objects[0].cap, + built_system.kernel_boot_info.untyped_objects[-1].cap + 1 + ) untyped_info_object_data = [] for idx, ut in enumerate(built_system.kernel_boot_info.untyped_objects): object_data = MONITOR_CONFIG.untyped_info_object_struct.pack(ut.base, ut.size_bits, ut.is_device) @@ -1722,10 +1719,9 @@ def main() -> int: names_array = bytearray([0] * (64 * 16)) for idx, pd in enumerate(system_description.protection_domains, 1): nm = pd.name.encode("utf8")[:15] - names_array[idx * 16:idx * 16+len(nm)] = nm + names_array[idx * 16:idx * 16 + len(nm)] = nm monitor_elf.write_symbol("pd_names", names_array) - # B: The loader # B.1: The loader is primarily about loading 'regions' of memory. diff --git a/tool/microkit/elf.py b/tool/microkit/elf.py index 36912c34..a972815a 100644 --- a/tool/microkit/elf.py +++ b/tool/microkit/elf.py @@ -44,6 +44,7 @@ class SegmentType(IntEnum): PT_SHLID = 5 PT_PHDR = 6 + class SegmentAttributes(IntFlag): PF_X = 0x1 PF_W = 0x2 @@ -163,6 +164,7 @@ class ElfVersion(IntEnum): "size", ) + class InvalidElf(Exception): pass @@ -302,7 +304,6 @@ def from_path(cls, path: Path) -> "ElfFile": zeros = bytes(phent.memsz - phent.filesz) elf.segments.append(ElfSegment(phent.paddr, phent.vaddr, bytearray(data + zeros), phent.type_ == 1, SegmentAttributes(phent.flags))) - # FIXME: Add support for sections and symbols f.seek(hdr.shoff) shents = [] @@ -353,7 +354,7 @@ def write(self, path: Path) -> None: ident_version=ElfVersion.EV_CURRENT, ident_osabi=OperatingSystemAbi.ELFOSABI_STANDALINE, ident_abiversion=0, - type_ = ObjectFileType.ET_EXEC, + type_=ObjectFileType.ET_EXEC, machine=MachineType.EM_AARCH64, version=ElfVersion.EV_CURRENT, entry=self.entry, @@ -375,15 +376,15 @@ def write(self, path: Path) -> None: data_offset = ehsize + len(self.segments) * phentsize for segment in self.segments: pheader = ElfProgramHeader( - type_ = SegmentType.PT_LOAD, - offset = data_offset, - vaddr = segment.virt_addr, - paddr = segment.phys_addr, - filesz = segment.mem_size, - memsz = segment.mem_size, + type_=SegmentType.PT_LOAD, + offset=data_offset, + vaddr=segment.virt_addr, + paddr=segment.phys_addr, + filesz=segment.mem_size, + memsz=segment.mem_size, # FIXME: Need to do something better with permissions in the future! - flags = SegmentAttributes.PF_R | SegmentAttributes.PF_W | SegmentAttributes.PF_X, - align = 1, + flags=SegmentAttributes.PF_R | SegmentAttributes.PF_W | SegmentAttributes.PF_X, + align=1, ) pheader_bytes = ELF_PROGRAM_HEADER64.pack(*(getattr(pheader, field) for field in ELF_PROGRAM_HEADER64_FIELDS)) f.write(pheader_bytes) @@ -392,19 +393,17 @@ def write(self, path: Path) -> None: for segment in self.segments: f.write(segment.data) - def add_segment(self, segment: ElfSegment) -> None: # TODO: Check that the segment doesn't overlap any existing # segment # TODO: We may want to keep segments in order. self.segments.append(segment) - def get_data(self, vaddr: int, size: int) -> bytes: for seg in self.segments: if vaddr >= seg.virt_addr and vaddr + size <= seg.virt_addr + len(seg.data): offset = vaddr - seg.virt_addr - return seg.data[offset:offset+size] + return seg.data[offset:offset + size] raise Exception(f"Unable to find data for vaddr=0x{vaddr:x} size=0x{size:x}") @@ -414,8 +413,7 @@ def write_symbol(self, variable_name: str, data: bytes) -> None: if vaddr >= seg.virt_addr and vaddr + size <= seg.virt_addr + len(seg.data): offset = vaddr - seg.virt_addr assert len(data) <= size - seg.data[offset:offset+len(data)] = data - + seg.data[offset:offset + len(data)] = data # def read(self, offset: int, size: int) -> bytes: # self._f.seek(offset) @@ -442,11 +440,10 @@ def find_symbol(self, variable_name: str) -> Tuple[int, int]: raise KeyError(f"No symbol named {variable_name} found") # symbol_type = found_sym.info & 0xf # symbol_binding = found_sym.info >> 4 - #if symbol_type != 1: + # if symbol_type != 1: # raise Exception(f"Unexpected symbol type {symbol_type}. Expect STT_OBJECT") return found_sym.value, found_sym.size def read_struct(self, variable_name: str, struct_: Struct) -> Tuple[int, ...]: vaddr, size = self.find_symbol(variable_name) return struct_.unpack_from(self.get_data(vaddr, size)) - diff --git a/tool/microkit/loader.py b/tool/microkit/loader.py index b5c0f24d..55f28afc 100644 --- a/tool/microkit/loader.py +++ b/tool/microkit/loader.py @@ -20,6 +20,7 @@ PAGE_TABLE_SIZE = 4096 + def mask(x: int) -> int: return ((1 << x) - 1) @@ -62,29 +63,30 @@ def _check_non_overlapping(regions: List[Tuple[int, bytes]]) -> None: checked.append((base, end)) + class Loader: def __init__(self, - loader_elf_path: Path, - kernel_elf: ElfFile, - initial_task_elf: ElfFile, - initial_task_phys_base: Optional[int], - reserved_region: MemoryRegion, - regions: List[Tuple[int, bytes]] - ) -> None: + loader_elf_path: Path, + kernel_elf: ElfFile, + initial_task_elf: ElfFile, + initial_task_phys_base: Optional[int], + reserved_region: MemoryRegion, + regions: List[Tuple[int, bytes]] + ) -> None: """ Note: If initial_task_phys_base is not None, then it just this address as the base physical address of the initial task, rather than the address that comes from the initial_task_elf file. """ - # Setup the pagetable data structures (directly embedded in the loader) + # Setup the pagetable data structures (directly embedded in the loader) self._elf = ElfFile.from_path(loader_elf_path) sz = self._elf.word_size self._header_struct_fmt = " ui_p_reg_start) + assert (ui_p_reg_end > ui_p_reg_start) v_entry = initial_task_elf.entry extra_device_addr_p = reserved_region.base @@ -210,33 +210,33 @@ def _setup_pagetables(self, first_vaddr: int, first_paddr: int) -> Dict[str, byt for i in range(512): pt_entry = ( (i << AARCH64_1GB_BLOCK_BITS) | - (1 << 10) | # access flag - (0 << 2) | # strongly ordered memory - (1) # 1G block + (1 << 10) | # access flag + (0 << 2) | # strongly ordered memory + (1) # 1G block ) - boot_lvl1_lower[8*i:8*(i+1)] = pack(" int: def _get_arch_n_paging(region: MemoryRegion) -> int: - PT_INDEX_OFFSET = 12 - PD_INDEX_OFFSET = (PT_INDEX_OFFSET + 9) - PUD_INDEX_OFFSET = (PD_INDEX_OFFSET + 9) - PGD_INDEX_OFFSET = (PUD_INDEX_OFFSET + 9) + PT_INDEX_OFFSET = 12 + PD_INDEX_OFFSET = (PT_INDEX_OFFSET + 9) + PUD_INDEX_OFFSET = (PD_INDEX_OFFSET + 9) + PGD_INDEX_OFFSET = (PUD_INDEX_OFFSET + 9) return ( _get_n_paging(region, PGD_INDEX_OFFSET) + @@ -152,9 +152,9 @@ def calculate_rootserver_size(initial_task_region: MemoryRegion) -> int: tcb_bits = 11 # seL4_TCBBits page_bits = 12 # seL4_PageBits asid_pool_bits = 12 # seL4_ASIDPoolBits - vspace_bits = 12 #seL4_VSpaceBits + vspace_bits = 12 # seL4_VSpaceBits page_table_bits = 12 # seL4_PageTableBits - min_sched_context_bits = 8 # seL4_MinSchedContextBits + min_sched_context_bits = 8 # seL4_MinSchedContextBits size = 0 size += 1 << (root_cnode_bits + slot_bits) @@ -163,7 +163,7 @@ def calculate_rootserver_size(initial_task_region: MemoryRegion) -> int: size += 1 << asid_pool_bits size += 1 << vspace_bits size += _get_arch_n_paging(initial_task_region) * (1 << page_table_bits) - size += 1 < int: @@ -263,43 +264,43 @@ def count(self) -> int: return len(self.as_tuple()) def as_tuple(self) -> Tuple[int, ...]: - raw = ( - self.pc , - self.sp , - self.spsr , - self.x0 , - self.x1 , - self.x2 , - self.x3 , - self.x4 , - self.x5 , - self.x6 , - self.x7 , - self.x8 , - self.x16 , - self.x17 , - self.x18 , - self.x29 , - self.x30 , - self.x9 , - self.x10 , - self.x11 , - self.x12 , - self.x13 , - self.x14 , - self.x15 , - self.x19 , - self.x20 , - self.x21 , - self.x22 , - self.x23 , - self.x24 , - self.x25 , - self.x26 , - self.x27 , - self.x28 , - self.tpidr_el0 , - self.tpidrro_el0, + raw = ( + self.pc, + self.sp, + self.spsr, + self.x0, + self.x1, + self.x2, + self.x3, + self.x4, + self.x5, + self.x6, + self.x7, + self.x8, + self.x16, + self.x17, + self.x18, + self.x29, + self.x30, + self.x9, + self.x10, + self.x11, + self.x12, + self.x13, + self.x14, + self.x15, + self.x19, + self.x20, + self.x21, + self.x22, + self.x23, + self.x24, + self.x25, + self.x26, + self.x27, + self.x28, + self.tpidr_el0, + self.tpidrro_el0, ) return tuple(0 if x is None else x for x in raw) @@ -374,7 +375,7 @@ class Sel4Label(IntEnum): ARMIRQIssueIRQHandlerTrigger = 55 -### Invocations +# Invocations class Sel4Invocation: label: Sel4Label @@ -518,6 +519,7 @@ def _get_raw_invocation(self) -> bytes: return self._generic_invocation((), params) + @dataclass class Sel4TcbBindNotification(Sel4Invocation): _object_type = "TCB" @@ -625,6 +627,7 @@ class Sel4CnodeMint(Sel4Invocation): rights: int badge: int + @dataclass class Sel4CnodeCopy(Sel4Invocation): _object_type = "CNode" @@ -639,6 +642,7 @@ class Sel4CnodeCopy(Sel4Invocation): src_depth: int rights: int + @dataclass class Sel4CnodeMutate(Sel4Invocation): _object_type = "CNode" @@ -653,6 +657,7 @@ class Sel4CnodeMutate(Sel4Invocation): src_depth: int badge: int + @dataclass class Sel4SchedControlConfigureFlags(Sel4Invocation): _object_type = "SchedControl" @@ -667,6 +672,7 @@ class Sel4SchedControlConfigureFlags(Sel4Invocation): badge: int flags: int + @dataclass(frozen=True, eq=True) class UntypedObject: cap: int @@ -682,7 +688,6 @@ def size_bits(self) -> int: return lsb(self.region.end - self.region.base) - @dataclass(frozen=True, eq=True) class KernelBootInfo: fixed_cap_count: int @@ -745,7 +750,7 @@ def _kernel_phys_mem(kernel_elf: ElfFile) -> List[Tuple[int, int]]: def _kernel_self_mem(kernel_elf: ElfFile) -> Tuple[int, int]: """Return the physical memory range used by the kernel itself.""" base = kernel_elf.segments[0].phys_addr - ki_end_v, _= kernel_elf.find_symbol("ki_end") + ki_end_v, _ = kernel_elf.find_symbol("ki_end") ki_end_p = ki_end_v - kernel_elf.segments[0].virt_addr + base return (base, ki_end_p) @@ -760,7 +765,7 @@ def _kernel_boot_mem(kernel_elf: ElfFile) -> MemoryRegion: def _rootserver_max_size_bits() -> int: slot_bits = 5 # seL4_SlotBits root_cnode_bits = 12 # CONFIG_ROOT_CNODE_SIZE_BITS - vspace_bits = 12 #seL4_VSpaceBits + vspace_bits = 12 # seL4_VSpaceBits cnode_size_bits = root_cnode_bits + slot_bits return max(cnode_size_bits, vspace_bits) @@ -808,9 +813,9 @@ def _kernel_partial_boot( def emulate_kernel_boot_partial( - kernel_config: KernelConfig, - kernel_elf: ElfFile, - ) -> DisjointMemoryRegion: + kernel_config: KernelConfig, + kernel_elf: ElfFile, +) -> DisjointMemoryRegion: """Return the memory available after a 'partial' boot emulation. This allows the caller to allocation a reserved memory region at an @@ -869,10 +874,10 @@ def emulate_kernel_boot( untyped_objects.append(UntypedObject(cap, r, False)) return KernelBootInfo( - fixed_cap_count = fixed_cap_count, - paging_cap_count = paging_cap_count, - page_cap_count = page_cap_count, - schedcontrol_cap = schedcontrol_cap, - first_available_cap = first_untyped_cap + len(device_regions) + len(normal_regions), - untyped_objects = untyped_objects, + fixed_cap_count=fixed_cap_count, + paging_cap_count=paging_cap_count, + page_cap_count=page_cap_count, + schedcontrol_cap=schedcontrol_cap, + first_available_cap=first_untyped_cap + len(device_regions) + len(normal_regions), + untyped_objects=untyped_objects, ) diff --git a/tool/microkit/sysxml.py b/tool/microkit/sysxml.py index 065c0dde..9dc44476 100644 --- a/tool/microkit/sysxml.py +++ b/tool/microkit/sysxml.py @@ -3,19 +3,18 @@ # # SPDX-License-Identifier: BSD-2-Clause # +from microkit.util import str_to_bool, UserError +from typing import Dict, Iterable, Optional, Set, Tuple from dataclasses import dataclass from pathlib import Path # See: https://stackoverflow.com/questions/6949395/is-there-a-way-to-get-a-line-number-from-an-elementtree-element # Force use of Python elementtree to avoid overloading import sys sys.modules['_elementtree'] = None # type: ignore -import xml.etree.ElementTree as ET - -from typing import Dict, Iterable, Optional, Set, Tuple +import xml.etree.ElementTree as ET # noqa: E402 -from microkit.util import str_to_bool, UserError -MIN_PAGE_SIZE = 0x1000 # FIXME: This shouldn't be here +MIN_PAGE_SIZE = 0x1000 # FIXME: This shouldn't be here class MissingAttribute(Exception): @@ -111,6 +110,7 @@ class Channel: id_b: int element: ET.Element + class SystemDescription: def __init__( self, @@ -190,7 +190,6 @@ def __init__( if extra != 0: raise UserError(f"Invalid vaddr alignment on '{map.element.tag}' @ {map.element._loc_str}") # type: ignore - # Note: Overlapping memory is checked in the build. # Ensure all memory regions are used at least once. This only generates @@ -315,7 +314,6 @@ def xml2channel(ch_xml: ET.Element) -> Channel: return Channel(ends[0][0], ends[0][1], ends[1][0], ends[1][1], ch_xml) - def _check_no_text(el: ET.Element) -> None: if not (el.text is None or el.text.strip() == ""): raise UserError(f"Error: unexpected text found in element '{el.tag}' @ {el._loc_str}") # type: ignore diff --git a/tool/microkit/util.py b/tool/microkit/util.py index b055e599..e5000764 100644 --- a/tool/microkit/util.py +++ b/tool/microkit/util.py @@ -6,6 +6,7 @@ from dataclasses import dataclass from typing import List, Optional + class UserError(Exception): pass @@ -35,6 +36,7 @@ def round_down(n: int, x: int) -> int: d, m = divmod(n, x) return n if m == 0 else n - m + def mask_bits(n: int, bits: int) -> int: """mask out (set to zero) the lower bits from n""" assert n > 0 @@ -55,7 +57,6 @@ def str_to_bool(s: str) -> bool: raise ValueError("invalid boolean value") - @dataclass class MemoryRegion: # Note: base is inclusive, end is exclusive diff --git a/tool/test/__init__.py b/tool/test/__init__.py index 99f23c2c..2a987ab3 100644 --- a/tool/test/__init__.py +++ b/tool/test/__init__.py @@ -10,9 +10,10 @@ plat_desc = PlatformDescription( - page_sizes = [0x1_000, 0x200_000] + page_sizes=[0x1_000, 0x200_000] ) + def _file(filename: str) -> Path: return Path(__file__).parent / filename @@ -117,6 +118,7 @@ def test_id_less_than_0(self): def test_invalid_attrs(self): self._check_error("ch_invalid_attrs.xml", "Error: invalid attribute 'foo' on element 'channel': ") + class SystemParseTests(ExtendedTestCase): def test_duplicate_pd_names(self): self._check_error("sys_duplicate_pd_name.xml", "Duplicate protection domain name 'test'.") @@ -152,4 +154,4 @@ def test_map_not_aligned(self): self._check_error("sys_map_not_aligned.xml", "Invalid vaddr alignment on 'map' @ ") def test_too_many_pds(self): - self._check_error("sys_too_many_pds.xml", "Too many protection domains (64) defined. Maximum is 63.") \ No newline at end of file + self._check_error("sys_too_many_pds.xml", "Too many protection domains (64) defined. Maximum is 63.")