CWS paper

[Matthew Fluet]

> Matthew sent a proposed fix to the continuation based analysis to handle this
> problem.  Intuitively, it made sense, but I haven't quite figured out how to
> make an analysis of it.

Here's the sketch of the analysis I had in mind, as an extension of
Reppy's, tailored to the MLton CPS IL.

Let  Label = {f : f is top level CPS function name} U  
             {k : k is local return continuation} 
I guess this corresponds to the Func.t and the Jump.t types. 

Let  Return = {"return to f" | f in Label}.

Then, let  RCont = Label U Return U bot. 
Note, RCont is _not_ a domain, because we can't impose a partial order on 
RCont.  Instead, we'll impose the order on functions.

The result will still be  Gamma in REnv = Label -> RCont
Define the partial order REnv's as follows:

Gamma1 <= Gamma2  
iff  
forall l in Label. Gamma1(l) <=l Gamma2(l)
where
bot <=l l' <=l "return to l"   forall l' in Label, l' <> "return to l"

The idea is that the partial order <=l turns RCont into a squashed
powerset domain, with bot for the empty set, l' for the singleton
set {l}, and "return to l" for everything else.  Essentially, each
function and continuation gets a unique top-element.  Now, REnv is a
cpo (even though it is not the cpo of continuous functions from Label ->
RCont, which doesn't exist, because RCont isn't a cpo).  Least upper
bounds Gamma1 V Gamma2 are computed point-wise with the least upper bound
for <=l.  So,

Gamma1 V Gamma2
 = {l |--> r | l in Label
               r = case (Gamma1(x), Gamma2(x))
                     of (bot, r') => r'
                      | (r', bot) => r'
                      | (r1, r2) => if r1 = r2
                                     then r1
                                     else "return to l"}


I then imagined that the analysis on the CPS IL would go something like
this:

Program analysis:
Anal[<fun fi (<xij>*) = ei>*] = fix (fn Gamma => V_i R[ei] Gamma'(fi))
 where Gamma' = Gamma V {ft |--> "return to ft"}
   and ft is the main function
(fixed point necessary because top level CPS functions are mutually recursive)
(initializing ft to "return to ft" marks the main function and ensures
that bot really corresponds to no calls)

Dec analysis:
R[let fun k <xi>* = e in e']p = R[e]p' V Gamma
 where Gamma = R[e']p and p' = Gamma(k)
R[let val x = s in e']p = R[e']p

Transfer analysis:
R[f (<xi>*)]p = {f |--> p}
R[k (f (<xi>*))]p = {k |--> p} V {f |--> k}
R[k (<xi>*)]p = {k -> p}
R[<xi>*]p = {}
R[case x of <Ci => ki>]p = V_i {ki |--> p}

The notation <exp(i)>* indicates a list of expressions, indexed by i.
The notation V_i indicates the join over all i.


If Gamma = Anal[program]  and Gamma(l) = r  and  r <> "return to l",
 then the function with label l has exactly one continuation 
 and is contifiable.
Further, if Gamma(l) = bot, then the function with label l is never called.


Note that the join is taken over all sub-analysis, so for an
implementation, it would be sufficient to keep one property list that is
updated (or two, one for Func.t and one for Jump.t).

Examples: (unless otherwise specified, all calls are tail calls)

fun f () = let ... in loop () end
fun loop () = let ... in loop () end
fun g () = ... K1 (f ()) ... K2 (f ()) ...

Gamma(f) = "return to f"
Gamma(loop) = "return to f"


fun f () = let 
            fun K () = ...
            ...
              ... K (g (x)) ...
            ...
              ... K (g (x)) ...
fun g () = ...

Gamma(g) = K
           

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

Gamma(f) = K
Gamma(g) = K


fun f () = ... g () ... g () ...
fun g () = ... f () ...
fun h () = ... K1 (f ()) ... K2 (f ()) ...

Gamma(f) = "return to f"
Gamma(g) = "return to f"


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

Gamma(f) = K
Gamma(g) = K
Gamma(h) = K


Those were all the problematic examples that were brought up before.  This
essentially works by "abstracting" the rest of the continuation for any
function which returns to a function which is determined to have multiple
return continuations.