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

asidpools: consistently use ASID_HIGH macro

Browse source 
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 <git.ts@trainwit.ch>
This commit is contained in:
julia 2025-08-04 11:04:53 +10:00 committed by Indan Zupancic
parent 5aa9729ec3
commit b8e81b077a
11 changed files with 47 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
include/arch/arm/arch/32/mode/object/structures.h
View file

@ -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 */

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

@ -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)
{

2
include/arch/riscv/arch/object/structures.h
View file

@ -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;

3
include/arch/x86/arch/32/mode/object/structures.h
View file

@ -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");
}

3
include/arch/x86/arch/64/mode/object/structures.h
View file

@ -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;
}
}

21
src/arch/arm/32/kernel/vspace.c
View file

@ -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;

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

@ -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;

14
src/arch/riscv/kernel/vspace.c
View file

@ -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;

2
src/arch/x86/kernel/ept.c
View file

@ -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 &&

14
src/arch/x86/kernel/vspace.c
View file

@ -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;

2
src/kernel/boot.c
View file

@ -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 */