More precise typing at the C-- and Mach level:

- Register type "Addr" is split into . "Val" (well-formed OCaml values, appropriate as GC roots) . "Addr" (derived pointers within the heap, must not survive a GC) - memory_chunk "Word" is split into . "Word_val" (OCaml value) . "Word_int" (native-sized integer, not a pointer into the heap) Cmmgen was updated to use Word_val or Word_int as appropriate. Application #1: fail at compile-time if a derived pointer within the heap survives a GC point (cf. PR#6484). Application #2: CSE can do a better job across allocation points (keep factoring expressions of type Int, Val, Float, but not Addr). git-svn-id: http://caml.inria.fr/svn/ocaml/branches/cmm-mach-types@15568 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
ocaml · Nov 6, 2014 · ac02f56 · ac02f56
1 parent 26ee828
commit ac02f56
Show file tree

Hide file tree

Showing 30 changed files with 273 additions and 190 deletions.
diff --git a/asmcomp/CSEgen.ml b/asmcomp/CSEgen.ml
@@ -153,6 +153,12 @@ let set_unknown_regs n rs =
 let filter_equations pred n =
   { n with num_eqs = Equations.filter (fun (op,_) res -> pred op) n.num_eqs }
 
+(* Forget everything we know about registers of type [Addr]. *)
+
+let kill_addr_regs n =
+  { n with num_reg =
+              Reg.Map.filter (fun r n -> r.Reg.typ <> Cmm.Addr) n.num_reg }
+
 (* Prepend a set of moves before [i] to assign [srcs] to [dsts].  *)
 
 let insert_single_move i src dst = instr_cons (Iop Imove) [|src|] [|dst|] i
@@ -231,7 +237,8 @@ method private cse n i =
          - equations involving memory loads, since the callee can
            perform arbitrary memory stores;
          - equations involving arithmetic operations that can
-           produce bad pointers into the heap (see below for Ialloc);
+           produce [Addr]-typed derived pointers into the heap
+           (see below for Ialloc);
          - mappings from hardware registers to value numbers,
            since the callee does not preserve these registers.
          That doesn't leave much usable information: checkbounds
@@ -241,13 +248,14 @@ method private cse n i =
       {i with next = self#cse empty_numbering i.next}
   | Iop (Ialloc _) ->
       (* For allocations, we must avoid extending the live range of a
-         pseudoregister across the allocation if this pseudoreg can
-         contain a value that looks like a pointer into the heap but
-         is not a pointer to the beginning of a Caml object.  PR#6484
-         is an example of such a value (a derived pointer into a
-         block).  In the absence of more precise typing information,
-         we just forget everything. *)
-       {i with next = self#cse empty_numbering i.next}
+         pseudoregister across the allocation if this pseudoreg
+         is a derived heap pointer (a pointer into the heap that does
+         not point to the beginning of a Caml block).  PR#6484 is an
+         example of this situation.  Such pseudoregs have type [Addr].
+         Pseudoregs with types other than [Addr] can be kept. *)
+       let n1 = kill_addr_regs n in
+       let n2 = set_unknown_regs n1 i.res in
+       {i with next = self#cse n2 i.next}
   | Iop op ->
       begin match self#class_of_operation op with
       | Op_pure | Op_checkbound | Op_load ->

diff --git a/asmcomp/amd64/emit.mlp b/asmcomp/amd64/emit.mlp
@@ -165,10 +165,12 @@ let record_frame_label live dbg =
   let live_offset = ref [] in
   Reg.Set.iter
     (function
-        {typ = Addr; loc = Reg r} ->
+      | {typ = Val; loc = Reg r} ->
           live_offset := ((r lsl 1) + 1) :: !live_offset
-      | {typ = Addr; loc = Stack s} as reg ->
+      | {typ = Val; loc = Stack s} as reg ->
           live_offset := slot_offset s (register_class reg) :: !live_offset
+      | {typ = Addr} as r ->
+          Misc.fatal_error ("bad GC root " ^ Reg.name r)
       | _ -> ())
     live;
   frame_descriptors :=
@@ -430,7 +432,7 @@ let emit_instr fallthrough i =
     | Lop(Iload(chunk, addr)) ->
         let dest = i.res.(0) in
         begin match chunk with
-          | Word ->
+          | Word_int | Word_val ->
               `	movq	{emit_addressing addr i.arg 0}, {emit_reg dest}\n`
           | Byte_unsigned ->
               `	movzbq	{emit_addressing addr i.arg 0}, {emit_reg dest}\n`
@@ -451,7 +453,7 @@ let emit_instr fallthrough i =
         end
     | Lop(Istore(chunk, addr, _)) ->
         begin match chunk with
-          | Word ->
+          | Word_int | Word_val ->
             `	movq	{emit_reg i.arg.(0)}, {emit_addressing addr i.arg 1}\n`
           | Byte_unsigned | Byte_signed ->
             `	movb	{emit_reg8 i.arg.(0)}, {emit_addressing addr i.arg 1}\n`

diff --git a/asmcomp/amd64/emit_nt.mlp b/asmcomp/amd64/emit_nt.mlp
@@ -161,10 +161,12 @@ let record_frame_label live dbg =
   let live_offset = ref [] in
   Reg.Set.iter
     (function
-        {typ = Addr; loc = Reg r} ->
+      | {typ = Val; loc = Reg r} ->
           live_offset := ((r lsl 1) + 1) :: !live_offset
-      | {typ = Addr; loc = Stack s} as reg ->
+      | {typ = Val; loc = Stack s} as reg ->
           live_offset := slot_offset s (register_class reg) :: !live_offset
+      | {typ = Addr} as r ->
+          Misc.fatal_error ("bad GC root " ^ Reg.name r)
       | _ -> ())
     live;
   frame_descriptors :=
@@ -423,7 +425,7 @@ let emit_instr fallthrough i =
     | Lop(Iload(chunk, addr)) ->
         let dest = i.res.(0) in
         begin match chunk with
-          | Word ->
+          | Word_int | Word_val ->
               `	mov	{emit_reg dest}, QWORD PTR {emit_addressing addr i.arg 0}\n`
           | Byte_unsigned ->
               `	movzx	{emit_reg dest}, BYTE PTR {emit_addressing addr i.arg 0}\n`
@@ -445,7 +447,7 @@ let emit_instr fallthrough i =
         end
     | Lop(Istore(chunk, addr, _)) ->
         begin match chunk with
-          | Word ->
+          | Word_int | Word_val ->
             `	mov	QWORD PTR {emit_addressing addr i.arg 1}, {emit_reg i.arg.(0)}\n`
           | Byte_unsigned | Byte_signed ->
             `	mov	BYTE PTR {emit_addressing addr i.arg 1}, {emit_reg8 i.arg.(0)}\n`

diff --git a/asmcomp/amd64/proc.ml b/asmcomp/amd64/proc.ml
@@ -99,8 +99,7 @@ let num_register_classes = 2
 
 let register_class r =
   match r.typ with
-    Int -> 0
-  | Addr -> 0
+  | Val | Int | Addr -> 0
   | Float -> 1
 
 let num_available_registers = [| 13; 16 |]
@@ -155,7 +154,7 @@ let calling_conventions first_int last_int first_float last_float make_stack
   let ofs = ref 0 in
   for i = 0 to Array.length arg - 1 do
     match arg.(i).typ with
-      Int | Addr as ty ->
+    | Val | Int | Addr as ty ->
         if !int <= last_int then begin
           loc.(i) <- phys_reg !int;
           incr int
@@ -215,7 +214,7 @@ let win64_loc_external_arguments arg =
   and ofs = ref 32 in
   for i = 0 to Array.length arg - 1 do
     match arg.(i).typ with
-      Int | Addr as ty ->
+    | Val | Int | Addr as ty ->
         if !reg < 4 then begin
           loc.(i) <- phys_reg win64_int_external_arguments.(!reg);
           incr reg

diff --git a/asmcomp/amd64/selection.ml b/asmcomp/amd64/selection.ml
@@ -30,11 +30,11 @@ let rec select_addr exp =
   match exp with
     Cconst_symbol s when not !Clflags.dlcode ->
       (Asymbol s, 0)
-  | Cop((Caddi | Cadda), [arg; Cconst_int m]) ->
+  | Cop((Caddi | Caddv | Cadda), [arg; Cconst_int m]) ->
       let (a, n) = select_addr arg in (a, n + m)
-  | Cop((Csubi | Csuba), [arg; Cconst_int m]) ->
+  | Cop(Csubi, [arg; Cconst_int m]) ->
       let (a, n) = select_addr arg in (a, n - m)
-  | Cop((Caddi | Cadda), [Cconst_int m; arg]) ->
+  | Cop((Caddi | Caddv | Cadda), [Cconst_int m; arg]) ->
       let (a, n) = select_addr arg in (a, n + m)
   | Cop(Clsl, [arg; Cconst_int(1|2|3 as shift)]) ->
       begin match select_addr arg with
@@ -51,7 +51,7 @@ let rec select_addr exp =
         (Alinear e, n) -> (Ascale(e, mult), n * mult)
       | _ -> (Alinear exp, 0)
       end
-  | Cop((Caddi | Cadda), [arg1; arg2]) ->
+  | Cop((Caddi | Caddv | Cadda), [arg1; arg2]) ->
       begin match (select_addr arg1, select_addr arg2) with
           ((Alinear e1, n1), (Alinear e2, n2)) ->
               (Aadd(e1, e2), n1 + n2)
@@ -170,8 +170,8 @@ method! select_store is_assign addr exp =
 method! select_operation op args =
   match op with
   (* Recognize the LEA instruction *)
-    Caddi | Cadda | Csubi | Csuba ->
-      begin match self#select_addressing Word (Cop(op, args)) with
+    Caddi | Caddv | Cadda | Csubi ->
+      begin match self#select_addressing Word_int (Cop(op, args)) with
         (Iindexed d, _) -> super#select_operation op args
       | (Iindexed2 0, _) -> super#select_operation op args
       | (addr, arg) -> (Ispecific(Ilea addr), [arg])
@@ -196,11 +196,11 @@ method! select_operation op args =
          assert false
      end
   (* Recognize store instructions *)
-  | Cstore Word ->
+  | Cstore (Word_int|Word_val as chunk) ->
       begin match args with
         [loc; Cop(Caddi, [Cop(Cload _, [loc']); Cconst_int n])]
         when loc = loc' && self#is_immediate n ->
-          let (addr, arg) = self#select_addressing Word loc in
+          let (addr, arg) = self#select_addressing chunk loc in
           (Ispecific(Ioffset_loc(n, addr)), [arg])
       | _ ->
           super#select_operation op args

diff --git a/asmcomp/arm/emit.mlp b/asmcomp/arm/emit.mlp
@@ -103,10 +103,12 @@ let record_frame_label live dbg =
   let live_offset = ref [] in
   Reg.Set.iter
     (function
-        {typ = Addr; loc = Reg r} ->
+      | {typ = Val; loc = Reg r} ->
           live_offset := ((r lsl 1) + 1) :: !live_offset
-      | {typ = Addr; loc = Stack s} as reg ->
+      | {typ = Val; loc = Stack s} as reg ->
           live_offset := slot_offset s (register_class reg) :: !live_offset
+      | {typ = Addr} as r ->
+          Misc.fatal_error ("bad GC root " ^ Reg.name r)
       | _ -> ())
     live;
   frame_descriptors :=

diff --git a/asmcomp/arm/selection.ml b/asmcomp/arm/selection.ml
@@ -27,7 +27,7 @@ let is_offset chunk n =
   (* ARM load/store byte/word have -4095 to 4095 *)
   | Byte_unsigned | Byte_signed
   | Thirtytwo_unsigned | Thirtytwo_signed
-  | Word | Single
+  | Word_int | Word_val | Single
     when not !thumb ->
       n >= -4095 && n <= 4095
   (* Thumb-2 load/store have -255 to 4095 *)
@@ -231,12 +231,12 @@ method private select_operation_softfp op args =
        [Cop(Cextcall(func, typ_int, false, Debuginfo.none), args)])
   (* Add coercions around loads and stores of 32-bit floats *)
   | (Cload Single, args) ->
-      (Iextcall("__aeabi_f2d", false), [Cop(Cload Word, args)])
+      (Iextcall("__aeabi_f2d", false), [Cop(Cload Word_int, args)])
   | (Cstore Single, [arg1; arg2]) ->
       let arg2' =
         Cop(Cextcall("__aeabi_d2f", typ_int, false, Debuginfo.none),
             [arg2]) in
-      self#select_operation (Cstore Word) [arg1; arg2']
+      self#select_operation (Cstore Word_int) [arg1; arg2']
   (* Other operations are regular *)
   | (op, args) -> super#select_operation op args
 

diff --git a/asmcomp/arm64/emit.mlp b/asmcomp/arm64/emit.mlp
@@ -123,10 +123,12 @@ let record_frame_label live dbg =
   let live_offset = ref [] in
   Reg.Set.iter
     (function
-        {typ = Addr; loc = Reg r} ->
+      | {typ = Val; loc = Reg r} ->
           live_offset := ((r lsl 1) + 1) :: !live_offset
-      | {typ = Addr; loc = Stack s} as reg ->
+      | {typ = Val; loc = Stack s} as reg ->
           live_offset := slot_offset s (register_class reg) :: !live_offset
+      | {typ = Addr} as r ->
+          Misc.fatal_error ("bad GC root " ^ Reg.name r)
       | _ -> ())
     live;
   frame_descriptors :=
@@ -385,7 +387,7 @@ let emit_instr i =
         | Single ->
             `	ldr	s7, {emit_addressing addr base}\n`;
             `	fcvt	{emit_reg dst}, s7\n`
-        | Word | Double | Double_u ->
+        | Word_int | Word_val | Double | Double_u ->
             `	ldr	{emit_reg dst}, {emit_addressing addr base}\n`
         end
     | Lop(Istore(size, addr, _)) ->
@@ -406,7 +408,7 @@ let emit_instr i =
         | Single ->
             `	fcvt	s7, {emit_reg src}\n`;
             `	str	s7, {emit_addressing addr base}\n`;
-        | Word | Double | Double_u ->
+        | Word_int | Word_val | Double | Double_u ->
             `	str	{emit_reg src}, {emit_addressing addr base}\n`
         end
     | Lop(Ialloc n) ->

diff --git a/asmcomp/arm64/selection.ml b/asmcomp/arm64/selection.ml
@@ -28,7 +28,7 @@ let is_offset chunk n =
         n land 1 = 0 && n lsr 1 < 0x1000
     | Thirtytwo_unsigned | Thirtytwo_signed | Single ->
         n land 3 = 0 && n lsr 2 < 0x1000
-    | Word | Double | Double_u ->
+    | Word_int | Word_val | Double | Double_u ->
         n land 7 = 0 && n lsr 3 < 0x1000)
 
 (* An automaton to recognize ( 0+1+0* | 1+0+1* )

diff --git a/asmcomp/cmm.ml b/asmcomp/cmm.ml
@@ -11,19 +11,21 @@
 (***********************************************************************)
 
 type machtype_component =
-    Addr
+  | Val
+  | Addr
   | Int
   | Float
 
 type machtype = machtype_component array
 
 let typ_void = ([||] : machtype_component array)
+let typ_val = [|Val|]
 let typ_addr = [|Addr|]
 let typ_int = [|Int|]
 let typ_float = [|Float|]
 
 let size_component = function
-    Addr -> Arch.size_addr
+  | Val | Addr -> Arch.size_addr
   | Int -> Arch.size_int
   | Float -> Arch.size_float
 
@@ -59,7 +61,8 @@ type memory_chunk =
   | Sixteen_signed
   | Thirtytwo_unsigned
   | Thirtytwo_signed
-  | Word
+  | Word_int
+  | Word_val
   | Single
   | Double
   | Double_u
@@ -73,7 +76,7 @@ type operation =
   | Caddi | Csubi | Cmuli | Cmulhi | Cdivi | Cmodi
   | Cand | Cor | Cxor | Clsl | Clsr | Casr
   | Ccmpi of comparison
-  | Cadda | Csuba
+  | Caddv | Cadda
   | Ccmpa of comparison
   | Cnegf | Cabsf
   | Caddf | Csubf | Cmulf | Cdivf

diff --git a/asmcomp/cmm.mli b/asmcomp/cmm.mli
@@ -13,13 +13,41 @@
 (* Second intermediate language (machine independent) *)
 
 type machtype_component =
-    Addr
+  | Val
+  | Addr
   | Int
   | Float
 
+(* - [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.
+
+The purpose of these types is twofold.  First, they guide register
+allocation: type [Float] goes in FP registers, the other types go
+into integer registers.  Second, they determine how local variables 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 local variable if the heap block moves.
+   - Variables of type [Int] and [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.  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.
+*)
+
 type machtype = machtype_component array
 
 val typ_void: machtype
+val typ_val: machtype
 val typ_addr: machtype
 val typ_int: machtype
 val typ_float: machtype
@@ -45,10 +73,11 @@ type memory_chunk =
   | Sixteen_signed
   | Thirtytwo_unsigned
   | Thirtytwo_signed
-  | Word
+  | Word_int                           (* integer or pointer outside heap *)
+  | Word_val                           (* pointer inside heap or encoded int *)
   | Single
-  | Double                              (* 64-bit-aligned 64-bit float *)
-  | Double_u                            (* word-aligned 64-bit float *)
+  | Double                             (* 64-bit-aligned 64-bit float *)
+  | Double_u                           (* word-aligned 64-bit float *)
 
 type operation =
     Capply of machtype * Debuginfo.t
@@ -59,7 +88,8 @@ type operation =
   | Caddi | Csubi | Cmuli | Cmulhi | Cdivi | Cmodi
   | Cand | Cor | Cxor | Clsl | Clsr | Casr
   | Ccmpi of comparison
-  | Cadda | Csuba
+  | Caddv (* pointer addition that produces a [Val] (well-formed Caml value) *)
+  | Cadda (* pointer addition that produces a [Addr] (derived heap pointer) *)
   | Ccmpa of comparison
   | Cnegf | Cabsf
   | Caddf | Csubf | Cmulf | Cdivf