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, mailto:Adrian.Danis@data61.csiro.au> wrote: Not being able to get error information after doing an invocation is unacceptable as a default. I suppose if you have an application where you *know* you won't need the error information then you might want to re-enable this. Ideally we come up with some better stub generation that doesn't throw away the errors. OK, clearly I have to read these functions way more closely to grok the difference. :-) Oddly, I can't find any public code that uses the *WithMRs functions. In order to give them regular exercise, would you like me to add some of them to the syscalls tests? :-) Thanks, Jeff

On Thu 27-Oct-2016 1:12 PM, Jeff Waugh wrote: On Thu, Oct 27, 2016 at 12:08 PM, mailto:Adrian.Danis@data61.csiro.au> wrote: 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. I can see the more complex generated functions (that use more than the number of available real registers) are comfy using SetMR before and GetMR after *WithMRs calls. I'm assuming a SetMR is safe after the *WithMRs call? Correct me if I've misunderstood something in there, but it seems about right. Naively, would the following be appropriate to generate: LIBSEL4_INLINE long seL4_ARM_Page_Map(seL4_ARM_Page service, seL4_ARM_PageDirectory pd, seL4_Word vaddr, seL4_CapRights rights, seL4_ARM_VM Attributes attr) { ... /* Perform the call, passing in-register arguments directly. */ output_tag = seL4_CallWithMRs(service, tag, &mr0, &mr1, &mr2, seL4_Null); /* Unmarshal real register results into the IPC buffer. */ seL4_SetMR(0, mr0); seL4_SetMR(1, mr1); seL4_SetMR(2, mr2); // 4th register isn't relevant for this function, but would be elsewhere return seL4_MessageInfo_get_label(output_tag); } This is where things start to get complicated. Different errors have a different number of words for their fault. In the worst case this can be 5 words, so all 4 message registers on arm need to be stored. Without some detailed information to the syscall stub generator of exactly which invocations can cause which errors, you're looking at just always stashing all 4 MRs back into the IPC buffer. Could probably optimize this by checking the label before return and storing the MRs only if an error happened. I actually cannot think of a compelling reason for why that wouldn't work.... Either there is something I've forgotten, or the solution really is that simple. Adrian