seL4/camkes-tool

Error message for unsupported connection is misleading

Closed this issue · 3 comments

Given the helloworld assembly in http://sel4.systems/CAmkES/README.pml, i.e.,

assembly {
    composition {
        component Hello h;
        component Client c;
        connection seL4RPC conn(from c.iface, to h.inf);
    }
}

if you get the from and to mixed up (like I did the first time, because I didn't just copy and paste), i.e.,

        connection seL4RPC conn(from h.inf, to c.iface);

then the resulting error message is vague and doesn't suggest that this was the mistake:

Unresolved references in input specification:
 .../seL4/apps/helloworld/helloworld.camkes:11:'inf' of type Interface
 .../seL4/apps/helloworld/helloworld.camkes:11:'iface' of type Interface

What the parser is trying to indicate here is that it tried to look in h for an outgoing interface called inf and failed to find one. Similarly, it failed to find an incoming interface called iface in c.

I agree that this is confusing because, from a user point of view, incoming and outgoing interfaces share the same namespace. I confess I've made this mistake and been confused by this message myself. We could look into something more user-friendly here.

Okay. Great!

I don't remember if I explored this precisely when refactoring the CAmkES parser, but I believe on the "next" branch this is now handled in a more user-friendly way during so-called "freezing" (camkes/ast/objects.py:474-549). The complexity of back porting this logic to "master" is probably not worth it, but hopefully this pain point is only temporary until "next" becomes "master" (he says, conscious of this issue having been open for two years...).