From 1a1fdffb11d19ab0fddd6c2447784f1d87c282e1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 13 Dec 2022 10:14:37 +1100 Subject: [PATCH] aarch64 aspec: adjust Init_A to satisfy invariants - align init_irq_node_ptr to its size (which is larger than in RISCV) - remove ArmVSpaceUserRegion, because kernel has its own page table - define global_pt_obj, add to initial heap Co-authored-by: Rafal Kolanski Signed-off-by: Gerwin Klein --- spec/abstract/AARCH64/Init_A.thy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/abstract/AARCH64/Init_A.thy b/spec/abstract/AARCH64/Init_A.thy index 2e81b10f4..3b08aa35a 100644 --- a/spec/abstract/AARCH64/Init_A.thy +++ b/spec/abstract/AARCH64/Init_A.thy @@ -26,7 +26,7 @@ definition arm_global_pt_ptr :: obj_ref where (* Sufficiently aligned for irq type + cte_level_bits *) definition init_irq_node_ptr :: obj_ref where - "init_irq_node_ptr = pptr_base + 0x3000" + "init_irq_node_ptr = pptr_base + 0xc000" (* The highest user-virtual address that is still canonical. It can be larger than user_vtop, which is the highest address we allow to be mapped. @@ -41,7 +41,6 @@ definition canonical_user :: "vspace_ref" where definition init_vspace_uses :: "vspace_ref \ arm_vspace_region_use" where "init_vspace_uses p \ if p \ {pptr_base ..< pptr_base + (1 << 30)} then ArmVSpaceKernelWindow - else if p \ canonical_user then ArmVSpaceUserRegion else ArmVSpaceInvalidRegion" @@ -59,8 +58,8 @@ definition init_arch_state :: arch_state where (* The user-level global table in hyp mode is entirely empty. Kernel-level mappings are in a separate kernel page table, which is not modeled here. *) -definition global_pte :: "pt_index \ pte" where - "global_pte idx \ InvalidPTE" +definition global_pt_obj :: arch_kernel_obj where + "global_pt_obj \ PageTable (VSRootPT (\_. InvalidPTE))" definition init_kheap :: kheap where "init_kheap \ @@ -81,7 +80,8 @@ definition init_kheap :: kheap where tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb - \ + \, + arm_global_pt_ptr \ ArchObj global_pt_obj )" definition init_cdt :: cdt where