From daede1becb268d9b5b77bf7e8a116f04369018dc Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Wed, 17 Feb 2021 15:47:00 +0100 Subject: [PATCH 1/8] Improved debugging for invariant on canonical aliases --- .../flambda/types/env/typing_env.rec.ml | 28 +++++++++++-------- 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/middle_end/flambda/types/env/typing_env.rec.ml b/middle_end/flambda/types/env/typing_env.rec.ml index bdd88026d03a..dd7cc4b93725 100644 --- a/middle_end/flambda/types/env/typing_env.rec.ml +++ b/middle_end/flambda/types/env/typing_env.rec.ml @@ -934,18 +934,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; From b52fe696bb77b0260df8cca880c4f2ab17825bda Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Wed, 17 Feb 2021 16:07:08 +0100 Subject: [PATCH 2/8] Rework of meet functions: - Introduce a module Meet_result, which allows tracking whether the result the same as one of the arguments or actually more precise. This is used to guarantee that infinite recursive meets are impossible. - Make the functions add_equation and add_env_extension from Tying_env systematically meet the equations. This required patching the join algorithm in Typing_env_level to use these function correctly. - Error when bottom equations are added to the environment. The environment is equivalent to bottom whenever a single of its equations is bottom, so no bottom equations should be added to it. For equations coming from meet, the meet itself can return Bottom. For other equations, the caller must correctly handle the bottom cases before adding the equation. --- .depend | 41 ++++- compilerlibs/Makefile.compilerlibs | 1 + flambdatest/api_tests/Makefile | 2 +- flambdatest/api_tests/join_tests.ml | 89 ++++++++++ flambdatest/mlexamples/alias_bug.ml | 22 +++ middle_end/flambda/lifting/reification.ml | 3 +- middle_end/flambda/types/basic/meet_result.ml | 50 ++++++ .../flambda/types/basic/meet_result.mli | 48 +++++ .../flambda/types/env/typing_env.rec.ml | 36 ++-- .../types/env/typing_env_extension.rec.ml | 15 +- .../types/env/typing_env_extension.rec.mli | 2 + middle_end/flambda/types/flambda_type.mli | 2 +- .../types/structures/closures_entry.rec.ml | 81 +++++++-- .../function_declaration_type.rec.ml | 45 +++-- .../flambda/types/structures/product.rec.ml | 56 +++++- .../flambda/types/structures/row_like.rec.ml | 96 ++++++++-- .../types/structures/type_structure_intf.ml | 2 +- .../types/template/flambda_type.templ.ml | 2 +- middle_end/flambda/types/type_descr.rec.ml | 111 ++++++------ middle_end/flambda/types/type_descr_intf.ml | 4 +- middle_end/flambda/types/type_grammar.rec.ml | 14 +- middle_end/flambda/types/type_grammar.rec.mli | 2 +- middle_end/flambda/types/type_head_intf.ml | 2 +- .../type_of_kind_naked_float0.rec.ml | 7 +- .../type_of_kind_naked_immediate0.rec.ml | 134 ++++++++------ .../type_of_kind_naked_int32_0.rec.ml | 7 +- .../type_of_kind_naked_int64_0.rec.ml | 7 +- .../type_of_kind_naked_nativeint0.rec.ml | 7 +- .../type_of_kind/type_of_kind_value0.rec.ml | 167 +++++++++++------- 29 files changed, 767 insertions(+), 288 deletions(-) create mode 100644 flambdatest/api_tests/join_tests.ml create mode 100644 flambdatest/mlexamples/alias_bug.ml create mode 100644 middle_end/flambda/types/basic/meet_result.ml create mode 100644 middle_end/flambda/types/basic/meet_result.mli 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/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 dd7cc4b93725..b1ef1f53e8f8 100644 --- a/middle_end/flambda/types/env/typing_env.rec.ml +++ b/middle_end/flambda/types/env/typing_env.rec.ml @@ -1101,14 +1101,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 @@ -1198,8 +1198,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..0e9091e52385 100644 --- a/middle_end/flambda/types/structures/product.rec.ml +++ b/middle_end/flambda/types/structures/product.rec.ml @@ -62,24 +62,39 @@ 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') -> + | 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; - Some ty + 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; @@ -88,7 +103,12 @@ module Make (Index : Product_intf.Index) = struct 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 +224,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 +233,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 = @@ -228,14 +250,27 @@ module Int_indexed = struct | Some t, None | None, Some t -> 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 +278,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..7f15faf1d137 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,10 @@ module Make (Head : Type_head_intf.S | None, (Ok _ | Unknown), _, _ | _, _, None, (Ok _ | Unknown) -> Aliases.Alias_set.empty | Some simple1, _, _, Bottom -> + assert (Typing_env.mem_simple (Join_env.target_join_env join_env) simple1); Aliases.Alias_set.singleton simple1 | _, Bottom, Some simple2, _ -> + assert (Typing_env.mem_simple (Join_env.target_join_env join_env) 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..d04e0598172c 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,32 +926,32 @@ 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 -> 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_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 _ From 1f35a5fb046fb1c83a18ee2567f95137632353e7 Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Wed, 17 Feb 2021 17:18:14 +0100 Subject: [PATCH 3/8] Improve error message in Type_descr.join --- middle_end/flambda/types/type_descr.rec.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/middle_end/flambda/types/type_descr.rec.ml b/middle_end/flambda/types/type_descr.rec.ml index 7f15faf1d137..1fc263acbc07 100644 --- a/middle_end/flambda/types/type_descr.rec.ml +++ b/middle_end/flambda/types/type_descr.rec.ml @@ -470,10 +470,12 @@ module Make (Head : Type_head_intf.S | None, (Ok _ | Unknown), _, _ | _, _, None, (Ok _ | Unknown) -> Aliases.Alias_set.empty | Some simple1, _, _, Bottom -> - assert (Typing_env.mem_simple (Join_env.target_join_env join_env) simple1); + 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, _ -> - assert (Typing_env.mem_simple (Join_env.target_join_env join_env) 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 From 8c1330a84c35d46c36068f769a5a81144cc0dac7 Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Wed, 17 Feb 2021 17:18:53 +0100 Subject: [PATCH 4/8] Allow Typing_env.mem to consider symbols present even if their cmx is missing --- middle_end/flambda/types/env/typing_env.rec.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/middle_end/flambda/types/env/typing_env.rec.ml b/middle_end/flambda/types/env/typing_env.rec.ml index b1ef1f53e8f8..d01a7755230d 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 From bb0e1d4ac1d68ceb23e52289bec149ed105f9584 Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Thu, 18 Feb 2021 15:23:39 +0100 Subject: [PATCH 5/8] Fix Product meet functions with mismatched domains --- .../flambda/types/structures/product.rec.ml | 65 ++++++++++++------- 1 file changed, 40 insertions(+), 25 deletions(-) diff --git a/middle_end/flambda/types/structures/product.rec.ml b/middle_end/flambda/types/structures/product.rec.ml index 0e9091e52385..07988dee52b5 100644 --- a/middle_end/flambda/types/structures/product.rec.ml +++ b/middle_end/flambda/types/structures/product.rec.ml @@ -72,33 +72,43 @@ module Make (Index : Product_intf.Index) = struct 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 (meet_result, 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; - 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)) + end) components_by_index1 components_by_index2 in @@ -247,7 +257,12 @@ 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 (meet_result, env_extension') -> From 0a951b454f9a8ac3cb20901179aa57975d871992 Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Mon, 7 Jun 2021 14:42:02 +0200 Subject: [PATCH 6/8] Relax restriction on Bottom equations --- middle_end/flambda/types/env/typing_env.rec.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/middle_end/flambda/types/env/typing_env.rec.ml b/middle_end/flambda/types/env/typing_env.rec.ml index d01a7755230d..ef3d48c1f94b 100644 --- a/middle_end/flambda/types/env/typing_env.rec.ml +++ b/middle_end/flambda/types/env/typing_env.rec.ml @@ -1212,15 +1212,15 @@ let meet_equations_on_params t ~params ~param_types = 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) *) + (* 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 From cb097e0a0a74758aba3e8bf61537b56d1170f27a Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Mon, 7 Jun 2021 15:02:21 +0200 Subject: [PATCH 7/8] Fix meet_test.ml --- middle_end/flambda/tests/meet_test.ml | 34 +++++++++++++++++++-------- 1 file changed, 24 insertions(+), 10 deletions(-) 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; From 11da2030e31c8fab933950604a54f945f3dc89fa Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Tue, 22 Jun 2021 16:44:24 +0200 Subject: [PATCH 8/8] Rebase fix for Rec_info stuff --- middle_end/flambda/types/type_grammar.rec.ml | 2 +- .../types/type_of_kind/type_of_kind_rec_info0.rec.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/middle_end/flambda/types/type_grammar.rec.ml b/middle_end/flambda/types/type_grammar.rec.ml index d04e0598172c..3e6ab7a6a47f 100644 --- a/middle_end/flambda/types/type_grammar.rec.ml +++ b/middle_end/flambda/types/type_grammar.rec.ml @@ -956,7 +956,7 @@ let meet env t1 t2 = ~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_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