limit check insertion

[Stephen Weeks]

> I see what's going on.  The way limit checks are inserted is just
> plain wrong.  I need to take some time to think about it.

The current limit check pass is wrong because it does not take into
account all paths in the control-flow graph.  The difficulty arises
because it attempts to "coalesce" limit checks across basic blocks.  I
don't see an easy fix.  Over time, I am sure we can figure out
something that is correct and works across blocks, and have included a
framework below to start us thinking.  But, in the meantime, I propose
to replace the current limit check insertion with one that only
coalesces within blocks, and is hence "obviously" correct and "easy"
to implement.  My gut feeling is that this is good enough, and we may
not even want to consider the more complicated stuff below.

If others agree, I will start work with this as my #1 todo.  It
shouldn't take more than restricting the current pass a bit.

--------------------------------------------------------------------------------

Domains:
	l in Label
	s in Statement = Nat + Nat
	  written Alloc(n), LimitCheck(n)
	f as (ls, at, next) 
		in Func = Label x (Label -> Statement) x (Label -> P(Label))
	  ls is the start label
	  at tells the statement at a given label
	  next tells the labels that are next after a given label

Definition [path]:
A path in (ls, at, next) is a finite sequence of labels l0, l1, l2, ..., ln
with l_i+1 in n(li).

Definition [V]:
   V: Path x Int -> Int
   V ([], n) = n
   V (l :: p, n) = n - m  if at(li) = Alloc(m)
		   m      if at(li) = LimitCheck(m)

Intuitively, V gives how much memory is available after executing the statements
along the path.

Definition [sound]:
A function (ls, at, next) is sound if for all paths p = [ls, ..., ln] 
V (p, 0) >= 0.  

Intuitively, soundness means that after each allocation, there is space
remaining.

Definition [annotation]:
An annotation is a map in Label -> Nat.

Intuitively, an annotation gives a lower bound on the amount of space available
at the beginning of each label.

Definition [correct]:
An annotation A is correct if for all paths p = [ls, ..., ln, l_n+1]
V([ls, ..., ln], 0) >= A(l_n+1).

Theorem: If A is correct for f, then f is limit check correct.

Definition [safe]:
Annotation A is safe for (ls, at, next) if for all l
	forall l' in next(l)
		if at(l) = Alloc(m), then A(l') <= A(l) - m
		if at(l) = LimitCheck(m), then A(l') <= m

Theorem: If A is safe for f, then A is correct for f.

Corollary: If A is safe for f, then f is sound.

The job of limit check insertion is to take a function that doesn't have any
limit checks, produce an equivalent sound function that does have limit checks.
Hopefully it does this by producing a safe annotation that can be checked by
another pass.