diff --git a/apps/sel4test-tests/src/tests/cache.c b/apps/sel4test-tests/src/tests/cache.c index 5dabd50c..c596ac58 100644 --- a/apps/sel4test-tests/src/tests/cache.c +++ b/apps/sel4test-tests/src/tests/cache.c @@ -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 @@ -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; @@ -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))