diff --git a/apps/sel4test-tests/src/tests/smc.c b/apps/sel4test-tests/src/tests/smc.c index 07736ec4..91e068ee 100644 --- a/apps/sel4test-tests/src/tests/smc.c +++ b/apps/sel4test-tests/src/tests/smc.c @@ -74,4 +74,133 @@ static int test_smc_calls(env_t env) } DEFINE_TEST(SMC0001, "Test SMC calls", test_smc_calls, true) + +int test_smc_2(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_copy(env, env->smc, dest, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} +DEFINE_TEST(SMC0002, "SMC Caps can be copied", test_smc_2, true) + +int test_smc_3(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_copy(env, env->smc, dest, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + error = cnode_revoke(env, env->smc); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0003, "Copied SMC Caps lose revocable authority", test_smc_3, true) + +int test_smc_4(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0004, "Unbadged SMC Caps can be badged", test_smc_4, true) + + +int test_smc_5(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_mint(env, dest, dest2, seL4_AllRights, 2); + test_error_eq(error, seL4_IllegalOperation); + test_assert(is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0005, "Badged SMC caps cannot change badge", test_smc_5, true) + +int test_smc_6(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_copy(env, dest, dest2, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} +DEFINE_TEST(SMC0006, "Badged SMC caps can be copied", test_smc_6, true) + + +int test_smc_7(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_copy(env, dest, dest2, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + error = cnode_revoke(env, dest); + test_assert(is_slot_empty(env, dest2)); + + return sel4test_get_result(); +} + +DEFINE_TEST(SMC0007, "Original badged SMC caps can revoke copies", test_smc_7, true) + +int test_smc_8(env_t env) +{ + + seL4_CPtr dest = get_free_slot(env); + int error = cnode_mint(env, env->smc, dest, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest)); + + seL4_CPtr dest2 = get_free_slot(env); + error = cnode_mint(env, env->smc, dest2, seL4_AllRights, 1); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest2)); + + + seL4_CPtr dest3 = get_free_slot(env); + error = cnode_copy(env, dest2, dest3, seL4_AllRights); + test_error_eq(error, seL4_NoError); + test_assert(!is_slot_empty(env, dest3)); + + error = cnode_revoke(env, dest2); + test_assert(is_slot_empty(env, dest3)); + test_assert(!is_slot_empty(env, dest)); + + return sel4test_get_result(); +} + + +DEFINE_TEST(SMC0008, "Original badged SMC caps don't revoke other original badges", test_smc_8, true) + #endif