ocaml/ocaml — pull request #115 by xavierleroy (2014-11-06 09:23:24+00:00)
Title: More precise typing of the C-- and Mach intermediate languages

This branch makes register typing at the C-- and Mach level more precise.

Benefits:
* Safeguard against incorrect optimizations that break the GC interface.
* Possibly smaller sets of roots communicated to the GC.
* More opportunities for common subexpression elimination across allocation points.

What the branch does:

C-- variables and Mach registers are given types, which are currently one of:

`Float ` a unboxed floating-point number
`Int ` an integer or a pointer outside the heap
`Addr` anything else

The branch splits the `Addr` type into two types, `Val` for well-formed Caml values, `Addr` for derived pointers into the heap. In other words:

* `Val` denotes a valid OCaml value: either a pointer to the beginning of a heap block, an infix pointer if it is preceded by the correct infix header, or a 2n+1 encoded integer.
* `Int` is for integers (not necessarily 2n+1 encoded) and for pointers outside the heap.
* `Addr` denotes pointers that are neither Val nor Int, i.e. pointers into the heap that point in the middle of a heap block. Such derived pointers are produced by e.g. array indexing.
* `Float` is for unboxed floating-point numbers.

Concerning how variables and registers are tracked by the GC:
* Variables of type `Val` are GC roots. If they are pointers, the GC will not deallocate the addressed heap block, and will update the variable if the heap block moves.
* Variables of type `Int` or `Float` are ignored by the GC. The GC does not change their values.
* Variables of type `Addr` must never be live across an allocation point or function call. (Compiler internal error.) They cannot be given as roots to the GC because they don't point after a well-formed block header of the kind that the GC needs. However, the GC may move the block pointed into, invalidating the value of the `Addr` variable.

To infer types more precisely, the branch splits the `Word` quantity (type memory_chunk) into `Word_val` (well-formed OCaml values, type `Val`) and `Word_int` (integer but not heap pointer, type `Int`). Values of type `Addr` are never stored into / loaded from main memory, hence there is no `Word_addr` quantity.

The Cmm language now has no less than three integer addition operators:
* `Caddi` produces an integer or out-of-heap type (type `Int`)
* `Cadda` produces a derived pointer into the heap (type `Addr`)
* `Caddv` produces a pointer into the heap that is a well-formed Caml value (type `Val`)

The `Csuba` operator was unused, so I removed it.

The Cmmgen pass is updated to use Word_int/Word_val and Caddi/Cadda/Caddv appropriately. As a side benefit, some temporary values that point outside the heap (e.g. bigarray payload) and that used to have type Addr now have the more precise type Int, telling the GC it does not have to track them.

The CSE pass is updated to prevent factorization of subexpressions of type `Addr` across allocation points (this breaks the GC, cf. PR#6484), but keep factoring subexpressions of other types across allocation points. This should result in better CSE of e.g. array check bounds.

The Emit pass is updatd with the new cmmtypes and memory_chunks, plus a check that no register of type `Addr` is live across allocation points.