Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-05 06:49:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

aarch64/vspace: allow flushing larger pages

Browse Source 
- The failure condition `resolve_ret.ptBitsLeft > PAGE_BITS` prevented
  larger page sizes from being flushed in VSpaceRoot invocations.

  Instead of testing for number of bits left to resolve, simply check
  the PTE whether it is a page or not.

- reduce bitfield accesses via pointers to make verification a bit
  easier.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2024-01-22 11:29:04 +11:00
parent 0a0739074d
commit 494dd2dd96
2 changed files with 19 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
include/arch/arm/arch/64/mode/object/structures.h
View File

@@ -201,9 +201,21 @@ static inline bool_t pte_ptr_get_valid(pte_t *pt)
return (pte_ptr_get_pte_type(pt) != pte_pte_invalid);
}
static inline bool_t pte_is_page_type(pte_t pte)
{
return pte_get_pte_type(pte) == pte_pte_4k_page ||
pte_get_pte_type(pte) == pte_pte_page;
}
/** Return base address for both of pte_4k_page and pte_page */
static inline uint64_t pte_get_page_base_address(pte_t pte)
{
assert(pte_is_page_type(pte));
return pte.words[0] & 0xfffffffff000ull;
}
/** Return base address for both of pte_4k_page and pte_page */
static inline uint64_t pte_page_ptr_get_page_base_address(pte_t *pt)
{
uint64_t ret;
ret = (pt->words[0] & 0xfffffffff000ull);
return ret;
return pte_get_page_base_address(*pt);
}

7
src/arch/arm/64/kernel/vspace.c
View File

@@ -1273,6 +1273,7 @@ static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, word_t length,
vspace_root_t *vspaceRoot;
lookupPTSlot_ret_t resolve_ret;
findVSpaceForASID_ret_t find_ret;
pte_t pte;
switch (invLabel) {
case ARMVSpaceClean_Data:
@@ -1331,10 +1332,10 @@ static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, word_t length,
/* Look up the frame containing 'start'. */
resolve_ret = lookupPTSlot(vspaceRoot, start);
pte = *resolve_ret.ptSlot;
/* Check that the returned slot is a page. */
if (!pte_ptr_get_valid(resolve_ret.ptSlot) ||
(pte_pte_table_ptr_get_present(resolve_ret.ptSlot) && resolve_ret.ptBitsLeft > PAGE_BITS)) {
if (!pte_is_page_type(pte)) {
/* Fail silently, as there can't be any stale cached data (for the
* given address space), and getting a syscall error because the
@@ -1353,7 +1354,7 @@ static exception_t decodeARMVSpaceRootInvocation(word_t invLabel, word_t length,
}
/* Calculate the physical start address. */
paddr_t frame_base = pte_page_ptr_get_page_base_address(resolve_ret.ptSlot);
paddr_t frame_base = pte_get_page_base_address(pte);
pstart = frame_base + (start & MASK(resolve_ret.ptBitsLeft));