From b8e81b077aef280c5a771ee86df07bc0217abccb Mon Sep 17 00:00:00 2001 From: julia Date: Mon, 4 Aug 2025 11:04:53 +1000 Subject: [PATCH] asidpools: consistently use ASID_HIGH macro Also, change the definition of ASID_HIGH from ((a >> asidLowBits) & MASK(asidHighBits)) to ((a) >> asidLowBits) because the mask is an unnecessary operation (this is handled by the proofs). It is unnecessary because these (SW) ASIDs are kernel-only and are never exposed to users, so they will never set bits asid from the asidLow and asidHigh bits. Signed-off-by: julia --- .../arch/arm/arch/32/mode/object/structures.h | 9 ++++---- .../arch/arm/arch/64/mode/object/structures.h | 2 +- include/arch/riscv/arch/object/structures.h | 2 +- .../arch/x86/arch/32/mode/object/structures.h | 3 ++- .../arch/x86/arch/64/mode/object/structures.h | 3 ++- src/arch/arm/32/kernel/vspace.c | 21 +++++++++--------- src/arch/arm/64/kernel/vspace.c | 22 +++++++++---------- src/arch/riscv/kernel/vspace.c | 14 ++++++------ src/arch/x86/kernel/ept.c | 2 +- src/arch/x86/kernel/vspace.c | 14 ++++++------ src/kernel/boot.c | 2 +- 11 files changed, 47 insertions(+), 47 deletions(-) diff --git a/include/arch/arm/arch/32/mode/object/structures.h b/include/arch/arm/arch/32/mode/object/structures.h index 4b42228a1..d02527c62 100644 --- a/include/arch/arm/arch/32/mode/object/structures.h +++ b/include/arch/arm/arch/32/mode/object/structures.h @@ -104,14 +104,13 @@ typedef struct asid_pool asid_pool_t; #define nASIDPools BIT(asidHighBits) #define ASID_LOW(a) (a & MASK(asidLowBits)) -#define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) +#define ASID_HIGH(a) ((a) >> asidLowBits) static inline cap_t CONST cap_small_frame_cap_set_capFMappedASID(cap_t cap, word_t asid) { cap = cap_small_frame_cap_set_capFMappedASIDLow(cap, asid & MASK(asidLowBits)); - return cap_small_frame_cap_set_capFMappedASIDHigh(cap, - (asid >> asidLowBits) & MASK(asidHighBits)); + return cap_small_frame_cap_set_capFMappedASIDHigh(cap, ASID_HIGH(asid)); } static inline word_t CONST cap_small_frame_cap_get_capFMappedASID(cap_t cap) @@ -124,8 +123,7 @@ static inline cap_t CONST cap_frame_cap_set_capFMappedASID(cap_t cap, word_t asi { cap = cap_frame_cap_set_capFMappedASIDLow(cap, asid & MASK(asidLowBits)); - return cap_frame_cap_set_capFMappedASIDHigh(cap, - (asid >> asidLowBits) & MASK(asidHighBits)); + return cap_frame_cap_set_capFMappedASIDHigh(cap, ASID_HIGH(asid)); } static inline word_t CONST cap_frame_cap_get_capFMappedASID(cap_t cap) @@ -432,3 +430,4 @@ static inline word_t PURE pte_ptr_get_pteType(pte_t *pte_ptr) } } #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ + diff --git a/include/arch/arm/arch/64/mode/object/structures.h b/include/arch/arm/arch/64/mode/object/structures.h index bdfb25035..cbf7a9bc0 100644 --- a/include/arch/arm/arch/64/mode/object/structures.h +++ b/include/arch/arm/arch/64/mode/object/structures.h @@ -78,7 +78,7 @@ typedef pte_t pde_t; #define nASIDPools BIT(asidHighBits) #define ASID_LOW(a) (a & MASK(asidLowBits)) -#define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) +#define ASID_HIGH(a) ((a) >> asidLowBits) static inline word_t CONST cap_get_archCapSizeBits(cap_t cap) { diff --git a/include/arch/riscv/arch/object/structures.h b/include/arch/riscv/arch/object/structures.h index 35c216a21..b951918b7 100644 --- a/include/arch/riscv/arch/object/structures.h +++ b/include/arch/riscv/arch/object/structures.h @@ -31,7 +31,7 @@ typedef struct asid_pool asid_pool_t; #define ASID_BITS (asidHighBits + asidLowBits) #define nASIDPools BIT(asidHighBits) #define ASID_LOW(a) (a & MASK(asidLowBits)) -#define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) +#define ASID_HIGH(a) ((a) >> asidLowBits) typedef struct arch_tcb { user_context_t tcbContext; diff --git a/include/arch/x86/arch/32/mode/object/structures.h b/include/arch/x86/arch/32/mode/object/structures.h index 03b234ece..9a45b9ae4 100644 --- a/include/arch/x86/arch/32/mode/object/structures.h +++ b/include/arch/x86/arch/32/mode/object/structures.h @@ -56,7 +56,7 @@ typedef struct asid_pool asid_pool_t; #define ASID_BITS (asidHighBits + asidLowBits) #define nASIDPools BIT(asidHighBits) #define ASID_LOW(a) (a & MASK(asidLowBits)) -#define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) +#define ASID_HIGH(a) ((a) >> asidLowBits) static inline asid_t CONST cap_frame_cap_get_capFMappedASID(cap_t cap) { @@ -115,3 +115,4 @@ static inline void *CONST cap_get_modeCapPtr(cap_t cap) { fail("Invalid mode cap type"); } + diff --git a/include/arch/x86/arch/64/mode/object/structures.h b/include/arch/x86/arch/64/mode/object/structures.h index c68dcb9fd..70668a275 100644 --- a/include/arch/x86/arch/64/mode/object/structures.h +++ b/include/arch/x86/arch/64/mode/object/structures.h @@ -107,7 +107,7 @@ typedef struct asid_pool asid_pool_t; #define ASID_BITS (asidHighBits + asidLowBits) #define nASIDPools BIT(asidHighBits) #define ASID_LOW(a) (a & MASK(asidLowBits)) -#define ASID_HIGH(a) ((a >> asidLowBits) & MASK(asidHighBits)) +#define ASID_HIGH(a) ((a) >> asidLowBits) static inline asid_t PURE cap_get_capMappedASID(cap_t cap) { @@ -190,3 +190,4 @@ static inline void *CONST cap_get_modeCapPtr(cap_t cap) return NULL; } } + diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c index 0e77d1e08..2e1644671 100644 --- a/src/arch/arm/32/kernel/vspace.c +++ b/src/arch/arm/32/kernel/vspace.c @@ -592,7 +592,7 @@ BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_pd_cap) { asid_pool_t *ap = ASID_POOL_PTR(pptr_of_cap(it_ap_cap)); ap->array[IT_ASID] = PDE_PTR(pptr_of_cap(it_pd_cap)); - armKSASIDTable[IT_ASID >> asidLowBits] = ap; + armKSASIDTable[ASID_HIGH(IT_ASID)] = ap; } /* ==================== BOOT CODE FINISHES HERE ==================== */ @@ -603,7 +603,7 @@ findPDForASID_ret_t findPDForASID(asid_t asid) asid_pool_t *poolPtr; pde_t *pd; - poolPtr = armKSASIDTable[asid >> asidLowBits]; + poolPtr = armKSASIDTable[ASID_HIGH(asid)]; if (unlikely(!poolPtr)) { current_lookup_fault = lookup_fault_invalid_root_new(); @@ -1075,7 +1075,7 @@ static void invalidateASID(asid_t asid) asid_pool_t *asidPool; pde_t *pd; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); pd = asidPool->array[asid & MASK(asidLowBits)]; @@ -1089,7 +1089,7 @@ static pde_t PURE loadHWASID(asid_t asid) asid_pool_t *asidPool; pde_t *pd; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); pd = asidPool->array[asid & MASK(asidLowBits)]; @@ -1103,7 +1103,7 @@ static void storeHWASID(asid_t asid, hw_asid_t hw_asid) asid_pool_t *asidPool; pde_t *pd; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); pd = asidPool->array[asid & MASK(asidLowBits)]; @@ -1282,14 +1282,14 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) /* Haskell error: "ASID pool's base must be aligned" */ assert((asid_base & MASK(asidLowBits)) == 0); - if (armKSASIDTable[asid_base >> asidLowBits] == pool) { + if (armKSASIDTable[ASID_HIGH(asid_base)] == pool) { for (offset = 0; offset < BIT(asidLowBits); offset++) { if (pool->array[offset]) { flushSpace(asid_base + offset); invalidateASIDEntry(asid_base + offset); } } - armKSASIDTable[asid_base >> asidLowBits] = NULL; + armKSASIDTable[ASID_HIGH(asid_base)] = NULL; setVMRoot(NODE_STATE(ksCurThread)); } } @@ -1298,7 +1298,7 @@ void deleteASID(asid_t asid, pde_t *pd) { asid_pool_t *poolPtr; - poolPtr = armKSASIDTable[asid >> asidLowBits]; + poolPtr = armKSASIDTable[ASID_HIGH(asid)]; if (poolPtr != NULL && poolPtr->array[asid & MASK(asidLowBits)] == pd) { flushSpace(asid); @@ -1991,7 +1991,7 @@ static exception_t performASIDControlInvocation(void *frame, cte_t *slot, parent, slot);; /* Haskell error: "ASID pool's base must be aligned" */ assert((asid_base & MASK(asidLowBits)) == 0); - armKSASIDTable[asid_base >> asidLowBits] = (asid_pool_t *)frame; + armKSASIDTable[ASID_HIGH(asid_base)] = (asid_pool_t *)frame; return EXCEPTION_NONE; } @@ -2626,8 +2626,7 @@ exception_t decodeARMMMUInvocation(word_t invLabel, word_t length, cptr_t cptr, return EXCEPTION_SYSCALL_ERROR; } - pool = armKSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> - asidLowBits]; + pool = armKSASIDTable[ASID_HIGH(cap_asid_pool_cap_get_capASIDBase(cap))]; if (unlikely(!pool)) { userError("ASIDPoolAssign: Failed to lookup pool."); current_syscall_error.type = seL4_FailedLookup; diff --git a/src/arch/arm/64/kernel/vspace.c b/src/arch/arm/64/kernel/vspace.c index fed090bd5..ceb52b112 100644 --- a/src/arch/arm/64/kernel/vspace.c +++ b/src/arch/arm/64/kernel/vspace.c @@ -568,7 +568,7 @@ BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_vspace_cap) #endif ); ap->array[IT_ASID] = asid_map; - armKSASIDTable[IT_ASID >> asidLowBits] = ap; + armKSASIDTable[ASID_HIGH(IT_ASID)] = ap; } /* ==================== BOOT CODE FINISHES HERE ==================== */ @@ -577,7 +577,7 @@ asid_map_t findMapForASID(asid_t asid) { asid_pool_t *poolPtr; - poolPtr = armKSASIDTable[asid >> asidLowBits]; + poolPtr = armKSASIDTable[ASID_HIGH(asid)]; if (!poolPtr) { return asid_map_asid_map_none_new(); } @@ -811,7 +811,7 @@ static bool_t setVMRootForFlush(vspace_root_t *vspace, asid_t asid) static inline asid_pool_t *getPoolPtr(asid_t asid) { - return armKSASIDTable[asid >> asidLowBits]; + return armKSASIDTable[ASID_HIGH(asid)]; } static inline asid_map_t getASIDMap(asid_pool_t *poolPtr, asid_t asid) @@ -922,7 +922,7 @@ static word_t getASIDBindCB(asid_t asid) { asid_pool_t *asidPool; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); asid_map_t asid_map = asidPool->array[asid & MASK(asidLowBits)]; @@ -935,7 +935,7 @@ void increaseASIDBindCB(asid_t asid) { asid_pool_t *asidPool; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); asid_map_t *asid_map = &asidPool->array[asid & MASK(asidLowBits)]; @@ -948,7 +948,7 @@ void decreaseASIDBindCB(asid_t asid) { asid_pool_t *asidPool; - asidPool = armKSASIDTable[asid >> asidLowBits]; + asidPool = armKSASIDTable[ASID_HIGH(asid)]; assert(asidPool); asid_map_t *asid_map = &asidPool->array[asid & MASK(asidLowBits)]; @@ -1070,7 +1070,7 @@ void deleteASID(asid_t asid, vspace_root_t *vspace) { asid_pool_t *poolPtr; - poolPtr = armKSASIDTable[asid >> asidLowBits]; + poolPtr = armKSASIDTable[ASID_HIGH(asid)]; if (poolPtr != NULL) { asid_map_t asid_map = poolPtr->array[asid & MASK(asidLowBits)]; @@ -1092,7 +1092,7 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) assert((asid_base & MASK(asidLowBits)) == 0); - if (armKSASIDTable[asid_base >> asidLowBits] == pool) { + if (armKSASIDTable[ASID_HIGH(asid_base)] == pool) { for (offset = 0; offset < BIT(asidLowBits); offset++) { asid_map_t asid_map = pool->array[offset]; if (asid_map_get_type(asid_map) == asid_map_asid_map_vspace) { @@ -1102,7 +1102,7 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) #endif } } - armKSASIDTable[asid_base >> asidLowBits] = NULL; + armKSASIDTable[ASID_HIGH(asid_base)] = NULL; setVMRoot(NODE_STATE(ksCurThread)); } } @@ -1293,7 +1293,7 @@ static exception_t performASIDControlInvocation(void *frame, cte_t *slot, ), parent, slot); assert((asid_base & MASK(asidLowBits)) == 0); - armKSASIDTable[asid_base >> asidLowBits] = (asid_pool_t *)frame; + armKSASIDTable[ASID_HIGH(asid_base)] = (asid_pool_t *)frame; return EXCEPTION_NONE; } @@ -1816,7 +1816,7 @@ exception_t decodeARMMMUInvocation(word_t invLabel, word_t length, cptr_t cptr, return EXCEPTION_SYSCALL_ERROR; } - pool = armKSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> asidLowBits]; + pool = armKSASIDTable[ASID_HIGH(cap_asid_pool_cap_get_capASIDBase(cap))]; if (unlikely(!pool)) { current_syscall_error.type = seL4_FailedLookup; diff --git a/src/arch/riscv/kernel/vspace.c b/src/arch/riscv/kernel/vspace.c index 2011b5b56..99dfb47c4 100644 --- a/src/arch/riscv/kernel/vspace.c +++ b/src/arch/riscv/kernel/vspace.c @@ -311,7 +311,7 @@ BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_lvl1pt_cap) { asid_pool_t *ap = ASID_POOL_PTR(pptr_of_cap(it_ap_cap)); ap->array[IT_ASID] = PTE_PTR(pptr_of_cap(it_lvl1pt_cap)); - riscvKSASIDTable[IT_ASID >> asidLowBits] = ap; + riscvKSASIDTable[ASID_HIGH(IT_ASID)] = ap; } /* ==================== BOOT CODE FINISHES HERE ==================== */ @@ -322,7 +322,7 @@ static findVSpaceForASID_ret_t findVSpaceForASID(asid_t asid) asid_pool_t *poolPtr; pte_t *vspace_root; - poolPtr = riscvKSASIDTable[asid >> asidLowBits]; + poolPtr = riscvKSASIDTable[ASID_HIGH(asid)]; if (!poolPtr) { current_lookup_fault = lookup_fault_invalid_root_new(); @@ -444,8 +444,8 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) /* Haskell error: "ASID pool's base must be aligned" */ assert(IS_ALIGNED(asid_base, asidLowBits)); - if (riscvKSASIDTable[asid_base >> asidLowBits] == pool) { - riscvKSASIDTable[asid_base >> asidLowBits] = NULL; + if (riscvKSASIDTable[ASID_HIGH(asid_base)] == pool) { + riscvKSASIDTable[ASID_HIGH(asid_base)] = NULL; setVMRoot(NODE_STATE(ksCurThread)); } } @@ -470,7 +470,7 @@ static exception_t performASIDControlInvocation(void *frame, cte_t *slot, cte_t ); /* Haskell error: "ASID pool's base must be aligned" */ assert((asid_base & MASK(asidLowBits)) == 0); - riscvKSASIDTable[asid_base >> asidLowBits] = (asid_pool_t *)frame; + riscvKSASIDTable[ASID_HIGH(asid_base)] = (asid_pool_t *)frame; return EXCEPTION_NONE; } @@ -495,7 +495,7 @@ void deleteASID(asid_t asid, pte_t *vspace) { asid_pool_t *poolPtr; - poolPtr = riscvKSASIDTable[asid >> asidLowBits]; + poolPtr = riscvKSASIDTable[ASID_HIGH(asid)]; if (poolPtr != NULL && poolPtr->array[asid & MASK(asidLowBits)] == vspace) { hwASIDFlush(asid); poolPtr->array[asid & MASK(asidLowBits)] = NULL; @@ -1046,7 +1046,7 @@ exception_t decodeRISCVMMUInvocation(word_t label, word_t length, cptr_t cptr, return EXCEPTION_SYSCALL_ERROR; } - pool = riscvKSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> asidLowBits]; + pool = riscvKSASIDTable[ASID_HIGH(cap_asid_pool_cap_get_capASIDBase(cap))]; if (!pool) { current_syscall_error.type = seL4_FailedLookup; current_syscall_error.failedLookupWasSource = false; diff --git a/src/arch/x86/kernel/ept.c b/src/arch/x86/kernel/ept.c index 1a2d88b5e..6b48d1690 100644 --- a/src/arch/x86/kernel/ept.c +++ b/src/arch/x86/kernel/ept.c @@ -43,7 +43,7 @@ void deleteEPTASID(asid_t asid, ept_pml4e_t *ept) { asid_pool_t *poolPtr; - poolPtr = x86KSASIDTable[asid >> asidLowBits]; + poolPtr = x86KSASIDTable[ASID_HIGH(asid)]; if (poolPtr != NULL) { asid_map_t asid_map = poolPtr->array[asid & MASK(asidLowBits)]; if (asid_map_get_type(asid_map) == asid_map_asid_map_ept && diff --git a/src/arch/x86/kernel/vspace.c b/src/arch/x86/kernel/vspace.c index fc73f11cd..4b10b7e16 100644 --- a/src/arch/x86/kernel/vspace.c +++ b/src/arch/x86/kernel/vspace.c @@ -39,7 +39,7 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) /* Haskell error: "ASID pool's base must be aligned" */ assert(IS_ALIGNED(asid_base, asidLowBits)); - if (x86KSASIDTable[asid_base >> asidLowBits] == pool) { + if (x86KSASIDTable[ASID_HIGH(asid_base)] == pool) { for (unsigned int offset = 0; offset < BIT(asidLowBits); offset++) { asid_map_t asid_map = pool->array[offset]; if (asid_map_get_type(asid_map) == asid_map_asid_map_vspace) { @@ -47,7 +47,7 @@ void deleteASIDPool(asid_t asid_base, asid_pool_t *pool) hwASIDInvalidate(asid_base + offset, vspace); } } - x86KSASIDTable[asid_base >> asidLowBits] = NULL; + x86KSASIDTable[ASID_HIGH(asid_base)] = NULL; setVMRoot(NODE_STATE(ksCurThread)); } } @@ -72,7 +72,7 @@ exception_t performASIDControlInvocation(void *frame, cte_t *slot, cte_t *parent ); /* Haskell error: "ASID pool's base must be aligned" */ assert((asid_base & MASK(asidLowBits)) == 0); - x86KSASIDTable[asid_base >> asidLowBits] = (asid_pool_t *)frame; + x86KSASIDTable[ASID_HIGH(asid_base)] = (asid_pool_t *)frame; return EXCEPTION_NONE; } @@ -81,7 +81,7 @@ void deleteASID(asid_t asid, vspace_root_t *vspace) { asid_pool_t *poolPtr; - poolPtr = x86KSASIDTable[asid >> asidLowBits]; + poolPtr = x86KSASIDTable[ASID_HIGH(asid)]; if (poolPtr != NULL) { asid_map_t asid_map = poolPtr->array[asid & MASK(asidLowBits)]; if (asid_map_get_type(asid_map) == asid_map_asid_map_vspace && @@ -530,14 +530,14 @@ BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_vspace_cap) { asid_pool_t *ap = ASID_POOL_PTR(pptr_of_cap(it_ap_cap)); ap->array[IT_ASID] = asid_map_asid_map_vspace_new(pptr_of_cap(it_vspace_cap)); - x86KSASIDTable[IT_ASID >> asidLowBits] = ap; + x86KSASIDTable[ASID_HIGH(IT_ASID)] = ap; } asid_map_t findMapForASID(asid_t asid) { asid_pool_t *poolPtr; - poolPtr = x86KSASIDTable[asid >> asidLowBits]; + poolPtr = x86KSASIDTable[ASID_HIGH(asid)]; if (!poolPtr) { return asid_map_asid_map_none_new(); } @@ -1374,7 +1374,7 @@ exception_t decodeX86MMUInvocation( return EXCEPTION_SYSCALL_ERROR; } - pool = x86KSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> asidLowBits]; + pool = x86KSASIDTable[ASID_HIGH(cap_asid_pool_cap_get_capASIDBase(cap))]; if (!pool) { current_syscall_error.type = seL4_FailedLookup; current_syscall_error.failedLookupWasSource = false; diff --git a/src/kernel/boot.c b/src/kernel/boot.c index 2cb210d96..b63981e6b 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -432,7 +432,7 @@ BOOT_CODE create_frames_of_region_ret_t create_frames_of_region( BOOT_CODE cap_t create_it_asid_pool(cap_t root_cnode_cap) { - cap_t ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, rootserver.asid_pool); + cap_t ap_cap = cap_asid_pool_cap_new(ASID_HIGH(IT_ASID), rootserver.asid_pool); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadASIDPool), ap_cap); /* create ASID control cap */