apps/sel4test-tests/src/tests/cache.c - 3p/sel4/sel4test - Git at Google

 /*
  * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */

 #include <autoconf.h>
 #include <sel4test-driver/gen_config.h>
 #include <assert.h>
 #include <stddef.h>
 #include <stdio.h>
 #include <sel4/sel4.h>
 #include <vka/object.h>
 #include <vka/capops.h>
 #include <sel4utils/util.h>
 #include <sel4utils/arch/cache.h>

 #include "../helpers.h"
 #include "frame_type.h"

 #if defined(CONFIG_ARCH_ARM)
 static int test_page_flush(env_t env)
 {
     seL4_CPtr frame, framec;
     uintptr_t vstart, vstartc;
     volatile uint32_t *ptr, *ptrc;
     vka_t *vka;
     int error;

     vka = &env->vka;

     void *vaddr;
     void *vaddrc;
     reservation_t reservation, reservationc;

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

     vstart = (uintptr_t)vaddr;
     assert(IS_ALIGNED(vstart, seL4_PageBits));
     vstartc = (uintptr_t)vaddrc;
     assert(IS_ALIGNED(vstartc, seL4_PageBits));

     ptr = (volatile uint32_t *)vstart;
     ptrc = (volatile uint32_t *)vstartc;

     /* Create a frame */
     frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K);
     test_assert(frame != seL4_CapNull);

     /* Duplicate the cap */
     framec = get_free_slot(env);
     test_assert(framec != seL4_CapNull);
     error = cnode_copy(env, frame, framec, seL4_AllRights);
     test_error_eq(error, seL4_NoError);

     /* map in a cap with cacheability */
     error = vspace_map_pages_at_vaddr(&env->vspace, &framec, NULL, vaddrc, 1, seL4_PageBits, reservationc);
     test_error_eq(error, seL4_NoError);
     /* map in a cap without cacheability */
     error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
     test_error_eq(error, seL4_NoError);

     /* Clean makes data observable to non-cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K);
     assert(!error);
     test_assert(*ptr == 0xDEADBEEF);
     test_assert(*ptrc == 0xDEADBEEF);
     /* Clean/Invalidate makes data observable to non-cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     error = seL4_ARM_Page_CleanInvalidate_Data(framec, 0, PAGE_SIZE_4K);
     assert(!error);
     test_assert(*ptr == 0xDEADBEEF);
     test_assert(*ptrc == 0xDEADBEEF);
     /* Invalidate makes RAM data observable to cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K);
     assert(!error);

     /* In case the invalidation performs an implicit clean, write a new
        value to RAM and make sure the cached read retrieves it
        Remember to drain any store buffer!
     */
     *ptr = 0xBEEFCAFE;
 #if defined(CONFIG_ARCH_AARCH32)
     asm volatile("dmb" ::: "memory");
 #elif defined(CONFIG_ARCH_AARCH64)
     asm volatile("dmb sy" ::: "memory");
 #endif /* CONFIG_ARCH_AARCHxx */
     test_assert(*ptrc == 0xBEEFCAFE);
     test_assert(*ptr == 0xBEEFCAFE);

     return sel4test_get_result();
 }

 static int test_large_page_flush_operation(env_t env)
 {
     int num_frame_types = ARRAY_SIZE(frame_types);
     seL4_CPtr frames[num_frame_types];
     int error;
     vka_t *vka = &env->vka;

     /* Grab some free vspace big enough to hold all the tests. */
     seL4_Word vstart;
     reservation_t reserve = vspace_reserve_range_aligned(&env->vspace, VSPACE_RV_SIZE, VSPACE_RV_ALIGN_BITS,
                                                          seL4_AllRights, 1, (void **) &vstart);
     test_assert(reserve.res != 0);

     /* Create us some frames to play with. */
     for (int i = 0; i < num_frame_types; i++) {
         frames[i] = vka_alloc_frame_leaky(vka, frame_types[i].size_bits);
         assert(frames[i]);
     }

     /* Map the pages in. */
     for (int i = 0; i < num_frame_types; i++) {
         uintptr_t cookie = 0;
         error = vspace_map_pages_at_vaddr(&env->vspace, &frames[i], &cookie, (void *)(vstart + frame_types[i].vaddr_offset), 1,
                                           frame_types[i].size_bits, reserve);
         test_error_eq(error, seL4_NoError);
     }

     /* See if we can invoke page flush on each of them */
     for (int i = 0; i < num_frame_types; i++) {
         error = seL4_ARM_Page_Invalidate_Data(frames[i], 0, BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARM_Page_Clean_Data(frames[i], 0, BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARM_Page_CleanInvalidate_Data(frames[i], 0, BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARM_Page_Unify_Instruction(frames[i], 0, BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
                                                         vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
                                                    vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
                                                              vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
         error = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart + frame_types[i].vaddr_offset,
                                                           vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
         test_error_eq(error, 0);
     }

     return sel4test_get_result();
 }

 static int test_page_directory_flush(env_t env)
 {
     seL4_CPtr frame, framec;
     uintptr_t vstart, vstartc;
     volatile uint32_t *ptr, *ptrc;
     vka_t *vka;
     int err;

     vka = &env->vka;

     void *vaddr;
     void *vaddrc;
     reservation_t reservation, reservationc;

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

     vstart = (uintptr_t)vaddr;
     assert(IS_ALIGNED(vstart, seL4_PageBits));
     vstartc = (uintptr_t)vaddrc;
     assert(IS_ALIGNED(vstartc, seL4_PageBits));

     ptr = (volatile uint32_t *)vstart;
     ptrc = (volatile uint32_t *)vstartc;

     /* Create a frame */
     frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K);
     test_assert(frame != seL4_CapNull);

     /* Duplicate the cap */
     framec = get_free_slot(env);
     test_assert(framec != seL4_CapNull);
     err = cnode_copy(env, frame, framec, seL4_AllRights);
     test_error_eq(err, seL4_NoError);

     /* map in a cap with cacheability */
     err = vspace_map_pages_at_vaddr(&env->vspace, &framec, NULL, vaddrc, 1, seL4_PageBits, reservationc);
     test_error_eq(err, seL4_NoError);
     /* map in a cap without cacheability */
     err = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
     test_error_eq(err, seL4_NoError);

     /* Clean makes data observable to non-cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
     assert(!err);
     test_assert(*ptr == 0xDEADBEEF);
     test_assert(*ptrc == 0xDEADBEEF);
     /* Clean/Invalidate makes data observable to non-cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
     assert(!err);
     test_assert(*ptr == 0xDEADBEEF);
     test_assert(*ptrc == 0xDEADBEEF);
     /* Invalidate makes RAM data observable to cached page */
     *ptr = 0xC0FFEE;
     *ptrc = 0xDEADBEEF;
     test_assert(*ptr == 0xC0FFEE);
     test_assert(*ptrc == 0xDEADBEEF);
     err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
     assert(!err);
     /* In case the invalidation performs an implicit clean, write a new
        value to RAM and make sure the cached read retrieves it.
        Need to do an invalidate before retrieving though to guard
        against speculative loads */
     *ptr = 0xBEEFCAFE;
     err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
     assert(!err);
     test_assert(*ptrc == 0xBEEFCAFE);
     test_assert(*ptr == 0xBEEFCAFE);

     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))
	/*
	* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
	*
	* SPDX-License-Identifier: BSD-2-Clause
	*/

	#include <autoconf.h>
	#include <sel4test-driver/gen_config.h>
	#include <assert.h>
	#include <stddef.h>
	#include <stdio.h>
	#include <sel4/sel4.h>
	#include <vka/object.h>
	#include <vka/capops.h>
	#include <sel4utils/util.h>
	#include <sel4utils/arch/cache.h>

	#include "../helpers.h"
	#include "frame_type.h"

	#if defined(CONFIG_ARCH_ARM)
	static int test_page_flush(env_t env)
	{
	seL4_CPtr frame, framec;
	uintptr_t vstart, vstartc;
	volatile uint32_t ptr, ptrc;
	vka_t *vka;
	int error;

	vka = &env->vka;

	void *vaddr;
	void *vaddrc;
	reservation_t reservation, reservationc;

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

	vstart = (uintptr_t)vaddr;
	assert(IS_ALIGNED(vstart, seL4_PageBits));
	vstartc = (uintptr_t)vaddrc;
	assert(IS_ALIGNED(vstartc, seL4_PageBits));

	ptr = (volatile uint32_t *)vstart;
	ptrc = (volatile uint32_t *)vstartc;

	/* Create a frame */
	frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K);
	test_assert(frame != seL4_CapNull);

	/* Duplicate the cap */
	framec = get_free_slot(env);
	test_assert(framec != seL4_CapNull);
	error = cnode_copy(env, frame, framec, seL4_AllRights);
	test_error_eq(error, seL4_NoError);

	/* map in a cap with cacheability */
	error = vspace_map_pages_at_vaddr(&env->vspace, &framec, NULL, vaddrc, 1, seL4_PageBits, reservationc);
	test_error_eq(error, seL4_NoError);
	/* map in a cap without cacheability */
	error = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
	test_error_eq(error, seL4_NoError);

	/* Clean makes data observable to non-cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K);
	assert(!error);
	test_assert(*ptr == 0xDEADBEEF);
	test_assert(*ptrc == 0xDEADBEEF);
	/* Clean/Invalidate makes data observable to non-cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	error = seL4_ARM_Page_CleanInvalidate_Data(framec, 0, PAGE_SIZE_4K);
	assert(!error);
	test_assert(*ptr == 0xDEADBEEF);
	test_assert(*ptrc == 0xDEADBEEF);
	/* Invalidate makes RAM data observable to cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K);
	assert(!error);

	/* In case the invalidation performs an implicit clean, write a new
	value to RAM and make sure the cached read retrieves it
	Remember to drain any store buffer!
	*/
	*ptr = 0xBEEFCAFE;
	#if defined(CONFIG_ARCH_AARCH32)
	asm volatile("dmb" ::: "memory");
	#elif defined(CONFIG_ARCH_AARCH64)
	asm volatile("dmb sy" ::: "memory");
	#endif /* CONFIG_ARCH_AARCHxx */
	test_assert(*ptrc == 0xBEEFCAFE);
	test_assert(*ptr == 0xBEEFCAFE);

	return sel4test_get_result();
	}

	static int test_large_page_flush_operation(env_t env)
	{
	int num_frame_types = ARRAY_SIZE(frame_types);
	seL4_CPtr frames[num_frame_types];
	int error;
	vka_t *vka = &env->vka;

	/* Grab some free vspace big enough to hold all the tests. */
	seL4_Word vstart;
	reservation_t reserve = vspace_reserve_range_aligned(&env->vspace, VSPACE_RV_SIZE, VSPACE_RV_ALIGN_BITS,
	seL4_AllRights, 1, (void **) &vstart);
	test_assert(reserve.res != 0);

	/* Create us some frames to play with. */
	for (int i = 0; i < num_frame_types; i++) {
	frames[i] = vka_alloc_frame_leaky(vka, frame_types[i].size_bits);
	assert(frames[i]);
	}

	/* Map the pages in. */
	for (int i = 0; i < num_frame_types; i++) {
	uintptr_t cookie = 0;
	error = vspace_map_pages_at_vaddr(&env->vspace, &frames[i], &cookie, (void *)(vstart + frame_types[i].vaddr_offset), 1,
	frame_types[i].size_bits, reserve);
	test_error_eq(error, seL4_NoError);
	}

	/* See if we can invoke page flush on each of them */
	for (int i = 0; i < num_frame_types; i++) {
	error = seL4_ARM_Page_Invalidate_Data(frames[i], 0, BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARM_Page_Clean_Data(frames[i], 0, BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARM_Page_CleanInvalidate_Data(frames[i], 0, BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARM_Page_Unify_Instruction(frames[i], 0, BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
	vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
	vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart + frame_types[i].vaddr_offset,
	vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	error = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart + frame_types[i].vaddr_offset,
	vstart + frame_types[i].vaddr_offset + BIT(frame_types[i].size_bits));
	test_error_eq(error, 0);
	}

	return sel4test_get_result();
	}

	static int test_page_directory_flush(env_t env)
	{
	seL4_CPtr frame, framec;
	uintptr_t vstart, vstartc;
	volatile uint32_t ptr, ptrc;
	vka_t *vka;
	int err;

	vka = &env->vka;

	void *vaddr;
	void *vaddrc;
	reservation_t reservation, reservationc;

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

	vstart = (uintptr_t)vaddr;
	assert(IS_ALIGNED(vstart, seL4_PageBits));
	vstartc = (uintptr_t)vaddrc;
	assert(IS_ALIGNED(vstartc, seL4_PageBits));

	ptr = (volatile uint32_t *)vstart;
	ptrc = (volatile uint32_t *)vstartc;

	/* Create a frame */
	frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K);
	test_assert(frame != seL4_CapNull);

	/* Duplicate the cap */
	framec = get_free_slot(env);
	test_assert(framec != seL4_CapNull);
	err = cnode_copy(env, frame, framec, seL4_AllRights);
	test_error_eq(err, seL4_NoError);

	/* map in a cap with cacheability */
	err = vspace_map_pages_at_vaddr(&env->vspace, &framec, NULL, vaddrc, 1, seL4_PageBits, reservationc);
	test_error_eq(err, seL4_NoError);
	/* map in a cap without cacheability */
	err = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation);
	test_error_eq(err, seL4_NoError);

	/* Clean makes data observable to non-cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
	assert(!err);
	test_assert(*ptr == 0xDEADBEEF);
	test_assert(*ptrc == 0xDEADBEEF);
	/* Clean/Invalidate makes data observable to non-cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
	assert(!err);
	test_assert(*ptr == 0xDEADBEEF);
	test_assert(*ptrc == 0xDEADBEEF);
	/* Invalidate makes RAM data observable to cached page */
	*ptr = 0xC0FFEE;
	*ptrc = 0xDEADBEEF;
	test_assert(*ptr == 0xC0FFEE);
	test_assert(*ptrc == 0xDEADBEEF);
	err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
	assert(!err);
	/* In case the invalidation performs an implicit clean, write a new
	value to RAM and make sure the cached read retrieves it.
	Need to do an invalidate before retrieving though to guard
	against speculative loads */
	*ptr = 0xBEEFCAFE;
	err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstartc, vstartc + PAGE_SIZE_4K);
	assert(!err);
	test_assert(*ptrc == 0xBEEFCAFE);
	test_assert(*ptr == 0xBEEFCAFE);

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