cps & contification

[Stephen Weeks]

> Don't worry, I didn't find any new bugs.  Here's an updated description of
> the whole analysis.  I updated the proof that any fixed point of C is safe
> with the new definition of C. 

It all looks great.  Thanks.

> I also added a proof of the claim that
> A'(f) = Uncalled iff there does not exist a path from fm to f.

Here is a shorter proof of half of the claim

Claim: there does not exist a path of calls from fm to f
	==> A'(f) = Uncalled
Proof:
Define A'' (f) = Unknown	if there exists a path of calls from fm to f
	         Uncalled	otherwise
Observe that C (A'') = A''.
Hence A' <= A'' (since A' is lfp).
Hence, if there does not exist a path of calls from fm to f then
	A'(f) <= A''(f) = Uncalled

>  Finally, I
> ran through all of the problematic contification examples from the past
> emails, and they all work out the way we would like.

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

The snapshot that I just made available contains an implementation of the
Lengauer/Tarjan dominator algorithm as described on p. 185-191 of Muchnick's
book.  For testing purposes, I've integrated it so that it runs on the CPS call
graph after removeUseless runs.  It hasn't triggered any failures on the
regressions or a self-compile.  I'd like to have a slightly better way of
checking the result (see the validDominators function in directed-graph.sml).
Does anyone know an easy linear test for correctness of dominators (other than
recomputing them)?

Matthew, are you interested in doing the analysis implementation?  It shouldn't
be too bad given that the dominators algorithm is already there.  If you do, it
might be nice for you to catch up with the latest snapshot, which contains a new
CPS IL, in which many of the lists have been changed to vectors.