From 2b29446484ffdac45901fadcdf81f55a14e70344 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 10 Jan 2024 10:04:39 +1100 Subject: [PATCH] aarch64/vspace: add performASIDControl annotations Type and ghost state annotations for verification. Signed-off-by: Gerwin Klein --- src/arch/arm/64/kernel/vspace.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/arch/arm/64/kernel/vspace.c b/src/arch/arm/64/kernel/vspace.c index a5e5175c9..2304e6181 100644 --- a/src/arch/arm/64/kernel/vspace.c +++ b/src/arch/arm/64/kernel/vspace.c @@ -1244,10 +1244,13 @@ static exception_t performPageGetAddress(pptr_t base_ptr, bool_t call) static exception_t performASIDControlInvocation(void *frame, cte_t *slot, cte_t *parent, asid_t asid_base) { + /** AUXUPD: "(True, typ_region_bytes (ptr_val \frame) 12)" */ + /** GHOSTUPD: "(True, gs_clear_region (ptr_val \frame) 12)" */ cap_untyped_cap_ptr_set_capFreeIndex(&(parent->cap), MAX_FREE_INDEX(cap_untyped_cap_get_capBlockSize(parent->cap))); memzero(frame, BIT(seL4_ASIDPoolBits)); + /** AUXUPD: "(True, ptr_retyps 1 (Ptr (ptr_val \frame) :: asid_pool_C ptr))" */ cteInsert( cap_asid_pool_cap_new(