Note [EPT enforcement]

The goal of EnforceEPT pass is to mark as many binders as possible as EPT
(see Note [Evaluated and Properly Tagged]).
To find more EPT binders, it establishes the following

EPT INVARIANT:
> Any binder of
>   * a strict field (see Note [Strict fields in Core]), or
>   * a CBV argument (see Note [CBV Function Ids])
> is EPT.

(Note that prior to EPT enforcement, this invariant may *not* always be upheld.
An example can be found at the end of this Note.)
This is all to optimise code such as the following:

  data SPair a b = SP !a !b
  case p :: SP Bool Bool of
    SP x y ->
      case x of
        True  -> ...
        False -> ...

We can infer that the strict field x is EPT and hence may safely
omit the code to enter x and the check for the presence of a tag that goes along
with it. However we still branch on the tag as usual to jump to the True or
False case.

Note that for every example involving strict fields we could find a similar
example using CBV functions, e.g.

  $wf x[EPT] y =
    case x of
      True  -> ...
      False -> ...

is the above example translated to use a CBV function $wf.
Note that /any/ strict function can in principle be chosen as a CBV function;
however, we presently only promote worker functions such as $wf to CBV because
we see all its call sites and can use the proper by-value calling convention.
More precisely, with -O0, we guarantee that no CBV functions are visible in
the interface file, so that naïve clients do not need to know how to call CBV
functions. See Note [CBV Function Ids] for more details.

Specification

EPT enforcement works like implicit type conversions in C, such as from int to
float, only much simpler (no overloaded operations such as +).
For EPT enforcement, the "type system" in question is whether a binder is
statically EPT. We differentiate "EPT binder" from "non-EPT binder", where the
latter means "might be EPT, but we could not prove it so".
In this sense, EPT binders form a subtype of non-EPT binders.
We differentiate two conversion directions:

  * Downcast: EPT binders can be converted into non-EPT binders for free.
  * Upcast: non-EPT binders can be converted into EPT binders by inserting an eval.

The EPT invariant expresses type signatures. In particular, these type
signatures entail two things:

  * A _precondition_: Any binder that is passed as a CBV arg/strict field
    must be EPT (i.e. must have type "EPT binder").
  * A _postcondition_: Any binder of a CBV arg/strict field is EPT.

EPT enforcement is then simply a matter of figuring out where to insert
Upcasts (remember that Downcasts are free).
Since Upcasts (evals!) are not free, it is desirable to insert as few as possible.
To this end, we run a static *EPT analysis*, the purpose of which is to identify
as many EPT binders as possible.
Beyond discovering case binders and value bindings, EPT analysis exploits the
type signatures provided by the EPT invariant, looks inside returned tuples and
does some limited amount of fixpointing.
Afterwards, the *EPT rewriter* inserts the actual evals realising Upcasts.

Implementation


* EPT analysis is implemented in GHC.Stg.EnforceEpt.inferTags.
  It attaches its result to /binders/, not occurrence sites.
* The EPT rewriter establishes the EPT invariant by inserting evals. That is, if
    (a) a binder x is used to
          * construct a strict field (`SP x y`), or
          * passed as a CBV argument (`$wf x`),
        and
    (b) x was not inferred EPT,
  then the EPT rewriter inserts an eval prior to the call, e.g.
    case x of x' { __ DEFAULT -> SP x' y }.
    case x of x' { __ DEFAULT -> $wf x' }.
  (Recall that the case binder x' is always EPT.)
  This is implemented in GHC.Stg.EnforceEpt.Rewrite.rewriteTopBinds.
  This pass also propagates the EPTness from binders to occurrences.
  It is sound to insert evals on strict fields (Note [Strict fields in Core]),
  and on CBV arguments as well (Note [CBV Function Ids]).
* We also export the EPTness of top level bindings to allow this optimisation
  to work across module boundaries.
  NB: The EPT Invariant *must* be upheld, regardless of the optimisation level;
  hence EPTness is practically part of the internal ABI of a strict data
  constructor or CBV function. Note [CBV Function Ids] contains the details.
* Finally, code generation skips the thunk check when branching on binders that
  are EPT. This is done by `cgExpr`/`cgCase` in the backend.

Evaluation

EPT enforcement can have large impact on spine-strict tree data structure
performance. For containers the reduction in runtimes with this optimization
was as follows:

intmap-benchmarks:    89.30%
intset-benchmarks:    90.87%
map-benchmarks:       88.00%
sequence-benchmarks:  99.84%
set-benchmarks:       85.00%
set-operations-intmap:88.64%
set-operations-map:   74.23%
set-operations-set:   76.50%
lookupge-intmap:      89.57%
lookupge-map:         70.95%

With nofib being ~0.3% faster as well.

Note that EPT enforcement may cause regressions in rare cases.
For example consider this code:

  foo x = ...
    let c = StrictJust x
    in ...

When x cannot be inferred EPT, the rewriter transforms to

  foo x = ...
    let c = case x of x' -> StrictJust x'
    in ...

which allocates an additional thunk for `c` that returns the constructor.  Boo!