cps & contification

[Matthew Fluet]

> 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.       

The proof of the last implication uses two lemmas:

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).

Claim: Let B be a safe analysis.
       Let Root -> f0 -> ... -> fn be a path in G.
       Then B(fn) in {fn-1, ..., f0, B(f0), Unknown}.
Proof: trivial induction using ***.


Here's the proof for the last implication.  Like I said, it's not quite as
clean as I'd like it.  The basic idea is as above.  Either A'(f) =
Uncalled, in which case A(f) = Uncalled, or A'(f) = Unknown, in which
case we prove that h dominates f in G, so parent(f) <> Root and A(f) in
Fun.  It goes straight back to the definition of dominates: pick any path
from Root to f and show that h has to appear somewhere on the path.

Claim: Let B be a safe analysis.
       If B(f) = h in Fun, then A(f) in {Uncalled} U Fun.
Proof:
Let B be a safe analysis.
Suppose B(f) = h in Fun.
 Then A'(f) in {Uncalled, Unknown} (by previous claim).
 Suppose A'(f) = Uncalled.
  Then A(f) = A'(f) because (Root, f) in Edge (by second clause).
  Hence A(f) = Uncalled.
 Suppose A'(f) = Unknown.
  Then (Root, f) notin Edge (by second clause).
  Suppose f = fm.
   Then B(f) = Unknown (because B is safe).
   But B(f) = h in Fun. ==><==
  Hence f <> fm and (Root, f) notin Edge (by first clause).
  Suppose there exists (g, f, j) in N such that A'(g) <> Uncalled.
   Then there exists a path of calls from fm to g (by previous claim).
   Hence, B(g) <> Uncalled (because B is safe).
   Therefore, B(f) in {j, Unknown}.
   But B(f) = h in Fun. ==><==
  Hence there does not exist (g, f, j) in N such that A'(g) <> Uncalled
   and (Root, f) notin Edge (by third clause).
  Thus, every path from Root to f in G has length greater than 1.
  Suppose Root -> g0 -> ... -> gn -> f is a path from Root to f in G.
   Then B(f) = h in {gn, ..., g0, B(g0), Unknown} (by previous claim).
   Note (Root, g0) in Edge implies g0 = fm 
                                or A'(g0) <> Unknown 
                                or there exists (g, g0, j) in N 
                                   such that A'(g) <> Uncalled.
   Suppose g0 = fm.
    Then B(g0) = Unknown (because B is safe).
   Suppose A'(g0) <> Unknown.
    Then A'(g0) = Uncalled or A'(g0) = j in Jump.
    Suppose A'(g0) = Uncalled.
     Then (g0, g1) notin Edge (by fourth clause). ==><==
    Suppose A'(g0) = j in Jump.
     Then B(g0) in {j, Unknown} (by previous claim).
   Suppose there exists (g, g0, j) in N such that A'(g) <> Uncalled.
    Then there exists a path of calls from fm to g (by previous claim).
    Then B(g) <> Uncalled (because B is safe).
    Then B(g0) in {j, Unknown}.
   Hence, B(g0) in {Unknown} U Jump.
   Therefore, B(f) = h in {gn, ..., g0, Unknown} U Jump.
   Thus, there exists i such that gi = h.
  Hence, any path from Root to f in G passes through h.
  Therefore, h dominates f in G.
  Then, parent(f) <> Root.
  Hence, A(g) in Fun.