IntInf asserts

[Matthew Fluet]

> Given  that the bignum C code already knows how to roll back the heap and how
> to change the size of an array, I would say that the correct thing to  do  is
> to  have  the  primitive  combine  the  check-for-space  and  then call the C
> function.  I can move the allocation into the C code and I would  think  that
> that kind of thing could be useful for other C code.

I was thinking about the IntInf allocation problem a little more.  Would
it make sense to make array allocation and int-inf allocation a little
more uniform?  My thoughts were somthing like this: switching the type of
the IntInf primitives basically requires some function of the form: 

val bytesNeeded: {prim: Prim.t, args: 'a vector} -> 'a option

(I would expect 'a to be instantiated to either SsaTree.Var.t or
Machine.Operand.t.  In the former case, we would use bytesNeeded to find
the blocks that do allocation in primitives and to insert the maybe limit
checks.  In the later case, we would use bytesNeeded to instantiate a
LimitCheck statement.)

Big picture: I'm shooting for a modification of the Machine IL where
AllocateArray isn't it's own statement; rather, Array_array (or
Array_allocate (see below)) just sticks around as a prim.  AllocateArray
is priviledged because it does allocation; so, it gets it's own GCInfo.t
and auxilary stuff to do it's own limit check.  But, in both codegen's,
the same limit check emitter is used -- either with a constant or a
computed bytesNeeded.  Seems extraneous.  And, with IntInf_* primitives
doing allocation themselves, either they become priviledged statements, or
we give them GCInfo.t's (like runtime primitives) and codegens know how to
extract the bytesNeeded and insert the limit checks.  

I think it would be better if LimitCheck statements were the only things
that gave rise to limit checks; if bytesNeeded {prim, args} = SOME x, for
some Assign {dst, prim, args, ...} statement, then the limit check
insertion code needs to ensure that x bytes are available at the Assign
statement.  (I think this fits in better with the limit check insertion
formalization.)  This means that LimitCheck statement would have bytes as
an Operand.t instead of int.

How would this work in practice?  IntInf_* are easy, with the proposal to
give them the type
   val add = _prim "IntInf_add": int * int * Int.int -> int
Then
fun bytesNeeded {prim, args} =
   case Prim.name prim of
      IntInf_add => Vector.sub (args, 2)
    | ...

Array_array is a little harder.  What I would propose is a quick rewrite
after Representations have been establised.  Run over the SSA program,
rewrite (excuse bad notation) every
Statement.T {var, ty, exp = Exp.Prim {prim = Array_array, targs, args, ...}}
into 
let
  val v0 = Var.newNoname ()
  val v1 = Var.newNoname ()
  val v2 = Var.newNoname ()
in
  Statement.T {var = SOME v0,
               ty = Type.int,
               exp = Exp.Const (sizeof (Vector.sub (targs, 0)) in bytes)}
  Statement.T {var = SOME v1, 
               ty = Type.int, 
               exp = Exp.Prim {prim = Int_mul,
                               args = Vector.new2
                                      (Vector.sub (args, 0), v0)}
  Statement.T {var = SOME v2,
               ty = Type.int
               exp = Exp.Prim {prim = Int_add
                               args = Vector.new2
                                      (v1, (var for the constant 8))}
  Statement.T {var = var,
               ty = ty,
               exp = Exp.Prim {prim = Array_allocate,
                               args = Vector.new2
                                      (Vector.sub(args, 0), v2)}}
end

i.e., explicitly calculate the bytes needed by the array allocation and
stuff it in an SSA variable.

Now,
fun bytesNeeded {prim, args} =
   case Prim.name prim of
      Array_allocate => Vector.sub (args, 1)
    | ...

(In actuality, we might want to make Array_allocate take 4 args -- length,
bytesNeeded, numPointers, and numNonPointers.  The last two will be
integer constants, so they won't need to be allocated in pseudo-regs or
stack.)


Err... Need to run to colloquium, but there is a little more.  The major
point of this is that it might give the pass that actually chooses the
number of bytes for a limit check a little more freedom.  For example,
right now, doing
fun two_arrays n = (Array.array (n, 0), Array.array (n, 0))
is always going to require two limit checks.  But, we could be smart, and
realize that when it gets down to:

val v1 = n * 4 + 2
val a1 = Array_allocate (n, v1, _, _)
val v2 = n * 4 + 2
val a2 = Array_allocate (n, v2, _, _)
val t = (a1, a2)
return t

we can rewrite it as

val v1 = n * 4 + 2
val v2 = n * 4 + 2
val v3 = v1 + v2
val a1 = Array_allocate (n, v1, _, _)
val a2 = Array_allocate (n, v2, _, _)
val t = (a1, a2)
return t

and only do one limit check for v3 bytes.

I think this could be even more benefitial for IntInf's; think about
taking the dot product of two 3-tuples of IntInf's.  We could compute the
maximum size of all the IntInf results, do one limit check.  (Cross
product isn't so good -- the sizes of the intermediate results 
are needed, so we need some additional limit checks.)


Just some thoughts...