# Viper Encoding

## Future Generator Type
* each future generator is encoded as its own unique type, as they have different upvars and thus fields
* encoded like a struct with these fields:
* one field per upvar (i.e. argument captured in the generator)
* serves as the field that is actually present on the generator type
* may be read and mutated in the generator's body
* not used and thus not exposed to calling code
* initialized by future constructor
* one ghost field per upvar
* serves as a snapshot of the initial upvar's value at the point of calling the `async fn` / future constructor
* comparable to `old`-expressions
* neither read nor mutated by generator body
* guaranteed to be unchanged by poll stub
* initialized by future constructor
* single field for state (currently `u32`, but might be changed to custom `enum`)
* states correspond to labels of points in the code in which the generator may be when not currently polled, i.e. initialized, suspension points, or finished (currently not encoded)
* intialized to 0 (initialized, but not yet polled)
* suspension points may be labeled by user (see later)
* unlabeled suspension points are automatically assigned unique labels by [`SuspensionPointAnalysis`](https://github.com/erdmannc/prusti-dev/blob/async-testing/prusti-encoder/src/encoders/async/suspension_points.rs)
* poll stub requires and ensures that state belongs to set of valid labels
* generic arguments are just the generic arguments inherited from the parent context, no additional ones for `resume_ty`, `yield_ty`, etc.

## Preconditions
* simple preconditions about the arguments passed to a call to an `async fn` work out of the box, as they simply end up as that precondition on the future constructor
* preconditions also incorporating the future generator to be put on the poll method are currently not supported (see section on such postconditions below for more details)

## Postconditions
* simple postconditions relating result to arguments are supported
* can be specified by decorating an `async fn` with `#[ensures(...)]`
* [marked as `async` postconditions](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-contracts/prusti-specs/src/lib.rs#L135) and [collected as their own entry in method specs](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-interface/src/specs/mod.rs#L208)
* [creates two spec items](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-contracts/prusti-specs/src/lib.rs#L261), both of which are (initially) attached to the generator body, as the poll stub does not exist in rust/MIR:
* [the postcondition itself](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-contracts/prusti-specs/src/lib.rs#L269), which will be added to the generator body ([by the standard encoding of the body as a method](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-encoder/src/encoder_traits/impure_function_enc.rs#L224) since the postcondition was moved from the future constructor to the body)
* [a version wrapped in `Poll`](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-contracts/prusti-specs/src/rewriter.rs#L151) (containing the postcondition for `Ready(result)` and `true` for `Pending`), which will be added to the poll stub ([as the poll stub encoder uses `async` postconditions instead of postconditions](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-encoder/src/encoders/async/poll_stub.rs#L379))
* enabling caller to actually make use of postcondition requires some work due to busy loop:
* [take snapshot of arguments passed to future constructor](https://github.com/erdmannc/prusti-dev/blob/1d301db212b57b1c65bea95c440b5f9dcdab2627/prusti-encoder/src/encoders/mir_impure.rs#L1305) in order to refer back to them later, thereby acting similarly to `old`-expressions
* [add invariant to busy loop, stating that generator's ghost fields are equal to these snapshots](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L647), in order to tie ghost fields (which appear in the poll stub's postconditions) to the values passed to the future as arguments
* this way, when obtaining the meaningful postcondition in the `Ready` branch after polling, we obtain a postcondition relating the result inside `Ready` to the generator's ghost fields. Due to our invariant, we can thus relate the obtained result to the snapshots of the arguments passed to the future in its constructor call (which corresponds to the "call" of the `async fn` at the rust level)

* postconditions also involving the generator to be put on the poll stub are currently not supported
* could be implemented by introducing different syntax so they are collected differently and only requested by poll stub encoder
* implementation would be similar to `async` invariants (except only adding them as postcondition)
* should be able to refer to both generator and all of its fields, e.g. to express how mutable upvars might change in relation to their initial value or how state changes depending on upvars in the case of interior mutability or channels
* might be necessary in order to really make use of suspension point labels, on-exit- and on-entry conditions by expressing how future generator makes progress

## Async Invariants
* express properties that future and caller guarantee to each other when control flow switches between them without exposing future's internals (e.g. suspension points) to calling code
* may be violated temporarily by future between suspension points
* calling code may only temporarily violate between poll calls, meaning it cannot violate it at a lowered `.await`
* not necessarily guaranteed by future constructor, so responsibility of establishing before first poll (or making sure arguments passed to future constructor will satisfy invariant) lies with calling code
* specified by decorating `async fn` with `#[async_invariant(..)]`
* in generator body:
* [expression evaluated with arguments substituted by upvar fields read from generator](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/pure/spec.rs#L288)
* all async invariants are [added as invariants to the each suspension point's busy loop](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L676)
* they are also [exhaled at every `yield`](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L1432) [as well as `return`](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L1058)
* NOTE: currently, invariants inside the body are encoded using the wrong place for the generator, namely the one containing the first argument instead of the one containing the generator in the busy loop. This should be possible to fix by manually encoding (using `MirPureEnc`) and reifying with the correct place (which can be obtained from the `SuspensionPointAnalysis`)
* in the poll stub, all invariants are added [as pre-](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/poll_stub.rs#L360) and [postconditions](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/poll_stub.rs#L394)

## Suspension Point Specifications
* also provide contracts between future and calling code at suspension points
* more fine-grained, may differ between suspension points as well as between guarantees for calling code and future
* annotated using [`suspension_point!` macro](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-contracts/prusti-specs/src/lib.rs#L526):

suspension_point!(
    #[label(1)]
    #[on_exit(x > 0)]
    #[on_entry(true)]
    fut.await
)

* expanded to something like this:

{
    let fut = fut.await;
    suspension_point_on_exit_marker(1, (|| x > 0,));
    let res = fut.await;
    suspension_point_on_entry_marker(1, (|| true,));
    res
}

* marker functions are dummies that should never be called and only serve to preserve the (tupled up) on-exit/on-entry condition closures
* label:
* should uniquely identify suspension point
* 0 currently reserved for initialized but not yet polled
* unlabeled suspension points are [labeled by `SuspensionPointAnalysis`](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/suspension_points.rs#L119)
* currently only integers, should at some point be extended to an `enum` with variant for each albel
* on-exit conditions:
* must hold when future yields / returns `Pending` at that suspension point
* in body: encoded by [replacing the marker function call with exhaling condition bodies](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L1082)
* in poll stub: [encoded as precondition](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/poll_stub.rs#L356) that must only hold [if generator is in state corresponding to suspension point](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/poll_stub.rs#L301)
* on-entry conditions:
* must hold when future is resumed / polled again at that suspension point
* encoded analogously to on-exit conditions (but are inhaled and added as postcondition)
* NOTE: these two types of conditions are rather awkward to encode, as they are bodies of closures. Specifically, the closure body takes a reference to a closure object and reads captured upvars (i.e. future arguments in our case) from that closure object. Therefore, we sometimes need to create such a reference to a closure in order to encode and in-/exhale these conditions.
* TODO: currently, on-exit conditions are exhaled right before and on-entry conditions are inhaled right after a suspension point (like in the expanded code), but once shared state is supported, they need to be ex-/inhaled before/after all shared state is havoced when yielding, as the awaited future might also share some of that state. This should be possible to implement by reading the BBs containing the marker function calls when encoding the `yield` and then in-/exhaling the conditions there.

# (Some) Implementation Details
* Spec collection
* when spec collector encounters an async body, it [locates its corresponding constructor (i.e. the parent in the HIR) and marks both as such](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-interface/src/specs/mod.rs#L550)
* when determining a method's specs, [they are ignored](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-interface/src/specs/mod.rs#L161)
* after determining all method specs, [all async specs attached to some parent are instead moved to the child](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-interface/src/specs/mod.rs#L228)
* Suspension point analysis
* can be accessed like all other encoders (even though it technically doesn't encode anything)
* attempts to locate suspension points by detecting their pattern of basic blocks, see [`check_suspension_point`](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/async/suspension_points.rs#L164), where this pattern is documented
* for the most part, this only considers terminators and ignores the statements in the BBs
* also attempts to determine the locals containing the future when it is created, just before the busy loop, and inside the busy loop as well as the local containing the pinned reference inside the busy loop
* in order to this, assignments inside relevant BBs are considered, aborting if the BBs contain unexpexted statements (note that the list of "expected" statements might need to be extended at some point)
* this heuristic might be imprecise for some code, but has been reliable so far. note, however, that it will probably always be possible to manually "fake" such a pattern that is indistinguishable from a "real" suspension point.
* Busy loop invariants
* the busy loops corresponding to suspension points require some additional invariants in order to be able to verify code
* permissions to both the [generator](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L673) and [`ResumeTy` argument](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L674) need to be preserved
* [equality between ghost fields and future argument snapshots](https://github.com/erdmannc/prusti-dev/blob/ed930ce5730ad751ae58f1b688832fb78b8ad62a/prusti-encoder/src/encoders/mir_impure.rs#L647) also needs to be preserved
* Creating the most generic type of a generator requires some care
* only "actual" generic arguments on the `async fn` (i.e. those obtained from the parent, not `resume_ty`, `witness_ty`, etc) should be replaced by placeholders
* we use `List::identity_for_item` in order to get placeholders with correct names, as creating placeholders ourselves might result in us misnaming parameters that are used in the upvars (note that attempting to recreate the names from the parent-args also doesn't work, since they might already be substituted)
* the placeholders corresponding to the parent args are extracted based on the generic parameters' layout, so we need to make sure this stays stable
* Since the upvar types might already contain some substitutions (and simply replacing all upvar types by generic placeholders is also wrong), we use `TyCtxt::type_of` to obtain a "most generic" version of the generator type (and thus upvar types)
* the witness type is replaced by some dummy in order to make sure all occurrences of the same generator type are resolved to the same most generic type (this is also the case for some other types)

# Limitations
* heavy manual patching due to missing support for references or pledges for `Pin`
* manual patching for unspecified `IntoFuture::into_future` call
* currently, poll stub also ensures permission to pinned reference back to caller, which is *not* how prusti usually operates, but done here in order to get updated generator back and update it inside busy loop
* slightly limited detection of suspension points as well as tracking of future's places from constructor call to suspension point
* so far, everything is only for `async fn`'s, `async` blocks need to be handled slightly differently

# TODOs
* update state inside generator body
* add label for finished state, in which generator may be after poll stub call
* async invariants need to be correctly encoded in generator bodies, accounting for the generator being moved to different places

# Working with`async` Constructs

## StateTransform Pass
* defined in `compiler/rustc_mir_transform/src/generator.rs`
* called as part of lowering passes from analysis MIR to runtime MIR
* happens *after* borrow-check
* called by queries `promoted_mir` and `mir_drops_elaborated_and_const_checked`
* passes between `after_analysis` and `StateTransform`:
* `run_analysis_cleanup_passes`
* `CleanupPostBorrowck`: remove MIR parts no longer necessary after borrow-check, e.g. false edges, user type annotations, and replaces the following with noop: `AscribeUserType` / `FakeRead` / `Assign` with shallow borrow
* `RemoveNoopLandingPads`: remove dummy blocks on unwind paths
* `SimplyCfg-early-opt`: , collapses goto-chains, change branches with identical targets to goto, merge switch targets identical with otherwise, merges singular goto-blocks with successor, removes noops, removes duplicate unreachable blocks, removes dead blocks
* `Derefer`
* `run_runtime_lowering_passes`:
* `AddCallGuards` / `CriticalCallEdges`: remove critical edges (edges that are neither only outgoing nor only incoming) around calls by inserting new blocks, necessary due to LLVM using slightly different terminators
* `ElaborateDrops`: change drops from value may be dropped here to value will be dropped here and destructor run, i.e. avoid dropping when uninitialized
* `AbortUnwindingCalls`: if compiled with `panic=abort`, catches all possible unwinds and aborts instead
* `AddMovesForPackedDrops`: moves values dropped in a packed struct to temporary, so they are dropped from aligned address
* `ElaborateBoxDerefs`: transform derefs of boxes to derefs of underlying pointer
* `StateTransform`

## Generator Type
* passed as first argument to poll method
* can be inspected by getting the first `mir::Local` (wrapper around an index) of a `mir::Body` using `args_iter` and then indexing into `body.local_decls`
* its `ty` should be a `ty::TyKind::Generator`
* `generic_args` field can be converted to `ty::GeneratorArgs` using `as_generator`-method to conveniently access information
* see also documentation of `ty::ClosureArgs` for information about generator arguments
* according to `rustc_mir_transform` doc, generator struct looks like this:

struct Generator {
    upvars...,
    state: u32,
    mir_locals...,
}

* state is a discriminant, to inspect states and their names use methods `discriminants` and `variant_name`
* generally, the states are `Unresumed`, `Returned`, `Panicked`, `Suspend0`, ...
* to see the types of variables each state holds (i.e. locals that outlive a suspension point), use `state_tys` method
* use `generator_layout` method on `TyCtxt` for more information on layout
* generator type can be obtained from the constructor's return type (which is an opaque type alias) using `type_of` or `expand_opaque_types` (on 1.74, on latest use `try_expand_impl_trait_type`) methods on `TyCtxt`, see also [`param_env_reveal_all_normalized`](https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.param_env_reveal_all_normalized)
* note that there is `opaque_ty_origin` on the `TyCtxt`

## Detecting `async` Constructs
* Poll Method / Generator
* `TyCtxt` provides methods to check whether a `DefId` is `async`, namely `generator_is_async`, `asyncness`, or `generator_kind`
* `TyCtxt::generator_kind` can be used to check the kind of `async` construct (by inspecting the `hir::AsyncGeneratorKind` within a returned `hir::GeneratorKind::Async`)
* `mir::Body` also provides `generator_kind`
* note that the above is for rustc 1.74.0 (what prusti uses as of now), for current nightly (1.76.0):
* `DefKind::Generator` no longer exists
* `TyCtxt` provides `coroutine_is_async`, `coroutine_is_async_gen`, and `asyncness`

* Future Constructor
* in the HIR, the constructor is an `Item` of variant `ItemKind::Fn`
* use `expect_fn` on the `Item` to obtain a `FnSig`
* the `FnSig` contains a `FnHeader`, which in turn has an `asyncness` field, which will be `IsAsync::Async` for future constructors

* Linking Generator to Constructor
* obtain generator's `HirId` using `local_def_id_to_hir_id`
* constructor is its parent in the HIR (`opt_parent_id`)
*