Fix bug in unboxing decision code + use max unboxing depth cli flag

middle_end/flambda/tests/meet_test.ml

@@ -143,15 +143,69 @@ let meet_variants_don't_lose_aliases () =
         T.print tag_meet_ty
         TEE.print tag_meet_env_extension
 
+let test_meet_two_blocks () =
+  let define env v =
+    let v' = Var_in_binding_pos.create v Name_mode.normal in
+    TE.add_definition env (Name_in_binding_pos.var v') K.value
+  in
+  let defines env l = List.fold_left define env l in
+  let env = TE.create ~resolver ~get_imported_names in
+  let block1 = Variable.create "block1" in
+  let field1 = Variable.create "field1" in
+  let block2 = Variable.create "block2" in
+  let field2 = Variable.create "field2" in
+  let env = defines env [block1; block2; field1; field2] in
+
+  let env =
+    TE.add_equation env (Name.var block1)
+      (T.immutable_block ~is_unique:false Tag.zero ~field_kind:K.value
+        ~fields:[T.alias_type_of K.value (Simple.var field1)])
+  in
+  let env =
+    TE.add_equation env (Name.var block2)
+      (T.immutable_block ~is_unique:false Tag.zero ~field_kind:K.value
+        ~fields:[T.alias_type_of K.value (Simple.var field2)])
+  in
+  (* let test b1 b2 env =
+   *   let eq_block2 = T.alias_type_of K.value (Simple.var b2) in
+   *   let env =
+   *     TE.add_equation env (Name.var b1) eq_block2
+   *   in
+   *   Format.eprintf "Res:@ %a@.@."
+   *     TE.print env
+   * in
+   * test block1 block2 env;
+   * test block2 block1 env; *)
+
+  let f b1 b2 =
+    match
+    T.meet env
+      (T.alias_type_of K.value (Simple.var b1))
+      (T.alias_type_of K.value (Simple.var b2))
+    with
+    | Bottom -> assert false
+    | Ok (t, tee) ->
+        Format.eprintf "Res:@ %a@.%a@."
+          T.print t
+          TEE.print tee;
+        let env = TE.add_env_extension env tee in
+        Format.eprintf "Env:@.%a@.@."
+          TE.print env
+  in
+  f block1 block2;
+  f block2 block1
+
 let () =
   let comp_unit =
     Compilation_unit.create (Ident.create_persistent "Meet_test")
       (Linkage_name.create "meet_test")
   in
   Compilation_unit.set_current comp_unit;
-  Format.eprintf "MEET CHAINS WITH TWO VARS\n\n%!";
+  Format.eprintf "MEET CHAINS WITH TWO VARS@\n@.";
   test_meet_chains_two_vars ();
-  Format.eprintf "\nMEET CHAINS WITH THREE VARS\n\n%!";
+  Format.eprintf "@.MEET CHAINS WITH THREE VARS@\n@.";
   test_meet_chains_three_vars ();
-  Format.eprintf "@.MEET VARIANT@.@.";
-  meet_variants_don't_lose_aliases ()
+  Format.eprintf "@.MEET VARIANT@\n@.";
+  meet_variants_don't_lose_aliases ();
+  Format.eprintf "@.MEET TWO BLOCKS@\n@.";
+  test_meet_two_blocks ()

middle_end/flambda/types/env/typing_env.rec.ml

@@ -43,16 +43,16 @@ module Cached : sig
     -> Type_grammar.t
     -> Binding_time.t
     -> Name_mode.t
-    -> new_aliases:Aliases.t
     -> t
 
   val replace_variable_binding
      : t
     -> Variable.t
     -> Type_grammar.t
-    -> new_aliases:Aliases.t
     -> t
 
+  val with_aliases : t -> aliases:Aliases.t -> t
+
   val add_symbol_projection : t -> Variable.t -> Symbol_projection.t -> t
 
   val find_symbol_projection : t -> Variable.t -> Symbol_projection.t option
@@ -131,27 +131,30 @@ end = struct
      (used to be add-or-replace), the [names_to_types] map addition was a
      major source of allocation. *)
 
-  let add_or_replace_binding t (name : Name.t) ty binding_time name_mode ~new_aliases =
+  let add_or_replace_binding t (name : Name.t) ty binding_time name_mode =
     let names_to_types =
       Name.Map.add name (ty, binding_time, name_mode) t.names_to_types
     in
     { names_to_types;
-      aliases = new_aliases;
+      aliases = t.aliases;
       symbol_projections = t.symbol_projections;
     }
 
-  let replace_variable_binding t var ty ~new_aliases =
+  let replace_variable_binding t var ty =
     let names_to_types =
       Name.Map.replace (Name.var var)
         (function (_old_ty, binding_time, name_mode) ->
           ty, binding_time, name_mode)
         t.names_to_types
     in
     { names_to_types;
-      aliases = new_aliases;
+      aliases = t.aliases;
       symbol_projections = t.symbol_projections;
     }
 
+  let with_aliases t ~aliases =
+    { t with aliases; }
+
   let add_symbol_projection t var proj =
     let symbol_projections = Variable.Map.add var proj t.symbol_projections in
     { t with symbol_projections; }
@@ -260,6 +263,12 @@ module One_level = struct
   let level t = t.level
   let just_after_level t = t.just_after_level
 
+  let with_aliases t ~aliases =
+    let just_after_level =
+      Cached.with_aliases t.just_after_level ~aliases
+    in
+    { t with just_after_level; }
+
   let is_empty t = Typing_env_level.is_empty t.level
 
 (*
@@ -781,6 +790,12 @@ let with_current_level_and_next_binding_time t ~current_level
   invariant t;
   t
 
+let with_aliases t ~aliases =
+  let current_level =
+    One_level.with_aliases t.current_level ~aliases
+  in
+  with_current_level t ~current_level
+
 let cached t = One_level.just_after_level t.current_level
 
 let add_variable_definition t var kind name_mode =
@@ -810,7 +825,6 @@ let add_variable_definition t var kind name_mode =
     Cached.add_or_replace_binding (cached t)
       name (Type_grammar.unknown kind)
       t.next_binding_time name_mode
-      ~new_aliases:(aliases t)
   in
   let current_level =
     One_level.create (current_scope t) level ~just_after_level
@@ -866,8 +880,33 @@ let add_definition t (name : Name_in_binding_pos.t) kind =
       end;
       add_symbol_definition t sym)
 
-let invariant_for_new_equation t name ty =
+let invariant_for_alias (t:t) name ty =
+  (* Check that no canonical element gets an [Equals] type *)
+  if !Clflags.flambda_invariant_checks || true then begin
+    match Type_grammar.get_alias_exn ty with
+    | exception Not_found -> ()
+    | alias ->
+      assert (not (Simple.equal alias (Simple.name name)));
+      let canonical =
+        Aliases.get_canonical_ignoring_name_mode (aliases t) name
+      in
+      if Simple.equal canonical (Simple.name name) then
+        Misc.fatal_errorf
+          "There is about to be an [Equals] equation on canonical name %a@\nequation: %a@\n@."
+          Name.print name Type_grammar.print ty
+     end
+
+(* This is too costly to check, but it can be useful for debugging problems with
+   canonical aliases.
+let invariant_for_aliases (t:t) =
+  Name.Map.iter (fun name (ty, _, _) ->
+      invariant_for_alias t name ty
+   ) (names_to_types t)
+*)
+
+let invariant_for_new_equation (t:t) name ty =
   if !Clflags.flambda_invariant_checks then begin
+    invariant_for_alias t name ty;
     (* CR mshinwell: This should check that precision is not decreasing. *)
     let defined_names =
       Name_occurrences.create_names
@@ -888,7 +927,7 @@ let invariant_for_new_equation t name ty =
     end
   end
 
-let rec add_equation0 t aliases name ty =
+let rec add_equation0 (t:t) name ty =
   if !Clflags.Flambda.Debug.concrete_types_only_on_canonicals then begin
     let is_concrete =
       match Type_grammar.get_alias_exn ty with
@@ -897,7 +936,7 @@ let rec add_equation0 t aliases name ty =
     in
     if is_concrete then begin
       let canonical =
-        Aliases.get_canonical_ignoring_name_mode aliases name
+        Aliases.get_canonical_ignoring_name_mode (aliases t) name
         |> Simple.without_coercion
       in
       if not (Simple.equal canonical (Simple.name name)) then begin
@@ -923,27 +962,27 @@ let rec add_equation0 t aliases name ty =
           then
             Cached.replace_variable_binding
               (One_level.just_after_level t.current_level)
-              var ty ~new_aliases:aliases
+              var ty
           else
             Cached.add_or_replace_binding
               (One_level.just_after_level t.current_level)
               name ty Binding_time.imported_variables Name_mode.in_types
-              ~new_aliases:aliases
         in
         just_after_level)
       ~symbol:(fun _ ->
         let just_after_level =
           Cached.add_or_replace_binding
             (One_level.just_after_level t.current_level)
             name ty Binding_time.symbols Name_mode.normal
-            ~new_aliases:aliases
         in
         just_after_level)
   in
   let current_level =
     One_level.create (current_scope t) level ~just_after_level
   in
-  with_current_level t ~current_level
+  let res = with_current_level t ~current_level in
+  (* invariant_for_aliases res; *)
+  res
 
 and add_equation t name ty =
   if !Clflags.flambda_invariant_checks then begin
@@ -989,15 +1028,15 @@ and add_equation t name ty =
           end)
         ~const:(fun _ -> ())
   end;
-  let aliases, simple, t, ty =
+  let simple, t, ty =
     let aliases = aliases t in
     match Type_grammar.get_alias_exn ty with
     | exception Not_found ->
       (* Equations giving concrete types may only be added to the canonical
          element as known by the alias tracker (the actual canonical, ignoring
          any name modes). *)
       let canonical = Aliases.get_canonical_ignoring_name_mode aliases name in
-      aliases, canonical, t, ty
+      canonical, t, ty
     | alias_of ->
       let alias_of = Simple.without_coercion alias_of in
       (* Forget where [name] and [alias_of] came from---our job is now to
@@ -1016,19 +1055,20 @@ and add_equation t name ty =
       in
       let ({ canonical_element; alias_of_demoted_element; t = aliases; }
             : Aliases.add_result) =
-        Aliases.add 
+        Aliases.add
           aliases
           ~element1:alias
           ~binding_time_and_mode1:binding_time_and_mode_alias
           ~element2:alias_of
           ~binding_time_and_mode2:binding_time_and_mode_alias_of
       in
+      let t = with_aliases t ~aliases in
       (* We need to change the demoted alias's type to point to the new
          canonical element. *)
       let ty =
         Type_grammar.alias_type_of kind canonical_element
       in
-      aliases, alias_of_demoted_element, t, ty
+      alias_of_demoted_element, t, ty
   in
   (* Beware: if we're about to add the equation on a name which is different
      from the one that the caller passed in, then we need to make sure that the
@@ -1071,7 +1111,7 @@ and add_equation t name ty =
   in
   let [@inline always] name name ~coercion:_ =
     (* [bare_lhs] has no coercion by its definition *)
-    add_equation0 t aliases name ty
+    add_equation0 t name ty
   in
   Simple.pattern_match bare_lhs ~name ~const:(fun _ -> t)
 

middle_end/flambda/unboxing/optimistic_unboxing_decision.ml

@@ -24,8 +24,7 @@ module Extra_param_and_args = U.Extra_param_and_args
 let pp_tag print_tag ppf tag =
   if print_tag then Format.fprintf ppf "_%d" (Tag.to_int tag)
 
-(* CR gbury: make this a Clflag *)
-let max_unboxing_depth = 1
+(* Internal control knobs *)
 let unbox_numbers = true
 let unbox_blocks = true
 let unbox_variants = true
@@ -66,7 +65,8 @@ let rec make_optimistic_decision ~depth tenv ~param_type : U.decision =
   | Some decision ->
     if unbox_numbers then decision else Do_not_unbox Incomplete_parameter_type
   | None ->
-    if depth >= max_unboxing_depth then Do_not_unbox Max_depth_exceeded
+    if depth >= !Clflags.Flambda.Expert.max_unboxing_depth then
+      Do_not_unbox Max_depth_exceeded
     else match T.prove_unique_tag_and_size tenv param_type with
       | Proved (tag, size) when unbox_blocks ->
         let fields =
@@ -140,6 +140,12 @@ and make_optimistic_fields
     | Ok (_, env_extension) -> env_extension
     | Bottom ->
       Misc.fatal_errorf "Meet failed whereas prove previously succeeded"
+    | exception (Misc.Fatal_error as exn) ->
+      Format.eprintf "Context is meet of type: %a@\nwith shape: %a@\nin env: @\n%a@."
+        T.print param_type
+        T.print shape
+        TE.print tenv;
+      raise exn
   in
   let tenv = TE.add_env_extension tenv env_extension in
   let fields =