To give a bit more detailed explanation. Take the Page_Map invocation, more concretely let's look at seL4_ARM_Page_Map in the case where we do not pass --buffer
LIBSEL4_INLINE long
seL4_ARM_Page_Map(seL4_X86_Page service, seL4_CPtr vroot, seL4_Word vaddr, seL4_CapRights rights, seL4_ARM_VMAttributes attr)
{
seL4_MessageInfo_t tag = seL4_MessageInfo_new(ARMPageMap, 0, 1, 3);
seL4_MessageInfo_t output_tag;
seL4_Word mr0;
seL4_Word mr1;
seL4_Word mr2;
/* Setup input capabilities. */
seL4_SetCap(0, vroot);
/* Marshal input parameters. */
mr0 = vaddr;
mr1 = rights;
mr2 = attr;
/* Perform the call, passing in-register arguments directly. */
output_tag = seL4_CallWithMRs(service, tag,
&mr0, &mr1, &mr2, seL4_Null);
return seL4_MessageInfo_get_label(output_tag);
}
Now let's suppose we call this, and it returns an error.
seL4_Error error = seL4_X86_Page_Map( [args] );
if (error == seL4_FailedLookup) {
/* do something */
}
Now in the case of a failed lookup when mapping a page the kernel gives us some useful information, it tells us how far through traversing the paging structures it got, before it failed to find something. (okay, on ARM the only failure can be because of a missing page table, but on x86_64 it becomes more relevant). So let's go and do that (please note that libsel4 has constants and helpers for all these, I've put in the raw constants to make the example easier)
seL4_Word failed_bits = seL4_GetMR(2);
if (failed_bits == 20) {
/* need a page table */
} else {
/* something crazy just happened */
}
Now here's the problem. We want message register two. But on ARM, the first 4 message registers are done actually in register (not the IPC buffer). When we called seL4_CallWithMRs, it gave returned us message register 2 in the variable we passed to it, but we have then thrown it away, thus forever losing the error information.
As for adding more tests, people are always encouraged to do that :)
Adrian
On Thu 27-Oct-2016 11:49 AM, Jeff Waugh wrote:
On Thu, Oct 27, 2016 at 11:03 AM,