Allow a function to associated with both new and use interface annotations

[duncanatt]

The current implementation allows a function to be annotated with exactly one new or use mailbox annotation. This is too strict because it does not support tail-recursive functions with receive blocks. For instance:

-new({pong_mb, [pong/0]}).
-use({pong_mb, [pong/0]}).
...
-spec pong() -> no_return().
pong() ->
  ?mb_assert_regex("*(Ping + Stop)"),
  receive
    {ping, Ping} ->
      Ping ! {pong},
      pong();
    {stop} ->
      pong_exit()
  end.

The pong/0 function above would need to be rewritten to make use of a second function, pong_loop/0 as follows:

-new({pong_mb, [pong/0]}).
-use({pong_mb, [pong_loop/0]}).
...
-spec pong() -> no_return().
pong() ->
  pong_loop().

-spec pong_loop() -> no_return().
pong_loop() ->
  ?mb_assert_regex("*(Ping + Stop)"),
  receive
    {ping, Ping} ->
      Ping ! {pong},
      pong_loop();
    {stop} ->
      pong_exit()
  end.

We want to allow tail-recursive functions to be associated with both new and use modalities in mailbox annotations.

[duncanatt]

Using -new and -use to annotate function calls

There are two cases where functions are used in code:

1. spawn expressions, and
2. call expressions.

Currently, typespec annotations permit developers to associate functions with mailbox interfaces and one of two usage modalities: new and use. These determine the default usage modalities for when functions are called (i.e., point 2 above).

However, inline code annotations via the ?new and ?use macros can be used to alter this behaviour in a limited way. If no such annotations are provided, then paterl defaults to the modalities declared in typespecs; otherwise, the modality described by the inline code annotations ?new and ?use takes precedence. This applies only to function call expressions but not spawn expressions.

The inline code annotations ?new and ?use may be omitted whenever the function being called or spawned is implicit (i.e. the function name is an atom). In this case, the usage modality is obtained from the typespec declaration. Explicit function (i.e. the function name is an expression) usages must be annotated with ?new and ?use since the modality cannot be obtained from the typespec declaration.

spawn and call expressions

The usage modality is obtained via the following rules:

• a spawn expression always assigns a new modality for a function f regardless of the modality specified for f in typespecs
• a call expression to a function f assigns the modality specified for f in typespecs

In summary:

Expression	Modality in typespec	Modality in inline annotation	Final assigned modality
* spawn	Any	Only new permitted	new
* call	new	new	new
call	new	use	use
call	use	new	Error
* call	use	use	use

Developers need not specify inline code annotations for the cases marked with an asterisk since the final assigned modality (last column) can be obtained from typespecs. It also makes the code less verbose. A function declared with the new modality in typespecs can always be superseded by an inline code use annotation. However, a function declared with a use modality in typespecs cannot be superseded by an inline code new annotation (we have not yet found a use-case where this makes sense).

The above table applies only to cases where the function being spawned or called is implicit. Explicit function spawns and calls must always be annotated with inline code annotations ?new or ?use since the mailbox interface association cannot be inferred from typespecs. In this case, the developer is fully trusted and paterl assigns the annotation as specified without any error checking.