cps & contification

[Matthew Fluet]

> We should also try to figure out the relaxation of the safety that is just
> sufficient to meet the lexical scoping constraints of the IL.

Consider the following:

Given an analysis A, define A* : Fun -> 2^RCont as follows:
    A*(f) = 
         {f} U (if A(f) in Fun
                  then A*(A(f))
                  else {A(f)})

An analysis A is safe for program p = (fm, T, N) if 
        *   A(fm) = Unknown
        **  For all nontail calls (f, g, j) in N,
                A(f) = Uncalled 
                or A(g) in {j, Unknown}
        *** For all tail calls (f, g) in T,
                A(f) = Uncalled
                or A(g) in A*(f) U {Unknown}
(note the change in ***).

(Easy proof is that {f, A(f)} subset A*(f), so this version of safety is a
relaxation of the previous version.)

Lexical scoping will still be possible (although maybe harder to compute).
Suppose (f, g) in T and Reach(f) (and assume no mutual recursion problems).
 If A(f) = Unknown and A(g) = Unknown: no problem.
 If A(f) = Unknown and A(g) = h2 in Fun, then h2 = f: no problem.
 If A(f) = j1 in Jump and A(g) = Unknown: no problem.
 If A(f) = j1 in Jump and A(g) = j2 in Jump, then j1 = j2: no problem.
 If A(f) = j1 in Jump and A(g) = h2 in Fun, then h2 = f: no problem.
 If A(f) = h1 in Fun and A(g) = Unknown: no problem.
 If A(f) = h1 in Fun and A(g) = j2 in Jump,
  then f is made a local function in h1
   now either A(h1) = j or A(h1) = h2 in Fun.
    if A(h1) = j, then h1 and g are added to the same function, 
                   so put g before h1.
    if A(h1) = h2, then h1 is made a local function in h2 
                   and repeat until have A(hn) = j
                   and put g before hn.
 If A(f) = h1 in Fun and A(g) = f in Fun
  then f is made a local function in h1
   and g is made a local function in f
 If A(f) = h1 in Fun and A(g) = i in Fun, i <> f
  then f is made a local function in h1
   now either A(h1) = i or A(h1) = h2 in Fun
    if A(h1) = i, then put g before f in h1
    if A(h1) = h2, then h1 is made a local function in h2
                    and repeat until have A(hn) = i
                    and put g before hn

If we have mutual recursion, all the functions participating in the mutual
recursion will have the same continuation, so the scc and outside caller
check will still work.

But, the upshot of this is that we can use the same G but define A as
    A(f) = 
         if parent(f) = Root
           then if Reach(f) then Unknown else Uncalled
         else parent(f)

and get an analysis that is safe, provably minimal (in the same way as
before), and contifies those two annoying functions in logic.

If we decide to go the route of making local functions mutually recursive
in the CPS IL, then this doesn't buy us much of anything, other than
better nesting of functions.  But, I was just curious to see how much
modification it would take to push this definition of safety and A
through.  The changes are actually fairly minor.  I needed a few lemmas
to talk about A*(f) and a general pattern of proof was to prove something
for A*(f) and then consider the restriction to A(f).  Another interesting
result was slightly modified minimality constraints:

Theorem 14: Let B be a safe analysis.
            If B(f) = Uncalled, then A(f) = Uncalled.
            If B(f) = j in Jump, then A(f) in {Uncalled, j} U Fun.
            If B(f) = h in Fun, then A(f) in {Uncalled} U Fun.

(the previous theorem had
            If B(f) = j in Jump, then A(f) in {Uncalled, j}.
            If B(f) = h in Fun, then A(f) in {Uncalled} U Jump U Fun.)

This arises because B(f) = j/h pins down some dominator of f in G and we
know that j in Jump nodes must have (Root, j) in Edge.

When assigning A(f) by walking back up the dominator tree, if j in Jump is
a dominator, then we must assign A(f) = j.  But when just looking at the
parent of f, if it is a Jump node, it must be j, but it could also be any
Fun node.

Similarly when B(f) = h in Fun. If h in Fun is a dominator of f, then
parent(f) <> Root and parent(f) <> j in Jump.  So parent(f) = g in Fun.
When walking up the dominator tree, we could find out that the ancestor is
either a Fun or a Jump.  But the parent must be a Fun.