On Thu, Oct 27, 2016 at 12:08 PM,
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); } At the moment, the generator only spews unmarshalling code if there are output parameters. I can hang an else on that to generate the SetMR calls. As for adding more tests, people are always encouraged to do that :)
Cool, I'll add some. :-) Thanks, Jeff