portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

aarch64: use VS prefix for vspace_cap fields

Browse source 
The vspace (top level PT) cap had non-standard names which were a bit
confusing to reason about. The name conflict with capPTBasePtr also
spits out fully-qualified names in verification.
This commit updates all the field names of vspace_cap to start with
"capVS" and updates all the call sites.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2023-10-26 09:59:31 +11:00 committed by Rafal Kolanski
parent b4592ebc97
commit 4f9b736526
9 changed files with 60 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
include/arch/arm/arch/64/mode/fastpath/fastpath.h
View file

@ -25,7 +25,7 @@ compile_assert(SysReplyRecv_Minus2, SysReplyRecv == -2)
/* Use macros to not break verification */
#define endpoint_ptr_get_epQueue_tail_fp(ep_ptr) TCB_PTR(endpoint_ptr_get_epQueue_tail(ep_ptr))
#define cap_vtable_cap_get_vspace_root_fp(vtable_cap) VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(vtable_cap))
#define cap_vtable_cap_get_vspace_root_fp(vtable_cap) VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(vtable_cap))
static inline void FORCE_INLINE
switchToThread_fp(tcb_t *thread, vspace_root_t *vroot, pde_t stored_hw_asid)
@ -97,7 +97,7 @@ static inline void mdb_node_ptr_set_mdbPrev_np(mdb_node_t *node_ptr, word_t mdbP
static inline bool_t isValidVTableRoot_fp(cap_t vspace_root_cap)
{
return cap_capType_equals(vspace_root_cap, cap_vspace_cap)
&& cap_vspace_cap_get_capIsMapped(vspace_root_cap);
&& cap_vspace_cap_get_capVSIsMapped(vspace_root_cap);
}
/* This is an accelerated check that msgLength, which appears

6
include/arch/arm/arch/64/mode/kernel/vspace.h
View file

@ -47,14 +47,14 @@ static inline exception_t performASIDPoolInvocation(asid_t asid, asid_pool_t *po
0,
#endif
/* vspace_root: reference to vspace root page table object */
cap_vspace_cap_get_capPTBasePtr(cap)
cap_vspace_cap_get_capVSBasePtr(cap)
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
/* stored_hw_vmid, stored_vmid_valid: Assigned hardware VMID for TLB. */
, 0, false
#endif
);
cap = cap_vspace_cap_set_capMappedASID(cap, asid);
cap = cap_vspace_cap_set_capIsMapped(cap, 1);
cap = cap_vspace_cap_set_capVSMappedASID(cap, asid);
cap = cap_vspace_cap_set_capVSIsMapped(cap, 1);
vspaceCapSlot->cap = cap;
poolPtr->array[asid & MASK(asidLowBits)] = asid_map;

14
include/arch/arm/arch/64/mode/object/structures.bf
View file

@ -46,17 +46,17 @@ block page_table_cap {
-- First-level page table (vspace_root)
block vspace_cap {
field capMappedASID 16
field_high capPTBasePtr 48
field capVSMappedASID 16
field_high capVSBasePtr 48
field capType 5
field capIsMapped 1
#ifdef CONFIG_ARM_SMMU
field capMappedCB 8
field capVSIsMapped 1
#ifdef CONFIG_ARM_SMMU
field capVSMappedCB 8
padding 50
#else
#else
padding 58
#endif
#endif
}
-- Cap to the table of 2^7 ASID pools

2
include/arch/arm/arch/64/mode/object/structures.h
View file

@ -162,7 +162,7 @@ static inline void *CONST cap_get_archCapPtr(cap_t cap)
return PT_PTR(cap_page_table_cap_get_capPTBasePtr(cap));
case cap_vspace_cap:
return VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(cap));
return VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(cap));
case cap_asid_control_cap:
return NULL;

36
src/arch/arm/64/kernel/vspace.c
View file

@ -449,11 +449,11 @@ BOOT_CODE cap_t create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_re
/* create the PGD */
vspace_cap = cap_vspace_cap_new(
IT_ASID, /* capMappedASID */
rootserver.vspace, /* capPTBasePtr */
1 /* capIsMapped */
IT_ASID, /* capVSMappedASID */
rootserver.vspace, /* capVSBasePtr */
1 /* capVSIsMapped */
#ifdef CONFIG_ARM_SMMU
, 0 /* capMappedCB */
, 0 /* capVSMappedCB */
#endif
);
slot_pos_before = ndks_boot.slot_pos_cur;
@ -528,7 +528,7 @@ BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_vspace_cap)
0,
#endif
/* vspace_root: reference to vspace root page table object */
(word_t)cap_vspace_cap_get_capPTBasePtr(it_vspace_cap)
(word_t)cap_vspace_cap_get_capVSBasePtr(it_vspace_cap)
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
/* stored_hw_vmid, stored_vmid_valid: Assigned hardware VMID for TLB. */
, 0, false
@ -724,7 +724,7 @@ bool_t CONST isVTableRoot(cap_t cap)
bool_t CONST isValidNativeRoot(cap_t cap)
{
return isVTableRoot(cap) &&
cap_vspace_cap_get_capIsMapped(cap);
cap_vspace_cap_get_capVSIsMapped(cap);
}
bool_t CONST isValidVTableRoot(cap_t cap)
@ -746,8 +746,8 @@ void setVMRoot(tcb_t *tcb)
return;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(threadRoot));
asid = cap_vspace_cap_get_capMappedASID(threadRoot);
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(threadRoot));
asid = cap_vspace_cap_get_capVSMappedASID(threadRoot);
find_ret = findVSpaceForASID(asid);
if (unlikely(find_ret.status != EXCEPTION_NONE || find_ret.vspace_root != vspaceRoot)) {
setCurrentUserVSpaceRoot(ttbr_new(0, addrFromKPPtr(armKSGlobalUserVSpace)));
@ -764,8 +764,8 @@ static bool_t setVMRootForFlush(vspace_root_t *vspace, asid_t asid)
threadRoot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbVTable)->cap;
if (cap_get_capType(threadRoot) == cap_vspace_cap &&
cap_vspace_cap_get_capIsMapped(threadRoot) &&
VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(threadRoot)) == vspace) {
cap_vspace_cap_get_capVSIsMapped(threadRoot) &&
VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(threadRoot)) == vspace) {
return false;
}
@ -1294,8 +1294,8 @@ static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, unsigned int l
}
/* Make sure that the supplied pgd is ok */
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(cap));
asid = cap_vspace_cap_get_capMappedASID(cap);
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(cap));
asid = cap_vspace_cap_get_capVSMappedASID(cap);
find_ret = findVSpaceForASID(asid);
if (unlikely(find_ret.status != EXCEPTION_NONE)) {
@ -1396,8 +1396,8 @@ static exception_t decodeARMPageTableInvocation(word_t invLabel, unsigned int le
return EXCEPTION_SYSCALL_ERROR;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(vspaceRootCap));
asid = cap_vspace_cap_get_capMappedASID(vspaceRootCap);
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(vspaceRootCap));
asid = cap_vspace_cap_get_capVSMappedASID(vspaceRootCap);
if (unlikely(vaddr > USER_TOP)) {
current_syscall_error.type = seL4_InvalidArgument;
@ -1474,8 +1474,8 @@ static exception_t decodeARMFrameInvocation(word_t invLabel, unsigned int length
return EXCEPTION_SYSCALL_ERROR;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(vspaceRootCap));
asid = cap_vspace_cap_get_capMappedASID(vspaceRootCap);
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(vspaceRootCap));
asid = cap_vspace_cap_get_capVSMappedASID(vspaceRootCap);
find_ret = findVSpaceForASID(asid);
if (unlikely(find_ret.status != EXCEPTION_NONE)) {
@ -1725,7 +1725,7 @@ exception_t decodeARMMMUInvocation(word_t invLabel, word_t length, cptr_t cptr,
vspaceCapSlot = current_extra_caps.excaprefs[0];
vspaceCap = vspaceCapSlot->cap;
if (unlikely(!isVTableRoot(vspaceCap) || cap_vspace_cap_get_capIsMapped(vspaceCap))) {
if (unlikely(!isVTableRoot(vspaceCap) || cap_vspace_cap_get_capVSIsMapped(vspaceCap))) {
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
@ -1838,7 +1838,7 @@ void Arch_userStackTrace(tcb_t *tptr)
return;
}
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(threadRoot));
vspaceRoot = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(threadRoot));
sp = getRegister(tptr, SP_EL0);
/* check for alignment so we don't have to worry about accessing

6
src/arch/arm/64/machine/capdl.c
View file

@ -224,7 +224,7 @@ void obj_vtable_print_slots(tcb_t *tcb)
{
if (isVTableRoot(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap) && !seen(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap)) {
add_to_seen(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap);
vspace_root_t *vspace = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap));
vspace_root_t *vspace = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap));
/*
* ARM hyp uses 3 level translation rather than the usual 4 level.
@ -295,7 +295,7 @@ void print_cap_arch(cap_t cap)
break;
}
case cap_vspace_cap: {
asid_t asid = cap_vspace_cap_get_capMappedASID(cap);
asid_t asid = cap_vspace_cap_get_capVSMappedASID(cap);
findVSpaceForASID_ret_t find_ret = findVSpaceForASID(asid);
if (asid) {
printf("%p_pd (asid: %lu)\n",
@ -461,7 +461,7 @@ void obj_tcb_print_vtable(tcb_t *tcb)
{
if (isVTableRoot(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap) && !seen(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap)) {
add_to_seen(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap);
vspace_root_t *vspace = VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap));
vspace_root_t *vspace = VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(TCB_PTR_CTE_PTR(tcb, tcbVTable)->cap));
/*
* ARM hyp uses 3 level translation rather than the usual 4 level.

32
src/arch/arm/64/object/objecttype.c
View file

@ -33,7 +33,7 @@ deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
switch (cap_get_capType(cap)) {
case cap_vspace_cap:
if (cap_vspace_cap_get_capIsMapped(cap)) {
if (cap_vspace_cap_get_capVSIsMapped(cap)) {
ret.cap = cap;
ret.status = EXCEPTION_NONE;
} else {
@ -143,14 +143,14 @@ finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
case cap_vspace_cap:
#ifdef CONFIG_ARM_SMMU
if (cap_vspace_cap_get_capMappedCB(cap) != CB_INVALID) {
smmu_cb_delete_vspace(cap_vspace_cap_get_capMappedCB(cap),
cap_vspace_cap_get_capMappedASID(cap));
if (cap_vspace_cap_get_capVSMappedCB(cap) != CB_INVALID) {
smmu_cb_delete_vspace(cap_vspace_cap_get_capVSMappedCB(cap),
cap_vspace_cap_get_capVSMappedASID(cap));
}
#endif
if (final && cap_vspace_cap_get_capIsMapped(cap)) {
deleteASID(cap_vspace_cap_get_capMappedASID(cap),
VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(cap)));
if (final && cap_vspace_cap_get_capVSIsMapped(cap)) {
deleteASID(cap_vspace_cap_get_capVSMappedASID(cap),
VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(cap)));
}
break;
@ -223,8 +223,8 @@ bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
case cap_vspace_cap:
if (cap_get_capType(cap_b) == cap_vspace_cap) {
return cap_vspace_cap_get_capPTBasePtr(cap_a) ==
cap_vspace_cap_get_capPTBasePtr(cap_b);
return cap_vspace_cap_get_capVSBasePtr(cap_a) ==
cap_vspace_cap_get_capVSBasePtr(cap_b);
}
break;
@ -370,17 +370,17 @@ cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t de
#ifdef CONFIG_ARM_SMMU
return cap_vspace_cap_new(
asidInvalid, /* capMappedASID */
(word_t)regionBase, /* capPTBasePtr */
0, /* capIsMapped */
CB_INVALID /* capMappedCB */
asidInvalid, /* capVSMappedASID */
(word_t)regionBase, /* capVSBasePtr */
0, /* capVSIsMapped */
CB_INVALID /* capVSMappedCB */
);
#else
return cap_vspace_cap_new(
asidInvalid, /* capMappedASID */
(word_t)regionBase, /* capPTBasePtr */
0 /* capIsMapped */
asidInvalid, /* capVSMappedASID */
(word_t)regionBase, /* capVSBasePtr */
0 /* capVSIsMapped */
);
#endif /*!CONFIG_ARM_SMMU*/
case seL4_ARM_PageTableObject:

14
src/arch/arm/object/smmu.c
View file

@ -272,7 +272,7 @@ exception_t decodeARMCBInvocation(word_t label, unsigned int length, cptr_t cptr
cb = cap_cb_cap_get_capCB(cap);
cbSlot = smmuStateCBNode + cb;
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
smmu_tlb_invalidate_cb(cb, cap_vspace_cap_get_capMappedASID(cbSlot->cap));
smmu_tlb_invalidate_cb(cb, cap_vspace_cap_get_capVSMappedASID(cbSlot->cap));
return EXCEPTION_NONE;
case ARMCBAssignVspace:
@ -284,7 +284,7 @@ exception_t decodeARMCBInvocation(word_t label, unsigned int length, cptr_t cptr
vspaceCapSlot = current_extra_caps.excaprefs[0];
vspaceCap = vspaceCapSlot->cap;
if (unlikely(!isVTableRoot(vspaceCap) || !cap_vspace_cap_get_capIsMapped(vspaceCap))) {
if (unlikely(!isVTableRoot(vspaceCap) || !cap_vspace_cap_get_capVSIsMapped(vspaceCap))) {
userError("ARMCBAssignVspace: the vspace is invalid");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
@ -302,14 +302,14 @@ exception_t decodeARMCBInvocation(word_t label, unsigned int length, cptr_t cptr
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
/*setting up vspace for the context bank in SMMU*/
smmu_cb_assign_vspace(cb, VSPACE_PTR(cap_vspace_cap_get_capPTBasePtr(vspaceCap)),
cap_vspace_cap_get_capMappedASID(vspaceCap));
smmu_cb_assign_vspace(cb, VSPACE_PTR(cap_vspace_cap_get_capVSBasePtr(vspaceCap)),
cap_vspace_cap_get_capVSMappedASID(vspaceCap));
/*Connecting vspace cap to context bank*/
cteInsert(vspaceCap, vspaceCapSlot, cbSlot);
cap_vspace_cap_ptr_set_capMappedCB(&(cbSlot->cap), cb);
cap_vspace_cap_ptr_set_capVSMappedCB(&(cbSlot->cap), cb);
/*set relationship between CB and ASID*/
smmuStateCBAsidTable[cb] = cap_vspace_cap_get_capMappedASID(vspaceCap);
increaseASIDBindCB(cap_vspace_cap_get_capMappedASID(vspaceCap));
smmuStateCBAsidTable[cb] = cap_vspace_cap_get_capVSMappedASID(vspaceCap);
increaseASIDBindCB(cap_vspace_cap_get_capVSMappedASID(vspaceCap));
return EXCEPTION_NONE;
case ARMCBUnassignVspace:

6
src/fastpath/fastpath.c
View file

@ -97,7 +97,7 @@ void NORETURN fastpath_call(word_t cptr, word_t msgInfo)
#endif
#ifdef CONFIG_ARCH_AARCH64
/* Need to test that the ASID is still valid */
asid_t asid = cap_vspace_cap_get_capMappedASID(newVTable);
asid_t asid = cap_vspace_cap_get_capVSMappedASID(newVTable);
asid_map_t asid_map = findMapForASID(asid);
if (unlikely(asid_map_get_type(asid_map) != asid_map_asid_map_vspace ||
VSPACE_PTR(asid_map_asid_map_vspace_get_vspace_root(asid_map)) != cap_pd)) {
@ -374,7 +374,7 @@ void NORETURN fastpath_reply_recv(word_t cptr, word_t msgInfo)
#endif
#ifdef CONFIG_ARCH_AARCH64
/* Need to test that the ASID is still valid */
asid_t asid = cap_vspace_cap_get_capMappedASID(newVTable);
asid_t asid = cap_vspace_cap_get_capVSMappedASID(newVTable);
asid_map_t asid_map = findMapForASID(asid);
if (unlikely(asid_map_get_type(asid_map) != asid_map_asid_map_vspace ||
VSPACE_PTR(asid_map_asid_map_vspace_get_vspace_root(asid_map)) != cap_pd)) {
@ -779,7 +779,7 @@ void NORETURN fastpath_vm_fault(vm_fault_type_t type)
#ifdef CONFIG_ARCH_AARCH64
/* Need to test that the ASID is still valid */
asid_t asid = cap_vspace_cap_get_capMappedASID(newVTable);
asid_t asid = cap_vspace_cap_get_capVSMappedASID(newVTable);
asid_map_t asid_map = findMapForASID(asid);
if (unlikely(asid_map_get_type(asid_map) != asid_map_asid_map_vspace ||
VSPACE_PTR(asid_map_asid_map_vspace_get_vspace_root(asid_map)) != cap_pd)) {