[Tinyos Core WG] Safe TinyOS annotation format

[John Regehr]

Please look over the proposed annotation format for Safe TinyOS below,
motivated by the discussion last Weds.

The first issue is determining which modules should be compiled as safe 
code.  We propose two new nesC attributes that are used like this:

module CC2420ActiveMessageP @safe() { ...

module CC2420ActiveMessageP @unsafe() { ...

If this attribute is omitted, the default (according to my understanding
of the current consensus) is unsafe, meaning that pointer/array accesses
in this module are unchecked.  This annotation applies only to modules,
not configurations.

Note that it will always be possible to override these module-level 
preferences by simply not invoking the Deputy compiler.  In that case no 
safety checks are added to an application; this is presumably useful for 
people who are more worried about code size than bugs.

The second issue is reducing the cognitive load due to annotations in
the TinyOS interface files.  Here we propose moving annotations into the 
comments that are parsed by nesdoc.  New nesdoc commands @deputyparam 
and @deputyreturn will serve two purposes.  First, the nesC compiler 
will translate these into regular Deputy annotations.  Second, it should 
be possible for nesdoc to translate annotations into human-readable 
documentation e.g. "the payload parameter is either NULL or refers to a 
memory region containing at least len bytes."

Just to be clear, in this proposal there are two ways to express Deputy 
annotations: the original inline way and a new outline way.  By 
convention, TinyOS interface files would use the latter.

interface Receive {

   /**
    * Receive a packet buffer, returning a buffer for the signaling
    * component to use for the next reception. The return value
    * can be the same as <tt>msg</tt>, as long as the handling
    * component copies out the data it needs.
    *
    * <b>Note</b> that misuse of this interface is one of the most
    * common bugs in TinyOS code. For example, if a component both calls a
    * send on the passed message and returns it, then it is possible
    * the buffer will be reused before the send occurs, overwriting
    * the component's data. This would cause the mote to possibly
    * instead send a packet it most recently received.
    *
    * @param        msg      the receied packet
    * @deputyparam  "COUNT(len) payload"  a pointer to the packet's payload
    * @param        len      the length of the data region pointed to by 
payload
    * @return       a packet buffer for the stack to use for the next
    *               received packet.
    */
   event message_t* receive(message_t* msg, void* payload, uint8_t len);

   /**
    * Return a pointer to a protocol's payload region if it is large
    * enough to hold len bytes. Otherwise return NULL. This command
    * behaves identically to <tt>Packet.getPayload</tt> and is included
    * in this interface as a convenience.
    *
    * @param             msg      the packet
    * @param             len   desired payload length
    * @deputyreturn      "void * COUNT(len)" a pointer to the packet's 
data payload for this layer,
    *    or NULL if the payload is smaller than len bytes
    */
   command void* getPayload(message_t* msg, uint8_t len);

   /**
    * Return the length of the payload of msg. This call is identical
    * to <TT>Packet.payloadLength</TT>, and is included in Receive as a
    * convenience.
    *
    * @param  msg      the packet
    * @return          the length of the packet's payload
    */
   command uint8_t payloadLength(message_t* msg);

}

John Regehr et al.