Ensure that register typing constraints are respected at join points

6 files changed, 98 insertions, 4 deletions

diff --git a/Changes b/Changes
index fbf9f92e75..ec6267f860 100644
--- a/Changes
+++ b/Changes
@@ -1006,6 +1006,11 @@ Features wishes:
   GNU parallel tool to run tests in parallel.
   (Gabriel Scherer)
 
+- GPR#555: ensure that register typing constraints are respected at
+  join points in the control flow graph
+  (Mark Shinwell, debugging & test case by Arseniy Alekseyev and Leo White,
+    code review by Xavier Leroy)
+
 Build system:
 =============
 
diff --git a/asmcomp/cmm.ml b/asmcomp/cmm.ml
index efb8adec42..9243cb47af 100644
--- a/asmcomp/cmm.ml
+++ b/asmcomp/cmm.ml
@@ -32,6 +32,56 @@ let size_component = function
   | Int -> Arch.size_int
   | Float -> Arch.size_float
 
+(** [machtype_component]s are partially ordered as follows:
+
+      Addr     Float
+       ^
+       |
+      Val
+       ^
+       |
+      Int
+
+  In particular, [Addr] must be above [Val], to ensure that if there is
+  a join point between a code path yielding [Addr] and one yielding [Val]
+  then the result is treated as a derived pointer into the heap (i.e. [Addr]).
+  (Such a result may not be live across any call site or a fatal compiler
+  error will result.)
+*)
+
+let lub_component comp1 comp2 =
+  match comp1, comp2 with
+  | Int, Int -> Int
+  | Int, Val -> Val
+  | Int, Addr -> Addr
+  | Val, Int -> Val
+  | Val, Val -> Val
+  | Val, Addr -> Addr
+  | Addr, Int -> Addr
+  | Addr, Addr -> Addr
+  | Addr, Val -> Addr
+  | Float, Float -> Float
+  | (Int | Addr | Val), Float
+  | Float, (Int | Addr | Val) ->
+    (* Float unboxing code must be sure to avoid this case. *)
+    assert false
+
+let ge_component comp1 comp2 =
+  match comp1, comp2 with
+  | Int, Int -> true
+  | Int, Addr -> false
+  | Int, Val -> false
+  | Val, Int -> true
+  | Val, Val -> true
+  | Val, Addr -> false
+  | Addr, Int -> true
+  | Addr, Addr -> true
+  | Addr, Val -> true
+  | Float, Float -> true
+  | (Int | Addr | Val), Float
+  | Float, (Int | Addr | Val) ->
+    assert false
+
 let size_machtype mty =
   let size = ref 0 in
   for i = 0 to Array.length mty - 1 do
diff --git a/asmcomp/cmm.mli b/asmcomp/cmm.mli
index aa6601d33e..31c222cf63 100644
--- a/asmcomp/cmm.mli
+++ b/asmcomp/cmm.mli
@@ -56,6 +56,20 @@ val typ_int: machtype
 val typ_float: machtype
 
 val size_component: machtype_component -> int
+
+(** Least upper bound of two [machtype_component]s. *)
+val lub_component
+   : machtype_component
+  -> machtype_component
+  -> machtype_component
+
+(** Returns [true] iff the first supplied [machtype_component] is greater than
+    or equal to the second under the relation used by [lub_component]. *)
+val ge_component
+   : machtype_component
+  -> machtype_component
+  -> bool
+
 val size_machtype: machtype -> int
 
 type comparison =
diff --git a/asmcomp/selectgen.ml b/asmcomp/selectgen.ml
index ce672a6bf2..257327a749 100644
--- a/asmcomp/selectgen.ml
+++ b/asmcomp/selectgen.ml
@@ -117,14 +117,19 @@ let join opt_r1 seq1 opt_r2 seq2 =
       assert (l1 = Array.length r2);
       let r = Array.make l1 Reg.dummy in
       for i = 0 to l1-1 do
-        if Reg.anonymous r1.(i) then begin
+        if Reg.anonymous r1.(i)
+          && Cmm.ge_component r1.(i).typ r2.(i).typ
+        then begin
           r.(i) <- r1.(i);
           seq2#insert_move r2.(i) r1.(i)
-        end else if Reg.anonymous r2.(i) then begin
+        end else if Reg.anonymous r2.(i)
+          && Cmm.ge_component r2.(i).typ r1.(i).typ
+        then begin
           r.(i) <- r2.(i);
           seq1#insert_move r1.(i) r2.(i)
         end else begin
-          r.(i) <- Reg.create r1.(i).typ;
+          let typ = Cmm.lub_component r1.(i).typ r2.(i).typ in
+          r.(i) <- Reg.create typ;
           seq1#insert_move r1.(i) r.(i);
           seq2#insert_move r2.(i) r.(i)
         end
diff --git a/testsuite/tests/asmcomp/Makefile b/testsuite/tests/asmcomp/Makefile
index 3e6e024af3..60da8213d4 100644
--- a/testsuite/tests/asmcomp/Makefile
+++ b/testsuite/tests/asmcomp/Makefile
@@ -47,7 +47,7 @@ parsecmm.mli parsecmm.ml: parsecmm.mly
 lexcmm.ml: lexcmm.mll
 	@$(OCAMLLEX) -q lexcmm.mll
 
-MLCASES=optargs staticalloc bind_tuples is_static
+MLCASES=optargs staticalloc bind_tuples is_static register_typing
 ARGS_is_static=-I $(OTOPDIR)/byterun is_in_static_data.c
 MLCASES_FLAMBDA=is_static_flambda
 ARGS_is_static_flambda=-I $(OTOPDIR)/byterun is_in_static_data.c
diff --git a/testsuite/tests/asmcomp/register_typing.ml b/testsuite/tests/asmcomp/register_typing.ml
new file mode 100644
index 0000000000..9d55d29ba0
--- /dev/null
+++ b/testsuite/tests/asmcomp/register_typing.ml
@@ -0,0 +1,20 @@
+type 'a typ = Int : int typ | Ptr : int list typ
+
+let f (type a) (t : a typ) (p : int list) : a =
+  match t with
+  | Int -> 100
+  | Ptr -> p
+
+let allocate_garbage () =
+  for i = 0 to 100 do
+    ignore (Array.make 200 0.0)
+  done
+
+let g (t : int list typ) x =
+  Gc.minor ();
+  let x = f t ([x; x; x; x; x]) in
+  Gc.minor ();
+  allocate_garbage ();
+  ignore (String.length (String.concat " " (List.map string_of_int x)))
+
+let () = g Ptr 5