cps & contification

[Matthew Fluet]

> Cool.  Now all we need is a (definition of and a) proof of minimality and an
> implementation.

I was thinking about trying to prove that the analysis A is the least safe
analysis under the RCont ordering extended pointwise to analyses.  But
this won't work, because of nesting of functions:

fun h () = ...
fun g () = ... h () ...
fun f () = ... g () ...
fun fm () = ... L1 (f ()) ... L2 (f ()) ...

Then A(fm) = Unknown
     A(f) = Unknown
     A(g) = f
     A(h) = f

But, B(fm) = Unknown
     B(f) = Unknown
     B(g) = f
     B(h) = g
is also a safe analysis, but is incomparable to A.

It seems like for tail calls (f, g) in T, we want to favor A(g) = A(f)
over A(g) = f.

On the other hand, there are some interesting properties that can be
shown.  If B is a safe analysis and B(f) = Uncalled, then A'(f) =
Uncalled and A(f) = Uncalled.  Likewise, if B is a safe analysis and B(f)
= j in Jump, then A'(f) <= j and A(f) <= j.

However, I did discover one "bug" in the definition of Edge, which would
have prevented any proof of minimality (for some reasonable definition).

Consider:

fun u () = ... K (g ()) ...
fun g () = ...
fun f () = ... g() ...
fun fm () = ... L1 (f ()) ... L2 (f ()) ...

Then A'(fm) = Unknown
     A'(f) = Unknown
     A'(g) = Unknown
     A'(u) = Uncalled

Edge =
{(Root, fm)}
U {}
U {(f,g)}
U {(Root, f), (Root, g)}

And A(fm) = Unknown
    A(f) = Unknown
    A(g) = Unknown
    A(u) = Uncalled,
but we would really like A(g) = f.

Similarly,

fun u () = ... g () ...
fun g () = ...
fun f () = ... g () ...
fun fm () = ... L1 (f ()) ... L2 (f ()) ...

A'(fm) = Unknown
A'(f) = Unknown
A'(g) = Unknown
A'(u) = Uncalled

Edge =
{(Root, fm)}
U {(Root, u)}
U {(u, g), (f, g)}
U {(Root, f)}

A(fm) = Unknown
A(f) = Unknown
A(g) = Unknown
A(u) = Uncalled,
but we would like A(g) = f.


The solution is to change the definition of Edge to the following:
        Edge = {(Root, fm)}
               U {(Root, f) | A'(f) <> Unknown}
               U {(f, g) | (f, g) in T and A'(f) <> Uncalled
                                       and A'(g) = Unknown}
               U {(Root, g) | (f, g, j) in N and A'(f) <> Uncalled 
                                             and A'(g) = Unknown}

Only minor changes to the proofs of safety and connectivity.

Also, I was considering a slightly different definition of A:

A(f) = if parent(f) = Root
         then A'(f)
         else the ancestor g of f such that parent(g) = Root

It's equivalent to the original definition, but I thought that less
branches in the definition might simplify a proof of minimality.  It also
shows a little more clearly when we fall back to the A' analysis.