Skip to content

Commit

Permalink
Address PR feedback
Browse files Browse the repository at this point in the history 
Signed-off-by: Ivan Velickovic <[email protected]>
  • Loading branch information
@Ivan-Velickovic
Ivan-Velickovic committed Jun 16, 2024
1 parent 3e71462 commit d5db3a5
Showing 1 changed file with 90 additions and 90 deletions.
180 changes: 90 additions & 90 deletions apps/sel4test-tests/src/tests/cache.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,91 @@ static int test_page_directory_flush(env_t env)
return sel4test_get_result();
}


DEFINE_TEST(CACHEFLUSH0001, "Test a cache maintenance on pages", test_page_flush, config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0002, "Test a cache maintenance on page directories", test_page_directory_flush,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0003, "Test that cache maintenance can be done on large pages", test_large_page_flush_operation,
config_set(CONFIG_HAVE_CACHE))
#endif


static int test_page_uncached_after_retype(env_t env)
{
seL4_CPtr frame, frame2, untyped;
uintptr_t vstart, vstart2;
volatile uint32_t *ptr, *ptr2;
vka_t *vka;
int error;

vka = &env->vka;

// Create 2 vspace reservations because when we revoke the untyped the state gets out of sync.
void *vaddr;
void *vaddr2;
reservation_t reservation, reservation2;

reservation = vspace_reserve_range(&env->vspace,
PAGE_SIZE_4K, seL4_AllRights, 0, &vaddr);
assert(reservation.res);
reservation2 = vspace_reserve_range(&env->vspace,
PAGE_SIZE_4K, seL4_AllRights, 0, &vaddr2);
assert(reservation2.res);

vstart = (uintptr_t)vaddr;
assert(IS_ALIGNED(vstart, seL4_PageBits));
vstart2 = (uintptr_t)vaddr2;
assert(IS_ALIGNED(vstart2, seL4_PageBits));

ptr = (volatile uint32_t *)vstart;
ptr2 = (volatile uint32_t *)vstart2;

/* Get an untyped */
untyped = vka_alloc_untyped_leaky(vka, PAGE_BITS_4K);
test_assert(untyped != seL4_CapNull);
cspacepath_t src_path;
vka_cspace_make_path(vka, untyped, &src_path);

frame = get_free_slot(env);
test_assert(frame != seL4_CapNull);
cspacepath_t dest_path;
vka_cspace_make_path(vka, frame, &dest_path);
/* Create a frame from the untyped */
error = seL4_Untyped_Retype(untyped, seL4_ARCH_4KPage, PAGE_BITS_4K, dest_path.root, dest_path.dest,
dest_path.destDepth, dest_path.offset, 1);
test_error_eq(error, seL4_NoError);

/* map in the without cacheability */
error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
test_error_eq(error, seL4_NoError);

/* Write some data directly to RAM as it's uncached */
*ptr = 0xC0FFEE;

/* Revoke the untyped. This deletes the frame. */
vka_cnode_revoke(&src_path);

/* Create the frame with the same untyped. The kernel guarantees that the contents have been zeroed. */
error = seL4_Untyped_Retype(untyped, seL4_ARCH_4KPage, PAGE_BITS_4K, dest_path.root, dest_path.dest,
dest_path.destDepth, dest_path.offset, 1);
test_error_eq(error, seL4_NoError);


/* map in the frame without cacheability again. */
error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr2, 1, seL4_PageBits, reservation2);
test_error_eq(error, seL4_NoError);
/* Confirm that the contents are zeroed */
test_assert(*ptr2 == 0x0);


return sel4test_get_result();
}
DEFINE_TEST(CACHEFLUSH0004, "Test that mapping a frame uncached doesn't see stale data after retype",
test_page_uncached_after_retype,
config_set(CONFIG_HAVE_CACHE))

#if defined(CONFIG_ARCH_ARM)

/*
* The following tests aim to test the seL4_ARM_* cache operations on every
* kind of frame mapping that can be created. The motivation behind this is
Expand All @@ -270,16 +355,12 @@ static int test_cache_invalid(env_t env)
{
seL4_CPtr frame;
uintptr_t vstart;
vka_t *vka;
int err;

vka = &env->vka;

void *vaddr;
reservation_t reservation;
vka_t *vka = env->vka;

reservation = vspace_reserve_range(&env->vspace,
PAGE_SIZE_4K, seL4_AllRights, 1, &vaddr);
reservation = vspace_reserve_range(&env->vspace, PAGE_SIZE_4K, seL4_AllRights, 1, &vaddr);
assert(reservation.res);

vstart = (uintptr_t)vaddr;
Expand Down Expand Up @@ -468,93 +549,12 @@ static int test_cache_read_only(env_t env)
return sel4test_get_result();
}

DEFINE_TEST(CACHEFLUSH0001, "Test a cache maintenance on pages", test_page_flush, config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0002, "Test a cache maintenance on page directories", test_page_directory_flush,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0003, "Test that cache maintenance can be done on large pages", test_large_page_flush_operation,
DEFINE_TEST(CACHEFLUSH0005, "Test cache maintenance on invalid mappings", test_cache_invalid,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0004, "Test cache maintenance on invalid mappings", test_cache_invalid,
DEFINE_TEST(CACHEFLUSH0006, "Test cache maintenance on kernel-only mappings", test_cache_kernel_only,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0005, "Test cache maintenance on kernel-only mappings", test_cache_kernel_only,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0006, "Test cache maintenance on read-write mappings", test_cache_read_write,
DEFINE_TEST(CACHEFLUSH0007, "Test cache maintenance on read-write mappings", test_cache_read_write,
config_set(CONFIG_HAVE_CACHE))
DEFINE_TEST(CACHEFLUSH0008, "Test cache maintenance on read-only mappings", test_cache_read_only,
config_set(CONFIG_HAVE_CACHE))

#endif


static int test_page_uncached_after_retype(env_t env)
{
seL4_CPtr frame, frame2, untyped;
uintptr_t vstart, vstart2;
volatile uint32_t *ptr, *ptr2;
vka_t *vka;
int error;

vka = &env->vka;

// Create 2 vspace reservations because when we revoke the untyped the state gets out of sync.
void *vaddr;
void *vaddr2;
reservation_t reservation, reservation2;

reservation = vspace_reserve_range(&env->vspace,
PAGE_SIZE_4K, seL4_AllRights, 0, &vaddr);
assert(reservation.res);
reservation2 = vspace_reserve_range(&env->vspace,
PAGE_SIZE_4K, seL4_AllRights, 0, &vaddr2);
assert(reservation2.res);

vstart = (uintptr_t)vaddr;
assert(IS_ALIGNED(vstart, seL4_PageBits));
vstart2 = (uintptr_t)vaddr2;
assert(IS_ALIGNED(vstart2, seL4_PageBits));

ptr = (volatile uint32_t *)vstart;
ptr2 = (volatile uint32_t *)vstart2;

/* Get an untyped */
untyped = vka_alloc_untyped_leaky(vka, PAGE_BITS_4K);
test_assert(untyped != seL4_CapNull);
cspacepath_t src_path;
vka_cspace_make_path(vka, untyped, &src_path);

frame = get_free_slot(env);
test_assert(frame != seL4_CapNull);
cspacepath_t dest_path;
vka_cspace_make_path(vka, frame, &dest_path);
/* Create a frame from the untyped */
error = seL4_Untyped_Retype(untyped, seL4_ARCH_4KPage, PAGE_BITS_4K, dest_path.root, dest_path.dest,
dest_path.destDepth, dest_path.offset, 1);
test_error_eq(error, seL4_NoError);

/* map in the without cacheability */
error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
test_error_eq(error, seL4_NoError);

/* Write some data directly to RAM as it's uncached */
*ptr = 0xC0FFEE;

/* Revoke the untyped. This deletes the frame. */
vka_cnode_revoke(&src_path);

/* Create the frame with the same untyped. The kernel guarantees that the contents have been zeroed. */
error = seL4_Untyped_Retype(untyped, seL4_ARCH_4KPage, PAGE_BITS_4K, dest_path.root, dest_path.dest,
dest_path.destDepth, dest_path.offset, 1);
test_error_eq(error, seL4_NoError);


/* map in the frame without cacheability again. */
error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr2, 1, seL4_PageBits, reservation2);
test_error_eq(error, seL4_NoError);
/* Confirm that the contents are zeroed */
test_assert(*ptr2 == 0x0);


return sel4test_get_result();
}
DEFINE_TEST(CACHEFLUSH0009, "Test that mapping a frame uncached doesn't see stale data after retype",
test_page_uncached_after_retype,
config_set(CONFIG_HAVE_CACHE))

0 comments on commit d5db3a5

Please sign in to comment.