cps & contification

[Matthew Fluet]

> > Also, I've been working on a proof that
> > If B is a safe analysis and B(f) = h in Fun, then A(f) in {Uncalled} U Fun.
> > The idea is the following: if B(f) = h and A'(f) <> Uncalled, then h must
> > dominate f in G.  But it keeps slipping away.
> 
> I finally pushed it through, although it's not as clean as I'd like it.
> But, here's the final result, which I think works as a reasonable proof of
> minimality (modulo the IL issues that have come up).
> 
> Claim: Let B be a safe analysis.
>        If B(f) = Uncalled, then A(f) = Uncalled.
>        If B(f) = j in Jump, then A(f) <= j.
>        If B(f) = h in Fun, then A(f) in {Uncalled} U Fun.       

Unfortunately, the last implication is not true...

> Claim: Let B be a safe analysis.
>        If A'(f) = j in Jump, then B(f) in {j, Unknown}.
>        If A'(f) = Unknown, then B(f) in {Unknown} U Fun.
> Proof: Simple enough; little contradictions using the version of the claim
>         above for A' (i.e., just drop the last implication).

because the last implication here is not true.  The quick counter example
is the following:

fun fm () = ... K (f ()) ...
fun f () = ... g () ...
fun g () = ...

Then A'(fm) = Unknown
     A'(f) = K
     A'(g) = K

But B(fm) = Unknown
    B(f) = K
    B(g) = f
is safe.


So, the best we can say is
If B(f) = h in Fun, then A'(f) in {Uncalled, Unknown} U Jump
                     and A(f) in {Uncalled} U Jump U Fun

Combined with the two other implications which are true, we still have the
result that if some safe analysis says a function is contifiable
somewhere, then our analysis also determines that the function is
contifiable (or uncalled).



After I found the error above, I started thinking about the possibility of
doing the entire analysis using the dominator approach. Here's a sketch of
what I was thinking:

Define a directed graph G_call = (Node_call, Edge_call) where 
        Node_call = Fun
        Edge_call = {(f, g) | (f, g) in T}
                    U {(f, g) | (f, g, j) in N}

Define A'(f) = Unknown   if there exists a path from fm to f in G_call
             = Uncalled  otherwise

Fact: A' is a safe analysis.

Define a directed graph G = (Node, Edge) where
	Node = Jump U Fun U {Root}
	Edge = {(Root, fm)} 
               U {(Root, j) | j in Jump}
               U {(f, g) | (f, g) in T and A'(f) <> Uncalled
                                       and A'(g) = Unknown}
               U {(j, g) | (f, g, j) in N and A'(f) <> Uncalled
                                          and A'(g) = Unknown}

Let D be the dominator tree of G rooted at Root.
For f in Fun, let parent(f) be the parent of f in D.

Define an analysis, A, based on A' and D as follows:
    A(f) = 
         if parent(f) = Root
           then A'(f)
         else the ancestor l of f in D such that parent(l) = Root