diff --git a/.depend b/.depend index 110398476e33..59d786f09b12 100644 --- a/.depend +++ b/.depend @@ -9177,6 +9177,7 @@ middle_end/flambda/types/flambda_type.cmo : \ middle_end/flambda/naming/name_in_binding_pos.cmi \ middle_end/flambda/basic/name.cmi \ utils/misc.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/basic/kinded_parameter.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ utils/identifiable.cmi \ @@ -9232,6 +9233,7 @@ middle_end/flambda/types/flambda_type.cmx : \ middle_end/flambda/naming/name_in_binding_pos.cmx \ middle_end/flambda/basic/name.cmx \ utils/misc.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/basic/kinded_parameter.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ utils/identifiable.cmx \ @@ -9277,6 +9279,7 @@ middle_end/flambda/types/flambda_type.cmi : \ middle_end/flambda/naming/name_mode.cmi \ middle_end/flambda/naming/name_in_binding_pos.cmi \ middle_end/flambda/basic/name.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/basic/kinded_parameter.cmi \ middle_end/flambda/basic/invariant_env.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ @@ -9315,6 +9318,7 @@ middle_end/flambda/types/type_descr.rec.cmo : \ middle_end/flambda/naming/name_occurrences.cmi \ middle_end/flambda/naming/name_mode.cmi \ utils/misc.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/flambda_colours.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ @@ -9334,6 +9338,7 @@ middle_end/flambda/types/type_descr.rec.cmx : \ middle_end/flambda/naming/name_occurrences.cmx \ middle_end/flambda/naming/name_mode.cmx \ utils/misc.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/flambda_colours.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ @@ -9350,6 +9355,7 @@ middle_end/flambda/types/type_descr_intf.cmo : \ middle_end/flambda/types/basic/or_unknown.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/basic/name.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/types/kinds/flambda_kind.cmi \ middle_end/flambda/naming/contains_names.cmo \ middle_end/flambda/cmx/contains_ids.cmo \ @@ -9361,6 +9367,7 @@ middle_end/flambda/types/type_descr_intf.cmx : \ middle_end/flambda/types/basic/or_unknown.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/basic/name.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/types/kinds/flambda_kind.cmx \ middle_end/flambda/naming/contains_names.cmx \ middle_end/flambda/cmx/contains_ids.cmx \ @@ -9428,6 +9435,7 @@ middle_end/flambda/types/type_grammar.rec.cmi : \ middle_end/flambda/types/basic/or_bottom.cmi \ utils/numbers.cmi \ middle_end/flambda/basic/name.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/types/kinds/flambda_kind.cmi \ lambda/debuginfo.cmi \ middle_end/flambda/naming/contains_names.cmo \ @@ -9439,6 +9447,7 @@ middle_end/flambda/types/type_head_intf.cmo : \ utils/printing_cache.cmi \ middle_end/flambda/types/basic/or_unknown.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/naming/contains_names.cmo \ middle_end/flambda/cmx/contains_ids.cmo \ middle_end/flambda/compilenv_deps/coercion.cmi @@ -9446,6 +9455,7 @@ middle_end/flambda/types/type_head_intf.cmx : \ utils/printing_cache.cmx \ middle_end/flambda/types/basic/or_unknown.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/naming/contains_names.cmx \ middle_end/flambda/cmx/contains_ids.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx @@ -9506,6 +9516,11 @@ middle_end/flambda/types/basic/meet_or_join_op.cmo : \ middle_end/flambda/types/basic/meet_or_join_op.cmx : \ middle_end/flambda/types/basic/meet_or_join_op.cmi middle_end/flambda/types/basic/meet_or_join_op.cmi : +middle_end/flambda/types/basic/meet_result.cmo : \ + middle_end/flambda/types/basic/meet_result.cmi +middle_end/flambda/types/basic/meet_result.cmx : \ + middle_end/flambda/types/basic/meet_result.cmi +middle_end/flambda/types/basic/meet_result.cmi : middle_end/flambda/types/basic/or_bottom.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi middle_end/flambda/types/basic/or_bottom.cmx : \ @@ -9690,6 +9705,7 @@ middle_end/flambda/types/env/typing_env.rec.cmo : \ middle_end/flambda/naming/name_in_binding_pos.cmi \ middle_end/flambda/basic/name.cmi \ utils/misc.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/basic/kinded_parameter.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/types/kinds/flambda_kind.cmi \ @@ -9715,6 +9731,7 @@ middle_end/flambda/types/env/typing_env.rec.cmx : \ middle_end/flambda/naming/name_in_binding_pos.cmx \ middle_end/flambda/basic/name.cmx \ utils/misc.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/basic/kinded_parameter.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/types/kinds/flambda_kind.cmx \ @@ -9865,6 +9882,7 @@ middle_end/flambda/types/structures/closures_entry.rec.cmo : \ utils/printing_cache.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/basic/closure_id.cmi \ middle_end/flambda/types/structures/closures_entry.rec.cmi @@ -9872,6 +9890,7 @@ middle_end/flambda/types/structures/closures_entry.rec.cmx : \ utils/printing_cache.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/basic/closure_id.cmx \ middle_end/flambda/types/structures/closures_entry.rec.cmi @@ -9912,6 +9931,7 @@ middle_end/flambda/types/structures/function_declaration_type.rec.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ middle_end/flambda/naming/name_mode.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ lambda/debuginfo.cmi \ middle_end/flambda/basic/code_id.cmi \ @@ -9924,6 +9944,7 @@ middle_end/flambda/types/structures/function_declaration_type.rec.cmx : \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ middle_end/flambda/naming/name_mode.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ lambda/debuginfo.cmx \ middle_end/flambda/basic/code_id.cmx \ @@ -9946,6 +9967,7 @@ middle_end/flambda/types/structures/product.rec.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ utils/misc.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/types/kinds/flambda_kind.cmi \ middle_end/flambda/basic/closure_id.cmi \ @@ -9959,6 +9981,7 @@ middle_end/flambda/types/structures/product.rec.cmx : \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ utils/misc.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/types/kinds/flambda_kind.cmx \ middle_end/flambda/basic/closure_id.cmx \ @@ -10001,6 +10024,7 @@ middle_end/flambda/types/structures/row_like.rec.cmo : \ utils/numbers.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ utils/misc.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ utils/identifiable.cmi \ middle_end/flambda/types/kinds/flambda_kind.cmi \ @@ -10024,6 +10048,7 @@ middle_end/flambda/types/structures/row_like.rec.cmx : \ utils/numbers.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ utils/misc.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ utils/identifiable.cmx \ middle_end/flambda/types/kinds/flambda_kind.cmx \ @@ -10072,12 +10097,12 @@ middle_end/flambda/types/structures/set_of_closures_contents.cmi : \ middle_end/flambda/basic/closure_id.cmi middle_end/flambda/types/structures/type_structure_intf.cmo : \ utils/printing_cache.cmi \ - middle_end/flambda/types/basic/or_bottom.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/naming/contains_names.cmo \ middle_end/flambda/cmx/contains_ids.cmo middle_end/flambda/types/structures/type_structure_intf.cmx : \ utils/printing_cache.cmx \ - middle_end/flambda/types/basic/or_bottom.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/naming/contains_names.cmx \ middle_end/flambda/cmx/contains_ids.cmx middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.cmo : \ @@ -10085,6 +10110,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi \ utils/numbers.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.cmi @@ -10093,6 +10119,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.cmx : \ middle_end/flambda/types/basic/or_bottom.cmx \ utils/numbers.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.cmi @@ -10106,6 +10133,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.cmo : \ middle_end/flambda/types/basic/or_unknown.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.cmi @@ -10116,6 +10144,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.cmx : \ middle_end/flambda/types/basic/or_unknown.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.cmi @@ -10127,6 +10156,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi \ utils/numbers.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.cmi @@ -10135,6 +10165,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.cmx : \ middle_end/flambda/types/basic/or_bottom.cmx \ utils/numbers.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.cmi @@ -10145,6 +10176,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.cmo : \ middle_end/flambda/types/basic/or_bottom.cmi \ utils/numbers.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.cmi @@ -10153,6 +10185,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.cmx : \ middle_end/flambda/types/basic/or_bottom.cmx \ utils/numbers.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.cmi @@ -10163,6 +10196,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.cmo : \ middle_end/flambda/types/basic/or_unknown.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.cmi @@ -10171,6 +10205,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.cmx : \ middle_end/flambda/types/basic/or_unknown.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.cmi @@ -10198,6 +10233,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.cmo : \ middle_end/flambda/types/basic/or_unknown.cmi \ middle_end/flambda/types/basic/or_bottom.cmi \ middle_end/flambda/naming/name_occurrences.cmi \ + middle_end/flambda/types/basic/meet_result.cmi \ middle_end/flambda/cmx/ids_for_export.cmi \ middle_end/flambda/compilenv_deps/coercion.cmi \ middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.cmi @@ -10207,6 +10243,7 @@ middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.cmx : \ middle_end/flambda/types/basic/or_unknown.cmx \ middle_end/flambda/types/basic/or_bottom.cmx \ middle_end/flambda/naming/name_occurrences.cmx \ + middle_end/flambda/types/basic/meet_result.cmx \ middle_end/flambda/cmx/ids_for_export.cmx \ middle_end/flambda/compilenv_deps/coercion.cmx \ middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.cmi diff --git a/compilerlibs/Makefile.compilerlibs b/compilerlibs/Makefile.compilerlibs index 04abdc3bf830..5a0642c48242 100644 --- a/compilerlibs/Makefile.compilerlibs +++ b/compilerlibs/Makefile.compilerlibs @@ -263,6 +263,7 @@ MIDDLE_END_FLAMBDA_TYPES=\ middle_end/flambda/types/env/aliases.cmo \ middle_end/flambda/types/basic/meet_or_join_op.cmo \ middle_end/flambda/types/basic/or_bottom.cmo \ + middle_end/flambda/types/basic/meet_result.cmo \ middle_end/flambda/types/basic/string_info.cmo \ middle_end/flambda/types/basic/or_unknown_or_bottom.cmo \ middle_end/flambda/types/structures/code_age_relation.cmo \ diff --git a/flambdatest/api_tests/Makefile b/flambdatest/api_tests/Makefile index 6ed76e47a696..5feed3f112bc 100644 --- a/flambdatest/api_tests/Makefile +++ b/flambdatest/api_tests/Makefile @@ -60,7 +60,7 @@ CAMLDEP=$(CAMLRUN) $(ROOTDIR)/boot/ocamlc -depend DEPFLAGS=-slash DEPINCLUDES=$(INCLUDES) -SOURCES=extension_meet.ml import_test.ml +SOURCES=extension_meet.ml import_test.ml join_tests.ml COMPILERLIBS=\ $(ROOTDIR)/compilerlibs/ocamlcommon.cma \ diff --git a/flambdatest/api_tests/join_tests.ml b/flambdatest/api_tests/join_tests.ml new file mode 100644 index 000000000000..994edb4b9d13 --- /dev/null +++ b/flambdatest/api_tests/join_tests.ml @@ -0,0 +1,89 @@ +(* + Continuation k has three parameters, three uses. + Variable x is defined after the fork but in all paths + Use types: + (=x, =x) { x : {0, 1} } + ({0, 1, 2}, {0, 1, 2}) { x : {0, 1, 2} } +*) + +module T = Flambda_type +module TE = Flambda_type.Typing_env + +let test_join () = + let env_at_fork = + TE.create + ~resolver:(fun _ -> None) + ~get_imported_names:(fun () -> Name.Set.empty) + in + let param_a = Variable.create "a" in + let param_b = Variable.create "b" in + let param_c = Variable.create "c" in + let n_a = Name.var param_a in + let n_b = Name.var param_b in + let n_c = Name.var param_c in + let kind_ni = Flambda_kind.With_subkind.naked_immediate in + let kp_a = Kinded_parameter.create param_a kind_ni in + let kp_b = Kinded_parameter.create param_b kind_ni in + let kp_c = Kinded_parameter.create param_c kind_ni in + let params = [kp_c; kp_b; kp_a] in + let env_at_fork = TE.add_definitions_of_params env_at_fork ~params in + let var_x = Variable.create "x" in + let n_x = Name.var var_x in + let nb_x = Name_in_binding_pos.create n_x Name_mode.normal in + let env = TE.add_definition env_at_fork nb_x Flambda_kind.naked_immediate in + let alias name = T.alias_type_of Flambda_kind.naked_immediate (Simple.name name) in + let imms_left = + T.these_naked_immediates Target_imm.all_bools + in + let imms_right = + T.these_naked_immediates Target_imm.zero_one_and_minus_one + in + let env_left = TE.add_equation env n_a imms_left in + let env_left = TE.add_equation env_left n_b (alias n_x) in + let env_left = TE.add_equation env_left n_c (alias n_x) in + let env_left = + TE.add_equation env_left n_x imms_left + in + let env_right = + TE.add_equation env n_a (alias n_x) + in + let env_right = + TE.add_equation env_right n_b imms_right + in + let env_right = + TE.add_equation env_right n_c (alias n_x) + in + let env_right = + TE.add_equation env_right n_x imms_right + in + let join_env = + TE.cut_and_n_way_join + env_at_fork + [env_left, Obj.magic 0, Obj.magic 0; + env_right, Obj.magic 0, Obj.magic 0] + ~params + ~unknown_if_defined_at_or_later_than:Scope.initial + ~extra_lifted_consts_in_use_envs:Symbol.Set.empty + ~extra_allowed_names:Name_occurrences.empty + in + Format.eprintf + "Environments:@.\ + Env at fork:@ %a@.\ + Left env:@ %a@.\ + Right env:@ %a@.@.\ + Join env:@ %a@.@." + TE.print env_at_fork + TE.print env_left + TE.print env_right + TE.print join_env; + () + +let _ = + let comp_unit = + let id = Ident.create_persistent "Test" in + let linkage_name = Linkage_name.create "camlTest" in + Compilation_unit.create id linkage_name + in + Compilation_unit.set_current comp_unit; + test_join () + diff --git a/flambdatest/mlexamples/alias_bug.ml b/flambdatest/mlexamples/alias_bug.ml new file mode 100644 index 000000000000..aca142e0a71e --- /dev/null +++ b/flambdatest/mlexamples/alias_bug.ml @@ -0,0 +1,22 @@ + +type float_kind_conv = + | Float_f (* %f | %+f | % f *) + | Float_e (* %e | %+e | % e *) + | Float_E (* %E | %+E | % E *) + | Float_g (* %g | %+g | % g *) + | Float_G (* %G | %+G | % G *) + | Float_F (* %F | %+F | % F *) + | Float_h (* %h | %+h | % h *) + | Float_H (* %H | %+H | % H *) + | Float_CF (* %#F| %+#F| % #F *) + +let char_of_fconv ?(cF='F') fconv = match snd fconv with + | Float_f -> 'f' | Float_e -> 'e' + | Float_E -> 'E' | Float_g -> 'g' + | Float_G -> 'G' | Float_F -> cF + | Float_h -> 'h' | Float_H -> 'H' + | Float_CF -> 'F' + +let f x = char_of_fconv x + +(* let g x = char_of_fconv ~cF:'g' x *) diff --git a/middle_end/flambda/lifting/reification.ml b/middle_end/flambda/lifting/reification.ml index 53717f7f389b..af7fa1ad1907 100644 --- a/middle_end/flambda/lifting/reification.ml +++ b/middle_end/flambda/lifting/reification.ml @@ -117,8 +117,7 @@ let try_to_reify dacc (term : Simplified_named.t) ~bound_to ~allow_lifting = match term with | Invalid _ -> let ty = T.bottom_like ty in - let denv = DE.add_equation_on_variable denv bound_to ty in - Simplified_named.invalid (), DA.with_denv dacc denv, ty + Simplified_named.invalid (), dacc, ty | Reachable _ -> let typing_env = DE.typing_env denv in let reify_result = diff --git a/middle_end/flambda/tests/meet_test.ml b/middle_end/flambda/tests/meet_test.ml index 560dce2c4e55..91ae0c883424 100644 --- a/middle_end/flambda/tests/meet_test.ml +++ b/middle_end/flambda/tests/meet_test.ml @@ -39,9 +39,13 @@ let test_meet_chains_two_vars () = T.print new_type_for_var2; match T.meet env first_type_for_var2 new_type_for_var2 with | Bottom -> assert false - | Ok (meet_ty, env_extension) -> + | Ok (meet_result, env_extension) -> Format.eprintf "Env extension:@ %a\n%!" TEE.print env_extension; let env = TE.add_env_extension env env_extension in + let meet_ty = + Meet_result.extract_value meet_result + first_type_for_var2 new_type_for_var2 + in let env = TE.add_equation env (Name.var var2) meet_ty in Format.eprintf "Final situation:@ %a\n%!" TE.print env @@ -85,7 +89,11 @@ let test_meet_chains_three_vars () = T.print new_type_for_var3; match T.meet env first_type_for_var3 new_type_for_var3 with | Bottom -> assert false - | Ok (meet_ty, env_extension) -> + | Ok (meet_result, env_extension) -> + let meet_ty = + Meet_result.extract_value meet_result + first_type_for_var3 new_type_for_var3 + in Format.eprintf "Env extension:@ %a\n%!" TEE.print env_extension; let env = TE.add_env_extension env env_extension in let env = TE.add_equation env (Name.var var3) meet_ty in @@ -125,7 +133,10 @@ let meet_variants_don't_lose_aliases () = T.variant ~const_ctors ~non_const_ctors in match T.meet env ty1 ty2 with | Bottom -> assert false - | Ok (meet_ty, env_extension) -> + | Ok (meet_result, env_extension) -> + let meet_ty = + Meet_result.extract_value meet_result ty1 ty2 + in Format.eprintf "@[Meet:@ %a@ /\\@ %a =>@ %a +@ %a@]@." T.print ty1 T.print ty2 T.print meet_ty TEE.print env_extension; @@ -135,7 +146,11 @@ let meet_variants_don't_lose_aliases () = let t_tag_1 = T.this_naked_immediate Target_imm.one in match T.meet env t_get_tag t_tag_1 with | Bottom -> assert false - | Ok (tag_meet_ty, tag_meet_env_extension) -> + | Ok (tag_meet_result, tag_meet_env_extension) -> + let tag_meet_ty = + Meet_result.extract_value tag_meet_result + t_get_tag t_tag_1 + in Format.eprintf "t_get_tag: %a@.t_tag: %a@." T.print t_get_tag T.print t_tag_1; @@ -178,13 +193,12 @@ let test_meet_two_blocks () = * 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 + let ty1 = T.alias_type_of K.value (Simple.var b1) in + let ty2 = T.alias_type_of K.value (Simple.var b2) in + match T.meet env ty1 ty2 with | Bottom -> assert false - | Ok (t, tee) -> + | Ok (result, tee) -> + let t = Meet_result.extract_value result ty1 ty2 in Format.eprintf "Res:@ %a@.%a@." T.print t TEE.print tee; diff --git a/middle_end/flambda/types/basic/meet_result.ml b/middle_end/flambda/types/basic/meet_result.ml new file mode 100644 index 000000000000..e136e2d20935 --- /dev/null +++ b/middle_end/flambda/types/basic/meet_result.ml @@ -0,0 +1,50 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Vincent Laviron, OCamlPro *) +(* *) +(* Copyright 2021 OCamlPro SAS *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +[@@@ocaml.warning "+a-4-30-40-41-42"] + +type 'a return_value = + | Left_input + | Right_input + | Both_inputs + | New_result of 'a + +type ('a, 'ext) t = + | Bottom + | Ok of 'a return_value * 'ext + +let map_result ~f = function + | Bottom -> Bottom + | Ok (Left_input, ext) -> Ok (Left_input, ext) + | Ok (Right_input, ext) -> Ok (Right_input, ext) + | Ok (Both_inputs, ext) -> Ok (Both_inputs, ext) + | Ok (New_result x, ext) -> Ok (New_result (f x), ext) + +let extract_value res left right = + match res with + | Left_input -> left + | Right_input -> right + | Both_inputs -> left + | New_result value -> value + +let set_meet (type a) ~no_extension (module S : Set.S with type t = a) + (s1 : a) (s2 : a) = + match S.subset s1 s2, S.subset s2 s1 with + | true, true -> Ok (Both_inputs, no_extension) + | true, false -> Ok (Left_input, no_extension) + | false, true -> Ok (Right_input, no_extension) + | false, false -> + let s = S.inter s1 s2 in + if S.is_empty s then Bottom + else Ok (New_result s, no_extension) diff --git a/middle_end/flambda/types/basic/meet_result.mli b/middle_end/flambda/types/basic/meet_result.mli new file mode 100644 index 000000000000..16254d78d8fd --- /dev/null +++ b/middle_end/flambda/types/basic/meet_result.mli @@ -0,0 +1,48 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Vincent Laviron, OCamlPro *) +(* *) +(* Copyright 2021 OCamlPro SAS *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +(* Type for the result of meet operations *) + +[@@@ocaml.warning "+a-4-30-40-41-42"] + +type 'a return_value = + | Left_input + | Right_input + | Both_inputs + | New_result of 'a + +type ('a, 'ext) t = + | Bottom + | Ok of 'a return_value * 'ext + +val map_result + : f:('a -> 'b) + -> ('a, 'ext) t + -> ('b, 'ext) t + +(** Given a result and the inputs used to generate it, + returns the corresponding value. + In the Both_inputs case, the left input is returned. *) +val extract_value + : 'a return_value + -> 'a + -> 'a + -> 'a + +val set_meet + : no_extension:'ext + -> (module Set.S with type t = 'a) + -> 'a + -> 'a + -> ('a, 'ext) t diff --git a/middle_end/flambda/types/env/typing_env.rec.ml b/middle_end/flambda/types/env/typing_env.rec.ml index bdd88026d03a..ef3d48c1f94b 100644 --- a/middle_end/flambda/types/env/typing_env.rec.ml +++ b/middle_end/flambda/types/env/typing_env.rec.ml @@ -771,8 +771,17 @@ let mem ?min_name_mode t name = ~symbol:(fun sym -> (* CR mshinwell: This might not take account of symbols in missing .cmx files *) - Symbol.Set.mem sym t.defined_symbols - || Name.Set.mem name (t.get_imported_names ())) + let comp_unit = Symbol.compilation_unit sym in + if Compilation_unit.equal comp_unit (Compilation_unit.get_current_exn ()) + then + Symbol.Set.mem sym t.defined_symbols + else + match (resolver t) comp_unit with + | None -> + (* The cmx is unavailable, but the symbol is valid *) + true + | Some _ -> + Name.Set.mem name (t.get_imported_names ())) let mem_simple ?min_name_mode t simple = Simple.pattern_match simple @@ -934,18 +943,22 @@ let rec add_equation0 (t:t) name ty = | exception Not_found -> true | _ -> false in - if is_concrete then begin - let canonical = - Aliases.get_canonical_ignoring_name_mode (aliases t) name - |> Simple.without_coercion - in - if not (Simple.equal canonical (Simple.name name)) then begin - Misc.fatal_errorf "Trying to add equation giving concrete type on %a \ - which is not canonical (its canonical is %a): %a" - Name.print name - Simple.print canonical - Type_grammar.print ty - end + let canonical = + Aliases.get_canonical_ignoring_name_mode (aliases t) name + |> Simple.without_coercion + in + if is_concrete && not (Simple.equal canonical (Simple.name name)) then begin + Misc.fatal_errorf "Trying to add equation giving concrete type on %a \ + which is not canonical (its canonical is %a): %a" + Name.print name + Simple.print canonical + Type_grammar.print ty + end; + if not is_concrete && Simple.equal canonical (Simple.name name) then begin + Misc.fatal_errorf "Trying to add equation giving alias type on %a \ + which is canonical: %a" + Name.print name + Type_grammar.print ty end end; invariant_for_new_equation t name ty; @@ -1097,14 +1110,14 @@ and add_equation t name ty = let ty, t = let [@inline always] name eqn_name ~coercion = assert (Coercion.is_id coercion); (* true by definition *) - if Name.equal name eqn_name then ty, t - else - let env = Meet_env.create t in - let existing_ty = find t eqn_name (Some (Type_grammar.kind ty)) in - match Type_grammar.meet env ty existing_ty with - | Bottom -> Type_grammar.bottom_like ty, t - | Ok (meet_ty, env_extension) -> - meet_ty, add_env_extension t env_extension + let env = Meet_env.create t in + let existing_ty = find t eqn_name (Some (Type_grammar.kind ty)) in + match Type_grammar.meet env ty existing_ty with + | Bottom -> + Type_grammar.bottom_like ty, t + | Ok (meet_result, env_extension) -> + let meet_ty = Meet_result.extract_value meet_result ty existing_ty in + meet_ty, add_env_extension t env_extension in Simple.pattern_match bare_lhs ~name ~const:(fun _ -> ty, t) in @@ -1194,8 +1207,24 @@ let meet_equations_on_params t ~params ~param_types = let existing_type = find t name (Some kind) in let env = Meet_env.create t in match Type_grammar.meet env existing_type param_type with - | Bottom -> add_equation t name (Type_grammar.bottom kind) - | Ok (meet_ty, env_extension) -> + | Bottom -> + (* Ideally we should adapt the type of this function so + that the caller can handle this case. + In practice, this would likely mean treating the + corresponding continuation handler as unreachable. *) + (* Misc.fatal_errorf + * "Bottom equation added on parameter:@.\ + * Parameter:@ %a@.\ + * Parameter type:@ %a@.\ + * Typing env:@ %a" + * Kinded_parameter.print param + * Type_grammar.print param_type + * print t *) + add_equation t name (Type_grammar.bottom kind) + | Ok (meet_result, env_extension) -> + let meet_ty = + Meet_result.extract_value meet_result existing_type param_type + in let t = add_equation t name meet_ty in add_env_extension t env_extension) t diff --git a/middle_end/flambda/types/env/typing_env_extension.rec.ml b/middle_end/flambda/types/env/typing_env_extension.rec.ml index e9c6c0d42483..bfdb646659aa 100644 --- a/middle_end/flambda/types/env/typing_env_extension.rec.ml +++ b/middle_end/flambda/types/env/typing_env_extension.rec.ml @@ -115,9 +115,18 @@ let rec meet0 env (t1 : t) (t2 : t) extra_extensions = | Some ty0 -> begin match Type_grammar.meet env ty0 ty with | Bottom -> raise Bottom_meet - | Ok (ty, new_ext) -> - Type_grammar.check_equation name ty; - Name.Map.add (*replace*) name ty eqs, new_ext :: extra_extensions + | Ok (res, new_ext) -> + let extra_extensions = new_ext :: extra_extensions in + begin match res with + | Left_input | Both_inputs -> + (* The equation is already there *) + eqs, extra_extensions + | Right_input -> + Name.Map.add (*replace*) name ty eqs, extra_extensions + | New_result ty -> + Type_grammar.check_equation name ty; + Name.Map.add (*replace*) name ty eqs, extra_extensions + end end) t2.equations (t1.equations, extra_extensions) diff --git a/middle_end/flambda/types/env/typing_env_extension.rec.mli b/middle_end/flambda/types/env/typing_env_extension.rec.mli index ff684d3d0440..a7ad8b297249 100644 --- a/middle_end/flambda/types/env/typing_env_extension.rec.mli +++ b/middle_end/flambda/types/env/typing_env_extension.rec.mli @@ -45,6 +45,8 @@ val from_map : Type_grammar.t Name.Map.t -> t val add_or_replace_equation : t -> Name.t -> Type_grammar.t -> t +(* Note: this doesn't use Meet_result.t, as the meet function here is used + to merge extensions together. *) val meet : Meet_env.t -> t -> t -> t Or_bottom.t val join : Join_env.t -> t -> t -> t diff --git a/middle_end/flambda/types/flambda_type.mli b/middle_end/flambda/types/flambda_type.mli index 6bcf1808041a..79c08e0db62e 100644 --- a/middle_end/flambda/types/flambda_type.mli +++ b/middle_end/flambda/types/flambda_type.mli @@ -215,7 +215,7 @@ module Typing_env : sig end end -val meet : Typing_env.t -> t -> t -> (t * Typing_env_extension.t) Or_bottom.t +val meet : Typing_env.t -> t -> t -> (t, Typing_env_extension.t) Meet_result.t val meet_shape : Typing_env.t diff --git a/middle_end/flambda/types/structures/closures_entry.rec.ml b/middle_end/flambda/types/structures/closures_entry.rec.ml index 709c43772c59..3f43e5c04aad 100644 --- a/middle_end/flambda/types/structures/closures_entry.rec.ml +++ b/middle_end/flambda/types/structures/closures_entry.rec.ml @@ -61,8 +61,10 @@ let meet env { function_decls = function_decls2; closure_types = closure_types2; closure_var_types = closure_var_types2; - } : _ Or_bottom.t = + } : _ Meet_result.t = let any_bottom = ref false in + let all_left = ref true in + let all_right = ref true in let env_extensions = ref (TEE.empty ()) in let function_decls = Closure_id.Map.merge (fun _closure_id func_decl1 func_decl2 -> @@ -74,36 +76,87 @@ let meet env | Bottom -> any_bottom := true; None - | Ok (func_decl, env_extension) -> + | Ok (meet_result, env_extension) -> begin match TEE.meet env !env_extensions env_extension with | Bottom -> any_bottom := true; | Ok env_extension -> env_extensions := env_extension end; - Some func_decl) + begin match meet_result with + | Left_input -> + all_right := false; + Some func_decl1 + | Right_input -> + all_left := false; + Some func_decl2 + | Both_inputs -> + Some func_decl1 + | New_result func_decl -> + all_left := false; + all_right := false; + Some func_decl + end) function_decls1 function_decls2 in if !any_bottom then Bottom else - Or_bottom.bind - (PC.meet env closure_types1 closure_types2) - ~f:(fun (closure_types, env_extension1) -> - Or_bottom.bind - (PV.meet env closure_var_types1 closure_var_types2) - ~f:(fun (closure_var_types, env_extension2) -> + let closure_types_meet = + PC.meet env closure_types1 closure_types2 + in + let closure_var_types_meet = + PV.meet env closure_var_types1 closure_var_types2 + in + match closure_types_meet, closure_var_types_meet with + | Bottom, _ | _, Bottom -> Bottom + | Ok (closure_types_res, env_extension1), + Ok (closure_var_types_res, env_extension2) -> + match TEE.meet env !env_extensions env_extension1 with + | Bottom -> Bottom + | Ok env_extension -> + match TEE.meet env env_extension env_extension2 with + | Bottom -> Bottom + | Ok env_extension -> + begin match closure_types_res, + closure_var_types_res, + !all_left, + !all_right with + | Both_inputs, Both_inputs, true, true -> + Ok (Both_inputs, env_extension) + | (Left_input | Both_inputs), + (Left_input | Both_inputs), + true, _ -> + Ok (Left_input, env_extension) + | (Right_input | Both_inputs), + (Right_input | Both_inputs), + _, true -> + Ok (Right_input, env_extension) + | New_result _, _, _, _ + | _, New_result _, _, _ + | _, _, false, false + | Left_input, Right_input, _, _ + | Left_input, _, false, _ + | Right_input, Left_input, _, _ + | Right_input, _, _, false + | _, Left_input, false, _ + | _, Right_input, _, false -> + let closure_types = + Meet_result.extract_value closure_types_res + closure_types1 closure_types2 + in + let closure_var_types = + Meet_result.extract_value closure_var_types_res + closure_var_types1 closure_var_types2 + in let closures_entry = { function_decls; closure_types; closure_var_types; } in - Or_bottom.bind (TEE.meet env !env_extensions env_extension1) - ~f:(fun env_extension -> - Or_bottom.bind (TEE.meet env env_extension env_extension2) - ~f:(fun env_extension -> - Ok (closures_entry, env_extension))))) + Ok (New_result closures_entry, env_extension) + end let join env { function_decls = function_decls1; diff --git a/middle_end/flambda/types/structures/function_declaration_type.rec.ml b/middle_end/flambda/types/structures/function_declaration_type.rec.ml index b2d791ac3137..d6db84a598f4 100644 --- a/middle_end/flambda/types/structures/function_declaration_type.rec.ml +++ b/middle_end/flambda/types/structures/function_declaration_type.rec.ml @@ -137,12 +137,13 @@ let apply_renaming (t : t) renaming : t = Ok (Non_inlinable (Non_inlinable.apply_renaming non_inlinable renaming)) let meet (env : Meet_env.t) (t1 : t) (t2 : t) - : (t * TEE.t) Or_bottom.t = + : (t, TEE.t) Meet_result.t = match t1, t2 with (* CR mshinwell: Try to factor out "Or_unknown_or_bottom" handling from here and elsewhere *) - | Bottom, _ | _, Bottom -> Ok (Bottom, TEE.empty ()) - | Unknown, t | t, Unknown -> Ok (t, TEE.empty ()) + | Bottom, Bottom -> Ok (Both_inputs, TEE.empty ()) + | Bottom, _ | _, Unknown -> Ok (Left_input, TEE.empty ()) + | _, Bottom | Unknown, _ -> Ok (Right_input, TEE.empty ()) | Ok (Non_inlinable { code_id = code_id1; is_tupled = is_tupled1; }), Ok (Non_inlinable { @@ -151,13 +152,18 @@ let meet (env : Meet_env.t) (t1 : t) (t2 : t) let typing_env = Meet_env.env env in let target_code_age_rel = TE.code_age_relation typing_env in let resolver = TE.code_age_relation_resolver typing_env in - let check_other_things_and_return code_id : (t * TEE.t) Or_bottom.t = + let check_other_things_and_return code_id : (t, TEE.t) Meet_result.t = assert (Bool.equal is_tupled1 is_tupled2); - Ok (Ok (Non_inlinable { + let meet_result : t Meet_result.return_value = + if Code_id.equal code_id1 code_id2 then Both_inputs + else if Code_id.equal code_id code_id1 then Left_input + else if Code_id.equal code_id code_id2 then Right_input + else New_result (Ok (Non_inlinable { code_id; is_tupled = is_tupled1; - }), - TEE.empty ()) + })) + in + Ok (meet_result, TEE.empty ()) in begin match Code_age_relation.meet target_code_age_rel ~resolver code_id1 code_id2 @@ -165,14 +171,12 @@ let meet (env : Meet_env.t) (t1 : t) (t2 : t) | Ok code_id -> check_other_things_and_return code_id | Bottom -> Bottom end - | Ok (Non_inlinable _), Ok (Inlinable _) | Ok (Inlinable _), Ok (Non_inlinable _) -> - (* CR mshinwell: This should presumably return [Non_inlinable] if - the arities match. *) - (* CR vlaviron: The above comment was from before meet and join were split. - Now that we know we're in meet, we can actually keep either of them - (the inlinable one seems better) *) - Ok (Unknown, TEE.empty ()) + (* We want a guarantee that we're always more precise, + so we can't return Unknown anymore *) + Ok (Left_input, TEE.empty ()) + | Ok (Non_inlinable _), Ok (Inlinable _) -> + Ok (Right_input, TEE.empty ()) | Ok (Inlinable { code_id = code_id1; dbg = dbg1; @@ -190,18 +194,23 @@ let meet (env : Meet_env.t) (t1 : t) (t2 : t) let typing_env = Meet_env.env env in let target_code_age_rel = TE.code_age_relation typing_env in let resolver = TE.code_age_relation_resolver typing_env in - let check_other_things_and_return code_id : (t * TEE.t) Or_bottom.t = + let check_other_things_and_return code_id : (t, TEE.t) Meet_result.t = assert (Int.equal (Debuginfo.compare dbg1 dbg2) 0); assert (Bool.equal is_tupled1 is_tupled2); assert (Bool.equal must_be_inlined1 must_be_inlined2); - Ok (Ok (Inlinable { + let meet_result : t Meet_result.return_value = + if Code_id.equal code_id1 code_id2 then Both_inputs + else if Code_id.equal code_id code_id1 then Left_input + else if Code_id.equal code_id code_id2 then Right_input + else New_result (Ok (Inlinable { code_id; dbg = dbg1; rec_info = Rec_info.unknown; is_tupled = is_tupled1; must_be_inlined = must_be_inlined1; - }), - TEE.empty ()) + })) + in + Ok (meet_result, TEE.empty ()) in begin match Code_age_relation.meet target_code_age_rel ~resolver code_id1 code_id2 diff --git a/middle_end/flambda/types/structures/product.rec.ml b/middle_end/flambda/types/structures/product.rec.ml index 09a89c2e6bb2..07988dee52b5 100644 --- a/middle_end/flambda/types/structures/product.rec.ml +++ b/middle_end/flambda/types/structures/product.rec.ml @@ -62,33 +62,63 @@ module Make (Index : Product_intf.Index) = struct let meet env { components_by_index = components_by_index1; kind = kind1; } { components_by_index = components_by_index2; kind = kind2; } - : _ Or_bottom.t = + : _ Meet_result.t = if not (Flambda_kind.equal kind1 kind2) then begin Misc.fatal_errorf "Product.meet between mismatching kinds %a and %a@." Flambda_kind.print kind1 Flambda_kind.print kind2 end; let any_bottom = ref false in + let all_left = ref true in + let all_right = ref true in let env_extension = ref (TEE.empty ()) in let components_by_index = - Index.Map.union (fun _index ty1 ty2 -> - match Type_grammar.meet env ty1 ty2 with - | Ok (ty, env_extension') -> - begin match TEE.meet env !env_extension env_extension' with + Index.Map.merge (fun _index ty1_opt ty2_opt -> + match ty1_opt, ty2_opt with + | None, None -> assert false + | Some ty1, None -> + all_right := false; + Some ty1 + | None, Some ty2 -> + all_left := false; + Some ty2 + | Some ty1, Some ty2 -> + begin match Type_grammar.meet env ty1 ty2 with + | Ok (meet_result, env_extension') -> + begin match TEE.meet env !env_extension env_extension' with + | Bottom -> + any_bottom := true; + Some (Type_grammar.bottom_like ty1) + | Ok extension -> + env_extension := extension; + begin match meet_result with + | Left_input -> + all_right := false; + Some ty1 + | Right_input -> + all_left := false; + Some ty2 + | Both_inputs -> + Some ty1 + | New_result ty -> + all_left := false; + all_right := false; + Some ty + end + end | Bottom -> any_bottom := true; Some (Type_grammar.bottom_like ty1) - | Ok extension -> - env_extension := extension; - Some ty - end - | Bottom -> - any_bottom := true; - Some (Type_grammar.bottom_like ty1)) + end) components_by_index1 components_by_index2 in if !any_bottom then Bottom - else Ok ({ components_by_index; kind = kind1; }, !env_extension) + else match !all_left, !all_right with + | true, true -> Ok (Both_inputs, !env_extension) + | true, false -> Ok (Left_input, !env_extension) + | false, true -> Ok (Right_input, !env_extension) + | false, false -> + Ok (New_result { components_by_index; kind = kind1; }, !env_extension) let join env { components_by_index = components_by_index1; kind = kind1; } @@ -204,7 +234,7 @@ module Int_indexed = struct if Array.length t.fields <= index then Unknown else Known t.fields.(index) - let meet env t1 t2 : _ Or_bottom.t = + let meet env t1 t2 : _ Meet_result.t = if not (Flambda_kind.equal t1.kind t2.kind) then begin Misc.fatal_errorf "Product.Int_indexed.meet between mismatching \ kinds %a and %a@." @@ -213,6 +243,8 @@ module Int_indexed = struct let fields1 = t1.fields in let fields2 = t2.fields in let any_bottom = ref false in + let all_left = ref true in + let all_right = ref true in let env_extension = ref (TEE.empty ()) in let length = max (Array.length fields1) (Array.length fields2) in let fields = @@ -225,17 +257,35 @@ module Int_indexed = struct in match get_opt fields1, get_opt fields2 with | None, None -> assert false - | Some t, None | None, Some t -> t + | Some t, None -> + all_right := false; + t + | None, Some t -> + all_left := false; + t | Some ty1, Some ty2 -> begin match Type_grammar.meet env ty1 ty2 with - | Ok (ty, env_extension') -> + | Ok (meet_result, env_extension') -> begin match TEE.meet env !env_extension env_extension' with | Bottom -> any_bottom := true; Type_grammar.bottom_like ty1 | Ok extension -> env_extension := extension; - ty + begin match meet_result with + | Left_input -> + all_right := false; + ty1 + | Right_input -> + all_left := false; + ty2 + | Both_inputs -> + ty1 + | New_result ty -> + all_left := false; + all_right := false; + ty + end end | Bottom -> any_bottom := true; @@ -243,7 +293,12 @@ module Int_indexed = struct end) in if !any_bottom then Bottom - else Ok ({ fields; kind = t1.kind; }, !env_extension) + else match !all_left, !all_right with + | true, true -> Ok (Both_inputs, !env_extension) + | true, false -> Ok (Left_input, !env_extension) + | false, true -> Ok (Right_input, !env_extension) + | false, false -> + Ok (New_result { fields; kind = t1.kind; }, !env_extension) let join env t1 t2 = if not (Flambda_kind.equal t1.kind t2.kind) then begin diff --git a/middle_end/flambda/types/structures/row_like.rec.ml b/middle_end/flambda/types/structures/row_like.rec.ml index 676e1e3149dd..fb67d540096d 100644 --- a/middle_end/flambda/types/structures/row_like.rec.ml +++ b/middle_end/flambda/types/structures/row_like.rec.ml @@ -147,7 +147,7 @@ struct * * other_tags = Bottom; * * } *\) *) - let meet (meet_env : Meet_env.t) t1 t2 : (t * Typing_env_extension.t) Or_bottom.t = + let meet (meet_env : Meet_env.t) t1 t2 : _ Meet_result.t = let ({ known_tags = known1; other_tags = other1; } : t) = t1 in let ({ known_tags = known2; other_tags = other2; } : t) = t2 in let env_extension = ref None in @@ -175,6 +175,8 @@ struct let join_env = Join_env.create env ~left_env:env ~right_env:env in + let result_is_t1 = ref true in + let result_is_t2 = ref true in let join_env_extension ext = match !env_extension with | None -> env_extension := Some ext @@ -182,39 +184,80 @@ struct assert need_join; env_extension := Some (TEE.join join_env ext2 ext) in - let meet_index i1 i2 : index Or_bottom.t = + let meet_index i1 i2 : (index, unit) Meet_result.t = match i1, i2 with | Known i1', Known i2' -> if Index.equal i1' i2' then - Ok i1 + Ok (Both_inputs, ()) else Bottom - | Known known, At_least at_least - | At_least at_least, Known known -> - if Index.subset at_least known then + | Known known, At_least at_least -> (* [at_least] is included in [known] hence [Known known] is included in [At_least at_least], hence [Known known] \inter [At_least at_least] = [Known known] *) - Ok (Known known) + if Index.subset at_least known then + Ok (Left_input, ()) + else + Bottom + | At_least at_least, Known known -> + if Index.subset at_least known then + Ok (Right_input, ()) else Bottom | At_least i1', At_least i2' -> - Ok (At_least (Index.union i1' i2')) + if Index.equal i1' i2' then + Ok (Both_inputs, ()) + else + let index = Index.union i1' i2' in + if Index.equal i1' index then + Ok (Left_input, ()) + else if Index.equal i2' index then + Ok (Right_input, ()) + else + Ok (New_result (At_least index), ()) + in + let bottom_case () = + result_is_t1 := false; + result_is_t2 := false; + None in let meet_case case1 case2 = match meet_index case1.index case2.index with - | Bottom -> None - | Ok index -> + | Bottom -> bottom_case () + | Ok (index_result, ()) -> match Maps_to.meet meet_env case1.maps_to case2.maps_to with - | Bottom -> None - | Ok (maps_to, env_extension') -> + | Bottom -> bottom_case () + | Ok (maps_to_result, env_extension') -> match TEE.meet meet_env case1.env_extension case2.env_extension with - | Bottom -> None + | Bottom -> bottom_case () | Ok env_extension'' -> match TEE.meet meet_env env_extension' env_extension'' with - | Bottom -> None + | Bottom -> bottom_case () | Ok env_extension -> join_env_extension env_extension; + begin match index_result with + | Both_inputs -> () + | Left_input -> result_is_t2 := false + | Right_input -> result_is_t1 := false + | New_result _ -> + result_is_t1 := false; + result_is_t2 := false + end; + begin match maps_to_result with + | Both_inputs -> () + | Left_input -> result_is_t2 := false + | Right_input -> result_is_t1 := false + | New_result _ -> + result_is_t1 := false; + result_is_t2 := false + end; + let index = + Meet_result.extract_value index_result case1.index case2.index + in + let maps_to = + Meet_result.extract_value maps_to_result + case1.maps_to case2.maps_to + in let env_extension = if need_join then env_extension else TEE.empty () @@ -226,13 +269,17 @@ struct | None, None -> None | Some case1, None -> begin match other2 with - | Bottom -> None + | Bottom -> + result_is_t1 := false; + None | Ok other_case -> meet_case case1 other_case end | None, Some case2 -> begin match other1 with - | Bottom -> None + | Bottom -> + result_is_t2 := false; + None | Ok other_case -> meet_case other_case case2 end @@ -245,7 +292,13 @@ struct in let other_tags : case Or_bottom.t = match other1, other2 with - | Bottom, _ | _, Bottom -> Bottom + | Bottom, Bottom -> Bottom + | Bottom, Ok _ -> + result_is_t2 := false; + Bottom + | Ok _, Bottom -> + result_is_t1 := false; + Bottom | Ok other1, Ok other2 -> match meet_case other1 other2 with | None -> Bottom @@ -260,7 +313,11 @@ struct | None -> assert false (* This should be bottom *) | Some ext -> ext in - Ok (result, env_extension) + match !result_is_t1, !result_is_t2 with + | true, true -> Ok (Both_inputs, env_extension) + | true, false -> Ok (Left_input, env_extension) + | false, true -> Ok (Right_input, env_extension) + | false, false -> Ok (New_result result, env_extension) let join (env : Join_env.t) t1 t2 = let ({ known_tags = known1; other_tags = other1; } : t) = t1 in @@ -476,6 +533,9 @@ struct end + (* This module represents non-empty sets of integers closed under the + predecessor relation. + They can be efficiently represented by their upper bound. *) module Targetint_ocaml_index = struct include Targetint.OCaml let subset t1 t2 = Stdlib.(<=) (compare t1 t2) 0 diff --git a/middle_end/flambda/types/structures/type_structure_intf.ml b/middle_end/flambda/types/structures/type_structure_intf.ml index 27ea160171e2..48517afb5b48 100644 --- a/middle_end/flambda/types/structures/type_structure_intf.ml +++ b/middle_end/flambda/types/structures/type_structure_intf.ml @@ -31,7 +31,7 @@ module type S = sig (* CR mshinwell: Add [bottom] here? Probably [is_bottom] too *) - val meet : meet_env -> t -> t -> (t * typing_env_extension) Or_bottom.t + val meet : meet_env -> t -> t -> (t, typing_env_extension) Meet_result.t (* Note that unlike the [join] function on regular types, for structures the return type is [t] (and not [t Or_unknown.t]). diff --git a/middle_end/flambda/types/template/flambda_type.templ.ml b/middle_end/flambda/types/template/flambda_type.templ.ml index a324eb0d5671..999f6ef4c325 100644 --- a/middle_end/flambda/types/template/flambda_type.templ.ml +++ b/middle_end/flambda/types/template/flambda_type.templ.ml @@ -35,7 +35,7 @@ include Type_grammar type flambda_type = t -let meet env t1 t2 : _ Or_bottom.t = +let meet env t1 t2 : _ Meet_result.t = let meet_env = Meet_env.create env in meet meet_env t1 t2 diff --git a/middle_end/flambda/types/type_descr.rec.ml b/middle_end/flambda/types/type_descr.rec.ml index 33a138e0b7f2..1fc263acbc07 100644 --- a/middle_end/flambda/types/type_descr.rec.ml +++ b/middle_end/flambda/types/type_descr.rec.ml @@ -137,7 +137,7 @@ module Make (Head : Type_head_intf.S | Some simple -> Ok (create_equals simple) end | No_alias Unknown -> Ok t - | No_alias Bottom -> Bottom + | No_alias Bottom -> Ok t | No_alias (Ok head) -> Or_bottom.map (Head.apply_coercion head coercion) ~f:(fun head -> create head) @@ -276,24 +276,18 @@ module Make (Head : Type_head_intf.S let head2 = expand_head ~force_to_kind right_ty right_env kind in canonical_simple1, head1, canonical_simple2, head2 - type meet_or_join_head_or_unknown_or_bottom_result = - | Left_head_unchanged - | Right_head_unchanged - | New_head of Head.t Or_unknown_or_bottom.t * TEE.t - let meet_head_or_unknown_or_bottom (env : Meet_env.t) (head1 : _ Or_unknown_or_bottom.t) (head2 : _ Or_unknown_or_bottom.t) - : meet_or_join_head_or_unknown_or_bottom_result = + : _ Meet_result.t = match head1, head2 with - | _, Unknown -> Left_head_unchanged - | Unknown, _ -> Right_head_unchanged - | Bottom, _ -> Left_head_unchanged - | _, Bottom -> Right_head_unchanged + | Unknown, Unknown -> Ok (Both_inputs, TEE.empty ()) + | _, Unknown -> Ok (Left_input, TEE.empty ()) + | Unknown, _ -> Ok (Right_input, TEE.empty ()) + | Bottom, _ -> Bottom + | _, Bottom -> Bottom | Ok head1, Ok head2 -> - match Head.meet env head1 head2 with - | Ok (head, env_extension) -> New_head (Ok head, env_extension) - | Bottom -> New_head (Bottom, TEE.empty ()) + Head.meet env head1 head2 let join_head_or_unknown_or_bottom (env : Join_env.t) (head1 : _ Or_unknown_or_bottom.t) @@ -335,7 +329,7 @@ module Make (Head : Type_head_intf.S which is just the same as that already in the environment. This shouldn't have been emitted from [meet]. *) - let meet ~force_to_kind ~to_type env kind ty1 ty2 t1 t2 : _ Or_bottom.t = + let meet ~force_to_kind ~to_type env kind t1 t2 : _ Meet_result.t = let typing_env = Meet_env.env env in let head1 = expand_head ~force_to_kind t1 typing_env kind in let head2 = expand_head ~force_to_kind t2 typing_env kind in @@ -350,33 +344,28 @@ module Make (Head : Type_head_intf.S with | exception Not_found -> begin match meet_head_or_unknown_or_bottom env head1 head2 with - | Left_head_unchanged -> Ok (ty1, TEE.empty ()) - | Right_head_unchanged -> Ok (ty2, TEE.empty ()) - | New_head (head, env_extension) -> - match head with - | Bottom -> Bottom - | Unknown -> Ok (to_type (unknown ()), env_extension) - | Ok head -> Ok (to_type (create head), env_extension) + | Bottom -> Bottom + | (Ok ((Left_input | Right_input | Both_inputs), _) as r) -> r + | Ok (New_result head, env_extension) -> + Ok (New_result (to_type (create head)), env_extension) end | simple2 -> begin match meet_head_or_unknown_or_bottom env head1 head2 with - | Left_head_unchanged -> + | Ok (Left_input, ext) -> let env_extension = - TEE.empty () + ext |> add_equation env simple2 (create_no_alias head1) ~to_type in - Ok (to_type (create_equals simple2), env_extension) - | Right_head_unchanged -> - Ok (to_type (create_equals simple2), TEE.empty ()) - | New_head (head, env_extension) -> + Ok (Right_input, env_extension) + | Ok ((Right_input | Both_inputs), ext) -> + Ok (Right_input, ext) + | Ok (New_result head, env_extension) -> let env_extension = env_extension - |> add_equation env simple2 (create_no_alias head) ~to_type + |> add_equation env simple2 (create head) ~to_type in - match head with - | Bottom -> Bottom - | Unknown | Ok _ -> - Ok (to_type (create_equals simple2), env_extension) + Ok (Right_input, env_extension) + | Bottom -> Bottom end end | simple1 -> @@ -386,23 +375,21 @@ module Make (Head : Type_head_intf.S with | exception Not_found -> begin match meet_head_or_unknown_or_bottom env head1 head2 with - | Left_head_unchanged -> - Ok (to_type (create_equals simple1), TEE.empty ()) - | Right_head_unchanged -> + | Ok (Right_input, ext) -> let env_extension = - TEE.empty () + ext |> add_equation env simple1 ~to_type (create_no_alias head2) in - Ok (to_type (create_equals simple1), env_extension) - | New_head (head, env_extension) -> + Ok (Left_input, env_extension) + | Ok ((Left_input | Both_inputs), ext) -> + Ok (Left_input, ext) + | Ok (New_result head, env_extension) -> let env_extension = env_extension - |> add_equation env simple1 ~to_type (create_no_alias head) + |> add_equation env simple1 ~to_type (create head) in - match head with - | Bottom -> Bottom - | Unknown | Ok _ -> - Ok (to_type (create_equals simple1), env_extension) + Ok (Left_input, env_extension) + | Bottom -> Bottom end | simple2 -> if Simple.equal simple1 simple2 @@ -411,7 +398,7 @@ module Make (Head : Type_head_intf.S (* This produces "=simple" for the output rather than a type that might need transformation back from an expanded head (as would happen if we used the next case). *) - Ok (to_type (create_equals simple1), TEE.empty ()) + Ok (Both_inputs, TEE.empty ()) end else begin assert (not (Simple.equal simple1 simple2)); let env = Meet_env.now_meeting env simple1 simple2 in @@ -422,33 +409,33 @@ module Make (Head : Type_head_intf.S (* CR mshinwell: May be able to improve efficiency by not doing [meet] again (via [TE.add_env_extension]) if we tried here to emit the equations the correct way around *) + (* Format.eprintf "Type_descr.meet:@.Head1 =@ %a@.Head2 =@ %a@." + * Descr.print (Descr.No_alias head1) Descr.print (Descr.No_alias head2); *) match meet_head_or_unknown_or_bottom env head1 head2 with - | Left_head_unchanged -> + (* Note: in the case where both heads are equal, we arbitrarily + pick the left side as the unchanged one. + Since for the other side we actually add an alias, it would be + wrong to claim that Both_inputs are returned. *) + | Ok ((Left_input | Both_inputs), ext) -> let env_extension = - TEE.empty () + ext |> add_equation env simple2 ~to_type (create_equals simple1) in - Ok (to_type (create_equals simple1), env_extension) - | Right_head_unchanged -> + Ok (Left_input, env_extension) + | Ok (Right_input, ext) -> let env_extension = - TEE.empty () + ext |> add_equation env simple1 ~to_type (create_equals simple2) in - Ok (to_type (create_equals simple2), env_extension) - | New_head (head, env_extension) -> + Ok (Right_input, env_extension) + | Ok (New_result head, env_extension) -> let env_extension = env_extension - |> add_equation env simple1 ~to_type (create_no_alias head) + |> add_equation env simple1 ~to_type (create head) |> add_equation env simple2 ~to_type (create_equals simple1) in - (* It makes things easier (to check if the result of [meet] was - bottom) to not return "=simple" in the bottom case. This is ok - because no constraint is being dropped; the type cannot be - refined any further. *) - match head with - | Bottom -> Bottom - | Unknown | Ok _ -> - Ok (to_type (create_equals simple1), env_extension) + Ok (Left_input, env_extension) + | Bottom -> Bottom end let join ?bound_name ~force_to_kind ~to_type join_env kind _ty1 _ty2 t1 t2 @@ -483,8 +470,12 @@ module Make (Head : Type_head_intf.S | None, (Ok _ | Unknown), _, _ | _, _, None, (Ok _ | Unknown) -> Aliases.Alias_set.empty | Some simple1, _, _, Bottom -> + if (Typing_env.mem_simple (Join_env.target_join_env join_env) simple1) then () + else Misc.fatal_errorf "Missing simple %a in join target env" Simple.print simple1; Aliases.Alias_set.singleton simple1 | _, Bottom, Some simple2, _ -> + if (Typing_env.mem_simple (Join_env.target_join_env join_env) simple2) then () + else Misc.fatal_errorf "Missing simple %a in join target env" Simple.print simple2; Aliases.Alias_set.singleton simple2 | Some simple1, _, Some simple2, _ -> if Simple.same simple1 simple2 diff --git a/middle_end/flambda/types/type_descr_intf.ml b/middle_end/flambda/types/type_descr_intf.ml index 64b88c6a8eca..57a08b02e6ba 100644 --- a/middle_end/flambda/types/type_descr_intf.ml +++ b/middle_end/flambda/types/type_descr_intf.ml @@ -90,11 +90,9 @@ module type S = sig -> to_type:(t -> flambda_type) -> meet_env -> Flambda_kind.t - -> flambda_type - -> flambda_type -> t -> t - -> (flambda_type * typing_env_extension) Or_bottom.t + -> (flambda_type, typing_env_extension) Meet_result.t val join : ?bound_name:Name.t diff --git a/middle_end/flambda/types/type_grammar.rec.ml b/middle_end/flambda/types/type_grammar.rec.ml index 4553a407c045..3e6ab7a6a47f 100644 --- a/middle_end/flambda/types/type_grammar.rec.ml +++ b/middle_end/flambda/types/type_grammar.rec.ml @@ -486,7 +486,7 @@ let these_tagged_immediates0 ~no_alias imms : t = else Value (T_V.create_no_alias (Ok (Variant (Variant.create ~is_unique:false - ~immediates:(Known (these_naked_immediates imms)) + ~immediates:(Known (these_naked_immediates0 ~no_alias imms)) ~blocks:(Known (Row_like.For_blocks.create_bottom ())))))) let these_tagged_immediates imms = @@ -926,37 +926,37 @@ let meet env t1 t2 = match t1, t2 with | Value ty1, Value ty2 -> T_V.meet env - K.value t1 t2 ty1 ty2 + K.value ty1 ty2 ~force_to_kind:force_to_kind_value ~to_type:(fun ty -> Value ty) | Naked_immediate ty1, Naked_immediate ty2 -> T_NI.meet env - K.naked_immediate t1 t2 ty1 ty2 + K.naked_immediate ty1 ty2 ~force_to_kind:force_to_kind_naked_immediate ~to_type:(fun ty -> Naked_immediate ty) | Naked_float ty1, Naked_float ty2 -> T_Nf.meet env - K.naked_float t1 t2 ty1 ty2 + K.naked_float ty1 ty2 ~force_to_kind:force_to_kind_naked_float ~to_type:(fun ty -> Naked_float ty) | Naked_int32 ty1, Naked_int32 ty2 -> T_N32.meet env - K.naked_int32 t1 t2 ty1 ty2 + K.naked_int32 ty1 ty2 ~force_to_kind:force_to_kind_naked_int32 ~to_type:(fun ty -> Naked_int32 ty) | Naked_int64 ty1, Naked_int64 ty2 -> T_N64.meet env - K.naked_int64 t1 t2 ty1 ty2 + K.naked_int64 ty1 ty2 ~force_to_kind:force_to_kind_naked_int64 ~to_type:(fun ty -> Naked_int64 ty) | Naked_nativeint ty1, Naked_nativeint ty2 -> T_NN.meet env - K.naked_nativeint t1 t2 ty1 ty2 + K.naked_nativeint ty1 ty2 ~force_to_kind:force_to_kind_naked_nativeint ~to_type:(fun ty -> Naked_nativeint ty) | Rec_info ty1, Rec_info ty2 -> T_RI.meet env - K.rec_info t1 t2 ty1 ty2 + K.rec_info ty1 ty2 ~force_to_kind:force_to_kind_rec_info ~to_type:(fun ty -> Rec_info ty) | (Value _ | Naked_immediate _ | Naked_float _ | Naked_int32 _ diff --git a/middle_end/flambda/types/type_grammar.rec.mli b/middle_end/flambda/types/type_grammar.rec.mli index fde4c83bcb75..a7c8f0297ec7 100644 --- a/middle_end/flambda/types/type_grammar.rec.mli +++ b/middle_end/flambda/types/type_grammar.rec.mli @@ -212,7 +212,7 @@ val make_suitable_for_environment val expand_head : t -> Typing_env.t -> Resolved_type.t (** Greatest lower bound of two types. *) -val meet : Meet_env.t -> t -> t -> (t * Typing_env_extension.t) Or_bottom.t +val meet : Meet_env.t -> t -> t -> (t, Typing_env_extension.t) Meet_result.t (** Least upper bound of two types. *) val join diff --git a/middle_end/flambda/types/type_head_intf.ml b/middle_end/flambda/types/type_head_intf.ml index 1d5ef3ade5f3..a1c84e3c7b86 100644 --- a/middle_end/flambda/types/type_head_intf.ml +++ b/middle_end/flambda/types/type_head_intf.ml @@ -35,7 +35,7 @@ module type S = sig : meet_env -> t -> t - -> (t * typing_env_extension) Or_bottom.t + -> (t, typing_env_extension) Meet_result.t val join : join_env diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.ml index 9a410512198f..483b01f310d8 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_float0.rec.ml @@ -38,10 +38,9 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet _env t1 t2 : _ Or_bottom.t = - let t = Float.Set.inter t1 t2 in - if Float.Set.is_empty t then Bottom - else Ok (t, TEE.empty ()) +let meet _env t1 t2 = + Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module Float.Set) t1 t2 let join _env t1 t2 : _ Or_unknown.t = Known (Float.Set.union t1 t2) diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.ml index 06f3f26909df..82801a41f2e2 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_immediate0.rec.ml @@ -67,63 +67,93 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet env t1 t2 : _ Or_bottom.t = - match t1, t2 with - | Naked_immediates is1, Naked_immediates is2 -> - let is = I.Set.inter is1 is2 in - if I.Set.is_empty is then Bottom - else Ok (Naked_immediates is, TEE.empty ()) - | Is_int ty1, Is_int ty2 -> - Or_bottom.map (T.meet env ty1 ty2) - ~f:(fun (ty, env_extension) -> Is_int ty, env_extension) - | Get_tag ty1, Get_tag ty2 -> - Or_bottom.map (T.meet env ty1 ty2) - ~f:(fun (ty, env_extension) -> Get_tag ty, env_extension) - | Is_int ty, Naked_immediates is_int - | Naked_immediates is_int, Is_int ty -> - begin match I.Set.elements is_int with - | [] -> Bottom - | [is_int] -> - let shape = - if I.equal is_int I.zero then Some (T.any_block ()) - else if I.equal is_int I.one then Some (T.any_tagged_immediate ()) - else None - in - begin match shape with - | Some shape -> - Or_bottom.map - (T.meet env ty shape) - ~f:(fun (ty, env_extension) -> Is_int ty, env_extension) - | None -> Bottom - end - | _ :: _ :: _ -> - (* Note: we're potentially losing precision because the set could end up - not containing either 0 or 1 or both, but this should be uncommon. *) - Ok (Is_int ty, TEE.empty ()) +type side = Left | Right + +let meet env t1 t2 : _ Meet_result.t = + let keep_side side : _ Meet_result.t = + match side with + | Left -> Ok (Left_input, TEE.empty ()) + | Right -> Ok (Right_input, TEE.empty ()) + in + let keep_other_side side : _ Meet_result.t = + match side with + | Left -> Ok (Right_input, TEE.empty ()) + | Right -> Ok (Left_input, TEE.empty ()) + in + let is_int_immediate ~is_int_ty ~immediates ~is_int_side = + begin match I.Set.elements immediates with + | [] -> + (* Keep the type of the immediates, no extension *) + keep_other_side is_int_side + | [imm] -> + let shape = + if I.equal imm I.zero then Some (T.any_block ()) + else if I.equal imm I.one then Some (T.any_tagged_immediate ()) + else None + in + begin match shape with + | Some shape -> + Meet_result.map_result + (match is_int_side with + | Left -> T.meet env is_int_ty shape + | Right -> T.meet env shape is_int_ty) + ~f:(fun ty -> Is_int ty) + | None -> Meet_result.Bottom end - | Get_tag ty, Naked_immediates tags - | Naked_immediates tags, Get_tag ty -> + | _ :: _ :: _ -> + (* Note: we're potentially losing precision because the set could end up + not containing either 0 or 1 or both, but this should be uncommon. *) + keep_side is_int_side + end + in + let get_tag_immediate ~get_tag_ty ~immediates ~get_tag_side = + if I.Set.is_empty immediates then keep_other_side get_tag_side + else let tags = I.Set.fold (fun tag tags -> - match Target_imm.to_tag tag with - | Some tag -> Tag.Set.add tag tags - | None -> tags (* No blocks exist with this tag *)) - tags + match Target_imm.to_tag tag with + | Some tag -> Tag.Set.add tag tags + | None -> tags (* No blocks exist with this tag *)) + immediates Tag.Set.empty in - begin match T.blocks_with_these_tags tags with - | Known shape -> - Or_bottom.map - (T.meet env ty shape) - ~f:(fun (ty, env_extension) -> Get_tag ty, env_extension) - | Unknown -> - Ok (Get_tag ty, TEE.empty ()) - end - | (Is_int _ | Get_tag _), (Is_int _ | Get_tag _) -> - (* We can't return Bottom, as it would be unsound, so we need to either - do the actual meet with Naked_immediates, or just give up and return - one of the arguments. *) - Ok (t1, TEE.empty ()) + if Tag.Set.is_empty tags then Meet_result.Bottom + else + begin match T.blocks_with_these_tags tags with + | Known shape -> + Meet_result.map_result + (match get_tag_side with + | Left -> T.meet env get_tag_ty shape + | Right -> T.meet env shape get_tag_ty) + ~f:(fun ty -> Get_tag ty) + | Unknown -> keep_side get_tag_side + end + in + match t1, t2 with + | Naked_immediates is1, Naked_immediates is2 -> + Meet_result.map_result + (Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module I.Set) is1 is2) + ~f:(fun is -> Naked_immediates is) + | Is_int ty1, Is_int ty2 -> + Meet_result.map_result (T.meet env ty1 ty2) + ~f:(fun ty -> Is_int ty) + | Get_tag ty1, Get_tag ty2 -> + Meet_result.map_result (T.meet env ty1 ty2) + ~f:(fun ty -> Get_tag ty) + | Is_int is_int_ty, Naked_immediates immediates -> + is_int_immediate ~is_int_ty ~immediates ~is_int_side:Left + | Naked_immediates immediates, Is_int is_int_ty -> + is_int_immediate ~is_int_ty ~immediates ~is_int_side:Right + | Get_tag get_tag_ty, Naked_immediates immediates -> + get_tag_immediate ~get_tag_ty ~immediates ~get_tag_side:Left + | Naked_immediates immediates, Get_tag get_tag_ty -> + get_tag_immediate ~get_tag_ty ~immediates ~get_tag_side:Right + | (Is_int _ | Get_tag _), (Is_int _ | Get_tag _) -> + (* We can't return Bottom, as it would be unsound, so we need to either + do the actual meet with Naked_immediates, or just give up and return + one of the arguments. *) + Ok (Left_input, TEE.empty ()) let join env t1 t2 : _ Or_unknown.t = match t1, t2 with diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.ml index 97971212904f..895bd5388074 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int32_0.rec.ml @@ -38,10 +38,9 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet _env t1 t2 : _ Or_bottom.t = - let t = Int32.Set.inter t1 t2 in - if Int32.Set.is_empty t then Bottom - else Ok (t, TEE.empty ()) +let meet _env t1 t2 = + Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module Int32.Set) t1 t2 let join _env t1 t2 : _ Or_unknown.t = Known (Int32.Set.union t1 t2) diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.ml index f27d517cf0f8..26d527a0cf09 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_int64_0.rec.ml @@ -38,10 +38,9 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet _env t1 t2 : _ Or_bottom.t = - let t = Int64.Set.inter t1 t2 in - if Int64.Set.is_empty t then Bottom - else Ok (t, TEE.empty ()) +let meet _env t1 t2 = + Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module Int64.Set) t1 t2 let join _env t1 t2 : _ Or_unknown.t = Known (Int64.Set.union t1 t2) diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.ml index 04eaac4913d4..c82aff6a03eb 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_naked_nativeint0.rec.ml @@ -37,10 +37,9 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet _env t1 t2 : _ Or_bottom.t = - let t = Targetint.Set.inter t1 t2 in - if Targetint.Set.is_empty t then Bottom - else Ok (t, TEE.empty ()) +let meet _env t1 t2 = + Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module Targetint.Set) t1 t2 let join _env t1 t2 : _ Or_unknown.t = Known (Targetint.Set.union t1 t2) diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_rec_info0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_rec_info0.rec.ml index 8a4609716743..fc8ecc52a4e4 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_rec_info0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_rec_info0.rec.ml @@ -34,12 +34,12 @@ let apply_coercion t coercion : _ Or_bottom.t = let eviscerate _ : _ Or_unknown.t = Unknown -let meet _env t1 t2 : _ Or_bottom.t = +let meet _env t1 t2 : _ Meet_result.t = (* CR lmaurer: This could be doing things like discovering two depth variables are equal *) if Rec_info_expr.equal t1 t2 then - Ok (t1, Typing_env_extension.empty ()) - else Bottom + Ok (Both_inputs, Typing_env_extension.empty ()) + else Bottom (* CR vlaviron: this looks obviously wrong *) let join _env t1 t2 : _ Or_unknown.t = if Rec_info_expr.equal t1 t2 then Known t1 else Unknown diff --git a/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml b/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml index a63b6ce25f86..9f3c7c5924eb 100644 --- a/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml +++ b/middle_end/flambda/types/type_of_kind/type_of_kind_value0.rec.ml @@ -189,26 +189,30 @@ let eviscerate t : _ Or_unknown.t = let meet_unknown meet_contents ~contents_is_bottom env (or_unknown1 : _ Or_unknown.t) (or_unknown2 : _ Or_unknown.t) - : ((_ Or_unknown.t) * TEE.t) Or_bottom.t = + : (_ Or_unknown.t, TEE.t) Meet_result.t = match or_unknown1, or_unknown2 with - | Unknown, Unknown -> Ok (Unknown, TEE.empty ()) + | Unknown, Unknown -> Ok (Both_inputs, TEE.empty ()) (* CR mshinwell: Think about the next two cases more *) - | Known contents, _ when contents_is_bottom contents -> Bottom - | _, Known contents when contents_is_bottom contents -> Bottom - | _, Unknown -> Ok (or_unknown1, TEE.empty ()) - | Unknown, _ -> Ok (or_unknown2, TEE.empty ()) + (* vlaviron: When at least one of the inputs is bottom we + will return a bottom value, but we can choose whether we want to + return the Bottom constructor directly or merely which inputs + are bottom. I chose the second version, because it allows the + meet_variant function to correctly propagate which input is + unchanged without calling is_bottom again. *) + | Known contents, _ when contents_is_bottom contents -> + begin match or_unknown2 with + | Known contents when contents_is_bottom contents -> + Ok (Both_inputs, TEE.empty ()) + | _ -> + Ok (Left_input, TEE.empty ()) + end + | _, Known contents when contents_is_bottom contents -> + Ok (Right_input, TEE.empty ()) + | _, Unknown -> Ok (Left_input, TEE.empty ()) + | Unknown, _ -> Ok (Right_input, TEE.empty ()) | Known contents1, Known contents2 -> - let result = - Or_bottom.map (meet_contents env contents1 contents2) - ~f:(fun (contents, env_extension) -> - Or_unknown.Known contents, env_extension) - in - match result with - | Bottom | Ok (Unknown, _) -> result - | Ok (Known contents, _env_extension) -> - (* XXX Why isn't [meet_contents] returning bottom? *) - if contents_is_bottom contents then Bottom - else result + Meet_result.map_result (meet_contents env contents1 contents2) + ~f:(fun contents -> Or_unknown.Known contents) let join_unknown join_contents (env : Join_env.t) (or_unknown1 : _ Or_unknown.t) (or_unknown2 : _ Or_unknown.t) @@ -220,96 +224,123 @@ let join_unknown join_contents (env : Join_env.t) join_contents env contents1 contents2 let meet_variant env - ~blocks1 ~imms1 ~blocks2 ~imms2 : _ Or_bottom.t = + ~blocks1 ~imms1 ~blocks2 ~imms2 : _ Meet_result.t = + let blocks_is_bottom blocks = + match (blocks : _ Or_unknown.t) with + | Unknown -> false + | Known blocks -> Blocks.is_bottom blocks + in + let immediates_is_bottom immediates = + match (immediates : _ Or_unknown.t) with + | Unknown -> false + | Known imms -> T.is_obviously_bottom imms + in let blocks = meet_unknown Blocks.meet ~contents_is_bottom:Blocks.is_bottom env blocks1 blocks2 in - let blocks : _ Or_bottom.t = - (* XXX Clean this up *) - match blocks with - | Bottom | Ok (Or_unknown.Unknown, _) -> blocks - | Ok (Or_unknown.Known blocks', _) -> - if Blocks.is_bottom blocks' then Bottom else blocks - in let imms = meet_unknown T.meet ~contents_is_bottom:T.is_obviously_bottom env imms1 imms2 in - let imms : _ Or_bottom.t = - match imms with - | Bottom | Ok (Or_unknown.Unknown, _) -> imms - | Ok (Or_unknown.Known imms', _) -> - if T.is_obviously_bottom imms' then Bottom else imms - in match blocks, imms with + (* CR vlaviron: Note on the Bottom cases: + We're only expecting the underlying meets to return Bottom if + neither input was already Bottom (otherwise, we would have gotten + one of Both_inputs, Left_input or Right_input). + Since we want to return Bottom rather than New_result in the case + where the returned type is bottom, we check for bottom results + in the cases where it can occur. + *) | Bottom, Bottom -> Bottom | Ok (blocks, env_extension), Bottom -> let immediates : _ Or_unknown.t = Known (T.bottom K.naked_immediate) in - Ok (blocks, immediates, env_extension) + let blocks = Meet_result.extract_value blocks blocks1 blocks2 in + if blocks_is_bottom blocks then + Bottom + else + Ok (New_result (blocks, immediates), env_extension) | Bottom, Ok (immediates, env_extension) -> let blocks : _ Or_unknown.t = Known (Blocks.create_bottom ()) in - Ok (blocks, immediates, env_extension) - | Ok (blocks, env_extension1), Ok (immediates, env_extension2) -> - begin match (blocks : _ Or_unknown.t) with - | Unknown -> () - | Known blocks -> assert (not (Blocks.is_bottom blocks)); - end; - begin match (immediates : _ Or_unknown.t) with - | Unknown -> () - | Known imms -> assert (not (T.is_obviously_bottom imms)); - end; + let immediates = Meet_result.extract_value immediates imms1 imms2 in + if immediates_is_bottom immediates then + Bottom + else + Ok (New_result (blocks, immediates), env_extension) + | Ok (blocks_res, env_extension1), Ok (immediates_res, env_extension2) -> + let blocks = Meet_result.extract_value blocks_res blocks1 blocks2 in + let immediates = Meet_result.extract_value immediates_res imms1 imms2 in + let bottom_blocks = blocks_is_bottom blocks in + let bottom_immediates = immediates_is_bottom immediates in let env_extension = - let env = Meet_env.env env in - let join_env = - Join_env.create env ~left_env:env ~right_env:env - in - TEE.join join_env env_extension1 env_extension2 + if bottom_immediates then env_extension1 + else if bottom_blocks then env_extension2 + else + let env = Meet_env.env env in + let join_env = + Join_env.create env ~left_env:env ~right_env:env + in + TEE.join join_env env_extension1 env_extension2 in - Ok (blocks, immediates, env_extension) + begin match blocks_res, immediates_res with + | Both_inputs, Both_inputs -> + Ok (Both_inputs, env_extension) + | (Left_input | Both_inputs), (Left_input | Both_inputs) -> + Ok (Left_input, env_extension) + | (Right_input | Both_inputs), (Right_input | Both_inputs) -> + Ok (Right_input, env_extension) + | Left_input, Right_input + | Right_input, Left_input + | New_result _, _ + | _, New_result _ -> + if bottom_blocks && bottom_immediates then + Bottom + else + Ok (New_result (blocks, immediates), env_extension) + end -let meet env t1 t2 : _ Or_bottom.t = +let meet env t1 t2 : _ Meet_result.t = match t1, t2 with | Variant { blocks = blocks1; immediates = imms1; is_unique = is_unique1; }, Variant { blocks = blocks2; immediates = imms2; is_unique = is_unique2; } -> - Or_bottom.map + Meet_result.map_result (meet_variant env ~blocks1 ~imms1 ~blocks2 ~imms2) - ~f:(fun (blocks, immediates, env_extension) -> + ~f:(fun (blocks, immediates) -> (* Uniqueness tracks whether duplication/lifting is allowed. It must always be propagated, both for meet and join. *) let is_unique = is_unique1 || is_unique2 in - Variant (Variant.create ~is_unique ~blocks ~immediates), env_extension) + Variant (Variant.create ~is_unique ~blocks ~immediates)) | Boxed_float n1, Boxed_float n2 -> - Or_bottom.map + Meet_result.map_result (T.meet env n1 n2) - ~f:(fun (n, env_extension) -> Boxed_float n, env_extension) + ~f:(fun n -> Boxed_float n) | Boxed_int32 n1, Boxed_int32 n2 -> - Or_bottom.map + Meet_result.map_result (T.meet env n1 n2) - ~f:(fun (n, env_extension) -> Boxed_int32 n, env_extension) + ~f:(fun n -> Boxed_int32 n) | Boxed_int64 n1, Boxed_int64 n2 -> - Or_bottom.map + Meet_result.map_result (T.meet env n1 n2) - ~f:(fun (n, env_extension) -> Boxed_int64 n, env_extension) + ~f:(fun n -> Boxed_int64 n) | Boxed_nativeint n1, Boxed_nativeint n2 -> - Or_bottom.map + Meet_result.map_result (T.meet env n1 n2) - ~f:(fun (n, env_extension) -> Boxed_nativeint n, env_extension) + ~f:(fun n -> Boxed_nativeint n) | Closures { by_closure_id = by_closure_id1; }, Closures { by_closure_id = by_closure_id2; } -> let module C = Row_like.For_closures_entry_by_set_of_closures_contents in - Or_bottom.map + Meet_result.map_result (C.meet env by_closure_id1 by_closure_id2) - ~f:(fun (by_closure_id, env_extension) -> - Closures { by_closure_id; }, env_extension) + ~f:(fun by_closure_id -> Closures { by_closure_id; }) | String strs1, String strs2 -> - let strs = String_info.Set.inter strs1 strs2 in - if String_info.Set.is_empty strs then Bottom - else Or_bottom.Ok (String strs, TEE.empty ()) + Meet_result.map_result + (Meet_result.set_meet ~no_extension:(TEE.empty ()) + (module String_info.Set) strs1 strs2) + ~f:(fun strs -> String strs) | Array { length = length1; }, Array { length = length2; } -> - Or_bottom.map + Meet_result.map_result (T.meet env length1 length2) - ~f:(fun (length, env_extension) -> Array { length; }, env_extension) + ~f:(fun length -> Array { length; }) | (Variant _ | Boxed_float _ | Boxed_int32 _