cps & contification
Matthew Fluet
fluet@CS.Cornell.EDU
Fri, 26 Jan 2001 09:19:33 -0500 (EST)
> > 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