Collect postconditions for async fns

[erdmannc]

Create two specification functions for postconditions on async fn (one for the poll implementation and a wrapped one for the poll call stub) and collect them into the spec-graph.

[xldenis]

Do you have anything I can read about the semantics of your async postconditions?

[erdmannc]

Sure, this special handling of postconditions on asynchronous functions is due to their lowering to futures. Specifically, all functions declared as async are transformed to a type implementing the Future trait and a corresponding poll method (by rewriting the async fn's body as a state machine as described here).

This lowering happens in two stages: First, in the analysis MIR (where prusti operates), the async fn is lowered to a generator type as well as a closure for advancing the generator. That closure (which corresponds to the poll method) takes as parameters the generator object to advance and a ResumeTy (indicating whether the generator should be advanced or dropped) and its return type is the original async fn's return type (and not wrapped in Poll).
Only later, in the runtime MIR, that generator is further lowered to a state machine, which returns Poll<T> instead of T.
Notably, while the generator's poll method has not yet been lowered, it invokes other futures in their fully lowered form - by calling poll inside a busy loop, yielding if it returns Pending and continuing if it returns Ready(result) - since they may or may not have been lowered from an asynchronous construct.

This has a couple of consequences regarding async postconditions for us. Namely, all attributes (e.g. the prusti::post_spec_id_ref) are attached to the future/generator type's constructor rather than the poll method. Therefore, we need to keep track of which postconditions are async postconditions and make sure they are attached to the poll method during spec-collection.

Furthermore, the spec-item's arguments (and thus typing inside the postcondition) match those of the original async fn and not those of the poll method. This means that we also cannot simply encode the postcondition as usual, but need to fix the arguments available to it.

Finally, notice that due to the different lowering stages, we will need two poll methods with different specifications for each future on the viper level. Naturally, we need the actual encoded poll implementation with return type T with the (slightly adjusted due to the parameter mismatch) postcondition in order to check a future's implementation against its specification.
However, we also need a bodyless call stub with return type Poll<T> with a wrapped postcondition - saying that if the method returns Ready(result), then result satisfies the original postcondition - in order to make the future's specification available to other async code invoking it.

This draft simply serves to illustrate a possible way of distinguishing synchronous and asynchronous postconditions and making sure they are attached to the right methods.

I hope that helps, just let me know if I can elaborate on something.