contification paper

[Matthew Fluet]

> How about we just use Reach in the definition of safety.  I.E.
> 	* if not(Reach(f)) then A(f) = Uncalled

Sounds like a good idea.

> After all, reachability is a trivial concept and any sane analysis would do this 
> (okok I know an old implementation of the contifier didn't :-).

Actually, neither does the new version I wrote up.  Which does mean that
it could be potentially cyclic:

fun f () = ... g () ...
fun g () = ... f () ...

The new transformation would raise an error, because the analysis is
cyclic.  The old transformation would actually go into an infinite 
loop.

The cont analysis has the same problem:

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

and in this case the acyclicity wouldn't be caught by the current version
of the transformation, so both analyses would diverge.

Obviously these have never occured in practice; I'm assuming that
removeUseless gets rid of uncalled functions like these.  What's kind of
surprising is that there are so many found in a self-compile.

In any event, it's easy fixes for the new versions of each transformation.
Reach is computed once before any of the analyses, so it will be easy to
incorporate them into these two.

> Hmmm.  I just thought of another possibility.  What if we use the A* safety
> definition, the parent analysis, and your latest transformation, but still
> pretend we have mutual recursion.  Maybe that's not too complicated.

I still suggest sticking with the original definition of safety.  I've got
proofs worked out for minimality of the analysis using A*, but they
require extra lemmas like:

(General purpose lemmas)
Lemma 2: Let B be an analysis.
         If h in Fun and h in B*(g),
          then h = g 
            or there exists f0,...,fn in Fun
               such that A(g) = f0 and A(fi) = fi+1 and h = fn.
Lemma 3: Let B be an analyis.
         If h in Fun and h in B*(g) then B*(h) subseteq B*(g).
(to prove safety)
Lemma 8: Let fi in Fun and Root -> l -> f0 -> ... -> fn is a path in D,
         If l in Fun, A*(fn) = {fn, ..., f0, l, Unknown}.
         If l in Jump, A*(fn) = {fn, ..., f0, l}.
(to prove minimality)
Lemma 10: Let B be a safe analysis.
          Let Root -> l -> f0 ... -> fn be a path in G.
          Then B*(fn) subset {fn, ..., f0, l, Unknown}.
Corollary 11: Let B be a safe analysis.
              Let Root -> l -> f0 ... -> fn be an acyclic path in G.
              Then B(fn) in {fn-1, ..., f0, l, Unknown}.

Corollary 11 is the only one that has an analogy in the proofs with the
original definition of safety, and for that we don't need the acyclicity
of the path in G.

The only motivation for A* and the more complicated transformation is to
contify a couple (and remember, literally two functions in one benchmark) 
of extra functions.  Even if you run with the parent analysis, you need to
do something to deal with mutual recursion.  The new transformation looks
just like the old transformation in these cases. 

So, the caveat for any benchmark results is that mutual recursion is
simulated by nesting where possible (and there is only one benchmark where
it is not possible).

> Good.  So we can stick with the one transformation that works for any safe
> analysis.  I think it's ok to present a slightly historically inaccurate call
> analysis, possibly with an incomprehensibly vague note about nesting.

We may not have to be that vague.  Something to note is the fact that this
whole analysis could be repeated on the body of each top level function to
transform them (with the simplification that there are no non-tail calls,
only tail calls between local functions).  When we do the nesting, we just
exploit the fact that we can transform an analysis A such that 
S = {g | A(g) = f} and exacty one element of g' in S is called by f, into
another safe analysis A' on the body of the transformed f where 
A(g') = Unknown, A(g) = g' for g \in S - {g'}, and A(j) = Unknown for all
other local functions of f. 

Or maybe that's getting too complicated.