limit check insertion

[Matthew Fluet]

> I like this, and would add one more thing, at least to the safety
> part, and have the limit check insertion return
> 
> 	limitCheck: label -> Nat option
> 	available: label -> Nat
> 
> so that we can easily check that limit check insertion has produced a
> safe, and hence sound function.

Nat or Nat option on limitCheck doesn't really matter.  Until we care
about threads, I would say that limitCheck(l) = SOME 0 is basically
equivalent to limitCheck(l) = NONE, so a simple Nat suffices.  But no big
deal either way.

The limit check insertion returning both it's limit check's and the
witness is good.

> > So, either there are a set of start labels (corresponding to
> > the "real" start label and then all continuation and handler labels) or
> > the start label is a dummy label with next(ls) being the real start label
> > and all continuation and handler labels.
> 
> I prefer the latter, keeping the framework simple, and slightly
> complicating how the IL is translated to a problem within the
> framework.

Fine by me.  It's just going to turn into a graph problem, so a single
root is probably the way to go.


> I would still like to hear opinions on the short term fix of
> restricting limit check coalescing to basic blocks.

Meaning, let alloc(l) = sum of allocations in the block and setting
limitCheck(l) = alloc(l)?

Sounds cheap and quick (to write); I guess we need to see how it plays out
in practice to determine how quickly we need to move to something else.
I've got no objections to it.