On Thu, Oct 27, 2016 at 12:08 PM, <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);

}

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