Optimize away some physical equality (#850)

Changes

@@ -32,6 +32,9 @@ Working version
   (Marcell Fischbach and Benedikt Meurer, adapted by Nicolas Ojeda
   Bar, review by Nicolas Ojeda Bar and Alain Frisch)
 
+- GPR#850: Optimize away some physical equality
+  (Pierre Chambart, review by Mark Shinwell and Leo White)
+
 - MPR#6927, GPR#988: On macOS, when compiling bytecode stubs, plugins,
   and shared libraries through -output-obj, generate dylibs instead of
   bundles.

middle_end/simplify_primitives.ml

@@ -37,6 +37,47 @@ let phys_equal (approxs:A.t list) =
     | Some (s1, Some f1), Some (s2, Some f2) -> Symbol.equal s1 s2 && f1 = f2
     | _ -> false
 
+let is_known_to_be_some_kind_of_int (arg:A.descr) =
+  match arg with
+  | Value_int _ | Value_char _ | Value_constptr _ -> true
+  | Value_block (_, _) | Value_float _ | Value_set_of_closures _
+  | Value_closure _ | Value_string _ | Value_float_array _
+  | A.Value_boxed_int _ | Value_unknown _ | Value_extern _
+  | Value_symbol _ | Value_unresolved _ | Value_bottom -> false
+
+let is_known_to_be_some_kind_of_block (arg:A.descr) =
+  match arg with
+  | Value_block _ | Value_float _ | Value_float_array _ | A.Value_boxed_int _
+  | Value_closure _ | Value_string _ -> true
+  | Value_set_of_closures _ | Value_int _ | Value_char _ | Value_constptr _
+  | Value_unknown _ | Value_extern _ | Value_symbol _
+  | Value_unresolved _ | Value_bottom -> false
+
+let rec structurally_different (arg1:A.t) (arg2:A.t) =
+  match arg1.descr, arg2.descr with
+  | (Value_int n1 | Value_constptr n1), (Value_int n2 | Value_constptr n2)
+    when n1 <> n2 ->
+    true
+  | Value_block (tag1, fields1), Value_block (tag2, fields2) ->
+    not (Tag.equal tag1 tag2)
+    || (Array.length fields1 <> Array.length fields2)
+    || Misc.Stdlib.Array.exists2 structurally_different fields1 fields2
+  | descr1, descr2 ->
+    (* This is not very precise as this won't allow to distinguish
+       blocks from strings for instance. This can be improved if it
+       is deemed valuable. *)
+    (is_known_to_be_some_kind_of_int descr1
+     && is_known_to_be_some_kind_of_block descr2)
+    || (is_known_to_be_some_kind_of_block descr1
+        && is_known_to_be_some_kind_of_int descr2)
+
+let phys_different (approxs:A.t list) =
+  match approxs with
+  | [] | [_] | _ :: _ :: _ :: _ ->
+    Misc.fatal_error "wrong number of arguments for equality"
+  | [a1; a2] ->
+    structurally_different a1 a2
+
 let primitive (p : Lambda.primitive) (args, approxs) expr dbg ~size_int
       ~big_endian : Flambda.named * A.t * Inlining_cost.Benefit.t =
   let fpc = !Clflags.float_const_prop in
@@ -97,6 +138,12 @@ let primitive (p : Lambda.primitive) (args, approxs) expr dbg ~size_int
        inlined later, [a] and [b] could be shared and thus [c] and [d] could
        be too.  As such, any intermediate non-aliasing judgement would be
        invalid. *)
+  | Pintcomp Ceq when phys_different approxs ->
+    S.const_bool_expr expr false
+  | Pintcomp Cneq when phys_different approxs ->
+    S.const_bool_expr expr true
+    (* If two values are structurally different we are certain they can never
+       be shared*)
   | _ ->
     match A.descrs approxs with
     | [Value_int x] ->

testsuite/tests/asmcomp/is_static_flambda.ml

@@ -113,3 +113,88 @@ let f x =
 let () =
   f true;
   f false
+
+(* Verify that physical equality/inequality is correctly propagated *)
+
+(* In these tests, tuple can be statically allocated only if it is a
+   known constant since the function is never inlined (hence this
+   code is never at toplevel) *)
+
+let () =
+  let f () =
+    let v = (1, 2) in
+    (* eq is supposed to be considered always true since v is a
+       constant, hence aliased to a symbol.
+       It is not yet optimized away if it is not constant *)
+    let eq = v == v in
+    let n = if eq then 1 else 2 in
+    let tuple = (n,n) in
+    assert(is_in_static_data tuple)
+  in
+  (f [@inlined never]) ()
+
+let () =
+  let f () =
+    let v = (1, 2) in
+    (* same with inequality *)
+    let eq = v != v in
+    let n = if eq then 1 else 2 in
+    let tuple = (n,n) in
+    assert(is_in_static_data tuple)
+  in
+  (f [@inlined never]) ()
+
+let () =
+  let f x =
+    let v1 = Some x in
+    let v2 = None in
+    let eq = v1 == v2 in
+    (* The values are structurally different, so must be physically
+       different *)
+    let n = if eq then 1 else 2 in
+    let tuple = (n,n) in
+    assert(is_in_static_data tuple)
+  in
+  (f [@inlined never]) ()
+
+let () =
+  let f x =
+    let v1 = Some x in
+    let v2 = None in
+    let eq = v1 != v2 in
+    (* same with inequality *)
+    let n = if eq then 1 else 2 in
+    let tuple = (n,n) in
+    assert(is_in_static_data tuple)
+  in
+  (f [@inlined never]) ()
+
+let () =
+  let f x =
+    let v1 = (1, 2) in
+    let v2 = (3, 2) in
+    let eq = v1 == v2 in
+    (* difference is deeper *)
+    let n = if eq then 1 else 2 in
+    let tuple = (n,n) in
+    assert(is_in_static_data tuple)
+  in
+  (f [@inlined never]) ()
+
+module Int = struct
+  type t = int
+  let compare (a:int) b = compare a b
+end
+module IntMap = (Map.Make [@inlined])(Int)
+
+let () =
+  let f () =
+    let a = IntMap.empty in
+    let b = (IntMap.add [@inlined]) 1 (Some 1) a in
+    assert(is_in_static_data b);
+    let c = (IntMap.add [@inlined]) 1 (Some 2) b in
+    assert(is_in_static_data c);
+    let d = (IntMap.add [@inlined]) 1 (Some 2) c in
+    assert(is_in_static_data d);
+  in
+  (f [@inlined never]) ()

utils/misc.ml

@@ -163,6 +163,17 @@ module Stdlib = struct
       | None -> default
       | Some a -> f a
   end
+
+  module Array = struct
+    let exists2 p a1 a2 =
+      let n = Array.length a1 in
+      if Array.length a2 <> n then invalid_arg "Misc.Stdlib.Array.exists2";
+      let rec loop i =
+        if i = n then false
+        else if p (Array.unsafe_get a1 i) (Array.unsafe_get a2 i) then true
+        else loop (succ i) in
+      loop 0
+  end
 end
 
 let may = Stdlib.Option.iter

utils/misc.mli

@@ -90,6 +90,13 @@ module Stdlib : sig
     val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
     val value_default : ('a -> 'b) -> default:'b -> 'a t -> 'b
   end
+
+  module Array : sig
+    val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
+    (* Same as [Array.exists], but for a two-argument predicate. Raise
+       Invalid_argument if the two arrays are determined to have
+       different lengths. *)
+  end
 end
 
 val find_in_path: string list -> string -> string